diff options
| author | adelon <22380201+adelon@users.noreply.github.com> | 2024-02-10 02:22:14 +0100 |
|---|---|---|
| committer | adelon <22380201+adelon@users.noreply.github.com> | 2024-02-10 02:22:14 +0100 |
| commit | 442d732696ad431b84f6e5c72b6ee785be4fd968 (patch) | |
| tree | b476f395e7e91d67bacb6758bc84914b8711593f /test/golden/union | |
Initial commit
Diffstat (limited to 'test/golden/union')
| -rw-r--r-- | test/golden/union/encoding tasks.golden | 21 | ||||
| -rw-r--r-- | test/golden/union/generating tasks.golden | 1335 | ||||
| -rw-r--r-- | test/golden/union/glossing.golden | 456 | ||||
| -rw-r--r-- | test/golden/union/parsing.golden | 406 | ||||
| -rw-r--r-- | test/golden/union/scanning.golden | 1 | ||||
| -rw-r--r-- | test/golden/union/tokenizing.golden | 168 | ||||
| -rw-r--r-- | test/golden/union/verification.golden | 1 |
7 files changed, 2388 insertions, 0 deletions
diff --git a/test/golden/union/encoding tasks.golden b/test/golden/union/encoding tasks.golden new file mode 100644 index 0000000..34d92fd --- /dev/null +++ b/test/golden/union/encoding tasks.golden @@ -0,0 +1,21 @@ +fof(union_comm,conjecture,union(fA,fB)=union(fB,fA)). +fof(union_defn,axiom,![Xa,XA,XB]:(elem(Xa,union(XA,XB))<=>(elem(Xa,XA)|elem(Xa,XB)))). +fof(ext,axiom,![XA,XB]:(![Xa]:(elem(Xa,XA)<=>elem(Xa,XB))=>XA=XB)). +------------------ +fof(union_assoc,conjecture,![Xa]:(elem(Xa,union(union(fA,fB),fC))=>elem(Xa,union(fA,union(fB,fC))))). +fof(union_comm,axiom,![XA,XB]:union(XA,XB)=union(XB,XA)). +fof(union_defn,axiom,![Xa,XA,XB]:(elem(Xa,union(XA,XB))<=>(elem(Xa,XA)|elem(Xa,XB)))). +fof(ext,axiom,![XA,XB]:(![Xa]:(elem(Xa,XA)<=>elem(Xa,XB))=>XA=XB)). +------------------ +fof(union_assoc,conjecture,![Xa]:(elem(Xa,union(fA,union(fB,fC)))=>elem(Xa,union(union(fA,fB),fC)))). +fof(union_comm,axiom,![XA,XB]:union(XA,XB)=union(XB,XA)). +fof(union_defn,axiom,![Xa,XA,XB]:(elem(Xa,union(XA,XB))<=>(elem(Xa,XA)|elem(Xa,XB)))). +fof(ext,axiom,![XA,XB]:(![Xa]:(elem(Xa,XA)<=>elem(Xa,XB))=>XA=XB)). +fof(union_assoc1,axiom,![Xa]:(elem(Xa,union(union(fA,fB),fC))=>elem(Xa,union(fA,union(fB,fC))))). +------------------ +fof(union_assoc,conjecture,union(union(fA,fB),fC)=union(fA,union(fB,fC))). +fof(union_comm,axiom,![XA,XB]:union(XA,XB)=union(XB,XA)). +fof(union_defn,axiom,![Xa,XA,XB]:(elem(Xa,union(XA,XB))<=>(elem(Xa,XA)|elem(Xa,XB)))). +fof(ext,axiom,![XA,XB]:(![Xa]:(elem(Xa,XA)<=>elem(Xa,XB))=>XA=XB)). +fof(union_assoc1,axiom,![Xa]:(elem(Xa,union(fA,union(fB,fC)))=>elem(Xa,union(union(fA,fB),fC)))). +fof(union_assoc2,axiom,![Xa]:(elem(Xa,union(union(fA,fB),fC))=>elem(Xa,union(fA,union(fB,fC))))).
\ No newline at end of file diff --git a/test/golden/union/generating tasks.golden b/test/golden/union/generating tasks.golden new file mode 100644 index 0000000..f7f72bb --- /dev/null +++ b/test/golden/union/generating tasks.golden @@ -0,0 +1,1335 @@ +[ Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "union_defn" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ] + ) + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "ext" + , Quantified Universally + ( Scope + ( Connected Implication + ( Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "A" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "B" ) + ) + ) + ) + ] + ) + ) + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "union_comm" + , taskConjecture = TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( NamedVar "A" ) + , TermVar + ( NamedVar "B" ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( NamedVar "B" ) + , TermVar + ( NamedVar "A" ) + ] + ] + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "union_comm" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "B" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + , + ( Marker "union_defn" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ] + ) + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "ext" + , Quantified Universally + ( Scope + ( Connected Implication + ( Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "A" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "B" ) + ) + ) + ) + ] + ) + ) + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "union_assoc" + , taskConjecture = Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + ] + , TermVar + ( F + ( TermVar + ( NamedVar "C" ) + ) + ) + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "C" ) + ) + ) + ] + ] + ] + ) + ) + ) + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "union_comm" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "B" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + , + ( Marker "union_defn" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ] + ) + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "ext" + , Quantified Universally + ( Scope + ( Connected Implication + ( Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "A" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "B" ) + ) + ) + ) + ] + ) + ) + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "union_assoc1" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + ] + , TermVar + ( F + ( TermVar + ( NamedVar "C" ) + ) + ) + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "C" ) + ) + ) + ] + ] + ] + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "union_assoc" + , taskConjecture = Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "C" ) + ) + ) + ] + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + ] + , TermVar + ( F + ( TermVar + ( NamedVar "C" ) + ) + ) + ] + ] + ) + ) + ) + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "union_comm" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "B" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + , + ( Marker "union_defn" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ] + ) + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ) + ) + ) + ) + , + ( Marker "ext" + , Quantified Universally + ( Scope + ( Connected Implication + ( Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "A" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "B" ) + ) + ) + ) + ] + ) + ) + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ) + ) + ) + , + ( Marker "union_assoc1" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "C" ) + ) + ) + ] + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + ] + , TermVar + ( F + ( TermVar + ( NamedVar "C" ) + ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "union_assoc2" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + ] + , TermVar + ( F + ( TermVar + ( NamedVar "C" ) + ) + ) + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "C" ) + ) + ) + ] + ] + ] + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "union_assoc" + , taskConjecture = TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( NamedVar "A" ) + , TermVar + ( NamedVar "B" ) + ] + , TermVar + ( NamedVar "C" ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( NamedVar "A" ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( NamedVar "B" ) + , TermVar + ( NamedVar "C" ) + ] + ] + ] + } +]
\ No newline at end of file diff --git a/test/golden/union/glossing.golden b/test/golden/union/glossing.golden new file mode 100644 index 0000000..1925c15 --- /dev/null +++ b/test/golden/union/glossing.golden @@ -0,0 +1,456 @@ +[ BlockAxiom + ( SourcePos + { sourceName = "test/examples/union.tex" + , sourceLine = Pos 1 + , sourceColumn = Pos 1 + } + ) + ( Marker "ext" ) + ( Axiom + [ Asm + ( Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + ] + ) + ) + ) + ) + ] + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( NamedVar "A" ) + , TermVar + ( NamedVar "B" ) + ] + ) + ) +, BlockAxiom + ( SourcePos + { sourceName = "test/examples/union.tex" + , sourceLine = Pos 6 + , sourceColumn = Pos 1 + } + ) + ( Marker "union_defn" ) + ( Axiom + [ Asm ( PropositionalConstant IsTop ) + , Asm ( PropositionalConstant IsTop ) + ] + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "a" ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( NamedVar "A" ) + , TermVar + ( NamedVar "B" ) + ] + ] + ) + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "A" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "B" ) + ] + ) + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/union.tex" + , sourceLine = Pos 11 + , sourceColumn = Pos 1 + } + ) + ( Marker "union_comm" ) + ( Lemma [] + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( NamedVar "A" ) + , TermVar + ( NamedVar "B" ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( NamedVar "B" ) + , TermVar + ( NamedVar "A" ) + ] + ] + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/union.tex" + , sourceLine = Pos 15 + , sourceColumn = Pos 1 + } + ) + ( Marker "union_assoc" ) + ( Lemma [] + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( NamedVar "A" ) + , TermVar + ( NamedVar "B" ) + ] + , TermVar + ( NamedVar "C" ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( NamedVar "A" ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( NamedVar "B" ) + , TermVar + ( NamedVar "C" ) + ] + ] + ] + ) + ) +, BlockProof + ( SourcePos + { sourceName = "test/examples/union.tex" + , sourceLine = Pos 18 + , sourceColumn = Pos 1 + } + ) + ( Have + ( Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + ] + , TermVar + ( F + ( TermVar + ( NamedVar "C" ) + ) + ) + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "C" ) + ) + ) + ] + ] + ] + ) + ) + ) + ) JustificationEmpty + ( Have + ( Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "C" ) + ) + ) + ] + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + ] + , TermVar + ( F + ( TermVar + ( NamedVar "C" ) + ) + ) + ] + ] + ) + ) + ) + ) JustificationEmpty ( Qed JustificationEmpty ) + ) + ) +]
\ No newline at end of file diff --git a/test/golden/union/parsing.golden b/test/golden/union/parsing.golden new file mode 100644 index 0000000..391f039 --- /dev/null +++ b/test/golden/union/parsing.golden @@ -0,0 +1,406 @@ +[ BlockAxiom + ( SourcePos + { sourceName = "test/examples/union.tex" + , sourceLine = Pos 1 + , sourceColumn = Pos 1 + } + ) + ( Marker "ext" ) + ( Axiom + [ AsmSuppose + ( SymbolicQuantified Universally + ( NamedVar "a" :| [] ) Unbounded Nothing + ( StmtConnected Equivalence + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "a" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "A" ) :| [] + ) + ) + ) + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "a" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "B" ) :| [] + ) + ) + ) + ) + ) + ) + ] + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "A" ) :| [] + ) Positive + ( RelationSymbol + ( Symbol "=" ) + ) + ( ExprVar + ( NamedVar "B" ) :| [] + ) + ) + ) + ) + ) +, BlockAxiom + ( SourcePos + { sourceName = "test/examples/union.tex" + , sourceLine = Pos 6 + , sourceColumn = Pos 1 + } + ) + ( Marker "union_defn" ) + ( Axiom + [ AsmLetNoun + ( NamedVar "A" :| + [ NamedVar "B" ] + ) NounPhrase ( [] ) + ( Noun + ( SgPl + { sg = + [ Just + ( Word "set" ) + ] + , pl = + [ Just + ( Word "sets" ) + ] + } + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + ] + ( StmtConnected Equivalence + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "a" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprOp + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + [ ExprVar + ( NamedVar "A" ) + , ExprVar + ( NamedVar "B" ) + ] :| [] + ) + ) + ) + ) + ( StmtConnected Disjunction + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "a" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "A" ) :| [] + ) + ) + ) + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "a" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "B" ) :| [] + ) + ) + ) + ) + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/union.tex" + , sourceLine = Pos 11 + , sourceColumn = Pos 1 + } + ) + ( Marker "union_comm" ) + ( Lemma [] + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprOp + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + [ ExprVar + ( NamedVar "A" ) + , ExprVar + ( NamedVar "B" ) + ] :| [] + ) Positive + ( RelationSymbol + ( Symbol "=" ) + ) + ( ExprOp + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + [ ExprVar + ( NamedVar "B" ) + , ExprVar + ( NamedVar "A" ) + ] :| [] + ) + ) + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/union.tex" + , sourceLine = Pos 15 + , sourceColumn = Pos 1 + } + ) + ( Marker "union_assoc" ) + ( Lemma [] + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprOp + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + [ ExprOp + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + [ ExprVar + ( NamedVar "A" ) + , ExprVar + ( NamedVar "B" ) + ] + , ExprVar + ( NamedVar "C" ) + ] :| [] + ) Positive + ( RelationSymbol + ( Symbol "=" ) + ) + ( ExprOp + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + [ ExprVar + ( NamedVar "A" ) + , ExprOp + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + [ ExprVar + ( NamedVar "B" ) + , ExprVar + ( NamedVar "C" ) + ] + ] :| [] + ) + ) + ) + ) + ) +, BlockProof + ( SourcePos + { sourceName = "test/examples/union.tex" + , sourceLine = Pos 18 + , sourceColumn = Pos 1 + } + ) + ( Have Nothing + ( SymbolicQuantified Universally + ( NamedVar "a" :| [] ) Unbounded Nothing + ( StmtConnected Implication + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "a" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprOp + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + [ ExprOp + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + [ ExprVar + ( NamedVar "A" ) + , ExprVar + ( NamedVar "B" ) + ] + , ExprVar + ( NamedVar "C" ) + ] :| [] + ) + ) + ) + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "a" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprOp + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + [ ExprVar + ( NamedVar "A" ) + , ExprOp + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + [ ExprVar + ( NamedVar "B" ) + , ExprVar + ( NamedVar "C" ) + ] + ] :| [] + ) + ) + ) + ) + ) + ) JustificationEmpty + ( Have Nothing + ( SymbolicQuantified Universally + ( NamedVar "a" :| [] ) Unbounded Nothing + ( StmtConnected Implication + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "a" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprOp + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + [ ExprVar + ( NamedVar "A" ) + , ExprOp + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + [ ExprVar + ( NamedVar "B" ) + , ExprVar + ( NamedVar "C" ) + ] + ] :| [] + ) + ) + ) + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "a" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprOp + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + [ ExprOp + [ Nothing + , Just + ( Command "union" ) + , Nothing + ] + [ ExprVar + ( NamedVar "A" ) + , ExprVar + ( NamedVar "B" ) + ] + , ExprVar + ( NamedVar "C" ) + ] :| [] + ) + ) + ) + ) + ) + ) JustificationEmpty ( Qed JustificationEmpty ) + ) + ) +]
\ No newline at end of file diff --git a/test/golden/union/scanning.golden b/test/golden/union/scanning.golden new file mode 100644 index 0000000..0637a08 --- /dev/null +++ b/test/golden/union/scanning.golden @@ -0,0 +1 @@ +[]
\ No newline at end of file diff --git a/test/golden/union/tokenizing.golden b/test/golden/union/tokenizing.golden new file mode 100644 index 0000000..e336098 --- /dev/null +++ b/test/golden/union/tokenizing.golden @@ -0,0 +1,168 @@ +[ BeginEnv "axiom" +, BracketL +, Word "extensionality" +, BracketR +, Label "ext" +, Word "suppose" +, Word "for" +, Word "all" +, BeginEnv "math" +, Variable "a" +, EndEnv "math" +, Word "we" +, Word "have" +, BeginEnv "math" +, Variable "a" +, Command "in" +, Variable "A" +, EndEnv "math" +, Word "iff" +, BeginEnv "math" +, Variable "a" +, Command "in" +, Variable "B" +, EndEnv "math" +, Symbol "." +, Word "then" +, BeginEnv "math" +, Variable "A" +, Symbol "=" +, Variable "B" +, EndEnv "math" +, Symbol "." +, EndEnv "axiom" +, BeginEnv "axiom" +, Label "union_defn" +, Word "let" +, BeginEnv "math" +, Variable "A" +, Symbol "," +, Variable "B" +, EndEnv "math" +, Word "be" +, Word "sets" +, Symbol "." +, BeginEnv "math" +, Variable "a" +, Command "in" +, Variable "A" +, Command "union" +, Variable "B" +, EndEnv "math" +, Word "iff" +, BeginEnv "math" +, Variable "a" +, Command "in" +, Variable "A" +, EndEnv "math" +, Word "or" +, BeginEnv "math" +, Variable "a" +, Command "in" +, Variable "B" +, EndEnv "math" +, Symbol "." +, EndEnv "axiom" +, BeginEnv "proposition" +, Label "union_comm" +, BeginEnv "math" +, Variable "A" +, Command "union" +, Variable "B" +, Symbol "=" +, Variable "B" +, Command "union" +, Variable "A" +, EndEnv "math" +, Symbol "." +, EndEnv "proposition" +, BeginEnv "proposition" +, Label "union_assoc" +, BeginEnv "math" +, ParenL +, Variable "A" +, Command "union" +, Variable "B" +, ParenR +, Command "union" +, Variable "C" +, Symbol "=" +, Variable "A" +, Command "union" +, ParenL +, Variable "B" +, Command "union" +, Variable "C" +, ParenR +, EndEnv "math" +, Symbol "." +, EndEnv "proposition" +, BeginEnv "proof" +, Word "for" +, Word "all" +, BeginEnv "math" +, Variable "a" +, EndEnv "math" +, Word "we" +, Word "have" +, Word "if" +, BeginEnv "math" +, Variable "a" +, Command "in" +, ParenL +, Variable "A" +, Command "union" +, Variable "B" +, ParenR +, Command "union" +, Variable "C" +, EndEnv "math" +, Symbol "," +, Word "then" +, BeginEnv "math" +, Variable "a" +, Command "in" +, Variable "A" +, Command "union" +, ParenL +, Variable "B" +, Command "union" +, Variable "C" +, ParenR +, EndEnv "math" +, Symbol "." +, Word "for" +, Word "all" +, BeginEnv "math" +, Variable "a" +, EndEnv "math" +, Word "we" +, Word "have" +, Word "if" +, BeginEnv "math" +, Variable "a" +, Command "in" +, Variable "A" +, Command "union" +, ParenL +, Variable "B" +, Command "union" +, Variable "C" +, ParenR +, EndEnv "math" +, Symbol "," +, Word "then" +, BeginEnv "math" +, Variable "a" +, Command "in" +, ParenL +, Variable "A" +, Command "union" +, Variable "B" +, ParenR +, Command "union" +, Variable "C" +, EndEnv "math" +, Symbol "." +, EndEnv "proof" +]
\ No newline at end of file diff --git a/test/golden/union/verification.golden b/test/golden/union/verification.golden new file mode 100644 index 0000000..69b9873 --- /dev/null +++ b/test/golden/union/verification.golden @@ -0,0 +1 @@ +VerificationSuccess
\ No newline at end of file |