Step |
Hyp |
Ref |
Expression |
1 |
|
mulsuniflem.1 |
|
2 |
|
mulsuniflem.2 |
|
3 |
|
mulsuniflem.3 |
|
4 |
|
mulsuniflem.4 |
|
5 |
1
|
scutcld |
|
6 |
3 5
|
eqeltrd |
|
7 |
2
|
scutcld |
|
8 |
4 7
|
eqeltrd |
|
9 |
|
mulsval |
|
10 |
6 8 9
|
syl2anc |
|
11 |
6 8
|
mulscut2 |
|
12 |
1 3
|
cofcutr1d |
|
13 |
2 4
|
cofcutr1d |
|
14 |
13
|
adantr |
|
15 |
|
reeanv |
|
16 |
|
leftssno |
|
17 |
|
simprl |
|
18 |
16 17
|
sselid |
|
19 |
18
|
adantrr |
|
20 |
8
|
adantr |
|
21 |
19 20
|
mulscld |
|
22 |
6
|
adantr |
|
23 |
|
leftssno |
|
24 |
|
simprr |
|
25 |
23 24
|
sselid |
|
26 |
25
|
adantrr |
|
27 |
22 26
|
mulscld |
|
28 |
21 27
|
addscld |
|
29 |
19 26
|
mulscld |
|
30 |
28 29
|
subscld |
|
31 |
30
|
adantrrr |
|
32 |
|
ssltss1 |
|
33 |
1 32
|
syl |
|
34 |
33
|
adantr |
|
35 |
|
simprl |
|
36 |
34 35
|
sseldd |
|
37 |
36
|
adantrl |
|
38 |
37 20
|
mulscld |
|
39 |
38 27
|
addscld |
|
40 |
37 26
|
mulscld |
|
41 |
39 40
|
subscld |
|
42 |
41
|
adantrrr |
|
43 |
|
ssltss1 |
|
44 |
2 43
|
syl |
|
45 |
44
|
adantr |
|
46 |
|
simprr |
|
47 |
45 46
|
sseldd |
|
48 |
47
|
adantrl |
|
49 |
22 48
|
mulscld |
|
50 |
38 49
|
addscld |
|
51 |
37 48
|
mulscld |
|
52 |
50 51
|
subscld |
|
53 |
52
|
adantrrr |
|
54 |
18
|
adantrr |
|
55 |
37
|
adantrrr |
|
56 |
25
|
adantrr |
|
57 |
8
|
adantr |
|
58 |
|
simprrl |
|
59 |
58
|
adantl |
|
60 |
8
|
adantr |
|
61 |
|
ssltleft |
|
62 |
8 61
|
syl |
|
63 |
62
|
adantr |
|
64 |
|
snidg |
|
65 |
8 64
|
syl |
|
66 |
65
|
adantr |
|
67 |
63 24 66
|
ssltsepcd |
|
68 |
25 60 67
|
sltled |
|
69 |
68
|
adantrr |
|
70 |
54 55 56 57 59 69
|
slemuld |
|
71 |
21 29
|
subscld |
|
72 |
38 40
|
subscld |
|
73 |
71 72 27
|
sleadd1d |
|
74 |
73
|
adantrrr |
|
75 |
70 74
|
mpbid |
|
76 |
21 27 29
|
addsubsd |
|
77 |
76
|
adantrrr |
|
78 |
38 27 40
|
addsubsd |
|
79 |
78
|
adantrrr |
|
80 |
75 77 79
|
3brtr4d |
|
81 |
6
|
adantr |
|
82 |
48
|
adantrrr |
|
83 |
6
|
adantr |
|
84 |
|
scutcut |
|
85 |
1 84
|
syl |
|
86 |
85
|
simp2d |
|
87 |
86
|
adantr |
|
88 |
|
ovex |
|
89 |
88
|
snid |
|
90 |
3 89
|
eqeltrdi |
|
91 |
90
|
adantr |
|
92 |
87 35 91
|
ssltsepcd |
|
93 |
36 83 92
|
sltled |
|
94 |
93
|
adantrl |
|
95 |
94
|
adantrrr |
|
96 |
|
simprrr |
|
97 |
96
|
adantl |
|
98 |
55 81 56 82 95 97
|
slemuld |
|
99 |
51 49 40 27
|
slesubsub3bd |
|
100 |
27 40
|
subscld |
|
101 |
49 51
|
subscld |
|
102 |
100 101 38
|
sleadd2d |
|
103 |
99 102
|
bitrd |
|
104 |
103
|
adantrrr |
|
105 |
98 104
|
mpbid |
|
106 |
38 27 40
|
addsubsassd |
|
107 |
106
|
adantrrr |
|
108 |
38 49 51
|
addsubsassd |
|
109 |
108
|
adantrrr |
|
110 |
105 107 109
|
3brtr4d |
|
111 |
31 42 53 80 110
|
sletrd |
|
112 |
111
|
anassrs |
|
113 |
112
|
expr |
|
114 |
113
|
reximdvva |
|
115 |
114
|
expcom |
|
116 |
115
|
com23 |
|
117 |
116
|
imp |
|
118 |
15 117
|
sylan2br |
|
119 |
118
|
an4s |
|
120 |
119
|
impcom |
|
121 |
120
|
anassrs |
|
122 |
121
|
expr |
|
123 |
122
|
ralimdva |
|
124 |
14 123
|
mpd |
|
125 |
124
|
expr |
|
126 |
125
|
ralimdva |
|
127 |
12 126
|
mpd |
|
128 |
|
eqeq1 |
|
129 |
128
|
2rexbidv |
|
130 |
129
|
rexab |
|
131 |
|
r19.41vv |
|
132 |
131
|
exbii |
|
133 |
|
rexcom4 |
|
134 |
|
rexcom4 |
|
135 |
|
ovex |
|
136 |
|
breq2 |
|
137 |
135 136
|
ceqsexv |
|
138 |
137
|
rexbii |
|
139 |
134 138
|
bitr3i |
|
140 |
139
|
rexbii |
|
141 |
133 140
|
bitr3i |
|
142 |
130 132 141
|
3bitr2i |
|
143 |
|
ssun1 |
|
144 |
|
ssrexv |
|
145 |
143 144
|
ax-mp |
|
146 |
142 145
|
sylbir |
|
147 |
146
|
2ralimi |
|
148 |
127 147
|
syl |
|
149 |
1 3
|
cofcutr2d |
|
150 |
2 4
|
cofcutr2d |
|
151 |
150
|
adantr |
|
152 |
|
reeanv |
|
153 |
|
rightssno |
|
154 |
|
simprl |
|
155 |
153 154
|
sselid |
|
156 |
155
|
adantrr |
|
157 |
8
|
adantr |
|
158 |
156 157
|
mulscld |
|
159 |
6
|
adantr |
|
160 |
|
rightssno |
|
161 |
|
simprr |
|
162 |
160 161
|
sselid |
|
163 |
162
|
adantrr |
|
164 |
159 163
|
mulscld |
|
165 |
158 164
|
addscld |
|
166 |
156 163
|
mulscld |
|
167 |
165 166
|
subscld |
|
168 |
167
|
adantrrr |
|
169 |
|
ssltss2 |
|
170 |
1 169
|
syl |
|
171 |
170
|
adantr |
|
172 |
|
simprl |
|
173 |
171 172
|
sseldd |
|
174 |
173
|
adantrl |
|
175 |
174 157
|
mulscld |
|
176 |
175 164
|
addscld |
|
177 |
174 163
|
mulscld |
|
178 |
176 177
|
subscld |
|
179 |
178
|
adantrrr |
|
180 |
|
ssltss2 |
|
181 |
2 180
|
syl |
|
182 |
181
|
adantr |
|
183 |
|
simprr |
|
184 |
182 183
|
sseldd |
|
185 |
184
|
adantrl |
|
186 |
159 185
|
mulscld |
|
187 |
175 186
|
addscld |
|
188 |
173 184
|
mulscld |
|
189 |
188
|
adantrl |
|
190 |
187 189
|
subscld |
|
191 |
190
|
adantrrr |
|
192 |
174
|
adantrrr |
|
193 |
155
|
adantrr |
|
194 |
8
|
adantr |
|
195 |
162
|
adantrr |
|
196 |
|
simprrl |
|
197 |
196
|
adantl |
|
198 |
8
|
adantr |
|
199 |
|
ssltright |
|
200 |
8 199
|
syl |
|
201 |
200
|
adantr |
|
202 |
65
|
adantr |
|
203 |
201 202 161
|
ssltsepcd |
|
204 |
198 162 203
|
sltled |
|
205 |
204
|
adantrr |
|
206 |
192 193 194 195 197 205
|
slemuld |
|
207 |
177 175 166 158
|
slesubsub2bd |
|
208 |
158 166
|
subscld |
|
209 |
175 177
|
subscld |
|
210 |
208 209 164
|
sleadd1d |
|
211 |
207 210
|
bitrd |
|
212 |
211
|
adantrrr |
|
213 |
206 212
|
mpbid |
|
214 |
158 164 166
|
addsubsd |
|
215 |
214
|
adantrrr |
|
216 |
175 164 177
|
addsubsd |
|
217 |
216
|
adantrrr |
|
218 |
213 215 217
|
3brtr4d |
|
219 |
6
|
adantr |
|
220 |
185
|
adantrrr |
|
221 |
6
|
adantr |
|
222 |
85
|
simp3d |
|
223 |
222
|
adantr |
|
224 |
90
|
adantr |
|
225 |
223 224 172
|
ssltsepcd |
|
226 |
221 173 225
|
sltled |
|
227 |
226
|
adantrl |
|
228 |
227
|
adantrrr |
|
229 |
|
simprrr |
|
230 |
229
|
adantl |
|
231 |
219 192 220 195 228 230
|
slemuld |
|
232 |
164 177 186 189
|
slesubsubbd |
|
233 |
164 177
|
subscld |
|
234 |
186 189
|
subscld |
|
235 |
233 234 175
|
sleadd2d |
|
236 |
232 235
|
bitrd |
|
237 |
236
|
adantrrr |
|
238 |
231 237
|
mpbid |
|
239 |
175 164 177
|
addsubsassd |
|
240 |
239
|
adantrrr |
|
241 |
175 186 189
|
addsubsassd |
|
242 |
241
|
adantrrr |
|
243 |
238 240 242
|
3brtr4d |
|
244 |
168 179 191 218 243
|
sletrd |
|
245 |
244
|
anassrs |
|
246 |
245
|
expr |
|
247 |
246
|
reximdvva |
|
248 |
247
|
expcom |
|
249 |
248
|
com23 |
|
250 |
249
|
imp |
|
251 |
152 250
|
sylan2br |
|
252 |
251
|
an4s |
|
253 |
252
|
impcom |
|
254 |
253
|
anassrs |
|
255 |
254
|
expr |
|
256 |
255
|
ralimdva |
|
257 |
151 256
|
mpd |
|
258 |
257
|
expr |
|
259 |
258
|
ralimdva |
|
260 |
149 259
|
mpd |
|
261 |
|
eqeq1 |
|
262 |
261
|
2rexbidv |
|
263 |
262
|
rexab |
|
264 |
|
r19.41vv |
|
265 |
264
|
exbii |
|
266 |
|
rexcom4 |
|
267 |
|
rexcom4 |
|
268 |
|
ovex |
|
269 |
|
breq2 |
|
270 |
268 269
|
ceqsexv |
|
271 |
270
|
rexbii |
|
272 |
267 271
|
bitr3i |
|
273 |
272
|
rexbii |
|
274 |
266 273
|
bitr3i |
|
275 |
263 265 274
|
3bitr2i |
|
276 |
|
ssun2 |
|
277 |
|
ssrexv |
|
278 |
276 277
|
ax-mp |
|
279 |
275 278
|
sylbir |
|
280 |
279
|
2ralimi |
|
281 |
260 280
|
syl |
|
282 |
|
ralunb |
Could not format ( A. xO e. ( { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } u. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> ( A. xO e. { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z /\ A. xO e. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. xO e. ( { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } u. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> ( A. xO e. { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z /\ A. xO e. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |- |
283 |
|
eqeq1 |
Could not format ( e = xO -> ( e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <-> xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) ) ) : No typesetting found for |- ( e = xO -> ( e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <-> xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) ) ) with typecode |- |
284 |
283
|
2rexbidv |
Could not format ( e = xO -> ( E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <-> E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) ) ) : No typesetting found for |- ( e = xO -> ( E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <-> E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) ) ) with typecode |- |
285 |
284
|
ralab |
Could not format ( A. xO e. { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> A. xO ( E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. xO e. { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> A. xO ( E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |- |
286 |
|
r19.23v |
Could not format ( A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |- |
287 |
286
|
ralbii |
Could not format ( A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. f e. ( _Left ` A ) ( E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. f e. ( _Left ` A ) ( E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |- |
288 |
|
r19.23v |
Could not format ( A. f e. ( _Left ` A ) ( E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. f e. ( _Left ` A ) ( E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |- |
289 |
287 288
|
bitri |
Could not format ( A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |- |
290 |
289
|
albii |
Could not format ( A. xO A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. xO ( E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. xO A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. xO ( E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |- |
291 |
|
ralcom4 |
Could not format ( A. f e. ( _Left ` A ) A. xO A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. xO A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. f e. ( _Left ` A ) A. xO A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. xO A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |- |
292 |
|
ralcom4 |
Could not format ( A. g e. ( _Left ` B ) A. xO ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. xO A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. g e. ( _Left ` B ) A. xO ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. xO A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |- |
293 |
|
ovex |
|
294 |
|
breq1 |
Could not format ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> ( xO <_s z <-> ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) ) : No typesetting found for |- ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> ( xO <_s z <-> ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) ) with typecode |- |
295 |
294
|
rexbidv |
Could not format ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> ( E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) ) : No typesetting found for |- ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> ( E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) ) with typecode |- |
296 |
293 295
|
ceqsalv |
Could not format ( A. xO ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) : No typesetting found for |- ( A. xO ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) with typecode |- |
297 |
296
|
ralbii |
Could not format ( A. g e. ( _Left ` B ) A. xO ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) : No typesetting found for |- ( A. g e. ( _Left ` B ) A. xO ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) with typecode |- |
298 |
292 297
|
bitr3i |
Could not format ( A. xO A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) : No typesetting found for |- ( A. xO A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) with typecode |- |
299 |
298
|
ralbii |
Could not format ( A. f e. ( _Left ` A ) A. xO A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) : No typesetting found for |- ( A. f e. ( _Left ` A ) A. xO A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) with typecode |- |
300 |
291 299
|
bitr3i |
Could not format ( A. xO A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) : No typesetting found for |- ( A. xO A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) ( xO = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) with typecode |- |
301 |
285 290 300
|
3bitr2i |
Could not format ( A. xO e. { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) : No typesetting found for |- ( A. xO e. { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z ) with typecode |- |
302 |
|
eqeq1 |
Could not format ( h = xO -> ( h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <-> xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) ) ) : No typesetting found for |- ( h = xO -> ( h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <-> xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) ) ) with typecode |- |
303 |
302
|
2rexbidv |
Could not format ( h = xO -> ( E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <-> E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) ) ) : No typesetting found for |- ( h = xO -> ( E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <-> E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) ) ) with typecode |- |
304 |
303
|
ralab |
Could not format ( A. xO e. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> A. xO ( E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. xO e. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> A. xO ( E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |- |
305 |
|
r19.23v |
Could not format ( A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |- |
306 |
305
|
ralbii |
Could not format ( A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. i e. ( _Right ` A ) ( E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. i e. ( _Right ` A ) ( E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |- |
307 |
|
r19.23v |
Could not format ( A. i e. ( _Right ` A ) ( E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. i e. ( _Right ` A ) ( E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |- |
308 |
306 307
|
bitri |
Could not format ( A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |- |
309 |
308
|
albii |
Could not format ( A. xO A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. xO ( E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. xO A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. xO ( E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |- |
310 |
|
ralcom4 |
Could not format ( A. i e. ( _Right ` A ) A. xO A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. xO A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. i e. ( _Right ` A ) A. xO A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. xO A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |- |
311 |
|
ralcom4 |
Could not format ( A. j e. ( _Right ` B ) A. xO ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. xO A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) : No typesetting found for |- ( A. j e. ( _Right ` B ) A. xO ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. xO A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) ) with typecode |- |
312 |
|
ovex |
|
313 |
|
breq1 |
Could not format ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> ( xO <_s z <-> ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) ) : No typesetting found for |- ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> ( xO <_s z <-> ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) ) with typecode |- |
314 |
313
|
rexbidv |
Could not format ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> ( E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) ) : No typesetting found for |- ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> ( E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) ) with typecode |- |
315 |
312 314
|
ceqsalv |
Could not format ( A. xO ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) : No typesetting found for |- ( A. xO ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) with typecode |- |
316 |
315
|
ralbii |
Could not format ( A. j e. ( _Right ` B ) A. xO ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) : No typesetting found for |- ( A. j e. ( _Right ` B ) A. xO ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) with typecode |- |
317 |
311 316
|
bitr3i |
Could not format ( A. xO A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) : No typesetting found for |- ( A. xO A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) with typecode |- |
318 |
317
|
ralbii |
Could not format ( A. i e. ( _Right ` A ) A. xO A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) : No typesetting found for |- ( A. i e. ( _Right ` A ) A. xO A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) with typecode |- |
319 |
310 318
|
bitr3i |
Could not format ( A. xO A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) : No typesetting found for |- ( A. xO A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) ( xO = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) -> E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) with typecode |- |
320 |
304 309 319
|
3bitr2i |
Could not format ( A. xO e. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) : No typesetting found for |- ( A. xO e. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) with typecode |- |
321 |
301 320
|
anbi12i |
Could not format ( ( A. xO e. { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z /\ A. xO e. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z /\ A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) ) : No typesetting found for |- ( ( A. xO e. { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z /\ A. xO e. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) <-> ( A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z /\ A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) ) with typecode |- |
322 |
282 321
|
bitri |
Could not format ( A. xO e. ( { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } u. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> ( A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z /\ A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) ) : No typesetting found for |- ( A. xO e. ( { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } u. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z <-> ( A. f e. ( _Left ` A ) A. g e. ( _Left ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) <_s z /\ A. i e. ( _Right ` A ) A. j e. ( _Right ` B ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) <_s z ) ) with typecode |- |
323 |
148 281 322
|
sylanbrc |
Could not format ( ph -> A. xO e. ( { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } u. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) : No typesetting found for |- ( ph -> A. xO e. ( { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } u. { h | E. i e. ( _Right ` A ) E. j e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s j ) ) -s ( i x.s j ) ) } ) E. z e. ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) xO <_s z ) with typecode |- |
324 |
1 3
|
cofcutr1d |
|
325 |
2 4
|
cofcutr2d |
|
326 |
325
|
adantr |
|
327 |
|
reeanv |
|
328 |
33
|
adantr |
|
329 |
|
simprl |
|
330 |
328 329
|
sseldd |
|
331 |
330
|
adantrl |
|
332 |
8
|
adantr |
|
333 |
331 332
|
mulscld |
|
334 |
6
|
adantr |
|
335 |
181
|
adantr |
|
336 |
|
simprr |
|
337 |
335 336
|
sseldd |
|
338 |
337
|
adantrl |
|
339 |
334 338
|
mulscld |
|
340 |
333 339
|
addscld |
|
341 |
331 338
|
mulscld |
|
342 |
340 341
|
subscld |
|
343 |
342
|
adantrrr |
|
344 |
|
simprl |
|
345 |
16 344
|
sselid |
|
346 |
8
|
adantr |
|
347 |
345 346
|
mulscld |
|
348 |
347
|
adantrr |
|
349 |
348 339
|
addscld |
|
350 |
345
|
adantrr |
|
351 |
350 338
|
mulscld |
|
352 |
349 351
|
subscld |
|
353 |
352
|
adantrrr |
|
354 |
6
|
adantr |
|
355 |
|
simprr |
|
356 |
160 355
|
sselid |
|
357 |
354 356
|
mulscld |
|
358 |
357
|
adantrr |
|
359 |
348 358
|
addscld |
|
360 |
345 356
|
mulscld |
|
361 |
360
|
adantrr |
|
362 |
359 361
|
subscld |
|
363 |
362
|
adantrrr |
|
364 |
345
|
adantrr |
|
365 |
331
|
adantrrr |
|
366 |
8
|
adantr |
|
367 |
338
|
adantrrr |
|
368 |
|
simprrl |
|
369 |
368
|
adantl |
|
370 |
8
|
adantr |
|
371 |
|
scutcut |
|
372 |
2 371
|
syl |
|
373 |
372
|
simp3d |
|
374 |
373
|
adantr |
|
375 |
|
ovex |
|
376 |
375
|
snid |
|
377 |
4 376
|
eqeltrdi |
|
378 |
377
|
adantr |
|
379 |
374 378 336
|
ssltsepcd |
|
380 |
370 337 379
|
sltled |
|
381 |
380
|
adantrl |
|
382 |
381
|
adantrrr |
|
383 |
364 365 366 367 369 382
|
slemuld |
|
384 |
351 348 341 333
|
slesubsub2bd |
|
385 |
333 341
|
subscld |
|
386 |
348 351
|
subscld |
|
387 |
385 386 339
|
sleadd1d |
|
388 |
384 387
|
bitrd |
|
389 |
388
|
adantrrr |
|
390 |
383 389
|
mpbid |
|
391 |
333 339 341
|
addsubsd |
|
392 |
391
|
adantrrr |
|
393 |
348 339 351
|
addsubsd |
|
394 |
393
|
adantrrr |
|
395 |
390 392 394
|
3brtr4d |
|
396 |
6
|
adantr |
|
397 |
356
|
adantrr |
|
398 |
|
ssltleft |
|
399 |
6 398
|
syl |
|
400 |
399
|
adantr |
|
401 |
|
snidg |
|
402 |
6 401
|
syl |
|
403 |
402
|
adantr |
|
404 |
400 344 403
|
ssltsepcd |
|
405 |
345 354 404
|
sltled |
|
406 |
405
|
adantrr |
|
407 |
|
simprrr |
|
408 |
407
|
adantl |
|
409 |
364 396 367 397 406 408
|
slemuld |
|
410 |
361 358 351 339
|
slesubsub3bd |
|
411 |
339 351
|
subscld |
|
412 |
358 361
|
subscld |
|
413 |
411 412 348
|
sleadd2d |
|
414 |
410 413
|
bitrd |
|
415 |
414
|
adantrrr |
|
416 |
409 415
|
mpbid |
|
417 |
348 339 351
|
addsubsassd |
|
418 |
417
|
adantrrr |
|
419 |
348 358 361
|
addsubsassd |
|
420 |
419
|
adantrrr |
|
421 |
416 418 420
|
3brtr4d |
|
422 |
343 353 363 395 421
|
sletrd |
|
423 |
422
|
anassrs |
|
424 |
423
|
expr |
|
425 |
424
|
reximdvva |
|
426 |
425
|
expcom |
|
427 |
426
|
com23 |
|
428 |
427
|
imp |
|
429 |
327 428
|
sylan2br |
|
430 |
429
|
an4s |
|
431 |
430
|
impcom |
|
432 |
431
|
anassrs |
|
433 |
432
|
expr |
|
434 |
433
|
ralimdva |
|
435 |
326 434
|
mpd |
|
436 |
435
|
expr |
|
437 |
436
|
ralimdva |
|
438 |
324 437
|
mpd |
|
439 |
|
eqeq1 |
|
440 |
439
|
2rexbidv |
|
441 |
440
|
rexab |
|
442 |
|
r19.41vv |
|
443 |
442
|
exbii |
|
444 |
|
rexcom4 |
|
445 |
|
rexcom4 |
|
446 |
|
ovex |
|
447 |
|
breq1 |
|
448 |
446 447
|
ceqsexv |
|
449 |
448
|
rexbii |
|
450 |
445 449
|
bitr3i |
|
451 |
450
|
rexbii |
|
452 |
444 451
|
bitr3i |
|
453 |
441 443 452
|
3bitr2i |
|
454 |
|
ssun1 |
|
455 |
|
ssrexv |
|
456 |
454 455
|
ax-mp |
|
457 |
453 456
|
sylbir |
|
458 |
457
|
2ralimi |
|
459 |
438 458
|
syl |
|
460 |
1 3
|
cofcutr2d |
|
461 |
2 4
|
cofcutr1d |
|
462 |
461
|
adantr |
|
463 |
|
reeanv |
|
464 |
170
|
adantr |
|
465 |
|
simprl |
|
466 |
464 465
|
sseldd |
|
467 |
8
|
adantr |
|
468 |
466 467
|
mulscld |
|
469 |
468
|
adantrl |
|
470 |
6
|
adantr |
|
471 |
44
|
adantr |
|
472 |
|
simprr |
|
473 |
471 472
|
sseldd |
|
474 |
470 473
|
mulscld |
|
475 |
474
|
adantrl |
|
476 |
469 475
|
addscld |
|
477 |
466 473
|
mulscld |
|
478 |
477
|
adantrl |
|
479 |
476 478
|
subscld |
|
480 |
479
|
adantrrr |
|
481 |
6
|
adantr |
|
482 |
|
simprr |
|
483 |
23 482
|
sselid |
|
484 |
483
|
adantrr |
|
485 |
481 484
|
mulscld |
|
486 |
469 485
|
addscld |
|
487 |
466
|
adantrl |
|
488 |
487 484
|
mulscld |
|
489 |
486 488
|
subscld |
|
490 |
489
|
adantrrr |
|
491 |
|
simprl |
|
492 |
153 491
|
sselid |
|
493 |
8
|
adantr |
|
494 |
492 493
|
mulscld |
|
495 |
494
|
adantrr |
|
496 |
495 485
|
addscld |
|
497 |
492 483
|
mulscld |
|
498 |
497
|
adantrr |
|
499 |
496 498
|
subscld |
|
500 |
499
|
adantrrr |
|
501 |
6
|
adantr |
|
502 |
487
|
adantrrr |
|
503 |
483
|
adantrr |
|
504 |
473
|
adantrl |
|
505 |
504
|
adantrrr |
|
506 |
3
|
sneqd |
|
507 |
506 222
|
eqbrtrd |
|
508 |
507
|
adantr |
|
509 |
481 401
|
syl |
|
510 |
|
simprrl |
|
511 |
508 509 510
|
ssltsepcd |
|
512 |
481 487 511
|
sltled |
|
513 |
512
|
adantrrr |
|
514 |
|
simprrr |
|
515 |
514
|
adantl |
|
516 |
501 502 503 505 513 515
|
slemuld |
|
517 |
475 478 485 488
|
slesubsubbd |
|
518 |
475 478
|
subscld |
|
519 |
485 488
|
subscld |
|
520 |
518 519 469
|
sleadd2d |
|
521 |
517 520
|
bitrd |
|
522 |
521
|
adantrrr |
|
523 |
516 522
|
mpbid |
|
524 |
469 475 478
|
addsubsassd |
|
525 |
524
|
adantrrr |
|
526 |
469 485 488
|
addsubsassd |
|
527 |
526
|
adantrrr |
|
528 |
523 525 527
|
3brtr4d |
|
529 |
492
|
adantrr |
|
530 |
8
|
adantr |
|
531 |
|
simprrl |
|
532 |
531
|
adantl |
|
533 |
493 61
|
syl |
|
534 |
65
|
adantr |
|
535 |
533 482 534
|
ssltsepcd |
|
536 |
483 493 535
|
sltled |
|
537 |
536
|
adantrr |
|
538 |
502 529 503 530 532 537
|
slemuld |
|
539 |
469 488
|
subscld |
|
540 |
539
|
adantrrr |
|
541 |
495 498
|
subscld |
|
542 |
541
|
adantrrr |
|
543 |
485
|
adantrrr |
|
544 |
540 542 543
|
sleadd1d |
|
545 |
538 544
|
mpbid |
|
546 |
469 485 488
|
addsubsd |
|
547 |
546
|
adantrrr |
|
548 |
6
|
adantr |
|
549 |
548 483
|
mulscld |
|
550 |
494 549 497
|
addsubsd |
|
551 |
550
|
adantrr |
|
552 |
545 547 551
|
3brtr4d |
|
553 |
480 490 500 528 552
|
sletrd |
|
554 |
553
|
anassrs |
|
555 |
554
|
expr |
|
556 |
555
|
reximdvva |
|
557 |
556
|
expcom |
|
558 |
557
|
com23 |
|
559 |
558
|
imp |
|
560 |
463 559
|
sylan2br |
|
561 |
560
|
an4s |
|
562 |
561
|
impcom |
|
563 |
562
|
anassrs |
|
564 |
563
|
expr |
|
565 |
564
|
ralimdva |
|
566 |
462 565
|
mpd |
|
567 |
566
|
expr |
|
568 |
567
|
ralimdva |
|
569 |
460 568
|
mpd |
|
570 |
|
eqeq1 |
|
571 |
570
|
2rexbidv |
|
572 |
571
|
rexab |
|
573 |
|
r19.41vv |
|
574 |
573
|
exbii |
|
575 |
|
rexcom4 |
|
576 |
|
rexcom4 |
|
577 |
|
ovex |
|
578 |
|
breq1 |
|
579 |
577 578
|
ceqsexv |
|
580 |
579
|
rexbii |
|
581 |
576 580
|
bitr3i |
|
582 |
581
|
rexbii |
|
583 |
575 582
|
bitr3i |
|
584 |
572 574 583
|
3bitr2i |
|
585 |
|
ssun2 |
|
586 |
|
ssrexv |
|
587 |
585 586
|
ax-mp |
|
588 |
584 587
|
sylbir |
|
589 |
588
|
2ralimi |
|
590 |
569 589
|
syl |
|
591 |
|
ralunb |
Could not format ( A. xO e. ( { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } u. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> ( A. xO e. { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO /\ A. xO e. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. xO e. ( { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } u. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> ( A. xO e. { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO /\ A. xO e. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |- |
592 |
|
eqeq1 |
Could not format ( k = xO -> ( k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) <-> xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) ) : No typesetting found for |- ( k = xO -> ( k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) <-> xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) ) with typecode |- |
593 |
592
|
2rexbidv |
Could not format ( k = xO -> ( E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) <-> E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) ) : No typesetting found for |- ( k = xO -> ( E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) <-> E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) ) with typecode |- |
594 |
593
|
ralab |
Could not format ( A. xO e. { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> A. xO ( E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. xO e. { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> A. xO ( E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |- |
595 |
|
r19.23v |
Could not format ( A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |- |
596 |
595
|
ralbii |
Could not format ( A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. l e. ( _Left ` A ) ( E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. l e. ( _Left ` A ) ( E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |- |
597 |
|
r19.23v |
Could not format ( A. l e. ( _Left ` A ) ( E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. l e. ( _Left ` A ) ( E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |- |
598 |
596 597
|
bitri |
Could not format ( A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |- |
599 |
598
|
albii |
Could not format ( A. xO A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. xO ( E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. xO A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. xO ( E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |- |
600 |
|
ralcom4 |
Could not format ( A. l e. ( _Left ` A ) A. xO A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. xO A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. l e. ( _Left ` A ) A. xO A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. xO A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |- |
601 |
|
ralcom4 |
Could not format ( A. m e. ( _Right ` B ) A. xO ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. xO A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. m e. ( _Right ` B ) A. xO ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. xO A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |- |
602 |
|
ovex |
|
603 |
|
breq2 |
Could not format ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> ( z <_s xO <-> z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) ) : No typesetting found for |- ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> ( z <_s xO <-> z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) ) with typecode |- |
604 |
603
|
rexbidv |
Could not format ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> ( E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) ) : No typesetting found for |- ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> ( E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) ) with typecode |- |
605 |
602 604
|
ceqsalv |
Could not format ( A. xO ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) : No typesetting found for |- ( A. xO ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) with typecode |- |
606 |
605
|
ralbii |
Could not format ( A. m e. ( _Right ` B ) A. xO ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) : No typesetting found for |- ( A. m e. ( _Right ` B ) A. xO ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) with typecode |- |
607 |
601 606
|
bitr3i |
Could not format ( A. xO A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) : No typesetting found for |- ( A. xO A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) with typecode |- |
608 |
607
|
ralbii |
Could not format ( A. l e. ( _Left ` A ) A. xO A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) : No typesetting found for |- ( A. l e. ( _Left ` A ) A. xO A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) with typecode |- |
609 |
600 608
|
bitr3i |
Could not format ( A. xO A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) : No typesetting found for |- ( A. xO A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) ( xO = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) with typecode |- |
610 |
594 599 609
|
3bitr2i |
Could not format ( A. xO e. { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) : No typesetting found for |- ( A. xO e. { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) ) with typecode |- |
611 |
|
eqeq1 |
Could not format ( n = xO -> ( n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) <-> xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) ) : No typesetting found for |- ( n = xO -> ( n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) <-> xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) ) with typecode |- |
612 |
611
|
2rexbidv |
Could not format ( n = xO -> ( E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) <-> E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) ) : No typesetting found for |- ( n = xO -> ( E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) <-> E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) ) with typecode |- |
613 |
612
|
ralab |
Could not format ( A. xO e. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> A. xO ( E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. xO e. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> A. xO ( E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |- |
614 |
|
r19.23v |
Could not format ( A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |- |
615 |
614
|
ralbii |
Could not format ( A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. x e. ( _Right ` A ) ( E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. x e. ( _Right ` A ) ( E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |- |
616 |
|
r19.23v |
Could not format ( A. x e. ( _Right ` A ) ( E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. x e. ( _Right ` A ) ( E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |- |
617 |
615 616
|
bitri |
Could not format ( A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |- |
618 |
617
|
albii |
Could not format ( A. xO A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. xO ( E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. xO A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. xO ( E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |- |
619 |
|
ralcom4 |
Could not format ( A. x e. ( _Right ` A ) A. xO A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. xO A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. x e. ( _Right ` A ) A. xO A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. xO A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |- |
620 |
|
ralcom4 |
Could not format ( A. y e. ( _Left ` B ) A. xO ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. xO A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) : No typesetting found for |- ( A. y e. ( _Left ` B ) A. xO ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. xO A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) ) with typecode |- |
621 |
|
ovex |
|
622 |
|
breq2 |
Could not format ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> ( z <_s xO <-> z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) ) : No typesetting found for |- ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> ( z <_s xO <-> z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) ) with typecode |- |
623 |
622
|
rexbidv |
Could not format ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> ( E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) ) : No typesetting found for |- ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> ( E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) ) with typecode |- |
624 |
621 623
|
ceqsalv |
Could not format ( A. xO ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) : No typesetting found for |- ( A. xO ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) with typecode |- |
625 |
624
|
ralbii |
Could not format ( A. y e. ( _Left ` B ) A. xO ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) : No typesetting found for |- ( A. y e. ( _Left ` B ) A. xO ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) with typecode |- |
626 |
620 625
|
bitr3i |
Could not format ( A. xO A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) : No typesetting found for |- ( A. xO A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) with typecode |- |
627 |
626
|
ralbii |
Could not format ( A. x e. ( _Right ` A ) A. xO A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) : No typesetting found for |- ( A. x e. ( _Right ` A ) A. xO A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) with typecode |- |
628 |
619 627
|
bitr3i |
Could not format ( A. xO A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) : No typesetting found for |- ( A. xO A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) ( xO = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) -> E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) with typecode |- |
629 |
613 618 628
|
3bitr2i |
Could not format ( A. xO e. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) : No typesetting found for |- ( A. xO e. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) with typecode |- |
630 |
610 629
|
anbi12i |
Could not format ( ( A. xO e. { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO /\ A. xO e. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) /\ A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) ) : No typesetting found for |- ( ( A. xO e. { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO /\ A. xO e. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) <-> ( A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) /\ A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) ) with typecode |- |
631 |
591 630
|
bitri |
Could not format ( A. xO e. ( { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } u. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> ( A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) /\ A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) ) : No typesetting found for |- ( A. xO e. ( { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } u. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO <-> ( A. l e. ( _Left ` A ) A. m e. ( _Right ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) /\ A. x e. ( _Right ` A ) A. y e. ( _Left ` B ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) ) ) with typecode |- |
632 |
459 590 631
|
sylanbrc |
Could not format ( ph -> A. xO e. ( { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } u. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) : No typesetting found for |- ( ph -> A. xO e. ( { k | E. l e. ( _Left ` A ) E. m e. ( _Right ` B ) k = ( ( ( l x.s B ) +s ( A x.s m ) ) -s ( l x.s m ) ) } u. { n | E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) n = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } ) E. z e. ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) z <_s xO ) with typecode |- |
633 |
1 2 3 4
|
ssltmul1 |
|
634 |
10
|
sneqd |
|
635 |
633 634
|
breqtrd |
|
636 |
1 2 3 4
|
ssltmul2 |
|
637 |
634 636
|
eqbrtrrd |
|
638 |
11 323 632 635 637
|
cofcut1d |
|
639 |
10 638
|
eqtrd |
|