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/encoding tasks.golden | |
Initial commit
Diffstat (limited to 'test/golden/inductive/encoding tasks.golden')
| -rw-r--r-- | test/golden/inductive/encoding tasks.golden | 170 |
1 files changed, 170 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 |