1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
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)).
|
