diff options
Diffstat (limited to 'test/golden/abbr')
| -rw-r--r-- | test/golden/abbr/encoding tasks.golden | 26 | ||||
| -rw-r--r-- | test/golden/abbr/generating tasks.golden | 1307 | ||||
| -rw-r--r-- | test/golden/abbr/glossing.golden | 519 | ||||
| -rw-r--r-- | test/golden/abbr/verification.golden | 11 |
4 files changed, 0 insertions, 1863 deletions
diff --git a/test/golden/abbr/encoding tasks.golden b/test/golden/abbr/encoding tasks.golden deleted file mode 100644 index cc4e8d9..0000000 --- a/test/golden/abbr/encoding tasks.golden +++ /dev/null @@ -1,26 +0,0 @@ -fof(zf_q0,conjecture,~?[V0]:zf_u0(V0,zf_f0)=>~?[V1]:zf_u0(V1,zf_f0)). ------------------- -fof(zf_q0,conjecture,![V0]:V0=V0). -fof(zf_h0,axiom,![V1]:(~?[V2]:zf_u0(V2,V1)=>~?[V3]:zf_u0(V3,V1))). ------------------- -fof(zf_q0,conjecture,zf_f0=zf_f1=>zf_f0=zf_f1). -fof(zf_h0,axiom,![V0]:(~?[V1]:zf_u0(V1,V0)=>~?[V2]:zf_u0(V2,V0))). -fof(zf_h1,axiom,![V3]:V3=V3). ------------------- -fof(zf_q0,conjecture,~zf_u0(zf_f0,zf_f1)=>~zf_u0(zf_f0,zf_f1)). -fof(zf_h0,axiom,![V0,V1]:(V0=V1=>V0=V1)). -fof(zf_h1,axiom,![V2]:(~?[V3]:zf_u0(V3,V2)=>~?[V4]:zf_u0(V4,V2))). -fof(zf_h2,axiom,![V5]:V5=V5). ------------------- -fof(zf_q0,conjecture,zf_u0(zf_f0,zf_f1)=>zf_u0(zf_f0,zf_f1)). -fof(zf_h0,axiom,![V0,V1]:(V0=V1=>V0=V1)). -fof(zf_h1,axiom,![V2,V3]:(~zf_u0(V2,V3)=>~zf_u0(V2,V3))). -fof(zf_h2,axiom,![V4]:(~?[V5]:zf_u0(V5,V4)=>~?[V6]:zf_u0(V6,V4))). -fof(zf_h3,axiom,![V7]:V7=V7). ------------------- -fof(zf_q0,conjecture,zf_f0=zf_f1=>zf_f0=zf_f1). -fof(zf_h0,axiom,![V0,V1]:(V0=V1=>V0=V1)). -fof(zf_h1,axiom,![V2,V3]:(zf_u0(V2,V3)=>zf_u0(V2,V3))). -fof(zf_h2,axiom,![V4,V5]:(~zf_u0(V4,V5)=>~zf_u0(V4,V5))). -fof(zf_h3,axiom,![V6]:(~?[V7]:zf_u0(V7,V6)=>~?[V8]:zf_u0(V8,V6))). -fof(zf_h4,axiom,![V9]:V9=V9).
\ No newline at end of file diff --git a/test/golden/abbr/generating tasks.golden b/test/golden/abbr/generating tasks.golden deleted file mode 100644 index 7802f08..0000000 --- a/test/golden/abbr/generating tasks.golden +++ /dev/null @@ -1,1307 +0,0 @@ -[ Task - { taskDirectness = Direct - , taskHypotheses = [] - , taskConjectureLabel = Marker "dummy_abbr_test_adj" - , taskLocation = Location - { locFile = "test/examples/abbr.tex" - , locLine = 5 - , locColumn = 1 - } - , taskConjecture = Connected Implication - ( Not - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 2 - , locColumn = 35 - } - ) - ( Quantified Existentially - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 2 - , locColumn = 54 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "x" ) - ) - ) - ] - ) - ) - ) - ) - ( Not - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 2 - , locColumn = 35 - } - ) - ( Quantified Existentially - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 2 - , locColumn = 54 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "x" ) - ) - ) - ] - ) - ) - ) - ) - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "dummy_abbr_test_adj" Quantified Universally - ( Scope - ( Connected Implication - ( Not - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 2 - , locColumn = 35 - } - ) - ( Quantified Existentially - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 2 - , locColumn = 54 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ( Not - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 2 - , locColumn = 35 - } - ) - ( Quantified Existentially - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 2 - , locColumn = 54 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - ] - , taskConjectureLabel = Marker "dummy_abbr_test_noun" - , taskLocation = Location - { locFile = "test/examples/abbr.tex" - , locLine = 15 - , locColumn = 1 - } - , taskConjecture = Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 12 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "dummy_abbr_test_noun" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 12 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - , Hypothesis Marker "dummy_abbr_test_adj" Quantified Universally - ( Scope - ( Connected Implication - ( Not - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 2 - , locColumn = 35 - } - ) - ( Quantified Existentially - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 2 - , locColumn = 54 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ( Not - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 2 - , locColumn = 35 - } - ) - ( Quantified Existentially - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 2 - , locColumn = 54 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - ] - , taskConjectureLabel = Marker "dummy_abbr_test_verb" - , taskLocation = Location - { locFile = "test/examples/abbr.tex" - , locLine = 25 - , locColumn = 1 - } - , taskConjecture = Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 22 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 26 - , locColumn = 38 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - ) - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "dummy_abbr_test_verb" Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 22 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 26 - , locColumn = 38 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "dummy_abbr_test_noun" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 12 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - , Hypothesis Marker "dummy_abbr_test_adj" Quantified Universally - ( Scope - ( Connected Implication - ( Not - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 2 - , locColumn = 35 - } - ) - ( Quantified Existentially - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 2 - , locColumn = 54 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ( Not - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 2 - , locColumn = 35 - } - ) - ( Quantified Existentially - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 2 - , locColumn = 54 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - ] - , taskConjectureLabel = Marker "abbr_test_notin" - , taskLocation = Location - { locFile = "test/examples/abbr.tex" - , locLine = 31 - , locColumn = 1 - } - , taskConjecture = Connected Implication - ( Not - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - ) - ) - ( Not - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 32 - , locColumn = 31 - } - ) - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 32 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - ) - ) - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "abbr_test_notin" Quantified Universally - ( Scope - ( Connected Implication - ( Not - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ( Not - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 32 - , locColumn = 31 - } - ) - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 32 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "dummy_abbr_test_verb" Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 22 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 26 - , locColumn = 38 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "dummy_abbr_test_noun" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 12 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - , Hypothesis Marker "dummy_abbr_test_adj" Quantified Universally - ( Scope - ( Connected Implication - ( Not - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 2 - , locColumn = 35 - } - ) - ( Quantified Existentially - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 2 - , locColumn = 54 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ( Not - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 2 - , locColumn = 35 - } - ) - ( Quantified Existentially - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 2 - , locColumn = 54 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - ] - , taskConjectureLabel = Marker "abbr_test_elementof_is_in" - , taskLocation = Location - { locFile = "test/examples/abbr.tex" - , locLine = 37 - , locColumn = 1 - } - , taskConjecture = Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 38 - , locColumn = 41 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - ) - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "abbr_test_elementof_is_in" Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 38 - , locColumn = 41 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "abbr_test_notin" Quantified Universally - ( Scope - ( Connected Implication - ( Not - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ( Not - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 32 - , locColumn = 31 - } - ) - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 32 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "dummy_abbr_test_verb" Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 22 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 26 - , locColumn = 38 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "dummy_abbr_test_noun" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 12 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - , Hypothesis Marker "dummy_abbr_test_adj" Quantified Universally - ( Scope - ( Connected Implication - ( Not - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 2 - , locColumn = 35 - } - ) - ( Quantified Existentially - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 2 - , locColumn = 54 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ( Not - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 2 - , locColumn = 35 - } - ) - ( Quantified Existentially - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 2 - , locColumn = 54 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - ] - , taskConjectureLabel = Marker "abbr_test_equals_is_eq" - , taskLocation = Location - { locFile = "test/examples/abbr.tex" - , locLine = 43 - , locColumn = 1 - } - , taskConjecture = Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 44 - , locColumn = 32 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - ) - } -]
\ No newline at end of file diff --git a/test/golden/abbr/glossing.golden b/test/golden/abbr/glossing.golden deleted file mode 100644 index 412f914..0000000 --- a/test/golden/abbr/glossing.golden +++ /dev/null @@ -1,519 +0,0 @@ -[ BlockAbbr - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 1 - , locColumn = 1 - } - ) - ( Marker "empty" ) - ( Abbreviation - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "empty" ) End - ) - ( Marker "empty" ) - ) - ) - ) - ( Scope - ( Not - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 2 - , locColumn = 35 - } - ) - ( Quantified Existentially - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 2 - , locColumn = 54 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( F - ( TermVar - ( B 0 ) - ) - ) - ] - ) - ) - ) - ) - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 5 - , locColumn = 1 - } - ) - ( Marker "dummy_abbr_test_adj" ) - ( Lemma [] - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 6 - , locColumn = 14 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "empty" ) End - ) - ( Marker "empty" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 6 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "empty" ) End - ) - ( Marker "empty" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - ] - ) - ) - ) -, BlockAbbr - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 11 - , locColumn = 1 - } - ) - ( Marker "function" ) - ( Abbreviation - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "function" ) End - , pl = TokenCons - ( Word "functions" ) End - } - ) - ( Marker "function" ) - ) - ) - ) - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 12 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B 0 ) - , TermVar - ( B 0 ) - ] - ) - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 15 - , locColumn = 1 - } - ) - ( Marker "dummy_abbr_test_noun" ) - ( Lemma [] - ( Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 16 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "function" ) End - , pl = TokenCons - ( Word "functions" ) End - } - ) - ( Marker "function" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ) - ) -, BlockAbbr - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 21 - , locColumn = 1 - } - ) - ( Marker "converges" ) - ( Abbreviation - ( SymbolPredicate - ( PredicateVerb - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "converges" ) - ( TokenCons - ( Word "to" ) ( HoleCons End ) - ) - , pl = TokenCons - ( Word "converge" ) - ( TokenCons - ( Word "to" ) ( HoleCons End ) - ) - } - ) - ( Marker "converges" ) - ) - ) - ) - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 22 - , locColumn = 33 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B 0 ) - , TermVar - ( B 1 ) - ] - ) - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 25 - , locColumn = 1 - } - ) - ( Marker "dummy_abbr_test_verb" ) - ( Lemma [] - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 26 - , locColumn = 12 - } - ) - ( SymbolPredicate - ( PredicateVerb - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "converges" ) - ( TokenCons - ( Word "to" ) ( HoleCons End ) - ) - , pl = TokenCons - ( Word "converge" ) - ( TokenCons - ( Word "to" ) ( HoleCons End ) - ) - } - ) - ( Marker "converges" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 26 - , locColumn = 38 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - ) - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 31 - , locColumn = 1 - } - ) - ( Marker "abbr_test_notin" ) - ( Lemma [] - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 32 - , locColumn = 9 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "notin" ) - ( ParameterArity 0 ) - ( Marker "notelem" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - ) - ( Not - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 32 - , locColumn = 31 - } - ) - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 32 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - ) - ) - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 37 - , locColumn = 1 - } - ) - ( Marker "abbr_test_elementof_is_in" ) - ( Lemma [] - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 38 - , locColumn = 18 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "element" ) - ( TokenCons - ( Word "of" ) ( HoleCons End ) - ) - , pl = TokenCons - ( Word "elements" ) - ( TokenCons - ( Word "of" ) ( HoleCons End ) - ) - } - ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 38 - , locColumn = 41 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - ) - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 43 - , locColumn = 1 - } - ) - ( Marker "abbr_test_equals_is_eq" ) - ( Lemma [] - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 44 - , locColumn = 12 - } - ) - ( SymbolPredicate - ( PredicateVerb - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "equals" ) ( HoleCons End ) - , pl = TokenCons - ( Word "equal" ) ( HoleCons End ) - } - ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/abbr.tex" - , locLine = 44 - , locColumn = 32 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - ) - ) - ) -]
\ No newline at end of file diff --git a/test/golden/abbr/verification.golden b/test/golden/abbr/verification.golden deleted file mode 100644 index 698681a..0000000 --- a/test/golden/abbr/verification.golden +++ /dev/null @@ -1,11 +0,0 @@ -VerifiedWithTrustedVampire - ( VerificationReport - { verificationRoute = LegacyVerificationRoute - , verificationLegacyDeclaredAssumptionCount = 0 - , verificationTypedDeclaredAssumptionCount = 0 - , verificationTrustedVampireCount = 6 - , verificationExplicitGapLocations = [] - , verificationTrustedLegacyRuleCount = 0 - , verificationKernelProofCount = 0 - } - )
\ No newline at end of file |