Theorem precsexlemcbv

Description: Lemma for surreal reciprocals. Change some bound variables. (Contributed by Scott Fenton, 15-Mar-2025)

	Ref	Expression
Hypothesis	precsexlem.1	No typesetting found for |- F = rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. ) with typecode |-
Assertion	precsexlemcbv	Could not format assertion : No typesetting found for |- F = rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		precsexlem.1	Could not format F = rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. ) : No typesetting found for |- F = rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. ) with typecode |-
2		fveq2	$$⊢p=q\to 1^{st}\left(p\right)=1^{st}\left(q\right)$$
3		fveq2	$$⊢p=q\to 2^{nd}\left(p\right)=2^{nd}\left(q\right)$$
4	3	csbeq1d	Could not format ( p = q -> [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . = [_ ( 2nd ` q ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) : No typesetting found for |- ( p = q -> [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . = [_ ( 2nd ` q ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) with typecode |-
5	2 4	csbeq12dv	Could not format ( p = q -> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . = [_ ( 1st ` q ) / l ]_ [_ ( 2nd ` q ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) : No typesetting found for |- ( p = q -> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . = [_ ( 1st ` q ) / l ]_ [_ ( 2nd ` q ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) with typecode |-
6		rexeq	Could not format ( r = s -> ( E. yR e. r a = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) <-> E. yR e. s a = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) ) ) : No typesetting found for |- ( r = s -> ( E. yR e. r a = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) <-> E. yR e. s a = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) ) ) with typecode |-
7	6	rexbidv	Could not format ( r = s -> ( E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s ( E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s
8	7	abbidv	Could not format ( r = s -> { a | E. xL e. { x e. ( _Left ` A ) | 0s { a | E. xL e. { x e. ( _Left ` A ) | 0s
9	8	uneq2d	Could not format ( r = s -> ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
10	9	uneq2d	Could not format ( r = s -> ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
11		id	$$⊢r=s\to r=s$$
12		rexeq	Could not format ( r = s -> ( E. yR e. r a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> E. yR e. s a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) ) : No typesetting found for |- ( r = s -> ( E. yR e. r a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> E. yR e. s a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) ) with typecode |-
13	12	rexbidv	Could not format ( r = s -> ( E. xR e. ( _Right ` A ) E. yR e. r a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> E. xR e. ( _Right ` A ) E. yR e. s a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) ) : No typesetting found for |- ( r = s -> ( E. xR e. ( _Right ` A ) E. yR e. r a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> E. xR e. ( _Right ` A ) E. yR e. s a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) ) with typecode |-
14	13	abbidv	Could not format ( r = s -> { a | E. xR e. ( _Right ` A ) E. yR e. r a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) } = { a | E. xR e. ( _Right ` A ) E. yR e. s a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) } ) : No typesetting found for |- ( r = s -> { a | E. xR e. ( _Right ` A ) E. yR e. r a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) } = { a | E. xR e. ( _Right ` A ) E. yR e. s a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) } ) with typecode |-
15	14	uneq2d	Could not format ( r = s -> ( { a | E. xL e. { x e. ( _Left ` A ) | 0s ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
16	11 15	uneq12d	Could not format ( r = s -> ( r u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s ( r u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
17	10 16	opeq12d	Could not format ( r = s -> <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . = <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) : No typesetting found for |- ( r = s -> <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . = <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) with typecode |-
18		eqeq1	Could not format ( a = b -> ( a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> b = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) ) : No typesetting found for |- ( a = b -> ( a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> b = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) ) with typecode |-
19	18	2rexbidv	Could not format ( a = b -> ( E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> E. xR e. ( _Right ` A ) E. yL e. l b = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) ) : No typesetting found for |- ( a = b -> ( E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> E. xR e. ( _Right ` A ) E. yL e. l b = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) ) with typecode |-
20		oveq1	Could not format ( xR = zR -> ( xR -s A ) = ( zR -s A ) ) : No typesetting found for |- ( xR = zR -> ( xR -s A ) = ( zR -s A ) ) with typecode |-
21	20	oveq1d	Could not format ( xR = zR -> ( ( xR -s A ) x.s yL ) = ( ( zR -s A ) x.s yL ) ) : No typesetting found for |- ( xR = zR -> ( ( xR -s A ) x.s yL ) = ( ( zR -s A ) x.s yL ) ) with typecode |-
22	21	oveq2d	Could not format ( xR = zR -> ( 1s +s ( ( xR -s A ) x.s yL ) ) = ( 1s +s ( ( zR -s A ) x.s yL ) ) ) : No typesetting found for |- ( xR = zR -> ( 1s +s ( ( xR -s A ) x.s yL ) ) = ( 1s +s ( ( zR -s A ) x.s yL ) ) ) with typecode |-
23		id	Could not format ( xR = zR -> xR = zR ) : No typesetting found for |- ( xR = zR -> xR = zR ) with typecode |-
24	22 23	oveq12d	Could not format ( xR = zR -> ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) = ( ( 1s +s ( ( zR -s A ) x.s yL ) ) /su zR ) ) : No typesetting found for |- ( xR = zR -> ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) = ( ( 1s +s ( ( zR -s A ) x.s yL ) ) /su zR ) ) with typecode |-
25	24	eqeq2d	Could not format ( xR = zR -> ( b = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> b = ( ( 1s +s ( ( zR -s A ) x.s yL ) ) /su zR ) ) ) : No typesetting found for |- ( xR = zR -> ( b = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> b = ( ( 1s +s ( ( zR -s A ) x.s yL ) ) /su zR ) ) ) with typecode |-
26		oveq2	Could not format ( yL = w -> ( ( zR -s A ) x.s yL ) = ( ( zR -s A ) x.s w ) ) : No typesetting found for |- ( yL = w -> ( ( zR -s A ) x.s yL ) = ( ( zR -s A ) x.s w ) ) with typecode |-
27	26	oveq2d	Could not format ( yL = w -> ( 1s +s ( ( zR -s A ) x.s yL ) ) = ( 1s +s ( ( zR -s A ) x.s w ) ) ) : No typesetting found for |- ( yL = w -> ( 1s +s ( ( zR -s A ) x.s yL ) ) = ( 1s +s ( ( zR -s A ) x.s w ) ) ) with typecode |-
28	27	oveq1d	Could not format ( yL = w -> ( ( 1s +s ( ( zR -s A ) x.s yL ) ) /su zR ) = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) ) : No typesetting found for |- ( yL = w -> ( ( 1s +s ( ( zR -s A ) x.s yL ) ) /su zR ) = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) ) with typecode |-
29	28	eqeq2d	Could not format ( yL = w -> ( b = ( ( 1s +s ( ( zR -s A ) x.s yL ) ) /su zR ) <-> b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) ) ) : No typesetting found for |- ( yL = w -> ( b = ( ( 1s +s ( ( zR -s A ) x.s yL ) ) /su zR ) <-> b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) ) ) with typecode |-
30	25 29	cbvrex2vw	Could not format ( E. xR e. ( _Right ` A ) E. yL e. l b = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) ) : No typesetting found for |- ( E. xR e. ( _Right ` A ) E. yL e. l b = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) ) with typecode |-
31	19 30	bitrdi	Could not format ( a = b -> ( E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) ) ) : No typesetting found for |- ( a = b -> ( E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) ) ) with typecode |-
32	31	cbvabv	Could not format { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } = { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } : No typesetting found for |- { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } = { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } with typecode |-
33		eqeq1	Could not format ( a = b -> ( a = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) <-> b = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) ) ) : No typesetting found for |- ( a = b -> ( a = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) <-> b = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) ) ) with typecode |-
34	33	2rexbidv	Could not format ( a = b -> ( E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s ( E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s
35		oveq1	Could not format ( xL = zL -> ( xL -s A ) = ( zL -s A ) ) : No typesetting found for |- ( xL = zL -> ( xL -s A ) = ( zL -s A ) ) with typecode |-
36	35	oveq1d	Could not format ( xL = zL -> ( ( xL -s A ) x.s yR ) = ( ( zL -s A ) x.s yR ) ) : No typesetting found for |- ( xL = zL -> ( ( xL -s A ) x.s yR ) = ( ( zL -s A ) x.s yR ) ) with typecode |-
37	36	oveq2d	Could not format ( xL = zL -> ( 1s +s ( ( xL -s A ) x.s yR ) ) = ( 1s +s ( ( zL -s A ) x.s yR ) ) ) : No typesetting found for |- ( xL = zL -> ( 1s +s ( ( xL -s A ) x.s yR ) ) = ( 1s +s ( ( zL -s A ) x.s yR ) ) ) with typecode |-
38		id	Could not format ( xL = zL -> xL = zL ) : No typesetting found for |- ( xL = zL -> xL = zL ) with typecode |-
39	37 38	oveq12d	Could not format ( xL = zL -> ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) = ( ( 1s +s ( ( zL -s A ) x.s yR ) ) /su zL ) ) : No typesetting found for |- ( xL = zL -> ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) = ( ( 1s +s ( ( zL -s A ) x.s yR ) ) /su zL ) ) with typecode |-
40	39	eqeq2d	Could not format ( xL = zL -> ( b = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) <-> b = ( ( 1s +s ( ( zL -s A ) x.s yR ) ) /su zL ) ) ) : No typesetting found for |- ( xL = zL -> ( b = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) <-> b = ( ( 1s +s ( ( zL -s A ) x.s yR ) ) /su zL ) ) ) with typecode |-
41		oveq2	Could not format ( yR = t -> ( ( zL -s A ) x.s yR ) = ( ( zL -s A ) x.s t ) ) : No typesetting found for |- ( yR = t -> ( ( zL -s A ) x.s yR ) = ( ( zL -s A ) x.s t ) ) with typecode |-
42	41	oveq2d	Could not format ( yR = t -> ( 1s +s ( ( zL -s A ) x.s yR ) ) = ( 1s +s ( ( zL -s A ) x.s t ) ) ) : No typesetting found for |- ( yR = t -> ( 1s +s ( ( zL -s A ) x.s yR ) ) = ( 1s +s ( ( zL -s A ) x.s t ) ) ) with typecode |-
43	42	oveq1d	Could not format ( yR = t -> ( ( 1s +s ( ( zL -s A ) x.s yR ) ) /su zL ) = ( ( 1s +s ( ( zL -s A ) x.s t ) ) /su zL ) ) : No typesetting found for |- ( yR = t -> ( ( 1s +s ( ( zL -s A ) x.s yR ) ) /su zL ) = ( ( 1s +s ( ( zL -s A ) x.s t ) ) /su zL ) ) with typecode |-
44	43	eqeq2d	Could not format ( yR = t -> ( b = ( ( 1s +s ( ( zL -s A ) x.s yR ) ) /su zL ) <-> b = ( ( 1s +s ( ( zL -s A ) x.s t ) ) /su zL ) ) ) : No typesetting found for |- ( yR = t -> ( b = ( ( 1s +s ( ( zL -s A ) x.s yR ) ) /su zL ) <-> b = ( ( 1s +s ( ( zL -s A ) x.s t ) ) /su zL ) ) ) with typecode |-
45	40 44	cbvrex2vw	Could not format ( E. xL e. { x e. ( _Left ` A ) | 0s E. zL e. { x e. ( _Left ` A ) | 0s E. zL e. { x e. ( _Left ` A ) | 0s
46		breq2	$$⊢x=z\to \left(0_s{<}_{s}x\leftrightarrow 0_s{<}_{s}z\right)$$
47	46	cbvrabv	$$⊢\left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}=\left\{z\in L\left(A\right)|0_s{<}_{s}z\right\}$$
48	47	rexeqi	Could not format ( E. zL e. { x e. ( _Left ` A ) | 0s E. zL e. { z e. ( _Left ` A ) | 0s E. zL e. { z e. ( _Left ` A ) | 0s
49	45 48	bitri	Could not format ( E. xL e. { x e. ( _Left ` A ) | 0s E. zL e. { z e. ( _Left ` A ) | 0s E. zL e. { z e. ( _Left ` A ) | 0s
50	34 49	bitrdi	Could not format ( a = b -> ( E. xL e. { x e. ( _Left ` A ) | 0s E. zL e. { z e. ( _Left ` A ) | 0s ( E. xL e. { x e. ( _Left ` A ) | 0s E. zL e. { z e. ( _Left ` A ) | 0s
51	50	cbvabv	Could not format { a | E. xL e. { x e. ( _Left ` A ) | 0s
52	32 51	uneq12i	Could not format ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
53	52	uneq2i	Could not format ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
54		eqeq1	Could not format ( a = b -> ( a = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) <-> b = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) ) ) : No typesetting found for |- ( a = b -> ( a = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) <-> b = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) ) ) with typecode |-
55	54	2rexbidv	Could not format ( a = b -> ( E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s ( E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s
56	35	oveq1d	Could not format ( xL = zL -> ( ( xL -s A ) x.s yL ) = ( ( zL -s A ) x.s yL ) ) : No typesetting found for |- ( xL = zL -> ( ( xL -s A ) x.s yL ) = ( ( zL -s A ) x.s yL ) ) with typecode |-
57	56	oveq2d	Could not format ( xL = zL -> ( 1s +s ( ( xL -s A ) x.s yL ) ) = ( 1s +s ( ( zL -s A ) x.s yL ) ) ) : No typesetting found for |- ( xL = zL -> ( 1s +s ( ( xL -s A ) x.s yL ) ) = ( 1s +s ( ( zL -s A ) x.s yL ) ) ) with typecode |-
58	57 38	oveq12d	Could not format ( xL = zL -> ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) = ( ( 1s +s ( ( zL -s A ) x.s yL ) ) /su zL ) ) : No typesetting found for |- ( xL = zL -> ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) = ( ( 1s +s ( ( zL -s A ) x.s yL ) ) /su zL ) ) with typecode |-
59	58	eqeq2d	Could not format ( xL = zL -> ( b = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) <-> b = ( ( 1s +s ( ( zL -s A ) x.s yL ) ) /su zL ) ) ) : No typesetting found for |- ( xL = zL -> ( b = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) <-> b = ( ( 1s +s ( ( zL -s A ) x.s yL ) ) /su zL ) ) ) with typecode |-
60		oveq2	Could not format ( yL = w -> ( ( zL -s A ) x.s yL ) = ( ( zL -s A ) x.s w ) ) : No typesetting found for |- ( yL = w -> ( ( zL -s A ) x.s yL ) = ( ( zL -s A ) x.s w ) ) with typecode |-
61	60	oveq2d	Could not format ( yL = w -> ( 1s +s ( ( zL -s A ) x.s yL ) ) = ( 1s +s ( ( zL -s A ) x.s w ) ) ) : No typesetting found for |- ( yL = w -> ( 1s +s ( ( zL -s A ) x.s yL ) ) = ( 1s +s ( ( zL -s A ) x.s w ) ) ) with typecode |-
62	61	oveq1d	Could not format ( yL = w -> ( ( 1s +s ( ( zL -s A ) x.s yL ) ) /su zL ) = ( ( 1s +s ( ( zL -s A ) x.s w ) ) /su zL ) ) : No typesetting found for |- ( yL = w -> ( ( 1s +s ( ( zL -s A ) x.s yL ) ) /su zL ) = ( ( 1s +s ( ( zL -s A ) x.s w ) ) /su zL ) ) with typecode |-
63	62	eqeq2d	Could not format ( yL = w -> ( b = ( ( 1s +s ( ( zL -s A ) x.s yL ) ) /su zL ) <-> b = ( ( 1s +s ( ( zL -s A ) x.s w ) ) /su zL ) ) ) : No typesetting found for |- ( yL = w -> ( b = ( ( 1s +s ( ( zL -s A ) x.s yL ) ) /su zL ) <-> b = ( ( 1s +s ( ( zL -s A ) x.s w ) ) /su zL ) ) ) with typecode |-
64	59 63	cbvrex2vw	Could not format ( E. xL e. { x e. ( _Left ` A ) | 0s E. zL e. { x e. ( _Left ` A ) | 0s E. zL e. { x e. ( _Left ` A ) | 0s
65	47	rexeqi	Could not format ( E. zL e. { x e. ( _Left ` A ) | 0s E. zL e. { z e. ( _Left ` A ) | 0s E. zL e. { z e. ( _Left ` A ) | 0s
66	64 65	bitri	Could not format ( E. xL e. { x e. ( _Left ` A ) | 0s E. zL e. { z e. ( _Left ` A ) | 0s E. zL e. { z e. ( _Left ` A ) | 0s
67	55 66	bitrdi	Could not format ( a = b -> ( E. xL e. { x e. ( _Left ` A ) | 0s E. zL e. { z e. ( _Left ` A ) | 0s ( E. xL e. { x e. ( _Left ` A ) | 0s E. zL e. { z e. ( _Left ` A ) | 0s
68	67	cbvabv	Could not format { a | E. xL e. { x e. ( _Left ` A ) | 0s
69		eqeq1	Could not format ( a = b -> ( a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> b = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) ) : No typesetting found for |- ( a = b -> ( a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> b = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) ) with typecode |-
70	69	2rexbidv	Could not format ( a = b -> ( E. xR e. ( _Right ` A ) E. yR e. s a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> E. xR e. ( _Right ` A ) E. yR e. s b = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) ) : No typesetting found for |- ( a = b -> ( E. xR e. ( _Right ` A ) E. yR e. s a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> E. xR e. ( _Right ` A ) E. yR e. s b = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) ) with typecode |-
71	20	oveq1d	Could not format ( xR = zR -> ( ( xR -s A ) x.s yR ) = ( ( zR -s A ) x.s yR ) ) : No typesetting found for |- ( xR = zR -> ( ( xR -s A ) x.s yR ) = ( ( zR -s A ) x.s yR ) ) with typecode |-
72	71	oveq2d	Could not format ( xR = zR -> ( 1s +s ( ( xR -s A ) x.s yR ) ) = ( 1s +s ( ( zR -s A ) x.s yR ) ) ) : No typesetting found for |- ( xR = zR -> ( 1s +s ( ( xR -s A ) x.s yR ) ) = ( 1s +s ( ( zR -s A ) x.s yR ) ) ) with typecode |-
73	72 23	oveq12d	Could not format ( xR = zR -> ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) = ( ( 1s +s ( ( zR -s A ) x.s yR ) ) /su zR ) ) : No typesetting found for |- ( xR = zR -> ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) = ( ( 1s +s ( ( zR -s A ) x.s yR ) ) /su zR ) ) with typecode |-
74	73	eqeq2d	Could not format ( xR = zR -> ( b = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> b = ( ( 1s +s ( ( zR -s A ) x.s yR ) ) /su zR ) ) ) : No typesetting found for |- ( xR = zR -> ( b = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> b = ( ( 1s +s ( ( zR -s A ) x.s yR ) ) /su zR ) ) ) with typecode |-
75		oveq2	Could not format ( yR = t -> ( ( zR -s A ) x.s yR ) = ( ( zR -s A ) x.s t ) ) : No typesetting found for |- ( yR = t -> ( ( zR -s A ) x.s yR ) = ( ( zR -s A ) x.s t ) ) with typecode |-
76	75	oveq2d	Could not format ( yR = t -> ( 1s +s ( ( zR -s A ) x.s yR ) ) = ( 1s +s ( ( zR -s A ) x.s t ) ) ) : No typesetting found for |- ( yR = t -> ( 1s +s ( ( zR -s A ) x.s yR ) ) = ( 1s +s ( ( zR -s A ) x.s t ) ) ) with typecode |-
77	76	oveq1d	Could not format ( yR = t -> ( ( 1s +s ( ( zR -s A ) x.s yR ) ) /su zR ) = ( ( 1s +s ( ( zR -s A ) x.s t ) ) /su zR ) ) : No typesetting found for |- ( yR = t -> ( ( 1s +s ( ( zR -s A ) x.s yR ) ) /su zR ) = ( ( 1s +s ( ( zR -s A ) x.s t ) ) /su zR ) ) with typecode |-
78	77	eqeq2d	Could not format ( yR = t -> ( b = ( ( 1s +s ( ( zR -s A ) x.s yR ) ) /su zR ) <-> b = ( ( 1s +s ( ( zR -s A ) x.s t ) ) /su zR ) ) ) : No typesetting found for |- ( yR = t -> ( b = ( ( 1s +s ( ( zR -s A ) x.s yR ) ) /su zR ) <-> b = ( ( 1s +s ( ( zR -s A ) x.s t ) ) /su zR ) ) ) with typecode |-
79	74 78	cbvrex2vw	Could not format ( E. xR e. ( _Right ` A ) E. yR e. s b = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> E. zR e. ( _Right ` A ) E. t e. s b = ( ( 1s +s ( ( zR -s A ) x.s t ) ) /su zR ) ) : No typesetting found for |- ( E. xR e. ( _Right ` A ) E. yR e. s b = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> E. zR e. ( _Right ` A ) E. t e. s b = ( ( 1s +s ( ( zR -s A ) x.s t ) ) /su zR ) ) with typecode |-
80	70 79	bitrdi	Could not format ( a = b -> ( E. xR e. ( _Right ` A ) E. yR e. s a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> E. zR e. ( _Right ` A ) E. t e. s b = ( ( 1s +s ( ( zR -s A ) x.s t ) ) /su zR ) ) ) : No typesetting found for |- ( a = b -> ( E. xR e. ( _Right ` A ) E. yR e. s a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> E. zR e. ( _Right ` A ) E. t e. s b = ( ( 1s +s ( ( zR -s A ) x.s t ) ) /su zR ) ) ) with typecode |-
81	80	cbvabv	Could not format { a | E. xR e. ( _Right ` A ) E. yR e. s a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) } = { b | E. zR e. ( _Right ` A ) E. t e. s b = ( ( 1s +s ( ( zR -s A ) x.s t ) ) /su zR ) } : No typesetting found for |- { a | E. xR e. ( _Right ` A ) E. yR e. s a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) } = { b | E. zR e. ( _Right ` A ) E. t e. s b = ( ( 1s +s ( ( zR -s A ) x.s t ) ) /su zR ) } with typecode |-
82	68 81	uneq12i	Could not format ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
83	82	uneq2i	Could not format ( s u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
84	53 83	opeq12i	Could not format <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . = <. ( l u. ( { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . : No typesetting found for |- <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . = <. ( l u. ( { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . with typecode |-
85	17 84	eqtrdi	Could not format ( r = s -> <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . = <. ( l u. ( { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . ) : No typesetting found for |- ( r = s -> <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . = <. ( l u. ( { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . ) with typecode |-
86	85	cbvcsbv	Could not format [_ ( 2nd ` q ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . = [_ ( 2nd ` q ) / s ]_ <. ( l u. ( { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . : No typesetting found for |- [_ ( 2nd ` q ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . = [_ ( 2nd ` q ) / s ]_ <. ( l u. ( { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . with typecode |-
87	86	csbeq2i	Could not format [_ ( 1st ` q ) / l ]_ [_ ( 2nd ` q ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . = [_ ( 1st ` q ) / l ]_ [_ ( 2nd ` q ) / s ]_ <. ( l u. ( { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . : No typesetting found for |- [_ ( 1st ` q ) / l ]_ [_ ( 2nd ` q ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . = [_ ( 1st ` q ) / l ]_ [_ ( 2nd ` q ) / s ]_ <. ( l u. ( { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . with typecode |-
88		id	$$⊢l=m\to l=m$$
89		rexeq	Could not format ( l = m -> ( E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) <-> E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) ) ) : No typesetting found for |- ( l = m -> ( E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) <-> E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) ) ) with typecode |-
90	89	rexbidv	Could not format ( l = m -> ( E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) <-> E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) ) ) : No typesetting found for |- ( l = m -> ( E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) <-> E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) ) ) with typecode |-
91	90	abbidv	Could not format ( l = m -> { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } = { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } ) : No typesetting found for |- ( l = m -> { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } = { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } ) with typecode |-
92	91	uneq1d	Could not format ( l = m -> ( { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s ( { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s
93	88 92	uneq12d	Could not format ( l = m -> ( l u. ( { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s ( l u. ( { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s
94		rexeq	Could not format ( l = m -> ( E. w e. l b = ( ( 1s +s ( ( zL -s A ) x.s w ) ) /su zL ) <-> E. w e. m b = ( ( 1s +s ( ( zL -s A ) x.s w ) ) /su zL ) ) ) : No typesetting found for |- ( l = m -> ( E. w e. l b = ( ( 1s +s ( ( zL -s A ) x.s w ) ) /su zL ) <-> E. w e. m b = ( ( 1s +s ( ( zL -s A ) x.s w ) ) /su zL ) ) ) with typecode |-
95	94	rexbidv	Could not format ( l = m -> ( E. zL e. { z e. ( _Left ` A ) | 0s E. zL e. { z e. ( _Left ` A ) | 0s ( E. zL e. { z e. ( _Left ` A ) | 0s E. zL e. { z e. ( _Left ` A ) | 0s
96	95	abbidv	Could not format ( l = m -> { b | E. zL e. { z e. ( _Left ` A ) | 0s { b | E. zL e. { z e. ( _Left ` A ) | 0s
97	96	uneq1d	Could not format ( l = m -> ( { b | E. zL e. { z e. ( _Left ` A ) | 0s ( { b | E. zL e. { z e. ( _Left ` A ) | 0s
98	97	uneq2d	Could not format ( l = m -> ( s u. ( { b | E. zL e. { z e. ( _Left ` A ) | 0s ( s u. ( { b | E. zL e. { z e. ( _Left ` A ) | 0s
99	93 98	opeq12d	Could not format ( l = m -> <. ( l u. ( { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . = <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . ) : No typesetting found for |- ( l = m -> <. ( l u. ( { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . = <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . ) with typecode |-
100	99	csbeq2dv	Could not format ( l = m -> [_ ( 2nd ` q ) / s ]_ <. ( l u. ( { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . = [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . ) : No typesetting found for |- ( l = m -> [_ ( 2nd ` q ) / s ]_ <. ( l u. ( { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . = [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . ) with typecode |-
101	100	cbvcsbv	Could not format [_ ( 1st ` q ) / l ]_ [_ ( 2nd ` q ) / s ]_ <. ( l u. ( { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . = [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . : No typesetting found for |- [_ ( 1st ` q ) / l ]_ [_ ( 2nd ` q ) / s ]_ <. ( l u. ( { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . = [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . with typecode |-
102	87 101	eqtri	Could not format [_ ( 1st ` q ) / l ]_ [_ ( 2nd ` q ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . = [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . : No typesetting found for |- [_ ( 1st ` q ) / l ]_ [_ ( 2nd ` q ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . = [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . with typecode |-
103	5 102	eqtrdi	Could not format ( p = q -> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . = [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . ) : No typesetting found for |- ( p = q -> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . = [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . ) with typecode |-
104	103	cbvmptv	Could not format ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) = ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . ) : No typesetting found for |- ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) = ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . ) with typecode |-
105		rdgeq1	Could not format ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) = ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . ) -> rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. ) = rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. ) ) : No typesetting found for |- ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) = ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . ) -> rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. ) = rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. ) ) with typecode |-
106	104 105	ax-mp	Could not format rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. ) = rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. ) : No typesetting found for |- rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. ) = rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. ) with typecode |-
107	1 106	eqtri	Could not format F = rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. ) : No typesetting found for |- F = rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. ) with typecode |-