Metamath Proof Explorer

Theorem addsass

Description: Surreal addition is associative. Part of theorem 3 of Conway p. 17. (Contributed by Scott Fenton, 22-Jan-2025)

Ref Expression
Assertion addsass Could not format assertion : No typesetting found for |- ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( A +s B ) +s C ) = ( A +s ( B +s C ) ) ) with typecode |-

Proof

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