Theorem addsdilem1

Description: Lemma for surreal distribution. Expand the left hand side of the main expression. (Contributed by Scott Fenton, 8-Mar-2025)

	Ref	Expression
Hypotheses	addsdilem.1	$$⊢\phi \to A\in \mathrm{No}$$
	addsdilem.2	$$⊢\phi \to B\in \mathrm{No}$$
	addsdilem.3	$$⊢\phi \to C\in \mathrm{No}$$
Assertion	addsdilem1	Could not format assertion : No typesetting found for |- ( ph -> ( A x.s ( B +s C ) ) = ( ( ( { a | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) } ) u. ( { a | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) } ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) } ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		addsdilem.1	$$⊢\phi \to A\in \mathrm{No}$$
2		addsdilem.2	$$⊢\phi \to B\in \mathrm{No}$$
3		addsdilem.3	$$⊢\phi \to C\in \mathrm{No}$$
4		lltropt	$$⊢L\left(A\right){\ll }_{s}R\left(A\right)$$
5	4	a1i	$$⊢\phi \to L\left(A\right){\ll }_{s}R\left(A\right)$$
6	2 3	addscut2	Could not format ( ph -> ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) < ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) <
7		lrcut	$$⊢A\in \mathrm{No}\to L\left(A\right){|}_{s}R\left(A\right)=A$$
8	1 7	syl	$$⊢\phi \to L\left(A\right){|}_{s}R\left(A\right)=A$$
9	8	eqcomd	$$⊢\phi \to A=L\left(A\right){|}_{s}R\left(A\right)$$
10		addsval2	Could not format ( ( B e. No /\ C e. No ) -> ( B +s C ) = ( ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) |s ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) ) ) : No typesetting found for |- ( ( B e. No /\ C e. No ) -> ( B +s C ) = ( ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) |s ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) ) ) with typecode |-
11	2 3 10	syl2anc	Could not format ( ph -> ( B +s C ) = ( ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) |s ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) ) ) : No typesetting found for |- ( ph -> ( B +s C ) = ( ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) |s ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) ) ) with typecode |-
12	5 6 9 11	mulsunif	Could not format ( ph -> ( A x.s ( B +s C ) ) = ( ( { a | E. xL e. ( _Left ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) } u. { a | E. xR e. ( _Right ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) } ) |s ( { a | E. xL e. ( _Left ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) } u. { a | E. xR e. ( _Right ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) } ) ) ) : No typesetting found for |- ( ph -> ( A x.s ( B +s C ) ) = ( ( { a | E. xL e. ( _Left ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) } u. { a | E. xR e. ( _Right ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) } ) |s ( { a | E. xL e. ( _Left ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) } u. { a | E. xR e. ( _Right ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) } ) ) ) with typecode |-
13		unab	Could not format ( { a | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) } ) = { a | ( E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) \/ E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) } : No typesetting found for |- ( { a | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) } ) = { a | ( E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) \/ E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) } with typecode |-
14		r19.43	Could not format ( E. xL e. ( _Left ` A ) ( E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) \/ E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) <-> ( E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) \/ E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) ) : No typesetting found for |- ( E. xL e. ( _Left ` A ) ( E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) \/ E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) <-> ( E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) \/ E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) ) with typecode |-
15		rexun	Could not format ( E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> ( E. b e. { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) \/ E. b e. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) : No typesetting found for |- ( E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> ( E. b e. { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) \/ E. b e. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) with typecode |-
16		eqeq1	Could not format ( t = b -> ( t = ( yL +s C ) <-> b = ( yL +s C ) ) ) : No typesetting found for |- ( t = b -> ( t = ( yL +s C ) <-> b = ( yL +s C ) ) ) with typecode |-
17	16	rexbidv	Could not format ( t = b -> ( E. yL e. ( _Left ` B ) t = ( yL +s C ) <-> E. yL e. ( _Left ` B ) b = ( yL +s C ) ) ) : No typesetting found for |- ( t = b -> ( E. yL e. ( _Left ` B ) t = ( yL +s C ) <-> E. yL e. ( _Left ` B ) b = ( yL +s C ) ) ) with typecode |-
18	17	rexab	Could not format ( E. b e. { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> E. b ( E. yL e. ( _Left ` B ) b = ( yL +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) : No typesetting found for |- ( E. b e. { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> E. b ( E. yL e. ( _Left ` B ) b = ( yL +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) with typecode |-
19		rexcom4	Could not format ( E. yL e. ( _Left ` B ) E. b ( b = ( yL +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. b E. yL e. ( _Left ` B ) ( b = ( yL +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) : No typesetting found for |- ( E. yL e. ( _Left ` B ) E. b ( b = ( yL +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. b E. yL e. ( _Left ` B ) ( b = ( yL +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) with typecode |-
20		ovex	Could not format ( yL +s C ) e. _V : No typesetting found for |- ( yL +s C ) e. _V with typecode |-
21		oveq2	Could not format ( b = ( yL +s C ) -> ( A x.s b ) = ( A x.s ( yL +s C ) ) ) : No typesetting found for |- ( b = ( yL +s C ) -> ( A x.s b ) = ( A x.s ( yL +s C ) ) ) with typecode |-
22	21	oveq2d	Could not format ( b = ( yL +s C ) -> ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) = ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) ) : No typesetting found for |- ( b = ( yL +s C ) -> ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) = ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) ) with typecode |-
23		oveq2	Could not format ( b = ( yL +s C ) -> ( xL x.s b ) = ( xL x.s ( yL +s C ) ) ) : No typesetting found for |- ( b = ( yL +s C ) -> ( xL x.s b ) = ( xL x.s ( yL +s C ) ) ) with typecode |-
24	22 23	oveq12d	Could not format ( b = ( yL +s C ) -> ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) ) : No typesetting found for |- ( b = ( yL +s C ) -> ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) ) with typecode |-
25	24	eqeq2d	Could not format ( b = ( yL +s C ) -> ( a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) ) ) : No typesetting found for |- ( b = ( yL +s C ) -> ( a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) ) ) with typecode |-
26	20 25	ceqsexv	Could not format ( E. b ( b = ( yL +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) ) : No typesetting found for |- ( E. b ( b = ( yL +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) ) with typecode |-
27	26	rexbii	Could not format ( E. yL e. ( _Left ` B ) E. b ( b = ( yL +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) ) : No typesetting found for |- ( E. yL e. ( _Left ` B ) E. b ( b = ( yL +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) ) with typecode |-
28		r19.41v	Could not format ( E. yL e. ( _Left ` B ) ( b = ( yL +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> ( E. yL e. ( _Left ` B ) b = ( yL +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) : No typesetting found for |- ( E. yL e. ( _Left ` B ) ( b = ( yL +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> ( E. yL e. ( _Left ` B ) b = ( yL +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) with typecode |-
29	28	exbii	Could not format ( E. b E. yL e. ( _Left ` B ) ( b = ( yL +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. b ( E. yL e. ( _Left ` B ) b = ( yL +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) : No typesetting found for |- ( E. b E. yL e. ( _Left ` B ) ( b = ( yL +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. b ( E. yL e. ( _Left ` B ) b = ( yL +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) with typecode |-
30	19 27 29	3bitr3ri	Could not format ( E. b ( E. yL e. ( _Left ` B ) b = ( yL +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) ) : No typesetting found for |- ( E. b ( E. yL e. ( _Left ` B ) b = ( yL +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) ) with typecode |-
31	18 30	bitri	Could not format ( E. b e. { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) ) : No typesetting found for |- ( E. b e. { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) ) with typecode |-
32		eqeq1	Could not format ( t = b -> ( t = ( B +s zL ) <-> b = ( B +s zL ) ) ) : No typesetting found for |- ( t = b -> ( t = ( B +s zL ) <-> b = ( B +s zL ) ) ) with typecode |-
33	32	rexbidv	Could not format ( t = b -> ( E. zL e. ( _Left ` C ) t = ( B +s zL ) <-> E. zL e. ( _Left ` C ) b = ( B +s zL ) ) ) : No typesetting found for |- ( t = b -> ( E. zL e. ( _Left ` C ) t = ( B +s zL ) <-> E. zL e. ( _Left ` C ) b = ( B +s zL ) ) ) with typecode |-
34	33	rexab	Could not format ( E. b e. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> E. b ( E. zL e. ( _Left ` C ) b = ( B +s zL ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) : No typesetting found for |- ( E. b e. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> E. b ( E. zL e. ( _Left ` C ) b = ( B +s zL ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) with typecode |-
35		rexcom4	Could not format ( E. zL e. ( _Left ` C ) E. b ( b = ( B +s zL ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. b E. zL e. ( _Left ` C ) ( b = ( B +s zL ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) : No typesetting found for |- ( E. zL e. ( _Left ` C ) E. b ( b = ( B +s zL ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. b E. zL e. ( _Left ` C ) ( b = ( B +s zL ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) with typecode |-
36		ovex	Could not format ( B +s zL ) e. _V : No typesetting found for |- ( B +s zL ) e. _V with typecode |-
37		oveq2	Could not format ( b = ( B +s zL ) -> ( A x.s b ) = ( A x.s ( B +s zL ) ) ) : No typesetting found for |- ( b = ( B +s zL ) -> ( A x.s b ) = ( A x.s ( B +s zL ) ) ) with typecode |-
38	37	oveq2d	Could not format ( b = ( B +s zL ) -> ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) = ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) ) : No typesetting found for |- ( b = ( B +s zL ) -> ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) = ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) ) with typecode |-
39		oveq2	Could not format ( b = ( B +s zL ) -> ( xL x.s b ) = ( xL x.s ( B +s zL ) ) ) : No typesetting found for |- ( b = ( B +s zL ) -> ( xL x.s b ) = ( xL x.s ( B +s zL ) ) ) with typecode |-
40	38 39	oveq12d	Could not format ( b = ( B +s zL ) -> ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) : No typesetting found for |- ( b = ( B +s zL ) -> ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) with typecode |-
41	40	eqeq2d	Could not format ( b = ( B +s zL ) -> ( a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) ) : No typesetting found for |- ( b = ( B +s zL ) -> ( a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) ) with typecode |-
42	36 41	ceqsexv	Could not format ( E. b ( b = ( B +s zL ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) : No typesetting found for |- ( E. b ( b = ( B +s zL ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) with typecode |-
43	42	rexbii	Could not format ( E. zL e. ( _Left ` C ) E. b ( b = ( B +s zL ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) : No typesetting found for |- ( E. zL e. ( _Left ` C ) E. b ( b = ( B +s zL ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) with typecode |-
44		r19.41v	Could not format ( E. zL e. ( _Left ` C ) ( b = ( B +s zL ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> ( E. zL e. ( _Left ` C ) b = ( B +s zL ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) : No typesetting found for |- ( E. zL e. ( _Left ` C ) ( b = ( B +s zL ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> ( E. zL e. ( _Left ` C ) b = ( B +s zL ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) with typecode |-
45	44	exbii	Could not format ( E. b E. zL e. ( _Left ` C ) ( b = ( B +s zL ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. b ( E. zL e. ( _Left ` C ) b = ( B +s zL ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) : No typesetting found for |- ( E. b E. zL e. ( _Left ` C ) ( b = ( B +s zL ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. b ( E. zL e. ( _Left ` C ) b = ( B +s zL ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) with typecode |-
46	35 43 45	3bitr3ri	Could not format ( E. b ( E. zL e. ( _Left ` C ) b = ( B +s zL ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) : No typesetting found for |- ( E. b ( E. zL e. ( _Left ` C ) b = ( B +s zL ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) with typecode |-
47	34 46	bitri	Could not format ( E. b e. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) : No typesetting found for |- ( E. b e. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) with typecode |-
48	31 47	orbi12i	Could not format ( ( E. b e. { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) \/ E. b e. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> ( E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) \/ E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) ) : No typesetting found for |- ( ( E. b e. { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) \/ E. b e. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> ( E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) \/ E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) ) with typecode |-
49	15 48	bitr2i	Could not format ( ( E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) \/ E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) <-> E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) : No typesetting found for |- ( ( E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) \/ E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) <-> E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) with typecode |-
50	49	rexbii	Could not format ( E. xL e. ( _Left ` A ) ( E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) \/ E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) <-> E. xL e. ( _Left ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) : No typesetting found for |- ( E. xL e. ( _Left ` A ) ( E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) \/ E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) <-> E. xL e. ( _Left ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) with typecode |-
51	14 50	bitr3i	Could not format ( ( E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) \/ E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) <-> E. xL e. ( _Left ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) : No typesetting found for |- ( ( E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) \/ E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) <-> E. xL e. ( _Left ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) with typecode |-
52	51	abbii	Could not format { a | ( E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) \/ E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) } = { a | E. xL e. ( _Left ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) } : No typesetting found for |- { a | ( E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) \/ E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) ) } = { a | E. xL e. ( _Left ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) } with typecode |-
53	13 52	eqtri	Could not format ( { a | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) } ) = { a | E. xL e. ( _Left ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) } : No typesetting found for |- ( { a | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) } ) = { a | E. xL e. ( _Left ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) } with typecode |-
54		unab	Could not format ( { a | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) } ) = { a | ( E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) \/ E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) } : No typesetting found for |- ( { a | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) } ) = { a | ( E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) \/ E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) } with typecode |-
55		r19.43	Could not format ( E. xR e. ( _Right ` A ) ( E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) \/ E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) <-> ( E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) \/ E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) ) : No typesetting found for |- ( E. xR e. ( _Right ` A ) ( E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) \/ E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) <-> ( E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) \/ E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) ) with typecode |-
56		rexun	Could not format ( E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> ( E. b e. { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) \/ E. b e. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) : No typesetting found for |- ( E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> ( E. b e. { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) \/ E. b e. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) with typecode |-
57		eqeq1	Could not format ( t = b -> ( t = ( yR +s C ) <-> b = ( yR +s C ) ) ) : No typesetting found for |- ( t = b -> ( t = ( yR +s C ) <-> b = ( yR +s C ) ) ) with typecode |-
58	57	rexbidv	Could not format ( t = b -> ( E. yR e. ( _Right ` B ) t = ( yR +s C ) <-> E. yR e. ( _Right ` B ) b = ( yR +s C ) ) ) : No typesetting found for |- ( t = b -> ( E. yR e. ( _Right ` B ) t = ( yR +s C ) <-> E. yR e. ( _Right ` B ) b = ( yR +s C ) ) ) with typecode |-
59	58	rexab	Could not format ( E. b e. { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> E. b ( E. yR e. ( _Right ` B ) b = ( yR +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) : No typesetting found for |- ( E. b e. { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> E. b ( E. yR e. ( _Right ` B ) b = ( yR +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) with typecode |-
60		rexcom4	Could not format ( E. yR e. ( _Right ` B ) E. b ( b = ( yR +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. b E. yR e. ( _Right ` B ) ( b = ( yR +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) : No typesetting found for |- ( E. yR e. ( _Right ` B ) E. b ( b = ( yR +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. b E. yR e. ( _Right ` B ) ( b = ( yR +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) with typecode |-
61		ovex	Could not format ( yR +s C ) e. _V : No typesetting found for |- ( yR +s C ) e. _V with typecode |-
62		oveq2	Could not format ( b = ( yR +s C ) -> ( A x.s b ) = ( A x.s ( yR +s C ) ) ) : No typesetting found for |- ( b = ( yR +s C ) -> ( A x.s b ) = ( A x.s ( yR +s C ) ) ) with typecode |-
63	62	oveq2d	Could not format ( b = ( yR +s C ) -> ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) = ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) ) : No typesetting found for |- ( b = ( yR +s C ) -> ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) = ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) ) with typecode |-
64		oveq2	Could not format ( b = ( yR +s C ) -> ( xR x.s b ) = ( xR x.s ( yR +s C ) ) ) : No typesetting found for |- ( b = ( yR +s C ) -> ( xR x.s b ) = ( xR x.s ( yR +s C ) ) ) with typecode |-
65	63 64	oveq12d	Could not format ( b = ( yR +s C ) -> ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) ) : No typesetting found for |- ( b = ( yR +s C ) -> ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) ) with typecode |-
66	65	eqeq2d	Could not format ( b = ( yR +s C ) -> ( a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) ) ) : No typesetting found for |- ( b = ( yR +s C ) -> ( a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) ) ) with typecode |-
67	61 66	ceqsexv	Could not format ( E. b ( b = ( yR +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) ) : No typesetting found for |- ( E. b ( b = ( yR +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) ) with typecode |-
68	67	rexbii	Could not format ( E. yR e. ( _Right ` B ) E. b ( b = ( yR +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) ) : No typesetting found for |- ( E. yR e. ( _Right ` B ) E. b ( b = ( yR +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) ) with typecode |-
69		r19.41v	Could not format ( E. yR e. ( _Right ` B ) ( b = ( yR +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> ( E. yR e. ( _Right ` B ) b = ( yR +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) : No typesetting found for |- ( E. yR e. ( _Right ` B ) ( b = ( yR +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> ( E. yR e. ( _Right ` B ) b = ( yR +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) with typecode |-
70	69	exbii	Could not format ( E. b E. yR e. ( _Right ` B ) ( b = ( yR +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. b ( E. yR e. ( _Right ` B ) b = ( yR +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) : No typesetting found for |- ( E. b E. yR e. ( _Right ` B ) ( b = ( yR +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. b ( E. yR e. ( _Right ` B ) b = ( yR +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) with typecode |-
71	60 68 70	3bitr3ri	Could not format ( E. b ( E. yR e. ( _Right ` B ) b = ( yR +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) ) : No typesetting found for |- ( E. b ( E. yR e. ( _Right ` B ) b = ( yR +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) ) with typecode |-
72	59 71	bitri	Could not format ( E. b e. { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) ) : No typesetting found for |- ( E. b e. { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) ) with typecode |-
73		eqeq1	Could not format ( t = b -> ( t = ( B +s zR ) <-> b = ( B +s zR ) ) ) : No typesetting found for |- ( t = b -> ( t = ( B +s zR ) <-> b = ( B +s zR ) ) ) with typecode |-
74	73	rexbidv	Could not format ( t = b -> ( E. zR e. ( _Right ` C ) t = ( B +s zR ) <-> E. zR e. ( _Right ` C ) b = ( B +s zR ) ) ) : No typesetting found for |- ( t = b -> ( E. zR e. ( _Right ` C ) t = ( B +s zR ) <-> E. zR e. ( _Right ` C ) b = ( B +s zR ) ) ) with typecode |-
75	74	rexab	Could not format ( E. b e. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> E. b ( E. zR e. ( _Right ` C ) b = ( B +s zR ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) : No typesetting found for |- ( E. b e. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> E. b ( E. zR e. ( _Right ` C ) b = ( B +s zR ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) with typecode |-
76		rexcom4	Could not format ( E. zR e. ( _Right ` C ) E. b ( b = ( B +s zR ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. b E. zR e. ( _Right ` C ) ( b = ( B +s zR ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) : No typesetting found for |- ( E. zR e. ( _Right ` C ) E. b ( b = ( B +s zR ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. b E. zR e. ( _Right ` C ) ( b = ( B +s zR ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) with typecode |-
77		ovex	Could not format ( B +s zR ) e. _V : No typesetting found for |- ( B +s zR ) e. _V with typecode |-
78		oveq2	Could not format ( b = ( B +s zR ) -> ( A x.s b ) = ( A x.s ( B +s zR ) ) ) : No typesetting found for |- ( b = ( B +s zR ) -> ( A x.s b ) = ( A x.s ( B +s zR ) ) ) with typecode |-
79	78	oveq2d	Could not format ( b = ( B +s zR ) -> ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) = ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) ) : No typesetting found for |- ( b = ( B +s zR ) -> ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) = ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) ) with typecode |-
80		oveq2	Could not format ( b = ( B +s zR ) -> ( xR x.s b ) = ( xR x.s ( B +s zR ) ) ) : No typesetting found for |- ( b = ( B +s zR ) -> ( xR x.s b ) = ( xR x.s ( B +s zR ) ) ) with typecode |-
81	79 80	oveq12d	Could not format ( b = ( B +s zR ) -> ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) : No typesetting found for |- ( b = ( B +s zR ) -> ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) with typecode |-
82	81	eqeq2d	Could not format ( b = ( B +s zR ) -> ( a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) ) : No typesetting found for |- ( b = ( B +s zR ) -> ( a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) ) with typecode |-
83	77 82	ceqsexv	Could not format ( E. b ( b = ( B +s zR ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) : No typesetting found for |- ( E. b ( b = ( B +s zR ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) with typecode |-
84	83	rexbii	Could not format ( E. zR e. ( _Right ` C ) E. b ( b = ( B +s zR ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) : No typesetting found for |- ( E. zR e. ( _Right ` C ) E. b ( b = ( B +s zR ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) with typecode |-
85		r19.41v	Could not format ( E. zR e. ( _Right ` C ) ( b = ( B +s zR ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> ( E. zR e. ( _Right ` C ) b = ( B +s zR ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) : No typesetting found for |- ( E. zR e. ( _Right ` C ) ( b = ( B +s zR ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> ( E. zR e. ( _Right ` C ) b = ( B +s zR ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) with typecode |-
86	85	exbii	Could not format ( E. b E. zR e. ( _Right ` C ) ( b = ( B +s zR ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. b ( E. zR e. ( _Right ` C ) b = ( B +s zR ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) : No typesetting found for |- ( E. b E. zR e. ( _Right ` C ) ( b = ( B +s zR ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. b ( E. zR e. ( _Right ` C ) b = ( B +s zR ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) with typecode |-
87	76 84 86	3bitr3ri	Could not format ( E. b ( E. zR e. ( _Right ` C ) b = ( B +s zR ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) : No typesetting found for |- ( E. b ( E. zR e. ( _Right ` C ) b = ( B +s zR ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) with typecode |-
88	75 87	bitri	Could not format ( E. b e. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) : No typesetting found for |- ( E. b e. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) with typecode |-
89	72 88	orbi12i	Could not format ( ( E. b e. { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) \/ E. b e. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> ( E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) \/ E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) ) : No typesetting found for |- ( ( E. b e. { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) \/ E. b e. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> ( E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) \/ E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) ) with typecode |-
90	56 89	bitr2i	Could not format ( ( E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) \/ E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) <-> E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) : No typesetting found for |- ( ( E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) \/ E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) <-> E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) with typecode |-
91	90	rexbii	Could not format ( E. xR e. ( _Right ` A ) ( E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) \/ E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) <-> E. xR e. ( _Right ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) : No typesetting found for |- ( E. xR e. ( _Right ` A ) ( E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) \/ E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) <-> E. xR e. ( _Right ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) with typecode |-
92	55 91	bitr3i	Could not format ( ( E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) \/ E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) <-> E. xR e. ( _Right ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) : No typesetting found for |- ( ( E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) \/ E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) <-> E. xR e. ( _Right ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) with typecode |-
93	92	abbii	Could not format { a | ( E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) \/ E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) } = { a | E. xR e. ( _Right ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) } : No typesetting found for |- { a | ( E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) \/ E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) ) } = { a | E. xR e. ( _Right ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) } with typecode |-
94	54 93	eqtri	Could not format ( { a | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) } ) = { a | E. xR e. ( _Right ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) } : No typesetting found for |- ( { a | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) } ) = { a | E. xR e. ( _Right ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) } with typecode |-
95	53 94	uneq12i	Could not format ( ( { a | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) } ) u. ( { a | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) } ) ) = ( { a | E. xL e. ( _Left ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) } u. { a | E. xR e. ( _Right ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) } ) : No typesetting found for |- ( ( { a | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) } ) u. ( { a | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) } ) ) = ( { a | E. xL e. ( _Left ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) } u. { a | E. xR e. ( _Right ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) } ) with typecode |-
96		unab	Could not format ( { a | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) } ) = { a | ( E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) \/ E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) } : No typesetting found for |- ( { a | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) } ) = { a | ( E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) \/ E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) } with typecode |-
97		r19.43	Could not format ( E. xL e. ( _Left ` A ) ( E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) \/ E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) <-> ( E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) \/ E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) ) : No typesetting found for |- ( E. xL e. ( _Left ` A ) ( E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) \/ E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) <-> ( E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) \/ E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) ) with typecode |-
98		rexun	Could not format ( E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> ( E. b e. { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) \/ E. b e. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) : No typesetting found for |- ( E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> ( E. b e. { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) \/ E. b e. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) with typecode |-
99	58	rexab	Could not format ( E. b e. { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> E. b ( E. yR e. ( _Right ` B ) b = ( yR +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) : No typesetting found for |- ( E. b e. { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> E. b ( E. yR e. ( _Right ` B ) b = ( yR +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) with typecode |-
100		rexcom4	Could not format ( E. yR e. ( _Right ` B ) E. b ( b = ( yR +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. b E. yR e. ( _Right ` B ) ( b = ( yR +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) : No typesetting found for |- ( E. yR e. ( _Right ` B ) E. b ( b = ( yR +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. b E. yR e. ( _Right ` B ) ( b = ( yR +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) with typecode |-
101	62	oveq2d	Could not format ( b = ( yR +s C ) -> ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) = ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) ) : No typesetting found for |- ( b = ( yR +s C ) -> ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) = ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) ) with typecode |-
102		oveq2	Could not format ( b = ( yR +s C ) -> ( xL x.s b ) = ( xL x.s ( yR +s C ) ) ) : No typesetting found for |- ( b = ( yR +s C ) -> ( xL x.s b ) = ( xL x.s ( yR +s C ) ) ) with typecode |-
103	101 102	oveq12d	Could not format ( b = ( yR +s C ) -> ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) ) : No typesetting found for |- ( b = ( yR +s C ) -> ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) ) with typecode |-
104	103	eqeq2d	Could not format ( b = ( yR +s C ) -> ( a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) ) ) : No typesetting found for |- ( b = ( yR +s C ) -> ( a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) ) ) with typecode |-
105	61 104	ceqsexv	Could not format ( E. b ( b = ( yR +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) ) : No typesetting found for |- ( E. b ( b = ( yR +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) ) with typecode |-
106	105	rexbii	Could not format ( E. yR e. ( _Right ` B ) E. b ( b = ( yR +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) ) : No typesetting found for |- ( E. yR e. ( _Right ` B ) E. b ( b = ( yR +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) ) with typecode |-
107		r19.41v	Could not format ( E. yR e. ( _Right ` B ) ( b = ( yR +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> ( E. yR e. ( _Right ` B ) b = ( yR +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) : No typesetting found for |- ( E. yR e. ( _Right ` B ) ( b = ( yR +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> ( E. yR e. ( _Right ` B ) b = ( yR +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) with typecode |-
108	107	exbii	Could not format ( E. b E. yR e. ( _Right ` B ) ( b = ( yR +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. b ( E. yR e. ( _Right ` B ) b = ( yR +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) : No typesetting found for |- ( E. b E. yR e. ( _Right ` B ) ( b = ( yR +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. b ( E. yR e. ( _Right ` B ) b = ( yR +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) with typecode |-
109	100 106 108	3bitr3ri	Could not format ( E. b ( E. yR e. ( _Right ` B ) b = ( yR +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) ) : No typesetting found for |- ( E. b ( E. yR e. ( _Right ` B ) b = ( yR +s C ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) ) with typecode |-
110	99 109	bitri	Could not format ( E. b e. { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) ) : No typesetting found for |- ( E. b e. { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) ) with typecode |-
111	74	rexab	Could not format ( E. b e. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> E. b ( E. zR e. ( _Right ` C ) b = ( B +s zR ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) : No typesetting found for |- ( E. b e. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> E. b ( E. zR e. ( _Right ` C ) b = ( B +s zR ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) with typecode |-
112		rexcom4	Could not format ( E. zR e. ( _Right ` C ) E. b ( b = ( B +s zR ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. b E. zR e. ( _Right ` C ) ( b = ( B +s zR ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) : No typesetting found for |- ( E. zR e. ( _Right ` C ) E. b ( b = ( B +s zR ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. b E. zR e. ( _Right ` C ) ( b = ( B +s zR ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) with typecode |-
113	78	oveq2d	Could not format ( b = ( B +s zR ) -> ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) = ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) ) : No typesetting found for |- ( b = ( B +s zR ) -> ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) = ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) ) with typecode |-
114		oveq2	Could not format ( b = ( B +s zR ) -> ( xL x.s b ) = ( xL x.s ( B +s zR ) ) ) : No typesetting found for |- ( b = ( B +s zR ) -> ( xL x.s b ) = ( xL x.s ( B +s zR ) ) ) with typecode |-
115	113 114	oveq12d	Could not format ( b = ( B +s zR ) -> ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) : No typesetting found for |- ( b = ( B +s zR ) -> ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) with typecode |-
116	115	eqeq2d	Could not format ( b = ( B +s zR ) -> ( a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) ) : No typesetting found for |- ( b = ( B +s zR ) -> ( a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) ) with typecode |-
117	77 116	ceqsexv	Could not format ( E. b ( b = ( B +s zR ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) : No typesetting found for |- ( E. b ( b = ( B +s zR ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) with typecode |-
118	117	rexbii	Could not format ( E. zR e. ( _Right ` C ) E. b ( b = ( B +s zR ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) : No typesetting found for |- ( E. zR e. ( _Right ` C ) E. b ( b = ( B +s zR ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) with typecode |-
119		r19.41v	Could not format ( E. zR e. ( _Right ` C ) ( b = ( B +s zR ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> ( E. zR e. ( _Right ` C ) b = ( B +s zR ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) : No typesetting found for |- ( E. zR e. ( _Right ` C ) ( b = ( B +s zR ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> ( E. zR e. ( _Right ` C ) b = ( B +s zR ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) with typecode |-
120	119	exbii	Could not format ( E. b E. zR e. ( _Right ` C ) ( b = ( B +s zR ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. b ( E. zR e. ( _Right ` C ) b = ( B +s zR ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) : No typesetting found for |- ( E. b E. zR e. ( _Right ` C ) ( b = ( B +s zR ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. b ( E. zR e. ( _Right ` C ) b = ( B +s zR ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) ) with typecode |-
121	112 118 120	3bitr3ri	Could not format ( E. b ( E. zR e. ( _Right ` C ) b = ( B +s zR ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) : No typesetting found for |- ( E. b ( E. zR e. ( _Right ` C ) b = ( B +s zR ) /\ a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) with typecode |-
122	111 121	bitri	Could not format ( E. b e. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) : No typesetting found for |- ( E. b e. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) <-> E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) with typecode |-
123	110 122	orbi12i	Could not format ( ( E. b e. { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) \/ E. b e. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> ( E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) \/ E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) ) : No typesetting found for |- ( ( E. b e. { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) \/ E. b e. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) <-> ( E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) \/ E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) ) with typecode |-
124	98 123	bitr2i	Could not format ( ( E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) \/ E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) <-> E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) : No typesetting found for |- ( ( E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) \/ E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) <-> E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) with typecode |-
125	124	rexbii	Could not format ( E. xL e. ( _Left ` A ) ( E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) \/ E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) <-> E. xL e. ( _Left ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) : No typesetting found for |- ( E. xL e. ( _Left ` A ) ( E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) \/ E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) <-> E. xL e. ( _Left ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) with typecode |-
126	97 125	bitr3i	Could not format ( ( E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) \/ E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) <-> E. xL e. ( _Left ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) : No typesetting found for |- ( ( E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) \/ E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) <-> E. xL e. ( _Left ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) ) with typecode |-
127	126	abbii	Could not format { a | ( E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) \/ E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) } = { a | E. xL e. ( _Left ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) } : No typesetting found for |- { a | ( E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) \/ E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) ) } = { a | E. xL e. ( _Left ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) } with typecode |-
128	96 127	eqtri	Could not format ( { a | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) } ) = { a | E. xL e. ( _Left ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) } : No typesetting found for |- ( { a | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) } ) = { a | E. xL e. ( _Left ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) } with typecode |-
129		unab	Could not format ( { a | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) } ) = { a | ( E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) \/ E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) } : No typesetting found for |- ( { a | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) } ) = { a | ( E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) \/ E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) } with typecode |-
130		r19.43	Could not format ( E. xR e. ( _Right ` A ) ( E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) \/ E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) <-> ( E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) \/ E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) ) : No typesetting found for |- ( E. xR e. ( _Right ` A ) ( E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) \/ E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) <-> ( E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) \/ E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) ) with typecode |-
131		rexun	Could not format ( E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> ( E. b e. { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) \/ E. b e. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) : No typesetting found for |- ( E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> ( E. b e. { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) \/ E. b e. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) with typecode |-
132	17	rexab	Could not format ( E. b e. { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> E. b ( E. yL e. ( _Left ` B ) b = ( yL +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) : No typesetting found for |- ( E. b e. { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> E. b ( E. yL e. ( _Left ` B ) b = ( yL +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) with typecode |-
133		rexcom4	Could not format ( E. yL e. ( _Left ` B ) E. b ( b = ( yL +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. b E. yL e. ( _Left ` B ) ( b = ( yL +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) : No typesetting found for |- ( E. yL e. ( _Left ` B ) E. b ( b = ( yL +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. b E. yL e. ( _Left ` B ) ( b = ( yL +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) with typecode |-
134	21	oveq2d	Could not format ( b = ( yL +s C ) -> ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) = ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) ) : No typesetting found for |- ( b = ( yL +s C ) -> ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) = ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) ) with typecode |-
135		oveq2	Could not format ( b = ( yL +s C ) -> ( xR x.s b ) = ( xR x.s ( yL +s C ) ) ) : No typesetting found for |- ( b = ( yL +s C ) -> ( xR x.s b ) = ( xR x.s ( yL +s C ) ) ) with typecode |-
136	134 135	oveq12d	Could not format ( b = ( yL +s C ) -> ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) ) : No typesetting found for |- ( b = ( yL +s C ) -> ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) ) with typecode |-
137	136	eqeq2d	Could not format ( b = ( yL +s C ) -> ( a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) ) ) : No typesetting found for |- ( b = ( yL +s C ) -> ( a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) ) ) with typecode |-
138	20 137	ceqsexv	Could not format ( E. b ( b = ( yL +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) ) : No typesetting found for |- ( E. b ( b = ( yL +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) ) with typecode |-
139	138	rexbii	Could not format ( E. yL e. ( _Left ` B ) E. b ( b = ( yL +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) ) : No typesetting found for |- ( E. yL e. ( _Left ` B ) E. b ( b = ( yL +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) ) with typecode |-
140		r19.41v	Could not format ( E. yL e. ( _Left ` B ) ( b = ( yL +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> ( E. yL e. ( _Left ` B ) b = ( yL +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) : No typesetting found for |- ( E. yL e. ( _Left ` B ) ( b = ( yL +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> ( E. yL e. ( _Left ` B ) b = ( yL +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) with typecode |-
141	140	exbii	Could not format ( E. b E. yL e. ( _Left ` B ) ( b = ( yL +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. b ( E. yL e. ( _Left ` B ) b = ( yL +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) : No typesetting found for |- ( E. b E. yL e. ( _Left ` B ) ( b = ( yL +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. b ( E. yL e. ( _Left ` B ) b = ( yL +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) with typecode |-
142	133 139 141	3bitr3ri	Could not format ( E. b ( E. yL e. ( _Left ` B ) b = ( yL +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) ) : No typesetting found for |- ( E. b ( E. yL e. ( _Left ` B ) b = ( yL +s C ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) ) with typecode |-
143	132 142	bitri	Could not format ( E. b e. { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) ) : No typesetting found for |- ( E. b e. { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) ) with typecode |-
144	33	rexab	Could not format ( E. b e. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> E. b ( E. zL e. ( _Left ` C ) b = ( B +s zL ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) : No typesetting found for |- ( E. b e. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> E. b ( E. zL e. ( _Left ` C ) b = ( B +s zL ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) with typecode |-
145		rexcom4	Could not format ( E. zL e. ( _Left ` C ) E. b ( b = ( B +s zL ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. b E. zL e. ( _Left ` C ) ( b = ( B +s zL ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) : No typesetting found for |- ( E. zL e. ( _Left ` C ) E. b ( b = ( B +s zL ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. b E. zL e. ( _Left ` C ) ( b = ( B +s zL ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) with typecode |-
146	37	oveq2d	Could not format ( b = ( B +s zL ) -> ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) = ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) ) : No typesetting found for |- ( b = ( B +s zL ) -> ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) = ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) ) with typecode |-
147		oveq2	Could not format ( b = ( B +s zL ) -> ( xR x.s b ) = ( xR x.s ( B +s zL ) ) ) : No typesetting found for |- ( b = ( B +s zL ) -> ( xR x.s b ) = ( xR x.s ( B +s zL ) ) ) with typecode |-
148	146 147	oveq12d	Could not format ( b = ( B +s zL ) -> ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) : No typesetting found for |- ( b = ( B +s zL ) -> ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) with typecode |-
149	148	eqeq2d	Could not format ( b = ( B +s zL ) -> ( a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) ) : No typesetting found for |- ( b = ( B +s zL ) -> ( a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) ) with typecode |-
150	36 149	ceqsexv	Could not format ( E. b ( b = ( B +s zL ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) : No typesetting found for |- ( E. b ( b = ( B +s zL ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) with typecode |-
151	150	rexbii	Could not format ( E. zL e. ( _Left ` C ) E. b ( b = ( B +s zL ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) : No typesetting found for |- ( E. zL e. ( _Left ` C ) E. b ( b = ( B +s zL ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) with typecode |-
152		r19.41v	Could not format ( E. zL e. ( _Left ` C ) ( b = ( B +s zL ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> ( E. zL e. ( _Left ` C ) b = ( B +s zL ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) : No typesetting found for |- ( E. zL e. ( _Left ` C ) ( b = ( B +s zL ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> ( E. zL e. ( _Left ` C ) b = ( B +s zL ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) with typecode |-
153	152	exbii	Could not format ( E. b E. zL e. ( _Left ` C ) ( b = ( B +s zL ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. b ( E. zL e. ( _Left ` C ) b = ( B +s zL ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) : No typesetting found for |- ( E. b E. zL e. ( _Left ` C ) ( b = ( B +s zL ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. b ( E. zL e. ( _Left ` C ) b = ( B +s zL ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) ) with typecode |-
154	145 151 153	3bitr3ri	Could not format ( E. b ( E. zL e. ( _Left ` C ) b = ( B +s zL ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) : No typesetting found for |- ( E. b ( E. zL e. ( _Left ` C ) b = ( B +s zL ) /\ a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) with typecode |-
155	144 154	bitri	Could not format ( E. b e. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) : No typesetting found for |- ( E. b e. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) <-> E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) with typecode |-
156	143 155	orbi12i	Could not format ( ( E. b e. { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) \/ E. b e. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> ( E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) \/ E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) ) : No typesetting found for |- ( ( E. b e. { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) \/ E. b e. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) <-> ( E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) \/ E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) ) with typecode |-
157	131 156	bitr2i	Could not format ( ( E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) \/ E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) <-> E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) : No typesetting found for |- ( ( E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) \/ E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) <-> E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) with typecode |-
158	157	rexbii	Could not format ( E. xR e. ( _Right ` A ) ( E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) \/ E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) <-> E. xR e. ( _Right ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) : No typesetting found for |- ( E. xR e. ( _Right ` A ) ( E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) \/ E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) <-> E. xR e. ( _Right ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) with typecode |-
159	130 158	bitr3i	Could not format ( ( E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) \/ E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) <-> E. xR e. ( _Right ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) : No typesetting found for |- ( ( E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) \/ E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) <-> E. xR e. ( _Right ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) ) with typecode |-
160	159	abbii	Could not format { a | ( E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) \/ E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) } = { a | E. xR e. ( _Right ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) } : No typesetting found for |- { a | ( E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) \/ E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) ) } = { a | E. xR e. ( _Right ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) } with typecode |-
161	129 160	eqtri	Could not format ( { a | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) } ) = { a | E. xR e. ( _Right ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) } : No typesetting found for |- ( { a | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) } ) = { a | E. xR e. ( _Right ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) } with typecode |-
162	128 161	uneq12i	Could not format ( ( { a | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) } ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) } ) ) = ( { a | E. xL e. ( _Left ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) } u. { a | E. xR e. ( _Right ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) } ) : No typesetting found for |- ( ( { a | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) } ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) } ) ) = ( { a | E. xL e. ( _Left ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) } u. { a | E. xR e. ( _Right ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) } ) with typecode |-
163	95 162	oveq12i	Could not format ( ( ( { a | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) } ) u. ( { a | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) } ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) } ) ) ) = ( ( { a | E. xL e. ( _Left ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) } u. { a | E. xR e. ( _Right ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) } ) |s ( { a | E. xL e. ( _Left ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) } u. { a | E. xR e. ( _Right ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) } ) ) : No typesetting found for |- ( ( ( { a | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) } ) u. ( { a | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) } ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) } ) ) ) = ( ( { a | E. xL e. ( _Left ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) } u. { a | E. xR e. ( _Right ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) } ) |s ( { a | E. xL e. ( _Left ` A ) E. b e. ( { t | E. yR e. ( _Right ` B ) t = ( yR +s C ) } u. { t | E. zR e. ( _Right ` C ) t = ( B +s zR ) } ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xL x.s b ) ) } u. { a | E. xR e. ( _Right ` A ) E. b e. ( { t | E. yL e. ( _Left ` B ) t = ( yL +s C ) } u. { t | E. zL e. ( _Left ` C ) t = ( B +s zL ) } ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s b ) ) -s ( xR x.s b ) ) } ) ) with typecode |-
164	12 163	eqtr4di	Could not format ( ph -> ( A x.s ( B +s C ) ) = ( ( ( { a | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) } ) u. ( { a | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) } ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) } ) ) ) ) : No typesetting found for |- ( ph -> ( A x.s ( B +s C ) ) = ( ( ( { a | E. xL e. ( _Left ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xL x.s ( yL +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xL x.s ( B +s zL ) ) ) } ) u. ( { a | E. xR e. ( _Right ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xR x.s ( yR +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xR x.s ( B +s zR ) ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` A ) E. yR e. ( _Right ` B ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( yR +s C ) ) ) -s ( xL x.s ( yR +s C ) ) ) } u. { a | E. xL e. ( _Left ` A ) E. zR e. ( _Right ` C ) a = ( ( ( xL x.s ( B +s C ) ) +s ( A x.s ( B +s zR ) ) ) -s ( xL x.s ( B +s zR ) ) ) } ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( _Left ` B ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( yL +s C ) ) ) -s ( xR x.s ( yL +s C ) ) ) } u. { a | E. xR e. ( _Right ` A ) E. zL e. ( _Left ` C ) a = ( ( ( xR x.s ( B +s C ) ) +s ( A x.s ( B +s zL ) ) ) -s ( xR x.s ( B +s zL ) ) ) } ) ) ) ) with typecode |-