summaryrefslogtreecommitdiff
path: root/test/golden/byRef/generating tasks.golden
diff options
context:
space:
mode:
Diffstat (limited to 'test/golden/byRef/generating tasks.golden')
-rw-r--r--test/golden/byRef/generating tasks.golden352
1 files changed, 352 insertions, 0 deletions
diff --git a/test/golden/byRef/generating tasks.golden b/test/golden/byRef/generating tasks.golden
new file mode 100644
index 0000000..3187198
--- /dev/null
+++ b/test/golden/byRef/generating tasks.golden
@@ -0,0 +1,352 @@
+[ Task
+ { taskDirectness = Direct
+ , taskHypotheses = []
+ , taskConjectureLabel = Marker "first_proposition"
+ , taskConjecture = TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( NamedVar "a" )
+ , TermVar
+ ( NamedVar "a" )
+ ]
+ }
+, Task
+ { taskDirectness = Direct
+ , taskHypotheses =
+ [
+ ( Marker "first_proposition"
+ , Quantified Universally
+ ( Scope
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "a" )
+ )
+ , TermVar
+ ( B
+ ( NamedVar "a" )
+ )
+ ]
+ )
+ )
+ )
+ ]
+ , taskConjectureLabel = Marker "second_proposition"
+ , taskConjecture = TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( NamedVar "b" )
+ , TermVar
+ ( NamedVar "b" )
+ ]
+ }
+, Task
+ { taskDirectness = Direct
+ , taskHypotheses =
+ [
+ ( Marker "first_proposition"
+ , Quantified Universally
+ ( Scope
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "a" )
+ )
+ , TermVar
+ ( B
+ ( NamedVar "a" )
+ )
+ ]
+ )
+ )
+ )
+ ]
+ , taskConjectureLabel = Marker "third_proposition"
+ , taskConjecture = TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( NamedVar "c" )
+ , TermVar
+ ( NamedVar "c" )
+ ]
+ }
+, Task
+ { taskDirectness = Direct
+ , taskHypotheses =
+ [
+ ( Marker "first_proposition"
+ , Quantified Universally
+ ( Scope
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "a" )
+ )
+ , TermVar
+ ( B
+ ( NamedVar "a" )
+ )
+ ]
+ )
+ )
+ )
+ ]
+ , taskConjectureLabel = Marker "fourth_proposition"
+ , taskConjecture = Quantified Universally
+ ( Scope
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "d" )
+ )
+ , TermVar
+ ( B
+ ( NamedVar "d" )
+ )
+ ]
+ )
+ )
+ }
+, Task
+ { taskDirectness = Direct
+ , taskHypotheses =
+ [
+ ( Marker "third_proposition"
+ , Quantified Universally
+ ( Scope
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "c" )
+ )
+ , TermVar
+ ( B
+ ( NamedVar "c" )
+ )
+ ]
+ )
+ )
+ )
+ ,
+ ( Marker "second_proposition"
+ , Quantified Universally
+ ( Scope
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "b" )
+ )
+ , TermVar
+ ( B
+ ( NamedVar "b" )
+ )
+ ]
+ )
+ )
+ )
+ ,
+ ( Marker "first_proposition"
+ , Quantified Universally
+ ( Scope
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "a" )
+ )
+ , TermVar
+ ( B
+ ( NamedVar "a" )
+ )
+ ]
+ )
+ )
+ )
+ ,
+ ( Marker "fourth_proposition1"
+ , Quantified Universally
+ ( Scope
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "d" )
+ )
+ , TermVar
+ ( B
+ ( NamedVar "d" )
+ )
+ ]
+ )
+ )
+ )
+ ]
+ , taskConjectureLabel = Marker "fourth_proposition"
+ , taskConjecture = TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( NamedVar "e" )
+ , TermVar
+ ( NamedVar "e" )
+ ]
+ }
+, Task
+ { taskDirectness = Direct
+ , taskHypotheses =
+ [
+ ( Marker "fourth_proposition"
+ , Quantified Universally
+ ( Scope
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "e" )
+ )
+ , TermVar
+ ( B
+ ( NamedVar "e" )
+ )
+ ]
+ )
+ )
+ )
+ ,
+ ( Marker "third_proposition"
+ , Quantified Universally
+ ( Scope
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "c" )
+ )
+ , TermVar
+ ( B
+ ( NamedVar "c" )
+ )
+ ]
+ )
+ )
+ )
+ ,
+ ( Marker "second_proposition"
+ , Quantified Universally
+ ( Scope
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "b" )
+ )
+ , TermVar
+ ( B
+ ( NamedVar "b" )
+ )
+ ]
+ )
+ )
+ )
+ ,
+ ( Marker "first_proposition"
+ , Quantified Universally
+ ( Scope
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "a" )
+ )
+ , TermVar
+ ( B
+ ( NamedVar "a" )
+ )
+ ]
+ )
+ )
+ )
+ ]
+ , taskConjectureLabel = Marker "fifth_proposition"
+ , taskConjecture = TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( NamedVar "f" )
+ , TermVar
+ ( NamedVar "f" )
+ ]
+ }
+] \ No newline at end of file