Theorem addsproplem2

Description: Lemma for surreal addition properties. When proving closure for operations defined using norec and norec2 , it is a strictly stronger statement to say that the cut defined is actually a cut than it is to say that the operation is closed. We will often prove this stronger statement. Here, we do so for the cut involved in surreal addition. (Contributed by Scott Fenton, 21-Jan-2025)

	Ref	Expression
Hypotheses	addsproplem.1	No typesetting found for |- ( ph -> A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
	addsproplem2.2	$$⊢\phi \to X\in \mathrm{No}$$
	addsproplem2.3	$$⊢\phi \to Y\in \mathrm{No}$$
Assertion	addsproplem2	Could not format assertion : No typesetting found for |- ( ph -> ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <

Proof

Step	Hyp	Ref	Expression
1		addsproplem.1	Could not format ( ph -> A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
2		addsproplem2.2	$$⊢\phi \to X\in \mathrm{No}$$
3		addsproplem2.3	$$⊢\phi \to Y\in \mathrm{No}$$
4		fvex	Could not format ( _Left ` X ) e. _V : No typesetting found for |- ( _Left ` X ) e. _V with typecode |-
5	4	abrexex	Could not format { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } e. _V : No typesetting found for |- { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } e. _V with typecode |-
6	5	a1i	Could not format ( ph -> { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } e. _V ) : No typesetting found for |- ( ph -> { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } e. _V ) with typecode |-
7		fvex	Could not format ( _Left ` Y ) e. _V : No typesetting found for |- ( _Left ` Y ) e. _V with typecode |-
8	7	abrexex	Could not format { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } e. _V : No typesetting found for |- { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } e. _V with typecode |-
9	8	a1i	Could not format ( ph -> { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } e. _V ) : No typesetting found for |- ( ph -> { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } e. _V ) with typecode |-
10	6 9	unexd	Could not format ( ph -> ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) e. _V ) : No typesetting found for |- ( ph -> ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) e. _V ) with typecode |-
11		fvex	Could not format ( _Right ` X ) e. _V : No typesetting found for |- ( _Right ` X ) e. _V with typecode |-
12	11	abrexex	Could not format { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } e. _V : No typesetting found for |- { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } e. _V with typecode |-
13	12	a1i	Could not format ( ph -> { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } e. _V ) : No typesetting found for |- ( ph -> { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } e. _V ) with typecode |-
14		fvex	Could not format ( _Right ` Y ) e. _V : No typesetting found for |- ( _Right ` Y ) e. _V with typecode |-
15	14	abrexex	Could not format { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } e. _V : No typesetting found for |- { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } e. _V with typecode |-
16	15	a1i	Could not format ( ph -> { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } e. _V ) : No typesetting found for |- ( ph -> { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } e. _V ) with typecode |-
17	13 16	unexd	Could not format ( ph -> ( { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) e. _V ) : No typesetting found for |- ( ph -> ( { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) e. _V ) with typecode |-
18	1	adantr	Could not format ( ( ph /\ l e. ( _Left ` X ) ) -> A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
19		leftssno	Could not format ( _Left ` X ) C_ No : No typesetting found for |- ( _Left ` X ) C_ No with typecode |-
20	19	sseli	Could not format ( l e. ( _Left ` X ) -> l e. No ) : No typesetting found for |- ( l e. ( _Left ` X ) -> l e. No ) with typecode |-
21	20	adantl	Could not format ( ( ph /\ l e. ( _Left ` X ) ) -> l e. No ) : No typesetting found for |- ( ( ph /\ l e. ( _Left ` X ) ) -> l e. No ) with typecode |-
22	3	adantr	Could not format ( ( ph /\ l e. ( _Left ` X ) ) -> Y e. No ) : No typesetting found for |- ( ( ph /\ l e. ( _Left ` X ) ) -> Y e. No ) with typecode |-
23		0sno	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
24	23	a1i	Could not format ( ( ph /\ l e. ( _Left ` X ) ) -> 0s e. No ) : No typesetting found for |- ( ( ph /\ l e. ( _Left ` X ) ) -> 0s e. No ) with typecode |-
25		bday0s	Could not format ( bday ` 0s ) = (/) : No typesetting found for |- ( bday ` 0s ) = (/) with typecode |-
26	25	oveq2i	Could not format ( ( bday ` l ) +no ( bday ` 0s ) ) = ( ( bday ` l ) +no (/) ) : No typesetting found for |- ( ( bday ` l ) +no ( bday ` 0s ) ) = ( ( bday ` l ) +no (/) ) with typecode |-
27		bdayelon	$$⊢\mathrm{bday}\left(l\right)\in \mathrm{On}$$
28		naddrid	Could not format ( ( bday ` l ) e. On -> ( ( bday ` l ) +no (/) ) = ( bday ` l ) ) : No typesetting found for |- ( ( bday ` l ) e. On -> ( ( bday ` l ) +no (/) ) = ( bday ` l ) ) with typecode |-
29	27 28	ax-mp	Could not format ( ( bday ` l ) +no (/) ) = ( bday ` l ) : No typesetting found for |- ( ( bday ` l ) +no (/) ) = ( bday ` l ) with typecode |-
30	26 29	eqtri	Could not format ( ( bday ` l ) +no ( bday ` 0s ) ) = ( bday ` l ) : No typesetting found for |- ( ( bday ` l ) +no ( bday ` 0s ) ) = ( bday ` l ) with typecode |-
31	30	uneq2i	Could not format ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( ( bday ` l ) +no ( bday ` 0s ) ) ) = ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( bday ` l ) ) : No typesetting found for |- ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( ( bday ` l ) +no ( bday ` 0s ) ) ) = ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( bday ` l ) ) with typecode |-
32		bdayelon	$$⊢\mathrm{bday}\left(Y\right)\in \mathrm{On}$$
33		naddword1	Could not format ( ( ( bday ` l ) e. On /\ ( bday ` Y ) e. On ) -> ( bday ` l ) C_ ( ( bday ` l ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ( bday ` l ) e. On /\ ( bday ` Y ) e. On ) -> ( bday ` l ) C_ ( ( bday ` l ) +no ( bday ` Y ) ) ) with typecode |-
34	27 32 33	mp2an	Could not format ( bday ` l ) C_ ( ( bday ` l ) +no ( bday ` Y ) ) : No typesetting found for |- ( bday ` l ) C_ ( ( bday ` l ) +no ( bday ` Y ) ) with typecode |-
35		ssequn2	Could not format ( ( bday ` l ) C_ ( ( bday ` l ) +no ( bday ` Y ) ) <-> ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( bday ` l ) ) = ( ( bday ` l ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( bday ` l ) C_ ( ( bday ` l ) +no ( bday ` Y ) ) <-> ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( bday ` l ) ) = ( ( bday ` l ) +no ( bday ` Y ) ) ) with typecode |-
36	34 35	mpbi	Could not format ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( bday ` l ) ) = ( ( bday ` l ) +no ( bday ` Y ) ) : No typesetting found for |- ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( bday ` l ) ) = ( ( bday ` l ) +no ( bday ` Y ) ) with typecode |-
37	31 36	eqtri	Could not format ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( ( bday ` l ) +no ( bday ` 0s ) ) ) = ( ( bday ` l ) +no ( bday ` Y ) ) : No typesetting found for |- ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( ( bday ` l ) +no ( bday ` 0s ) ) ) = ( ( bday ` l ) +no ( bday ` Y ) ) with typecode |-
38		leftssold	Could not format ( _Left ` X ) C_ ( _Old ` ( bday ` X ) ) : No typesetting found for |- ( _Left ` X ) C_ ( _Old ` ( bday ` X ) ) with typecode |-
39	38	sseli	Could not format ( l e. ( _Left ` X ) -> l e. ( _Old ` ( bday ` X ) ) ) : No typesetting found for |- ( l e. ( _Left ` X ) -> l e. ( _Old ` ( bday ` X ) ) ) with typecode |-
40		bdayelon	$$⊢\mathrm{bday}\left(X\right)\in \mathrm{On}$$
41		oldbday	$$⊢\left(\mathrm{bday}\left(X\right)\in \mathrm{On}\wedge l\in \mathrm{No}\right)\to \left(l\in \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\leftrightarrow \mathrm{bday}\left(l\right)\in \mathrm{bday}\left(X\right)\right)$$
42	40 20 41	sylancr	Could not format ( l e. ( _Left ` X ) -> ( l e. ( _Old ` ( bday ` X ) ) <-> ( bday ` l ) e. ( bday ` X ) ) ) : No typesetting found for |- ( l e. ( _Left ` X ) -> ( l e. ( _Old ` ( bday ` X ) ) <-> ( bday ` l ) e. ( bday ` X ) ) ) with typecode |-
43	39 42	mpbid	Could not format ( l e. ( _Left ` X ) -> ( bday ` l ) e. ( bday ` X ) ) : No typesetting found for |- ( l e. ( _Left ` X ) -> ( bday ` l ) e. ( bday ` X ) ) with typecode |-
44		naddel1	Could not format ( ( ( bday ` l ) e. On /\ ( bday ` X ) e. On /\ ( bday ` Y ) e. On ) -> ( ( bday ` l ) e. ( bday ` X ) <-> ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) : No typesetting found for |- ( ( ( bday ` l ) e. On /\ ( bday ` X ) e. On /\ ( bday ` Y ) e. On ) -> ( ( bday ` l ) e. ( bday ` X ) <-> ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) with typecode |-
45	27 40 32 44	mp3an	Could not format ( ( bday ` l ) e. ( bday ` X ) <-> ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( bday ` l ) e. ( bday ` X ) <-> ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
46	43 45	sylib	Could not format ( l e. ( _Left ` X ) -> ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( l e. ( _Left ` X ) -> ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
47	46	adantl	Could not format ( ( ph /\ l e. ( _Left ` X ) ) -> ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ph /\ l e. ( _Left ` X ) ) -> ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
48		elun1	Could not format ( ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
49	47 48	syl	Could not format ( ( ph /\ l e. ( _Left ` X ) ) -> ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ph /\ l e. ( _Left ` X ) ) -> ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
50	37 49	eqeltrid	Could not format ( ( ph /\ l e. ( _Left ` X ) ) -> ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( ( bday ` l ) +no ( bday ` 0s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ph /\ l e. ( _Left ` X ) ) -> ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( ( bday ` l ) +no ( bday ` 0s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
51	18 21 22 24 50	addsproplem1	Could not format ( ( ph /\ l e. ( _Left ` X ) ) -> ( ( l +s Y ) e. No /\ ( Y ( Y +s l ) ( ( l +s Y ) e. No /\ ( Y ( Y +s l )
52	51	simpld	Could not format ( ( ph /\ l e. ( _Left ` X ) ) -> ( l +s Y ) e. No ) : No typesetting found for |- ( ( ph /\ l e. ( _Left ` X ) ) -> ( l +s Y ) e. No ) with typecode |-
53		eleq1a	Could not format ( ( l +s Y ) e. No -> ( p = ( l +s Y ) -> p e. No ) ) : No typesetting found for |- ( ( l +s Y ) e. No -> ( p = ( l +s Y ) -> p e. No ) ) with typecode |-
54	52 53	syl	Could not format ( ( ph /\ l e. ( _Left ` X ) ) -> ( p = ( l +s Y ) -> p e. No ) ) : No typesetting found for |- ( ( ph /\ l e. ( _Left ` X ) ) -> ( p = ( l +s Y ) -> p e. No ) ) with typecode |-
55	54	rexlimdva	Could not format ( ph -> ( E. l e. ( _Left ` X ) p = ( l +s Y ) -> p e. No ) ) : No typesetting found for |- ( ph -> ( E. l e. ( _Left ` X ) p = ( l +s Y ) -> p e. No ) ) with typecode |-
56	55	abssdv	Could not format ( ph -> { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } C_ No ) : No typesetting found for |- ( ph -> { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } C_ No ) with typecode |-
57	1	adantr	Could not format ( ( ph /\ m e. ( _Left ` Y ) ) -> A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
58	2	adantr	Could not format ( ( ph /\ m e. ( _Left ` Y ) ) -> X e. No ) : No typesetting found for |- ( ( ph /\ m e. ( _Left ` Y ) ) -> X e. No ) with typecode |-
59		leftssno	Could not format ( _Left ` Y ) C_ No : No typesetting found for |- ( _Left ` Y ) C_ No with typecode |-
60	59	sseli	Could not format ( m e. ( _Left ` Y ) -> m e. No ) : No typesetting found for |- ( m e. ( _Left ` Y ) -> m e. No ) with typecode |-
61	60	adantl	Could not format ( ( ph /\ m e. ( _Left ` Y ) ) -> m e. No ) : No typesetting found for |- ( ( ph /\ m e. ( _Left ` Y ) ) -> m e. No ) with typecode |-
62	23	a1i	Could not format ( ( ph /\ m e. ( _Left ` Y ) ) -> 0s e. No ) : No typesetting found for |- ( ( ph /\ m e. ( _Left ` Y ) ) -> 0s e. No ) with typecode |-
63	25	oveq2i	Could not format ( ( bday ` X ) +no ( bday ` 0s ) ) = ( ( bday ` X ) +no (/) ) : No typesetting found for |- ( ( bday ` X ) +no ( bday ` 0s ) ) = ( ( bday ` X ) +no (/) ) with typecode |-
64		naddrid	Could not format ( ( bday ` X ) e. On -> ( ( bday ` X ) +no (/) ) = ( bday ` X ) ) : No typesetting found for |- ( ( bday ` X ) e. On -> ( ( bday ` X ) +no (/) ) = ( bday ` X ) ) with typecode |-
65	40 64	ax-mp	Could not format ( ( bday ` X ) +no (/) ) = ( bday ` X ) : No typesetting found for |- ( ( bday ` X ) +no (/) ) = ( bday ` X ) with typecode |-
66	63 65	eqtri	Could not format ( ( bday ` X ) +no ( bday ` 0s ) ) = ( bday ` X ) : No typesetting found for |- ( ( bday ` X ) +no ( bday ` 0s ) ) = ( bday ` X ) with typecode |-
67	66	uneq2i	Could not format ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` 0s ) ) ) = ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( bday ` X ) ) : No typesetting found for |- ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` 0s ) ) ) = ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( bday ` X ) ) with typecode |-
68		bdayelon	$$⊢\mathrm{bday}\left(m\right)\in \mathrm{On}$$
69		naddword1	Could not format ( ( ( bday ` X ) e. On /\ ( bday ` m ) e. On ) -> ( bday ` X ) C_ ( ( bday ` X ) +no ( bday ` m ) ) ) : No typesetting found for |- ( ( ( bday ` X ) e. On /\ ( bday ` m ) e. On ) -> ( bday ` X ) C_ ( ( bday ` X ) +no ( bday ` m ) ) ) with typecode |-
70	40 68 69	mp2an	Could not format ( bday ` X ) C_ ( ( bday ` X ) +no ( bday ` m ) ) : No typesetting found for |- ( bday ` X ) C_ ( ( bday ` X ) +no ( bday ` m ) ) with typecode |-
71		ssequn2	Could not format ( ( bday ` X ) C_ ( ( bday ` X ) +no ( bday ` m ) ) <-> ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( bday ` X ) ) = ( ( bday ` X ) +no ( bday ` m ) ) ) : No typesetting found for |- ( ( bday ` X ) C_ ( ( bday ` X ) +no ( bday ` m ) ) <-> ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( bday ` X ) ) = ( ( bday ` X ) +no ( bday ` m ) ) ) with typecode |-
72	70 71	mpbi	Could not format ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( bday ` X ) ) = ( ( bday ` X ) +no ( bday ` m ) ) : No typesetting found for |- ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( bday ` X ) ) = ( ( bday ` X ) +no ( bday ` m ) ) with typecode |-
73	67 72	eqtri	Could not format ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` 0s ) ) ) = ( ( bday ` X ) +no ( bday ` m ) ) : No typesetting found for |- ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` 0s ) ) ) = ( ( bday ` X ) +no ( bday ` m ) ) with typecode |-
74		leftssold	Could not format ( _Left ` Y ) C_ ( _Old ` ( bday ` Y ) ) : No typesetting found for |- ( _Left ` Y ) C_ ( _Old ` ( bday ` Y ) ) with typecode |-
75	74	sseli	Could not format ( m e. ( _Left ` Y ) -> m e. ( _Old ` ( bday ` Y ) ) ) : No typesetting found for |- ( m e. ( _Left ` Y ) -> m e. ( _Old ` ( bday ` Y ) ) ) with typecode |-
76		oldbday	$$⊢\left(\mathrm{bday}\left(Y\right)\in \mathrm{On}\wedge m\in \mathrm{No}\right)\to \left(m\in \mathrm{Old}\left(\mathrm{bday}\left(Y\right)\right)\leftrightarrow \mathrm{bday}\left(m\right)\in \mathrm{bday}\left(Y\right)\right)$$
77	32 60 76	sylancr	Could not format ( m e. ( _Left ` Y ) -> ( m e. ( _Old ` ( bday ` Y ) ) <-> ( bday ` m ) e. ( bday ` Y ) ) ) : No typesetting found for |- ( m e. ( _Left ` Y ) -> ( m e. ( _Old ` ( bday ` Y ) ) <-> ( bday ` m ) e. ( bday ` Y ) ) ) with typecode |-
78	75 77	mpbid	Could not format ( m e. ( _Left ` Y ) -> ( bday ` m ) e. ( bday ` Y ) ) : No typesetting found for |- ( m e. ( _Left ` Y ) -> ( bday ` m ) e. ( bday ` Y ) ) with typecode |-
79		naddel2	Could not format ( ( ( bday ` m ) e. On /\ ( bday ` Y ) e. On /\ ( bday ` X ) e. On ) -> ( ( bday ` m ) e. ( bday ` Y ) <-> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) : No typesetting found for |- ( ( ( bday ` m ) e. On /\ ( bday ` Y ) e. On /\ ( bday ` X ) e. On ) -> ( ( bday ` m ) e. ( bday ` Y ) <-> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) with typecode |-
80	68 32 40 79	mp3an	Could not format ( ( bday ` m ) e. ( bday ` Y ) <-> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( bday ` m ) e. ( bday ` Y ) <-> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
81	78 80	sylib	Could not format ( m e. ( _Left ` Y ) -> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( m e. ( _Left ` Y ) -> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
82	81	adantl	Could not format ( ( ph /\ m e. ( _Left ` Y ) ) -> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ph /\ m e. ( _Left ` Y ) ) -> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
83		elun1	Could not format ( ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
84	82 83	syl	Could not format ( ( ph /\ m e. ( _Left ` Y ) ) -> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ph /\ m e. ( _Left ` Y ) ) -> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
85	73 84	eqeltrid	Could not format ( ( ph /\ m e. ( _Left ` Y ) ) -> ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` 0s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ph /\ m e. ( _Left ` Y ) ) -> ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` 0s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
86	57 58 61 62 85	addsproplem1	Could not format ( ( ph /\ m e. ( _Left ` Y ) ) -> ( ( X +s m ) e. No /\ ( m ( m +s X ) ( ( X +s m ) e. No /\ ( m ( m +s X )
87	86	simpld	Could not format ( ( ph /\ m e. ( _Left ` Y ) ) -> ( X +s m ) e. No ) : No typesetting found for |- ( ( ph /\ m e. ( _Left ` Y ) ) -> ( X +s m ) e. No ) with typecode |-
88		eleq1a	Could not format ( ( X +s m ) e. No -> ( q = ( X +s m ) -> q e. No ) ) : No typesetting found for |- ( ( X +s m ) e. No -> ( q = ( X +s m ) -> q e. No ) ) with typecode |-
89	87 88	syl	Could not format ( ( ph /\ m e. ( _Left ` Y ) ) -> ( q = ( X +s m ) -> q e. No ) ) : No typesetting found for |- ( ( ph /\ m e. ( _Left ` Y ) ) -> ( q = ( X +s m ) -> q e. No ) ) with typecode |-
90	89	rexlimdva	Could not format ( ph -> ( E. m e. ( _Left ` Y ) q = ( X +s m ) -> q e. No ) ) : No typesetting found for |- ( ph -> ( E. m e. ( _Left ` Y ) q = ( X +s m ) -> q e. No ) ) with typecode |-
91	90	abssdv	Could not format ( ph -> { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } C_ No ) : No typesetting found for |- ( ph -> { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } C_ No ) with typecode |-
92	56 91	unssd	Could not format ( ph -> ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) C_ No ) : No typesetting found for |- ( ph -> ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) C_ No ) with typecode |-
93	1	adantr	Could not format ( ( ph /\ r e. ( _Right ` X ) ) -> A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
94		rightssno	Could not format ( _Right ` X ) C_ No : No typesetting found for |- ( _Right ` X ) C_ No with typecode |-
95	94	sseli	Could not format ( r e. ( _Right ` X ) -> r e. No ) : No typesetting found for |- ( r e. ( _Right ` X ) -> r e. No ) with typecode |-
96	95	adantl	Could not format ( ( ph /\ r e. ( _Right ` X ) ) -> r e. No ) : No typesetting found for |- ( ( ph /\ r e. ( _Right ` X ) ) -> r e. No ) with typecode |-
97	3	adantr	Could not format ( ( ph /\ r e. ( _Right ` X ) ) -> Y e. No ) : No typesetting found for |- ( ( ph /\ r e. ( _Right ` X ) ) -> Y e. No ) with typecode |-
98	23	a1i	Could not format ( ( ph /\ r e. ( _Right ` X ) ) -> 0s e. No ) : No typesetting found for |- ( ( ph /\ r e. ( _Right ` X ) ) -> 0s e. No ) with typecode |-
99	25	oveq2i	Could not format ( ( bday ` r ) +no ( bday ` 0s ) ) = ( ( bday ` r ) +no (/) ) : No typesetting found for |- ( ( bday ` r ) +no ( bday ` 0s ) ) = ( ( bday ` r ) +no (/) ) with typecode |-
100		bdayelon	$$⊢\mathrm{bday}\left(r\right)\in \mathrm{On}$$
101		naddrid	Could not format ( ( bday ` r ) e. On -> ( ( bday ` r ) +no (/) ) = ( bday ` r ) ) : No typesetting found for |- ( ( bday ` r ) e. On -> ( ( bday ` r ) +no (/) ) = ( bday ` r ) ) with typecode |-
102	100 101	ax-mp	Could not format ( ( bday ` r ) +no (/) ) = ( bday ` r ) : No typesetting found for |- ( ( bday ` r ) +no (/) ) = ( bday ` r ) with typecode |-
103	99 102	eqtri	Could not format ( ( bday ` r ) +no ( bday ` 0s ) ) = ( bday ` r ) : No typesetting found for |- ( ( bday ` r ) +no ( bday ` 0s ) ) = ( bday ` r ) with typecode |-
104	103	uneq2i	Could not format ( ( ( bday ` r ) +no ( bday ` Y ) ) u. ( ( bday ` r ) +no ( bday ` 0s ) ) ) = ( ( ( bday ` r ) +no ( bday ` Y ) ) u. ( bday ` r ) ) : No typesetting found for |- ( ( ( bday ` r ) +no ( bday ` Y ) ) u. ( ( bday ` r ) +no ( bday ` 0s ) ) ) = ( ( ( bday ` r ) +no ( bday ` Y ) ) u. ( bday ` r ) ) with typecode |-
105		naddword1	Could not format ( ( ( bday ` r ) e. On /\ ( bday ` Y ) e. On ) -> ( bday ` r ) C_ ( ( bday ` r ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ( bday ` r ) e. On /\ ( bday ` Y ) e. On ) -> ( bday ` r ) C_ ( ( bday ` r ) +no ( bday ` Y ) ) ) with typecode |-
106	100 32 105	mp2an	Could not format ( bday ` r ) C_ ( ( bday ` r ) +no ( bday ` Y ) ) : No typesetting found for |- ( bday ` r ) C_ ( ( bday ` r ) +no ( bday ` Y ) ) with typecode |-
107		ssequn2	Could not format ( ( bday ` r ) C_ ( ( bday ` r ) +no ( bday ` Y ) ) <-> ( ( ( bday ` r ) +no ( bday ` Y ) ) u. ( bday ` r ) ) = ( ( bday ` r ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( bday ` r ) C_ ( ( bday ` r ) +no ( bday ` Y ) ) <-> ( ( ( bday ` r ) +no ( bday ` Y ) ) u. ( bday ` r ) ) = ( ( bday ` r ) +no ( bday ` Y ) ) ) with typecode |-
108	106 107	mpbi	Could not format ( ( ( bday ` r ) +no ( bday ` Y ) ) u. ( bday ` r ) ) = ( ( bday ` r ) +no ( bday ` Y ) ) : No typesetting found for |- ( ( ( bday ` r ) +no ( bday ` Y ) ) u. ( bday ` r ) ) = ( ( bday ` r ) +no ( bday ` Y ) ) with typecode |-
109	104 108	eqtri	Could not format ( ( ( bday ` r ) +no ( bday ` Y ) ) u. ( ( bday ` r ) +no ( bday ` 0s ) ) ) = ( ( bday ` r ) +no ( bday ` Y ) ) : No typesetting found for |- ( ( ( bday ` r ) +no ( bday ` Y ) ) u. ( ( bday ` r ) +no ( bday ` 0s ) ) ) = ( ( bday ` r ) +no ( bday ` Y ) ) with typecode |-
110		rightssold	Could not format ( _Right ` X ) C_ ( _Old ` ( bday ` X ) ) : No typesetting found for |- ( _Right ` X ) C_ ( _Old ` ( bday ` X ) ) with typecode |-
111	110	sseli	Could not format ( r e. ( _Right ` X ) -> r e. ( _Old ` ( bday ` X ) ) ) : No typesetting found for |- ( r e. ( _Right ` X ) -> r e. ( _Old ` ( bday ` X ) ) ) with typecode |-
112		oldbday	$$⊢\left(\mathrm{bday}\left(X\right)\in \mathrm{On}\wedge r\in \mathrm{No}\right)\to \left(r\in \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\leftrightarrow \mathrm{bday}\left(r\right)\in \mathrm{bday}\left(X\right)\right)$$
113	40 95 112	sylancr	Could not format ( r e. ( _Right ` X ) -> ( r e. ( _Old ` ( bday ` X ) ) <-> ( bday ` r ) e. ( bday ` X ) ) ) : No typesetting found for |- ( r e. ( _Right ` X ) -> ( r e. ( _Old ` ( bday ` X ) ) <-> ( bday ` r ) e. ( bday ` X ) ) ) with typecode |-
114	111 113	mpbid	Could not format ( r e. ( _Right ` X ) -> ( bday ` r ) e. ( bday ` X ) ) : No typesetting found for |- ( r e. ( _Right ` X ) -> ( bday ` r ) e. ( bday ` X ) ) with typecode |-
115		naddel1	Could not format ( ( ( bday ` r ) e. On /\ ( bday ` X ) e. On /\ ( bday ` Y ) e. On ) -> ( ( bday ` r ) e. ( bday ` X ) <-> ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) : No typesetting found for |- ( ( ( bday ` r ) e. On /\ ( bday ` X ) e. On /\ ( bday ` Y ) e. On ) -> ( ( bday ` r ) e. ( bday ` X ) <-> ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) with typecode |-
116	100 40 32 115	mp3an	Could not format ( ( bday ` r ) e. ( bday ` X ) <-> ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( bday ` r ) e. ( bday ` X ) <-> ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
117	114 116	sylib	Could not format ( r e. ( _Right ` X ) -> ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( r e. ( _Right ` X ) -> ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
118	117	adantl	Could not format ( ( ph /\ r e. ( _Right ` X ) ) -> ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ph /\ r e. ( _Right ` X ) ) -> ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
119		elun1	Could not format ( ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
120	118 119	syl	Could not format ( ( ph /\ r e. ( _Right ` X ) ) -> ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ph /\ r e. ( _Right ` X ) ) -> ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
121	109 120	eqeltrid	Could not format ( ( ph /\ r e. ( _Right ` X ) ) -> ( ( ( bday ` r ) +no ( bday ` Y ) ) u. ( ( bday ` r ) +no ( bday ` 0s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ph /\ r e. ( _Right ` X ) ) -> ( ( ( bday ` r ) +no ( bday ` Y ) ) u. ( ( bday ` r ) +no ( bday ` 0s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
122	93 96 97 98 121	addsproplem1	Could not format ( ( ph /\ r e. ( _Right ` X ) ) -> ( ( r +s Y ) e. No /\ ( Y ( Y +s r ) ( ( r +s Y ) e. No /\ ( Y ( Y +s r )
123	122	simpld	Could not format ( ( ph /\ r e. ( _Right ` X ) ) -> ( r +s Y ) e. No ) : No typesetting found for |- ( ( ph /\ r e. ( _Right ` X ) ) -> ( r +s Y ) e. No ) with typecode |-
124		eleq1a	Could not format ( ( r +s Y ) e. No -> ( w = ( r +s Y ) -> w e. No ) ) : No typesetting found for |- ( ( r +s Y ) e. No -> ( w = ( r +s Y ) -> w e. No ) ) with typecode |-
125	123 124	syl	Could not format ( ( ph /\ r e. ( _Right ` X ) ) -> ( w = ( r +s Y ) -> w e. No ) ) : No typesetting found for |- ( ( ph /\ r e. ( _Right ` X ) ) -> ( w = ( r +s Y ) -> w e. No ) ) with typecode |-
126	125	rexlimdva	Could not format ( ph -> ( E. r e. ( _Right ` X ) w = ( r +s Y ) -> w e. No ) ) : No typesetting found for |- ( ph -> ( E. r e. ( _Right ` X ) w = ( r +s Y ) -> w e. No ) ) with typecode |-
127	126	abssdv	Could not format ( ph -> { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } C_ No ) : No typesetting found for |- ( ph -> { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } C_ No ) with typecode |-
128	1	adantr	Could not format ( ( ph /\ s e. ( _Right ` Y ) ) -> A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
129	2	adantr	Could not format ( ( ph /\ s e. ( _Right ` Y ) ) -> X e. No ) : No typesetting found for |- ( ( ph /\ s e. ( _Right ` Y ) ) -> X e. No ) with typecode |-
130		rightssno	Could not format ( _Right ` Y ) C_ No : No typesetting found for |- ( _Right ` Y ) C_ No with typecode |-
131	130	sseli	Could not format ( s e. ( _Right ` Y ) -> s e. No ) : No typesetting found for |- ( s e. ( _Right ` Y ) -> s e. No ) with typecode |-
132	131	adantl	Could not format ( ( ph /\ s e. ( _Right ` Y ) ) -> s e. No ) : No typesetting found for |- ( ( ph /\ s e. ( _Right ` Y ) ) -> s e. No ) with typecode |-
133	23	a1i	Could not format ( ( ph /\ s e. ( _Right ` Y ) ) -> 0s e. No ) : No typesetting found for |- ( ( ph /\ s e. ( _Right ` Y ) ) -> 0s e. No ) with typecode |-
134	66	uneq2i	Could not format ( ( ( bday ` X ) +no ( bday ` s ) ) u. ( ( bday ` X ) +no ( bday ` 0s ) ) ) = ( ( ( bday ` X ) +no ( bday ` s ) ) u. ( bday ` X ) ) : No typesetting found for |- ( ( ( bday ` X ) +no ( bday ` s ) ) u. ( ( bday ` X ) +no ( bday ` 0s ) ) ) = ( ( ( bday ` X ) +no ( bday ` s ) ) u. ( bday ` X ) ) with typecode |-
135		bdayelon	$$⊢\mathrm{bday}\left(s\right)\in \mathrm{On}$$
136		naddword1	Could not format ( ( ( bday ` X ) e. On /\ ( bday ` s ) e. On ) -> ( bday ` X ) C_ ( ( bday ` X ) +no ( bday ` s ) ) ) : No typesetting found for |- ( ( ( bday ` X ) e. On /\ ( bday ` s ) e. On ) -> ( bday ` X ) C_ ( ( bday ` X ) +no ( bday ` s ) ) ) with typecode |-
137	40 135 136	mp2an	Could not format ( bday ` X ) C_ ( ( bday ` X ) +no ( bday ` s ) ) : No typesetting found for |- ( bday ` X ) C_ ( ( bday ` X ) +no ( bday ` s ) ) with typecode |-
138		ssequn2	Could not format ( ( bday ` X ) C_ ( ( bday ` X ) +no ( bday ` s ) ) <-> ( ( ( bday ` X ) +no ( bday ` s ) ) u. ( bday ` X ) ) = ( ( bday ` X ) +no ( bday ` s ) ) ) : No typesetting found for |- ( ( bday ` X ) C_ ( ( bday ` X ) +no ( bday ` s ) ) <-> ( ( ( bday ` X ) +no ( bday ` s ) ) u. ( bday ` X ) ) = ( ( bday ` X ) +no ( bday ` s ) ) ) with typecode |-
139	137 138	mpbi	Could not format ( ( ( bday ` X ) +no ( bday ` s ) ) u. ( bday ` X ) ) = ( ( bday ` X ) +no ( bday ` s ) ) : No typesetting found for |- ( ( ( bday ` X ) +no ( bday ` s ) ) u. ( bday ` X ) ) = ( ( bday ` X ) +no ( bday ` s ) ) with typecode |-
140	134 139	eqtri	Could not format ( ( ( bday ` X ) +no ( bday ` s ) ) u. ( ( bday ` X ) +no ( bday ` 0s ) ) ) = ( ( bday ` X ) +no ( bday ` s ) ) : No typesetting found for |- ( ( ( bday ` X ) +no ( bday ` s ) ) u. ( ( bday ` X ) +no ( bday ` 0s ) ) ) = ( ( bday ` X ) +no ( bday ` s ) ) with typecode |-
141		rightssold	Could not format ( _Right ` Y ) C_ ( _Old ` ( bday ` Y ) ) : No typesetting found for |- ( _Right ` Y ) C_ ( _Old ` ( bday ` Y ) ) with typecode |-
142	141	sseli	Could not format ( s e. ( _Right ` Y ) -> s e. ( _Old ` ( bday ` Y ) ) ) : No typesetting found for |- ( s e. ( _Right ` Y ) -> s e. ( _Old ` ( bday ` Y ) ) ) with typecode |-
143		oldbday	$$⊢\left(\mathrm{bday}\left(Y\right)\in \mathrm{On}\wedge s\in \mathrm{No}\right)\to \left(s\in \mathrm{Old}\left(\mathrm{bday}\left(Y\right)\right)\leftrightarrow \mathrm{bday}\left(s\right)\in \mathrm{bday}\left(Y\right)\right)$$
144	32 131 143	sylancr	Could not format ( s e. ( _Right ` Y ) -> ( s e. ( _Old ` ( bday ` Y ) ) <-> ( bday ` s ) e. ( bday ` Y ) ) ) : No typesetting found for |- ( s e. ( _Right ` Y ) -> ( s e. ( _Old ` ( bday ` Y ) ) <-> ( bday ` s ) e. ( bday ` Y ) ) ) with typecode |-
145	142 144	mpbid	Could not format ( s e. ( _Right ` Y ) -> ( bday ` s ) e. ( bday ` Y ) ) : No typesetting found for |- ( s e. ( _Right ` Y ) -> ( bday ` s ) e. ( bday ` Y ) ) with typecode |-
146		naddel2	Could not format ( ( ( bday ` s ) e. On /\ ( bday ` Y ) e. On /\ ( bday ` X ) e. On ) -> ( ( bday ` s ) e. ( bday ` Y ) <-> ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) : No typesetting found for |- ( ( ( bday ` s ) e. On /\ ( bday ` Y ) e. On /\ ( bday ` X ) e. On ) -> ( ( bday ` s ) e. ( bday ` Y ) <-> ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) with typecode |-
147	135 32 40 146	mp3an	Could not format ( ( bday ` s ) e. ( bday ` Y ) <-> ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( bday ` s ) e. ( bday ` Y ) <-> ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
148	145 147	sylib	Could not format ( s e. ( _Right ` Y ) -> ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( s e. ( _Right ` Y ) -> ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
149	148	adantl	Could not format ( ( ph /\ s e. ( _Right ` Y ) ) -> ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ph /\ s e. ( _Right ` Y ) ) -> ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
150		elun1	Could not format ( ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
151	149 150	syl	Could not format ( ( ph /\ s e. ( _Right ` Y ) ) -> ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ph /\ s e. ( _Right ` Y ) ) -> ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
152	140 151	eqeltrid	Could not format ( ( ph /\ s e. ( _Right ` Y ) ) -> ( ( ( bday ` X ) +no ( bday ` s ) ) u. ( ( bday ` X ) +no ( bday ` 0s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ph /\ s e. ( _Right ` Y ) ) -> ( ( ( bday ` X ) +no ( bday ` s ) ) u. ( ( bday ` X ) +no ( bday ` 0s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
153	128 129 132 133 152	addsproplem1	Could not format ( ( ph /\ s e. ( _Right ` Y ) ) -> ( ( X +s s ) e. No /\ ( s ( s +s X ) ( ( X +s s ) e. No /\ ( s ( s +s X )
154	153	simpld	Could not format ( ( ph /\ s e. ( _Right ` Y ) ) -> ( X +s s ) e. No ) : No typesetting found for |- ( ( ph /\ s e. ( _Right ` Y ) ) -> ( X +s s ) e. No ) with typecode |-
155		eleq1a	Could not format ( ( X +s s ) e. No -> ( t = ( X +s s ) -> t e. No ) ) : No typesetting found for |- ( ( X +s s ) e. No -> ( t = ( X +s s ) -> t e. No ) ) with typecode |-
156	154 155	syl	Could not format ( ( ph /\ s e. ( _Right ` Y ) ) -> ( t = ( X +s s ) -> t e. No ) ) : No typesetting found for |- ( ( ph /\ s e. ( _Right ` Y ) ) -> ( t = ( X +s s ) -> t e. No ) ) with typecode |-
157	156	rexlimdva	Could not format ( ph -> ( E. s e. ( _Right ` Y ) t = ( X +s s ) -> t e. No ) ) : No typesetting found for |- ( ph -> ( E. s e. ( _Right ` Y ) t = ( X +s s ) -> t e. No ) ) with typecode |-
158	157	abssdv	Could not format ( ph -> { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } C_ No ) : No typesetting found for |- ( ph -> { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } C_ No ) with typecode |-
159	127 158	unssd	Could not format ( ph -> ( { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) C_ No ) : No typesetting found for |- ( ph -> ( { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) C_ No ) with typecode |-
160		elun	Could not format ( a e. ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <-> ( a e. { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } \/ a e. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) ) : No typesetting found for |- ( a e. ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <-> ( a e. { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } \/ a e. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) ) with typecode |-
161		vex	$$⊢a\in \mathrm{V}$$
162		eqeq1	Could not format ( p = a -> ( p = ( l +s Y ) <-> a = ( l +s Y ) ) ) : No typesetting found for |- ( p = a -> ( p = ( l +s Y ) <-> a = ( l +s Y ) ) ) with typecode |-
163	162	rexbidv	Could not format ( p = a -> ( E. l e. ( _Left ` X ) p = ( l +s Y ) <-> E. l e. ( _Left ` X ) a = ( l +s Y ) ) ) : No typesetting found for |- ( p = a -> ( E. l e. ( _Left ` X ) p = ( l +s Y ) <-> E. l e. ( _Left ` X ) a = ( l +s Y ) ) ) with typecode |-
164	161 163	elab	Could not format ( a e. { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } <-> E. l e. ( _Left ` X ) a = ( l +s Y ) ) : No typesetting found for |- ( a e. { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } <-> E. l e. ( _Left ` X ) a = ( l +s Y ) ) with typecode |-
165		eqeq1	Could not format ( q = a -> ( q = ( X +s m ) <-> a = ( X +s m ) ) ) : No typesetting found for |- ( q = a -> ( q = ( X +s m ) <-> a = ( X +s m ) ) ) with typecode |-
166	165	rexbidv	Could not format ( q = a -> ( E. m e. ( _Left ` Y ) q = ( X +s m ) <-> E. m e. ( _Left ` Y ) a = ( X +s m ) ) ) : No typesetting found for |- ( q = a -> ( E. m e. ( _Left ` Y ) q = ( X +s m ) <-> E. m e. ( _Left ` Y ) a = ( X +s m ) ) ) with typecode |-
167	161 166	elab	Could not format ( a e. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } <-> E. m e. ( _Left ` Y ) a = ( X +s m ) ) : No typesetting found for |- ( a e. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } <-> E. m e. ( _Left ` Y ) a = ( X +s m ) ) with typecode |-
168	164 167	orbi12i	Could not format ( ( a e. { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } \/ a e. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <-> ( E. l e. ( _Left ` X ) a = ( l +s Y ) \/ E. m e. ( _Left ` Y ) a = ( X +s m ) ) ) : No typesetting found for |- ( ( a e. { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } \/ a e. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <-> ( E. l e. ( _Left ` X ) a = ( l +s Y ) \/ E. m e. ( _Left ` Y ) a = ( X +s m ) ) ) with typecode |-
169	160 168	bitri	Could not format ( a e. ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <-> ( E. l e. ( _Left ` X ) a = ( l +s Y ) \/ E. m e. ( _Left ` Y ) a = ( X +s m ) ) ) : No typesetting found for |- ( a e. ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <-> ( E. l e. ( _Left ` X ) a = ( l +s Y ) \/ E. m e. ( _Left ` Y ) a = ( X +s m ) ) ) with typecode |-
170		elun	Could not format ( b e. ( { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) <-> ( b e. { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } \/ b e. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) ) : No typesetting found for |- ( b e. ( { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) <-> ( b e. { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } \/ b e. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) ) with typecode |-
171		vex	$$⊢b\in \mathrm{V}$$
172		eqeq1	Could not format ( w = b -> ( w = ( r +s Y ) <-> b = ( r +s Y ) ) ) : No typesetting found for |- ( w = b -> ( w = ( r +s Y ) <-> b = ( r +s Y ) ) ) with typecode |-
173	172	rexbidv	Could not format ( w = b -> ( E. r e. ( _Right ` X ) w = ( r +s Y ) <-> E. r e. ( _Right ` X ) b = ( r +s Y ) ) ) : No typesetting found for |- ( w = b -> ( E. r e. ( _Right ` X ) w = ( r +s Y ) <-> E. r e. ( _Right ` X ) b = ( r +s Y ) ) ) with typecode |-
174	171 173	elab	Could not format ( b e. { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } <-> E. r e. ( _Right ` X ) b = ( r +s Y ) ) : No typesetting found for |- ( b e. { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } <-> E. r e. ( _Right ` X ) b = ( r +s Y ) ) with typecode |-
175		eqeq1	Could not format ( t = b -> ( t = ( X +s s ) <-> b = ( X +s s ) ) ) : No typesetting found for |- ( t = b -> ( t = ( X +s s ) <-> b = ( X +s s ) ) ) with typecode |-
176	175	rexbidv	Could not format ( t = b -> ( E. s e. ( _Right ` Y ) t = ( X +s s ) <-> E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) : No typesetting found for |- ( t = b -> ( E. s e. ( _Right ` Y ) t = ( X +s s ) <-> E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) with typecode |-
177	171 176	elab	Could not format ( b e. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } <-> E. s e. ( _Right ` Y ) b = ( X +s s ) ) : No typesetting found for |- ( b e. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } <-> E. s e. ( _Right ` Y ) b = ( X +s s ) ) with typecode |-
178	174 177	orbi12i	Could not format ( ( b e. { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } \/ b e. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) <-> ( E. r e. ( _Right ` X ) b = ( r +s Y ) \/ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) : No typesetting found for |- ( ( b e. { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } \/ b e. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) <-> ( E. r e. ( _Right ` X ) b = ( r +s Y ) \/ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) with typecode |-
179	170 178	bitri	Could not format ( b e. ( { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) <-> ( E. r e. ( _Right ` X ) b = ( r +s Y ) \/ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) : No typesetting found for |- ( b e. ( { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) <-> ( E. r e. ( _Right ` X ) b = ( r +s Y ) \/ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) with typecode |-
180	169 179	anbi12i	Could not format ( ( a e. ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) /\ b e. ( { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) ) <-> ( ( E. l e. ( _Left ` X ) a = ( l +s Y ) \/ E. m e. ( _Left ` Y ) a = ( X +s m ) ) /\ ( E. r e. ( _Right ` X ) b = ( r +s Y ) \/ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) ) : No typesetting found for |- ( ( a e. ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) /\ b e. ( { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) ) <-> ( ( E. l e. ( _Left ` X ) a = ( l +s Y ) \/ E. m e. ( _Left ` Y ) a = ( X +s m ) ) /\ ( E. r e. ( _Right ` X ) b = ( r +s Y ) \/ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) ) with typecode |-
181		anddi	Could not format ( ( ( E. l e. ( _Left ` X ) a = ( l +s Y ) \/ E. m e. ( _Left ` Y ) a = ( X +s m ) ) /\ ( E. r e. ( _Right ` X ) b = ( r +s Y ) \/ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) <-> ( ( ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) \/ ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) \/ ( ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) \/ ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) ) ) : No typesetting found for |- ( ( ( E. l e. ( _Left ` X ) a = ( l +s Y ) \/ E. m e. ( _Left ` Y ) a = ( X +s m ) ) /\ ( E. r e. ( _Right ` X ) b = ( r +s Y ) \/ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) <-> ( ( ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) \/ ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) \/ ( ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) \/ ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) ) ) with typecode |-
182	180 181	bitri	Could not format ( ( a e. ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) /\ b e. ( { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) ) <-> ( ( ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) \/ ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) \/ ( ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) \/ ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) ) ) : No typesetting found for |- ( ( a e. ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) /\ b e. ( { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) ) <-> ( ( ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) \/ ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) \/ ( ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) \/ ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) ) ) with typecode |-
183		reeanv	Could not format ( E. l e. ( _Left ` X ) E. r e. ( _Right ` X ) ( a = ( l +s Y ) /\ b = ( r +s Y ) ) <-> ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) ) : No typesetting found for |- ( E. l e. ( _Left ` X ) E. r e. ( _Right ` X ) ( a = ( l +s Y ) /\ b = ( r +s Y ) ) <-> ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) ) with typecode |-
184		lltropt	Could not format ( _Left ` X ) <
185	184	a1i	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> ( _Left ` X ) < ( _Left ` X ) <
186		simprl	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> l e. ( _Left ` X ) ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> l e. ( _Left ` X ) ) with typecode |-
187		simprr	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> r e. ( _Right ` X ) ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> r e. ( _Right ` X ) ) with typecode |-
188	185 186 187	ssltsepcd	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> l l
189	1	adantr	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
190	3	adantr	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> Y e. No ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> Y e. No ) with typecode |-
191	20	ad2antrl	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> l e. No ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> l e. No ) with typecode |-
192	95	ad2antll	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> r e. No ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> r e. No ) with typecode |-
193		naddcom	Could not format ( ( ( bday ` Y ) e. On /\ ( bday ` l ) e. On ) -> ( ( bday ` Y ) +no ( bday ` l ) ) = ( ( bday ` l ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ( bday ` Y ) e. On /\ ( bday ` l ) e. On ) -> ( ( bday ` Y ) +no ( bday ` l ) ) = ( ( bday ` l ) +no ( bday ` Y ) ) ) with typecode |-
194	32 27 193	mp2an	Could not format ( ( bday ` Y ) +no ( bday ` l ) ) = ( ( bday ` l ) +no ( bday ` Y ) ) : No typesetting found for |- ( ( bday ` Y ) +no ( bday ` l ) ) = ( ( bday ` l ) +no ( bday ` Y ) ) with typecode |-
195	46	ad2antrl	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
196	194 195	eqeltrid	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` Y ) +no ( bday ` l ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` Y ) +no ( bday ` l ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
197		naddcom	Could not format ( ( ( bday ` Y ) e. On /\ ( bday ` r ) e. On ) -> ( ( bday ` Y ) +no ( bday ` r ) ) = ( ( bday ` r ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ( bday ` Y ) e. On /\ ( bday ` r ) e. On ) -> ( ( bday ` Y ) +no ( bday ` r ) ) = ( ( bday ` r ) +no ( bday ` Y ) ) ) with typecode |-
198	32 100 197	mp2an	Could not format ( ( bday ` Y ) +no ( bday ` r ) ) = ( ( bday ` r ) +no ( bday ` Y ) ) : No typesetting found for |- ( ( bday ` Y ) +no ( bday ` r ) ) = ( ( bday ` r ) +no ( bday ` Y ) ) with typecode |-
199	117	ad2antll	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
200	198 199	eqeltrid	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` Y ) +no ( bday ` r ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` Y ) +no ( bday ` r ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
201		naddcl	Could not format ( ( ( bday ` Y ) e. On /\ ( bday ` l ) e. On ) -> ( ( bday ` Y ) +no ( bday ` l ) ) e. On ) : No typesetting found for |- ( ( ( bday ` Y ) e. On /\ ( bday ` l ) e. On ) -> ( ( bday ` Y ) +no ( bday ` l ) ) e. On ) with typecode |-
202	32 27 201	mp2an	Could not format ( ( bday ` Y ) +no ( bday ` l ) ) e. On : No typesetting found for |- ( ( bday ` Y ) +no ( bday ` l ) ) e. On with typecode |-
203		naddcl	Could not format ( ( ( bday ` Y ) e. On /\ ( bday ` r ) e. On ) -> ( ( bday ` Y ) +no ( bday ` r ) ) e. On ) : No typesetting found for |- ( ( ( bday ` Y ) e. On /\ ( bday ` r ) e. On ) -> ( ( bday ` Y ) +no ( bday ` r ) ) e. On ) with typecode |-
204	32 100 203	mp2an	Could not format ( ( bday ` Y ) +no ( bday ` r ) ) e. On : No typesetting found for |- ( ( bday ` Y ) +no ( bday ` r ) ) e. On with typecode |-
205		naddcl	Could not format ( ( ( bday ` X ) e. On /\ ( bday ` Y ) e. On ) -> ( ( bday ` X ) +no ( bday ` Y ) ) e. On ) : No typesetting found for |- ( ( ( bday ` X ) e. On /\ ( bday ` Y ) e. On ) -> ( ( bday ` X ) +no ( bday ` Y ) ) e. On ) with typecode |-
206	40 32 205	mp2an	Could not format ( ( bday ` X ) +no ( bday ` Y ) ) e. On : No typesetting found for |- ( ( bday ` X ) +no ( bday ` Y ) ) e. On with typecode |-
207		onunel	Could not format ( ( ( ( bday ` Y ) +no ( bday ` l ) ) e. On /\ ( ( bday ` Y ) +no ( bday ` r ) ) e. On /\ ( ( bday ` X ) +no ( bday ` Y ) ) e. On ) -> ( ( ( ( bday ` Y ) +no ( bday ` l ) ) u. ( ( bday ` Y ) +no ( bday ` r ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` Y ) +no ( bday ` l ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` Y ) +no ( bday ` r ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` Y ) +no ( bday ` l ) ) e. On /\ ( ( bday ` Y ) +no ( bday ` r ) ) e. On /\ ( ( bday ` X ) +no ( bday ` Y ) ) e. On ) -> ( ( ( ( bday ` Y ) +no ( bday ` l ) ) u. ( ( bday ` Y ) +no ( bday ` r ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` Y ) +no ( bday ` l ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` Y ) +no ( bday ` r ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) ) with typecode |-
208	202 204 206 207	mp3an	Could not format ( ( ( ( bday ` Y ) +no ( bday ` l ) ) u. ( ( bday ` Y ) +no ( bday ` r ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` Y ) +no ( bday ` l ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` Y ) +no ( bday ` r ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` Y ) +no ( bday ` l ) ) u. ( ( bday ` Y ) +no ( bday ` r ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` Y ) +no ( bday ` l ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` Y ) +no ( bday ` r ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) with typecode |-
209	196 200 208	sylanbrc	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> ( ( ( bday ` Y ) +no ( bday ` l ) ) u. ( ( bday ` Y ) +no ( bday ` r ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> ( ( ( bday ` Y ) +no ( bday ` l ) ) u. ( ( bday ` Y ) +no ( bday ` r ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
210		elun1	Could not format ( ( ( ( bday ` Y ) +no ( bday ` l ) ) u. ( ( bday ` Y ) +no ( bday ` r ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( ( bday ` Y ) +no ( bday ` l ) ) u. ( ( bday ` Y ) +no ( bday ` r ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` Y ) +no ( bday ` l ) ) u. ( ( bday ` Y ) +no ( bday ` r ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( ( bday ` Y ) +no ( bday ` l ) ) u. ( ( bday ` Y ) +no ( bday ` r ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
211	209 210	syl	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> ( ( ( bday ` Y ) +no ( bday ` l ) ) u. ( ( bday ` Y ) +no ( bday ` r ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> ( ( ( bday ` Y ) +no ( bday ` l ) ) u. ( ( bday ` Y ) +no ( bday ` r ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
212	189 190 191 192 211	addsproplem1	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> ( ( Y +s l ) e. No /\ ( l ( l +s Y ) ( ( Y +s l ) e. No /\ ( l ( l +s Y )
213	212	simprd	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> ( l ( l +s Y ) ( l ( l +s Y )
214	188 213	mpd	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> ( l +s Y ) ( l +s Y )
215		breq12	Could not format ( ( a = ( l +s Y ) /\ b = ( r +s Y ) ) -> ( a ( l +s Y ) ( a ( l +s Y )
216	214 215	syl5ibrcom	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> ( ( a = ( l +s Y ) /\ b = ( r +s Y ) ) -> a ( ( a = ( l +s Y ) /\ b = ( r +s Y ) ) -> a
217	216	rexlimdvva	Could not format ( ph -> ( E. l e. ( _Left ` X ) E. r e. ( _Right ` X ) ( a = ( l +s Y ) /\ b = ( r +s Y ) ) -> a ( E. l e. ( _Left ` X ) E. r e. ( _Right ` X ) ( a = ( l +s Y ) /\ b = ( r +s Y ) ) -> a
218	183 217	biimtrrid	Could not format ( ph -> ( ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) -> a ( ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) -> a
219		reeanv	Could not format ( E. l e. ( _Left ` X ) E. s e. ( _Right ` Y ) ( a = ( l +s Y ) /\ b = ( X +s s ) ) <-> ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) : No typesetting found for |- ( E. l e. ( _Left ` X ) E. s e. ( _Right ` Y ) ( a = ( l +s Y ) /\ b = ( X +s s ) ) <-> ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) with typecode |-
220	52	adantrr	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( l +s Y ) e. No ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( l +s Y ) e. No ) with typecode |-
221	1	adantr	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
222	20	ad2antrl	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> l e. No ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> l e. No ) with typecode |-
223	131	ad2antll	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> s e. No ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> s e. No ) with typecode |-
224	23	a1i	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> 0s e. No ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> 0s e. No ) with typecode |-
225	30	uneq2i	Could not format ( ( ( bday ` l ) +no ( bday ` s ) ) u. ( ( bday ` l ) +no ( bday ` 0s ) ) ) = ( ( ( bday ` l ) +no ( bday ` s ) ) u. ( bday ` l ) ) : No typesetting found for |- ( ( ( bday ` l ) +no ( bday ` s ) ) u. ( ( bday ` l ) +no ( bday ` 0s ) ) ) = ( ( ( bday ` l ) +no ( bday ` s ) ) u. ( bday ` l ) ) with typecode |-
226		naddword1	Could not format ( ( ( bday ` l ) e. On /\ ( bday ` s ) e. On ) -> ( bday ` l ) C_ ( ( bday ` l ) +no ( bday ` s ) ) ) : No typesetting found for |- ( ( ( bday ` l ) e. On /\ ( bday ` s ) e. On ) -> ( bday ` l ) C_ ( ( bday ` l ) +no ( bday ` s ) ) ) with typecode |-
227	27 135 226	mp2an	Could not format ( bday ` l ) C_ ( ( bday ` l ) +no ( bday ` s ) ) : No typesetting found for |- ( bday ` l ) C_ ( ( bday ` l ) +no ( bday ` s ) ) with typecode |-
228		ssequn2	Could not format ( ( bday ` l ) C_ ( ( bday ` l ) +no ( bday ` s ) ) <-> ( ( ( bday ` l ) +no ( bday ` s ) ) u. ( bday ` l ) ) = ( ( bday ` l ) +no ( bday ` s ) ) ) : No typesetting found for |- ( ( bday ` l ) C_ ( ( bday ` l ) +no ( bday ` s ) ) <-> ( ( ( bday ` l ) +no ( bday ` s ) ) u. ( bday ` l ) ) = ( ( bday ` l ) +no ( bday ` s ) ) ) with typecode |-
229	227 228	mpbi	Could not format ( ( ( bday ` l ) +no ( bday ` s ) ) u. ( bday ` l ) ) = ( ( bday ` l ) +no ( bday ` s ) ) : No typesetting found for |- ( ( ( bday ` l ) +no ( bday ` s ) ) u. ( bday ` l ) ) = ( ( bday ` l ) +no ( bday ` s ) ) with typecode |-
230	225 229	eqtri	Could not format ( ( ( bday ` l ) +no ( bday ` s ) ) u. ( ( bday ` l ) +no ( bday ` 0s ) ) ) = ( ( bday ` l ) +no ( bday ` s ) ) : No typesetting found for |- ( ( ( bday ` l ) +no ( bday ` s ) ) u. ( ( bday ` l ) +no ( bday ` 0s ) ) ) = ( ( bday ` l ) +no ( bday ` s ) ) with typecode |-
231		naddel1	Could not format ( ( ( bday ` l ) e. On /\ ( bday ` X ) e. On /\ ( bday ` s ) e. On ) -> ( ( bday ` l ) e. ( bday ` X ) <-> ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` s ) ) ) ) : No typesetting found for |- ( ( ( bday ` l ) e. On /\ ( bday ` X ) e. On /\ ( bday ` s ) e. On ) -> ( ( bday ` l ) e. ( bday ` X ) <-> ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` s ) ) ) ) with typecode |-
232	27 40 135 231	mp3an	Could not format ( ( bday ` l ) e. ( bday ` X ) <-> ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` s ) ) ) : No typesetting found for |- ( ( bday ` l ) e. ( bday ` X ) <-> ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` s ) ) ) with typecode |-
233	43 232	sylib	Could not format ( l e. ( _Left ` X ) -> ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` s ) ) ) : No typesetting found for |- ( l e. ( _Left ` X ) -> ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` s ) ) ) with typecode |-
234	233	ad2antrl	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` s ) ) ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` s ) ) ) with typecode |-
235	148	ad2antll	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
236		ontr1	Could not format ( ( ( bday ` X ) +no ( bday ` Y ) ) e. On -> ( ( ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` s ) ) /\ ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) -> ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) : No typesetting found for |- ( ( ( bday ` X ) +no ( bday ` Y ) ) e. On -> ( ( ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` s ) ) /\ ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) -> ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) with typecode |-
237	206 236	ax-mp	Could not format ( ( ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` s ) ) /\ ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) -> ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` s ) ) /\ ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) -> ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
238	234 235 237	syl2anc	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
239		elun1	Could not format ( ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
240	238 239	syl	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
241	230 240	eqeltrid	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( ( bday ` l ) +no ( bday ` s ) ) u. ( ( bday ` l ) +no ( bday ` 0s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( ( bday ` l ) +no ( bday ` s ) ) u. ( ( bday ` l ) +no ( bday ` 0s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
242	221 222 223 224 241	addsproplem1	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( l +s s ) e. No /\ ( s ( s +s l ) ( ( l +s s ) e. No /\ ( s ( s +s l )
243	242	simpld	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( l +s s ) e. No ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( l +s s ) e. No ) with typecode |-
244	154	adantrl	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( X +s s ) e. No ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( X +s s ) e. No ) with typecode |-
245		rightval	Could not format ( _Right ` Y ) = { s e. ( _Old ` ( bday ` Y ) ) | Y
246	245	reqabi	Could not format ( s e. ( _Right ` Y ) <-> ( s e. ( _Old ` ( bday ` Y ) ) /\ Y ( s e. ( _Old ` ( bday ` Y ) ) /\ Y
247	246	simprbi	Could not format ( s e. ( _Right ` Y ) -> Y Y
248	247	ad2antll	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> Y Y
249	3	adantr	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> Y e. No ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> Y e. No ) with typecode |-
250	46	ad2antrl	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
251		naddcl	Could not format ( ( ( bday ` l ) e. On /\ ( bday ` Y ) e. On ) -> ( ( bday ` l ) +no ( bday ` Y ) ) e. On ) : No typesetting found for |- ( ( ( bday ` l ) e. On /\ ( bday ` Y ) e. On ) -> ( ( bday ` l ) +no ( bday ` Y ) ) e. On ) with typecode |-
252	27 32 251	mp2an	Could not format ( ( bday ` l ) +no ( bday ` Y ) ) e. On : No typesetting found for |- ( ( bday ` l ) +no ( bday ` Y ) ) e. On with typecode |-
253		naddcl	Could not format ( ( ( bday ` l ) e. On /\ ( bday ` s ) e. On ) -> ( ( bday ` l ) +no ( bday ` s ) ) e. On ) : No typesetting found for |- ( ( ( bday ` l ) e. On /\ ( bday ` s ) e. On ) -> ( ( bday ` l ) +no ( bday ` s ) ) e. On ) with typecode |-
254	27 135 253	mp2an	Could not format ( ( bday ` l ) +no ( bday ` s ) ) e. On : No typesetting found for |- ( ( bday ` l ) +no ( bday ` s ) ) e. On with typecode |-
255		onunel	Could not format ( ( ( ( bday ` l ) +no ( bday ` Y ) ) e. On /\ ( ( bday ` l ) +no ( bday ` s ) ) e. On /\ ( ( bday ` X ) +no ( bday ` Y ) ) e. On ) -> ( ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( ( bday ` l ) +no ( bday ` s ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` l ) +no ( bday ` Y ) ) e. On /\ ( ( bday ` l ) +no ( bday ` s ) ) e. On /\ ( ( bday ` X ) +no ( bday ` Y ) ) e. On ) -> ( ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( ( bday ` l ) +no ( bday ` s ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) ) with typecode |-
256	252 254 206 255	mp3an	Could not format ( ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( ( bday ` l ) +no ( bday ` s ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( ( bday ` l ) +no ( bday ` s ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) with typecode |-
257	250 238 256	sylanbrc	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( ( bday ` l ) +no ( bday ` s ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( ( bday ` l ) +no ( bday ` s ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
258		elun1	Could not format ( ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( ( bday ` l ) +no ( bday ` s ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( ( bday ` l ) +no ( bday ` s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( ( bday ` l ) +no ( bday ` s ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( ( bday ` l ) +no ( bday ` s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
259	257 258	syl	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( ( bday ` l ) +no ( bday ` s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( ( bday ` l ) +no ( bday ` s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
260	221 222 249 223 259	addsproplem1	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( l +s Y ) e. No /\ ( Y ( Y +s l ) ( ( l +s Y ) e. No /\ ( Y ( Y +s l )
261	260	simprd	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( Y ( Y +s l ) ( Y ( Y +s l )
262	248 261	mpd	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( Y +s l ) ( Y +s l )
263	222 249	addscomd	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( l +s Y ) = ( Y +s l ) ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( l +s Y ) = ( Y +s l ) ) with typecode |-
264	222 223	addscomd	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( l +s s ) = ( s +s l ) ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( l +s s ) = ( s +s l ) ) with typecode |-
265	262 263 264	3brtr4d	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( l +s Y ) ( l +s Y )
266		leftval	Could not format ( _Left ` X ) = { l e. ( _Old ` ( bday ` X ) ) | l
267	266	reqabi	Could not format ( l e. ( _Left ` X ) <-> ( l e. ( _Old ` ( bday ` X ) ) /\ l ( l e. ( _Old ` ( bday ` X ) ) /\ l
268	267	simprbi	Could not format ( l e. ( _Left ` X ) -> l l
269	268	ad2antrl	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> l l
270	2	adantr	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> X e. No ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> X e. No ) with typecode |-
271		naddcom	Could not format ( ( ( bday ` s ) e. On /\ ( bday ` l ) e. On ) -> ( ( bday ` s ) +no ( bday ` l ) ) = ( ( bday ` l ) +no ( bday ` s ) ) ) : No typesetting found for |- ( ( ( bday ` s ) e. On /\ ( bday ` l ) e. On ) -> ( ( bday ` s ) +no ( bday ` l ) ) = ( ( bday ` l ) +no ( bday ` s ) ) ) with typecode |-
272	135 27 271	mp2an	Could not format ( ( bday ` s ) +no ( bday ` l ) ) = ( ( bday ` l ) +no ( bday ` s ) ) : No typesetting found for |- ( ( bday ` s ) +no ( bday ` l ) ) = ( ( bday ` l ) +no ( bday ` s ) ) with typecode |-
273	272 238	eqeltrid	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( bday ` s ) +no ( bday ` l ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( bday ` s ) +no ( bday ` l ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
274		naddcom	Could not format ( ( ( bday ` s ) e. On /\ ( bday ` X ) e. On ) -> ( ( bday ` s ) +no ( bday ` X ) ) = ( ( bday ` X ) +no ( bday ` s ) ) ) : No typesetting found for |- ( ( ( bday ` s ) e. On /\ ( bday ` X ) e. On ) -> ( ( bday ` s ) +no ( bday ` X ) ) = ( ( bday ` X ) +no ( bday ` s ) ) ) with typecode |-
275	135 40 274	mp2an	Could not format ( ( bday ` s ) +no ( bday ` X ) ) = ( ( bday ` X ) +no ( bday ` s ) ) : No typesetting found for |- ( ( bday ` s ) +no ( bday ` X ) ) = ( ( bday ` X ) +no ( bday ` s ) ) with typecode |-
276	275 235	eqeltrid	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( bday ` s ) +no ( bday ` X ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( bday ` s ) +no ( bday ` X ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
277		naddcl	Could not format ( ( ( bday ` s ) e. On /\ ( bday ` l ) e. On ) -> ( ( bday ` s ) +no ( bday ` l ) ) e. On ) : No typesetting found for |- ( ( ( bday ` s ) e. On /\ ( bday ` l ) e. On ) -> ( ( bday ` s ) +no ( bday ` l ) ) e. On ) with typecode |-
278	135 27 277	mp2an	Could not format ( ( bday ` s ) +no ( bday ` l ) ) e. On : No typesetting found for |- ( ( bday ` s ) +no ( bday ` l ) ) e. On with typecode |-
279		naddcl	Could not format ( ( ( bday ` s ) e. On /\ ( bday ` X ) e. On ) -> ( ( bday ` s ) +no ( bday ` X ) ) e. On ) : No typesetting found for |- ( ( ( bday ` s ) e. On /\ ( bday ` X ) e. On ) -> ( ( bday ` s ) +no ( bday ` X ) ) e. On ) with typecode |-
280	135 40 279	mp2an	Could not format ( ( bday ` s ) +no ( bday ` X ) ) e. On : No typesetting found for |- ( ( bday ` s ) +no ( bday ` X ) ) e. On with typecode |-
281		onunel	Could not format ( ( ( ( bday ` s ) +no ( bday ` l ) ) e. On /\ ( ( bday ` s ) +no ( bday ` X ) ) e. On /\ ( ( bday ` X ) +no ( bday ` Y ) ) e. On ) -> ( ( ( ( bday ` s ) +no ( bday ` l ) ) u. ( ( bday ` s ) +no ( bday ` X ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` s ) +no ( bday ` l ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` s ) +no ( bday ` X ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` s ) +no ( bday ` l ) ) e. On /\ ( ( bday ` s ) +no ( bday ` X ) ) e. On /\ ( ( bday ` X ) +no ( bday ` Y ) ) e. On ) -> ( ( ( ( bday ` s ) +no ( bday ` l ) ) u. ( ( bday ` s ) +no ( bday ` X ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` s ) +no ( bday ` l ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` s ) +no ( bday ` X ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) ) with typecode |-
282	278 280 206 281	mp3an	Could not format ( ( ( ( bday ` s ) +no ( bday ` l ) ) u. ( ( bday ` s ) +no ( bday ` X ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` s ) +no ( bday ` l ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` s ) +no ( bday ` X ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` s ) +no ( bday ` l ) ) u. ( ( bday ` s ) +no ( bday ` X ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` s ) +no ( bday ` l ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` s ) +no ( bday ` X ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) with typecode |-
283	273 276 282	sylanbrc	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( ( bday ` s ) +no ( bday ` l ) ) u. ( ( bday ` s ) +no ( bday ` X ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( ( bday ` s ) +no ( bday ` l ) ) u. ( ( bday ` s ) +no ( bday ` X ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
284		elun1	Could not format ( ( ( ( bday ` s ) +no ( bday ` l ) ) u. ( ( bday ` s ) +no ( bday ` X ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( ( bday ` s ) +no ( bday ` l ) ) u. ( ( bday ` s ) +no ( bday ` X ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` s ) +no ( bday ` l ) ) u. ( ( bday ` s ) +no ( bday ` X ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( ( bday ` s ) +no ( bday ` l ) ) u. ( ( bday ` s ) +no ( bday ` X ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
285	283 284	syl	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( ( bday ` s ) +no ( bday ` l ) ) u. ( ( bday ` s ) +no ( bday ` X ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( ( bday ` s ) +no ( bday ` l ) ) u. ( ( bday ` s ) +no ( bday ` X ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
286	221 223 222 270 285	addsproplem1	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( s +s l ) e. No /\ ( l ( l +s s ) ( ( s +s l ) e. No /\ ( l ( l +s s )
287	286	simprd	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( l ( l +s s ) ( l ( l +s s )
288	269 287	mpd	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( l +s s ) ( l +s s )
289	220 243 244 265 288	slttrd	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( l +s Y ) ( l +s Y )
290		breq12	Could not format ( ( a = ( l +s Y ) /\ b = ( X +s s ) ) -> ( a ( l +s Y ) ( a ( l +s Y )
291	289 290	syl5ibrcom	Could not format ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( a = ( l +s Y ) /\ b = ( X +s s ) ) -> a ( ( a = ( l +s Y ) /\ b = ( X +s s ) ) -> a
292	291	rexlimdvva	Could not format ( ph -> ( E. l e. ( _Left ` X ) E. s e. ( _Right ` Y ) ( a = ( l +s Y ) /\ b = ( X +s s ) ) -> a ( E. l e. ( _Left ` X ) E. s e. ( _Right ` Y ) ( a = ( l +s Y ) /\ b = ( X +s s ) ) -> a
293	219 292	biimtrrid	Could not format ( ph -> ( ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) -> a ( ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) -> a
294	218 293	jaod	Could not format ( ph -> ( ( ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) \/ ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) -> a ( ( ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) \/ ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) -> a
295		reeanv	Could not format ( E. m e. ( _Left ` Y ) E. r e. ( _Right ` X ) ( a = ( X +s m ) /\ b = ( r +s Y ) ) <-> ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) ) : No typesetting found for |- ( E. m e. ( _Left ` Y ) E. r e. ( _Right ` X ) ( a = ( X +s m ) /\ b = ( r +s Y ) ) <-> ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) ) with typecode |-
296	1	adantr	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
297	2	adantr	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> X e. No ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> X e. No ) with typecode |-
298	60	ad2antrl	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> m e. No ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> m e. No ) with typecode |-
299	23	a1i	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> 0s e. No ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> 0s e. No ) with typecode |-
300	81	ad2antrl	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
301	300 83	syl	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
302	73 301	eqeltrid	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` 0s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` 0s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
303	296 297 298 299 302	addsproplem1	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( X +s m ) e. No /\ ( m ( m +s X ) ( ( X +s m ) e. No /\ ( m ( m +s X )
304	303	simpld	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( X +s m ) e. No ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( X +s m ) e. No ) with typecode |-
305	95	ad2antll	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> r e. No ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> r e. No ) with typecode |-
306	103	uneq2i	Could not format ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( ( bday ` r ) +no ( bday ` 0s ) ) ) = ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( bday ` r ) ) : No typesetting found for |- ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( ( bday ` r ) +no ( bday ` 0s ) ) ) = ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( bday ` r ) ) with typecode |-
307		naddword1	Could not format ( ( ( bday ` r ) e. On /\ ( bday ` m ) e. On ) -> ( bday ` r ) C_ ( ( bday ` r ) +no ( bday ` m ) ) ) : No typesetting found for |- ( ( ( bday ` r ) e. On /\ ( bday ` m ) e. On ) -> ( bday ` r ) C_ ( ( bday ` r ) +no ( bday ` m ) ) ) with typecode |-
308	100 68 307	mp2an	Could not format ( bday ` r ) C_ ( ( bday ` r ) +no ( bday ` m ) ) : No typesetting found for |- ( bday ` r ) C_ ( ( bday ` r ) +no ( bday ` m ) ) with typecode |-
309		ssequn2	Could not format ( ( bday ` r ) C_ ( ( bday ` r ) +no ( bday ` m ) ) <-> ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( bday ` r ) ) = ( ( bday ` r ) +no ( bday ` m ) ) ) : No typesetting found for |- ( ( bday ` r ) C_ ( ( bday ` r ) +no ( bday ` m ) ) <-> ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( bday ` r ) ) = ( ( bday ` r ) +no ( bday ` m ) ) ) with typecode |-
310	308 309	mpbi	Could not format ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( bday ` r ) ) = ( ( bday ` r ) +no ( bday ` m ) ) : No typesetting found for |- ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( bday ` r ) ) = ( ( bday ` r ) +no ( bday ` m ) ) with typecode |-
311	306 310	eqtri	Could not format ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( ( bday ` r ) +no ( bday ` 0s ) ) ) = ( ( bday ` r ) +no ( bday ` m ) ) : No typesetting found for |- ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( ( bday ` r ) +no ( bday ` 0s ) ) ) = ( ( bday ` r ) +no ( bday ` m ) ) with typecode |-
312		naddel1	Could not format ( ( ( bday ` r ) e. On /\ ( bday ` X ) e. On /\ ( bday ` m ) e. On ) -> ( ( bday ` r ) e. ( bday ` X ) <-> ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` m ) ) ) ) : No typesetting found for |- ( ( ( bday ` r ) e. On /\ ( bday ` X ) e. On /\ ( bday ` m ) e. On ) -> ( ( bday ` r ) e. ( bday ` X ) <-> ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` m ) ) ) ) with typecode |-
313	100 40 68 312	mp3an	Could not format ( ( bday ` r ) e. ( bday ` X ) <-> ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` m ) ) ) : No typesetting found for |- ( ( bday ` r ) e. ( bday ` X ) <-> ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` m ) ) ) with typecode |-
314	114 313	sylib	Could not format ( r e. ( _Right ` X ) -> ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` m ) ) ) : No typesetting found for |- ( r e. ( _Right ` X ) -> ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` m ) ) ) with typecode |-
315	314	ad2antll	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` m ) ) ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` m ) ) ) with typecode |-
316		ontr1	Could not format ( ( ( bday ` X ) +no ( bday ` Y ) ) e. On -> ( ( ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` m ) ) /\ ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) -> ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) : No typesetting found for |- ( ( ( bday ` X ) +no ( bday ` Y ) ) e. On -> ( ( ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` m ) ) /\ ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) -> ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) with typecode |-
317	206 316	ax-mp	Could not format ( ( ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` m ) ) /\ ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) -> ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` m ) ) /\ ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) -> ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
318	315 300 317	syl2anc	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
319		elun1	Could not format ( ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
320	318 319	syl	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
321	311 320	eqeltrid	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( ( bday ` r ) +no ( bday ` 0s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( ( bday ` r ) +no ( bday ` 0s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
322	296 305 298 299 321	addsproplem1	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( r +s m ) e. No /\ ( m ( m +s r ) ( ( r +s m ) e. No /\ ( m ( m +s r )
323	322	simpld	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( r +s m ) e. No ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( r +s m ) e. No ) with typecode |-
324	3	adantr	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> Y e. No ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> Y e. No ) with typecode |-
325	117	ad2antll	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
326	325 119	syl	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
327	109 326	eqeltrid	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( ( bday ` r ) +no ( bday ` Y ) ) u. ( ( bday ` r ) +no ( bday ` 0s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( ( bday ` r ) +no ( bday ` Y ) ) u. ( ( bday ` r ) +no ( bday ` 0s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
328	296 305 324 299 327	addsproplem1	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( r +s Y ) e. No /\ ( Y ( Y +s r ) ( ( r +s Y ) e. No /\ ( Y ( Y +s r )
329	328	simpld	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( r +s Y ) e. No ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( r +s Y ) e. No ) with typecode |-
330		rightval	Could not format ( _Right ` X ) = { r e. ( _Old ` ( bday ` X ) ) | X
331	330	eleq2i	Could not format ( r e. ( _Right ` X ) <-> r e. { r e. ( _Old ` ( bday ` X ) ) | X r e. { r e. ( _Old ` ( bday ` X ) ) | X
332	331	biimpi	Could not format ( r e. ( _Right ` X ) -> r e. { r e. ( _Old ` ( bday ` X ) ) | X r e. { r e. ( _Old ` ( bday ` X ) ) | X
333	332	ad2antll	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> r e. { r e. ( _Old ` ( bday ` X ) ) | X r e. { r e. ( _Old ` ( bday ` X ) ) | X
334		rabid	$$⊢r\in \left\{r\in \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)|X{<}_{s}r\right\}\leftrightarrow \left(r\in \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\wedge X{<}_{s}r\right)$$
335	333 334	sylib	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( r e. ( _Old ` ( bday ` X ) ) /\ X ( r e. ( _Old ` ( bday ` X ) ) /\ X
336	335	simprd	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> X X
337		naddcom	Could not format ( ( ( bday ` m ) e. On /\ ( bday ` X ) e. On ) -> ( ( bday ` m ) +no ( bday ` X ) ) = ( ( bday ` X ) +no ( bday ` m ) ) ) : No typesetting found for |- ( ( ( bday ` m ) e. On /\ ( bday ` X ) e. On ) -> ( ( bday ` m ) +no ( bday ` X ) ) = ( ( bday ` X ) +no ( bday ` m ) ) ) with typecode |-
338	68 40 337	mp2an	Could not format ( ( bday ` m ) +no ( bday ` X ) ) = ( ( bday ` X ) +no ( bday ` m ) ) : No typesetting found for |- ( ( bday ` m ) +no ( bday ` X ) ) = ( ( bday ` X ) +no ( bday ` m ) ) with typecode |-
339	338 300	eqeltrid	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` m ) +no ( bday ` X ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` m ) +no ( bday ` X ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
340		naddcom	Could not format ( ( ( bday ` m ) e. On /\ ( bday ` r ) e. On ) -> ( ( bday ` m ) +no ( bday ` r ) ) = ( ( bday ` r ) +no ( bday ` m ) ) ) : No typesetting found for |- ( ( ( bday ` m ) e. On /\ ( bday ` r ) e. On ) -> ( ( bday ` m ) +no ( bday ` r ) ) = ( ( bday ` r ) +no ( bday ` m ) ) ) with typecode |-
341	68 100 340	mp2an	Could not format ( ( bday ` m ) +no ( bday ` r ) ) = ( ( bday ` r ) +no ( bday ` m ) ) : No typesetting found for |- ( ( bday ` m ) +no ( bday ` r ) ) = ( ( bday ` r ) +no ( bday ` m ) ) with typecode |-
342	341 318	eqeltrid	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` m ) +no ( bday ` r ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` m ) +no ( bday ` r ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
343		naddcl	Could not format ( ( ( bday ` m ) e. On /\ ( bday ` X ) e. On ) -> ( ( bday ` m ) +no ( bday ` X ) ) e. On ) : No typesetting found for |- ( ( ( bday ` m ) e. On /\ ( bday ` X ) e. On ) -> ( ( bday ` m ) +no ( bday ` X ) ) e. On ) with typecode |-
344	68 40 343	mp2an	Could not format ( ( bday ` m ) +no ( bday ` X ) ) e. On : No typesetting found for |- ( ( bday ` m ) +no ( bday ` X ) ) e. On with typecode |-
345		naddcl	Could not format ( ( ( bday ` m ) e. On /\ ( bday ` r ) e. On ) -> ( ( bday ` m ) +no ( bday ` r ) ) e. On ) : No typesetting found for |- ( ( ( bday ` m ) e. On /\ ( bday ` r ) e. On ) -> ( ( bday ` m ) +no ( bday ` r ) ) e. On ) with typecode |-
346	68 100 345	mp2an	Could not format ( ( bday ` m ) +no ( bday ` r ) ) e. On : No typesetting found for |- ( ( bday ` m ) +no ( bday ` r ) ) e. On with typecode |-
347		onunel	Could not format ( ( ( ( bday ` m ) +no ( bday ` X ) ) e. On /\ ( ( bday ` m ) +no ( bday ` r ) ) e. On /\ ( ( bday ` X ) +no ( bday ` Y ) ) e. On ) -> ( ( ( ( bday ` m ) +no ( bday ` X ) ) u. ( ( bday ` m ) +no ( bday ` r ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` m ) +no ( bday ` X ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` m ) +no ( bday ` r ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` m ) +no ( bday ` X ) ) e. On /\ ( ( bday ` m ) +no ( bday ` r ) ) e. On /\ ( ( bday ` X ) +no ( bday ` Y ) ) e. On ) -> ( ( ( ( bday ` m ) +no ( bday ` X ) ) u. ( ( bday ` m ) +no ( bday ` r ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` m ) +no ( bday ` X ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` m ) +no ( bday ` r ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) ) with typecode |-
348	344 346 206 347	mp3an	Could not format ( ( ( ( bday ` m ) +no ( bday ` X ) ) u. ( ( bday ` m ) +no ( bday ` r ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` m ) +no ( bday ` X ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` m ) +no ( bday ` r ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` m ) +no ( bday ` X ) ) u. ( ( bday ` m ) +no ( bday ` r ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` m ) +no ( bday ` X ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` m ) +no ( bday ` r ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) with typecode |-
349	339 342 348	sylanbrc	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( ( bday ` m ) +no ( bday ` X ) ) u. ( ( bday ` m ) +no ( bday ` r ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( ( bday ` m ) +no ( bday ` X ) ) u. ( ( bday ` m ) +no ( bday ` r ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
350		elun1	Could not format ( ( ( ( bday ` m ) +no ( bday ` X ) ) u. ( ( bday ` m ) +no ( bday ` r ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( ( bday ` m ) +no ( bday ` X ) ) u. ( ( bday ` m ) +no ( bday ` r ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` m ) +no ( bday ` X ) ) u. ( ( bday ` m ) +no ( bday ` r ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( ( bday ` m ) +no ( bday ` X ) ) u. ( ( bday ` m ) +no ( bday ` r ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
351	349 350	syl	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( ( bday ` m ) +no ( bday ` X ) ) u. ( ( bday ` m ) +no ( bday ` r ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( ( bday ` m ) +no ( bday ` X ) ) u. ( ( bday ` m ) +no ( bday ` r ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
352	296 298 297 305 351	addsproplem1	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( m +s X ) e. No /\ ( X ( X +s m ) ( ( m +s X ) e. No /\ ( X ( X +s m )
353	352	simprd	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( X ( X +s m ) ( X ( X +s m )
354	336 353	mpd	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( X +s m ) ( X +s m )
355		leftval	Could not format ( _Left ` Y ) = { m e. ( _Old ` ( bday ` Y ) ) | m
356	355	eleq2i	Could not format ( m e. ( _Left ` Y ) <-> m e. { m e. ( _Old ` ( bday ` Y ) ) | m m e. { m e. ( _Old ` ( bday ` Y ) ) | m
357	356	biimpi	Could not format ( m e. ( _Left ` Y ) -> m e. { m e. ( _Old ` ( bday ` Y ) ) | m m e. { m e. ( _Old ` ( bday ` Y ) ) | m
358	357	ad2antrl	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> m e. { m e. ( _Old ` ( bday ` Y ) ) | m m e. { m e. ( _Old ` ( bday ` Y ) ) | m
359		rabid	$$⊢m\in \left\{m\in \mathrm{Old}\left(\mathrm{bday}\left(Y\right)\right)|m{<}_{s}Y\right\}\leftrightarrow \left(m\in \mathrm{Old}\left(\mathrm{bday}\left(Y\right)\right)\wedge m{<}_{s}Y\right)$$
360	358 359	sylib	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( m e. ( _Old ` ( bday ` Y ) ) /\ m ( m e. ( _Old ` ( bday ` Y ) ) /\ m
361	360	simprd	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> m m
362		naddcl	Could not format ( ( ( bday ` r ) e. On /\ ( bday ` m ) e. On ) -> ( ( bday ` r ) +no ( bday ` m ) ) e. On ) : No typesetting found for |- ( ( ( bday ` r ) e. On /\ ( bday ` m ) e. On ) -> ( ( bday ` r ) +no ( bday ` m ) ) e. On ) with typecode |-
363	100 68 362	mp2an	Could not format ( ( bday ` r ) +no ( bday ` m ) ) e. On : No typesetting found for |- ( ( bday ` r ) +no ( bday ` m ) ) e. On with typecode |-
364		naddcl	Could not format ( ( ( bday ` r ) e. On /\ ( bday ` Y ) e. On ) -> ( ( bday ` r ) +no ( bday ` Y ) ) e. On ) : No typesetting found for |- ( ( ( bday ` r ) e. On /\ ( bday ` Y ) e. On ) -> ( ( bday ` r ) +no ( bday ` Y ) ) e. On ) with typecode |-
365	100 32 364	mp2an	Could not format ( ( bday ` r ) +no ( bday ` Y ) ) e. On : No typesetting found for |- ( ( bday ` r ) +no ( bday ` Y ) ) e. On with typecode |-
366		onunel	Could not format ( ( ( ( bday ` r ) +no ( bday ` m ) ) e. On /\ ( ( bday ` r ) +no ( bday ` Y ) ) e. On /\ ( ( bday ` X ) +no ( bday ` Y ) ) e. On ) -> ( ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( ( bday ` r ) +no ( bday ` Y ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` r ) +no ( bday ` m ) ) e. On /\ ( ( bday ` r ) +no ( bday ` Y ) ) e. On /\ ( ( bday ` X ) +no ( bday ` Y ) ) e. On ) -> ( ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( ( bday ` r ) +no ( bday ` Y ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) ) with typecode |-
367	363 365 206 366	mp3an	Could not format ( ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( ( bday ` r ) +no ( bday ` Y ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( ( bday ` r ) +no ( bday ` Y ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) with typecode |-
368	318 325 367	sylanbrc	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( ( bday ` r ) +no ( bday ` Y ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( ( bday ` r ) +no ( bday ` Y ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
369		elun1	Could not format ( ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( ( bday ` r ) +no ( bday ` Y ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( ( bday ` r ) +no ( bday ` Y ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( ( bday ` r ) +no ( bday ` Y ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( ( bday ` r ) +no ( bday ` Y ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
370	368 369	syl	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( ( bday ` r ) +no ( bday ` Y ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( ( bday ` r ) +no ( bday ` Y ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
371	296 305 298 324 370	addsproplem1	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( r +s m ) e. No /\ ( m ( m +s r ) ( ( r +s m ) e. No /\ ( m ( m +s r )
372	371	simprd	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( m ( m +s r ) ( m ( m +s r )
373	361 372	mpd	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( m +s r ) ( m +s r )
374	305 298	addscomd	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( r +s m ) = ( m +s r ) ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( r +s m ) = ( m +s r ) ) with typecode |-
375	305 324	addscomd	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( r +s Y ) = ( Y +s r ) ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( r +s Y ) = ( Y +s r ) ) with typecode |-
376	373 374 375	3brtr4d	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( r +s m ) ( r +s m )
377	304 323 329 354 376	slttrd	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( X +s m ) ( X +s m )
378		breq12	Could not format ( ( a = ( X +s m ) /\ b = ( r +s Y ) ) -> ( a ( X +s m ) ( a ( X +s m )
379	377 378	syl5ibrcom	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( a = ( X +s m ) /\ b = ( r +s Y ) ) -> a ( ( a = ( X +s m ) /\ b = ( r +s Y ) ) -> a
380	379	rexlimdvva	Could not format ( ph -> ( E. m e. ( _Left ` Y ) E. r e. ( _Right ` X ) ( a = ( X +s m ) /\ b = ( r +s Y ) ) -> a ( E. m e. ( _Left ` Y ) E. r e. ( _Right ` X ) ( a = ( X +s m ) /\ b = ( r +s Y ) ) -> a
381	295 380	biimtrrid	Could not format ( ph -> ( ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) -> a ( ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) -> a
382		reeanv	Could not format ( E. m e. ( _Left ` Y ) E. s e. ( _Right ` Y ) ( a = ( X +s m ) /\ b = ( X +s s ) ) <-> ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) : No typesetting found for |- ( E. m e. ( _Left ` Y ) E. s e. ( _Right ` Y ) ( a = ( X +s m ) /\ b = ( X +s s ) ) <-> ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) with typecode |-
383		lltropt	Could not format ( _Left ` Y ) <
384	383	a1i	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> ( _Left ` Y ) < ( _Left ` Y ) <
385		simprl	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> m e. ( _Left ` Y ) ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> m e. ( _Left ` Y ) ) with typecode |-
386		simprr	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> s e. ( _Right ` Y ) ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> s e. ( _Right ` Y ) ) with typecode |-
387	384 385 386	ssltsepcd	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> m m
388	1	adantr	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
389	2	adantr	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> X e. No ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> X e. No ) with typecode |-
390	60	ad2antrl	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> m e. No ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> m e. No ) with typecode |-
391	131	ad2antll	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> s e. No ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> s e. No ) with typecode |-
392	81	ad2antrl	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
393	148	ad2antll	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
394		naddcl	Could not format ( ( ( bday ` X ) e. On /\ ( bday ` m ) e. On ) -> ( ( bday ` X ) +no ( bday ` m ) ) e. On ) : No typesetting found for |- ( ( ( bday ` X ) e. On /\ ( bday ` m ) e. On ) -> ( ( bday ` X ) +no ( bday ` m ) ) e. On ) with typecode |-
395	40 68 394	mp2an	Could not format ( ( bday ` X ) +no ( bday ` m ) ) e. On : No typesetting found for |- ( ( bday ` X ) +no ( bday ` m ) ) e. On with typecode |-
396		naddcl	Could not format ( ( ( bday ` X ) e. On /\ ( bday ` s ) e. On ) -> ( ( bday ` X ) +no ( bday ` s ) ) e. On ) : No typesetting found for |- ( ( ( bday ` X ) e. On /\ ( bday ` s ) e. On ) -> ( ( bday ` X ) +no ( bday ` s ) ) e. On ) with typecode |-
397	40 135 396	mp2an	Could not format ( ( bday ` X ) +no ( bday ` s ) ) e. On : No typesetting found for |- ( ( bday ` X ) +no ( bday ` s ) ) e. On with typecode |-
398		onunel	Could not format ( ( ( ( bday ` X ) +no ( bday ` m ) ) e. On /\ ( ( bday ` X ) +no ( bday ` s ) ) e. On /\ ( ( bday ` X ) +no ( bday ` Y ) ) e. On ) -> ( ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` s ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` X ) +no ( bday ` m ) ) e. On /\ ( ( bday ` X ) +no ( bday ` s ) ) e. On /\ ( ( bday ` X ) +no ( bday ` Y ) ) e. On ) -> ( ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` s ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) ) with typecode |-
399	395 397 206 398	mp3an	Could not format ( ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` s ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` s ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) with typecode |-
400	392 393 399	sylanbrc	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` s ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` s ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) with typecode |-
401		elun1	Could not format ( ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` s ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` s ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
402	400 401	syl	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
403	388 389 390 391 402	addsproplem1	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> ( ( X +s m ) e. No /\ ( m ( m +s X ) ( ( X +s m ) e. No /\ ( m ( m +s X )
404	403	simprd	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> ( m ( m +s X ) ( m ( m +s X )
405	387 404	mpd	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> ( m +s X ) ( m +s X )
406	389 390	addscomd	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> ( X +s m ) = ( m +s X ) ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> ( X +s m ) = ( m +s X ) ) with typecode |-
407	389 391	addscomd	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> ( X +s s ) = ( s +s X ) ) : No typesetting found for |- ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> ( X +s s ) = ( s +s X ) ) with typecode |-
408	405 406 407	3brtr4d	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> ( X +s m ) ( X +s m )
409		breq12	Could not format ( ( a = ( X +s m ) /\ b = ( X +s s ) ) -> ( a ( X +s m ) ( a ( X +s m )
410	408 409	syl5ibrcom	Could not format ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> ( ( a = ( X +s m ) /\ b = ( X +s s ) ) -> a ( ( a = ( X +s m ) /\ b = ( X +s s ) ) -> a
411	410	rexlimdvva	Could not format ( ph -> ( E. m e. ( _Left ` Y ) E. s e. ( _Right ` Y ) ( a = ( X +s m ) /\ b = ( X +s s ) ) -> a ( E. m e. ( _Left ` Y ) E. s e. ( _Right ` Y ) ( a = ( X +s m ) /\ b = ( X +s s ) ) -> a
412	382 411	biimtrrid	Could not format ( ph -> ( ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) -> a ( ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) -> a
413	381 412	jaod	Could not format ( ph -> ( ( ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) \/ ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) -> a ( ( ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) \/ ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) -> a
414	294 413	jaod	Could not format ( ph -> ( ( ( ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) \/ ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) \/ ( ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) \/ ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) ) -> a ( ( ( ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) \/ ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) \/ ( ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) \/ ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) ) -> a
415	182 414	biimtrid	Could not format ( ph -> ( ( a e. ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) /\ b e. ( { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) ) -> a ( ( a e. ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) /\ b e. ( { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) ) -> a
416	415	3impib	Could not format ( ( ph /\ a e. ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) /\ b e. ( { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) ) -> a a
417	10 17 92 159 416	ssltd	Could not format ( ph -> ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) < ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <