diff options
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 | 2039 | ||||
| -rw-r--r-- | test/golden/union/glossing.golden | 734 | ||||
| -rw-r--r-- | test/golden/union/verification.golden | 11 |
4 files changed, 0 insertions, 2805 deletions
diff --git a/test/golden/union/encoding tasks.golden b/test/golden/union/encoding tasks.golden deleted file mode 100644 index 444a277..0000000 --- a/test/golden/union/encoding tasks.golden +++ /dev/null @@ -1,21 +0,0 @@ -fof(zf_q0,conjecture,zf_u0(zf_f0,zf_f1)=zf_u0(zf_f1,zf_f0)). -fof(zf_h0,axiom,![V0,V1,V2]:(zf_u1(V0,zf_u0(V1,V2))<=>(zf_u1(V0,V1)|zf_u1(V0,V2)))). -fof(zf_h1,axiom,![V3,V4]:(![V5]:(zf_u1(V5,V3)<=>zf_u1(V5,V4))=>V3=V4)). ------------------- -fof(zf_q0,conjecture,![V0]:(zf_u1(V0,zf_u0(zf_u0(zf_f0,zf_f1),zf_f2))=>zf_u1(V0,zf_u0(zf_f0,zf_u0(zf_f1,zf_f2))))). -fof(zf_h0,axiom,![V1,V2,V3]:(zf_u1(V1,zf_u0(V2,V3))<=>(zf_u1(V1,V2)|zf_u1(V1,V3)))). -fof(zf_h1,axiom,![V4,V5]:(![V6]:(zf_u1(V6,V4)<=>zf_u1(V6,V5))=>V4=V5)). -fof(zf_h2,axiom,![V7,V8]:zf_u0(V7,V8)=zf_u0(V8,V7)). ------------------- -fof(zf_q0,conjecture,![V0]:(zf_u1(V0,zf_u0(zf_f0,zf_u0(zf_f1,zf_f2)))=>zf_u1(V0,zf_u0(zf_u0(zf_f0,zf_f1),zf_f2)))). -fof(zf_h0,axiom,![V1,V2,V3]:(zf_u1(V1,zf_u0(V2,V3))<=>(zf_u1(V1,V2)|zf_u1(V1,V3)))). -fof(zf_h1,axiom,![V4,V5]:(![V6]:(zf_u1(V6,V4)<=>zf_u1(V6,V5))=>V4=V5)). -fof(zf_h2,axiom,![V7,V8]:zf_u0(V7,V8)=zf_u0(V8,V7)). -fof(zf_h3,axiom,![V9]:(zf_u1(V9,zf_u0(zf_u0(zf_f0,zf_f1),zf_f2))=>zf_u1(V9,zf_u0(zf_f0,zf_u0(zf_f1,zf_f2))))). ------------------- -fof(zf_q0,conjecture,zf_u0(zf_u0(zf_f0,zf_f1),zf_f2)=zf_u0(zf_f0,zf_u0(zf_f1,zf_f2))). -fof(zf_h0,axiom,![V0,V1,V2]:(zf_u1(V0,zf_u0(V1,V2))<=>(zf_u1(V0,V1)|zf_u1(V0,V2)))). -fof(zf_h1,axiom,![V3,V4]:(![V5]:(zf_u1(V5,V3)<=>zf_u1(V5,V4))=>V3=V4)). -fof(zf_h2,axiom,![V6,V7]:zf_u0(V6,V7)=zf_u0(V7,V6)). -fof(zf_h3,axiom,![V8]:(zf_u1(V8,zf_u0(zf_f0,zf_u0(zf_f1,zf_f2)))=>zf_u1(V8,zf_u0(zf_u0(zf_f0,zf_f1),zf_f2)))). -fof(zf_h4,axiom,![V9]:(zf_u1(V9,zf_u0(zf_u0(zf_f0,zf_f1),zf_f2))=>zf_u1(V9,zf_u0(zf_f0,zf_u0(zf_f1,zf_f2))))).
\ No newline at end of file diff --git a/test/golden/union/generating tasks.golden b/test/golden/union/generating tasks.golden deleted file mode 100644 index 06620f8..0000000 --- a/test/golden/union/generating tasks.golden +++ /dev/null @@ -1,2039 +0,0 @@ -[ Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "union_defn" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction ( PropositionalConstant IsTop ) ( PropositionalConstant IsTop ) ) - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 8 - , locColumn = 7 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 8 - , locColumn = 11 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "A" ) - ) - , TermVar - ( B - ( NamedVar "B" ) - ) - ] - ] - ) - ( Connected Disjunction - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 8 - , locColumn = 28 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "A" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 8 - , locColumn = 40 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "B" ) - ) - ] - ) - ) - ) - ) - ) - , Hypothesis Marker "ext" Quantified Universally - ( Scope - ( Connected Implication - ( Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 2 - , locColumn = 35 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "A" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 2 - , locColumn = 48 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "B" ) - ) - ) - ) - ] - ) - ) - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 3 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "A" ) - ) - , TermVar - ( B - ( NamedVar "B" ) - ) - ] - ) - ) - ) - ] - , taskConjectureLabel = Marker "union_comm" - , taskLocation = Location - { locFile = "test/examples/union.tex" - , locLine = 11 - , locColumn = 1 - } - , taskConjecture = TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 12 - , locColumn = 16 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 12 - , locColumn = 6 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( NamedVar "A" ) - , TermVar - ( NamedVar "B" ) - ] - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 12 - , locColumn = 18 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( NamedVar "B" ) - , TermVar - ( NamedVar "A" ) - ] - ] - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "union_comm" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 12 - , locColumn = 16 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 12 - , locColumn = 6 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "A" ) - ) - , TermVar - ( B - ( NamedVar "B" ) - ) - ] - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 12 - , locColumn = 18 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "B" ) - ) - , TermVar - ( B - ( NamedVar "A" ) - ) - ] - ] - ) - ) - , Hypothesis Marker "union_defn" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction ( PropositionalConstant IsTop ) ( PropositionalConstant IsTop ) ) - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 8 - , locColumn = 7 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 8 - , locColumn = 11 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "A" ) - ) - , TermVar - ( B - ( NamedVar "B" ) - ) - ] - ] - ) - ( Connected Disjunction - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 8 - , locColumn = 28 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "A" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 8 - , locColumn = 40 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "B" ) - ) - ] - ) - ) - ) - ) - ) - , Hypothesis Marker "ext" Quantified Universally - ( Scope - ( Connected Implication - ( Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 2 - , locColumn = 35 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "A" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 2 - , locColumn = 48 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "B" ) - ) - ) - ) - ] - ) - ) - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 3 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "A" ) - ) - , TermVar - ( B - ( NamedVar "B" ) - ) - ] - ) - ) - ) - ] - , taskConjectureLabel = Marker "union_assoc" - , taskLocation = Location - { locFile = "test/examples/union.tex" - , locLine = 19 - , locColumn = 5 - } - , taskConjecture = Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 19 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 19 - , locColumn = 35 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 19 - , locColumn = 35 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( F - ( TermVar - ( NamedVar "A" ) - ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "B" ) - ) - ) - ] - , TermVar - ( F - ( TermVar - ( NamedVar "C" ) - ) - ) - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 19 - , locColumn = 63 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 19 - , locColumn = 67 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( F - ( TermVar - ( NamedVar "A" ) - ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 19 - , locColumn = 76 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( F - ( TermVar - ( NamedVar "B" ) - ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "C" ) - ) - ) - ] - ] - ] - ) - ) - ) - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "union_comm" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 12 - , locColumn = 16 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 12 - , locColumn = 6 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "A" ) - ) - , TermVar - ( B - ( NamedVar "B" ) - ) - ] - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 12 - , locColumn = 18 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "B" ) - ) - , TermVar - ( B - ( NamedVar "A" ) - ) - ] - ] - ) - ) - , Hypothesis Marker "union_defn" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction ( PropositionalConstant IsTop ) ( PropositionalConstant IsTop ) ) - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 8 - , locColumn = 7 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 8 - , locColumn = 11 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "A" ) - ) - , TermVar - ( B - ( NamedVar "B" ) - ) - ] - ] - ) - ( Connected Disjunction - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 8 - , locColumn = 28 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "A" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 8 - , locColumn = 40 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "B" ) - ) - ] - ) - ) - ) - ) - ) - , Hypothesis Marker "ext" Quantified Universally - ( Scope - ( Connected Implication - ( Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 2 - , locColumn = 35 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "A" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 2 - , locColumn = 48 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "B" ) - ) - ) - ) - ] - ) - ) - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 3 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "A" ) - ) - , TermVar - ( B - ( NamedVar "B" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "_local_1" Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 19 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 19 - , locColumn = 35 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 19 - , locColumn = 35 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( F - ( TermVar - ( NamedVar "A" ) - ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "B" ) - ) - ) - ] - , TermVar - ( F - ( TermVar - ( NamedVar "C" ) - ) - ) - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 19 - , locColumn = 63 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 19 - , locColumn = 67 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( F - ( TermVar - ( NamedVar "A" ) - ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 19 - , locColumn = 76 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( F - ( TermVar - ( NamedVar "B" ) - ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "C" ) - ) - ) - ] - ] - ] - ) - ) - ) - ] - , taskConjectureLabel = Marker "union_assoc" - , taskLocation = Location - { locFile = "test/examples/union.tex" - , locLine = 20 - , locColumn = 5 - } - , taskConjecture = Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 20 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 20 - , locColumn = 34 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( F - ( TermVar - ( NamedVar "A" ) - ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 20 - , locColumn = 43 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( F - ( TermVar - ( NamedVar "B" ) - ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "C" ) - ) - ) - ] - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 20 - , locColumn = 63 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 20 - , locColumn = 68 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 20 - , locColumn = 68 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( F - ( TermVar - ( NamedVar "A" ) - ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "B" ) - ) - ) - ] - , TermVar - ( F - ( TermVar - ( NamedVar "C" ) - ) - ) - ] - ] - ) - ) - ) - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "union_comm" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 12 - , locColumn = 16 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 12 - , locColumn = 6 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "A" ) - ) - , TermVar - ( B - ( NamedVar "B" ) - ) - ] - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 12 - , locColumn = 18 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "B" ) - ) - , TermVar - ( B - ( NamedVar "A" ) - ) - ] - ] - ) - ) - , Hypothesis Marker "union_defn" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction ( PropositionalConstant IsTop ) ( PropositionalConstant IsTop ) ) - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 8 - , locColumn = 7 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 8 - , locColumn = 11 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "A" ) - ) - , TermVar - ( B - ( NamedVar "B" ) - ) - ] - ] - ) - ( Connected Disjunction - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 8 - , locColumn = 28 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "A" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 8 - , locColumn = 40 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "B" ) - ) - ] - ) - ) - ) - ) - ) - , Hypothesis Marker "ext" Quantified Universally - ( Scope - ( Connected Implication - ( Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 2 - , locColumn = 35 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "A" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 2 - , locColumn = 48 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "B" ) - ) - ) - ) - ] - ) - ) - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 3 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "A" ) - ) - , TermVar - ( B - ( NamedVar "B" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "_local_2" Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 20 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 20 - , locColumn = 34 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( F - ( TermVar - ( NamedVar "A" ) - ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 20 - , locColumn = 43 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( F - ( TermVar - ( NamedVar "B" ) - ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "C" ) - ) - ) - ] - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 20 - , locColumn = 63 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 20 - , locColumn = 68 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 20 - , locColumn = 68 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( F - ( TermVar - ( NamedVar "A" ) - ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "B" ) - ) - ) - ] - , TermVar - ( F - ( TermVar - ( NamedVar "C" ) - ) - ) - ] - ] - ) - ) - ) - , Hypothesis Marker "_local_1" Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 19 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 19 - , locColumn = 35 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 19 - , locColumn = 35 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( F - ( TermVar - ( NamedVar "A" ) - ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "B" ) - ) - ) - ] - , TermVar - ( F - ( TermVar - ( NamedVar "C" ) - ) - ) - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 19 - , locColumn = 63 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 19 - , locColumn = 67 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( F - ( TermVar - ( NamedVar "A" ) - ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 19 - , locColumn = 76 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( F - ( TermVar - ( NamedVar "B" ) - ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "C" ) - ) - ) - ] - ] - ] - ) - ) - ) - ] - , taskConjectureLabel = Marker "union_assoc" - , taskLocation = Location - { locFile = "test/examples/union.tex" - , locLine = 21 - , locColumn = 1 - } - , taskConjecture = TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 16 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 16 - , locColumn = 7 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 16 - , locColumn = 7 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( NamedVar "A" ) - , TermVar - ( NamedVar "B" ) - ] - , TermVar - ( NamedVar "C" ) - ] - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 16 - , locColumn = 28 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( NamedVar "A" ) - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 16 - , locColumn = 37 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ 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 deleted file mode 100644 index 31d05fe..0000000 --- a/test/golden/union/glossing.golden +++ /dev/null @@ -1,734 +0,0 @@ -[ BlockAxiom - ( Location - { locFile = "test/examples/union.tex" - , locLine = 1 - , locColumn = 1 - } - ) - ( Marker "ext" ) - ( Axiom - [ Asm - ( Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 2 - , locColumn = 35 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "A" ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 2 - , locColumn = 48 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "B" ) - ) - ) - ] - ) - ) - ) - ) - ] - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 3 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "A" ) - , TermVar - ( NamedVar "B" ) - ] - ) - ) -, BlockAxiom - ( Location - { locFile = "test/examples/union.tex" - , locLine = 6 - , locColumn = 1 - } - ) - ( Marker "union_defn" ) - ( Axiom - [ Asm ( PropositionalConstant IsTop ) - , Asm ( PropositionalConstant IsTop ) - ] - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 8 - , locColumn = 7 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "a" ) - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 8 - , locColumn = 11 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( NamedVar "A" ) - , TermVar - ( NamedVar "B" ) - ] - ] - ) - ( Connected Disjunction - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 8 - , locColumn = 28 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "A" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 8 - , locColumn = 40 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "B" ) - ] - ) - ) - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/union.tex" - , locLine = 11 - , locColumn = 1 - } - ) - ( Marker "union_comm" ) - ( Lemma [] - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 12 - , locColumn = 16 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 12 - , locColumn = 6 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( NamedVar "A" ) - , TermVar - ( NamedVar "B" ) - ] - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 12 - , locColumn = 18 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( NamedVar "B" ) - , TermVar - ( NamedVar "A" ) - ] - ] - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/union.tex" - , locLine = 15 - , locColumn = 1 - } - ) - ( Marker "union_assoc" ) - ( Lemma [] - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 16 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 16 - , locColumn = 7 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 16 - , locColumn = 7 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( NamedVar "A" ) - , TermVar - ( NamedVar "B" ) - ] - , TermVar - ( NamedVar "C" ) - ] - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 16 - , locColumn = 28 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( NamedVar "A" ) - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 16 - , locColumn = 37 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( NamedVar "B" ) - , TermVar - ( NamedVar "C" ) - ] - ] - ] - ) - ) -, BlockProof - ( Location - { locFile = "test/examples/union.tex" - , locLine = 18 - , locColumn = 1 - } - ) - ( Location - { locFile = "test/examples/union.tex" - , locLine = 21 - , locColumn = 1 - } - ) - ( Have - ( Location - { locFile = "test/examples/union.tex" - , locLine = 19 - , locColumn = 5 - } - ) - ( Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 19 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 19 - , locColumn = 35 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 19 - , locColumn = 35 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( F - ( TermVar - ( NamedVar "A" ) - ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "B" ) - ) - ) - ] - , TermVar - ( F - ( TermVar - ( NamedVar "C" ) - ) - ) - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 19 - , locColumn = 63 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 19 - , locColumn = 67 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( F - ( TermVar - ( NamedVar "A" ) - ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 19 - , locColumn = 76 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( F - ( TermVar - ( NamedVar "B" ) - ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "C" ) - ) - ) - ] - ] - ] - ) - ) - ) - ) JustificationEmpty - ( Have - ( Location - { locFile = "test/examples/union.tex" - , locLine = 20 - , locColumn = 5 - } - ) - ( Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 20 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 20 - , locColumn = 34 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( F - ( TermVar - ( NamedVar "A" ) - ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 20 - , locColumn = 43 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( F - ( TermVar - ( NamedVar "B" ) - ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "C" ) - ) - ) - ] - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 20 - , locColumn = 63 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 20 - , locColumn = 68 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/union.tex" - , locLine = 20 - , locColumn = 68 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "union" ) ( HoleCons End ) - ) - ) - ( Marker "union" ) LeftAssoc - ) - ) - [ TermVar - ( F - ( TermVar - ( NamedVar "A" ) - ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "B" ) - ) - ) - ] - , TermVar - ( F - ( TermVar - ( NamedVar "C" ) - ) - ) - ] - ] - ) - ) - ) - ) JustificationEmpty - ( Qed - { mloc = Nothing - , by = JustificationEmpty - } - ) - ) - ) -]
\ No newline at end of file diff --git a/test/golden/union/verification.golden b/test/golden/union/verification.golden deleted file mode 100644 index e7f6356..0000000 --- a/test/golden/union/verification.golden +++ /dev/null @@ -1,11 +0,0 @@ -VerifiedWithTrustedVampire - ( VerificationReport - { verificationRoute = LegacyVerificationRoute - , verificationLegacyDeclaredAssumptionCount = 2 - , verificationTypedDeclaredAssumptionCount = 0 - , verificationTrustedVampireCount = 4 - , verificationExplicitGapLocations = [] - , verificationTrustedLegacyRuleCount = 1 - , verificationKernelProofCount = 0 - } - )
\ No newline at end of file |