private void checkProofStep(final Token token) throws ExpressionException, ScannerException, VerifyException {
		// expression?
		if (token.getTokenClass() == Token.Class.BEGIN_EXP) {
			feed.putToken(token);
			mandatoryStack.push(expressionFactory.createExpression(module, feed));
			if (logger.isDebugEnabled())
				logger.debug("Proof object: " + mandatoryStack.peek());
			return;
		}
		assert (token.getTokenClass() == Token.Class.ATOM): "Wrong token class";
		final String label = token.getTokenString();
		// hypothesis?
		if (hypotheses.containsKey(label)) {
			if (!mandatoryStack.empty()) {
				feed.reject("Proof step " + label + " is a hypothesis but mandatory variable stack is not "
						+ "empty. (Remember to place mandatory terms after the hypotheses!)");
				logger.debug("Proof stack:     " + proofStack);
				logger.debug("Mandatory stack: " + mandatoryStack);
				throw new VerifyException("Proof step is a hypothesis but mandatory variable stack is not "
						+ "empty.");
			}
			proofStack.push(hypotheses.get(label).totalUnfold());
			if (logger.isDebugEnabled())
				logger.debug("Proof object: " + proofStack.peek());
			feed.confirmLabel();
			return;
		}
		// label must be symbol now
		final Symbol symbol = symbolNamespace.getObjectByString(label);
		if (logger.isDebugEnabled())
			logger.debug("Proof object: " + symbol);
		if (symbol == null) {
			feed.reject("Proof step is neither a symbol nor a hypothesis: " + label);
			throw new VerifyException("Proof step is neither a symbol nor a hypothesis");
		}
		// variable?
		if (symbol.isVariable()) {
			mandatoryStack.push(expressionFactory.createExpression((Variable) symbol));
			feed.confirmVar();
			return;
		}
		// Aha, Statement!
		checkStatement((Statement) symbol);
		feed.confirmStatement();
	}