Theorem addsbday

Description: The birthday of the sum of two surreals is less than or equal to the natural ordinal sum of their individual birthdays. Theorem 6.1 of Gonshor p. 95. (Contributed by Scott Fenton, 12-Aug-2025)

	Ref	Expression
Assertion	addsbday	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \mathrm{bday}\left(A{+}_{s}B\right)\subseteq \mathrm{bday}\left(A\right)+\mathrm{bday}\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		fvoveq1	Could not format ( x = xO -> ( bday ` ( x +s y ) ) = ( bday ` ( xO +s y ) ) ) : No typesetting found for |- ( x = xO -> ( bday ` ( x +s y ) ) = ( bday ` ( xO +s y ) ) ) with typecode |-
2		fveq2	Could not format ( x = xO -> ( bday ` x ) = ( bday ` xO ) ) : No typesetting found for |- ( x = xO -> ( bday ` x ) = ( bday ` xO ) ) with typecode |-
3	2	oveq1d	Could not format ( x = xO -> ( ( bday ` x ) +no ( bday ` y ) ) = ( ( bday ` xO ) +no ( bday ` y ) ) ) : No typesetting found for |- ( x = xO -> ( ( bday ` x ) +no ( bday ` y ) ) = ( ( bday ` xO ) +no ( bday ` y ) ) ) with typecode |-
4	1 3	sseq12d	Could not format ( x = xO -> ( ( bday ` ( x +s y ) ) C_ ( ( bday ` x ) +no ( bday ` y ) ) <-> ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) ) ) : No typesetting found for |- ( x = xO -> ( ( bday ` ( x +s y ) ) C_ ( ( bday ` x ) +no ( bday ` y ) ) <-> ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) ) ) with typecode |-
5		oveq2	Could not format ( y = yO -> ( xO +s y ) = ( xO +s yO ) ) : No typesetting found for |- ( y = yO -> ( xO +s y ) = ( xO +s yO ) ) with typecode |-
6	5	fveq2d	Could not format ( y = yO -> ( bday ` ( xO +s y ) ) = ( bday ` ( xO +s yO ) ) ) : No typesetting found for |- ( y = yO -> ( bday ` ( xO +s y ) ) = ( bday ` ( xO +s yO ) ) ) with typecode |-
7		fveq2	Could not format ( y = yO -> ( bday ` y ) = ( bday ` yO ) ) : No typesetting found for |- ( y = yO -> ( bday ` y ) = ( bday ` yO ) ) with typecode |-
8	7	oveq2d	Could not format ( y = yO -> ( ( bday ` xO ) +no ( bday ` y ) ) = ( ( bday ` xO ) +no ( bday ` yO ) ) ) : No typesetting found for |- ( y = yO -> ( ( bday ` xO ) +no ( bday ` y ) ) = ( ( bday ` xO ) +no ( bday ` yO ) ) ) with typecode |-
9	6 8	sseq12d	Could not format ( y = yO -> ( ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) <-> ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) ) ) : No typesetting found for |- ( y = yO -> ( ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) <-> ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) ) ) with typecode |-
10		fvoveq1	Could not format ( x = xO -> ( bday ` ( x +s yO ) ) = ( bday ` ( xO +s yO ) ) ) : No typesetting found for |- ( x = xO -> ( bday ` ( x +s yO ) ) = ( bday ` ( xO +s yO ) ) ) with typecode |-
11	2	oveq1d	Could not format ( x = xO -> ( ( bday ` x ) +no ( bday ` yO ) ) = ( ( bday ` xO ) +no ( bday ` yO ) ) ) : No typesetting found for |- ( x = xO -> ( ( bday ` x ) +no ( bday ` yO ) ) = ( ( bday ` xO ) +no ( bday ` yO ) ) ) with typecode |-
12	10 11	sseq12d	Could not format ( x = xO -> ( ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) <-> ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) ) ) : No typesetting found for |- ( x = xO -> ( ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) <-> ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) ) ) with typecode |-
13		fvoveq1	$$⊢x=A\to \mathrm{bday}\left(x{+}_{s}y\right)=\mathrm{bday}\left(A{+}_{s}y\right)$$
14		fveq2	$$⊢x=A\to \mathrm{bday}\left(x\right)=\mathrm{bday}\left(A\right)$$
15	14	oveq1d	$$⊢x=A\to \mathrm{bday}\left(x\right)+\mathrm{bday}\left(y\right)=\mathrm{bday}\left(A\right)+\mathrm{bday}\left(y\right)$$
16	13 15	sseq12d	$$⊢x=A\to \left(\mathrm{bday}\left(x{+}_{s}y\right)\subseteq \mathrm{bday}\left(x\right)+\mathrm{bday}\left(y\right)\leftrightarrow \mathrm{bday}\left(A{+}_{s}y\right)\subseteq \mathrm{bday}\left(A\right)+\mathrm{bday}\left(y\right)\right)$$
17		oveq2	$$⊢y=B\to A{+}_{s}y=A{+}_{s}B$$
18	17	fveq2d	$$⊢y=B\to \mathrm{bday}\left(A{+}_{s}y\right)=\mathrm{bday}\left(A{+}_{s}B\right)$$
19		fveq2	$$⊢y=B\to \mathrm{bday}\left(y\right)=\mathrm{bday}\left(B\right)$$
20	19	oveq2d	$$⊢y=B\to \mathrm{bday}\left(A\right)+\mathrm{bday}\left(y\right)=\mathrm{bday}\left(A\right)+\mathrm{bday}\left(B\right)$$
21	18 20	sseq12d	$$⊢y=B\to \left(\mathrm{bday}\left(A{+}_{s}y\right)\subseteq \mathrm{bday}\left(A\right)+\mathrm{bday}\left(y\right)\leftrightarrow \mathrm{bday}\left(A{+}_{s}B\right)\subseteq \mathrm{bday}\left(A\right)+\mathrm{bday}\left(B\right)\right)$$
22		addsval2	Could not format ( ( x e. No /\ y e. No ) -> ( x +s y ) = ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) |s ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) : No typesetting found for |- ( ( x e. No /\ y e. No ) -> ( x +s y ) = ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) |s ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) with typecode |-
23	22	fveq2d	Could not format ( ( x e. No /\ y e. No ) -> ( bday ` ( x +s y ) ) = ( bday ` ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) |s ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) ) : No typesetting found for |- ( ( x e. No /\ y e. No ) -> ( bday ` ( x +s y ) ) = ( bday ` ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) |s ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) ) with typecode |-
24	23	adantr	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday ` ( x +s y ) ) = ( bday ` ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) |s ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday ` ( x +s y ) ) = ( bday ` ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) |s ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) ) with typecode |-
25		simpl	$$⊢\left(x\in \mathrm{No}\wedge y\in \mathrm{No}\right)\to x\in \mathrm{No}$$
26		simpr	$$⊢\left(x\in \mathrm{No}\wedge y\in \mathrm{No}\right)\to y\in \mathrm{No}$$
27	25 26	addscut2	Could not format ( ( x e. No /\ y e. No ) -> ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) < ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) <
28		imaundi	Could not format ( bday " ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) u. ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) = ( ( bday " ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) ) u. ( bday " ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) : No typesetting found for |- ( bday " ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) u. ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) = ( ( bday " ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) ) u. ( bday " ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) with typecode |-
29		imaundi	Could not format ( bday " ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) ) = ( ( bday " { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } ) u. ( bday " { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) ) : No typesetting found for |- ( bday " ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) ) = ( ( bday " { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } ) u. ( bday " { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) ) with typecode |-
30		imaundi	Could not format ( bday " ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) = ( ( bday " { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } ) u. ( bday " { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) : No typesetting found for |- ( bday " ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) = ( ( bday " { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } ) u. ( bday " { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) with typecode |-
31	29 30	uneq12i	Could not format ( ( bday " ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) ) u. ( bday " ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) = ( ( ( bday " { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } ) u. ( bday " { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) ) u. ( ( bday " { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } ) u. ( bday " { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) : No typesetting found for |- ( ( bday " ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) ) u. ( bday " ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) = ( ( ( bday " { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } ) u. ( bday " { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) ) u. ( ( bday " { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } ) u. ( bday " { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) with typecode |-
32	28 31	eqtri	Could not format ( bday " ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) u. ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) = ( ( ( bday " { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } ) u. ( bday " { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) ) u. ( ( bday " { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } ) u. ( bday " { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) : No typesetting found for |- ( bday " ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) u. ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) = ( ( ( bday " { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } ) u. ( bday " { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) ) u. ( ( bday " { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } ) u. ( bday " { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) with typecode |-
33		simplr	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> y e. No ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> y e. No ) with typecode |-
34		simpr2	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) ) with typecode |-
35		simplr	Could not format ( ( ( x e. No /\ y e. No ) /\ xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) -> y e. No ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) -> y e. No ) with typecode |-
36		leftssno	$$⊢L\left(x\right)\subseteq \mathrm{No}$$
37		rightssno	$$⊢R\left(x\right)\subseteq \mathrm{No}$$
38	36 37	unssi	$$⊢L\left(x\right)\cup R\left(x\right)\subseteq \mathrm{No}$$
39	38	sseli	Could not format ( xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) -> xO e. No ) : No typesetting found for |- ( xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) -> xO e. No ) with typecode |-
40	39	adantl	Could not format ( ( ( x e. No /\ y e. No ) /\ xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) -> xO e. No ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) -> xO e. No ) with typecode |-
41	35 40	addscomd	Could not format ( ( ( x e. No /\ y e. No ) /\ xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) -> ( y +s xO ) = ( xO +s y ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) -> ( y +s xO ) = ( xO +s y ) ) with typecode |-
42	41	fveq2d	Could not format ( ( ( x e. No /\ y e. No ) /\ xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) -> ( bday ` ( y +s xO ) ) = ( bday ` ( xO +s y ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) -> ( bday ` ( y +s xO ) ) = ( bday ` ( xO +s y ) ) ) with typecode |-
43		bdayelon	$$⊢\mathrm{bday}\left(y\right)\in \mathrm{On}$$
44		bdayelon	Could not format ( bday ` xO ) e. On : No typesetting found for |- ( bday ` xO ) e. On with typecode |-
45		naddcom	Could not format ( ( ( bday ` y ) e. On /\ ( bday ` xO ) e. On ) -> ( ( bday ` y ) +no ( bday ` xO ) ) = ( ( bday ` xO ) +no ( bday ` y ) ) ) : No typesetting found for |- ( ( ( bday ` y ) e. On /\ ( bday ` xO ) e. On ) -> ( ( bday ` y ) +no ( bday ` xO ) ) = ( ( bday ` xO ) +no ( bday ` y ) ) ) with typecode |-
46	43 44 45	mp2an	Could not format ( ( bday ` y ) +no ( bday ` xO ) ) = ( ( bday ` xO ) +no ( bday ` y ) ) : No typesetting found for |- ( ( bday ` y ) +no ( bday ` xO ) ) = ( ( bday ` xO ) +no ( bday ` y ) ) with typecode |-
47	46	a1i	Could not format ( ( ( x e. No /\ y e. No ) /\ xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) -> ( ( bday ` y ) +no ( bday ` xO ) ) = ( ( bday ` xO ) +no ( bday ` y ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) -> ( ( bday ` y ) +no ( bday ` xO ) ) = ( ( bday ` xO ) +no ( bday ` y ) ) ) with typecode |-
48	42 47	sseq12d	Could not format ( ( ( x e. No /\ y e. No ) /\ xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) -> ( ( bday ` ( y +s xO ) ) C_ ( ( bday ` y ) +no ( bday ` xO ) ) <-> ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) -> ( ( bday ` ( y +s xO ) ) C_ ( ( bday ` y ) +no ( bday ` xO ) ) <-> ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) ) ) with typecode |-
49	48	ralbidva	Could not format ( ( x e. No /\ y e. No ) -> ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( y +s xO ) ) C_ ( ( bday ` y ) +no ( bday ` xO ) ) <-> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) ) ) : No typesetting found for |- ( ( x e. No /\ y e. No ) -> ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( y +s xO ) ) C_ ( ( bday ` y ) +no ( bday ` xO ) ) <-> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) ) ) with typecode |-
50	49	adantr	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( y +s xO ) ) C_ ( ( bday ` y ) +no ( bday ` xO ) ) <-> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( y +s xO ) ) C_ ( ( bday ` y ) +no ( bday ` xO ) ) <-> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) ) ) with typecode |-
51	34 50	mpbird	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( y +s xO ) ) C_ ( ( bday ` y ) +no ( bday ` xO ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( y +s xO ) ) C_ ( ( bday ` y ) +no ( bday ` xO ) ) ) with typecode |-
52		ssun1	$$⊢L\left(x\right)\subseteq L\left(x\right)\cup R\left(x\right)$$
53	33 51 52	addsbdaylem	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday " { z | E. xL e. ( _Left ` x ) z = ( y +s xL ) } ) C_ ( ( bday ` y ) +no ( bday ` x ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday " { z | E. xL e. ( _Left ` x ) z = ( y +s xL ) } ) C_ ( ( bday ` y ) +no ( bday ` x ) ) ) with typecode |-
54	36	sseli	Could not format ( xL e. ( _Left ` x ) -> xL e. No ) : No typesetting found for |- ( xL e. ( _Left ` x ) -> xL e. No ) with typecode |-
55	54	adantl	Could not format ( ( ( x e. No /\ y e. No ) /\ xL e. ( _Left ` x ) ) -> xL e. No ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ xL e. ( _Left ` x ) ) -> xL e. No ) with typecode |-
56		simplr	Could not format ( ( ( x e. No /\ y e. No ) /\ xL e. ( _Left ` x ) ) -> y e. No ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ xL e. ( _Left ` x ) ) -> y e. No ) with typecode |-
57	55 56	addscomd	Could not format ( ( ( x e. No /\ y e. No ) /\ xL e. ( _Left ` x ) ) -> ( xL +s y ) = ( y +s xL ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ xL e. ( _Left ` x ) ) -> ( xL +s y ) = ( y +s xL ) ) with typecode |-
58	57	eqeq2d	Could not format ( ( ( x e. No /\ y e. No ) /\ xL e. ( _Left ` x ) ) -> ( z = ( xL +s y ) <-> z = ( y +s xL ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ xL e. ( _Left ` x ) ) -> ( z = ( xL +s y ) <-> z = ( y +s xL ) ) ) with typecode |-
59	58	rexbidva	Could not format ( ( x e. No /\ y e. No ) -> ( E. xL e. ( _Left ` x ) z = ( xL +s y ) <-> E. xL e. ( _Left ` x ) z = ( y +s xL ) ) ) : No typesetting found for |- ( ( x e. No /\ y e. No ) -> ( E. xL e. ( _Left ` x ) z = ( xL +s y ) <-> E. xL e. ( _Left ` x ) z = ( y +s xL ) ) ) with typecode |-
60	59	abbidv	Could not format ( ( x e. No /\ y e. No ) -> { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } = { z | E. xL e. ( _Left ` x ) z = ( y +s xL ) } ) : No typesetting found for |- ( ( x e. No /\ y e. No ) -> { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } = { z | E. xL e. ( _Left ` x ) z = ( y +s xL ) } ) with typecode |-
61	60	imaeq2d	Could not format ( ( x e. No /\ y e. No ) -> ( bday " { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } ) = ( bday " { z | E. xL e. ( _Left ` x ) z = ( y +s xL ) } ) ) : No typesetting found for |- ( ( x e. No /\ y e. No ) -> ( bday " { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } ) = ( bday " { z | E. xL e. ( _Left ` x ) z = ( y +s xL ) } ) ) with typecode |-
62	61	adantr	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday " { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } ) = ( bday " { z | E. xL e. ( _Left ` x ) z = ( y +s xL ) } ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday " { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } ) = ( bday " { z | E. xL e. ( _Left ` x ) z = ( y +s xL ) } ) ) with typecode |-
63		bdayelon	$$⊢\mathrm{bday}\left(x\right)\in \mathrm{On}$$
64		naddcom	$$⊢\left(\mathrm{bday}\left(x\right)\in \mathrm{On}\wedge \mathrm{bday}\left(y\right)\in \mathrm{On}\right)\to \mathrm{bday}\left(x\right)+\mathrm{bday}\left(y\right)=\mathrm{bday}\left(y\right)+\mathrm{bday}\left(x\right)$$
65	63 43 64	mp2an	$$⊢\mathrm{bday}\left(x\right)+\mathrm{bday}\left(y\right)=\mathrm{bday}\left(y\right)+\mathrm{bday}\left(x\right)$$
66	65	a1i	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( ( bday ` x ) +no ( bday ` y ) ) = ( ( bday ` y ) +no ( bday ` x ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( ( bday ` x ) +no ( bday ` y ) ) = ( ( bday ` y ) +no ( bday ` x ) ) ) with typecode |-
67	53 62 66	3sstr4d	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday " { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } ) C_ ( ( bday ` x ) +no ( bday ` y ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday " { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } ) C_ ( ( bday ` x ) +no ( bday ` y ) ) ) with typecode |-
68		simpll	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> x e. No ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> x e. No ) with typecode |-
69		simpr3	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) with typecode |-
70		ssun1	$$⊢L\left(y\right)\subseteq L\left(y\right)\cup R\left(y\right)$$
71	68 69 70	addsbdaylem	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday " { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) C_ ( ( bday ` x ) +no ( bday ` y ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday " { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) C_ ( ( bday ` x ) +no ( bday ` y ) ) ) with typecode |-
72	67 71	unssd	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( ( bday " { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } ) u. ( bday " { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) ) C_ ( ( bday ` x ) +no ( bday ` y ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( ( bday " { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } ) u. ( bday " { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) ) C_ ( ( bday ` x ) +no ( bday ` y ) ) ) with typecode |-
73		ssun2	$$⊢R\left(x\right)\subseteq L\left(x\right)\cup R\left(x\right)$$
74	33 51 73	addsbdaylem	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday " { z | E. xR e. ( _Right ` x ) z = ( y +s xR ) } ) C_ ( ( bday ` y ) +no ( bday ` x ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday " { z | E. xR e. ( _Right ` x ) z = ( y +s xR ) } ) C_ ( ( bday ` y ) +no ( bday ` x ) ) ) with typecode |-
75	37	sseli	Could not format ( xR e. ( _Right ` x ) -> xR e. No ) : No typesetting found for |- ( xR e. ( _Right ` x ) -> xR e. No ) with typecode |-
76	75	adantl	Could not format ( ( ( x e. No /\ y e. No ) /\ xR e. ( _Right ` x ) ) -> xR e. No ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ xR e. ( _Right ` x ) ) -> xR e. No ) with typecode |-
77		simplr	Could not format ( ( ( x e. No /\ y e. No ) /\ xR e. ( _Right ` x ) ) -> y e. No ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ xR e. ( _Right ` x ) ) -> y e. No ) with typecode |-
78	76 77	addscomd	Could not format ( ( ( x e. No /\ y e. No ) /\ xR e. ( _Right ` x ) ) -> ( xR +s y ) = ( y +s xR ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ xR e. ( _Right ` x ) ) -> ( xR +s y ) = ( y +s xR ) ) with typecode |-
79	78	eqeq2d	Could not format ( ( ( x e. No /\ y e. No ) /\ xR e. ( _Right ` x ) ) -> ( z = ( xR +s y ) <-> z = ( y +s xR ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ xR e. ( _Right ` x ) ) -> ( z = ( xR +s y ) <-> z = ( y +s xR ) ) ) with typecode |-
80	79	rexbidva	Could not format ( ( x e. No /\ y e. No ) -> ( E. xR e. ( _Right ` x ) z = ( xR +s y ) <-> E. xR e. ( _Right ` x ) z = ( y +s xR ) ) ) : No typesetting found for |- ( ( x e. No /\ y e. No ) -> ( E. xR e. ( _Right ` x ) z = ( xR +s y ) <-> E. xR e. ( _Right ` x ) z = ( y +s xR ) ) ) with typecode |-
81	80	abbidv	Could not format ( ( x e. No /\ y e. No ) -> { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } = { z | E. xR e. ( _Right ` x ) z = ( y +s xR ) } ) : No typesetting found for |- ( ( x e. No /\ y e. No ) -> { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } = { z | E. xR e. ( _Right ` x ) z = ( y +s xR ) } ) with typecode |-
82	81	imaeq2d	Could not format ( ( x e. No /\ y e. No ) -> ( bday " { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } ) = ( bday " { z | E. xR e. ( _Right ` x ) z = ( y +s xR ) } ) ) : No typesetting found for |- ( ( x e. No /\ y e. No ) -> ( bday " { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } ) = ( bday " { z | E. xR e. ( _Right ` x ) z = ( y +s xR ) } ) ) with typecode |-
83	82	adantr	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday " { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } ) = ( bday " { z | E. xR e. ( _Right ` x ) z = ( y +s xR ) } ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday " { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } ) = ( bday " { z | E. xR e. ( _Right ` x ) z = ( y +s xR ) } ) ) with typecode |-
84	74 83 66	3sstr4d	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday " { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } ) C_ ( ( bday ` x ) +no ( bday ` y ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday " { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } ) C_ ( ( bday ` x ) +no ( bday ` y ) ) ) with typecode |-
85		ssun2	$$⊢R\left(y\right)\subseteq L\left(y\right)\cup R\left(y\right)$$
86	68 69 85	addsbdaylem	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday " { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) C_ ( ( bday ` x ) +no ( bday ` y ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday " { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) C_ ( ( bday ` x ) +no ( bday ` y ) ) ) with typecode |-
87	84 86	unssd	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( ( bday " { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } ) u. ( bday " { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) C_ ( ( bday ` x ) +no ( bday ` y ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( ( bday " { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } ) u. ( bday " { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) C_ ( ( bday ` x ) +no ( bday ` y ) ) ) with typecode |-
88	72 87	unssd	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( ( ( bday " { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } ) u. ( bday " { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) ) u. ( ( bday " { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } ) u. ( bday " { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) C_ ( ( bday ` x ) +no ( bday ` y ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( ( ( bday " { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } ) u. ( bday " { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) ) u. ( ( bday " { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } ) u. ( bday " { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) C_ ( ( bday ` x ) +no ( bday ` y ) ) ) with typecode |-
89	32 88	eqsstrid	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday " ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) u. ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) C_ ( ( bday ` x ) +no ( bday ` y ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday " ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) u. ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) C_ ( ( bday ` x ) +no ( bday ` y ) ) ) with typecode |-
90		naddcl	$$⊢\left(\mathrm{bday}\left(x\right)\in \mathrm{On}\wedge \mathrm{bday}\left(y\right)\in \mathrm{On}\right)\to \mathrm{bday}\left(x\right)+\mathrm{bday}\left(y\right)\in \mathrm{On}$$
91	63 43 90	mp2an	$$⊢\mathrm{bday}\left(x\right)+\mathrm{bday}\left(y\right)\in \mathrm{On}$$
92		scutbdaybnd	Could not format ( ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) < ( bday ` ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) |s ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) C_ ( ( bday ` x ) +no ( bday ` y ) ) ) : No typesetting found for |- ( ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) < ( bday ` ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) |s ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) C_ ( ( bday ` x ) +no ( bday ` y ) ) ) with typecode |-
93	91 92	mp3an2	Could not format ( ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) < ( bday ` ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) |s ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) C_ ( ( bday ` x ) +no ( bday ` y ) ) ) : No typesetting found for |- ( ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) < ( bday ` ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) |s ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) C_ ( ( bday ` x ) +no ( bday ` y ) ) ) with typecode |-
94	27 89 93	syl2an2r	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday ` ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) |s ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) C_ ( ( bday ` x ) +no ( bday ` y ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday ` ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) |s ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) C_ ( ( bday ` x ) +no ( bday ` y ) ) ) with typecode |-
95	24 94	eqsstrd	Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday ` ( x +s y ) ) C_ ( ( bday ` x ) +no ( bday ` y ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday ` ( x +s y ) ) C_ ( ( bday ` x ) +no ( bday ` y ) ) ) with typecode |-
96	95	ex	Could not format ( ( x e. No /\ y e. No ) -> ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) -> ( bday ` ( x +s y ) ) C_ ( ( bday ` x ) +no ( bday ` y ) ) ) ) : No typesetting found for |- ( ( x e. No /\ y e. No ) -> ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) -> ( bday ` ( x +s y ) ) C_ ( ( bday ` x ) +no ( bday ` y ) ) ) ) with typecode |-
97	4 9 12 16 21 96	no2inds	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \mathrm{bday}\left(A{+}_{s}B\right)\subseteq \mathrm{bday}\left(A\right)+\mathrm{bday}\left(B\right)$$