Theorem addsasslem1

Description: Lemma for addition associativity. Expand one form of the triple sum. (Contributed by Scott Fenton, 21-Jan-2025)

	Ref	Expression
Hypotheses	addsasslem.1	$$⊢\phi \to A\in \mathrm{No}$$
	addsasslem.2	$$⊢\phi \to B\in \mathrm{No}$$
	addsasslem.3	$$⊢\phi \to C\in \mathrm{No}$$
Assertion	addsasslem1	Could not format assertion : No typesetting found for |- ( ph -> ( ( A +s B ) +s C ) = ( ( ( { y | E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) } u. { z | E. m e. ( _Left ` B ) z = ( ( A +s m ) +s C ) } ) u. { w | E. n e. ( _Left ` C ) w = ( ( A +s B ) +s n ) } ) |s ( ( { a | E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) } u. { b | E. q e. ( _Right ` B ) b = ( ( A +s q ) +s C ) } ) u. { c | E. r e. ( _Right ` C ) c = ( ( A +s B ) +s r ) } ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		addsasslem.1	$$⊢\phi \to A\in \mathrm{No}$$
2		addsasslem.2	$$⊢\phi \to B\in \mathrm{No}$$
3		addsasslem.3	$$⊢\phi \to C\in \mathrm{No}$$
4	1 2	addscut	Could not format ( ph -> ( ( A +s B ) e. No /\ ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) < ( ( A +s B ) e. No /\ ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) <
5	4	simp2d	Could not format ( ph -> ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) < ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) <
6	4	simp3d	Could not format ( ph -> { ( A +s B ) } < { ( A +s B ) } <
7		ovex	Could not format ( A +s B ) e. _V : No typesetting found for |- ( A +s B ) e. _V with typecode |-
8	7	snnz	Could not format { ( A +s B ) } =/= (/) : No typesetting found for |- { ( A +s B ) } =/= (/) with typecode |-
9		sslttr	Could not format ( ( ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) < ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) < ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) <
10	8 9	mp3an3	Could not format ( ( ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) < ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) < ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) <
11	5 6 10	syl2anc	Could not format ( ph -> ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) < ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) <
12		lltropt	Could not format ( _Left ` C ) <
13	12	a1i	Could not format ( ph -> ( _Left ` C ) < ( _Left ` C ) <
14		addsval2	Could not format ( ( A e. No /\ B e. No ) -> ( A +s B ) = ( ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) |s ( { f | E. p e. ( _Right ` A ) f = ( p +s B ) } u. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( A +s B ) = ( ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) |s ( { f | E. p e. ( _Right ` A ) f = ( p +s B ) } u. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } ) ) ) with typecode |-
15	1 2 14	syl2anc	Could not format ( ph -> ( A +s B ) = ( ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) |s ( { f | E. p e. ( _Right ` A ) f = ( p +s B ) } u. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } ) ) ) : No typesetting found for |- ( ph -> ( A +s B ) = ( ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) |s ( { f | E. p e. ( _Right ` A ) f = ( p +s B ) } u. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } ) ) ) with typecode |-
16		lrcut	Could not format ( C e. No -> ( ( _Left ` C ) |s ( _Right ` C ) ) = C ) : No typesetting found for |- ( C e. No -> ( ( _Left ` C ) |s ( _Right ` C ) ) = C ) with typecode |-
17	3 16	syl	Could not format ( ph -> ( ( _Left ` C ) |s ( _Right ` C ) ) = C ) : No typesetting found for |- ( ph -> ( ( _Left ` C ) |s ( _Right ` C ) ) = C ) with typecode |-
18	17	eqcomd	Could not format ( ph -> C = ( ( _Left ` C ) |s ( _Right ` C ) ) ) : No typesetting found for |- ( ph -> C = ( ( _Left ` C ) |s ( _Right ` C ) ) ) with typecode |-
19	11 13 15 18	addsunif	Could not format ( ph -> ( ( A +s B ) +s C ) = ( ( { y | E. h e. ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) y = ( h +s C ) } u. { w | E. n e. ( _Left ` C ) w = ( ( A +s B ) +s n ) } ) |s ( { a | E. i e. ( { f | E. p e. ( _Right ` A ) f = ( p +s B ) } u. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } ) a = ( i +s C ) } u. { c | E. r e. ( _Right ` C ) c = ( ( A +s B ) +s r ) } ) ) ) : No typesetting found for |- ( ph -> ( ( A +s B ) +s C ) = ( ( { y | E. h e. ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) y = ( h +s C ) } u. { w | E. n e. ( _Left ` C ) w = ( ( A +s B ) +s n ) } ) |s ( { a | E. i e. ( { f | E. p e. ( _Right ` A ) f = ( p +s B ) } u. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } ) a = ( i +s C ) } u. { c | E. r e. ( _Right ` C ) c = ( ( A +s B ) +s r ) } ) ) ) with typecode |-
20		unab	Could not format ( { y | E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) } u. { y | E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) } ) = { y | ( E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) \/ E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) ) } : No typesetting found for |- ( { y | E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) } u. { y | E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) } ) = { y | ( E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) \/ E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) ) } with typecode |-
21		eqeq1	Could not format ( z = y -> ( z = ( ( A +s m ) +s C ) <-> y = ( ( A +s m ) +s C ) ) ) : No typesetting found for |- ( z = y -> ( z = ( ( A +s m ) +s C ) <-> y = ( ( A +s m ) +s C ) ) ) with typecode |-
22	21	rexbidv	Could not format ( z = y -> ( E. m e. ( _Left ` B ) z = ( ( A +s m ) +s C ) <-> E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) ) ) : No typesetting found for |- ( z = y -> ( E. m e. ( _Left ` B ) z = ( ( A +s m ) +s C ) <-> E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) ) ) with typecode |-
23	22	cbvabv	Could not format { z | E. m e. ( _Left ` B ) z = ( ( A +s m ) +s C ) } = { y | E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) } : No typesetting found for |- { z | E. m e. ( _Left ` B ) z = ( ( A +s m ) +s C ) } = { y | E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) } with typecode |-
24	23	uneq2i	Could not format ( { y | E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) } u. { z | E. m e. ( _Left ` B ) z = ( ( A +s m ) +s C ) } ) = ( { y | E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) } u. { y | E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) } ) : No typesetting found for |- ( { y | E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) } u. { z | E. m e. ( _Left ` B ) z = ( ( A +s m ) +s C ) } ) = ( { y | E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) } u. { y | E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) } ) with typecode |-
25		rexun	Could not format ( E. h e. ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) y = ( h +s C ) <-> ( E. h e. { d | E. l e. ( _Left ` A ) d = ( l +s B ) } y = ( h +s C ) \/ E. h e. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } y = ( h +s C ) ) ) : No typesetting found for |- ( E. h e. ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) y = ( h +s C ) <-> ( E. h e. { d | E. l e. ( _Left ` A ) d = ( l +s B ) } y = ( h +s C ) \/ E. h e. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } y = ( h +s C ) ) ) with typecode |-
26		eqeq1	Could not format ( d = h -> ( d = ( l +s B ) <-> h = ( l +s B ) ) ) : No typesetting found for |- ( d = h -> ( d = ( l +s B ) <-> h = ( l +s B ) ) ) with typecode |-
27	26	rexbidv	Could not format ( d = h -> ( E. l e. ( _Left ` A ) d = ( l +s B ) <-> E. l e. ( _Left ` A ) h = ( l +s B ) ) ) : No typesetting found for |- ( d = h -> ( E. l e. ( _Left ` A ) d = ( l +s B ) <-> E. l e. ( _Left ` A ) h = ( l +s B ) ) ) with typecode |-
28	27	rexab	Could not format ( E. h e. { d | E. l e. ( _Left ` A ) d = ( l +s B ) } y = ( h +s C ) <-> E. h ( E. l e. ( _Left ` A ) h = ( l +s B ) /\ y = ( h +s C ) ) ) : No typesetting found for |- ( E. h e. { d | E. l e. ( _Left ` A ) d = ( l +s B ) } y = ( h +s C ) <-> E. h ( E. l e. ( _Left ` A ) h = ( l +s B ) /\ y = ( h +s C ) ) ) with typecode |-
29		rexcom4	Could not format ( E. l e. ( _Left ` A ) E. h ( h = ( l +s B ) /\ y = ( h +s C ) ) <-> E. h E. l e. ( _Left ` A ) ( h = ( l +s B ) /\ y = ( h +s C ) ) ) : No typesetting found for |- ( E. l e. ( _Left ` A ) E. h ( h = ( l +s B ) /\ y = ( h +s C ) ) <-> E. h E. l e. ( _Left ` A ) ( h = ( l +s B ) /\ y = ( h +s C ) ) ) with typecode |-
30		ovex	Could not format ( l +s B ) e. _V : No typesetting found for |- ( l +s B ) e. _V with typecode |-
31		oveq1	Could not format ( h = ( l +s B ) -> ( h +s C ) = ( ( l +s B ) +s C ) ) : No typesetting found for |- ( h = ( l +s B ) -> ( h +s C ) = ( ( l +s B ) +s C ) ) with typecode |-
32	31	eqeq2d	Could not format ( h = ( l +s B ) -> ( y = ( h +s C ) <-> y = ( ( l +s B ) +s C ) ) ) : No typesetting found for |- ( h = ( l +s B ) -> ( y = ( h +s C ) <-> y = ( ( l +s B ) +s C ) ) ) with typecode |-
33	30 32	ceqsexv	Could not format ( E. h ( h = ( l +s B ) /\ y = ( h +s C ) ) <-> y = ( ( l +s B ) +s C ) ) : No typesetting found for |- ( E. h ( h = ( l +s B ) /\ y = ( h +s C ) ) <-> y = ( ( l +s B ) +s C ) ) with typecode |-
34	33	rexbii	Could not format ( E. l e. ( _Left ` A ) E. h ( h = ( l +s B ) /\ y = ( h +s C ) ) <-> E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) ) : No typesetting found for |- ( E. l e. ( _Left ` A ) E. h ( h = ( l +s B ) /\ y = ( h +s C ) ) <-> E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) ) with typecode |-
35		r19.41v	Could not format ( E. l e. ( _Left ` A ) ( h = ( l +s B ) /\ y = ( h +s C ) ) <-> ( E. l e. ( _Left ` A ) h = ( l +s B ) /\ y = ( h +s C ) ) ) : No typesetting found for |- ( E. l e. ( _Left ` A ) ( h = ( l +s B ) /\ y = ( h +s C ) ) <-> ( E. l e. ( _Left ` A ) h = ( l +s B ) /\ y = ( h +s C ) ) ) with typecode |-
36	35	exbii	Could not format ( E. h E. l e. ( _Left ` A ) ( h = ( l +s B ) /\ y = ( h +s C ) ) <-> E. h ( E. l e. ( _Left ` A ) h = ( l +s B ) /\ y = ( h +s C ) ) ) : No typesetting found for |- ( E. h E. l e. ( _Left ` A ) ( h = ( l +s B ) /\ y = ( h +s C ) ) <-> E. h ( E. l e. ( _Left ` A ) h = ( l +s B ) /\ y = ( h +s C ) ) ) with typecode |-
37	29 34 36	3bitr3ri	Could not format ( E. h ( E. l e. ( _Left ` A ) h = ( l +s B ) /\ y = ( h +s C ) ) <-> E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) ) : No typesetting found for |- ( E. h ( E. l e. ( _Left ` A ) h = ( l +s B ) /\ y = ( h +s C ) ) <-> E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) ) with typecode |-
38	28 37	bitri	Could not format ( E. h e. { d | E. l e. ( _Left ` A ) d = ( l +s B ) } y = ( h +s C ) <-> E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) ) : No typesetting found for |- ( E. h e. { d | E. l e. ( _Left ` A ) d = ( l +s B ) } y = ( h +s C ) <-> E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) ) with typecode |-
39		eqeq1	Could not format ( e = h -> ( e = ( A +s m ) <-> h = ( A +s m ) ) ) : No typesetting found for |- ( e = h -> ( e = ( A +s m ) <-> h = ( A +s m ) ) ) with typecode |-
40	39	rexbidv	Could not format ( e = h -> ( E. m e. ( _Left ` B ) e = ( A +s m ) <-> E. m e. ( _Left ` B ) h = ( A +s m ) ) ) : No typesetting found for |- ( e = h -> ( E. m e. ( _Left ` B ) e = ( A +s m ) <-> E. m e. ( _Left ` B ) h = ( A +s m ) ) ) with typecode |-
41	40	rexab	Could not format ( E. h e. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } y = ( h +s C ) <-> E. h ( E. m e. ( _Left ` B ) h = ( A +s m ) /\ y = ( h +s C ) ) ) : No typesetting found for |- ( E. h e. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } y = ( h +s C ) <-> E. h ( E. m e. ( _Left ` B ) h = ( A +s m ) /\ y = ( h +s C ) ) ) with typecode |-
42		rexcom4	Could not format ( E. m e. ( _Left ` B ) E. h ( h = ( A +s m ) /\ y = ( h +s C ) ) <-> E. h E. m e. ( _Left ` B ) ( h = ( A +s m ) /\ y = ( h +s C ) ) ) : No typesetting found for |- ( E. m e. ( _Left ` B ) E. h ( h = ( A +s m ) /\ y = ( h +s C ) ) <-> E. h E. m e. ( _Left ` B ) ( h = ( A +s m ) /\ y = ( h +s C ) ) ) with typecode |-
43		ovex	Could not format ( A +s m ) e. _V : No typesetting found for |- ( A +s m ) e. _V with typecode |-
44		oveq1	Could not format ( h = ( A +s m ) -> ( h +s C ) = ( ( A +s m ) +s C ) ) : No typesetting found for |- ( h = ( A +s m ) -> ( h +s C ) = ( ( A +s m ) +s C ) ) with typecode |-
45	44	eqeq2d	Could not format ( h = ( A +s m ) -> ( y = ( h +s C ) <-> y = ( ( A +s m ) +s C ) ) ) : No typesetting found for |- ( h = ( A +s m ) -> ( y = ( h +s C ) <-> y = ( ( A +s m ) +s C ) ) ) with typecode |-
46	43 45	ceqsexv	Could not format ( E. h ( h = ( A +s m ) /\ y = ( h +s C ) ) <-> y = ( ( A +s m ) +s C ) ) : No typesetting found for |- ( E. h ( h = ( A +s m ) /\ y = ( h +s C ) ) <-> y = ( ( A +s m ) +s C ) ) with typecode |-
47	46	rexbii	Could not format ( E. m e. ( _Left ` B ) E. h ( h = ( A +s m ) /\ y = ( h +s C ) ) <-> E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) ) : No typesetting found for |- ( E. m e. ( _Left ` B ) E. h ( h = ( A +s m ) /\ y = ( h +s C ) ) <-> E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) ) with typecode |-
48		r19.41v	Could not format ( E. m e. ( _Left ` B ) ( h = ( A +s m ) /\ y = ( h +s C ) ) <-> ( E. m e. ( _Left ` B ) h = ( A +s m ) /\ y = ( h +s C ) ) ) : No typesetting found for |- ( E. m e. ( _Left ` B ) ( h = ( A +s m ) /\ y = ( h +s C ) ) <-> ( E. m e. ( _Left ` B ) h = ( A +s m ) /\ y = ( h +s C ) ) ) with typecode |-
49	48	exbii	Could not format ( E. h E. m e. ( _Left ` B ) ( h = ( A +s m ) /\ y = ( h +s C ) ) <-> E. h ( E. m e. ( _Left ` B ) h = ( A +s m ) /\ y = ( h +s C ) ) ) : No typesetting found for |- ( E. h E. m e. ( _Left ` B ) ( h = ( A +s m ) /\ y = ( h +s C ) ) <-> E. h ( E. m e. ( _Left ` B ) h = ( A +s m ) /\ y = ( h +s C ) ) ) with typecode |-
50	42 47 49	3bitr3ri	Could not format ( E. h ( E. m e. ( _Left ` B ) h = ( A +s m ) /\ y = ( h +s C ) ) <-> E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) ) : No typesetting found for |- ( E. h ( E. m e. ( _Left ` B ) h = ( A +s m ) /\ y = ( h +s C ) ) <-> E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) ) with typecode |-
51	41 50	bitri	Could not format ( E. h e. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } y = ( h +s C ) <-> E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) ) : No typesetting found for |- ( E. h e. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } y = ( h +s C ) <-> E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) ) with typecode |-
52	38 51	orbi12i	Could not format ( ( E. h e. { d | E. l e. ( _Left ` A ) d = ( l +s B ) } y = ( h +s C ) \/ E. h e. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } y = ( h +s C ) ) <-> ( E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) \/ E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) ) ) : No typesetting found for |- ( ( E. h e. { d | E. l e. ( _Left ` A ) d = ( l +s B ) } y = ( h +s C ) \/ E. h e. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } y = ( h +s C ) ) <-> ( E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) \/ E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) ) ) with typecode |-
53	25 52	bitri	Could not format ( E. h e. ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) y = ( h +s C ) <-> ( E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) \/ E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) ) ) : No typesetting found for |- ( E. h e. ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) y = ( h +s C ) <-> ( E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) \/ E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) ) ) with typecode |-
54	53	abbii	Could not format { y | E. h e. ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) y = ( h +s C ) } = { y | ( E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) \/ E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) ) } : No typesetting found for |- { y | E. h e. ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) y = ( h +s C ) } = { y | ( E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) \/ E. m e. ( _Left ` B ) y = ( ( A +s m ) +s C ) ) } with typecode |-
55	20 24 54	3eqtr4ri	Could not format { y | E. h e. ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) y = ( h +s C ) } = ( { y | E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) } u. { z | E. m e. ( _Left ` B ) z = ( ( A +s m ) +s C ) } ) : No typesetting found for |- { y | E. h e. ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) y = ( h +s C ) } = ( { y | E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) } u. { z | E. m e. ( _Left ` B ) z = ( ( A +s m ) +s C ) } ) with typecode |-
56	55	uneq1i	Could not format ( { y | E. h e. ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) y = ( h +s C ) } u. { w | E. n e. ( _Left ` C ) w = ( ( A +s B ) +s n ) } ) = ( ( { y | E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) } u. { z | E. m e. ( _Left ` B ) z = ( ( A +s m ) +s C ) } ) u. { w | E. n e. ( _Left ` C ) w = ( ( A +s B ) +s n ) } ) : No typesetting found for |- ( { y | E. h e. ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) y = ( h +s C ) } u. { w | E. n e. ( _Left ` C ) w = ( ( A +s B ) +s n ) } ) = ( ( { y | E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) } u. { z | E. m e. ( _Left ` B ) z = ( ( A +s m ) +s C ) } ) u. { w | E. n e. ( _Left ` C ) w = ( ( A +s B ) +s n ) } ) with typecode |-
57		unab	Could not format ( { a | E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) } u. { a | E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) } ) = { a | ( E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) \/ E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) ) } : No typesetting found for |- ( { a | E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) } u. { a | E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) } ) = { a | ( E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) \/ E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) ) } with typecode |-
58		eqeq1	Could not format ( b = a -> ( b = ( ( A +s q ) +s C ) <-> a = ( ( A +s q ) +s C ) ) ) : No typesetting found for |- ( b = a -> ( b = ( ( A +s q ) +s C ) <-> a = ( ( A +s q ) +s C ) ) ) with typecode |-
59	58	rexbidv	Could not format ( b = a -> ( E. q e. ( _Right ` B ) b = ( ( A +s q ) +s C ) <-> E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) ) ) : No typesetting found for |- ( b = a -> ( E. q e. ( _Right ` B ) b = ( ( A +s q ) +s C ) <-> E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) ) ) with typecode |-
60	59	cbvabv	Could not format { b | E. q e. ( _Right ` B ) b = ( ( A +s q ) +s C ) } = { a | E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) } : No typesetting found for |- { b | E. q e. ( _Right ` B ) b = ( ( A +s q ) +s C ) } = { a | E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) } with typecode |-
61	60	uneq2i	Could not format ( { a | E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) } u. { b | E. q e. ( _Right ` B ) b = ( ( A +s q ) +s C ) } ) = ( { a | E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) } u. { a | E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) } ) : No typesetting found for |- ( { a | E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) } u. { b | E. q e. ( _Right ` B ) b = ( ( A +s q ) +s C ) } ) = ( { a | E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) } u. { a | E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) } ) with typecode |-
62		rexun	Could not format ( E. i e. ( { f | E. p e. ( _Right ` A ) f = ( p +s B ) } u. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } ) a = ( i +s C ) <-> ( E. i e. { f | E. p e. ( _Right ` A ) f = ( p +s B ) } a = ( i +s C ) \/ E. i e. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } a = ( i +s C ) ) ) : No typesetting found for |- ( E. i e. ( { f | E. p e. ( _Right ` A ) f = ( p +s B ) } u. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } ) a = ( i +s C ) <-> ( E. i e. { f | E. p e. ( _Right ` A ) f = ( p +s B ) } a = ( i +s C ) \/ E. i e. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } a = ( i +s C ) ) ) with typecode |-
63		eqeq1	Could not format ( f = i -> ( f = ( p +s B ) <-> i = ( p +s B ) ) ) : No typesetting found for |- ( f = i -> ( f = ( p +s B ) <-> i = ( p +s B ) ) ) with typecode |-
64	63	rexbidv	Could not format ( f = i -> ( E. p e. ( _Right ` A ) f = ( p +s B ) <-> E. p e. ( _Right ` A ) i = ( p +s B ) ) ) : No typesetting found for |- ( f = i -> ( E. p e. ( _Right ` A ) f = ( p +s B ) <-> E. p e. ( _Right ` A ) i = ( p +s B ) ) ) with typecode |-
65	64	rexab	Could not format ( E. i e. { f | E. p e. ( _Right ` A ) f = ( p +s B ) } a = ( i +s C ) <-> E. i ( E. p e. ( _Right ` A ) i = ( p +s B ) /\ a = ( i +s C ) ) ) : No typesetting found for |- ( E. i e. { f | E. p e. ( _Right ` A ) f = ( p +s B ) } a = ( i +s C ) <-> E. i ( E. p e. ( _Right ` A ) i = ( p +s B ) /\ a = ( i +s C ) ) ) with typecode |-
66		rexcom4	Could not format ( E. p e. ( _Right ` A ) E. i ( i = ( p +s B ) /\ a = ( i +s C ) ) <-> E. i E. p e. ( _Right ` A ) ( i = ( p +s B ) /\ a = ( i +s C ) ) ) : No typesetting found for |- ( E. p e. ( _Right ` A ) E. i ( i = ( p +s B ) /\ a = ( i +s C ) ) <-> E. i E. p e. ( _Right ` A ) ( i = ( p +s B ) /\ a = ( i +s C ) ) ) with typecode |-
67		ovex	Could not format ( p +s B ) e. _V : No typesetting found for |- ( p +s B ) e. _V with typecode |-
68		oveq1	Could not format ( i = ( p +s B ) -> ( i +s C ) = ( ( p +s B ) +s C ) ) : No typesetting found for |- ( i = ( p +s B ) -> ( i +s C ) = ( ( p +s B ) +s C ) ) with typecode |-
69	68	eqeq2d	Could not format ( i = ( p +s B ) -> ( a = ( i +s C ) <-> a = ( ( p +s B ) +s C ) ) ) : No typesetting found for |- ( i = ( p +s B ) -> ( a = ( i +s C ) <-> a = ( ( p +s B ) +s C ) ) ) with typecode |-
70	67 69	ceqsexv	Could not format ( E. i ( i = ( p +s B ) /\ a = ( i +s C ) ) <-> a = ( ( p +s B ) +s C ) ) : No typesetting found for |- ( E. i ( i = ( p +s B ) /\ a = ( i +s C ) ) <-> a = ( ( p +s B ) +s C ) ) with typecode |-
71	70	rexbii	Could not format ( E. p e. ( _Right ` A ) E. i ( i = ( p +s B ) /\ a = ( i +s C ) ) <-> E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) ) : No typesetting found for |- ( E. p e. ( _Right ` A ) E. i ( i = ( p +s B ) /\ a = ( i +s C ) ) <-> E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) ) with typecode |-
72		r19.41v	Could not format ( E. p e. ( _Right ` A ) ( i = ( p +s B ) /\ a = ( i +s C ) ) <-> ( E. p e. ( _Right ` A ) i = ( p +s B ) /\ a = ( i +s C ) ) ) : No typesetting found for |- ( E. p e. ( _Right ` A ) ( i = ( p +s B ) /\ a = ( i +s C ) ) <-> ( E. p e. ( _Right ` A ) i = ( p +s B ) /\ a = ( i +s C ) ) ) with typecode |-
73	72	exbii	Could not format ( E. i E. p e. ( _Right ` A ) ( i = ( p +s B ) /\ a = ( i +s C ) ) <-> E. i ( E. p e. ( _Right ` A ) i = ( p +s B ) /\ a = ( i +s C ) ) ) : No typesetting found for |- ( E. i E. p e. ( _Right ` A ) ( i = ( p +s B ) /\ a = ( i +s C ) ) <-> E. i ( E. p e. ( _Right ` A ) i = ( p +s B ) /\ a = ( i +s C ) ) ) with typecode |-
74	66 71 73	3bitr3ri	Could not format ( E. i ( E. p e. ( _Right ` A ) i = ( p +s B ) /\ a = ( i +s C ) ) <-> E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) ) : No typesetting found for |- ( E. i ( E. p e. ( _Right ` A ) i = ( p +s B ) /\ a = ( i +s C ) ) <-> E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) ) with typecode |-
75	65 74	bitri	Could not format ( E. i e. { f | E. p e. ( _Right ` A ) f = ( p +s B ) } a = ( i +s C ) <-> E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) ) : No typesetting found for |- ( E. i e. { f | E. p e. ( _Right ` A ) f = ( p +s B ) } a = ( i +s C ) <-> E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) ) with typecode |-
76		eqeq1	Could not format ( g = i -> ( g = ( A +s q ) <-> i = ( A +s q ) ) ) : No typesetting found for |- ( g = i -> ( g = ( A +s q ) <-> i = ( A +s q ) ) ) with typecode |-
77	76	rexbidv	Could not format ( g = i -> ( E. q e. ( _Right ` B ) g = ( A +s q ) <-> E. q e. ( _Right ` B ) i = ( A +s q ) ) ) : No typesetting found for |- ( g = i -> ( E. q e. ( _Right ` B ) g = ( A +s q ) <-> E. q e. ( _Right ` B ) i = ( A +s q ) ) ) with typecode |-
78	77	rexab	Could not format ( E. i e. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } a = ( i +s C ) <-> E. i ( E. q e. ( _Right ` B ) i = ( A +s q ) /\ a = ( i +s C ) ) ) : No typesetting found for |- ( E. i e. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } a = ( i +s C ) <-> E. i ( E. q e. ( _Right ` B ) i = ( A +s q ) /\ a = ( i +s C ) ) ) with typecode |-
79		rexcom4	Could not format ( E. q e. ( _Right ` B ) E. i ( i = ( A +s q ) /\ a = ( i +s C ) ) <-> E. i E. q e. ( _Right ` B ) ( i = ( A +s q ) /\ a = ( i +s C ) ) ) : No typesetting found for |- ( E. q e. ( _Right ` B ) E. i ( i = ( A +s q ) /\ a = ( i +s C ) ) <-> E. i E. q e. ( _Right ` B ) ( i = ( A +s q ) /\ a = ( i +s C ) ) ) with typecode |-
80		ovex	Could not format ( A +s q ) e. _V : No typesetting found for |- ( A +s q ) e. _V with typecode |-
81		oveq1	Could not format ( i = ( A +s q ) -> ( i +s C ) = ( ( A +s q ) +s C ) ) : No typesetting found for |- ( i = ( A +s q ) -> ( i +s C ) = ( ( A +s q ) +s C ) ) with typecode |-
82	81	eqeq2d	Could not format ( i = ( A +s q ) -> ( a = ( i +s C ) <-> a = ( ( A +s q ) +s C ) ) ) : No typesetting found for |- ( i = ( A +s q ) -> ( a = ( i +s C ) <-> a = ( ( A +s q ) +s C ) ) ) with typecode |-
83	80 82	ceqsexv	Could not format ( E. i ( i = ( A +s q ) /\ a = ( i +s C ) ) <-> a = ( ( A +s q ) +s C ) ) : No typesetting found for |- ( E. i ( i = ( A +s q ) /\ a = ( i +s C ) ) <-> a = ( ( A +s q ) +s C ) ) with typecode |-
84	83	rexbii	Could not format ( E. q e. ( _Right ` B ) E. i ( i = ( A +s q ) /\ a = ( i +s C ) ) <-> E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) ) : No typesetting found for |- ( E. q e. ( _Right ` B ) E. i ( i = ( A +s q ) /\ a = ( i +s C ) ) <-> E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) ) with typecode |-
85		r19.41v	Could not format ( E. q e. ( _Right ` B ) ( i = ( A +s q ) /\ a = ( i +s C ) ) <-> ( E. q e. ( _Right ` B ) i = ( A +s q ) /\ a = ( i +s C ) ) ) : No typesetting found for |- ( E. q e. ( _Right ` B ) ( i = ( A +s q ) /\ a = ( i +s C ) ) <-> ( E. q e. ( _Right ` B ) i = ( A +s q ) /\ a = ( i +s C ) ) ) with typecode |-
86	85	exbii	Could not format ( E. i E. q e. ( _Right ` B ) ( i = ( A +s q ) /\ a = ( i +s C ) ) <-> E. i ( E. q e. ( _Right ` B ) i = ( A +s q ) /\ a = ( i +s C ) ) ) : No typesetting found for |- ( E. i E. q e. ( _Right ` B ) ( i = ( A +s q ) /\ a = ( i +s C ) ) <-> E. i ( E. q e. ( _Right ` B ) i = ( A +s q ) /\ a = ( i +s C ) ) ) with typecode |-
87	79 84 86	3bitr3ri	Could not format ( E. i ( E. q e. ( _Right ` B ) i = ( A +s q ) /\ a = ( i +s C ) ) <-> E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) ) : No typesetting found for |- ( E. i ( E. q e. ( _Right ` B ) i = ( A +s q ) /\ a = ( i +s C ) ) <-> E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) ) with typecode |-
88	78 87	bitri	Could not format ( E. i e. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } a = ( i +s C ) <-> E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) ) : No typesetting found for |- ( E. i e. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } a = ( i +s C ) <-> E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) ) with typecode |-
89	75 88	orbi12i	Could not format ( ( E. i e. { f | E. p e. ( _Right ` A ) f = ( p +s B ) } a = ( i +s C ) \/ E. i e. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } a = ( i +s C ) ) <-> ( E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) \/ E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) ) ) : No typesetting found for |- ( ( E. i e. { f | E. p e. ( _Right ` A ) f = ( p +s B ) } a = ( i +s C ) \/ E. i e. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } a = ( i +s C ) ) <-> ( E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) \/ E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) ) ) with typecode |-
90	62 89	bitri	Could not format ( E. i e. ( { f | E. p e. ( _Right ` A ) f = ( p +s B ) } u. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } ) a = ( i +s C ) <-> ( E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) \/ E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) ) ) : No typesetting found for |- ( E. i e. ( { f | E. p e. ( _Right ` A ) f = ( p +s B ) } u. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } ) a = ( i +s C ) <-> ( E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) \/ E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) ) ) with typecode |-
91	90	abbii	Could not format { a | E. i e. ( { f | E. p e. ( _Right ` A ) f = ( p +s B ) } u. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } ) a = ( i +s C ) } = { a | ( E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) \/ E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) ) } : No typesetting found for |- { a | E. i e. ( { f | E. p e. ( _Right ` A ) f = ( p +s B ) } u. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } ) a = ( i +s C ) } = { a | ( E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) \/ E. q e. ( _Right ` B ) a = ( ( A +s q ) +s C ) ) } with typecode |-
92	57 61 91	3eqtr4ri	Could not format { a | E. i e. ( { f | E. p e. ( _Right ` A ) f = ( p +s B ) } u. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } ) a = ( i +s C ) } = ( { a | E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) } u. { b | E. q e. ( _Right ` B ) b = ( ( A +s q ) +s C ) } ) : No typesetting found for |- { a | E. i e. ( { f | E. p e. ( _Right ` A ) f = ( p +s B ) } u. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } ) a = ( i +s C ) } = ( { a | E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) } u. { b | E. q e. ( _Right ` B ) b = ( ( A +s q ) +s C ) } ) with typecode |-
93	92	uneq1i	Could not format ( { a | E. i e. ( { f | E. p e. ( _Right ` A ) f = ( p +s B ) } u. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } ) a = ( i +s C ) } u. { c | E. r e. ( _Right ` C ) c = ( ( A +s B ) +s r ) } ) = ( ( { a | E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) } u. { b | E. q e. ( _Right ` B ) b = ( ( A +s q ) +s C ) } ) u. { c | E. r e. ( _Right ` C ) c = ( ( A +s B ) +s r ) } ) : No typesetting found for |- ( { a | E. i e. ( { f | E. p e. ( _Right ` A ) f = ( p +s B ) } u. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } ) a = ( i +s C ) } u. { c | E. r e. ( _Right ` C ) c = ( ( A +s B ) +s r ) } ) = ( ( { a | E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) } u. { b | E. q e. ( _Right ` B ) b = ( ( A +s q ) +s C ) } ) u. { c | E. r e. ( _Right ` C ) c = ( ( A +s B ) +s r ) } ) with typecode |-
94	56 93	oveq12i	Could not format ( ( { y | E. h e. ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) y = ( h +s C ) } u. { w | E. n e. ( _Left ` C ) w = ( ( A +s B ) +s n ) } ) |s ( { a | E. i e. ( { f | E. p e. ( _Right ` A ) f = ( p +s B ) } u. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } ) a = ( i +s C ) } u. { c | E. r e. ( _Right ` C ) c = ( ( A +s B ) +s r ) } ) ) = ( ( ( { y | E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) } u. { z | E. m e. ( _Left ` B ) z = ( ( A +s m ) +s C ) } ) u. { w | E. n e. ( _Left ` C ) w = ( ( A +s B ) +s n ) } ) |s ( ( { a | E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) } u. { b | E. q e. ( _Right ` B ) b = ( ( A +s q ) +s C ) } ) u. { c | E. r e. ( _Right ` C ) c = ( ( A +s B ) +s r ) } ) ) : No typesetting found for |- ( ( { y | E. h e. ( { d | E. l e. ( _Left ` A ) d = ( l +s B ) } u. { e | E. m e. ( _Left ` B ) e = ( A +s m ) } ) y = ( h +s C ) } u. { w | E. n e. ( _Left ` C ) w = ( ( A +s B ) +s n ) } ) |s ( { a | E. i e. ( { f | E. p e. ( _Right ` A ) f = ( p +s B ) } u. { g | E. q e. ( _Right ` B ) g = ( A +s q ) } ) a = ( i +s C ) } u. { c | E. r e. ( _Right ` C ) c = ( ( A +s B ) +s r ) } ) ) = ( ( ( { y | E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) } u. { z | E. m e. ( _Left ` B ) z = ( ( A +s m ) +s C ) } ) u. { w | E. n e. ( _Left ` C ) w = ( ( A +s B ) +s n ) } ) |s ( ( { a | E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) } u. { b | E. q e. ( _Right ` B ) b = ( ( A +s q ) +s C ) } ) u. { c | E. r e. ( _Right ` C ) c = ( ( A +s B ) +s r ) } ) ) with typecode |-
95	19 94	eqtrdi	Could not format ( ph -> ( ( A +s B ) +s C ) = ( ( ( { y | E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) } u. { z | E. m e. ( _Left ` B ) z = ( ( A +s m ) +s C ) } ) u. { w | E. n e. ( _Left ` C ) w = ( ( A +s B ) +s n ) } ) |s ( ( { a | E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) } u. { b | E. q e. ( _Right ` B ) b = ( ( A +s q ) +s C ) } ) u. { c | E. r e. ( _Right ` C ) c = ( ( A +s B ) +s r ) } ) ) ) : No typesetting found for |- ( ph -> ( ( A +s B ) +s C ) = ( ( ( { y | E. l e. ( _Left ` A ) y = ( ( l +s B ) +s C ) } u. { z | E. m e. ( _Left ` B ) z = ( ( A +s m ) +s C ) } ) u. { w | E. n e. ( _Left ` C ) w = ( ( A +s B ) +s n ) } ) |s ( ( { a | E. p e. ( _Right ` A ) a = ( ( p +s B ) +s C ) } u. { b | E. q e. ( _Right ` B ) b = ( ( A +s q ) +s C ) } ) u. { c | E. r e. ( _Right ` C ) c = ( ( A +s B ) +s r ) } ) ) ) with typecode |-