diff options
Diffstat (limited to 'test/golden/relparam')
| -rw-r--r-- | test/golden/relparam/encoding tasks.golden | 4 | ||||
| -rw-r--r-- | test/golden/relparam/generating tasks.golden | 109 | ||||
| -rw-r--r-- | test/golden/relparam/glossing.golden | 185 | ||||
| -rw-r--r-- | test/golden/relparam/verification.golden | 11 |
4 files changed, 0 insertions, 309 deletions
diff --git a/test/golden/relparam/encoding tasks.golden b/test/golden/relparam/encoding tasks.golden deleted file mode 100644 index 593b681..0000000 --- a/test/golden/relparam/encoding tasks.golden +++ /dev/null @@ -1,4 +0,0 @@ -fof(zf_q0,conjecture,![V0]:V0=V0). ------------------- -fof(zf_q0,conjecture,![V0]:V0=V0). -fof(zf_h0,axiom,![V1]:V1=V1).
\ No newline at end of file diff --git a/test/golden/relparam/generating tasks.golden b/test/golden/relparam/generating tasks.golden deleted file mode 100644 index 46d7cb7..0000000 --- a/test/golden/relparam/generating tasks.golden +++ /dev/null @@ -1,109 +0,0 @@ -[ Task - { taskDirectness = Direct - , taskHypotheses = [] - , taskConjectureLabel = Marker "dummy_abbr_test" - , taskLocation = Location - { locFile = "test/examples/relparam.tex" - , locLine = 6 - , locColumn = 1 - } - , taskConjecture = Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/relparam.tex" - , locLine = 3 - , locColumn = 27 - } - ) - ( 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" Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/relparam.tex" - , locLine = 3 - , locColumn = 27 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ] - , taskConjectureLabel = Marker "dummy_defn_test" - , taskLocation = Location - { locFile = "test/examples/relparam.tex" - , locLine = 15 - , locColumn = 1 - } - , taskConjecture = Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/relparam.tex" - , locLine = 12 - , locColumn = 31 - } - ) - ( 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/relparam/glossing.golden b/test/golden/relparam/glossing.golden deleted file mode 100644 index 4f724d1..0000000 --- a/test/golden/relparam/glossing.golden +++ /dev/null @@ -1,185 +0,0 @@ -[ BlockAbbr - ( Location - { locFile = "test/examples/relparam.tex" - , locLine = 2 - , locColumn = 1 - } - ) - ( Marker "abbr_equal" ) - ( Abbreviation - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "EQUAL" ) - ( ParameterArity 1 ) - ( Marker "abbr_equal" ) - ) - ) - ) - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/relparam.tex" - , locLine = 3 - , locColumn = 27 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B 1 ) - , TermVar - ( B 2 ) - ] - ) - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/relparam.tex" - , locLine = 6 - , locColumn = 1 - } - ) - ( Marker "dummy_abbr_test" ) - ( Lemma [] - ( Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/relparam.tex" - , locLine = 7 - , locColumn = 27 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "EQUAL" ) - ( ParameterArity 1 ) - ( Marker "abbr_equal" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( NamedVar "y" ) - ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ) - ) -, BlockAbbr - ( Location - { locFile = "test/examples/relparam.tex" - , locLine = 11 - , locColumn = 1 - } - ) - ( Marker "defn_equals" ) - ( Abbreviation - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "EQUALS" ) - ( ParameterArity 2 ) - ( Marker "defn_equals" ) - ) - ) - ) - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/relparam.tex" - , locLine = 12 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B 2 ) - , TermVar - ( B 3 ) - ] - ) - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/relparam.tex" - , locLine = 15 - , locColumn = 1 - } - ) - ( Marker "dummy_defn_test" ) - ( Lemma [] - ( Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/relparam.tex" - , locLine = 16 - , locColumn = 27 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "EQUALS" ) - ( ParameterArity 2 ) - ( Marker "defn_equals" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( NamedVar "y" ) - ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "w" ) - ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ) - ) -]
\ No newline at end of file diff --git a/test/golden/relparam/verification.golden b/test/golden/relparam/verification.golden deleted file mode 100644 index 24830d8..0000000 --- a/test/golden/relparam/verification.golden +++ /dev/null @@ -1,11 +0,0 @@ -VerifiedWithTrustedVampire - ( VerificationReport - { verificationRoute = LegacyVerificationRoute - , verificationLegacyDeclaredAssumptionCount = 0 - , verificationTypedDeclaredAssumptionCount = 0 - , verificationTrustedVampireCount = 2 - , verificationExplicitGapLocations = [] - , verificationTrustedLegacyRuleCount = 0 - , verificationKernelProofCount = 0 - } - )
\ No newline at end of file |