summaryrefslogtreecommitdiff
path: root/test/golden/separation/generating tasks.golden
diff options
context:
space:
mode:
Diffstat (limited to 'test/golden/separation/generating tasks.golden')
-rw-r--r--test/golden/separation/generating tasks.golden65
1 files changed, 65 insertions, 0 deletions
diff --git a/test/golden/separation/generating tasks.golden b/test/golden/separation/generating tasks.golden
new file mode 100644
index 0000000..889906b
--- /dev/null
+++ b/test/golden/separation/generating tasks.golden
@@ -0,0 +1,65 @@
+[ Task
+ { taskDirectness = Direct
+ , taskHypotheses = []
+ , taskConjectureLabel = Marker "sep_test"
+ , taskConjecture = Quantified Universally
+ ( Scope
+ ( Connected Equivalence
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Command "in" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "x" )
+ )
+ , TermVar
+ ( F
+ ( TermVar
+ ( NamedVar "X" )
+ )
+ )
+ ]
+ )
+ ( Connected Conjunction
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Command "in" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "x" )
+ )
+ , TermVar
+ ( F
+ ( TermVar
+ ( NamedVar "X" )
+ )
+ )
+ ]
+ )
+ ( TermSymbol
+ ( SymbolPredicate
+ ( PredicateRelation
+ ( Symbol "=" )
+ )
+ )
+ [ TermVar
+ ( B
+ ( NamedVar "x" )
+ )
+ , TermVar
+ ( B
+ ( NamedVar "x" )
+ )
+ ]
+ )
+ )
+ )
+ )
+ }
+] \ No newline at end of file