diff options
Diffstat (limited to 'test/golden/no-reflexive-set')
| -rw-r--r-- | test/golden/no-reflexive-set/encoding tasks.golden | 2 | ||||
| -rw-r--r-- | test/golden/no-reflexive-set/generating tasks.golden | 110 | ||||
| -rw-r--r-- | test/golden/no-reflexive-set/glossing.golden | 83 | ||||
| -rw-r--r-- | test/golden/no-reflexive-set/verification.golden | 11 |
4 files changed, 0 insertions, 206 deletions
diff --git a/test/golden/no-reflexive-set/encoding tasks.golden b/test/golden/no-reflexive-set/encoding tasks.golden deleted file mode 100644 index 444124c..0000000 --- a/test/golden/no-reflexive-set/encoding tasks.golden +++ /dev/null @@ -1,2 +0,0 @@ -fof(zf_q0,conjecture,~zf_u0(zf_f0,zf_f0)). -fof(zf_h0,axiom,![V0]:(zf_u0(V0,zf_f0)=>~zf_u0(V0,V0))).
\ No newline at end of file diff --git a/test/golden/no-reflexive-set/generating tasks.golden b/test/golden/no-reflexive-set/generating tasks.golden deleted file mode 100644 index fa8d25d..0000000 --- a/test/golden/no-reflexive-set/generating tasks.golden +++ /dev/null @@ -1,110 +0,0 @@ -[ Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "_local_1" 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 "IndAntecedent" ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "A" ) - ) - ) - ] - ) - ( Connected Implication ( PropositionalConstant IsTop ) - ( Not - ( Location - { locFile = "test/examples/no-reflexive-set.tex" - , locLine = 2 - , locColumn = 36 - } - ) - ( TermSymbol - ( Location - { locFile = "test/examples/no-reflexive-set.tex" - , locLine = 2 - , locColumn = 36 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "IndAntecedent" ) - ) - , TermVar - ( B - ( NamedVar "IndAntecedent" ) - ) - ] - ) - ) - ) - ) - ) - ] - , taskConjectureLabel = Marker "in_irrefl" - , taskLocation = Location - { locFile = "test/examples/no-reflexive-set.tex" - , locLine = 10 - , locColumn = 5 - } - , taskConjecture = Not - ( Location - { locFile = "test/examples/no-reflexive-set.tex" - , locLine = 2 - , locColumn = 36 - } - ) - ( TermSymbol - ( Location - { locFile = "test/examples/no-reflexive-set.tex" - , locLine = 2 - , locColumn = 36 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "A" ) - , TermVar - ( NamedVar "A" ) - ] - ) - } -]
\ No newline at end of file diff --git a/test/golden/no-reflexive-set/glossing.golden b/test/golden/no-reflexive-set/glossing.golden deleted file mode 100644 index 9de8fd4..0000000 --- a/test/golden/no-reflexive-set/glossing.golden +++ /dev/null @@ -1,83 +0,0 @@ -[ BlockLemma - ( Location - { locFile = "test/examples/no-reflexive-set.tex" - , locLine = 1 - , locColumn = 1 - } - ) - ( Marker "in_irrefl" ) - ( Lemma [] - ( Quantified Universally - ( Scope - ( Connected Implication ( PropositionalConstant IsTop ) - ( Not - ( Location - { locFile = "test/examples/no-reflexive-set.tex" - , locLine = 2 - , locColumn = 36 - } - ) - ( TermSymbol - ( Location - { locFile = "test/examples/no-reflexive-set.tex" - , locLine = 2 - , locColumn = 36 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "A" ) - ) - , TermVar - ( B - ( NamedVar "A" ) - ) - ] - ) - ) - ) - ) - ) - ) -, BlockProof - ( Location - { locFile = "test/examples/no-reflexive-set.tex" - , locLine = 4 - , locColumn = 1 - } - ) - ( Location - { locFile = "test/examples/no-reflexive-set.tex" - , locLine = 11 - , locColumn = 1 - } - ) - ( BySetInduction - ( Location - { locFile = "test/examples/no-reflexive-set.tex" - , locLine = 4 - , locColumn = 21 - } - ) Nothing - ( Qed - { mloc = Just - ( Location - { locFile = "test/examples/no-reflexive-set.tex" - , locLine = 10 - , locColumn = 5 - } - ) - , by = JustificationEmpty - } - ) - ) -]
\ No newline at end of file diff --git a/test/golden/no-reflexive-set/verification.golden b/test/golden/no-reflexive-set/verification.golden deleted file mode 100644 index c72009c..0000000 --- a/test/golden/no-reflexive-set/verification.golden +++ /dev/null @@ -1,11 +0,0 @@ -VerifiedWithTrustedVampire - ( VerificationReport - { verificationRoute = LegacyVerificationRoute - , verificationLegacyDeclaredAssumptionCount = 0 - , verificationTypedDeclaredAssumptionCount = 0 - , verificationTrustedVampireCount = 1 - , verificationExplicitGapLocations = [] - , verificationTrustedLegacyRuleCount = 1 - , verificationKernelProofCount = 0 - } - )
\ No newline at end of file |