Theorem addsdi

Description: Distributive law for surreal numbers. Commuted form of part of theorem 7 of Conway p. 19. (Contributed by Scott Fenton, 9-Mar-2025)

	Ref	Expression
Assertion	addsdi	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge C\in \mathrm{No}\right)\to A{\cdot }_s\left(B{+}_{s}C\right)=\left(A{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}C\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	Could not format ( x = xO -> ( x x.s ( y +s z ) ) = ( xO x.s ( y +s z ) ) ) : No typesetting found for |- ( x = xO -> ( x x.s ( y +s z ) ) = ( xO x.s ( y +s z ) ) ) with typecode |-
2		oveq1	Could not format ( x = xO -> ( x x.s y ) = ( xO x.s y ) ) : No typesetting found for |- ( x = xO -> ( x x.s y ) = ( xO x.s y ) ) with typecode |-
3		oveq1	Could not format ( x = xO -> ( x x.s z ) = ( xO x.s z ) ) : No typesetting found for |- ( x = xO -> ( x x.s z ) = ( xO x.s z ) ) with typecode |-
4	2 3	oveq12d	Could not format ( x = xO -> ( ( x x.s y ) +s ( x x.s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) ) : No typesetting found for |- ( x = xO -> ( ( x x.s y ) +s ( x x.s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) ) with typecode |-
5	1 4	eqeq12d	Could not format ( x = xO -> ( ( x x.s ( y +s z ) ) = ( ( x x.s y ) +s ( x x.s z ) ) <-> ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) ) ) : No typesetting found for |- ( x = xO -> ( ( x x.s ( y +s z ) ) = ( ( x x.s y ) +s ( x x.s z ) ) <-> ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) ) ) with typecode |-
6		oveq1	Could not format ( y = yO -> ( y +s z ) = ( yO +s z ) ) : No typesetting found for |- ( y = yO -> ( y +s z ) = ( yO +s z ) ) with typecode |-
7	6	oveq2d	Could not format ( y = yO -> ( xO x.s ( y +s z ) ) = ( xO x.s ( yO +s z ) ) ) : No typesetting found for |- ( y = yO -> ( xO x.s ( y +s z ) ) = ( xO x.s ( yO +s z ) ) ) with typecode |-
8		oveq2	Could not format ( y = yO -> ( xO x.s y ) = ( xO x.s yO ) ) : No typesetting found for |- ( y = yO -> ( xO x.s y ) = ( xO x.s yO ) ) with typecode |-
9	8	oveq1d	Could not format ( y = yO -> ( ( xO x.s y ) +s ( xO x.s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) ) : No typesetting found for |- ( y = yO -> ( ( xO x.s y ) +s ( xO x.s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) ) with typecode |-
10	7 9	eqeq12d	Could not format ( y = yO -> ( ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) <-> ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) ) ) : No typesetting found for |- ( y = yO -> ( ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) <-> ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) ) ) with typecode |-
11		oveq2	Could not format ( z = zO -> ( yO +s z ) = ( yO +s zO ) ) : No typesetting found for |- ( z = zO -> ( yO +s z ) = ( yO +s zO ) ) with typecode |-
12	11	oveq2d	Could not format ( z = zO -> ( xO x.s ( yO +s z ) ) = ( xO x.s ( yO +s zO ) ) ) : No typesetting found for |- ( z = zO -> ( xO x.s ( yO +s z ) ) = ( xO x.s ( yO +s zO ) ) ) with typecode |-
13		oveq2	Could not format ( z = zO -> ( xO x.s z ) = ( xO x.s zO ) ) : No typesetting found for |- ( z = zO -> ( xO x.s z ) = ( xO x.s zO ) ) with typecode |-
14	13	oveq2d	Could not format ( z = zO -> ( ( xO x.s yO ) +s ( xO x.s z ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) ) : No typesetting found for |- ( z = zO -> ( ( xO x.s yO ) +s ( xO x.s z ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) ) with typecode |-
15	12 14	eqeq12d	Could not format ( z = zO -> ( ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) <-> ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) ) ) : No typesetting found for |- ( z = zO -> ( ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) <-> ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) ) ) with typecode |-
16		oveq1	Could not format ( x = xO -> ( x x.s ( yO +s zO ) ) = ( xO x.s ( yO +s zO ) ) ) : No typesetting found for |- ( x = xO -> ( x x.s ( yO +s zO ) ) = ( xO x.s ( yO +s zO ) ) ) with typecode |-
17		oveq1	Could not format ( x = xO -> ( x x.s yO ) = ( xO x.s yO ) ) : No typesetting found for |- ( x = xO -> ( x x.s yO ) = ( xO x.s yO ) ) with typecode |-
18		oveq1	Could not format ( x = xO -> ( x x.s zO ) = ( xO x.s zO ) ) : No typesetting found for |- ( x = xO -> ( x x.s zO ) = ( xO x.s zO ) ) with typecode |-
19	17 18	oveq12d	Could not format ( x = xO -> ( ( x x.s yO ) +s ( x x.s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) ) : No typesetting found for |- ( x = xO -> ( ( x x.s yO ) +s ( x x.s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) ) with typecode |-
20	16 19	eqeq12d	Could not format ( x = xO -> ( ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) <-> ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) ) ) : No typesetting found for |- ( x = xO -> ( ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) <-> ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) ) ) with typecode |-
21		oveq1	Could not format ( y = yO -> ( y +s zO ) = ( yO +s zO ) ) : No typesetting found for |- ( y = yO -> ( y +s zO ) = ( yO +s zO ) ) with typecode |-
22	21	oveq2d	Could not format ( y = yO -> ( x x.s ( y +s zO ) ) = ( x x.s ( yO +s zO ) ) ) : No typesetting found for |- ( y = yO -> ( x x.s ( y +s zO ) ) = ( x x.s ( yO +s zO ) ) ) with typecode |-
23		oveq2	Could not format ( y = yO -> ( x x.s y ) = ( x x.s yO ) ) : No typesetting found for |- ( y = yO -> ( x x.s y ) = ( x x.s yO ) ) with typecode |-
24	23	oveq1d	Could not format ( y = yO -> ( ( x x.s y ) +s ( x x.s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) ) : No typesetting found for |- ( y = yO -> ( ( x x.s y ) +s ( x x.s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) ) with typecode |-
25	22 24	eqeq12d	Could not format ( y = yO -> ( ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) <-> ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) ) ) : No typesetting found for |- ( y = yO -> ( ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) <-> ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) ) ) with typecode |-
26	21	oveq2d	Could not format ( y = yO -> ( xO x.s ( y +s zO ) ) = ( xO x.s ( yO +s zO ) ) ) : No typesetting found for |- ( y = yO -> ( xO x.s ( y +s zO ) ) = ( xO x.s ( yO +s zO ) ) ) with typecode |-
27	8	oveq1d	Could not format ( y = yO -> ( ( xO x.s y ) +s ( xO x.s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) ) : No typesetting found for |- ( y = yO -> ( ( xO x.s y ) +s ( xO x.s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) ) with typecode |-
28	26 27	eqeq12d	Could not format ( y = yO -> ( ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) <-> ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) ) ) : No typesetting found for |- ( y = yO -> ( ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) <-> ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) ) ) with typecode |-
29	11	oveq2d	Could not format ( z = zO -> ( x x.s ( yO +s z ) ) = ( x x.s ( yO +s zO ) ) ) : No typesetting found for |- ( z = zO -> ( x x.s ( yO +s z ) ) = ( x x.s ( yO +s zO ) ) ) with typecode |-
30		oveq2	Could not format ( z = zO -> ( x x.s z ) = ( x x.s zO ) ) : No typesetting found for |- ( z = zO -> ( x x.s z ) = ( x x.s zO ) ) with typecode |-
31	30	oveq2d	Could not format ( z = zO -> ( ( x x.s yO ) +s ( x x.s z ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) ) : No typesetting found for |- ( z = zO -> ( ( x x.s yO ) +s ( x x.s z ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) ) with typecode |-
32	29 31	eqeq12d	Could not format ( z = zO -> ( ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) <-> ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) ) ) : No typesetting found for |- ( z = zO -> ( ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) <-> ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) ) ) with typecode |-
33		oveq1	$$⊢x=A\to x{\cdot }_s\left(y{+}_{s}z\right)=A{\cdot }_s\left(y{+}_{s}z\right)$$
34		oveq1	$$⊢x=A\to x{\cdot }_{s}y=A{\cdot }_{s}y$$
35		oveq1	$$⊢x=A\to x{\cdot }_{s}z=A{\cdot }_{s}z$$
36	34 35	oveq12d	$$⊢x=A\to \left(x{\cdot }_{s}y\right){+}_s\left(x{\cdot }_{s}z\right)=\left(A{\cdot }_{s}y\right){+}_s\left(A{\cdot }_{s}z\right)$$
37	33 36	eqeq12d	$$⊢x=A\to \left(x{\cdot }_s\left(y{+}_{s}z\right)=\left(x{\cdot }_{s}y\right){+}_s\left(x{\cdot }_{s}z\right)\leftrightarrow A{\cdot }_s\left(y{+}_{s}z\right)=\left(A{\cdot }_{s}y\right){+}_s\left(A{\cdot }_{s}z\right)\right)$$
38		oveq1	$$⊢y=B\to y{+}_{s}z=B{+}_{s}z$$
39	38	oveq2d	$$⊢y=B\to A{\cdot }_s\left(y{+}_{s}z\right)=A{\cdot }_s\left(B{+}_{s}z\right)$$
40		oveq2	$$⊢y=B\to A{\cdot }_{s}y=A{\cdot }_{s}B$$
41	40	oveq1d	$$⊢y=B\to \left(A{\cdot }_{s}y\right){+}_s\left(A{\cdot }_{s}z\right)=\left(A{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}z\right)$$
42	39 41	eqeq12d	$$⊢y=B\to \left(A{\cdot }_s\left(y{+}_{s}z\right)=\left(A{\cdot }_{s}y\right){+}_s\left(A{\cdot }_{s}z\right)\leftrightarrow A{\cdot }_s\left(B{+}_{s}z\right)=\left(A{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}z\right)\right)$$
43		oveq2	$$⊢z=C\to B{+}_{s}z=B{+}_{s}C$$
44	43	oveq2d	$$⊢z=C\to A{\cdot }_s\left(B{+}_{s}z\right)=A{\cdot }_s\left(B{+}_{s}C\right)$$
45		oveq2	$$⊢z=C\to A{\cdot }_{s}z=A{\cdot }_{s}C$$
46	45	oveq2d	$$⊢z=C\to \left(A{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}z\right)=\left(A{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}C\right)$$
47	44 46	eqeq12d	$$⊢z=C\to \left(A{\cdot }_s\left(B{+}_{s}z\right)=\left(A{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}z\right)\leftrightarrow A{\cdot }_s\left(B{+}_{s}C\right)=\left(A{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}C\right)\right)$$
48		simpl1	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> x e. No ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> x e. No ) with typecode |-
49		simpl2	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> y e. No ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> y e. No ) with typecode |-
50		simpl3	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> z e. No ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> z e. No ) with typecode |-
51		simpr21	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) ) with typecode |-
52		simpr23	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) with typecode |-
53		simpr12	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) ) with typecode |-
54		elun1	Could not format ( xL e. ( _Left ` x ) -> xL e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) : No typesetting found for |- ( xL e. ( _Left ` x ) -> xL e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) with typecode |-
55	54	adantr	Could not format ( ( xL e. ( _Left ` x ) /\ yL e. ( _Left ` y ) ) -> xL e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) : No typesetting found for |- ( ( xL e. ( _Left ` x ) /\ yL e. ( _Left ` y ) ) -> xL e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) with typecode |-
56		elun1	Could not format ( yL e. ( _Left ` y ) -> yL e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) : No typesetting found for |- ( yL e. ( _Left ` y ) -> yL e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) with typecode |-
57	56	adantl	Could not format ( ( xL e. ( _Left ` x ) /\ yL e. ( _Left ` y ) ) -> yL e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) : No typesetting found for |- ( ( xL e. ( _Left ` x ) /\ yL e. ( _Left ` y ) ) -> yL e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) with typecode |-
58	48 49 50 51 52 53 55 57	addsdilem3	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xL e. ( _Left ` x ) /\ yL e. ( _Left ` y ) ) ) -> ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xL x.s ( yL +s z ) ) ) = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xL e. ( _Left ` x ) /\ yL e. ( _Left ` y ) ) ) -> ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xL x.s ( yL +s z ) ) ) = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) ) with typecode |-
59	58	eqeq2d	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xL e. ( _Left ` x ) /\ yL e. ( _Left ` y ) ) ) -> ( a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xL x.s ( yL +s z ) ) ) <-> a = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xL e. ( _Left ` x ) /\ yL e. ( _Left ` y ) ) ) -> ( a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xL x.s ( yL +s z ) ) ) <-> a = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) ) ) with typecode |-
60	59	2rexbidva	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xL x.s ( yL +s z ) ) ) <-> E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xL x.s ( yL +s z ) ) ) <-> E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) ) ) with typecode |-
61	60	abbidv	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xL x.s ( yL +s z ) ) ) } = { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) } ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xL x.s ( yL +s z ) ) ) } = { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) } ) with typecode |-
62		simpr3	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) with typecode |-
63		simpr13	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) with typecode |-
64	54	adantr	Could not format ( ( xL e. ( _Left ` x ) /\ zL e. ( _Left ` z ) ) -> xL e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) : No typesetting found for |- ( ( xL e. ( _Left ` x ) /\ zL e. ( _Left ` z ) ) -> xL e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) with typecode |-
65		elun1	Could not format ( zL e. ( _Left ` z ) -> zL e. ( ( _Left ` z ) u. ( _Right ` z ) ) ) : No typesetting found for |- ( zL e. ( _Left ` z ) -> zL e. ( ( _Left ` z ) u. ( _Right ` z ) ) ) with typecode |-
66	65	adantl	Could not format ( ( xL e. ( _Left ` x ) /\ zL e. ( _Left ` z ) ) -> zL e. ( ( _Left ` z ) u. ( _Right ` z ) ) ) : No typesetting found for |- ( ( xL e. ( _Left ` x ) /\ zL e. ( _Left ` z ) ) -> zL e. ( ( _Left ` z ) u. ( _Right ` z ) ) ) with typecode |-
67	48 49 50 51 62 63 64 66	addsdilem4	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xL e. ( _Left ` x ) /\ zL e. ( _Left ` z ) ) ) -> ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xL x.s ( y +s zL ) ) ) = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xL e. ( _Left ` x ) /\ zL e. ( _Left ` z ) ) ) -> ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xL x.s ( y +s zL ) ) ) = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) ) with typecode |-
68	67	eqeq2d	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xL e. ( _Left ` x ) /\ zL e. ( _Left ` z ) ) ) -> ( a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xL x.s ( y +s zL ) ) ) <-> a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xL e. ( _Left ` x ) /\ zL e. ( _Left ` z ) ) ) -> ( a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xL x.s ( y +s zL ) ) ) <-> a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) ) ) with typecode |-
69	68	2rexbidva	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xL x.s ( y +s zL ) ) ) <-> E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xL x.s ( y +s zL ) ) ) <-> E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) ) ) with typecode |-
70	69	abbidv	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xL x.s ( y +s zL ) ) ) } = { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) } ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xL x.s ( y +s zL ) ) ) } = { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) } ) with typecode |-
71	61 70	uneq12d	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xL x.s ( yL +s z ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xL x.s ( y +s zL ) ) ) } ) = ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) } u. { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) } ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xL x.s ( yL +s z ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xL x.s ( y +s zL ) ) ) } ) = ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) } u. { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) } ) ) with typecode |-
72		elun2	Could not format ( xR e. ( _Right ` x ) -> xR e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) : No typesetting found for |- ( xR e. ( _Right ` x ) -> xR e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) with typecode |-
73	72	adantr	Could not format ( ( xR e. ( _Right ` x ) /\ yR e. ( _Right ` y ) ) -> xR e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) : No typesetting found for |- ( ( xR e. ( _Right ` x ) /\ yR e. ( _Right ` y ) ) -> xR e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) with typecode |-
74		elun2	Could not format ( yR e. ( _Right ` y ) -> yR e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) : No typesetting found for |- ( yR e. ( _Right ` y ) -> yR e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) with typecode |-
75	74	adantl	Could not format ( ( xR e. ( _Right ` x ) /\ yR e. ( _Right ` y ) ) -> yR e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) : No typesetting found for |- ( ( xR e. ( _Right ` x ) /\ yR e. ( _Right ` y ) ) -> yR e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) with typecode |-
76	48 49 50 51 52 53 73 75	addsdilem3	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xR e. ( _Right ` x ) /\ yR e. ( _Right ` y ) ) ) -> ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xR x.s ( yR +s z ) ) ) = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xR e. ( _Right ` x ) /\ yR e. ( _Right ` y ) ) ) -> ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xR x.s ( yR +s z ) ) ) = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) ) with typecode |-
77	76	eqeq2d	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xR e. ( _Right ` x ) /\ yR e. ( _Right ` y ) ) ) -> ( a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xR x.s ( yR +s z ) ) ) <-> a = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xR e. ( _Right ` x ) /\ yR e. ( _Right ` y ) ) ) -> ( a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xR x.s ( yR +s z ) ) ) <-> a = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) ) ) with typecode |-
78	77	2rexbidva	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xR x.s ( yR +s z ) ) ) <-> E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xR x.s ( yR +s z ) ) ) <-> E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) ) ) with typecode |-
79	78	abbidv	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xR x.s ( yR +s z ) ) ) } = { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) } ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xR x.s ( yR +s z ) ) ) } = { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) } ) with typecode |-
80	72	adantr	Could not format ( ( xR e. ( _Right ` x ) /\ zR e. ( _Right ` z ) ) -> xR e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) : No typesetting found for |- ( ( xR e. ( _Right ` x ) /\ zR e. ( _Right ` z ) ) -> xR e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) with typecode |-
81		elun2	Could not format ( zR e. ( _Right ` z ) -> zR e. ( ( _Left ` z ) u. ( _Right ` z ) ) ) : No typesetting found for |- ( zR e. ( _Right ` z ) -> zR e. ( ( _Left ` z ) u. ( _Right ` z ) ) ) with typecode |-
82	81	adantl	Could not format ( ( xR e. ( _Right ` x ) /\ zR e. ( _Right ` z ) ) -> zR e. ( ( _Left ` z ) u. ( _Right ` z ) ) ) : No typesetting found for |- ( ( xR e. ( _Right ` x ) /\ zR e. ( _Right ` z ) ) -> zR e. ( ( _Left ` z ) u. ( _Right ` z ) ) ) with typecode |-
83	48 49 50 51 62 63 80 82	addsdilem4	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xR e. ( _Right ` x ) /\ zR e. ( _Right ` z ) ) ) -> ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xR x.s ( y +s zR ) ) ) = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xR e. ( _Right ` x ) /\ zR e. ( _Right ` z ) ) ) -> ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xR x.s ( y +s zR ) ) ) = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) ) with typecode |-
84	83	eqeq2d	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xR e. ( _Right ` x ) /\ zR e. ( _Right ` z ) ) ) -> ( a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xR x.s ( y +s zR ) ) ) <-> a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xR e. ( _Right ` x ) /\ zR e. ( _Right ` z ) ) ) -> ( a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xR x.s ( y +s zR ) ) ) <-> a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) ) ) with typecode |-
85	84	2rexbidva	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xR x.s ( y +s zR ) ) ) <-> E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xR x.s ( y +s zR ) ) ) <-> E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) ) ) with typecode |-
86	85	abbidv	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xR x.s ( y +s zR ) ) ) } = { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) } ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xR x.s ( y +s zR ) ) ) } = { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) } ) with typecode |-
87	79 86	uneq12d	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xR x.s ( yR +s z ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xR x.s ( y +s zR ) ) ) } ) = ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) } ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xR x.s ( yR +s z ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xR x.s ( y +s zR ) ) ) } ) = ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) } ) ) with typecode |-
88	71 87	uneq12d	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xL x.s ( yL +s z ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xL x.s ( y +s zL ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xR x.s ( yR +s z ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xR x.s ( y +s zR ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) } u. { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) } ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xL x.s ( yL +s z ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xL x.s ( y +s zL ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xR x.s ( yR +s z ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xR x.s ( y +s zR ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) } u. { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) } ) ) ) with typecode |-
89		un4	Could not format ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) } u. { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) } ) ) : No typesetting found for |- ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) } u. { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) } ) ) with typecode |-
90	88 89	eqtrdi	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xL x.s ( yL +s z ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xL x.s ( y +s zL ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xR x.s ( yR +s z ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xR x.s ( y +s zR ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) } ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xL x.s ( yL +s z ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xL x.s ( y +s zL ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xR x.s ( yR +s z ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xR x.s ( y +s zR ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) } ) ) ) with typecode |-
91	54	adantr	Could not format ( ( xL e. ( _Left ` x ) /\ yR e. ( _Right ` y ) ) -> xL e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) : No typesetting found for |- ( ( xL e. ( _Left ` x ) /\ yR e. ( _Right ` y ) ) -> xL e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) with typecode |-
92	74	adantl	Could not format ( ( xL e. ( _Left ` x ) /\ yR e. ( _Right ` y ) ) -> yR e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) : No typesetting found for |- ( ( xL e. ( _Left ` x ) /\ yR e. ( _Right ` y ) ) -> yR e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) with typecode |-
93	48 49 50 51 52 53 91 92	addsdilem3	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xL e. ( _Left ` x ) /\ yR e. ( _Right ` y ) ) ) -> ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xL x.s ( yR +s z ) ) ) = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xL e. ( _Left ` x ) /\ yR e. ( _Right ` y ) ) ) -> ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xL x.s ( yR +s z ) ) ) = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) ) with typecode |-
94	93	eqeq2d	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xL e. ( _Left ` x ) /\ yR e. ( _Right ` y ) ) ) -> ( a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xL x.s ( yR +s z ) ) ) <-> a = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xL e. ( _Left ` x ) /\ yR e. ( _Right ` y ) ) ) -> ( a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xL x.s ( yR +s z ) ) ) <-> a = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) ) ) with typecode |-
95	94	2rexbidva	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xL x.s ( yR +s z ) ) ) <-> E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xL x.s ( yR +s z ) ) ) <-> E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) ) ) with typecode |-
96	95	abbidv	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xL x.s ( yR +s z ) ) ) } = { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) } ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xL x.s ( yR +s z ) ) ) } = { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) } ) with typecode |-
97	54	adantr	Could not format ( ( xL e. ( _Left ` x ) /\ zR e. ( _Right ` z ) ) -> xL e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) : No typesetting found for |- ( ( xL e. ( _Left ` x ) /\ zR e. ( _Right ` z ) ) -> xL e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) with typecode |-
98	81	adantl	Could not format ( ( xL e. ( _Left ` x ) /\ zR e. ( _Right ` z ) ) -> zR e. ( ( _Left ` z ) u. ( _Right ` z ) ) ) : No typesetting found for |- ( ( xL e. ( _Left ` x ) /\ zR e. ( _Right ` z ) ) -> zR e. ( ( _Left ` z ) u. ( _Right ` z ) ) ) with typecode |-
99	48 49 50 51 62 63 97 98	addsdilem4	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xL e. ( _Left ` x ) /\ zR e. ( _Right ` z ) ) ) -> ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xL x.s ( y +s zR ) ) ) = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xL e. ( _Left ` x ) /\ zR e. ( _Right ` z ) ) ) -> ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xL x.s ( y +s zR ) ) ) = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) ) with typecode |-
100	99	eqeq2d	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xL e. ( _Left ` x ) /\ zR e. ( _Right ` z ) ) ) -> ( a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xL x.s ( y +s zR ) ) ) <-> a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xL e. ( _Left ` x ) /\ zR e. ( _Right ` z ) ) ) -> ( a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xL x.s ( y +s zR ) ) ) <-> a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) ) ) with typecode |-
101	100	2rexbidva	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xL x.s ( y +s zR ) ) ) <-> E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xL x.s ( y +s zR ) ) ) <-> E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) ) ) with typecode |-
102	101	abbidv	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xL x.s ( y +s zR ) ) ) } = { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) } ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xL x.s ( y +s zR ) ) ) } = { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) } ) with typecode |-
103	96 102	uneq12d	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xL x.s ( yR +s z ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xL x.s ( y +s zR ) ) ) } ) = ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) } u. { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) } ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xL x.s ( yR +s z ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xL x.s ( y +s zR ) ) ) } ) = ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) } u. { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) } ) ) with typecode |-
104	72	adantr	Could not format ( ( xR e. ( _Right ` x ) /\ yL e. ( _Left ` y ) ) -> xR e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) : No typesetting found for |- ( ( xR e. ( _Right ` x ) /\ yL e. ( _Left ` y ) ) -> xR e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) with typecode |-
105	56	adantl	Could not format ( ( xR e. ( _Right ` x ) /\ yL e. ( _Left ` y ) ) -> yL e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) : No typesetting found for |- ( ( xR e. ( _Right ` x ) /\ yL e. ( _Left ` y ) ) -> yL e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) with typecode |-
106	48 49 50 51 52 53 104 105	addsdilem3	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xR e. ( _Right ` x ) /\ yL e. ( _Left ` y ) ) ) -> ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xR x.s ( yL +s z ) ) ) = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xR e. ( _Right ` x ) /\ yL e. ( _Left ` y ) ) ) -> ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xR x.s ( yL +s z ) ) ) = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) ) with typecode |-
107	106	eqeq2d	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xR e. ( _Right ` x ) /\ yL e. ( _Left ` y ) ) ) -> ( a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xR x.s ( yL +s z ) ) ) <-> a = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xR e. ( _Right ` x ) /\ yL e. ( _Left ` y ) ) ) -> ( a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xR x.s ( yL +s z ) ) ) <-> a = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) ) ) with typecode |-
108	107	2rexbidva	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xR x.s ( yL +s z ) ) ) <-> E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xR x.s ( yL +s z ) ) ) <-> E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) ) ) with typecode |-
109	108	abbidv	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xR x.s ( yL +s z ) ) ) } = { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) } ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xR x.s ( yL +s z ) ) ) } = { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) } ) with typecode |-
110	72	adantr	Could not format ( ( xR e. ( _Right ` x ) /\ zL e. ( _Left ` z ) ) -> xR e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) : No typesetting found for |- ( ( xR e. ( _Right ` x ) /\ zL e. ( _Left ` z ) ) -> xR e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) with typecode |-
111	65	adantl	Could not format ( ( xR e. ( _Right ` x ) /\ zL e. ( _Left ` z ) ) -> zL e. ( ( _Left ` z ) u. ( _Right ` z ) ) ) : No typesetting found for |- ( ( xR e. ( _Right ` x ) /\ zL e. ( _Left ` z ) ) -> zL e. ( ( _Left ` z ) u. ( _Right ` z ) ) ) with typecode |-
112	48 49 50 51 62 63 110 111	addsdilem4	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xR e. ( _Right ` x ) /\ zL e. ( _Left ` z ) ) ) -> ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xR x.s ( y +s zL ) ) ) = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xR e. ( _Right ` x ) /\ zL e. ( _Left ` z ) ) ) -> ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xR x.s ( y +s zL ) ) ) = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) ) with typecode |-
113	112	eqeq2d	Could not format ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xR e. ( _Right ` x ) /\ zL e. ( _Left ` z ) ) ) -> ( a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xR x.s ( y +s zL ) ) ) <-> a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) /\ ( xR e. ( _Right ` x ) /\ zL e. ( _Left ` z ) ) ) -> ( a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xR x.s ( y +s zL ) ) ) <-> a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) ) ) with typecode |-
114	113	2rexbidva	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xR x.s ( y +s zL ) ) ) <-> E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xR x.s ( y +s zL ) ) ) <-> E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) ) ) with typecode |-
115	114	abbidv	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xR x.s ( y +s zL ) ) ) } = { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) } ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xR x.s ( y +s zL ) ) ) } = { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) } ) with typecode |-
116	109 115	uneq12d	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xR x.s ( yL +s z ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xR x.s ( y +s zL ) ) ) } ) = ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) } ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xR x.s ( yL +s z ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xR x.s ( y +s zL ) ) ) } ) = ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) } ) ) with typecode |-
117	103 116	uneq12d	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xL x.s ( yR +s z ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xL x.s ( y +s zR ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xR x.s ( yL +s z ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xR x.s ( y +s zL ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) } u. { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) } ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xL x.s ( yR +s z ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xL x.s ( y +s zR ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xR x.s ( yL +s z ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xR x.s ( y +s zL ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) } u. { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) } ) ) ) with typecode |-
118		un4	Could not format ( ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) } u. { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) } ) ) : No typesetting found for |- ( ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) } u. { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) } ) ) with typecode |-
119	117 118	eqtrdi	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xL x.s ( yR +s z ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xL x.s ( y +s zR ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xR x.s ( yL +s z ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xR x.s ( y +s zL ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) } ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xL x.s ( yR +s z ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xL x.s ( y +s zR ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xR x.s ( yL +s z ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xR x.s ( y +s zL ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) } ) ) ) with typecode |-
120	90 119	oveq12d	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xL x.s ( yL +s z ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xL x.s ( y +s zL ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xR x.s ( yR +s z ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xR x.s ( y +s zR ) ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xL x.s ( yR +s z ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xL x.s ( y +s zR ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xR x.s ( yL +s z ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xR x.s ( y +s zL ) ) ) } ) ) ) = ( ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) } ) ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xL x.s ( yL +s z ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xL x.s ( y +s zL ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xR x.s ( yR +s z ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xR x.s ( y +s zR ) ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xL x.s ( yR +s z ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xL x.s ( y +s zR ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xR x.s ( yL +s z ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xR x.s ( y +s zL ) ) ) } ) ) ) = ( ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) } ) ) ) ) with typecode |-
121	48 49 50	addsdilem1	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( x x.s ( y +s z ) ) = ( ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xL x.s ( yL +s z ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xL x.s ( y +s zL ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xR x.s ( yR +s z ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xR x.s ( y +s zR ) ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xL x.s ( yR +s z ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xL x.s ( y +s zR ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xR x.s ( yL +s z ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xR x.s ( y +s zL ) ) ) } ) ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( x x.s ( y +s z ) ) = ( ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xL x.s ( yL +s z ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xL x.s ( y +s zL ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xR x.s ( yR +s z ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xR x.s ( y +s zR ) ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( yR +s z ) ) ) -s ( xL x.s ( yR +s z ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y +s z ) ) +s ( x x.s ( y +s zR ) ) ) -s ( xL x.s ( y +s zR ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( yL +s z ) ) ) -s ( xR x.s ( yL +s z ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y +s z ) ) +s ( x x.s ( y +s zL ) ) ) -s ( xR x.s ( y +s zL ) ) ) } ) ) ) ) with typecode |-
122	48 49 50	addsdilem2	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( ( x x.s y ) +s ( x x.s z ) ) = ( ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) } ) ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( ( x x.s y ) +s ( x x.s z ) ) = ( ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) +s ( x x.s z ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zL ) ) -s ( xL x.s zL ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zR ) ) -s ( xR x.s zR ) ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) a = ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) +s ( x x.s z ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) a = ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) +s ( x x.s z ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. zR e. ( _Right ` z ) a = ( ( x x.s y ) +s ( ( ( xL x.s z ) +s ( x x.s zR ) ) -s ( xL x.s zR ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. zL e. ( _Left ` z ) a = ( ( x x.s y ) +s ( ( ( xR x.s z ) +s ( x x.s zL ) ) -s ( xR x.s zL ) ) ) } ) ) ) ) with typecode |-
123	120 121 122	3eqtr4d	Could not format ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( x x.s ( y +s z ) ) = ( ( x x.s y ) +s ( x x.s z ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) ) -> ( x x.s ( y +s z ) ) = ( ( x x.s y ) +s ( x x.s z ) ) ) with typecode |-
124	123	ex	Could not format ( ( x e. No /\ y e. No /\ z e. No ) -> ( ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) -> ( x x.s ( y +s z ) ) = ( ( x x.s y ) +s ( x x.s z ) ) ) ) : No typesetting found for |- ( ( x e. No /\ y e. No /\ z e. No ) -> ( ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( yO +s zO ) ) = ( ( xO x.s yO ) +s ( xO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( xO x.s ( yO +s z ) ) = ( ( xO x.s yO ) +s ( xO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( xO x.s ( y +s zO ) ) = ( ( xO x.s y ) +s ( xO x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s ( y +s z ) ) = ( ( xO x.s y ) +s ( xO x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( yO +s zO ) ) = ( ( x x.s yO ) +s ( x x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( x x.s ( yO +s z ) ) = ( ( x x.s yO ) +s ( x x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( x x.s ( y +s zO ) ) = ( ( x x.s y ) +s ( x x.s zO ) ) ) -> ( x x.s ( y +s z ) ) = ( ( x x.s y ) +s ( x x.s z ) ) ) ) with typecode |-
125	5 10 15 20 25 28 32 37 42 47 124	no3inds	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge C\in \mathrm{No}\right)\to A{\cdot }_s\left(B{+}_{s}C\right)=\left(A{\cdot }_{s}B\right){+}_s\left(A{\cdot }_{s}C\right)$$