diff options
| author | adelon <22380201+adelon@users.noreply.github.com> | 2024-02-10 02:22:14 +0100 |
|---|---|---|
| committer | adelon <22380201+adelon@users.noreply.github.com> | 2024-02-10 02:22:14 +0100 |
| commit | 442d732696ad431b84f6e5c72b6ee785be4fd968 (patch) | |
| tree | b476f395e7e91d67bacb6758bc84914b8711593f /test/golden/inductive | |
Initial commit
Diffstat (limited to 'test/golden/inductive')
| -rw-r--r-- | test/golden/inductive/encoding tasks.golden | 170 | ||||
| -rw-r--r-- | test/golden/inductive/generating tasks.golden | 8965 | ||||
| -rw-r--r-- | test/golden/inductive/glossing.golden | 1136 | ||||
| -rw-r--r-- | test/golden/inductive/parsing.golden | 1076 | ||||
| -rw-r--r-- | test/golden/inductive/scanning.golden | 92 | ||||
| -rw-r--r-- | test/golden/inductive/tokenizing.golden | 514 | ||||
| -rw-r--r-- | test/golden/inductive/verification.golden | 1 |
7 files changed, 11954 insertions, 0 deletions
diff --git a/test/golden/inductive/encoding tasks.golden b/test/golden/inductive/encoding tasks.golden new file mode 100644 index 0000000..2e9a2d5 --- /dev/null +++ b/test/golden/inductive/encoding tasks.golden @@ -0,0 +1,170 @@ +fof(fin,conjecture,elem(emptyset,pow(fA))). +fof(lmao,axiom,![Xx]:elem(Xx,emptyset)). +fof(preimg,axiom,![XR,XA]:preimg(XR,XA)=emptyset). +fof(fld,axiom,![XR]:fld(XR)=emptyset). +fof(times,axiom,![XA,XB]:times(XA,XB)=emptyset). +fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). +fof(pow,axiom,![XA]:pow(XA)=emptyset). +fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). +------------------ +fof(fin,conjecture,(elem(fa,fA)&elem(fB,pow(fA)))=>elem(cons(fa,fB),pow(fA))). +fof(lmao,axiom,![Xx]:elem(Xx,emptyset)). +fof(preimg,axiom,![XR,XA]:preimg(XR,XA)=emptyset). +fof(fld,axiom,![XR]:fld(XR)=emptyset). +fof(times,axiom,![XA,XB]:times(XA,XB)=emptyset). +fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). +fof(pow,axiom,![XA]:pow(XA)=emptyset). +fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). +------------------ +fof(fin_mono,conjecture,subseteq(fin(fA),fin(fB))). +fof(fin,axiom,![Xa,XA,XB]:((elem(Xa,XA)&elem(XB,fin(XA)))=>elem(cons(Xa,XB),fin(XA)))). +fof(fin,axiom,![XA]:elem(emptyset,fin(XA))). +fof(fin,axiom,![XA]:subseteq(fin(XA),pow(XA))). +fof(lmao,axiom,![Xx]:elem(Xx,emptyset)). +fof(preimg,axiom,![XR,XA]:preimg(XR,XA)=emptyset). +fof(fld,axiom,![XR]:fld(XR)=emptyset). +fof(times,axiom,![XA,XB]:times(XA,XB)=emptyset). +fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). +fof(pow,axiom,![XA]:pow(XA)=emptyset). +fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). +fof(fin_mono1,axiom,subseteq(fA,fB)). +------------------ +fof(tracl,conjecture,elem(fw,fR)=>elem(fw,times(fld(fR),fld(fR)))). +fof(fin_mono,axiom,![XA,XB]:(subseteq(XA,XB)=>subseteq(fin(XA),fin(XB)))). +fof(fin,axiom,![Xa,XA,XB]:((elem(Xa,XA)&elem(XB,fin(XA)))=>elem(cons(Xa,XB),fin(XA)))). +fof(fin,axiom,![XA]:elem(emptyset,fin(XA))). +fof(fin,axiom,![XA]:subseteq(fin(XA),pow(XA))). +fof(lmao,axiom,![Xx]:elem(Xx,emptyset)). +fof(preimg,axiom,![XR,XA]:preimg(XR,XA)=emptyset). +fof(fld,axiom,![XR]:fld(XR)=emptyset). +fof(times,axiom,![XA,XB]:times(XA,XB)=emptyset). +fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). +fof(pow,axiom,![XA]:pow(XA)=emptyset). +fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). +------------------ +fof(tracl,conjecture,(elem(pair(fa,fb),times(fld(fR),fld(fR)))&elem(pair(fb,fc),fR))=>elem(pair(fa,fc),times(fld(fR),fld(fR)))). +fof(fin_mono,axiom,![XA,XB]:(subseteq(XA,XB)=>subseteq(fin(XA),fin(XB)))). +fof(fin,axiom,![Xa,XA,XB]:((elem(Xa,XA)&elem(XB,fin(XA)))=>elem(cons(Xa,XB),fin(XA)))). +fof(fin,axiom,![XA]:elem(emptyset,fin(XA))). +fof(fin,axiom,![XA]:subseteq(fin(XA),pow(XA))). +fof(lmao,axiom,![Xx]:elem(Xx,emptyset)). +fof(preimg,axiom,![XR,XA]:preimg(XR,XA)=emptyset). +fof(fld,axiom,![XR]:fld(XR)=emptyset). +fof(times,axiom,![XA,XB]:times(XA,XB)=emptyset). +fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). +fof(pow,axiom,![XA]:pow(XA)=emptyset). +fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). +------------------ +fof(quasirefltracl,conjecture,elem(fa,fld(fR))=>elem(pair(fa,fa),times(fld(fR),fld(fR)))). +fof(tracl,axiom,![Xa,Xb,XR,Xc]:((elem(pair(Xa,Xb),tracl(XR))&elem(pair(Xb,Xc),XR))=>elem(pair(Xa,Xc),tracl(XR)))). +fof(tracl,axiom,![Xw,XR]:(elem(Xw,XR)=>elem(Xw,tracl(XR)))). +fof(tracl,axiom,![XR]:subseteq(tracl(XR),times(fld(XR),fld(XR)))). +fof(fin_mono,axiom,![XA,XB]:(subseteq(XA,XB)=>subseteq(fin(XA),fin(XB)))). +fof(fin,axiom,![Xa,XA,XB]:((elem(Xa,XA)&elem(XB,fin(XA)))=>elem(cons(Xa,XB),fin(XA)))). +fof(fin,axiom,![XA]:elem(emptyset,fin(XA))). +fof(fin,axiom,![XA]:subseteq(fin(XA),pow(XA))). +fof(lmao,axiom,![Xx]:elem(Xx,emptyset)). +fof(preimg,axiom,![XR,XA]:preimg(XR,XA)=emptyset). +fof(fld,axiom,![XR]:fld(XR)=emptyset). +fof(times,axiom,![XA,XB]:times(XA,XB)=emptyset). +fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). +fof(pow,axiom,![XA]:pow(XA)=emptyset). +fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). +------------------ +fof(quasirefltracl,conjecture,(elem(pair(fa,fb),times(fld(fR),fld(fR)))&elem(pair(fb,fc),fR))=>elem(pair(fa,fc),times(fld(fR),fld(fR)))). +fof(tracl,axiom,![Xa,Xb,XR,Xc]:((elem(pair(Xa,Xb),tracl(XR))&elem(pair(Xb,Xc),XR))=>elem(pair(Xa,Xc),tracl(XR)))). +fof(tracl,axiom,![Xw,XR]:(elem(Xw,XR)=>elem(Xw,tracl(XR)))). +fof(tracl,axiom,![XR]:subseteq(tracl(XR),times(fld(XR),fld(XR)))). +fof(fin_mono,axiom,![XA,XB]:(subseteq(XA,XB)=>subseteq(fin(XA),fin(XB)))). +fof(fin,axiom,![Xa,XA,XB]:((elem(Xa,XA)&elem(XB,fin(XA)))=>elem(cons(Xa,XB),fin(XA)))). +fof(fin,axiom,![XA]:elem(emptyset,fin(XA))). +fof(fin,axiom,![XA]:subseteq(fin(XA),pow(XA))). +fof(lmao,axiom,![Xx]:elem(Xx,emptyset)). +fof(preimg,axiom,![XR,XA]:preimg(XR,XA)=emptyset). +fof(fld,axiom,![XR]:fld(XR)=emptyset). +fof(times,axiom,![XA,XB]:times(XA,XB)=emptyset). +fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). +fof(pow,axiom,![XA]:pow(XA)=emptyset). +fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). +------------------ +fof(refltracl,conjecture,elem(fa,fA)=>elem(pair(fa,fa),times(fA,fA))). +fof(quasirefltracl,axiom,![Xa,Xb,XR,Xc]:((elem(pair(Xa,Xb),quasirefltracl(XR))&elem(pair(Xb,Xc),XR))=>elem(pair(Xa,Xc),quasirefltracl(XR)))). +fof(quasirefltracl,axiom,![Xa,XR]:(elem(Xa,fld(XR))=>elem(pair(Xa,Xa),quasirefltracl(XR)))). +fof(quasirefltracl,axiom,![XR]:subseteq(quasirefltracl(XR),times(fld(XR),fld(XR)))). +fof(tracl,axiom,![Xa,Xb,XR,Xc]:((elem(pair(Xa,Xb),tracl(XR))&elem(pair(Xb,Xc),XR))=>elem(pair(Xa,Xc),tracl(XR)))). +fof(tracl,axiom,![Xw,XR]:(elem(Xw,XR)=>elem(Xw,tracl(XR)))). +fof(tracl,axiom,![XR]:subseteq(tracl(XR),times(fld(XR),fld(XR)))). +fof(fin_mono,axiom,![XA,XB]:(subseteq(XA,XB)=>subseteq(fin(XA),fin(XB)))). +fof(fin,axiom,![Xa,XA,XB]:((elem(Xa,XA)&elem(XB,fin(XA)))=>elem(cons(Xa,XB),fin(XA)))). +fof(fin,axiom,![XA]:elem(emptyset,fin(XA))). +fof(fin,axiom,![XA]:subseteq(fin(XA),pow(XA))). +fof(lmao,axiom,![Xx]:elem(Xx,emptyset)). +fof(preimg,axiom,![XR,XA]:preimg(XR,XA)=emptyset). +fof(fld,axiom,![XR]:fld(XR)=emptyset). +fof(times,axiom,![XA,XB]:times(XA,XB)=emptyset). +fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). +fof(pow,axiom,![XA]:pow(XA)=emptyset). +fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). +------------------ +fof(refltracl,conjecture,(elem(pair(fa,fb),times(fA,fA))&elem(pair(fb,fc),fR))=>elem(pair(fa,fc),times(fA,fA))). +fof(quasirefltracl,axiom,![Xa,Xb,XR,Xc]:((elem(pair(Xa,Xb),quasirefltracl(XR))&elem(pair(Xb,Xc),XR))=>elem(pair(Xa,Xc),quasirefltracl(XR)))). +fof(quasirefltracl,axiom,![Xa,XR]:(elem(Xa,fld(XR))=>elem(pair(Xa,Xa),quasirefltracl(XR)))). +fof(quasirefltracl,axiom,![XR]:subseteq(quasirefltracl(XR),times(fld(XR),fld(XR)))). +fof(tracl,axiom,![Xa,Xb,XR,Xc]:((elem(pair(Xa,Xb),tracl(XR))&elem(pair(Xb,Xc),XR))=>elem(pair(Xa,Xc),tracl(XR)))). +fof(tracl,axiom,![Xw,XR]:(elem(Xw,XR)=>elem(Xw,tracl(XR)))). +fof(tracl,axiom,![XR]:subseteq(tracl(XR),times(fld(XR),fld(XR)))). +fof(fin_mono,axiom,![XA,XB]:(subseteq(XA,XB)=>subseteq(fin(XA),fin(XB)))). +fof(fin,axiom,![Xa,XA,XB]:((elem(Xa,XA)&elem(XB,fin(XA)))=>elem(cons(Xa,XB),fin(XA)))). +fof(fin,axiom,![XA]:elem(emptyset,fin(XA))). +fof(fin,axiom,![XA]:subseteq(fin(XA),pow(XA))). +fof(lmao,axiom,![Xx]:elem(Xx,emptyset)). +fof(preimg,axiom,![XR,XA]:preimg(XR,XA)=emptyset). +fof(fld,axiom,![XR]:fld(XR)=emptyset). +fof(times,axiom,![XA,XB]:times(XA,XB)=emptyset). +fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). +fof(pow,axiom,![XA]:pow(XA)=emptyset). +fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). +------------------ +fof(acc,conjecture,![Xxa,Xxb]:(subseteq(Xxa,Xxb)=>subseteq(pow(Xxa),pow(Xxb)))). +fof(refltracl,axiom,![Xa,Xb,XA,XR,Xc]:((elem(pair(Xa,Xb),refltracl(XA,XR))&elem(pair(Xb,Xc),XR))=>elem(pair(Xa,Xc),refltracl(XA,XR)))). +fof(refltracl,axiom,![Xa,XA,XR]:(elem(Xa,XA)=>elem(pair(Xa,Xa),refltracl(XA,XR)))). +fof(refltracl,axiom,![XA,XR]:subseteq(refltracl(XA,XR),times(XA,XA))). +fof(quasirefltracl,axiom,![Xa,Xb,XR,Xc]:((elem(pair(Xa,Xb),quasirefltracl(XR))&elem(pair(Xb,Xc),XR))=>elem(pair(Xa,Xc),quasirefltracl(XR)))). +fof(quasirefltracl,axiom,![Xa,XR]:(elem(Xa,fld(XR))=>elem(pair(Xa,Xa),quasirefltracl(XR)))). +fof(quasirefltracl,axiom,![XR]:subseteq(quasirefltracl(XR),times(fld(XR),fld(XR)))). +fof(tracl,axiom,![Xa,Xb,XR,Xc]:((elem(pair(Xa,Xb),tracl(XR))&elem(pair(Xb,Xc),XR))=>elem(pair(Xa,Xc),tracl(XR)))). +fof(tracl,axiom,![Xw,XR]:(elem(Xw,XR)=>elem(Xw,tracl(XR)))). +fof(tracl,axiom,![XR]:subseteq(tracl(XR),times(fld(XR),fld(XR)))). +fof(fin_mono,axiom,![XA,XB]:(subseteq(XA,XB)=>subseteq(fin(XA),fin(XB)))). +fof(fin,axiom,![Xa,XA,XB]:((elem(Xa,XA)&elem(XB,fin(XA)))=>elem(cons(Xa,XB),fin(XA)))). +fof(fin,axiom,![XA]:elem(emptyset,fin(XA))). +fof(fin,axiom,![XA]:subseteq(fin(XA),pow(XA))). +fof(lmao,axiom,![Xx]:elem(Xx,emptyset)). +fof(preimg,axiom,![XR,XA]:preimg(XR,XA)=emptyset). +fof(fld,axiom,![XR]:fld(XR)=emptyset). +fof(times,axiom,![XA,XB]:times(XA,XB)=emptyset). +fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). +fof(pow,axiom,![XA]:pow(XA)=emptyset). +fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). +------------------ +fof(acc,conjecture,(elem(fa,fld(fR))&elem(preimg(fR,cons(fa,emptyset)),pow(fld(fR))))=>elem(fa,fld(fR))). +fof(refltracl,axiom,![Xa,Xb,XA,XR,Xc]:((elem(pair(Xa,Xb),refltracl(XA,XR))&elem(pair(Xb,Xc),XR))=>elem(pair(Xa,Xc),refltracl(XA,XR)))). +fof(refltracl,axiom,![Xa,XA,XR]:(elem(Xa,XA)=>elem(pair(Xa,Xa),refltracl(XA,XR)))). +fof(refltracl,axiom,![XA,XR]:subseteq(refltracl(XA,XR),times(XA,XA))). +fof(quasirefltracl,axiom,![Xa,Xb,XR,Xc]:((elem(pair(Xa,Xb),quasirefltracl(XR))&elem(pair(Xb,Xc),XR))=>elem(pair(Xa,Xc),quasirefltracl(XR)))). +fof(quasirefltracl,axiom,![Xa,XR]:(elem(Xa,fld(XR))=>elem(pair(Xa,Xa),quasirefltracl(XR)))). +fof(quasirefltracl,axiom,![XR]:subseteq(quasirefltracl(XR),times(fld(XR),fld(XR)))). +fof(tracl,axiom,![Xa,Xb,XR,Xc]:((elem(pair(Xa,Xb),tracl(XR))&elem(pair(Xb,Xc),XR))=>elem(pair(Xa,Xc),tracl(XR)))). +fof(tracl,axiom,![Xw,XR]:(elem(Xw,XR)=>elem(Xw,tracl(XR)))). +fof(tracl,axiom,![XR]:subseteq(tracl(XR),times(fld(XR),fld(XR)))). +fof(fin_mono,axiom,![XA,XB]:(subseteq(XA,XB)=>subseteq(fin(XA),fin(XB)))). +fof(fin,axiom,![Xa,XA,XB]:((elem(Xa,XA)&elem(XB,fin(XA)))=>elem(cons(Xa,XB),fin(XA)))). +fof(fin,axiom,![XA]:elem(emptyset,fin(XA))). +fof(fin,axiom,![XA]:subseteq(fin(XA),pow(XA))). +fof(lmao,axiom,![Xx]:elem(Xx,emptyset)). +fof(preimg,axiom,![XR,XA]:preimg(XR,XA)=emptyset). +fof(fld,axiom,![XR]:fld(XR)=emptyset). +fof(times,axiom,![XA,XB]:times(XA,XB)=emptyset). +fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). +fof(pow,axiom,![XA]:pow(XA)=emptyset). +fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)).
\ No newline at end of file diff --git a/test/golden/inductive/generating tasks.golden b/test/golden/inductive/generating tasks.golden new file mode 100644 index 0000000..2fb04fe --- /dev/null +++ b/test/golden/inductive/generating tasks.golden @@ -0,0 +1,8965 @@ +[ Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "lmao" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "preimg" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "preimg" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "fld" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "times" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "cons" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "pow" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "subseteq" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "A" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "B" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "fin" + , taskConjecture = TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "A" ) + ] + ] + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "lmao" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "preimg" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "preimg" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "fld" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "times" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "cons" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "pow" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "subseteq" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "A" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "B" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "fin" + , taskConjecture = Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "A" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "B" ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "A" ) + ] + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "B" ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "A" ) + ] + ] + ) + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "fin" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "B" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "fin" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + , + ( Marker "fin" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + , + ( Marker "lmao" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "preimg" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "preimg" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "fld" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "times" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "cons" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "pow" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "subseteq" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "A" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "B" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + , + ( Marker "fin_mono1" + , TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermVar + ( NamedVar "A" ) + , TermVar + ( NamedVar "B" ) + ] + ) + ] + , taskConjectureLabel = Marker "fin_mono" + , taskConjecture = TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "A" ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "B" ) + ] + ] + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "fin_mono" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "B" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "fin" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "B" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "fin" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + , + ( Marker "fin" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + , + ( Marker "lmao" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "preimg" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "preimg" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "fld" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "times" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "cons" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "pow" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "subseteq" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "A" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "B" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "tracl" + , taskConjecture = Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "w" ) + , TermVar + ( NamedVar "R" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "w" ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + ] + ] + ] + ) + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "fin_mono" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "B" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "fin" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "B" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "fin" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + , + ( Marker "fin" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + , + ( Marker "lmao" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "preimg" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "preimg" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "fld" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "times" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "cons" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "pow" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "subseteq" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "A" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "B" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "tracl" + , taskConjecture = Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + ] + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "c" ) + ] + , TermVar + ( NamedVar "R" ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "c" ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + ] + ] + ] + ) + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "tracl" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + , TermVar + ( B + ( NamedVar "R" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "tracl" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( B + ( NamedVar "R" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "tracl" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ] + ) + ) + ) + , + ( Marker "fin_mono" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "B" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "fin" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "B" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "fin" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + , + ( Marker "fin" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + , + ( Marker "lmao" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "preimg" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "preimg" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "fld" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "times" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "cons" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "pow" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "subseteq" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "A" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "B" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "quasirefltracl" + , taskConjecture = Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "a" ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "a" ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + ] + ] + ] + ) + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "tracl" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + , TermVar + ( B + ( NamedVar "R" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "tracl" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( B + ( NamedVar "R" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "tracl" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ] + ) + ) + ) + , + ( Marker "fin_mono" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "B" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "fin" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "B" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "fin" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + , + ( Marker "fin" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + , + ( Marker "lmao" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "preimg" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "preimg" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "fld" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "times" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "cons" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "pow" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "subseteq" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "A" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "B" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "quasirefltracl" + , taskConjecture = Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + ] + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "c" ) + ] + , TermVar + ( NamedVar "R" ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "c" ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + ] + ] + ] + ) + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "quasirefltracl" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "qrefltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + , TermVar + ( B + ( NamedVar "R" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "qrefltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "quasirefltracl" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "qrefltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "quasirefltracl" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "qrefltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ] + ) + ) + ) + , + ( Marker "tracl" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + , TermVar + ( B + ( NamedVar "R" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "tracl" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( B + ( NamedVar "R" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "tracl" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ] + ) + ) + ) + , + ( Marker "fin_mono" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "B" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "fin" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "B" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "fin" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + , + ( Marker "fin" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + , + ( Marker "lmao" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "preimg" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "preimg" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "fld" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "times" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "cons" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "pow" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "subseteq" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "A" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "B" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "refltracl" + , taskConjecture = Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "A" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "a" ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermVar + ( NamedVar "A" ) + , TermVar + ( NamedVar "A" ) + ] + ] + ) + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "quasirefltracl" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "qrefltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + , TermVar + ( B + ( NamedVar "R" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "qrefltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "quasirefltracl" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "qrefltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "quasirefltracl" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "qrefltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ] + ) + ) + ) + , + ( Marker "tracl" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + , TermVar + ( B + ( NamedVar "R" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "tracl" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( B + ( NamedVar "R" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "tracl" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ] + ) + ) + ) + , + ( Marker "fin_mono" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "B" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "fin" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "B" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "fin" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + , + ( Marker "fin" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + , + ( Marker "lmao" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "preimg" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "preimg" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "fld" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "times" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "cons" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "pow" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "subseteq" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "A" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "B" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "refltracl" + , taskConjecture = Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermVar + ( NamedVar "A" ) + , TermVar + ( NamedVar "A" ) + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "c" ) + ] + , TermVar + ( NamedVar "R" ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "c" ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermVar + ( NamedVar "A" ) + , TermVar + ( NamedVar "A" ) + ] + ] + ) + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "refltracl" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "refltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + , TermVar + ( B + ( NamedVar "R" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "refltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "refltracl" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "refltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "refltracl" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "refltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + , + ( Marker "quasirefltracl" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "qrefltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + , TermVar + ( B + ( NamedVar "R" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "qrefltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "quasirefltracl" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "qrefltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "quasirefltracl" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "qrefltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ] + ) + ) + ) + , + ( Marker "tracl" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + , TermVar + ( B + ( NamedVar "R" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "tracl" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( B + ( NamedVar "R" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "tracl" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ] + ) + ) + ) + , + ( Marker "fin_mono" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "B" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "fin" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "B" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "fin" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + , + ( Marker "fin" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + , + ( Marker "lmao" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "preimg" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "preimg" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "fld" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "times" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "cons" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "pow" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "subseteq" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "A" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "B" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "acc" + , taskConjecture = Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "xa" ) + ) + , TermVar + ( B + ( NamedVar "xb" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "xa" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "xb" ) + ) + ] + ] + ) + ) + ) + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "refltracl" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "refltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + , TermVar + ( B + ( NamedVar "R" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "refltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "refltracl" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "refltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "refltracl" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "refltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + , + ( Marker "quasirefltracl" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "qrefltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + , TermVar + ( B + ( NamedVar "R" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "qrefltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "quasirefltracl" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "a" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "qrefltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "quasirefltracl" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "qrefltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ] + ) + ) + ) + , + ( Marker "tracl" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + , TermVar + ( B + ( NamedVar "R" ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "c" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "tracl" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + , TermVar + ( B + ( NamedVar "R" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "w" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "tracl" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + ] + ] + ) + ) + ) + , + ( Marker "fin_mono" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "B" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "fin" + , Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "B" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + ) + , + ( Marker "fin" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + , + ( Marker "fin" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + ] + ) + ) + ) + , + ( Marker "lmao" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "preimg" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "preimg" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "fld" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "R" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "times" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "cons" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "pow" + , Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + , + ( Marker "subseteq" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "B" ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "A" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "B" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "acc" + , taskConjecture = Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "a" ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "preimg" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "a" ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + ] + ] + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "a" ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + ] + ] + ) + } +]
\ No newline at end of file diff --git a/test/golden/inductive/glossing.golden b/test/golden/inductive/glossing.golden new file mode 100644 index 0000000..e76a88f --- /dev/null +++ b/test/golden/inductive/glossing.golden @@ -0,0 +1,1136 @@ +[ BlockDefn + ( SourcePos + { sourceName = "test/examples/inductive.tex" + , sourceLine = Pos 3 + , sourceColumn = Pos 1 + } + ) + ( Marker "subseteq" ) + ( DefnPredicate [] + ( PredicateRelation + ( Command "subseteq" ) + ) + ( NamedVar "A" :| + [ NamedVar "B" ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( NamedVar "A" ) + , TermVar + ( NamedVar "B" ) + ] + ) + ) +, BlockDefn + ( SourcePos + { sourceName = "test/examples/inductive.tex" + , sourceLine = Pos 7 + , sourceColumn = Pos 1 + } + ) + ( Marker "pow" ) + ( DefnOp + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ NamedVar "A" ] + ( TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ) + ) +, BlockDefn + ( SourcePos + { sourceName = "test/examples/inductive.tex" + , sourceLine = Pos 11 + , sourceColumn = Pos 1 + } + ) + ( Marker "cons" ) + ( DefnOp + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ NamedVar "a" + , NamedVar "B" + ] + ( TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ) + ) +, BlockDefn + ( SourcePos + { sourceName = "test/examples/inductive.tex" + , sourceLine = Pos 15 + , sourceColumn = Pos 1 + } + ) + ( Marker "times" ) + ( DefnOp + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + [ NamedVar "A" + , NamedVar "B" + ] + ( TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ) + ) +, BlockDefn + ( SourcePos + { sourceName = "test/examples/inductive.tex" + , sourceLine = Pos 19 + , sourceColumn = Pos 1 + } + ) + ( Marker "fld" ) + ( DefnOp + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ NamedVar "R" ] + ( TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ) + ) +, BlockDefn + ( SourcePos + { sourceName = "test/examples/inductive.tex" + , sourceLine = Pos 23 + , sourceColumn = Pos 1 + } + ) + ( Marker "preimg" ) + ( DefnOp + [ Just + ( Command "preimg" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ NamedVar "R" + , NamedVar "A" + ] + ( TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ) + ) +, BlockAxiom + ( SourcePos + { sourceName = "test/examples/inductive.tex" + , sourceLine = Pos 27 + , sourceColumn = Pos 1 + } + ) + ( Marker "lmao" ) + ( Axiom [] + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) +, BlockInductive + ( SourcePos + { sourceName = "test/examples/inductive.tex" + , sourceLine = Pos 31 + , sourceColumn = Pos 1 + } + ) + ( Marker "fin" ) + ( Inductive + { inductiveSymbol = + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + , inductiveParams = + [ NamedVar "A" ] + , inductiveDomain = TermSymbol + ( SymbolMixfix + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "A" ) + ] + , inductiveIntros = IntroRule + { introConditions = [] + , introResult = TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "A" ) + ] + ] + } :| + [ IntroRule + { introConditions = + [ TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "A" ) + ] + , TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "B" ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "A" ) + ] + ] + ] + , introResult = TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "B" ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "A" ) + ] + ] + } + ] + } + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/inductive.tex" + , sourceLine = Pos 39 + , sourceColumn = Pos 1 + } + ) + ( Marker "fin_mono" ) + ( Lemma + [ Asm ( PropositionalConstant IsTop ) + , Asm ( PropositionalConstant IsTop ) + , Asm + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermVar + ( NamedVar "A" ) + , TermVar + ( NamedVar "B" ) + ] + ) + ] + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "subseteq" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "A" ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "B" ) + ] + ] + ) + ) +, BlockInductive + ( SourcePos + { sourceName = "test/examples/inductive.tex" + , sourceLine = Pos 45 + , sourceColumn = Pos 1 + } + ) + ( Marker "tracl" ) + ( Inductive + { inductiveSymbol = + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + , inductiveParams = + [ NamedVar "R" ] + , inductiveDomain = TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + ] + ] + , inductiveIntros = IntroRule + { introConditions = + [ TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "w" ) + , TermVar + ( NamedVar "R" ) + ] + ] + , introResult = TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "w" ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + ] + ] + } :| + [ IntroRule + { introConditions = + [ TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + ] + ] + , TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "c" ) + ] + , TermVar + ( NamedVar "R" ) + ] + ] + , introResult = TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "c" ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + ] + ] + } + ] + } + ) +, BlockInductive + ( SourcePos + { sourceName = "test/examples/inductive.tex" + , sourceLine = Pos 53 + , sourceColumn = Pos 1 + } + ) + ( Marker "quasirefltracl" ) + ( Inductive + { inductiveSymbol = + [ Just + ( Command "qrefltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + , inductiveParams = + [ NamedVar "R" ] + , inductiveDomain = TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + ] + ] + , inductiveIntros = IntroRule + { introConditions = + [ TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "a" ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + ] + ] + ] + , introResult = TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "a" ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "qrefltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + ] + ] + } :| + [ IntroRule + { introConditions = + [ TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "qrefltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + ] + ] + , TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "c" ) + ] + , TermVar + ( NamedVar "R" ) + ] + ] + , introResult = TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "c" ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "qrefltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + ] + ] + } + ] + } + ) +, BlockInductive + ( SourcePos + { sourceName = "test/examples/inductive.tex" + , sourceLine = Pos 61 + , sourceColumn = Pos 1 + } + ) + ( Marker "refltracl" ) + ( Inductive + { inductiveSymbol = + [ Just + ( Command "refltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + , inductiveParams = + [ NamedVar "A" + , NamedVar "R" + ] + , inductiveDomain = TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermVar + ( NamedVar "A" ) + , TermVar + ( NamedVar "A" ) + ] + , inductiveIntros = IntroRule + { introConditions = + [ TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "A" ) + ] + ] + , introResult = TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "a" ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "refltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "A" ) + , TermVar + ( NamedVar "R" ) + ] + ] + } :| + [ IntroRule + { introConditions = + [ TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "b" ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "refltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "A" ) + , TermVar + ( NamedVar "R" ) + ] + ] + , TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "b" ) + , TermVar + ( NamedVar "c" ) + ] + , TermVar + ( NamedVar "R" ) + ] + ] + , introResult = TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "a" ) + , TermVar + ( NamedVar "c" ) + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "refltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "A" ) + , TermVar + ( NamedVar "R" ) + ] + ] + } + ] + } + ) +, BlockInductive + ( SourcePos + { sourceName = "test/examples/inductive.tex" + , sourceLine = Pos 69 + , sourceColumn = Pos 1 + } + ) + ( Marker "acc" ) + ( Inductive + { inductiveSymbol = + [ Just + ( Command "acc" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + , inductiveParams = + [ NamedVar "R" ] + , inductiveDomain = TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + ] + , inductiveIntros = IntroRule + { introConditions = + [ TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "a" ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + ] + ] + , TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "preimg" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "a" ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "acc" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + ] + ] + ] + ] + , introResult = TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "a" ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "acc" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "R" ) + ] + ] + } :| [] + } + ) +]
\ No newline at end of file diff --git a/test/golden/inductive/parsing.golden b/test/golden/inductive/parsing.golden new file mode 100644 index 0000000..7438daa --- /dev/null +++ b/test/golden/inductive/parsing.golden @@ -0,0 +1,1076 @@ +[ BlockDefn + ( SourcePos + { sourceName = "test/examples/inductive.tex" + , sourceLine = Pos 3 + , sourceColumn = Pos 1 + } + ) + ( Marker "subseteq" ) + ( Defn [] + ( DefnRel + ( NamedVar "A" ) + ( Command "subseteq" ) + ( NamedVar "B" ) + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "A" ) :| [] + ) Positive + ( RelationSymbol + ( Symbol "=" ) + ) + ( ExprVar + ( NamedVar "B" ) :| [] + ) + ) + ) + ) + ) +, BlockDefn + ( SourcePos + { sourceName = "test/examples/inductive.tex" + , sourceLine = Pos 7 + , sourceColumn = Pos 1 + } + ) + ( Marker "pow" ) + ( DefnOp + ( SymbolPattern + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ NamedVar "A" ] + ) + ( ExprOp + [ Just + ( Command "emptyset" ) + ] [] + ) + ) +, BlockDefn + ( SourcePos + { sourceName = "test/examples/inductive.tex" + , sourceLine = Pos 11 + , sourceColumn = Pos 1 + } + ) + ( Marker "cons" ) + ( DefnOp + ( SymbolPattern + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ NamedVar "a" + , NamedVar "B" + ] + ) + ( ExprOp + [ Just + ( Command "emptyset" ) + ] [] + ) + ) +, BlockDefn + ( SourcePos + { sourceName = "test/examples/inductive.tex" + , sourceLine = Pos 15 + , sourceColumn = Pos 1 + } + ) + ( Marker "times" ) + ( DefnOp + ( SymbolPattern + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + [ NamedVar "A" + , NamedVar "B" + ] + ) + ( ExprOp + [ Just + ( Command "emptyset" ) + ] [] + ) + ) +, BlockDefn + ( SourcePos + { sourceName = "test/examples/inductive.tex" + , sourceLine = Pos 19 + , sourceColumn = Pos 1 + } + ) + ( Marker "fld" ) + ( DefnOp + ( SymbolPattern + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ NamedVar "R" ] + ) + ( ExprOp + [ Just + ( Command "emptyset" ) + ] [] + ) + ) +, BlockDefn + ( SourcePos + { sourceName = "test/examples/inductive.tex" + , sourceLine = Pos 23 + , sourceColumn = Pos 1 + } + ) + ( Marker "preimg" ) + ( DefnOp + ( SymbolPattern + [ Just + ( Command "preimg" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ NamedVar "R" + , NamedVar "A" + ] + ) + ( ExprOp + [ Just + ( Command "emptyset" ) + ] [] + ) + ) +, BlockAxiom + ( SourcePos + { sourceName = "test/examples/inductive.tex" + , sourceLine = Pos 27 + , sourceColumn = Pos 1 + } + ) + ( Marker "lmao" ) + ( Axiom [] + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "x" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprOp + [ Just + ( Command "emptyset" ) + ] [] :| [] + ) + ) + ) + ) + ) +, BlockInductive + ( SourcePos + { sourceName = "test/examples/inductive.tex" + , sourceLine = Pos 31 + , sourceColumn = Pos 1 + } + ) + ( Marker "fin" ) + ( Inductive + { inductiveSymbolPattern = SymbolPattern + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ NamedVar "A" ] + , inductiveDomain = ExprOp + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "A" ) + ] + , inductiveIntros = IntroRule + { introConditions = [] + , introResult = FormulaChain + ( ChainBase + ( ExprOp + [ Just + ( Command "emptyset" ) + ] [] :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprOp + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "A" ) + ] :| [] + ) + ) + } :| + [ IntroRule + { introConditions = + [ FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "a" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "A" ) :| [] + ) + ) + , FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "B" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprOp + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "A" ) + ] :| [] + ) + ) + ] + , introResult = FormulaChain + ( ChainBase + ( ExprOp + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "a" ) + , ExprVar + ( NamedVar "B" ) + ] :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprOp + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "A" ) + ] :| [] + ) + ) + } + ] + } + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/inductive.tex" + , sourceLine = Pos 39 + , sourceColumn = Pos 1 + } + ) + ( Marker "fin_mono" ) + ( Lemma + [ AsmLetNoun + ( NamedVar "A" :| + [ NamedVar "B" ] + ) NounPhrase ( [] ) + ( Noun + ( SgPl + { sg = + [ Just + ( Word "set" ) + ] + , pl = + [ Just + ( Word "sets" ) + ] + } + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + , AsmSuppose + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "A" ) :| [] + ) Positive + ( RelationSymbol + ( Command "subseteq" ) + ) + ( ExprVar + ( NamedVar "B" ) :| [] + ) + ) + ) + ) + ] + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprOp + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "A" ) + ] :| [] + ) Positive + ( RelationSymbol + ( Command "subseteq" ) + ) + ( ExprOp + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "B" ) + ] :| [] + ) + ) + ) + ) + ) +, BlockInductive + ( SourcePos + { sourceName = "test/examples/inductive.tex" + , sourceLine = Pos 45 + , sourceColumn = Pos 1 + } + ) + ( Marker "tracl" ) + ( Inductive + { inductiveSymbolPattern = SymbolPattern + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ NamedVar "R" ] + , inductiveDomain = ExprOp + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + [ ExprOp + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "R" ) + ] + , ExprOp + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "R" ) + ] + ] + , inductiveIntros = IntroRule + { introConditions = + [ FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "w" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "R" ) :| [] + ) + ) + ] + , introResult = FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "w" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprOp + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "R" ) + ] :| [] + ) + ) + } :| + [ IntroRule + { introConditions = + [ FormulaChain + ( ChainBase + ( ExprOp + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "a" ) + , ExprVar + ( NamedVar "b" ) + ] :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprOp + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "R" ) + ] :| [] + ) + ) + , FormulaChain + ( ChainBase + ( ExprOp + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "b" ) + , ExprVar + ( NamedVar "c" ) + ] :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "R" ) :| [] + ) + ) + ] + , introResult = FormulaChain + ( ChainBase + ( ExprOp + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "a" ) + , ExprVar + ( NamedVar "c" ) + ] :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprOp + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "R" ) + ] :| [] + ) + ) + } + ] + } + ) +, BlockInductive + ( SourcePos + { sourceName = "test/examples/inductive.tex" + , sourceLine = Pos 53 + , sourceColumn = Pos 1 + } + ) + ( Marker "quasirefltracl" ) + ( Inductive + { inductiveSymbolPattern = SymbolPattern + [ Just + ( Command "qrefltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ NamedVar "R" ] + , inductiveDomain = ExprOp + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + [ ExprOp + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "R" ) + ] + , ExprOp + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "R" ) + ] + ] + , inductiveIntros = IntroRule + { introConditions = + [ FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "a" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprOp + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "R" ) + ] :| [] + ) + ) + ] + , introResult = FormulaChain + ( ChainBase + ( ExprOp + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "a" ) + , ExprVar + ( NamedVar "a" ) + ] :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprOp + [ Just + ( Command "qrefltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "R" ) + ] :| [] + ) + ) + } :| + [ IntroRule + { introConditions = + [ FormulaChain + ( ChainBase + ( ExprOp + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "a" ) + , ExprVar + ( NamedVar "b" ) + ] :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprOp + [ Just + ( Command "qrefltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "R" ) + ] :| [] + ) + ) + , FormulaChain + ( ChainBase + ( ExprOp + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "b" ) + , ExprVar + ( NamedVar "c" ) + ] :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "R" ) :| [] + ) + ) + ] + , introResult = FormulaChain + ( ChainBase + ( ExprOp + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "a" ) + , ExprVar + ( NamedVar "c" ) + ] :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprOp + [ Just + ( Command "qrefltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "R" ) + ] :| [] + ) + ) + } + ] + } + ) +, BlockInductive + ( SourcePos + { sourceName = "test/examples/inductive.tex" + , sourceLine = Pos 61 + , sourceColumn = Pos 1 + } + ) + ( Marker "refltracl" ) + ( Inductive + { inductiveSymbolPattern = SymbolPattern + [ Just + ( Command "refltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ NamedVar "A" + , NamedVar "R" + ] + , inductiveDomain = ExprOp + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + [ ExprVar + ( NamedVar "A" ) + , ExprVar + ( NamedVar "A" ) + ] + , inductiveIntros = IntroRule + { introConditions = + [ FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "a" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "A" ) :| [] + ) + ) + ] + , introResult = FormulaChain + ( ChainBase + ( ExprOp + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "a" ) + , ExprVar + ( NamedVar "a" ) + ] :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprOp + [ Just + ( Command "refltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "A" ) + , ExprVar + ( NamedVar "R" ) + ] :| [] + ) + ) + } :| + [ IntroRule + { introConditions = + [ FormulaChain + ( ChainBase + ( ExprOp + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "a" ) + , ExprVar + ( NamedVar "b" ) + ] :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprOp + [ Just + ( Command "refltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "A" ) + , ExprVar + ( NamedVar "R" ) + ] :| [] + ) + ) + , FormulaChain + ( ChainBase + ( ExprOp + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "b" ) + , ExprVar + ( NamedVar "c" ) + ] :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "R" ) :| [] + ) + ) + ] + , introResult = FormulaChain + ( ChainBase + ( ExprOp + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "a" ) + , ExprVar + ( NamedVar "c" ) + ] :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprOp + [ Just + ( Command "refltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "A" ) + , ExprVar + ( NamedVar "R" ) + ] :| [] + ) + ) + } + ] + } + ) +, BlockInductive + ( SourcePos + { sourceName = "test/examples/inductive.tex" + , sourceLine = Pos 69 + , sourceColumn = Pos 1 + } + ) + ( Marker "acc" ) + ( Inductive + { inductiveSymbolPattern = SymbolPattern + [ Just + ( Command "acc" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ NamedVar "R" ] + , inductiveDomain = ExprOp + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "R" ) + ] + , inductiveIntros = IntroRule + { introConditions = + [ FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "a" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprOp + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "R" ) + ] :| [] + ) + ) + , FormulaChain + ( ChainBase + ( ExprOp + [ Just + ( Command "preimg" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "R" ) + , ExprFiniteSet + ( ExprVar + ( NamedVar "a" ) :| [] + ) + ] :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprOp + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprOp + [ Just + ( Command "acc" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "R" ) + ] + ] :| [] + ) + ) + ] + , introResult = FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "a" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprOp + [ Just + ( Command "acc" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "R" ) + ] :| [] + ) + ) + } :| [] + } + ) +]
\ No newline at end of file diff --git a/test/golden/inductive/scanning.golden b/test/golden/inductive/scanning.golden new file mode 100644 index 0000000..c3ad452 --- /dev/null +++ b/test/golden/inductive/scanning.golden @@ -0,0 +1,92 @@ +[ ScanRelationSymbol + ( Command "subseteq" ) + ( Marker "subseteq" ) +, ScanFunctionSymbol + [ Just + ( Command "pow" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ( Marker "pow" ) +, ScanFunctionSymbol + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ( Marker "cons" ) +, ScanFunctionSymbol + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ( Marker "times" ) +, ScanFunctionSymbol + [ Just + ( Command "fld" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ( Marker "fld" ) +, ScanFunctionSymbol + [ Just + ( Command "preimg" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ( Marker "preimg" ) +, ScanFunctionSymbol + [ Just + ( Command "fin" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ( Marker "fin" ) +, ScanFunctionSymbol + [ Just + ( Command "tracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ( Marker "tracl" ) +, ScanFunctionSymbol + [ Just + ( Command "qrefltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ( Marker "quasirefltracl" ) +, ScanFunctionSymbol + [ Just + ( Command "refltracl" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ( Marker "refltracl" ) +, ScanFunctionSymbol + [ Just + ( Command "acc" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ( Marker "acc" ) +]
\ No newline at end of file diff --git a/test/golden/inductive/tokenizing.golden b/test/golden/inductive/tokenizing.golden new file mode 100644 index 0000000..b43d176 --- /dev/null +++ b/test/golden/inductive/tokenizing.golden @@ -0,0 +1,514 @@ +[ BeginEnv "definition" +, Label "subseteq" +, BeginEnv "math" +, Variable "A" +, Command "subseteq" +, Variable "B" +, EndEnv "math" +, Word "iff" +, BeginEnv "math" +, Variable "A" +, Symbol "=" +, Variable "B" +, EndEnv "math" +, Symbol "." +, EndEnv "definition" +, BeginEnv "definition" +, Label "pow" +, BeginEnv "math" +, Command "pow" +, InvisibleBraceL +, Variable "A" +, InvisibleBraceR +, Symbol "=" +, Command "emptyset" +, EndEnv "math" +, Symbol "." +, EndEnv "definition" +, BeginEnv "definition" +, Label "cons" +, BeginEnv "math" +, Command "cons" +, InvisibleBraceL +, Variable "a" +, InvisibleBraceR +, InvisibleBraceL +, Variable "B" +, InvisibleBraceR +, Symbol "=" +, Command "emptyset" +, EndEnv "math" +, Symbol "." +, EndEnv "definition" +, BeginEnv "definition" +, Label "times" +, BeginEnv "math" +, Variable "A" +, Command "times" +, Variable "B" +, Symbol "=" +, Command "emptyset" +, EndEnv "math" +, Symbol "." +, EndEnv "definition" +, BeginEnv "definition" +, Label "fld" +, BeginEnv "math" +, Command "fld" +, InvisibleBraceL +, Variable "R" +, InvisibleBraceR +, Symbol "=" +, Command "emptyset" +, EndEnv "math" +, Symbol "." +, EndEnv "definition" +, BeginEnv "definition" +, Label "preimg" +, BeginEnv "math" +, Command "preimg" +, InvisibleBraceL +, Variable "R" +, InvisibleBraceR +, InvisibleBraceL +, Variable "A" +, InvisibleBraceR +, Symbol "=" +, Command "emptyset" +, EndEnv "math" +, Symbol "." +, EndEnv "definition" +, BeginEnv "axiom" +, Label "lmao" +, BeginEnv "math" +, Variable "x" +, Command "in" +, Command "emptyset" +, EndEnv "math" +, Symbol "." +, EndEnv "axiom" +, BeginEnv "inductive" +, Label "fin" +, Word "define" +, BeginEnv "math" +, Command "fin" +, InvisibleBraceL +, Variable "A" +, InvisibleBraceR +, Command "subseteq" +, Command "pow" +, InvisibleBraceL +, Variable "A" +, InvisibleBraceR +, EndEnv "math" +, Word "inductively" +, Word "as" +, Word "follows" +, Symbol "." +, BeginEnv "enumerate" +, Command "item" +, BeginEnv "math" +, Command "emptyset" +, Command "in" +, Command "fin" +, InvisibleBraceL +, Variable "A" +, InvisibleBraceR +, EndEnv "math" +, Symbol "." +, Command "item" +, Word "if" +, BeginEnv "math" +, Variable "a" +, Command "in" +, Variable "A" +, EndEnv "math" +, Word "and" +, BeginEnv "math" +, Variable "B" +, Command "in" +, Command "fin" +, InvisibleBraceL +, Variable "A" +, InvisibleBraceR +, EndEnv "math" +, Symbol "," +, Word "then" +, BeginEnv "math" +, Command "cons" +, InvisibleBraceL +, Variable "a" +, InvisibleBraceR +, InvisibleBraceL +, Variable "B" +, InvisibleBraceR +, Command "in" +, Command "fin" +, InvisibleBraceL +, Variable "A" +, InvisibleBraceR +, EndEnv "math" +, Symbol "." +, EndEnv "enumerate" +, EndEnv "inductive" +, BeginEnv "lemma" +, Label "fin_mono" +, Word "let" +, BeginEnv "math" +, Variable "A" +, Symbol "," +, Variable "B" +, EndEnv "math" +, Word "be" +, Word "sets" +, Symbol "." +, Word "suppose" +, BeginEnv "math" +, Variable "A" +, Command "subseteq" +, Variable "B" +, EndEnv "math" +, Symbol "." +, Word "then" +, BeginEnv "math" +, Command "fin" +, InvisibleBraceL +, Variable "A" +, InvisibleBraceR +, Command "subseteq" +, Command "fin" +, InvisibleBraceL +, Variable "B" +, InvisibleBraceR +, EndEnv "math" +, Symbol "." +, EndEnv "lemma" +, BeginEnv "inductive" +, Label "tracl" +, Word "define" +, BeginEnv "math" +, Command "tracl" +, InvisibleBraceL +, Variable "R" +, InvisibleBraceR +, Command "subseteq" +, Command "fld" +, InvisibleBraceL +, Variable "R" +, InvisibleBraceR +, Command "times" +, Command "fld" +, InvisibleBraceL +, Variable "R" +, InvisibleBraceR +, EndEnv "math" +, Word "inductively" +, Word "as" +, Word "follows" +, Symbol "." +, BeginEnv "enumerate" +, Command "item" +, Word "if" +, BeginEnv "math" +, Variable "w" +, Command "in" +, Variable "R" +, EndEnv "math" +, Symbol "," +, Word "then" +, BeginEnv "math" +, Variable "w" +, Command "in" +, Command "tracl" +, InvisibleBraceL +, Variable "R" +, InvisibleBraceR +, EndEnv "math" +, Symbol "." +, Command "item" +, Word "if" +, BeginEnv "math" +, ParenL +, Variable "a" +, Symbol "," +, Variable "b" +, ParenR +, Command "in" +, Command "tracl" +, InvisibleBraceL +, Variable "R" +, InvisibleBraceR +, EndEnv "math" +, Word "and" +, BeginEnv "math" +, ParenL +, Variable "b" +, Symbol "," +, Variable "c" +, ParenR +, Command "in" +, Variable "R" +, EndEnv "math" +, Symbol "," +, Word "then" +, BeginEnv "math" +, ParenL +, Variable "a" +, Symbol "," +, Variable "c" +, ParenR +, Command "in" +, Command "tracl" +, InvisibleBraceL +, Variable "R" +, InvisibleBraceR +, EndEnv "math" +, Symbol "." +, EndEnv "enumerate" +, EndEnv "inductive" +, BeginEnv "inductive" +, Label "quasirefltracl" +, Word "define" +, BeginEnv "math" +, Command "qrefltracl" +, InvisibleBraceL +, Variable "R" +, InvisibleBraceR +, Command "subseteq" +, Command "fld" +, InvisibleBraceL +, Variable "R" +, InvisibleBraceR +, Command "times" +, Command "fld" +, InvisibleBraceL +, Variable "R" +, InvisibleBraceR +, EndEnv "math" +, Word "inductively" +, Word "as" +, Word "follows" +, Symbol "." +, BeginEnv "enumerate" +, Command "item" +, Word "if" +, BeginEnv "math" +, Variable "a" +, Command "in" +, Command "fld" +, InvisibleBraceL +, Variable "R" +, InvisibleBraceR +, EndEnv "math" +, Symbol "," +, Word "then" +, BeginEnv "math" +, ParenL +, Variable "a" +, Symbol "," +, Variable "a" +, ParenR +, Command "in" +, Command "qrefltracl" +, InvisibleBraceL +, Variable "R" +, InvisibleBraceR +, EndEnv "math" +, Symbol "." +, Command "item" +, Word "if" +, BeginEnv "math" +, ParenL +, Variable "a" +, Symbol "," +, Variable "b" +, ParenR +, Command "in" +, Command "qrefltracl" +, InvisibleBraceL +, Variable "R" +, InvisibleBraceR +, EndEnv "math" +, Word "and" +, BeginEnv "math" +, ParenL +, Variable "b" +, Symbol "," +, Variable "c" +, ParenR +, Command "in" +, Variable "R" +, EndEnv "math" +, Symbol "," +, Word "then" +, BeginEnv "math" +, ParenL +, Variable "a" +, Symbol "," +, Variable "c" +, ParenR +, Command "in" +, Command "qrefltracl" +, InvisibleBraceL +, Variable "R" +, InvisibleBraceR +, EndEnv "math" +, Symbol "." +, EndEnv "enumerate" +, EndEnv "inductive" +, BeginEnv "inductive" +, Label "refltracl" +, Word "define" +, BeginEnv "math" +, Command "refltracl" +, InvisibleBraceL +, Variable "A" +, InvisibleBraceR +, InvisibleBraceL +, Variable "R" +, InvisibleBraceR +, Command "subseteq" +, Variable "A" +, Command "times" +, Variable "A" +, EndEnv "math" +, Word "inductively" +, Word "as" +, Word "follows" +, Symbol "." +, BeginEnv "enumerate" +, Command "item" +, Word "if" +, BeginEnv "math" +, Variable "a" +, Command "in" +, Variable "A" +, EndEnv "math" +, Symbol "," +, Word "then" +, BeginEnv "math" +, ParenL +, Variable "a" +, Symbol "," +, Variable "a" +, ParenR +, Command "in" +, Command "refltracl" +, InvisibleBraceL +, Variable "A" +, InvisibleBraceR +, InvisibleBraceL +, Variable "R" +, InvisibleBraceR +, EndEnv "math" +, Symbol "." +, Command "item" +, Word "if" +, BeginEnv "math" +, ParenL +, Variable "a" +, Symbol "," +, Variable "b" +, ParenR +, Command "in" +, Command "refltracl" +, InvisibleBraceL +, Variable "A" +, InvisibleBraceR +, InvisibleBraceL +, Variable "R" +, InvisibleBraceR +, EndEnv "math" +, Word "and" +, BeginEnv "math" +, ParenL +, Variable "b" +, Symbol "," +, Variable "c" +, ParenR +, Command "in" +, Variable "R" +, EndEnv "math" +, Symbol "," +, Word "then" +, BeginEnv "math" +, ParenL +, Variable "a" +, Symbol "," +, Variable "c" +, ParenR +, Command "in" +, Command "refltracl" +, InvisibleBraceL +, Variable "A" +, InvisibleBraceR +, InvisibleBraceL +, Variable "R" +, InvisibleBraceR +, EndEnv "math" +, Symbol "." +, EndEnv "enumerate" +, EndEnv "inductive" +, BeginEnv "inductive" +, Label "acc" +, Word "define" +, BeginEnv "math" +, Command "acc" +, InvisibleBraceL +, Variable "R" +, InvisibleBraceR +, Command "subseteq" +, Command "fld" +, InvisibleBraceL +, Variable "R" +, InvisibleBraceR +, EndEnv "math" +, Word "inductively" +, Word "as" +, Word "follows" +, Symbol "." +, BeginEnv "enumerate" +, Command "item" +, Word "if" +, BeginEnv "math" +, Variable "a" +, Command "in" +, Command "fld" +, InvisibleBraceL +, Variable "R" +, InvisibleBraceR +, EndEnv "math" +, Word "and" +, BeginEnv "math" +, Command "preimg" +, InvisibleBraceL +, Variable "R" +, InvisibleBraceR +, InvisibleBraceL +, VisibleBraceL +, Variable "a" +, VisibleBraceR +, InvisibleBraceR +, Command "in" +, Command "pow" +, InvisibleBraceL +, Command "acc" +, InvisibleBraceL +, Variable "R" +, InvisibleBraceR +, InvisibleBraceR +, EndEnv "math" +, Symbol "," +, Word "then" +, BeginEnv "math" +, Variable "a" +, Command "in" +, Command "acc" +, InvisibleBraceL +, Variable "R" +, InvisibleBraceR +, EndEnv "math" +, Symbol "." +, EndEnv "enumerate" +, EndEnv "inductive" +]
\ No newline at end of file diff --git a/test/golden/inductive/verification.golden b/test/golden/inductive/verification.golden new file mode 100644 index 0000000..69b9873 --- /dev/null +++ b/test/golden/inductive/verification.golden @@ -0,0 +1 @@ +VerificationSuccess
\ No newline at end of file |