Theorem addsasslem2

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