final Element current = resolver.getNormalizedFormula(element);
        if (substFunc.getSubstituteTerm() == null) {
            ok = false;
            handleProofCheckException(
                BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_CODE,
                BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_TEXT,
                getCurrentContext());
            return ok;
        }
        final Element sigma = resolver.getNormalizedFormula(substFunc.getFunctionVariable());
        final Element tau = resolver.getNormalizedFormula(substFunc.getSubstituteTerm());
        final Element expected = FormulaUtility.replaceOperatorVariable(alpha, sigma, tau);
        if (!EqualsUtility.equals(current, expected)) {
            ok = false;
            handleProofCheckException(
                BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
                BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
                + substFunc.getReference(),
                getDiffModuleContextOfProofLineFormula(i, expected));
            return ok;
        }
        // check precondition: function variable $\sigma$ must have n pairwise different free
        // subject variables as arguments
        final ElementSet funcFree = FormulaUtility.getFreeSubjectVariables(sigma);
        if (funcFree.size() != sigma.getList().size() - 1) {
            ok = false;
            setLocationWithinModule(context + ".getPredicateVariable()");
            handleProofCheckException(
                BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
                BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
                getDiffModuleContextOfProofLineFormula(i, expected));
            return ok;
        }
        for (int j = 1; j < sigma.getList().size(); j++) {
            if (!FormulaUtility.isSubjectVariable(sigma.getList().getElement(j))) {
                ok = false;
                setLocationWithinModule(context + ".getPredicateVariable()");
                handleProofCheckException(
                    BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
                    BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
                    getCurrentContext());
                return ok;
            }
        }
        // check precondition: the free variables of $\tau(x_1, \ldots, x_n)$
        // without $x_1$, \ldots, $x_n$ do not occur as bound variables in $\alpha$
        final ElementSet fBound = FormulaUtility.getBoundSubjectVariables(alpha);
        final ElementSet sigmaFree = FormulaUtility.getFreeSubjectVariables(tau);
        if (!fBound.intersection(sigmaFree.minus(funcFree)).isEmpty()) {
            ok = false;
            setLocationWithinModule(context + ".getSubstituteFormula()");
            handleProofCheckException(
                BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_CODE,
                BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_TEXT,
                getCurrentContext());
            return ok;
        }
        // check precondition: each occurrence of $\sigma(t_1, \ldots, t_n)$ in $\alpha$
        // contains no bound variable of $\tau(x_1, \ldots, x_n)$
        final ElementSet sigmaBound = FormulaUtility.getBoundSubjectVariables(tau);
        if (!FormulaUtility.testOperatorVariable(alpha, sigma, sigmaBound)) {
            ok = false;
            setLocationWithinModule(context + ".getSubstituteFormula()");
            handleProofCheckException(
                BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_CODE,
                BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_TEXT,
                getCurrentContext());
            return ok;
        }

        final Element current = resolver.getNormalizedFormula(element);
        if (substPred.getSubstituteFormula() == null) {
            ok = false;
            handleProofCheckException(
                BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_CODE,
                BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_TEXT,
                getCurrentContext());
            return ok;
        }
        final Element p = resolver.getNormalizedFormula(substPred.getPredicateVariable());
        final Element beta = resolver.getNormalizedFormula(substPred.getSubstituteFormula());
        final Element expected = FormulaUtility.replaceOperatorVariable(alpha, p, beta);
        if (!EqualsUtility.equals(current, expected)) {
            ok = false;
            handleProofCheckException(
                BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
                BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
                + substPred.getReference(),
                getDiffModuleContextOfProofLineFormula(i, expected));
            return ok;
        }
        // check precondition: predicate variable p must have n pairwise different free subject
        // variables as arguments
        final ElementSet predFree = FormulaUtility.getFreeSubjectVariables(p);
        if (predFree.size() != p.getList().size() - 1) {
            ok = false;
            setLocationWithinModule(context + ".getPredicateVariable()");
            handleProofCheckException(
                BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
                BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
                getDiffModuleContextOfProofLineFormula(i, expected));
            return ok;
        }
        for (int j = 1; j < p.getList().size(); j++) {
            if (!FormulaUtility.isSubjectVariable(p.getList().getElement(j))) {
                ok = false;
                setLocationWithinModule(context + ".getPredicateVariable()");
                handleProofCheckException(
                    BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
                    BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
                    getCurrentContext());
                return ok;
            }
        }
        // check precondition: the free variables of $\beta(x_1, \ldots, x_n)$ without
        // $x_1$, \ldots, $x_n$ do not occur as bound variables in $\alpha$
        final ElementSet fBound = FormulaUtility.getBoundSubjectVariables(alpha);
        final ElementSet betaFree = FormulaUtility.getFreeSubjectVariables(beta);
        if (!fBound.intersection(betaFree.minus(predFree)).isEmpty()) {
            ok = false;
            setLocationWithinModule(context + ".getSubstituteFormula()");
            handleProofCheckException(
                BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_CODE,
                BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_TEXT,
                getCurrentContext());
            return ok;
        }
        // check precondition: each occurrence of $p(t_1, \ldots, t_n)$ in $\alpha$ contains
        // no bound variable of $\beta(x_1, \ldots, x_n)$
        final ElementSet betaBound = FormulaUtility.getBoundSubjectVariables(beta);
        if (!FormulaUtility.testOperatorVariable(alpha, p, betaBound)) {
            ok = false;
            setLocationWithinModule(context + ".getSubstituteFormula()");
            handleProofCheckException(
                BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_CODE,
                BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_TEXT,
                getCurrentContext());
            return ok;
        }

            }

            // check if only defined rules are used
            // TODO 20110316 m31: this is a dirty trick to get the context of the reason
            //                    perhaps we can solve this more elegantly?
            String getReason = ".get" + StringUtility.getClassName(reason.getClass());
            if (getReason.endsWith("Vo")) {
                getReason = getReason.substring(0, getReason.length() - 2) + "()";
                setLocationWithinModule(context + ".get(" + i + ").getReason()"
                    + getReason);
//                System.out.println(getCurrentContext());
            }
            if (reason instanceof Add) {
                ok = check((Add) reason, i, line.getFormula().getElement());
            } else if (reason instanceof Rename) {
                ok = check((Rename) reason, i, line.getFormula().getElement());
            } else if (reason instanceof ModusPonens) {
                ok = check((ModusPonens) reason, i, line.getFormula().getElement());
            } else if (reason instanceof SubstFree) {
                ok = check((SubstFree) reason, i, line.getFormula().getElement());
            } else if (reason instanceof SubstPred) {
                ok = check((SubstPred) reason, i, line.getFormula().getElement());
            } else if (reason instanceof SubstFunc) {
                ok = check((SubstFunc) reason, i, line.getFormula().getElement());
            } else if (reason instanceof Universal) {
                ok = check((Universal) reason, i, line.getFormula().getElement());
            } else if (reason instanceof Existential) {
                ok = check((Existential) reason, i, line.getFormula().getElement());
            } else if (reason instanceof ConditionalProof) {

            definition = new PredicateDefinitionVo();
            definition.setArgumentNumber(attributes.getString("arguments"));
            definition.setName(attributes.getString("name"));
        } else if ("LATEXPATTERN".equals(name)) {
            // nothing to do yet
        } else if (formulaHandler.getStartTag().equals(name)) {
            changeHandler(formulaHandler, name, attributes);
        } else if (descriptionHandler.getStartTag().equals(name)) {
            changeHandler(descriptionHandler, name, attributes);
        } else {
            throw XmlSyntaxException.createUnexpectedTagException(name);
        }
    }

    public final void endElement(final String name) throws XmlSyntaxException {
        if (getStartTag().equals(name)) {
            // nothing to do
        } else if ("LATEXPATTERN".equals(name)) {
            definition.setLatexPattern(latexPattern);
        } else if (formulaHandler.getStartTag().equals(name)) {
            definition.setFormula(formulaHandler.getFormula());
        } else if (descriptionHandler.getStartTag().equals(name)) {
            definition.setDescription(descriptionHandler.getLatexList());
        } else {
            throw XmlSyntaxException.createUnexpectedTagException(name);
        }
    }

    public final void characters(final String name, final String data) {
        if ("LATEXPATTERN".equals(name)) {
            latexPattern = data;
        } else {
            throw new RuntimeException("Unexpected character data in tag: " + name);
        }
    }


}

    }

    private boolean check(final Add add, final int i, final Element element) {
        final String context = currentContext.getLocationWithinModule();
        boolean ok = true;
        if (add.getReference() == null) {
            ok = false;
            setLocationWithinModule(context + ".getReference()");
            handleProofCheckException(
                BasicProofErrors.REFERENCE_TO_PROVED_FORMULA_IS_MISSING_CODE,
                BasicProofErrors.REFERENCE_TO_PROVED_FORMULA_IS_MISSING_TEXT,
                getCurrentContext());
            return ok;
        }
        if (!resolver.isProvedFormula(add.getReference())) {
            ok = false;
            setLocationWithinModule(context + ".getReference()");
            handleProofCheckException(
                BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
                BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
                + add.getReference(),
                getCurrentContext());
            return ok;
        }
        final Element expected = resolver.getNormalizedReferenceFormula(add.getReference());
        final Element current = resolver.getNormalizedFormula(element);
        if (!EqualsUtility.equals(expected, current)) {
            ok = false;
            handleProofCheckException(
                BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
                BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
                + add.getReference(),
                getDiffModuleContextOfProofLineFormula(i, expected));
            return ok;
        }
        final RuleKey defined = checker.getRule(add.getName());
        if (defined == null) {
            ok = false;
            handleProofCheckException(
                BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
                BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
                + add.getName(),
                getCurrentContext());
            return ok;
        } else if (!supported.contains(defined.getVersion())) {

        printImports();
    }

    /**
     * Get URL for QEDEQ XML module.
     *
     * @param   address         Current module address.
     * @param   specification   Find URL for this location list.
     * @return  URL or <code>""</code> if none (valid?) was found.
     */
    private String getUrl(final ModuleAddress address, final Specification specification) {
        final LocationList list = specification.getLocationList();
        if (list == null || list.size() <= 0) {
            return "";
        }
        try {
            return address.getModulePaths(specification)[0].getUrl();
        } catch (IOException e) {
            return "";
        }
    }

    public void visitEnter(final Chapter chapter) {
        // check if we print only brief and test for non text subnodes
        if (brief) {
            boolean hasFormalContent = false;
            do {
                final SectionList sections = chapter.getSectionList();
                if (sections == null) {
                    break;
                }
                for (int i = 0; i < sections.size() && !hasFormalContent; i++) {
                    final Section section = sections.get(i);
                    if (section == null) {
                        continue;
                    }
                    final SubsectionList subSections = section.getSubsectionList();
                    if (subSections == null) {
                        continue;
                    }
                    for (int j = 0; j < subSections.size(); j++) {
                        final SubsectionType subSection = subSections.get(j);
                        if (!(subSection instanceof Subsection)) {
                            hasFormalContent = true;
                            break;
                        }
                    }
                }
            } while (false);
            if (!hasFormalContent) {
                setBlocked(true);
                return;
            }
        }

        return token.toString();
    }

    protected final Operator getOperator(final String token) {
        Operator result = null;
        if (token == null) {
            return result;
        }
        for (int i = 0; i < getOperators().size(); i++) {
            if (token.equals(((Operator) getOperators().get(i)).getStartSymbol())) {
                result = (Operator) getOperators().get(i);
                break;
            }
        }
        return result;
    }

    protected final List getOperators(final String token) {
        final List result = new ArrayList();
        if (token == null) {
            return result;
        }
        for (int i = 0; i < getOperators().size(); i++) {
            if (token.equals(((Operator) getOperators().get(i)).getStartSymbol())) {
                result.add(getOperators().get(i));
            }
        }
        return result;
    }

    protected boolean eot(final String token) {
        return token == null || token.trim().length() == 0;
    }

}

        final ProofListVo otherList = (ProofListVo) obj;
        if (size() != otherList.size()) {
            return false;
        }
        for (int i = 0; i < size(); i++) {
            if (!EqualsUtility.equals(get(i), otherList.get(i))) {
                return false;
            }
        }
        return true;
    }

    public int hashCode() {
        int hash = 0;
        for (int i = 0; i < size(); i++) {
            hash = hash ^ (i + 1);
            if (get(i) != null) {
                hash = hash ^ get(i).hashCode();
            }
        }
        return hash;
    }

    public String toString() {
        final StringBuffer buffer = new StringBuffer("Proofs:\n");
        for (int i = 0; i < size(); i++) {
            if (i != 0) {
                buffer.append("\n");
            }
            buffer.append((i + 1) + ":\t");
            buffer.append(get(i) != null ? get(i).toString() : null);
        }
        return buffer.toString();
    }

}

        currentContext = new ModuleContext(moduleContext);
        exceptions = new LogicalCheckExceptionList();
        final String context = moduleContext.getLocationWithinModule();
        lineProved = new boolean[proof.size()];
        label2line = new HashMap();
        for (int i = 0; i < proof.size(); i++) {
            boolean ok = true;
            setLocationWithinModule(context + ".get(" + i + ")");
            final FormalProofLine line = proof.get(i);
            if (line == null || line.getFormula() == null
                    || line.getFormula().getElement() == null) {
                ok = false;
                handleProofCheckException(
                    BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_CODE,
                    BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_TEXT,
                    getCurrentContext());
                continue;
            }
            setLocationWithinModule(context + ".get(" + i + ").getReason()");
            final Reason reason = line.getReason();
            if (reason == null) {
                ok = false;
                handleProofCheckException(
                    BasicProofErrors.REASON_MUST_NOT_BE_NULL_CODE,
                    BasicProofErrors.REASON_MUST_NOT_BE_NULL_TEXT,
                    getCurrentContext());
                continue;
            }
            if (line.getLabel() != null && line.getLabel().length() > 0) {

        } catch (final SourceFileExceptionList e) {
            final String msg = "Generation failed";
            Trace.fatal(CLASS, this, method, msg, e);
            QedeqLog.getInstance().logFailureReply(msg, visitor.getKernelQedeqBo().getUrl(), e.getMessage());
        } catch (IOException e) {
            final String msg = "Generation failed";
            Trace.fatal(CLASS, this, method, msg, e);
            QedeqLog.getInstance().logFailureReply(msg, visitor.getKernelQedeqBo().getUrl(), e.getMessage());
        } catch (final RuntimeException e) {
            Trace.fatal(CLASS, this, method, "unexpected problem", e);
            QedeqLog.getInstance().logFailureReply(
                "Generation failed", visitor.getKernelQedeqBo().getUrl(), "unexpected problem: "
                + (e.getMessage() != null ? e.getMessage() : e.toString()));
        }
        return null;

                definition = (FunctionDefinition) Element2LatexImpl.this.getBackupFunctionDefinitions()
                    .get(identifier);
            }
            if (definition != null) {
                final StringBuffer define = new StringBuffer(definition.getLatexPattern());
                for (int i = list.size() - 1; i >= 1; i--) {
                    StringUtility.replace(define, "#" + i, Element2LatexImpl.this.
                        getLatex(list.getElement(i), false));
                }
                buffer.append(define);
            } else {
                buffer.append(identifier);
                buffer.append("(");
                for (int i = 1; i < list.size(); i++) {
                    buffer.append(Element2LatexImpl.this.getLatex(list.getElement(i), false));
                    if (i + 1 < list.size()) {
                        buffer.append(", ");
                    }
                }
                buffer.append(")");
            }
            return buffer.toString();
        }
    }

        final UniversalVo other = (UniversalVo) obj;
        return EqualsUtility.equals(reference, other.reference)
            && EqualsUtility.equals(subjectVariable, other.subjectVariable);
    }

    public int hashCode() {
        return (reference != null ? reference.hashCode() : 0)
            ^ (subjectVariable != null ? 2 ^ subjectVariable.hashCode() : 0);
    }

    public String toString() {
        StringBuffer result = new StringBuffer();
        result.append(getName());
        if (reference != null || subjectVariable != null) {
            result.append(" (");
            boolean w = false;
            if (reference != null) {
                result.append(reference);
                w = true;
            }
            if (subjectVariable != null) {
                if (w) {
                    result.append(", ");
                }
                result.append(subjectVariable);
                w = true;
            }
            result.append(")");
        }
        return result.toString();
    }

}

    public void visitEnter(final FunctionDefinition definition) {
        final QedeqNumbers numbers = getCurrentNumbers();
        printer.print("\u2609 ");
        final StringBuffer buffer = new StringBuffer();
        buffer.append("Definition " + (numbers.getPredicateDefinitionNumber()
                + numbers.getFunctionDefinitionNumber()));
        printer.print(buffer.toString());
        printer.print(" ");
        if (title != null && title.length() > 0) {
            printer.print(" (" + title + ")");
        }
        if (info) {
            printer.print("  [" + id + "]");
        }
        printer.println();
        printer.println();
        printer.print("     ");
        printer.println(getUtf8(definition.getFormula().getElement()));
        printer.println();
        if (definition.getDescription() != null) {
            printer.println(getLatexListEntry("getDescription()", definition.getDescription()));

    public void visitEnter(final InitialFunctionDefinition definition) {
        final QedeqNumbers numbers = getCurrentNumbers();
        printer.print("\u2609 ");
        final StringBuffer buffer = new StringBuffer();
        if ("de".equals(language)) {
            buffer.append("initiale ");
        } else {
            buffer.append("initial ");
        }
        buffer.append("Definition " + (numbers.getPredicateDefinitionNumber()
                + numbers.getFunctionDefinitionNumber()));
        printer.print(buffer.toString());
        printer.print(" ");
        if (title != null && title.length() > 0) {
            printer.print(" (" + title + ")");
        }
        if (info) {
            printer.print("  [" + id + "]");
        }
        printer.println();
        printer.println();
        printer.print("     ");
        printer.println(getUtf8(definition.getFunCon()));

        final PredicateDefinition other = (PredicateDefinition) obj;
        return  EqualsUtility.equals(getArgumentNumber(), other.getArgumentNumber())
            &&  EqualsUtility.equals(getName(), other.getName())
            &&  EqualsUtility.equals(getLatexPattern(), other.getLatexPattern())
            &&  EqualsUtility.equals(getFormula(), other.getFormula())
            &&  EqualsUtility.equals(getDescription(), other.getDescription());
    }

    public int hashCode() {
        return (getArgumentNumber() != null ? getArgumentNumber().hashCode() : 0)
            ^ (getName() != null ? 1 ^ getName().hashCode() : 0)
            ^ (getLatexPattern() != null ? 2 ^ getLatexPattern().hashCode() : 0)
            ^ (getFormula() != null ? 4 ^ getFormula().hashCode() : 0)

    public static final Predicate IS_TWO = Predicate.isEntity(TWO);

    /** Map to one. */
    /** Modulo 3. */
    private final Function functionModulo3 = new Function(0, 99, "% 3", "modulo 3") {
        public Entity map(final Entity[] entities) {
            int result = 0;
            for (int i = 0; i < entities.length; i++) {
                result += entities[i].getValue() % 3;
            }
            result = result % 3;
            return getEntity(result);
        }
    };

    /** +1 Modulo 3. */
    private final Function functionPlus1Modulo3 = new Function(0, 99, "+1 % 3", "plus 1 modulo 3") {
        public Entity map(final Entity[] entities) {
            int result = 1;
            for (int i = 0; i < entities.length; i++) {
                result += entities[i].getValue() % 3;
            }
            result = result % 3;
            return getEntity(result);
        }
    };


    /**
     * Constructor.
     */
    public ThreeDynamicModel() {

            final Element expected = FormulaUtility.replaceSubjectVariableQuantifier(
                rename.getOriginalSubjectVariable(),
                rename.getReplacementSubjectVariable(), f, rename.getOccurrence(),
                new Enumerator());
            final Element current = resolver.getNormalizedFormula(element);
            if (!EqualsUtility.equals(expected, current)) {
                ok = false;
                handleProofCheckException(
                    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
                    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
                    + rename.getReference(),
                    getDiffModuleContextOfProofLineFormula(i, expected));
            } else {
                ok = true;
            }
        }
        final RuleKey defined = checker.getRule(rename.getName());
        if (defined == null) {
            ok = false;
            handleProofCheckException(
                BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
                BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
                + rename.getName(),
                getCurrentContext());
            return ok;
        } else if (!supported.contains(defined.getVersion())) {

    class Funvar implements ListType {
        public String getLatex(final ElementList list, final boolean first) {
            final StringBuffer buffer = new StringBuffer();
            final String identifier = list.getElement(0).getAtom().getString();
            buffer.append(identifier);
            if (list.size() > 1) {
                buffer.append("(");
                for (int i = 1; i < list.size(); i++) {
                    buffer.append(Element2LatexImpl.this.getLatex(list.getElement(i), false));
                    if (i + 1 < list.size()) {
                        buffer.append(", ");
                    }
                }
                buffer.append(")");
            }
            return buffer.toString();
        }
    }

    /**
     * Transformer for a predicate constant.
     */
    class Predcon implements ListType {

        Trace.param(CLASS, this, method, "current", current);
        final String context = traverser.getCurrentContext().getLocationWithinModule();
        checkMatching(method);

        traverser.setLocationWithinModule(context + ".getArgumentNumber()");
        current.setAttribute("arguments");
        checkIfFound();

        traverser.setLocationWithinModule(context + ".getName()");
        current.setAttribute("name");
        checkIfFound();

        traverser.setLocationWithinModule(context + ".getLatexPattern()");
        enter("LATEXPATTERN");
        if (find.getLocationWithinModule().equals(traverser.getCurrentContext()
                .getLocationWithinModule())) {
            if (definition.getLatexPattern() == null) { // NOT FOUND
                leave();
            }
            throw new LocationFoundException(traverser.getCurrentContext());
        }
        leave();
    }

    public final void visitLeave(final FunctionDefinition definition) {

        final UsedByListVo otherList = (UsedByListVo) obj;
        if (size() != otherList.size()) {
            return false;
        }
        for (int i = 0; i < size(); i++) {
            if (!EqualsUtility.equals(get(i), otherList.get(i))) {
                return false;
            }
        }
        return true;
    }

    public int hashCode() {
        int hash = 0;
        for (int i = 0; i < size(); i++) {
            hash = hash ^ (i + 1);
            if (get(i) != null) {
                hash = hash ^ get(i).hashCode();
            }
        }
        return hash;
    }

    public String toString() {
        final StringBuffer buffer = new StringBuffer("List of modules that use the current one:\n");

                Element2LatexImpl.this.labels.getFunctionDefinitions().get(identifier);
            if (definition == null) {
                // try external modules
                try {
                    final int external = name.indexOf(".");
                    if (external >= 0) {
                        final String shortName = name.substring(external + 1);
                        identifier = shortName + "_" + (arguments);
                        if (Element2LatexImpl.this.labels.getReferences() != null
                                && Element2LatexImpl.this.labels.getReferences().size() > 0) {
                            final String label = name.substring(0, external);
                            final KernelQedeqBo newProp = (KernelQedeqBo)
                                Element2LatexImpl.this.labels.getReferences().getQedeqBo(label);
                            if (newProp != null) {
                                if (newProp.getExistenceChecker().functionExists(shortName,

        final ElementList variable = list.getElement(0).getList();
        final SubjectVariable var = new SubjectVariable(variable.getElement(0).getAtom().getString());
        subjectVariableInterpreter.addSubjectVariable(var);
        for (int i = 0; i < model.getEntitiesSize(); i++) {
            if (Trace.isDebugEnabled(CLASS)) {
                Trace.param(CLASS, this, method, deepness.toString() + Latex2UnicodeParser
                    .transform(null, qedeq.getElement2Latex().getLatex(variable), 0),
                    model.getEntity(i));
            }
            if (list.size() == 2) {
                setLocationWithinModule(context + ".getElement(1)");
                result |= calculateValue(list.getElement(1));

        final String context = getLocationWithinModule();
        boolean result = false;
        final ElementList variable = list.getElement(0).getList();
        final SubjectVariable var = new SubjectVariable(variable.getElement(0).getAtom().getString());
        subjectVariableInterpreter.addSubjectVariable(var);
        for (int i = 0; i < model.getEntitiesSize(); i++) {
            if (Trace.isDebugEnabled(CLASS)) {
                Trace.param(CLASS, this, method, deepness.toString() + Latex2UnicodeParser.transform(null,
                        qedeq.getElement2Latex().getLatex(variable), 0), model.getEntity(i));
            }

    private int addOccurence(final String name) {
        while (level < elements.size()) {
            elements.remove(elements.size() - 1);
        }
        while (level > elements.size()) {
            elements.add(new HashMap());
        }
        final Map levelMap = (Map) elements.get(level - 1);
        final Enumerator counter;
        if (levelMap.containsKey(name)) {
            counter = (Enumerator) levelMap.get(name);
            counter.increaseNumber();
        } else {
            counter = new Enumerator(1);
            levelMap.put(name, counter);
        }
        return counter.getNumber();
    }

                printer.print("\\bibitem{" + imp.getLabel() + "} ");
                final Specification spec = imp.getSpecification();
                printer.print(getLatex(spec.getName()));
                if (spec.getLocationList() != null && spec.getLocationList().size() > 0
                        && spec.getLocationList().get(0).getLocation().length() > 0) {
                    printer.print(" ");
                    // TODO m31 20070205, 2010727: later on here must stand the location that was used
                    //   to verify the document contents.
                    //   Also get other informations like authors, title, etc.
                    //   It might also be better to link to URL?
//                    printer.print("\\url{" + getUrl(getQedeqBo().getModuleAddress(), spec) + "}");
                    printer.print("\\url{" + getPdfLink((KernelQedeqBo) getKernelQedeqBo()
                        .getLabels().getReferences().getQedeqBo(imp.getLabel())) + "}");
                }
                printer.println();
            }

                + existential.getName(),
                getCurrentContext());
            return ok;
        } else if (!supported.contains(defined.getVersion())) {
            ok = false;
            handleProofCheckException(
                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
                + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
                getCurrentContext());
            return ok;
        } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
            ok = false;
            handleProofCheckException(
                BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
                BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
                + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
                getCurrentContext());
            return ok;
        }
        return ok;
    }

    private boolean check(final ConditionalProof cp, final int i, final Element element) {

        if (i < 0 || i >= proof.size()) {
            return null;
        }
        return resolver.getNormalizedFormula(proof.get(i).getFormula().getElement());
    }

    /**
     * Add new {@link ProofCheckException} to exception list.
     *
     * @param code      Error code.
     * @param msg       Error message.
     * @param context   Error context.
     */
    private void handleProofCheckException(final int code, final String msg,
            final ModuleContext context) {
//        System.out.println(context);
//        System.setProperty("qedeq.test.xmlLocationFailures", "true");
        final ProofCheckException ex = new ProofCheckException(code, msg, context);
        exceptions.add(ex);
    }

    /**
     * Add new {@link ProofCheckException} to exception list.
     *
     * @param code              Error code.
     * @param msg               Error message.
     * @param context           Error context.
     * @param referenceContext  Reference context.
     */
    private void handleProofCheckException(final int code, final String msg,
            final ModuleContext context, final ModuleContext referenceContext) {
//        System.out.println(context);
//        System.setProperty("qedeq.test.xmlLocationFailures", "true");
        final ProofCheckException ex = new ProofCheckException(code, msg, null, context,
            referenceContext);
        exceptions.add(ex);
    }

    /**
     * Get current context within original.
     *
     * @return  Current context.
     */
    protected final ModuleContext getCurrentContext() {

        if (size > size()) {
            return false;
        }
        if (size != currentSummary.size()) {
            throw new IllegalArgumentException("summary size doesn't match");
        }

        for (int i = 0; i < size; i++) {
            if ("*".equals(getElementName(i))) {
                if (getElementOccurrence(i) != currentSummary.getElementOccurrence(i)) {
                    return false;
                }
                continue;
            }
            if (!EqualsUtility.equals(current.getElementName(i), getElementName(i))) {
                return false;
            }
            if (current.getElementOccurrence(i) != getElementOccurrence(i)) {
                return false;
            }
        }
        return true;
    }

    public final String toString() {

                + cp.getName(),
                getCurrentContext());
            return ok;
        } else if (!supported.contains(defined.getVersion())) {
            ok = false;
            handleProofCheckException(
                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
                + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
                getCurrentContext());
            return ok;
        } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
            ok = false;
            handleProofCheckException(
                BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
                BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
                + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
                getCurrentContext());
            return ok;
        }
        return ok;
    }

    private ModuleContext getModuleContextOfProofLineFormula(final int i) {

    }

    public InitialFunctionDefinition getInitialFunctionDefinition() {
        return null;
    }

    public FunctionDefinition getFunctionDefinition() {
        return null;
    }

    public Proposition getProposition() {
        return null;
    }

    public Rule getRule() {
        return null;
    }

    /**
     * Set information about the argument number the defined object needs.
     *
     * @param   argumentNumber  Argument number information.
     */
    public final void setArgumentNumber(final String argumentNumber) {
        this.argumentNumber = argumentNumber;
    }

    public final String getArgumentNumber() {
        return argumentNumber;
    }

    /**
     * Set predicate name. Together with {@link #getArgumentNumber()} this
     * identifies a predicate.
     *
     * @param   name    Predicate name.
     */
    public void setName(final String name) {
        this.name = name;
    }

    public String getName() {
        return name;
    }

    /**
     * Set LaTeX pattern for definition visualisation. The replaceable arguments are
     * marked as <code>#1</code>, <code>#2</code> and so on. For example
     * <code>\mathfrak{M}(#1)</code>.
     *
     * @param   latexPattern    LaTeX pattern for definition visualisation.
     */
    public final void setLatexPattern(final String latexPattern) {
        this.latexPattern = latexPattern;
    }

    public final String getLatexPattern() {
        return latexPattern;
    }

    /**
     * Set defining formula or term that defines the object. Could be <code>null</code>.
     *
     * @param   formulaOrTerm   Formula or term that defines the new operator.
     */
    public final void setFormula(final FormulaVo formulaOrTerm) {

        final ElementList variable = list.getElement(0).getList();
        final SubjectVariable var = new SubjectVariable(variable.getElement(0).getAtom().getString());
        subjectVariableInterpreter.addSubjectVariable(var);
        for (int i = 0; i < model.getEntitiesSize(); i++) {
            if (Trace.isDebugEnabled(CLASS)) {
                Trace.param(CLASS, this, method, deepness.toString() + Latex2UnicodeParser.transform(null,
                        qedeq.getElement2Latex().getLatex(variable), 0), model.getEntity(i));
            }

            final FunctionKey key = new FunctionKey(formula.getElement(0).getAtom().getString(),
                    "" + (formula.getList().size() - 1));
            final DefaultAtom atom = new DefaultAtom(
                qedeq.getExistenceChecker().get(key).getContext().getModuleLocation().getUrl()
                + "$" + key.getName());
            result.add(atom);
            for (int i = 1; i < formula.size(); i++) {
                result.add(getNormalizedFormula(qedeq, formula.getElement(i)));
            }
        } else {

        printer.print("<DEFINITION_PREDICATE");
        if (definition.getArgumentNumber() != null) {
            printer.print(" arguments=\"" + StringUtility.escapeXml(definition.getArgumentNumber()) + "\"");
        }
        if (definition.getName() != null) {
            printer.print(" name=\"" + StringUtility.escapeXml(definition.getName()) + "\"");
        }
        printer.println(">");
        printer.pushLevel();
        if (definition.getLatexPattern() != null) {
            printer.println("<LATEXPATTERN>" + StringUtility.escapeXml(definition.getLatexPattern())
                + "</LATEXPATTERN>");
        }
    }

    public void visitLeave(final PredicateDefinition definition) {

        location.set(location.size() - 1, "Definition " + (data.getFunctionDefinitionNumber()
                + data.getFunctionDefinitionNumber()) + " "
                + (String) location.lastElement());
        final String context = getCurrentContext().getLocationWithinModule();
        visitor.visitEnter(definition);
        if (definition.getFormula() != null) {
            setLocationWithinModule(context + ".getFormula()");
            accept(definition.getFormula());
        }
        if (definition.getDescription() != null) {
            setLocationWithinModule(context + ".getDescription()");
            accept(definition.getDescription());
        }
        setLocationWithinModule(context);
        visitor.visitLeave(definition);
        setLocationWithinModule(context);
    }

    public void accept(final Proposition proposition) throws ModuleDataException {

            uni.add(reference.getList().getElement(1));
            expected.add(uni);
//            System.out.print("Expected: ");
//            ProofFinderUtility.println(expected);
//            System.out.print("Current : ");
//            ProofFinderUtility.println(current);
            if (!EqualsUtility.equals(current, expected)) {
                ok = false;
                handleProofCheckException(
                    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
                    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
                    + universal.getReference(),
                    getDiffModuleContextOfProofLineFormula(i, expected));
                return ok;
            }
        }
        final RuleKey defined = checker.getRule(universal.getName());
        if (defined == null) {
            ok = false;
            handleProofCheckException(
                BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
                BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
                + universal.getName(),
                getCurrentContext());
            return ok;
        } else if (!supported.contains(defined.getVersion())) {

        final ModuleReferenceList ref = prop.getRequiredModules();
        for (int i = 0; i < ref.size(); i++) {
            final KernelQedeqBo newProp = (KernelQedeqBo) ref.getQedeqBo(i);
            final RuleKey found = newProp.getExistenceChecker().getRuleKey(ruleName);
            if (found != null && found.getVersion() != null && (ruleKey == null
                    || ruleKey.getVersion() == null
                    || 0 < found.getVersion().compareTo(ruleKey.getVersion()))) {
                ruleKey = found;
            }
        }
        return ruleKey;
    }

    public Rule get(final RuleKey ruleKey) {

        printer.print("<DEFINITION_FUNCTION");
        if (definition.getArgumentNumber() != null) {
            printer.print(" arguments=\"" + StringUtility.escapeXml(definition.getArgumentNumber()) + "\"");
        }
        if (definition.getName() != null) {
            printer.print(" name=\"" + StringUtility.escapeXml(definition.getName()) + "\"");
        }
        printer.println(">");
        printer.pushLevel();
        if (definition.getLatexPattern() != null) {
            printer.println("<LATEXPATTERN>" + definition.getLatexPattern()
                + "</LATEXPATTERN>");
        }
    }

    public void visitLeave(final FunctionDefinition definition) {

    }

    public FunctionDefinition getFunctionDefinition() {
        return null;
    }

    public Proposition getProposition() {
        return null;
    }

    public Rule getRule() {
        return null;
    }

    /**
     * Set information about the argument number the defined object needs.
     *
     * @param   argumentNumber  Argument number information.
     */
    public final void setArgumentNumber(final String argumentNumber) {
        this.argumentNumber = argumentNumber;
    }

    public final String getArgumentNumber() {
        return argumentNumber;
    }

    /**
     * Set predicate name. Together with {@link #getArgumentNumber()} this
     * identifies a predicate.
     *
     * @param   name    Predicate name.
     */
    public void setName(final String name) {
        this.name = name;
    }

    public String getName() {
        return name;
    }

    /**
     * Set LaTeX pattern for definition visualisation. The replaceable arguments are
     * marked as <code>#1</code>, <code>#2</code> and so on. For example
     * <code>\mathfrak{M}(#1)</code>.
     *
     * @param   latexPattern    LaTeX pattern for definition visualisation.
     */
    public final void setLatexPattern(final String latexPattern) {
        this.latexPattern = latexPattern;
    }

    public final String getLatexPattern() {
        return latexPattern;
    }

    /**
     * Set new predicate constant with free subject variables. The predicate constant must
     * match {@link #getName()} and {@link #getArgumentNumber()}.
     *
     * @param   predCon Predicate constant with free subject variables.
     */
    public final void setPredCon(final Element predCon) {

            expected.add((reference.getList().getElement(1)));
            if (!EqualsUtility.equals(current, expected)) {
                ok = false;
                handleProofCheckException(
                    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
                    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
                    + existential.getReference(),
                    getDiffModuleContextOfProofLineFormula(i, expected));
                return ok;
            }
        }
        final RuleKey defined = checker.getRule(existential.getName());
        if (defined == null) {
            ok = false;
            handleProofCheckException(
                BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
                BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
                + existential.getName(),
                getCurrentContext());
            return ok;
        } else if (!supported.contains(defined.getVersion())) {

            if (list.size() < 1 + minArguments) {
                return false;
            }
            final Element first = element.getList().getElement(0);
            if (first == null || !first.isAtom() || first.getAtom() == null) {
                return false;
            }
            final Atom atom = first.getAtom();
            if (atom.getString() == null || atom.getAtom().getString() == null
                    || atom.getString().length() == 0) {
                return false;
            }
        } else {
            return false;
        }
        return true;
    }

    /**
     * Return all free subject variables of an element.
     *
     * @param   element    Work on this element.
     * @return  All free subject variables.
     */
    public static final ElementSet getFreeSubjectVariables(final Element element) {

            return this.elements.equals(((ElementSet) obj).elements);
        }
        return false;
    }

    public final int hashCode() {
        return elements.hashCode();
    }

    public final String toString() {
        final StringBuffer result = new StringBuffer();
        result.append("{");
        final Iterator iterator = elements.iterator();
        while (iterator.hasNext()) {
            result.append(iterator.next());
            if (iterator.hasNext()) {
                result.append(", ");
            }
        }
        result.append("}");
        return result.toString();
    }

        buffer.append("Definition " + (numbers.getPredicateDefinitionNumber()
            + numbers.getFunctionDefinitionNumber()));
        printer.print(buffer.toString());
        printer.print(" ");
        if (title != null && title.length() > 0) {
            printer.print(" (" + title + ")");
        }
        if (info) {
            printer.print("  [" + id + "]");
        }
        printer.println();
        printer.println();
        printer.print("     ");
        printer.println(getUtf8(definition.getFormula().getElement()));

    }

    public void visitEnter(final LinkList linkList) {
        if (linkList.size() <= 0) {
            return;
        }
        if ("de".equals(language)) {
            printer.println("Basierend auf: ");
        } else {
            if (!"en".equals(language)) {
                printer.println("%%% TODO unknown language: " + language);
            }
            printer.println("Based on: ");
        }
        for (int i = 0; i < linkList.size(); i++) {
            if (linkList.get(i) != null) {
                printer.print(" (" + linkList.get(i) + ")");

        setBlocked(false);
    }

    public void visitEnter(final Section section) {
        // check if we print only brief and test for non text subnodes
        if (brief) {
            boolean hasFormalContent = false;
            do {
                final SubsectionList subSections = section.getSubsectionList();
                if (subSections == null) {
                    break;
                }
                for (int j = 0; j < subSections.size(); j++) {
                    final SubsectionType subSection = subSections.get(j);
                    if (!(subSection instanceof Subsection)) {
                        hasFormalContent = true;
                        break;
                    }
                }
            } while (false);
            if (!hasFormalContent) {
                setBlocked(true);
                return;
            }
        }

        final FunctionDefinitionVo d = new FunctionDefinitionVo();
        final String context = getCurrentContext().getLocationWithinModule();
        if (definition.getLatexPattern() != null) {
            setLocationWithinModule(context + ".getLatexPattern()");
            d.setLatexPattern(definition.getLatexPattern());
        }
        if (definition.getArgumentNumber() != null) {
            setLocationWithinModule(context + ".getArgumentNumber()");
            d.setArgumentNumber(definition.getArgumentNumber());
        }
        if (definition.getName() != null) {
            setLocationWithinModule(context + ".getName()");
            d.setName(definition.getName());
        }
        if (definition.getFormula() != null) {

        final PredicateDefinitionVo d = new PredicateDefinitionVo();
        final String context = getCurrentContext().getLocationWithinModule();
        if (definition.getLatexPattern() != null) {
            setLocationWithinModule(context + ".getLatexPattern()");
            d.setLatexPattern(definition.getLatexPattern());
        }
        if (definition.getName() != null) {
            setLocationWithinModule(context + ".getName()");
            d.setName(definition.getName());
        }
        if (definition.getArgumentNumber() != null) {
            setLocationWithinModule(context + ".getArgumentNumber()");
            d.setArgumentNumber(definition.getArgumentNumber());
        }
        if (definition.getFormula() != null) {

            + ref.getNodeLabel()
            + (ref.isSubReference() ? "/" + ref.getSubLabel() : "")
            + (ref.isProofLineReference() ? "!" + ref.getProofLineLabel() : "")
            + "}{" + getNodeDisplay(ref.getNodeLabel(), ref.getNode())
                + (ref.isSubReference() ? " (" + ref.getSubLabel() + ")" : "")
                + (ref.isProofLineReference() ? " (" + ref.getProofLineLabel() + ")" : "")
            + "}~\\cite{" + ref.getExternalQedeqLabel() + "}";