From 442d732696ad431b84f6e5c72b6ee785be4fd968 Mon Sep 17 00:00:00 2001 From: adelon <22380201+adelon@users.noreply.github.com> Date: Sat, 10 Feb 2024 02:22:14 +0100 Subject: Initial commit --- test/golden/russell/encoding tasks.golden | 24 + test/golden/russell/generating tasks.golden | 769 ++++++++++++++++++++++++++++ test/golden/russell/glossing.golden | 155 ++++++ test/golden/russell/parsing.golden | 198 +++++++ test/golden/russell/scanning.golden | 6 + test/golden/russell/tokenizing.golden | 80 +++ test/golden/russell/verification.golden | 1 + 7 files changed, 1233 insertions(+) create mode 100644 test/golden/russell/encoding tasks.golden create mode 100644 test/golden/russell/generating tasks.golden create mode 100644 test/golden/russell/glossing.golden create mode 100644 test/golden/russell/parsing.golden create mode 100644 test/golden/russell/scanning.golden create mode 100644 test/golden/russell/tokenizing.golden create mode 100644 test/golden/russell/verification.golden (limited to 'test/golden/russell') diff --git a/test/golden/russell/encoding tasks.golden b/test/golden/russell/encoding tasks.golden new file mode 100644 index 0000000..c8fa769 --- /dev/null +++ b/test/golden/russell/encoding tasks.golden @@ -0,0 +1,24 @@ +fof(no_universal_set,conjecture,?[XV]:universal_set(XV)). +fof(universal_set,axiom,![XV]:(universal_set(XV)<=>![Xx]:elem(Xx,XV))). +fof(no_universal_set1,axiom,~~?[X0]:universal_set(X0)). +------------------ +fof(no_universal_set,conjecture,elem(fR,fR)<=>~elem(fR,fR)). +fof(universal_set,axiom,![XV]:(universal_set(XV)<=>![Xx]:elem(Xx,XV))). +fof(no_universal_set1,axiom,![Xx]:(elem(Xx,fR)<=>(elem(Xx,fV)&~elem(Xx,Xx)))). +fof(no_universal_set2,axiom,universal_set(fV)). +fof(no_universal_set3,axiom,~~?[X0]:universal_set(X0)). +------------------ +fof(no_universal_set,conjecture,$false). +fof(universal_set,axiom,![XV]:(universal_set(XV)<=>![Xx]:elem(Xx,XV))). +fof(no_universal_set1,axiom,elem(fR,fR)<=>~elem(fR,fR)). +fof(no_universal_set2,axiom,![Xx]:(elem(Xx,fR)<=>(elem(Xx,fV)&~elem(Xx,Xx)))). +fof(no_universal_set3,axiom,universal_set(fV)). +fof(no_universal_set4,axiom,~~?[X0]:universal_set(X0)). +------------------ +fof(no_universal_set,conjecture,$false). +fof(universal_set,axiom,![XV]:(universal_set(XV)<=>![Xx]:elem(Xx,XV))). +fof(no_universal_set1,axiom,$false). +fof(no_universal_set2,axiom,elem(fR,fR)<=>~elem(fR,fR)). +fof(no_universal_set3,axiom,![Xx]:(elem(Xx,fR)<=>(elem(Xx,fV)&~elem(Xx,Xx)))). +fof(no_universal_set4,axiom,universal_set(fV)). +fof(no_universal_set5,axiom,~~?[X0]:universal_set(X0)). \ No newline at end of file diff --git a/test/golden/russell/generating tasks.golden b/test/golden/russell/generating tasks.golden new file mode 100644 index 0000000..a509323 --- /dev/null +++ b/test/golden/russell/generating tasks.golden @@ -0,0 +1,769 @@ +[ Task + { taskDirectness = Indirect + ( Not + ( Quantified Existentially + ( Scope + ( Connected Conjunction ( PropositionalConstant IsTop ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "universal" ) + ] + ) + ) + [ TermVar + ( B + ( FreshVar 0 ) + ) + ] + ) + ) + ) + ) + ) + , taskHypotheses = + [ + ( Marker "universal_set" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "universal" ) + ] + ) + ) + [ TermVar + ( B + ( NamedVar "V" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( F + ( TermVar + ( F + ( TermVar + ( B + ( NamedVar "V" ) + ) + ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "no_universal_set1" + , Not + ( Not + ( Quantified Existentially + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "universal" ) + ] + ) + ) + [ TermVar + ( B + ( FreshVar 0 ) + ) + ] + ) + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "no_universal_set" + , taskConjecture = Quantified Existentially + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "universal" ) + ] + ) + ) + [ TermVar + ( B + ( NamedVar "V" ) + ) + ] + ) + ) + } +, Task + { taskDirectness = Indirect + ( Not + ( Quantified Existentially + ( Scope + ( Connected Conjunction ( PropositionalConstant IsTop ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "universal" ) + ] + ) + ) + [ TermVar + ( B + ( FreshVar 0 ) + ) + ] + ) + ) + ) + ) + ) + , taskHypotheses = + [ + ( Marker "universal_set" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "universal" ) + ] + ) + ) + [ TermVar + ( B + ( NamedVar "V" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( F + ( TermVar + ( F + ( TermVar + ( B + ( NamedVar "V" ) + ) + ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "no_universal_set1" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "R" ) + ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "V" ) + ) + ) + ] + ) + ( Not + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ) + ) + ) + ) + ) + , + ( Marker "no_universal_set2" + , TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "universal" ) + ] + ) + ) + [ TermVar + ( NamedVar "V" ) + ] + ) + , + ( Marker "no_universal_set3" + , Not + ( Not + ( Quantified Existentially + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "universal" ) + ] + ) + ) + [ TermVar + ( B + ( FreshVar 0 ) + ) + ] + ) + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "no_universal_set" + , taskConjecture = Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "R" ) + , TermVar + ( NamedVar "R" ) + ] + ) + ( Not + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "R" ) + , TermVar + ( NamedVar "R" ) + ] + ) + ) + } +, Task + { taskDirectness = Indirect + ( Not + ( Quantified Existentially + ( Scope + ( Connected Conjunction ( PropositionalConstant IsTop ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "universal" ) + ] + ) + ) + [ TermVar + ( B + ( FreshVar 0 ) + ) + ] + ) + ) + ) + ) + ) + , taskHypotheses = + [ + ( Marker "universal_set" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "universal" ) + ] + ) + ) + [ TermVar + ( B + ( NamedVar "V" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( F + ( TermVar + ( F + ( TermVar + ( B + ( NamedVar "V" ) + ) + ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "no_universal_set1" + , Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "R" ) + , TermVar + ( NamedVar "R" ) + ] + ) + ( Not + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "R" ) + , TermVar + ( NamedVar "R" ) + ] + ) + ) + ) + , + ( Marker "no_universal_set2" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "R" ) + ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "V" ) + ) + ) + ] + ) + ( Not + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ) + ) + ) + ) + ) + , + ( Marker "no_universal_set3" + , TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "universal" ) + ] + ) + ) + [ TermVar + ( NamedVar "V" ) + ] + ) + , + ( Marker "no_universal_set4" + , Not + ( Not + ( Quantified Existentially + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "universal" ) + ] + ) + ) + [ TermVar + ( B + ( FreshVar 0 ) + ) + ] + ) + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "no_universal_set" + , taskConjecture = PropositionalConstant IsBottom + } +, Task + { taskDirectness = Indirect + ( Not + ( Quantified Existentially + ( Scope + ( Connected Conjunction ( PropositionalConstant IsTop ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "universal" ) + ] + ) + ) + [ TermVar + ( B + ( FreshVar 0 ) + ) + ] + ) + ) + ) + ) + ) + , taskHypotheses = + [ + ( Marker "universal_set" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "universal" ) + ] + ) + ) + [ TermVar + ( B + ( NamedVar "V" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( F + ( TermVar + ( F + ( TermVar + ( B + ( NamedVar "V" ) + ) + ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "no_universal_set1" + , PropositionalConstant IsBottom + ) + , + ( Marker "no_universal_set2" + , Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "R" ) + , TermVar + ( NamedVar "R" ) + ] + ) + ( Not + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "R" ) + , TermVar + ( NamedVar "R" ) + ] + ) + ) + ) + , + ( Marker "no_universal_set3" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "R" ) + ) + ) + ] + ) + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "V" ) + ) + ) + ] + ) + ( Not + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ) + ) + ) + ) + ) + , + ( Marker "no_universal_set4" + , TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "universal" ) + ] + ) + ) + [ TermVar + ( NamedVar "V" ) + ] + ) + , + ( Marker "no_universal_set5" + , Not + ( Not + ( Quantified Existentially + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "universal" ) + ] + ) + ) + [ TermVar + ( B + ( FreshVar 0 ) + ) + ] + ) + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "no_universal_set" + , taskConjecture = PropositionalConstant IsBottom + } +] \ No newline at end of file diff --git a/test/golden/russell/glossing.golden b/test/golden/russell/glossing.golden new file mode 100644 index 0000000..e8ef25d --- /dev/null +++ b/test/golden/russell/glossing.golden @@ -0,0 +1,155 @@ +[ BlockDefn + ( SourcePos + { sourceName = "test/examples/russell.tex" + , sourceLine = Pos 1 + , sourceColumn = Pos 1 + } + ) + ( Marker "universal_set" ) + ( DefnPredicate [] + ( PredicateAdj + [ Just + ( Word "universal" ) + ] + ) + ( NamedVar "V" :| [] ) + ( Quantified Universally + ( Scope + ( Connected Implication ( PropositionalConstant IsTop ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "V" ) + ) + ) + ] + ) + ) + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/russell.tex" + , sourceLine = Pos 7 + , sourceColumn = Pos 1 + } + ) + ( Marker "no_universal_set" ) + ( Lemma [] + ( Not + ( Quantified Existentially + ( Scope + ( Connected Conjunction ( PropositionalConstant IsTop ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "universal" ) + ] + ) + ) + [ TermVar + ( B + ( FreshVar 0 ) + ) + ] + ) + ) + ) + ) + ) + ) +, BlockProof + ( SourcePos + { sourceName = "test/examples/russell.tex" + , sourceLine = Pos 10 + , sourceColumn = Pos 1 + } + ) + ( ByContradiction + ( Take + ( NamedVar "V" :| [] ) + ( Connected Conjunction ( PropositionalConstant IsTop ) + ( TermSymbol + ( SymbolPredicate + ( PredicateAdj + [ Just + ( Word "universal" ) + ] + ) + ) + [ TermVar + ( NamedVar "V" ) + ] + ) + ) JustificationEmpty + ( Define + ( NamedVar "R" ) + ( TermSep + ( NamedVar "x" ) + ( TermVar + ( NamedVar "V" ) + ) + ( Scope + ( Not + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B () ) + , TermVar + ( B () ) + ] + ) + ) + ) + ) + ( Have + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "R" ) + , TermVar + ( NamedVar "R" ) + ] + ) + ( Not + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "R" ) + , TermVar + ( NamedVar "R" ) + ] + ) + ) + ) JustificationEmpty + ( Have ( PropositionalConstant IsBottom ) JustificationEmpty ( Qed JustificationEmpty ) ) + ) + ) + ) + ) +] \ No newline at end of file diff --git a/test/golden/russell/parsing.golden b/test/golden/russell/parsing.golden new file mode 100644 index 0000000..f924229 --- /dev/null +++ b/test/golden/russell/parsing.golden @@ -0,0 +1,198 @@ +[ BlockDefn + ( SourcePos + { sourceName = "test/examples/russell.tex" + , sourceLine = Pos 1 + , sourceColumn = Pos 1 + } + ) + ( Marker "universal_set" ) + ( Defn [] + ( DefnAdj + ( Just NounPhrase ( [] ) + ( Noun + ( SgPl + { sg = + [ Just + ( Word "set" ) + ] + , pl = + [ Just + ( Word "sets" ) + ] + } + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + ) + ( NamedVar "V" ) + ( Adj + [ Just + ( Word "universal" ) + ] [] + ) + ) + ( StmtQuantPhrase + ( QuantPhrase Universally NounPhrase ( [] ) + ( Noun + ( SgPl + { sg = + [ Just + ( Word "set" ) + ] + , pl = + [ Just + ( Word "sets" ) + ] + } + ) [] + ) + ( + [ NamedVar "x" ] + ) ( [] ) ( Nothing ) + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "x" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "V" ) :| [] + ) + ) + ) + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/russell.tex" + , sourceLine = Pos 7 + , sourceColumn = Pos 1 + } + ) + ( Marker "no_universal_set" ) + ( Lemma [] + ( StmtNeg + ( StmtExists NounPhrase + ( + [ AdjL + [ Just + ( Word "universal" ) + ] [] + ] + ) + ( Noun + ( SgPl + { sg = + [ Just + ( Word "set" ) + ] + , pl = + [ Just + ( Word "sets" ) + ] + } + ) [] + ) ( [] ) ( [] ) ( Nothing ) + ) + ) + ) +, BlockProof + ( SourcePos + { sourceName = "test/examples/russell.tex" + , sourceLine = Pos 10 + , sourceColumn = Pos 1 + } + ) + ( ByContradiction + ( TakeNoun NounPhrase + ( + [ AdjL + [ Just + ( Word "universal" ) + ] [] + ] + ) + ( Noun + ( SgPl + { sg = + [ Just + ( Word "set" ) + ] + , pl = + [ Just + ( Word "sets" ) + ] + } + ) [] + ) + ( + [ NamedVar "V" ] + ) ( [] ) ( Nothing ) JustificationEmpty + ( Define + ( NamedVar "R" ) + ( ExprSep + ( NamedVar "x" ) + ( ExprVar + ( NamedVar "V" ) + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "x" ) :| [] + ) Negative + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "x" ) :| [] + ) + ) + ) + ) + ) + ( Have Nothing + ( StmtConnected Equivalence + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "R" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "R" ) :| [] + ) + ) + ) + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "R" ) :| [] + ) Negative + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "R" ) :| [] + ) + ) + ) + ) + ) JustificationEmpty + ( Have Nothing + ( StmtFormula ( PropositionalConstant IsBottom ) ) JustificationEmpty ( Qed JustificationEmpty ) + ) + ) + ) + ) + ) +] \ No newline at end of file diff --git a/test/golden/russell/scanning.golden b/test/golden/russell/scanning.golden new file mode 100644 index 0000000..c0111b2 --- /dev/null +++ b/test/golden/russell/scanning.golden @@ -0,0 +1,6 @@ +[ ScanAdj + [ Just + ( Word "universal" ) + ] + ( Marker "universal_set" ) +] \ No newline at end of file diff --git a/test/golden/russell/tokenizing.golden b/test/golden/russell/tokenizing.golden new file mode 100644 index 0000000..c2de55f --- /dev/null +++ b/test/golden/russell/tokenizing.golden @@ -0,0 +1,80 @@ +[ BeginEnv "definition" +, Label "universal_set" +, Word "a" +, Word "set" +, BeginEnv "math" +, Variable "V" +, EndEnv "math" +, Word "is" +, Word "universal" +, Word "iff" +, Word "for" +, Word "all" +, Word "sets" +, BeginEnv "math" +, Variable "x" +, EndEnv "math" +, Word "we" +, Word "have" +, BeginEnv "math" +, Variable "x" +, Command "in" +, Variable "V" +, EndEnv "math" +, Symbol "." +, EndEnv "definition" +, BeginEnv "theorem" +, Label "no_universal_set" +, Word "there" +, Word "exists" +, Word "no" +, Word "universal" +, Word "set" +, Symbol "." +, EndEnv "theorem" +, BeginEnv "proof" +, Word "suppose" +, Word "not" +, Symbol "." +, Word "take" +, Word "a" +, Word "universal" +, Word "set" +, BeginEnv "math" +, Variable "V" +, EndEnv "math" +, Symbol "." +, Word "let" +, BeginEnv "math" +, Variable "R" +, Symbol "=" +, VisibleBraceL +, Variable "x" +, Command "in" +, Variable "V" +, Command "mid" +, Variable "x" +, Command "not" +, Command "in" +, Variable "x" +, VisibleBraceR +, EndEnv "math" +, Symbol "." +, Word "then" +, BeginEnv "math" +, Variable "R" +, Command "in" +, Variable "R" +, EndEnv "math" +, Word "iff" +, BeginEnv "math" +, Variable "R" +, Command "not" +, Command "in" +, Variable "R" +, EndEnv "math" +, Symbol "." +, Word "contradiction" +, Symbol "." +, EndEnv "proof" +] \ No newline at end of file diff --git a/test/golden/russell/verification.golden b/test/golden/russell/verification.golden new file mode 100644 index 0000000..69b9873 --- /dev/null +++ b/test/golden/russell/verification.golden @@ -0,0 +1 @@ +VerificationSuccess \ No newline at end of file -- cgit v1.2.3