diff options
| author | adelon <22380201+adelon@users.noreply.github.com> | 2026-08-03 21:00:28 +0200 |
|---|---|---|
| committer | adelon <22380201+adelon@users.noreply.github.com> | 2026-08-03 21:00:28 +0200 |
| commit | 5cdde1fd0f976863ae4b5831ab389048138b06a4 (patch) | |
| tree | f6c58aa3d08a62429188d2de9ece98c49c022b2a /test/golden/proofassume/generating tasks.golden | |
| parent | d4667c50132fc5c55383ee3b8907705738608bff (diff) | |
Remove obsolete verification machinery
Diffstat (limited to 'test/golden/proofassume/generating tasks.golden')
| -rw-r--r-- | test/golden/proofassume/generating tasks.golden | 411 |
1 files changed, 0 insertions, 411 deletions
diff --git a/test/golden/proofassume/generating tasks.golden b/test/golden/proofassume/generating tasks.golden deleted file mode 100644 index 6f12c09..0000000 --- a/test/golden/proofassume/generating tasks.golden +++ /dev/null @@ -1,411 +0,0 @@ -[ Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "_local_1" TermSymbol - ( Location - { locFile = "test/examples/proofassume.tex" - , locLine = 5 - , locColumn = 14 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - ] - , taskConjectureLabel = Marker "assumetest" - , taskLocation = Location - { locFile = "test/examples/proofassume.tex" - , locLine = 6 - , locColumn = 5 - } - , taskConjecture = TermSymbol - ( Location - { locFile = "test/examples/proofassume.tex" - , locLine = 6 - , locColumn = 12 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "_local_2" TermSymbol - ( Location - { locFile = "test/examples/proofassume.tex" - , locLine = 6 - , locColumn = 12 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - , Hypothesis Marker "_local_1" TermSymbol - ( Location - { locFile = "test/examples/proofassume.tex" - , locLine = 5 - , locColumn = 14 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - ] - , taskConjectureLabel = Marker "assumetest" - , taskLocation = Location - { locFile = "test/examples/proofassume.tex" - , locLine = 7 - , locColumn = 1 - } - , taskConjecture = TermSymbol - ( Location - { locFile = "test/examples/proofassume.tex" - , locLine = 2 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "assumetest" Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/proofassume.tex" - , locLine = 2 - , locColumn = 10 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/proofassume.tex" - , locLine = 2 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "_local_2" TermSymbol - ( Location - { locFile = "test/examples/proofassume.tex" - , locLine = 14 - , locColumn = 14 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - , Hypothesis Marker "_local_1" TermSymbol - ( Location - { locFile = "test/examples/proofassume.tex" - , locLine = 13 - , locColumn = 14 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "b" ) - ] - ] - , taskConjectureLabel = Marker "assumetesttwo" - , taskLocation = Location - { locFile = "test/examples/proofassume.tex" - , locLine = 15 - , locColumn = 5 - } - , taskConjecture = TermSymbol - ( Location - { locFile = "test/examples/proofassume.tex" - , locLine = 15 - , locColumn = 12 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "assumetest" Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/proofassume.tex" - , locLine = 2 - , locColumn = 10 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/proofassume.tex" - , locLine = 2 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "_local_3" TermSymbol - ( Location - { locFile = "test/examples/proofassume.tex" - , locLine = 15 - , locColumn = 12 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - , Hypothesis Marker "_local_2" TermSymbol - ( Location - { locFile = "test/examples/proofassume.tex" - , locLine = 14 - , locColumn = 14 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - , Hypothesis Marker "_local_1" TermSymbol - ( Location - { locFile = "test/examples/proofassume.tex" - , locLine = 13 - , locColumn = 14 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "b" ) - ] - ] - , taskConjectureLabel = Marker "assumetesttwo" - , taskLocation = Location - { locFile = "test/examples/proofassume.tex" - , locLine = 16 - , locColumn = 1 - } - , taskConjecture = TermSymbol - ( Location - { locFile = "test/examples/proofassume.tex" - , locLine = 10 - , locColumn = 38 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - } -]
\ No newline at end of file |