diff options
Diffstat (limited to 'test/golden/calc')
| -rw-r--r-- | test/golden/calc/encoding tasks.golden | 58 | ||||
| -rw-r--r-- | test/golden/calc/generating tasks.golden | 1775 | ||||
| -rw-r--r-- | test/golden/calc/glossing.golden | 574 | ||||
| -rw-r--r-- | test/golden/calc/verification.golden | 11 |
4 files changed, 0 insertions, 2418 deletions
diff --git a/test/golden/calc/encoding tasks.golden b/test/golden/calc/encoding tasks.golden deleted file mode 100644 index cf23f08..0000000 --- a/test/golden/calc/encoding tasks.golden +++ /dev/null @@ -1,58 +0,0 @@ -fof(zf_q0,conjecture,zf_f0=zf_f0). ------------------- -fof(zf_q0,conjecture,zf_f0=zf_f0). -fof(zf_h0,axiom,![V0]:V0=V0). ------------------- -fof(zf_q0,conjecture,zf_f0=zf_f0). -fof(zf_h0,axiom,![V0]:V0=V0). -fof(zf_h1,axiom,![V1]:V1=V1). ------------------- -fof(zf_q0,conjecture,zf_f0=zf_f0). -fof(zf_h0,axiom,![V0]:V0=V0). ------------------- -fof(zf_q0,conjecture,zf_f0=zf_f0). -fof(zf_h0,axiom,![V0]:V0=V0). -fof(zf_h1,axiom,![V1]:V1=V1). -fof(zf_h2,axiom,zf_f0=zf_f0). ------------------- -fof(zf_q0,conjecture,zf_f0=zf_f0). -fof(zf_h0,axiom,![V0]:V0=V0). -fof(zf_h1,axiom,![V1]:V1=V1). -fof(zf_h2,axiom,![V2]:V2=V2). ------------------- -fof(zf_q0,conjecture,zf_f0=zf_f0). -fof(zf_h0,axiom,![V0]:V0=V0). ------------------- -fof(zf_q0,conjecture,zf_f0=zf_f0). -fof(zf_h0,axiom,![V0]:V0=V0). -fof(zf_h1,axiom,![V1]:V1=V1). -fof(zf_h2,axiom,![V2]:V2=V2). -fof(zf_h3,axiom,zf_f0=zf_f0<=>zf_f0=zf_f0). ------------------- -fof(zf_q0,conjecture,![V0]:(zf_u0(V0,zf_f0)=>V0=V0)). -fof(zf_h0,axiom,![V1]:V1=V1). -fof(zf_h1,axiom,![V2]:V2=V2). -fof(zf_h2,axiom,![V3]:V3=V3). -fof(zf_h3,axiom,![V4]:V4=V4). ------------------- -fof(zf_q0,conjecture,![V0]:(zf_u0(V0,zf_f0)=>V0=V0)). -fof(zf_h0,axiom,![V1]:(zf_u0(V1,zf_f0)=>V1=V1)). -fof(zf_h1,axiom,![V2]:V2=V2). -fof(zf_h2,axiom,![V3]:V3=V3). -fof(zf_h3,axiom,![V4]:V4=V4). -fof(zf_h4,axiom,![V5]:V5=V5). ------------------- -fof(zf_q0,conjecture,![V0]:((zf_u0(V0,zf_f0)&V0=V0)=>V0=V0)). -fof(zf_h0,axiom,![V1]:![V2]:(zf_u0(V2,V1)=>V2=V2)). -fof(zf_h1,axiom,![V3]:V3=V3). -fof(zf_h2,axiom,![V4]:V4=V4). -fof(zf_h3,axiom,![V5]:V5=V5). -fof(zf_h4,axiom,![V6]:V6=V6). ------------------- -fof(zf_q0,conjecture,![V0]:((zf_u0(V0,zf_f0)&V0=V0)=>V0=V0)). -fof(zf_h0,axiom,![V1]:![V2]:(zf_u0(V2,V1)=>V2=V2)). -fof(zf_h1,axiom,![V3]:((zf_u0(V3,zf_f0)&V3=V3)=>V3=V3)). -fof(zf_h2,axiom,![V4]:V4=V4). -fof(zf_h3,axiom,![V5]:V5=V5). -fof(zf_h4,axiom,![V6]:V6=V6). -fof(zf_h5,axiom,![V7]:V7=V7).
\ No newline at end of file diff --git a/test/golden/calc/generating tasks.golden b/test/golden/calc/generating tasks.golden deleted file mode 100644 index a6ae184..0000000 --- a/test/golden/calc/generating tasks.golden +++ /dev/null @@ -1,1775 +0,0 @@ -[ Task - { taskDirectness = Direct - , taskHypotheses = [] - , taskConjectureLabel = Marker "trivial" - , taskLocation = Location - { locFile = "test/examples/calc.tex" - , locLine = 1 - , locColumn = 1 - } - , taskConjecture = TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 2 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "x" ) - ] - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "trivial" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 2 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ] - , taskConjectureLabel = Marker "irrelevant" - , taskLocation = Location - { locFile = "test/examples/calc.tex" - , locLine = 5 - , locColumn = 1 - } - , taskConjecture = TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 6 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "z" ) - , TermVar - ( NamedVar "z" ) - ] - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "irrelevant" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 6 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - , Hypothesis Marker "trivial" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 2 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ] - , taskConjectureLabel = Marker "alsotrivial" - , taskLocation = Location - { locFile = "test/examples/calc.tex" - , locLine = 13 - , locColumn = 5 - } - , taskConjecture = TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - , TermVar - ( NamedVar "y" ) - ] - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "trivial" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 2 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ] - , taskConjectureLabel = Marker "alsotrivial" - , taskLocation = Location - { locFile = "test/examples/calc.tex" - , locLine = 13 - , locColumn = 5 - } - , taskConjecture = TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - , TermVar - ( NamedVar "y" ) - ] - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "irrelevant" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 6 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - , Hypothesis Marker "trivial" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 2 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - , Hypothesis Marker "_local_1" TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - , TermVar - ( NamedVar "y" ) - ] - ] - , taskConjectureLabel = Marker "alsotrivial" - , taskLocation = Location - { locFile = "test/examples/calc.tex" - , locLine = 20 - , locColumn = 1 - } - , taskConjecture = TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 10 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - , TermVar - ( NamedVar "y" ) - ] - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "alsotrivial" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 10 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - , Hypothesis Marker "irrelevant" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 6 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - , Hypothesis Marker "trivial" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 2 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ] - , taskConjectureLabel = Marker "trivial_biconditionals" - , taskLocation = Location - { locFile = "test/examples/calc.tex" - , locLine = 26 - , locColumn = 5 - } - , taskConjecture = TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 27 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - , TermVar - ( NamedVar "y" ) - ] - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "trivial" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 2 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ] - , taskConjectureLabel = Marker "trivial_biconditionals" - , taskLocation = Location - { locFile = "test/examples/calc.tex" - , locLine = 26 - , locColumn = 5 - } - , taskConjecture = TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 30 - , locColumn = 21 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - , TermVar - ( NamedVar "y" ) - ] - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "alsotrivial" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 10 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - , Hypothesis Marker "irrelevant" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 6 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - , Hypothesis Marker "trivial" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 2 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - , Hypothesis Marker "_local_1" Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 27 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - , TermVar - ( NamedVar "y" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 30 - , locColumn = 21 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - , TermVar - ( NamedVar "y" ) - ] - ) - ] - , taskConjectureLabel = Marker "trivial_biconditionals" - , taskLocation = Location - { locFile = "test/examples/calc.tex" - , locLine = 33 - , locColumn = 1 - } - , taskConjecture = TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 23 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - , TermVar - ( NamedVar "y" ) - ] - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "trivial_biconditionals" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 23 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - , Hypothesis Marker "alsotrivial" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 10 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - , Hypothesis Marker "irrelevant" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 6 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - , Hypothesis Marker "trivial" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 2 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ] - , taskConjectureLabel = Marker "bounded_calc" - , taskLocation = Location - { locFile = "test/examples/calc.tex" - , locLine = 39 - , locColumn = 5 - } - , taskConjecture = Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 39 - , locColumn = 16 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "A" ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ) - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "trivial_biconditionals" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 23 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - , Hypothesis Marker "alsotrivial" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 10 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - , Hypothesis Marker "irrelevant" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 6 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - , Hypothesis Marker "trivial" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 2 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - , Hypothesis Marker "_local_1" Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 39 - , locColumn = 16 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "A" ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ) - ] - , taskConjectureLabel = Marker "bounded_calc" - , taskLocation = Location - { locFile = "test/examples/calc.tex" - , locLine = 44 - , locColumn = 1 - } - , taskConjecture = Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 36 - , locColumn = 16 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "A" ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 36 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ) - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "bounded_calc" Quantified Universally - ( Scope - ( Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 36 - , locColumn = 16 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "A" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 36 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ) - ) - ) - , Hypothesis Marker "trivial_biconditionals" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 23 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - , Hypothesis Marker "alsotrivial" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 10 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - , Hypothesis Marker "irrelevant" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 6 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - , Hypothesis Marker "trivial" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 2 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ] - , taskConjectureLabel = Marker "bounded_calc_such_that" - , taskLocation = Location - { locFile = "test/examples/calc.tex" - , locLine = 50 - , locColumn = 5 - } - , taskConjecture = Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 50 - , locColumn = 16 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "A" ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 50 - , locColumn = 36 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ) - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "bounded_calc" Quantified Universally - ( Scope - ( Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 36 - , locColumn = 16 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "A" ) - ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 36 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ) - ) - ) - , Hypothesis Marker "trivial_biconditionals" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 23 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - , Hypothesis Marker "alsotrivial" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 10 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - , Hypothesis Marker "irrelevant" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 6 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "z" ) - ) - , TermVar - ( B - ( NamedVar "z" ) - ) - ] - ) - ) - , Hypothesis Marker "trivial" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 2 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - , Hypothesis Marker "_local_1" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 50 - , locColumn = 16 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "A" ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 50 - , locColumn = 36 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ) - ] - , taskConjectureLabel = Marker "bounded_calc_such_that" - , taskLocation = Location - { locFile = "test/examples/calc.tex" - , locLine = 55 - , locColumn = 1 - } - , taskConjecture = Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 47 - , locColumn = 16 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "A" ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 47 - , locColumn = 36 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 47 - , locColumn = 52 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ) - } -]
\ No newline at end of file diff --git a/test/golden/calc/glossing.golden b/test/golden/calc/glossing.golden deleted file mode 100644 index ccf40c4..0000000 --- a/test/golden/calc/glossing.golden +++ /dev/null @@ -1,574 +0,0 @@ -[ BlockLemma - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 1 - , locColumn = 1 - } - ) - ( Marker "trivial" ) - ( Lemma [] - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 2 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "x" ) - ] - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 5 - , locColumn = 1 - } - ) - ( Marker "irrelevant" ) - ( Lemma [] - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 6 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "z" ) - , TermVar - ( NamedVar "z" ) - ] - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 9 - , locColumn = 1 - } - ) - ( Marker "alsotrivial" ) - ( Lemma [] - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 10 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - , TermVar - ( NamedVar "y" ) - ] - ) - ) -, BlockProof - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 12 - , locColumn = 1 - } - ) - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 20 - , locColumn = 1 - } - ) - ( Calc - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 13 - , locColumn = 5 - } - ) CalcUnquantified - ( Equation - ( TermVar - ( NamedVar "y" ) - ) - ( - ( TermVar - ( NamedVar "y" ) - , JustificationEmpty - ) :| - [ - ( TermVar - ( NamedVar "y" ) - , JustificationRef - ( Marker "trivial" :| [] ) - ) - ] - ) - ) - ( Qed - { mloc = Nothing - , by = JustificationEmpty - } - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 22 - , locColumn = 1 - } - ) - ( Marker "trivial_biconditionals" ) - ( Lemma [] - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 23 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - , TermVar - ( NamedVar "y" ) - ] - ) - ) -, BlockProof - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 25 - , locColumn = 1 - } - ) - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 33 - , locColumn = 1 - } - ) - ( Calc - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 26 - , locColumn = 5 - } - ) CalcUnquantified - ( Biconditionals - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 27 - , locColumn = 11 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - , TermVar - ( NamedVar "y" ) - ] - ) - ( - ( PropositionalConstant IsTop - , JustificationEmpty - ) :| - [ - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 30 - , locColumn = 21 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - , TermVar - ( NamedVar "y" ) - ] - , JustificationRef - ( Marker "trivial" :| [] ) - ) - ] - ) - ) - ( Qed - { mloc = Nothing - , by = JustificationEmpty - } - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 35 - , locColumn = 1 - } - ) - ( Marker "bounded_calc" ) - ( Lemma [] - ( Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 36 - , locColumn = 16 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "A" ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 36 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ) - ) - ) -, BlockProof - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 38 - , locColumn = 1 - } - ) - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 44 - , locColumn = 1 - } - ) - ( Calc - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 39 - , locColumn = 5 - } - ) - ( CalcForall - ( NamedVar "x" :| [] ) - ( Just - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 39 - , locColumn = 16 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "A" ) - ] - ) - ) - ) - ( Equation - ( TermVar - ( NamedVar "x" ) - ) - ( - ( TermVar - ( NamedVar "x" ) - , JustificationEmpty - ) :| [] - ) - ) - ( Qed - { mloc = Nothing - , by = JustificationEmpty - } - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 46 - , locColumn = 1 - } - ) - ( Marker "bounded_calc_such_that" ) - ( Lemma [] - ( Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 47 - , locColumn = 16 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "A" ) - ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 47 - , locColumn = 36 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 47 - , locColumn = 52 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ) - ) - ) -, BlockProof - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 49 - , locColumn = 1 - } - ) - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 55 - , locColumn = 1 - } - ) - ( Calc - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 50 - , locColumn = 5 - } - ) - ( CalcForall - ( NamedVar "x" :| [] ) - ( Just - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 50 - , locColumn = 16 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "A" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/calc.tex" - , locLine = 50 - , locColumn = 36 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "x" ) - ] - ) - ) - ) - ) - ( Equation - ( TermVar - ( NamedVar "x" ) - ) - ( - ( TermVar - ( NamedVar "x" ) - , JustificationEmpty - ) :| [] - ) - ) - ( Qed - { mloc = Nothing - , by = JustificationEmpty - } - ) - ) -]
\ No newline at end of file diff --git a/test/golden/calc/verification.golden b/test/golden/calc/verification.golden deleted file mode 100644 index 5e297bb..0000000 --- a/test/golden/calc/verification.golden +++ /dev/null @@ -1,11 +0,0 @@ -VerifiedWithTrustedVampire - ( VerificationReport - { verificationRoute = LegacyVerificationRoute - , verificationLegacyDeclaredAssumptionCount = 0 - , verificationTypedDeclaredAssumptionCount = 0 - , verificationTrustedVampireCount = 12 - , verificationExplicitGapLocations = [] - , verificationTrustedLegacyRuleCount = 4 - , verificationKernelProofCount = 0 - } - )
\ No newline at end of file |