summaryrefslogtreecommitdiff
path: root/test/golden/proofdefinefunction
diff options
context:
space:
mode:
Diffstat (limited to 'test/golden/proofdefinefunction')
-rw-r--r--test/golden/proofdefinefunction/encoding tasks.golden9
-rw-r--r--test/golden/proofdefinefunction/generating tasks.golden473
-rw-r--r--test/golden/proofdefinefunction/glossing.golden231
-rw-r--r--test/golden/proofdefinefunction/verification.golden11
4 files changed, 0 insertions, 724 deletions
diff --git a/test/golden/proofdefinefunction/encoding tasks.golden b/test/golden/proofdefinefunction/encoding tasks.golden
deleted file mode 100644
index 0569ea8..0000000
--- a/test/golden/proofdefinefunction/encoding tasks.golden
+++ /dev/null
@@ -1,9 +0,0 @@
-fof(zf_q0,conjecture,zf_u4(zf_f1,zf_f2)=>zf_u4(zf_f1,zf_f2)).
-fof(zf_h0,axiom,![V0,V1]:zf_u0(V0,V1)=V1).
-fof(zf_h1,axiom,![V2]:(zf_u2(V2)<=>V2=V2)).
-fof(zf_h2,axiom,![V3]:(zf_u3(V3)<=>V3=V3)).
-fof(zf_h3,axiom,![V4]:(zf_u4(V4,zf_f1)=>zf_u0(zf_f0,V4)=V4)).
-fof(zf_h4,axiom,![V5]:zf_u1(V5)=V5).
-fof(zf_h5,axiom,zf_u1(zf_f0)=zf_f1).
-fof(zf_h6,axiom,zf_u2(zf_f0)).
-fof(zf_h7,axiom,zf_u3(zf_f0)). \ No newline at end of file
diff --git a/test/golden/proofdefinefunction/generating tasks.golden b/test/golden/proofdefinefunction/generating tasks.golden
deleted file mode 100644
index 9573633..0000000
--- a/test/golden/proofdefinefunction/generating tasks.golden
+++ /dev/null
@@ -1,473 +0,0 @@
-[ Task
- { taskDirectness = Direct
- , taskHypotheses =
- [ Hypothesis Marker "relation" Quantified Universally
- ( Scope
- ( Connected Equivalence
- ( TermSymbol
- ( Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 18
- , locColumn = 1
- }
- )
- ( SymbolPredicate
- ( PredicateNoun
- ( LexicalItemSgPl
- ( SgPl
- { sg = TokenCons
- ( Word "relation" ) End
- , pl = TokenCons
- ( Word "relations" ) End
- }
- )
- ( Marker "relation" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "f" )
- )
- ]
- )
- ( Quantified Universally
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 19
- , locColumn = 29
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( F
- ( TermVar
- ( B
- ( NamedVar "f" )
- )
- )
- )
- , TermVar
- ( F
- ( TermVar
- ( B
- ( NamedVar "f" )
- )
- )
- )
- ]
- )
- )
- )
- )
- )
- , Hypothesis Marker "rightunique" Quantified Universally
- ( Scope
- ( Connected Equivalence
- ( TermSymbol
- ( Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 13
- , locColumn = 1
- }
- )
- ( SymbolPredicate
- ( PredicateAdj
- ( LexicalItem
- ( TokenCons
- ( Word "right-unique" ) End
- )
- ( Marker "rightunique" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "f" )
- )
- ]
- )
- ( Quantified Universally
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 14
- , locColumn = 31
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( F
- ( TermVar
- ( B
- ( NamedVar "f" )
- )
- )
- )
- , TermVar
- ( F
- ( TermVar
- ( B
- ( NamedVar "f" )
- )
- )
- )
- ]
- )
- )
- )
- )
- )
- , Hypothesis Marker "dom" Quantified Universally
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "<nowhere>"
- , locLine = -1
- , locColumn = -1
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermSymbol
- ( Location
- { locFile = "<nowhere>"
- , locLine = -1
- , locColumn = -1
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( TokenCons
- ( Command "dom" )
- ( TokenCons InvisibleBraceL
- ( HoleCons ( TokenCons InvisibleBraceR End ) )
- )
- )
- ( Marker "dom" ) NonAssoc
- )
- )
- [ TermVar
- ( B
- ( NamedVar "f" )
- )
- ]
- , TermVar
- ( B
- ( NamedVar "f" )
- )
- ]
- )
- )
- , Hypothesis Marker "apply" Quantified Universally
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "<nowhere>"
- , locLine = -1
- , locColumn = -1
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermSymbol
- ( Location
- { locFile = "<nowhere>"
- , locLine = -1
- , locColumn = -1
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( TokenCons
- ( Command "apply" )
- ( TokenCons InvisibleBraceL
- ( HoleCons
- ( TokenCons InvisibleBraceR
- ( TokenCons InvisibleBraceL
- ( HoleCons ( TokenCons InvisibleBraceR End ) )
- )
- )
- )
- )
- )
- ( Marker "apply" ) NonAssoc
- )
- )
- [ TermVar
- ( B
- ( NamedVar "f" )
- )
- , TermVar
- ( B
- ( NamedVar "x" )
- )
- ]
- , TermVar
- ( B
- ( NamedVar "x" )
- )
- ]
- )
- )
- , Hypothesis Marker "_local_4" TermSymbol
- ( Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 26
- , locColumn = 5
- }
- )
- ( SymbolPredicate
- ( PredicateNoun
- ( LexicalItemSgPl
- ( SgPl
- { sg = TokenCons
- ( Word "relation" ) End
- , pl = TokenCons
- ( Word "relations" ) End
- }
- )
- ( Marker "relation" )
- )
- )
- )
- [ TermVar
- ( NamedVar "f" )
- ]
- , Hypothesis Marker "_local_3" TermSymbol
- ( Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 26
- , locColumn = 5
- }
- )
- ( SymbolPredicate
- ( PredicateAdj
- ( LexicalItem
- ( TokenCons
- ( Word "right-unique" ) End
- )
- ( Marker "rightunique" )
- )
- )
- )
- [ TermVar
- ( NamedVar "f" )
- ]
- , Hypothesis Marker "_local_2" 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 "z" )
- )
- , TermVar
- ( F
- ( TermVar
- ( NamedVar "x" )
- )
- )
- ]
- )
- ( TermSymbol
- ( Location
- { locFile = "<nowhere>"
- , locLine = -1
- , locColumn = -1
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermSymbol
- ( Location
- { locFile = "<nowhere>"
- , locLine = -1
- , locColumn = -1
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( TokenCons
- ( Command "apply" )
- ( TokenCons InvisibleBraceL
- ( HoleCons
- ( TokenCons InvisibleBraceR
- ( TokenCons InvisibleBraceL
- ( HoleCons ( TokenCons InvisibleBraceR End ) )
- )
- )
- )
- )
- )
- ( Marker "apply" ) NonAssoc
- )
- )
- [ TermVar
- ( F
- ( TermVar
- ( NamedVar "f" )
- )
- )
- , TermVar
- ( B
- ( NamedVar "z" )
- )
- ]
- , TermVar
- ( B
- ( NamedVar "z" )
- )
- ]
- )
- )
- )
- , Hypothesis Marker "_local_1" TermSymbol
- ( Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 26
- , locColumn = 5
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermSymbol
- ( Location
- { locFile = "<nowhere>"
- , locLine = -1
- , locColumn = -1
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( TokenCons
- ( Command "dom" )
- ( TokenCons InvisibleBraceL
- ( HoleCons ( TokenCons InvisibleBraceR End ) )
- )
- )
- ( Marker "dom" ) NonAssoc
- )
- )
- [ TermVar
- ( NamedVar "f" )
- ]
- , TermVar
- ( NamedVar "x" )
- ]
- ]
- , taskConjectureLabel = Marker "definefunctiontest"
- , taskLocation = Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 27
- , locColumn = 1
- }
- , taskConjecture = Connected Implication
- ( TermSymbol
- ( Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 23
- , locColumn = 10
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Command "in" )
- ( ParameterArity 0 )
- ( Marker "elem" )
- )
- )
- )
- [ TermVar
- ( NamedVar "x" )
- , TermVar
- ( NamedVar "y" )
- ]
- )
- ( TermSymbol
- ( Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 23
- , locColumn = 25
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Command "in" )
- ( ParameterArity 0 )
- ( Marker "elem" )
- )
- )
- )
- [ TermVar
- ( NamedVar "x" )
- , TermVar
- ( NamedVar "y" )
- ]
- )
- }
-] \ No newline at end of file
diff --git a/test/golden/proofdefinefunction/glossing.golden b/test/golden/proofdefinefunction/glossing.golden
deleted file mode 100644
index a638a71..0000000
--- a/test/golden/proofdefinefunction/glossing.golden
+++ /dev/null
@@ -1,231 +0,0 @@
-[ BlockDefn
- ( Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 3
- , locColumn = 1
- }
- )
- ( Marker "apply" )
- ( DefnOp
- ( MixfixItem
- ( TokenCons
- ( Command "apply" )
- ( TokenCons InvisibleBraceL
- ( HoleCons
- ( TokenCons InvisibleBraceR
- ( TokenCons InvisibleBraceL
- ( HoleCons ( TokenCons InvisibleBraceR End ) )
- )
- )
- )
- )
- )
- ( Marker "apply" ) NonAssoc
- )
- [ NamedVar "f"
- , NamedVar "x"
- ]
- ( TermVar
- ( NamedVar "x" )
- )
- )
-, BlockDefn
- ( Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 8
- , locColumn = 1
- }
- )
- ( Marker "dom" )
- ( DefnOp
- ( MixfixItem
- ( TokenCons
- ( Command "dom" )
- ( TokenCons InvisibleBraceL
- ( HoleCons ( TokenCons InvisibleBraceR End ) )
- )
- )
- ( Marker "dom" ) NonAssoc
- )
- [ NamedVar "f" ]
- ( TermVar
- ( NamedVar "f" )
- )
- )
-, BlockDefn
- ( Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 13
- , locColumn = 1
- }
- )
- ( Marker "rightunique" )
- ( DefnPredicate []
- ( PredicateAdj
- ( LexicalItem
- ( TokenCons
- ( Word "right-unique" ) End
- )
- ( Marker "rightunique" )
- )
- )
- ( NamedVar "f" :| [] )
- ( TermSymbol
- ( Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 14
- , locColumn = 31
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( NamedVar "f" )
- , TermVar
- ( NamedVar "f" )
- ]
- )
- )
-, BlockDefn
- ( Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 18
- , locColumn = 1
- }
- )
- ( Marker "relation" )
- ( DefnPredicate []
- ( PredicateNoun
- ( LexicalItemSgPl
- ( SgPl
- { sg = TokenCons
- ( Word "relation" ) End
- , pl = TokenCons
- ( Word "relations" ) End
- }
- )
- ( Marker "relation" )
- )
- )
- ( NamedVar "f" :| [] )
- ( TermSymbol
- ( Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 19
- , locColumn = 29
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( NamedVar "f" )
- , TermVar
- ( NamedVar "f" )
- ]
- )
- )
-, BlockLemma
- ( Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 22
- , locColumn = 1
- }
- )
- ( Marker "definefunctiontest" )
- ( Lemma []
- ( Connected Implication
- ( TermSymbol
- ( Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 23
- , locColumn = 10
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Command "in" )
- ( ParameterArity 0 )
- ( Marker "elem" )
- )
- )
- )
- [ TermVar
- ( NamedVar "x" )
- , TermVar
- ( NamedVar "y" )
- ]
- )
- ( TermSymbol
- ( Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 23
- , locColumn = 25
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Command "in" )
- ( ParameterArity 0 )
- ( Marker "elem" )
- )
- )
- )
- [ TermVar
- ( NamedVar "x" )
- , TermVar
- ( NamedVar "y" )
- ]
- )
- )
- )
-, BlockProof
- ( Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 25
- , locColumn = 1
- }
- )
- ( Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 27
- , locColumn = 1
- }
- )
- ( DefineFunction
- ( Location
- { locFile = "test/examples/proofdefinefunction.tex"
- , locLine = 26
- , locColumn = 5
- }
- )
- ( NamedVar "f" )
- ( NamedVar "z" )
- ( TermVar
- ( NamedVar "z" )
- )
- ( TermVar
- ( NamedVar "x" )
- )
- ( Qed
- { mloc = Nothing
- , by = JustificationEmpty
- }
- )
- )
-] \ No newline at end of file
diff --git a/test/golden/proofdefinefunction/verification.golden b/test/golden/proofdefinefunction/verification.golden
deleted file mode 100644
index 92226be..0000000
--- a/test/golden/proofdefinefunction/verification.golden
+++ /dev/null
@@ -1,11 +0,0 @@
-VerifiedWithTrustedVampire
- ( VerificationReport
- { verificationRoute = LegacyVerificationRoute
- , verificationLegacyDeclaredAssumptionCount = 0
- , verificationTypedDeclaredAssumptionCount = 0
- , verificationTrustedVampireCount = 1
- , verificationExplicitGapLocations = []
- , verificationTrustedLegacyRuleCount = 5
- , verificationKernelProofCount = 0
- }
- ) \ No newline at end of file
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-04 07:35:13 +0000