Theorem mulsass

Description: Associative law for surreal multiplication. Part of theorem 7 of Conway p. 19. Much like the case for additive groups, this theorem together with mulscom , addsdi , mulsgt0 , and the addition theorems would make the surreals into an ordered ring except that they are a proper class. (Contributed by Scott Fenton, 10-Mar-2025)

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

Proof

Step	Hyp	Ref	Expression
1		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 |-
2	1	oveq1d	Could not format ( x = xO -> ( ( x x.s y ) x.s z ) = ( ( xO x.s y ) x.s z ) ) : No typesetting found for |- ( x = xO -> ( ( x x.s y ) x.s z ) = ( ( xO x.s y ) x.s z ) ) with typecode |-
3		oveq1	Could not format ( x = xO -> ( x x.s ( y x.s z ) ) = ( xO x.s ( y x.s z ) ) ) : No typesetting found for |- ( x = xO -> ( x x.s ( y x.s z ) ) = ( xO x.s ( y x.s z ) ) ) with typecode |-
4	2 3	eqeq12d	Could not format ( x = xO -> ( ( ( x x.s y ) x.s z ) = ( x x.s ( y x.s z ) ) <-> ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) ) ) : No typesetting found for |- ( x = xO -> ( ( ( x x.s y ) x.s z ) = ( x x.s ( y x.s z ) ) <-> ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) ) ) with typecode |-
5		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 |-
6	5	oveq1d	Could not format ( y = yO -> ( ( xO x.s y ) x.s z ) = ( ( xO x.s yO ) x.s z ) ) : No typesetting found for |- ( y = yO -> ( ( xO x.s y ) x.s z ) = ( ( xO x.s yO ) x.s z ) ) with typecode |-
7		oveq1	Could not format ( y = yO -> ( y x.s z ) = ( yO x.s z ) ) : No typesetting found for |- ( y = yO -> ( y x.s z ) = ( yO x.s z ) ) with typecode |-
8	7	oveq2d	Could not format ( y = yO -> ( xO x.s ( y x.s z ) ) = ( xO x.s ( yO x.s z ) ) ) : No typesetting found for |- ( y = yO -> ( xO x.s ( y x.s z ) ) = ( xO x.s ( yO x.s z ) ) ) with typecode |-
9	6 8	eqeq12d	Could not format ( y = yO -> ( ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) <-> ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) ) ) : No typesetting found for |- ( y = yO -> ( ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) <-> ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) ) ) with typecode |-
10		oveq2	Could not format ( z = zO -> ( ( xO x.s yO ) x.s z ) = ( ( xO x.s yO ) x.s zO ) ) : No typesetting found for |- ( z = zO -> ( ( xO x.s yO ) x.s z ) = ( ( xO x.s yO ) x.s zO ) ) with typecode |-
11		oveq2	Could not format ( z = zO -> ( yO x.s z ) = ( yO x.s zO ) ) : No typesetting found for |- ( z = zO -> ( yO x.s z ) = ( yO x.s zO ) ) with typecode |-
12	11	oveq2d	Could not format ( z = zO -> ( xO x.s ( yO x.s z ) ) = ( xO x.s ( yO x.s zO ) ) ) : No typesetting found for |- ( z = zO -> ( xO x.s ( yO x.s z ) ) = ( xO x.s ( yO x.s zO ) ) ) with typecode |-
13	10 12	eqeq12d	Could not format ( z = zO -> ( ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) <-> ( ( xO x.s yO ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) ) ) : No typesetting found for |- ( z = zO -> ( ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) <-> ( ( xO x.s yO ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) ) ) with typecode |-
14		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 |-
15	14	oveq1d	Could not format ( x = xO -> ( ( x x.s yO ) x.s zO ) = ( ( xO x.s yO ) x.s zO ) ) : No typesetting found for |- ( x = xO -> ( ( x x.s yO ) x.s zO ) = ( ( xO x.s yO ) x.s zO ) ) with typecode |-
16		oveq1	Could not format ( x = xO -> ( x x.s ( yO x.s zO ) ) = ( xO x.s ( yO x.s zO ) ) ) : No typesetting found for |- ( x = xO -> ( x x.s ( yO x.s zO ) ) = ( xO x.s ( yO x.s zO ) ) ) with typecode |-
17	15 16	eqeq12d	Could not format ( x = xO -> ( ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) <-> ( ( xO x.s yO ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) ) ) : No typesetting found for |- ( x = xO -> ( ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) <-> ( ( xO x.s yO ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) ) ) with typecode |-
18		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 |-
19	18	oveq1d	Could not format ( y = yO -> ( ( x x.s y ) x.s zO ) = ( ( x x.s yO ) x.s zO ) ) : No typesetting found for |- ( y = yO -> ( ( x x.s y ) x.s zO ) = ( ( x x.s yO ) x.s zO ) ) with typecode |-
20		oveq1	Could not format ( y = yO -> ( y x.s zO ) = ( yO x.s zO ) ) : No typesetting found for |- ( y = yO -> ( y x.s zO ) = ( yO x.s zO ) ) with typecode |-
21	20	oveq2d	Could not format ( y = yO -> ( x x.s ( y x.s zO ) ) = ( x x.s ( yO x.s zO ) ) ) : No typesetting found for |- ( y = yO -> ( x x.s ( y x.s zO ) ) = ( x x.s ( yO x.s zO ) ) ) with typecode |-
22	19 21	eqeq12d	Could not format ( y = yO -> ( ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) <-> ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) ) ) : No typesetting found for |- ( y = yO -> ( ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) <-> ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) ) ) with typecode |-
23	5	oveq1d	Could not format ( y = yO -> ( ( xO x.s y ) x.s zO ) = ( ( xO x.s yO ) x.s zO ) ) : No typesetting found for |- ( y = yO -> ( ( xO x.s y ) x.s zO ) = ( ( xO x.s yO ) x.s zO ) ) with typecode |-
24	20	oveq2d	Could not format ( y = yO -> ( xO x.s ( y x.s zO ) ) = ( xO x.s ( yO x.s zO ) ) ) : No typesetting found for |- ( y = yO -> ( xO x.s ( y x.s zO ) ) = ( xO x.s ( yO x.s zO ) ) ) with typecode |-
25	23 24	eqeq12d	Could not format ( y = yO -> ( ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) <-> ( ( xO x.s yO ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) ) ) : No typesetting found for |- ( y = yO -> ( ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) <-> ( ( xO x.s yO ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) ) ) with typecode |-
26		oveq2	Could not format ( z = zO -> ( ( x x.s yO ) x.s z ) = ( ( x x.s yO ) x.s zO ) ) : No typesetting found for |- ( z = zO -> ( ( x x.s yO ) x.s z ) = ( ( x x.s yO ) x.s zO ) ) with typecode |-
27	11	oveq2d	Could not format ( z = zO -> ( x x.s ( yO x.s z ) ) = ( x x.s ( yO x.s zO ) ) ) : No typesetting found for |- ( z = zO -> ( x x.s ( yO x.s z ) ) = ( x x.s ( yO x.s zO ) ) ) with typecode |-
28	26 27	eqeq12d	Could not format ( z = zO -> ( ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) <-> ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) ) ) : No typesetting found for |- ( z = zO -> ( ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) <-> ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) ) ) with typecode |-
29		oveq1	$$⊢x=A\to x{\cdot }_{s}y=A{\cdot }_{s}y$$
30	29	oveq1d	$$⊢x=A\to \left(x{\cdot }_{s}y\right){\cdot }_{s}z=\left(A{\cdot }_{s}y\right){\cdot }_{s}z$$
31		oveq1	$$⊢x=A\to x{\cdot }_s\left(y{\cdot }_{s}z\right)=A{\cdot }_s\left(y{\cdot }_{s}z\right)$$
32	30 31	eqeq12d	$$⊢x=A\to \left(\left(x{\cdot }_{s}y\right){\cdot }_{s}z=x{\cdot }_s\left(y{\cdot }_{s}z\right)\leftrightarrow \left(A{\cdot }_{s}y\right){\cdot }_{s}z=A{\cdot }_s\left(y{\cdot }_{s}z\right)\right)$$
33		oveq2	$$⊢y=B\to A{\cdot }_{s}y=A{\cdot }_{s}B$$
34	33	oveq1d	$$⊢y=B\to \left(A{\cdot }_{s}y\right){\cdot }_{s}z=\left(A{\cdot }_{s}B\right){\cdot }_{s}z$$
35		oveq1	$$⊢y=B\to y{\cdot }_{s}z=B{\cdot }_{s}z$$
36	35	oveq2d	$$⊢y=B\to A{\cdot }_s\left(y{\cdot }_{s}z\right)=A{\cdot }_s\left(B{\cdot }_{s}z\right)$$
37	34 36	eqeq12d	$$⊢y=B\to \left(\left(A{\cdot }_{s}y\right){\cdot }_{s}z=A{\cdot }_s\left(y{\cdot }_{s}z\right)\leftrightarrow \left(A{\cdot }_{s}B\right){\cdot }_{s}z=A{\cdot }_s\left(B{\cdot }_{s}z\right)\right)$$
38		oveq2	$$⊢z=C\to \left(A{\cdot }_{s}B\right){\cdot }_{s}z=\left(A{\cdot }_{s}B\right){\cdot }_{s}C$$
39		oveq2	$$⊢z=C\to B{\cdot }_{s}z=B{\cdot }_{s}C$$
40	39	oveq2d	$$⊢z=C\to A{\cdot }_s\left(B{\cdot }_{s}z\right)=A{\cdot }_s\left(B{\cdot }_{s}C\right)$$
41	38 40	eqeq12d	$$⊢z=C\to \left(\left(A{\cdot }_{s}B\right){\cdot }_{s}z=A{\cdot }_s\left(B{\cdot }_{s}z\right)\leftrightarrow \left(A{\cdot }_{s}B\right){\cdot }_{s}C=A{\cdot }_s\left(B{\cdot }_{s}C\right)\right)$$
42		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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> x e. No ) with typecode |-
43		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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> y e. No ) with typecode |-
44		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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> z e. No ) with typecode |-
45		ssun1	$$⊢L\left(x\right)\subseteq L\left(x\right)\cup R\left(x\right)$$
46		ssun1	$$⊢L\left(y\right)\subseteq L\left(y\right)\cup R\left(y\right)$$
47		ssun1	$$⊢L\left(z\right)\subseteq L\left(z\right)\cup R\left(z\right)$$
48		simpr11	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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> 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 ) x.s zO ) = ( xO x.s ( yO 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) ) with typecode |-
49		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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) ) with typecode |-
50		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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) with typecode |-
51		simpr22	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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) ) with typecode |-
52		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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) ) with typecode |-
53		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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) with typecode |-
54		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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) with typecode |-
55	42 43 44 45 46 47 48 49 50 51 52 53 54	mulsasslem3	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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zL ) ) <-> E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zL ) ) <-> E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) ) ) with typecode |-
56	55	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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zL ) ) } = { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zL ) ) } = { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } ) with typecode |-
57		ssun2	$$⊢R\left(x\right)\subseteq L\left(x\right)\cup R\left(x\right)$$
58		ssun2	$$⊢R\left(y\right)\subseteq L\left(y\right)\cup R\left(y\right)$$
59	42 43 44 57 58 47 48 49 50 51 52 53 54	mulsasslem3	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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zL ) ) <-> E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zL ) ) <-> E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) ) ) with typecode |-
60	59	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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zL ) ) } = { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zL ) ) } = { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) with typecode |-
61	56 60	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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zL ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zL ) ) } ) = ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zL ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zL ) ) } ) = ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) ) with typecode |-
62		ssun2	$$⊢R\left(z\right)\subseteq L\left(z\right)\cup R\left(z\right)$$
63	42 43 44 45 58 62 48 49 50 51 52 53 54	mulsasslem3	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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zR ) ) <-> E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zR ) ) <-> E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) ) ) with typecode |-
64	63	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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zR ) ) } = { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zR ) ) } = { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) with typecode |-
65	42 43 44 57 46 62 48 49 50 51 52 53 54	mulsasslem3	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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zR ) ) <-> E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zR ) ) <-> E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) ) ) with typecode |-
66	65	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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zR ) ) } = { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zR ) ) } = { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } ) with typecode |-
67	64 66	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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zR ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zR ) ) } ) = ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zR ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zR ) ) } ) = ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } ) ) with typecode |-
68	61 67	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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zL ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zL ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zR ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zR ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zL ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zL ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zR ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zR ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } ) ) ) with typecode |-
69		un4	Could not format ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } ) ) : No typesetting found for |- ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } ) ) with typecode |-
70		uncom	Could not format ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } ) = ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) : No typesetting found for |- ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } ) = ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) with typecode |-
71	70	uneq2i	Could not format ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) ) : No typesetting found for |- ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) ) with typecode |-
72	69 71	eqtri	Could not format ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) ) : No typesetting found for |- ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) ) with typecode |-
73	68 72	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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zL ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zL ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zR ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zR ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zL ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zL ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zR ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zR ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) ) ) with typecode |-
74	42 43 44 45 46 62 48 49 50 51 52 53 54	mulsasslem3	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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zR ) ) <-> E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zR ) ) <-> E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) ) ) with typecode |-
75	74	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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zR ) ) } = { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zR ) ) } = { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } ) with typecode |-
76	42 43 44 57 58 62 48 49 50 51 52 53 54	mulsasslem3	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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zR ) ) <-> E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zR ) ) <-> E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) ) ) with typecode |-
77	76	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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zR ) ) } = { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zR ) ) } = { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) with typecode |-
78	75 77	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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zR ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zR ) ) } ) = ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zR ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zR ) ) } ) = ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) ) with typecode |-
79	42 43 44 45 58 47 48 49 50 51 52 53 54	mulsasslem3	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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zL ) ) <-> E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zL ) ) <-> E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) ) ) with typecode |-
80	79	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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zL ) ) } = { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zL ) ) } = { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) with typecode |-
81	42 43 44 57 46 47 48 49 50 51 52 53 54	mulsasslem3	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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zL ) ) <-> E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zL ) ) <-> E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) ) ) with typecode |-
82	81	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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zL ) ) } = { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zL ) ) } = { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } ) with typecode |-
83	80 82	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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zL ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zL ) ) } ) = ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zL ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zL ) ) } ) = ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } ) ) with typecode |-
84	78 83	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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zR ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zR ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zL ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zL ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zR ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zR ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zL ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zL ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } ) ) ) with typecode |-
85		un4	Could not format ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } ) ) : No typesetting found for |- ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } ) ) with typecode |-
86		uncom	Could not format ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } ) = ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) : No typesetting found for |- ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } ) = ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) with typecode |-
87	86	uneq2i	Could not format ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) ) : No typesetting found for |- ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) ) with typecode |-
88	85 87	eqtri	Could not format ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) ) : No typesetting found for |- ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) ) with typecode |-
89	84 88	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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zR ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zR ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zL ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zL ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zR ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zR ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zL ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zL ) ) } ) ) = ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) ) ) with typecode |-
90	73 89	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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zL ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zL ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zR ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zR ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zR ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zR ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zL ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zL ) ) } ) ) ) = ( ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zL ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zL ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zR ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zR ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zR ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zR ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zL ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zL ) ) } ) ) ) = ( ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) ) ) ) with typecode |-
91	42 43 44	mulsasslem1	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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( ( x x.s y ) x.s z ) = ( ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zL ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zL ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zR ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zR ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zR ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zR ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zL ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( ( x x.s y ) x.s z ) = ( ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zL ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zL ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zR ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zR ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yL ) ) -s ( xL x.s yL ) ) x.s zR ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zR ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yR ) ) -s ( xR x.s yR ) ) x.s zR ) ) } ) u. ( { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xL x.s y ) +s ( x x.s yR ) ) -s ( xL x.s yR ) ) x.s zL ) ) } u. { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s z ) +s ( ( x x.s y ) x.s zL ) ) -s ( ( ( ( xR x.s y ) +s ( x x.s yL ) ) -s ( xR x.s yL ) ) x.s zL ) ) } ) ) ) ) with typecode |-
92	42 43 44	mulsasslem2	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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( x x.s ( y x.s z ) ) = ( ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( x x.s ( y x.s z ) ) = ( ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) ) |s ( ( { a | E. xL e. ( _Left ` x ) E. yL e. ( _Left ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) -s ( xL x.s ( ( ( yL x.s z ) +s ( y x.s zR ) ) -s ( yL x.s zR ) ) ) ) } u. { a | E. xL e. ( _Left ` x ) E. yR e. ( _Right ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xL x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) -s ( xL x.s ( ( ( yR x.s z ) +s ( y x.s zL ) ) -s ( yR x.s zL ) ) ) ) } ) u. ( { a | E. xR e. ( _Right ` x ) E. yL e. ( _Left ` y ) E. zL e. ( _Left ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) -s ( xR x.s ( ( ( yL x.s z ) +s ( y x.s zL ) ) -s ( yL x.s zL ) ) ) ) } u. { a | E. xR e. ( _Right ` x ) E. yR e. ( _Right ` y ) E. zR e. ( _Right ` z ) a = ( ( ( xR x.s ( y x.s z ) ) +s ( x x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) -s ( xR x.s ( ( ( yR x.s z ) +s ( y x.s zR ) ) -s ( yR x.s zR ) ) ) ) } ) ) ) ) with typecode |-
93	90 91 92	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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( ( x x.s y ) x.s z ) = ( x x.s ( y 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) ) -> ( ( x x.s y ) x.s z ) = ( x x.s ( y x.s z ) ) ) with typecode |-
94	93	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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) -> ( ( x x.s y ) x.s z ) = ( x x.s ( y 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 ) x.s zO ) = ( xO x.s ( yO x.s zO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( xO x.s yO ) x.s z ) = ( xO x.s ( yO x.s z ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( xO x.s y ) x.s zO ) = ( xO x.s ( y x.s zO ) ) ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( ( xO x.s y ) x.s z ) = ( xO x.s ( y x.s z ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s yO ) x.s zO ) = ( x x.s ( yO x.s zO ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( ( x x.s yO ) x.s z ) = ( x x.s ( yO x.s z ) ) ) /\ A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( x x.s y ) x.s zO ) = ( x x.s ( y x.s zO ) ) ) -> ( ( x x.s y ) x.s z ) = ( x x.s ( y x.s z ) ) ) ) with typecode |-
95	4 9 13 17 22 25 28 32 37 41 94	no3inds	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge C\in \mathrm{No}\right)\to \left(A{\cdot }_{s}B\right){\cdot }_{s}C=A{\cdot }_s\left(B{\cdot }_{s}C\right)$$