Theorem addsdilem2

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