diff options
Diffstat (limited to 'test/golden/replace')
| -rw-r--r-- | test/golden/replace/encoding tasks.golden | 17 | ||||
| -rw-r--r-- | test/golden/replace/generating tasks.golden | 2241 | ||||
| -rw-r--r-- | test/golden/replace/glossing.golden | 572 | ||||
| -rw-r--r-- | test/golden/replace/verification.golden | 11 |
4 files changed, 0 insertions, 2841 deletions
diff --git a/test/golden/replace/encoding tasks.golden b/test/golden/replace/encoding tasks.golden deleted file mode 100644 index a359f42..0000000 --- a/test/golden/replace/encoding tasks.golden +++ /dev/null @@ -1,17 +0,0 @@ -fof(zf_q0,conjecture,zf_u5(zf_u3(zf_u2,zf_u2),zf_u0(zf_u4,zf_u4))). -fof(zf_h0,axiom,![V0,V1,V2]:(zf_u5(V0,zf_u1(V1,V2))<=>(V0=V1|zf_u5(V0,V2)))). -fof(zf_h1,axiom,![V3,V4]:![V5]:(zf_u5(V5,zf_u0(V3,V4))<=>?[V6,V7]:(zf_u5(V6,V3)&zf_u5(V7,V4)&zf_u3(V6,V7)=V5))). -fof(zf_h2,axiom,![V8]:(zf_u5(V8,zf_u4)<=>(zf_u5(V8,zf_u2)|V8=zf_u2))). ------------------- -fof(zf_q0,conjecture,![V0]:(zf_u5(V0,zf_f0)=>![V1,V2]:((V1=zf_u1(V0,zf_u2)&V2=zf_u1(V0,zf_u2))=>V1=V2))). -fof(zf_h0,axiom,![V3,V4,V5]:(zf_u5(V3,zf_u1(V4,V5))<=>(V3=V4|zf_u5(V3,V5)))). -fof(zf_h1,axiom,![V6,V7]:![V8]:(zf_u5(V8,zf_u0(V6,V7))<=>?[V9,V10]:(zf_u5(V9,V6)&zf_u5(V10,V7)&zf_u3(V9,V10)=V8))). -fof(zf_h2,axiom,![V11]:(zf_u5(V11,zf_u4)<=>(zf_u5(V11,zf_u2)|V11=zf_u2))). -fof(zf_h3,axiom,zf_u5(zf_u3(zf_u2,zf_u2),zf_u0(zf_u4,zf_u4))). ------------------- -fof(zf_q0,conjecture,![V0]:(zf_u6(V0,zf_u0(zf_f0,zf_f1))<=>?[V1,V2]:(zf_u6(V1,zf_f0)&zf_u6(V2,zf_f1)&zf_u3(V1,V2)=V0))). -fof(zf_h0,axiom,![V3,V4,V5]:(zf_u6(V3,zf_u1(V4,V5))<=>(V3=V4|zf_u6(V3,V5)))). -fof(zf_h1,axiom,![V6,V7]:![V8]:(zf_u6(V8,zf_u0(V6,V7))<=>?[V9,V10]:(zf_u6(V9,V6)&zf_u6(V10,V7)&zf_u3(V9,V10)=V8))). -fof(zf_h2,axiom,![V11,V12]:(zf_u6(V11,zf_u4(V12))<=>?[V13]:(zf_u6(V13,V12)&V11=zf_u1(V13,zf_u2)))). -fof(zf_h3,axiom,![V14]:(zf_u6(V14,zf_u5)<=>(zf_u6(V14,zf_u2)|V14=zf_u2))). -fof(zf_h4,axiom,zf_u6(zf_u3(zf_u2,zf_u2),zf_u0(zf_u5,zf_u5))).
\ No newline at end of file diff --git a/test/golden/replace/generating tasks.golden b/test/golden/replace/generating tasks.golden deleted file mode 100644 index cedbc68..0000000 --- a/test/golden/replace/generating tasks.golden +++ /dev/null @@ -1,2241 +0,0 @@ -[ Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "unit" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "any" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 9 - , locColumn = 1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "unit" ) End - ) - ( Marker "unit" ) NonAssoc - ) - ) [] - ] - ) - ( Connected Disjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "any" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 10 - , locColumn = 14 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 9 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "any" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 10 - , locColumn = 16 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - ) - ) - ) - ) - , Hypothesis Marker "times" Quantified Universally - ( Scope - ( Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "frv" ) - ) - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "times" ) ( HoleCons End ) - ) - ) - ( Marker "times" ) RightAssoc - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "A" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "B" ) - ) - ) - ) - ] - ] - ) - ( Quantified Existentially - ( Scope - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( F - ( TermVar - ( F - ( TermVar - ( B - ( NamedVar "A" ) - ) - ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( F - ( TermVar - ( F - ( TermVar - ( B - ( NamedVar "B" ) - ) - ) - ) - ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 6 - , locColumn = 21 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "pair" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "pair" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "frv" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "cons" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 2 - , locColumn = 7 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 2 - , locColumn = 11 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "cons" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "cons" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "X" ) - ) - ] - ] - ) - ( Connected Disjunction - ( TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 2 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 2 - , locColumn = 41 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "X" ) - ) - ] - ) - ) - ) - ) - ] - , taskConjectureLabel = Marker "pair_emptyset_in_times_unit" - , taskLocation = Location - { locFile = "test/examples/replace.tex" - , locLine = 13 - , locColumn = 1 - } - , taskConjecture = TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 14 - , locColumn = 27 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 14 - , locColumn = 6 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "pair" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "pair" ) NonAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 14 - , locColumn = 7 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 14 - , locColumn = 17 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 14 - , locColumn = 31 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "times" ) ( HoleCons End ) - ) - ) - ( Marker "times" ) RightAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 14 - , locColumn = 31 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "unit" ) End - ) - ( Marker "unit" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 14 - , locColumn = 42 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "unit" ) End - ) - ( Marker "unit" ) NonAssoc - ) - ) [] - ] - ] - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "pair_emptyset_in_times_unit" TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 14 - , locColumn = 27 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 14 - , locColumn = 6 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "pair" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "pair" ) NonAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 14 - , locColumn = 7 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 14 - , locColumn = 17 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 14 - , locColumn = 31 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "times" ) ( HoleCons End ) - ) - ) - ( Marker "times" ) RightAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 14 - , locColumn = 31 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "unit" ) End - ) - ( Marker "unit" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 14 - , locColumn = 42 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "unit" ) End - ) - ( Marker "unit" ) NonAssoc - ) - ) [] - ] - ] - , Hypothesis Marker "unit" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "any" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 9 - , locColumn = 1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "unit" ) End - ) - ( Marker "unit" ) NonAssoc - ) - ) [] - ] - ) - ( Connected Disjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "any" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 10 - , locColumn = 14 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 9 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "any" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 10 - , locColumn = 16 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - ) - ) - ) - ) - , Hypothesis Marker "times" Quantified Universally - ( Scope - ( Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "frv" ) - ) - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "times" ) ( HoleCons End ) - ) - ) - ( Marker "times" ) RightAssoc - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "A" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "B" ) - ) - ) - ) - ] - ] - ) - ( Quantified Existentially - ( Scope - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( F - ( TermVar - ( F - ( TermVar - ( B - ( NamedVar "A" ) - ) - ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( F - ( TermVar - ( F - ( TermVar - ( B - ( NamedVar "B" ) - ) - ) - ) - ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 6 - , locColumn = 21 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "pair" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "pair" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "frv" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "cons" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 2 - , locColumn = 7 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 2 - , locColumn = 11 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "cons" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "cons" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "X" ) - ) - ] - ] - ) - ( Connected Disjunction - ( TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 2 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 2 - , locColumn = 41 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "X" ) - ) - ] - ) - ) - ) - ) - ] - , taskConjectureLabel = Marker "suc" - , taskLocation = Location - { locFile = "test/examples/replace.tex" - , locLine = 19 - , locColumn = 1 - } - , taskConjecture = Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( FreshVar 0 ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "a" ) - ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 20 - , locColumn = 44 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( FreshVar 1 ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 20 - , locColumn = 46 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "cons" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "cons" ) NonAssoc - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( FreshVar 0 ) - ) - ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 20 - , locColumn = 46 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 20 - , locColumn = 44 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( FreshVar 2 ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 20 - , locColumn = 46 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "cons" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "cons" ) NonAssoc - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( FreshVar 0 ) - ) - ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 20 - , locColumn = 46 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( FreshVar 1 ) - ) - , TermVar - ( B - ( FreshVar 2 ) - ) - ] - ) - ) - ) - ) - ) - ) - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "suc" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( FreshVar 1 ) - ) - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "suc" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "suc" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - ] - ] - ) - ( Quantified Existentially - ( Scope - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( FreshVar 0 ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "a" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 20 - , locColumn = 44 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( FreshVar 1 ) - ) - ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 20 - , locColumn = 46 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "cons" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "cons" ) NonAssoc - ) - ) - [ TermVar - ( B - ( FreshVar 0 ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 20 - , locColumn = 46 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - ] - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "pair_emptyset_in_times_unit" TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 14 - , locColumn = 27 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 14 - , locColumn = 6 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "pair" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "pair" ) NonAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 14 - , locColumn = 7 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 14 - , locColumn = 17 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 14 - , locColumn = 31 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "times" ) ( HoleCons End ) - ) - ) - ( Marker "times" ) RightAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 14 - , locColumn = 31 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "unit" ) End - ) - ( Marker "unit" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 14 - , locColumn = 42 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "unit" ) End - ) - ( Marker "unit" ) NonAssoc - ) - ) [] - ] - ] - , Hypothesis Marker "unit" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "any" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 9 - , locColumn = 1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "unit" ) End - ) - ( Marker "unit" ) NonAssoc - ) - ) [] - ] - ) - ( Connected Disjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "any" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 10 - , locColumn = 14 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 9 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "any" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 10 - , locColumn = 16 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - ) - ) - ) - ) - , Hypothesis Marker "times" Quantified Universally - ( Scope - ( Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "frv" ) - ) - , TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "times" ) ( HoleCons End ) - ) - ) - ( Marker "times" ) RightAssoc - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "A" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "B" ) - ) - ) - ) - ] - ] - ) - ( Quantified Existentially - ( Scope - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( F - ( TermVar - ( F - ( TermVar - ( B - ( NamedVar "A" ) - ) - ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( F - ( TermVar - ( F - ( TermVar - ( B - ( NamedVar "B" ) - ) - ) - ) - ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 6 - , locColumn = 21 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "pair" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "pair" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "frv" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "cons" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 2 - , locColumn = 7 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 2 - , locColumn = 11 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "cons" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "cons" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "X" ) - ) - ] - ] - ) - ( Connected Disjunction - ( TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 2 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 2 - , locColumn = 41 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "X" ) - ) - ] - ) - ) - ) - ) - ] - , taskConjectureLabel = Marker "times_replacement_test" - , taskLocation = Location - { locFile = "test/examples/replace.tex" - , locLine = 25 - , locColumn = 1 - } - , taskConjecture = Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "frv" ) - ) - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 26 - , locColumn = 6 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "times" ) ( HoleCons End ) - ) - ) - ( Marker "times" ) RightAssoc - ) - ) - [ TermVar - ( F - ( TermVar - ( NamedVar "A" ) - ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "B" ) - ) - ) - ] - ] - ) - ( Quantified Existentially - ( Scope - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( F - ( TermVar - ( F - ( TermVar - ( NamedVar "A" ) - ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "b" ) - ) - , TermVar - ( F - ( TermVar - ( F - ( TermVar - ( NamedVar "B" ) - ) - ) - ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 26 - , locColumn = 21 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "pair" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "pair" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "frv" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - } -]
\ No newline at end of file diff --git a/test/golden/replace/glossing.golden b/test/golden/replace/glossing.golden deleted file mode 100644 index dfded02..0000000 --- a/test/golden/replace/glossing.golden +++ /dev/null @@ -1,572 +0,0 @@ -[ BlockAxiom - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 1 - , locColumn = 1 - } - ) - ( Marker "cons" ) - ( Axiom [] - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 2 - , locColumn = 7 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 2 - , locColumn = 11 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "cons" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "cons" ) NonAssoc - ) - ) - [ TermVar - ( NamedVar "y" ) - , TermVar - ( NamedVar "X" ) - ] - ] - ) - ( Connected Disjunction - ( TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 2 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 2 - , locColumn = 41 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "X" ) - ] - ) - ) - ) - ) -, BlockDefn - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 5 - , locColumn = 1 - } - ) - ( Marker "times" ) - ( DefnOp - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "times" ) ( HoleCons End ) - ) - ) - ( Marker "times" ) RightAssoc - ) - [ NamedVar "A" - , NamedVar "B" - ] - ( ReplaceFun - ( - ( NamedVar "a" - , TermVar - ( NamedVar "A" ) - ) :| - [ - ( NamedVar "b" - , TermVar - ( NamedVar "B" ) - ) - ] - ) - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 6 - , locColumn = 21 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "pair" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "pair" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( Scope ( PropositionalConstant IsTop ) ) - ) - ) -, BlockDefn - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 9 - , locColumn = 1 - } - ) - ( Marker "unit" ) - ( DefnOp - ( MixfixItem - ( TokenCons - ( Command "unit" ) End - ) - ( Marker "unit" ) NonAssoc - ) [] - ( TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 10 - , locColumn = 14 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "cons" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "cons" ) NonAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 10 - , locColumn = 16 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 10 - , locColumn = 14 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 13 - , locColumn = 1 - } - ) - ( Marker "pair_emptyset_in_times_unit" ) - ( Lemma [] - ( TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 14 - , locColumn = 27 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 14 - , locColumn = 6 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "pair" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "pair" ) NonAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 14 - , locColumn = 7 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 14 - , locColumn = 17 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 14 - , locColumn = 31 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "times" ) ( HoleCons End ) - ) - ) - ( Marker "times" ) RightAssoc - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 14 - , locColumn = 31 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "unit" ) End - ) - ( Marker "unit" ) NonAssoc - ) - ) [] - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 14 - , locColumn = 42 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "unit" ) End - ) - ( Marker "unit" ) NonAssoc - ) - ) [] - ] - ] - ) - ) -, BlockDefn - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 19 - , locColumn = 1 - } - ) - ( Marker "suc" ) - ( DefnOp - ( MixfixItem - ( TokenCons - ( Command "suc" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "suc" ) NonAssoc - ) - [ NamedVar "a" ] - ( ReplacePred - ( NamedVar "y" ) - ( NamedVar "x" ) - ( TermVar - ( NamedVar "a" ) - ) - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 20 - , locColumn = 44 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar ( B ReplacementRangeVar ) - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 20 - , locColumn = 46 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "cons" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "cons" ) NonAssoc - ) - ) - [ TermVar ( B ReplacementDomVar ) - , TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 20 - , locColumn = 46 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "emptyset" ) End - ) - ( Marker "emptyset" ) NonAssoc - ) - ) [] - ] - ] - ) - ) - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 25 - , locColumn = 1 - } - ) - ( Marker "times_replacement_test" ) - ( Lemma [] - ( TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 26 - , locColumn = 16 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 26 - , locColumn = 6 - } - ) - ( SymbolMixfix - ( MixfixItem - ( HoleCons - ( TokenCons - ( Command "times" ) ( HoleCons End ) - ) - ) - ( Marker "times" ) RightAssoc - ) - ) - [ TermVar - ( NamedVar "A" ) - , TermVar - ( NamedVar "B" ) - ] - , ReplaceFun - ( - ( NamedVar "a" - , TermVar - ( NamedVar "A" ) - ) :| - [ - ( NamedVar "b" - , TermVar - ( NamedVar "B" ) - ) - ] - ) - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/replace.tex" - , locLine = 26 - , locColumn = 21 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "pair" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "pair" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "a" ) - ) - , TermVar - ( B - ( NamedVar "b" ) - ) - ] - ) - ) - ( Scope ( PropositionalConstant IsTop ) ) - ] - ) - ) -]
\ No newline at end of file diff --git a/test/golden/replace/verification.golden b/test/golden/replace/verification.golden deleted file mode 100644 index 68500ff..0000000 --- a/test/golden/replace/verification.golden +++ /dev/null @@ -1,11 +0,0 @@ -VerifiedWithTrustedVampire - ( VerificationReport - { verificationRoute = LegacyVerificationRoute - , verificationLegacyDeclaredAssumptionCount = 1 - , verificationTypedDeclaredAssumptionCount = 0 - , verificationTrustedVampireCount = 3 - , verificationExplicitGapLocations = [] - , verificationTrustedLegacyRuleCount = 3 - , verificationKernelProofCount = 0 - } - )
\ No newline at end of file |