summaryrefslogtreecommitdiff
path: root/test/golden/finite-set-terms
diff options
context:
space:
mode:
Diffstat (limited to 'test/golden/finite-set-terms')
-rw-r--r--test/golden/finite-set-terms/encoding tasks.golden3
-rw-r--r--test/golden/finite-set-terms/generating tasks.golden291
-rw-r--r--test/golden/finite-set-terms/glossing.golden238
-rw-r--r--test/golden/finite-set-terms/verification.golden11
4 files changed, 0 insertions, 543 deletions
diff --git a/test/golden/finite-set-terms/encoding tasks.golden b/test/golden/finite-set-terms/encoding tasks.golden
deleted file mode 100644
index 3a359a5..0000000
--- a/test/golden/finite-set-terms/encoding tasks.golden
+++ /dev/null
@@ -1,3 +0,0 @@
-fof(zf_q0,conjecture,zf_u3(zf_u1,zf_u2)).
-fof(zf_h0,axiom,![V0,V1,V2]:(zf_u3(V0,zf_u0(V1,V2))<=>(V0=V1|zf_u3(V0,V2)))).
-fof(zf_h1,axiom,![V3]:(zf_u3(V3,zf_u2)<=>(zf_u3(V3,zf_u1)|V3=zf_u1))). \ No newline at end of file
diff --git a/test/golden/finite-set-terms/generating tasks.golden b/test/golden/finite-set-terms/generating tasks.golden
deleted file mode 100644
index 1c396ab..0000000
--- a/test/golden/finite-set-terms/generating tasks.golden
+++ /dev/null
@@ -1,291 +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/finite-set-terms.tex"
- , locLine = 5
- , 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/finite-set-terms.tex"
- , locLine = 6
- , locColumn = 14
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( TokenCons
- ( Command "emptyset" ) End
- )
- ( Marker "emptyset" ) NonAssoc
- )
- ) []
- ]
- )
- ( TermSymbol
- ( Location
- { locFile = "test/examples/finite-set-terms.tex"
- , locLine = 5
- , locColumn = 1
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "any" )
- )
- , TermSymbol
- ( Location
- { locFile = "test/examples/finite-set-terms.tex"
- , locLine = 6
- , locColumn = 16
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( TokenCons
- ( Command "emptyset" ) End
- )
- ( Marker "emptyset" ) NonAssoc
- )
- ) []
- ]
- )
- )
- )
- )
- , Hypothesis Marker "cons" Quantified Universally
- ( Scope
- ( Connected Equivalence
- ( TermSymbol
- ( Location
- { locFile = "test/examples/finite-set-terms.tex"
- , locLine = 2
- , locColumn = 7
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Command "in" )
- ( ParameterArity 0 )
- ( Marker "elem" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "x" )
- )
- , TermSymbol
- ( Location
- { locFile = "test/examples/finite-set-terms.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/finite-set-terms.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/finite-set-terms.tex"
- , locLine = 2
- , locColumn = 41
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Command "in" )
- ( ParameterArity 0 )
- ( Marker "elem" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "x" )
- )
- , TermVar
- ( B
- ( NamedVar "X" )
- )
- ]
- )
- )
- )
- )
- ]
- , taskConjectureLabel = Marker "emptyset_in_unit"
- , taskLocation = Location
- { locFile = "test/examples/finite-set-terms.tex"
- , locLine = 9
- , locColumn = 1
- }
- , taskConjecture = TermSymbol
- ( Location
- { locFile = "test/examples/finite-set-terms.tex"
- , locLine = 10
- , locColumn = 15
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Command "in" )
- ( ParameterArity 0 )
- ( Marker "elem" )
- )
- )
- )
- [ TermSymbol
- ( Location
- { locFile = "test/examples/finite-set-terms.tex"
- , locLine = 10
- , locColumn = 6
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( TokenCons
- ( Command "emptyset" ) End
- )
- ( Marker "emptyset" ) NonAssoc
- )
- ) []
- , TermSymbol
- ( Location
- { locFile = "test/examples/finite-set-terms.tex"
- , locLine = 10
- , locColumn = 18
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( TokenCons
- ( Command "unit" ) End
- )
- ( Marker "unit" ) NonAssoc
- )
- ) []
- ]
- }
-] \ No newline at end of file
diff --git a/test/golden/finite-set-terms/glossing.golden b/test/golden/finite-set-terms/glossing.golden
deleted file mode 100644
index a531e00..0000000
--- a/test/golden/finite-set-terms/glossing.golden
+++ /dev/null
@@ -1,238 +0,0 @@
-[ BlockAxiom
- ( Location
- { locFile = "test/examples/finite-set-terms.tex"
- , locLine = 1
- , locColumn = 1
- }
- )
- ( Marker "cons" )
- ( Axiom []
- ( Connected Equivalence
- ( TermSymbol
- ( Location
- { locFile = "test/examples/finite-set-terms.tex"
- , locLine = 2
- , locColumn = 7
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Command "in" )
- ( ParameterArity 0 )
- ( Marker "elem" )
- )
- )
- )
- [ TermVar
- ( NamedVar "x" )
- , TermSymbol
- ( Location
- { locFile = "test/examples/finite-set-terms.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/finite-set-terms.tex"
- , locLine = 2
- , locColumn = 31
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( NamedVar "x" )
- , TermVar
- ( NamedVar "y" )
- ]
- )
- ( TermSymbol
- ( Location
- { locFile = "test/examples/finite-set-terms.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/finite-set-terms.tex"
- , locLine = 5
- , locColumn = 1
- }
- )
- ( Marker "unit" )
- ( DefnOp
- ( MixfixItem
- ( TokenCons
- ( Command "unit" ) End
- )
- ( Marker "unit" ) NonAssoc
- ) []
- ( TermSymbol
- ( Location
- { locFile = "test/examples/finite-set-terms.tex"
- , locLine = 6
- , 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/finite-set-terms.tex"
- , locLine = 6
- , locColumn = 16
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( TokenCons
- ( Command "emptyset" ) End
- )
- ( Marker "emptyset" ) NonAssoc
- )
- ) []
- , TermSymbol
- ( Location
- { locFile = "test/examples/finite-set-terms.tex"
- , locLine = 6
- , locColumn = 14
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( TokenCons
- ( Command "emptyset" ) End
- )
- ( Marker "emptyset" ) NonAssoc
- )
- ) []
- ]
- )
- )
-, BlockLemma
- ( Location
- { locFile = "test/examples/finite-set-terms.tex"
- , locLine = 9
- , locColumn = 1
- }
- )
- ( Marker "emptyset_in_unit" )
- ( Lemma []
- ( TermSymbol
- ( Location
- { locFile = "test/examples/finite-set-terms.tex"
- , locLine = 10
- , locColumn = 15
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Command "in" )
- ( ParameterArity 0 )
- ( Marker "elem" )
- )
- )
- )
- [ TermSymbol
- ( Location
- { locFile = "test/examples/finite-set-terms.tex"
- , locLine = 10
- , locColumn = 6
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( TokenCons
- ( Command "emptyset" ) End
- )
- ( Marker "emptyset" ) NonAssoc
- )
- ) []
- , TermSymbol
- ( Location
- { locFile = "test/examples/finite-set-terms.tex"
- , locLine = 10
- , locColumn = 18
- }
- )
- ( SymbolMixfix
- ( MixfixItem
- ( TokenCons
- ( Command "unit" ) End
- )
- ( Marker "unit" ) NonAssoc
- )
- ) []
- ]
- )
- )
-] \ No newline at end of file
diff --git a/test/golden/finite-set-terms/verification.golden b/test/golden/finite-set-terms/verification.golden
deleted file mode 100644
index 6411375..0000000
--- a/test/golden/finite-set-terms/verification.golden
+++ /dev/null
@@ -1,11 +0,0 @@
-VerifiedWithTrustedVampire
- ( VerificationReport
- { verificationRoute = LegacyVerificationRoute
- , verificationLegacyDeclaredAssumptionCount = 1
- , verificationTypedDeclaredAssumptionCount = 0
- , verificationTrustedVampireCount = 1
- , verificationExplicitGapLocations = []
- , verificationTrustedLegacyRuleCount = 1
- , verificationKernelProofCount = 0
- }
- ) \ No newline at end of file
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-05 09:09:07 +0000