Theorem bdaypw2n0s

Description: Upper bound for the birthday of a proper fraction of a power of two. This is actually a strict equality, but we do not need this for the rest of our development. (Contributed by Scott Fenton, 21-Feb-2026)

	Ref	Expression
Assertion	bdaypw2n0s	Could not format assertion : No typesetting found for |- ( ( A e. NN0_s /\ N e. NN0_s /\ A ( bday ` ( A /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢m=0_s\to m{+}_s{1}_s=0_s{+}_s{1}_s$$
2		1sno	$$⊢1_s\in \mathrm{No}$$
3		addslid	$$⊢1_s\in \mathrm{No}\to 0_s{+}_s{1}_s=1_s$$
4	2 3	ax-mp	$$⊢0_s{+}_s{1}_s=1_s$$
5	1 4	eqtrdi	$$⊢m=0_s\to m{+}_s{1}_s=1_s$$
6	5	oveq2d	Could not format ( m = 0s -> ( 2s ^su ( m +s 1s ) ) = ( 2s ^su 1s ) ) : No typesetting found for |- ( m = 0s -> ( 2s ^su ( m +s 1s ) ) = ( 2s ^su 1s ) ) with typecode |-
7		2sno	Could not format 2s e. No : No typesetting found for |- 2s e. No with typecode |-
8		exps1	Could not format ( 2s e. No -> ( 2s ^su 1s ) = 2s ) : No typesetting found for |- ( 2s e. No -> ( 2s ^su 1s ) = 2s ) with typecode |-
9	7 8	ax-mp	Could not format ( 2s ^su 1s ) = 2s : No typesetting found for |- ( 2s ^su 1s ) = 2s with typecode |-
10	6 9	eqtrdi	Could not format ( m = 0s -> ( 2s ^su ( m +s 1s ) ) = 2s ) : No typesetting found for |- ( m = 0s -> ( 2s ^su ( m +s 1s ) ) = 2s ) with typecode |-
11	10	breq2d	Could not format ( m = 0s -> ( a a ( a a
12	10	oveq2d	Could not format ( m = 0s -> ( a /su ( 2s ^su ( m +s 1s ) ) ) = ( a /su 2s ) ) : No typesetting found for |- ( m = 0s -> ( a /su ( 2s ^su ( m +s 1s ) ) ) = ( a /su 2s ) ) with typecode |-
13	12	fveq2d	Could not format ( m = 0s -> ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) = ( bday ` ( a /su 2s ) ) ) : No typesetting found for |- ( m = 0s -> ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) = ( bday ` ( a /su 2s ) ) ) with typecode |-
14	5	fveq2d	$$⊢m=0_s\to \mathrm{bday}\left(m{+}_s{1}_s\right)=\mathrm{bday}\left(1_s\right)$$
15		bday1s	$$⊢\mathrm{bday}\left(1_s\right)=1_{𝑜}$$
16	14 15	eqtrdi	$$⊢m=0_s\to \mathrm{bday}\left(m{+}_s{1}_s\right)=1_{𝑜}$$
17	16	suceqd	$$⊢m=0_s\to \mathrm{suc}\mathrm{bday}\left(m{+}_s{1}_s\right)=\mathrm{suc}{1}_{𝑜}$$
18		df-2o	$$⊢2_{𝑜}=\mathrm{suc}{1}_{𝑜}$$
19	17 18	eqtr4di	$$⊢m=0_s\to \mathrm{suc}\mathrm{bday}\left(m{+}_s{1}_s\right)=2_{𝑜}$$
20	13 19	sseq12d	Could not format ( m = 0s -> ( ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) <-> ( bday ` ( a /su 2s ) ) C_ 2o ) ) : No typesetting found for |- ( m = 0s -> ( ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) <-> ( bday ` ( a /su 2s ) ) C_ 2o ) ) with typecode |-
21	11 20	imbi12d	Could not format ( m = 0s -> ( ( a ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) ) <-> ( a ( bday ` ( a /su 2s ) ) C_ 2o ) ) ) : No typesetting found for |- ( m = 0s -> ( ( a ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) ) <-> ( a ( bday ` ( a /su 2s ) ) C_ 2o ) ) ) with typecode |-
22	21	ralbidv	Could not format ( m = 0s -> ( A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) ) <-> A. a e. NN0_s ( a ( bday ` ( a /su 2s ) ) C_ 2o ) ) ) : No typesetting found for |- ( m = 0s -> ( A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) ) <-> A. a e. NN0_s ( a ( bday ` ( a /su 2s ) ) C_ 2o ) ) ) with typecode |-
23		oveq1	$$⊢m=n\to m{+}_s{1}_s=n{+}_s{1}_s$$
24	23	oveq2d	Could not format ( m = n -> ( 2s ^su ( m +s 1s ) ) = ( 2s ^su ( n +s 1s ) ) ) : No typesetting found for |- ( m = n -> ( 2s ^su ( m +s 1s ) ) = ( 2s ^su ( n +s 1s ) ) ) with typecode |-
25	24	breq2d	Could not format ( m = n -> ( a a ( a a
26	24	oveq2d	Could not format ( m = n -> ( a /su ( 2s ^su ( m +s 1s ) ) ) = ( a /su ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( m = n -> ( a /su ( 2s ^su ( m +s 1s ) ) ) = ( a /su ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
27	26	fveq2d	Could not format ( m = n -> ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) = ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( m = n -> ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) = ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) ) with typecode |-
28	23	fveq2d	$$⊢m=n\to \mathrm{bday}\left(m{+}_s{1}_s\right)=\mathrm{bday}\left(n{+}_s{1}_s\right)$$
29	28	suceqd	$$⊢m=n\to \mathrm{suc}\mathrm{bday}\left(m{+}_s{1}_s\right)=\mathrm{suc}\mathrm{bday}\left(n{+}_s{1}_s\right)$$
30	27 29	sseq12d	Could not format ( m = n -> ( ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) <-> ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) : No typesetting found for |- ( m = n -> ( ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) <-> ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) with typecode |-
31	25 30	imbi12d	Could not format ( m = n -> ( ( a ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) ) <-> ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( m = n -> ( ( a ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) ) <-> ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) ) with typecode |-
32	31	ralbidv	Could not format ( m = n -> ( A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) ) <-> A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( m = n -> ( A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) ) <-> A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) ) with typecode |-
33		oveq1	$$⊢m=n{+}_s{1}_s\to m{+}_s{1}_s=\left(n{+}_s{1}_s\right){+}_s{1}_s$$
34	33	oveq2d	Could not format ( m = ( n +s 1s ) -> ( 2s ^su ( m +s 1s ) ) = ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( 2s ^su ( m +s 1s ) ) = ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) with typecode |-
35	34	breq2d	Could not format ( m = ( n +s 1s ) -> ( a a ( a a
36	34	oveq2d	Could not format ( m = ( n +s 1s ) -> ( a /su ( 2s ^su ( m +s 1s ) ) ) = ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( a /su ( 2s ^su ( m +s 1s ) ) ) = ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) with typecode |-
37	36	fveq2d	Could not format ( m = ( n +s 1s ) -> ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) = ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) = ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) ) with typecode |-
38	33	fveq2d	$$⊢m=n{+}_s{1}_s\to \mathrm{bday}\left(m{+}_s{1}_s\right)=\mathrm{bday}\left(\left(n{+}_s{1}_s\right){+}_s{1}_s\right)$$
39	38	suceqd	$$⊢m=n{+}_s{1}_s\to \mathrm{suc}\mathrm{bday}\left(m{+}_s{1}_s\right)=\mathrm{suc}\mathrm{bday}\left(\left(n{+}_s{1}_s\right){+}_s{1}_s\right)$$
40	37 39	sseq12d	Could not format ( m = ( n +s 1s ) -> ( ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) <-> ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) <-> ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) with typecode |-
41	35 40	imbi12d	Could not format ( m = ( n +s 1s ) -> ( ( a ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) ) <-> ( a ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( ( a ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) ) <-> ( a ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) ) with typecode |-
42	41	ralbidv	Could not format ( m = ( n +s 1s ) -> ( A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) ) <-> A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) ) <-> A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) ) with typecode |-
43		oveq1	$$⊢m=N\to m{+}_s{1}_s=N{+}_s{1}_s$$
44	43	oveq2d	Could not format ( m = N -> ( 2s ^su ( m +s 1s ) ) = ( 2s ^su ( N +s 1s ) ) ) : No typesetting found for |- ( m = N -> ( 2s ^su ( m +s 1s ) ) = ( 2s ^su ( N +s 1s ) ) ) with typecode |-
45	44	breq2d	Could not format ( m = N -> ( a a ( a a
46	44	oveq2d	Could not format ( m = N -> ( a /su ( 2s ^su ( m +s 1s ) ) ) = ( a /su ( 2s ^su ( N +s 1s ) ) ) ) : No typesetting found for |- ( m = N -> ( a /su ( 2s ^su ( m +s 1s ) ) ) = ( a /su ( 2s ^su ( N +s 1s ) ) ) ) with typecode |-
47	46	fveq2d	Could not format ( m = N -> ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) = ( bday ` ( a /su ( 2s ^su ( N +s 1s ) ) ) ) ) : No typesetting found for |- ( m = N -> ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) = ( bday ` ( a /su ( 2s ^su ( N +s 1s ) ) ) ) ) with typecode |-
48	43	fveq2d	$$⊢m=N\to \mathrm{bday}\left(m{+}_s{1}_s\right)=\mathrm{bday}\left(N{+}_s{1}_s\right)$$
49	48	suceqd	$$⊢m=N\to \mathrm{suc}\mathrm{bday}\left(m{+}_s{1}_s\right)=\mathrm{suc}\mathrm{bday}\left(N{+}_s{1}_s\right)$$
50	47 49	sseq12d	Could not format ( m = N -> ( ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) <-> ( bday ` ( a /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) ) : No typesetting found for |- ( m = N -> ( ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) <-> ( bday ` ( a /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) ) with typecode |-
51	45 50	imbi12d	Could not format ( m = N -> ( ( a ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) ) <-> ( a ( bday ` ( a /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) ) ) : No typesetting found for |- ( m = N -> ( ( a ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) ) <-> ( a ( bday ` ( a /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) ) ) with typecode |-
52	51	ralbidv	Could not format ( m = N -> ( A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) ) <-> A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) ) ) : No typesetting found for |- ( m = N -> ( A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( m +s 1s ) ) ) ) C_ suc ( bday ` ( m +s 1s ) ) ) <-> A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) ) ) with typecode |-
53		1n0s	$$⊢1_s\in {\mathbb{N}}_{\mathrm{0s}}$$
54		n0sleltp1	$$⊢\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge 1_s\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(a{\le }_s{1}_s\leftrightarrow a{<}_s\left(1_s{+}_s{1}_s\right)\right)$$
55	53 54	mpan2	$$⊢a\in {\mathbb{N}}_{\mathrm{0s}}\to \left(a{\le }_s{1}_s\leftrightarrow a{<}_s\left(1_s{+}_s{1}_s\right)\right)$$
56		1p1e2s	Could not format ( 1s +s 1s ) = 2s : No typesetting found for |- ( 1s +s 1s ) = 2s with typecode |-
57	56	breq2i	Could not format ( a a a
58	55 57	bitrdi	Could not format ( a e. NN0_s -> ( a <_s 1s <-> a ( a <_s 1s <-> a
59		n0sno	$$⊢a\in {\mathbb{N}}_{\mathrm{0s}}\to a\in \mathrm{No}$$
60		sleloe	$$⊢\left(a\in \mathrm{No}\wedge 1_s\in \mathrm{No}\right)\to \left(a{\le }_s{1}_s\leftrightarrow \left(a{<}_s{1}_s\vee a=1_s\right)\right)$$
61	59 2 60	sylancl	$$⊢a\in {\mathbb{N}}_{\mathrm{0s}}\to \left(a{\le }_s{1}_s\leftrightarrow \left(a{<}_s{1}_s\vee a=1_s\right)\right)$$
62		0sno	$$⊢0_s\in \mathrm{No}$$
63		sletri3	$$⊢\left(a\in \mathrm{No}\wedge 0_s\in \mathrm{No}\right)\to \left(a=0_s\leftrightarrow \left(a{\le }_s{0}_s\wedge 0_s{\le }_{s}a\right)\right)$$
64	59 62 63	sylancl	$$⊢a\in {\mathbb{N}}_{\mathrm{0s}}\to \left(a=0_s\leftrightarrow \left(a{\le }_s{0}_s\wedge 0_s{\le }_{s}a\right)\right)$$
65		n0sge0	$$⊢a\in {\mathbb{N}}_{\mathrm{0s}}\to 0_s{\le }_{s}a$$
66	65	biantrud	$$⊢a\in {\mathbb{N}}_{\mathrm{0s}}\to \left(a{\le }_s{0}_s\leftrightarrow \left(a{\le }_s{0}_s\wedge 0_s{\le }_{s}a\right)\right)$$
67	64 66	bitr4d	$$⊢a\in {\mathbb{N}}_{\mathrm{0s}}\to \left(a=0_s\leftrightarrow a{\le }_s{0}_s\right)$$
68		0n0s	$$⊢0_s\in {\mathbb{N}}_{\mathrm{0s}}$$
69		n0sleltp1	$$⊢\left(a\in {\mathbb{N}}_{\mathrm{0s}}\wedge 0_s\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(a{\le }_s{0}_s\leftrightarrow a{<}_s\left(0_s{+}_s{1}_s\right)\right)$$
70	68 69	mpan2	$$⊢a\in {\mathbb{N}}_{\mathrm{0s}}\to \left(a{\le }_s{0}_s\leftrightarrow a{<}_s\left(0_s{+}_s{1}_s\right)\right)$$
71	67 70	bitrd	$$⊢a\in {\mathbb{N}}_{\mathrm{0s}}\to \left(a=0_s\leftrightarrow a{<}_s\left(0_s{+}_s{1}_s\right)\right)$$
72	4	breq2i	$$⊢a{<}_s\left(0_s{+}_s{1}_s\right)\leftrightarrow a{<}_s{1}_s$$
73	71 72	bitrdi	$$⊢a\in {\mathbb{N}}_{\mathrm{0s}}\to \left(a=0_s\leftrightarrow a{<}_s{1}_s\right)$$
74	73	orbi1d	$$⊢a\in {\mathbb{N}}_{\mathrm{0s}}\to \left(\left(a=0_s\vee a=1_s\right)\leftrightarrow \left(a{<}_s{1}_s\vee a=1_s\right)\right)$$
75	61 74	bitr4d	$$⊢a\in {\mathbb{N}}_{\mathrm{0s}}\to \left(a{\le }_s{1}_s\leftrightarrow \left(a=0_s\vee a=1_s\right)\right)$$
76	58 75	bitr3d	Could not format ( a e. NN0_s -> ( a ( a = 0s \/ a = 1s ) ) ) : No typesetting found for |- ( a e. NN0_s -> ( a ( a = 0s \/ a = 1s ) ) ) with typecode |-
77		oveq1	Could not format ( a = 0s -> ( a /su 2s ) = ( 0s /su 2s ) ) : No typesetting found for |- ( a = 0s -> ( a /su 2s ) = ( 0s /su 2s ) ) with typecode |-
78	9	oveq2i	Could not format ( 0s /su ( 2s ^su 1s ) ) = ( 0s /su 2s ) : No typesetting found for |- ( 0s /su ( 2s ^su 1s ) ) = ( 0s /su 2s ) with typecode |-
79	53	a1i	$$⊢\top \to 1_s\in {\mathbb{N}}_{\mathrm{0s}}$$
80	79	pw2divs0d	Could not format ( T. -> ( 0s /su ( 2s ^su 1s ) ) = 0s ) : No typesetting found for |- ( T. -> ( 0s /su ( 2s ^su 1s ) ) = 0s ) with typecode |-
81	80	mptru	Could not format ( 0s /su ( 2s ^su 1s ) ) = 0s : No typesetting found for |- ( 0s /su ( 2s ^su 1s ) ) = 0s with typecode |-
82	78 81	eqtr3i	Could not format ( 0s /su 2s ) = 0s : No typesetting found for |- ( 0s /su 2s ) = 0s with typecode |-
83	77 82	eqtrdi	Could not format ( a = 0s -> ( a /su 2s ) = 0s ) : No typesetting found for |- ( a = 0s -> ( a /su 2s ) = 0s ) with typecode |-
84	83	fveq2d	Could not format ( a = 0s -> ( bday ` ( a /su 2s ) ) = ( bday ` 0s ) ) : No typesetting found for |- ( a = 0s -> ( bday ` ( a /su 2s ) ) = ( bday ` 0s ) ) with typecode |-
85		bday0s	$$⊢\mathrm{bday}\left(0_s\right)=\varnothing$$
86	84 85	eqtrdi	Could not format ( a = 0s -> ( bday ` ( a /su 2s ) ) = (/) ) : No typesetting found for |- ( a = 0s -> ( bday ` ( a /su 2s ) ) = (/) ) with typecode |-
87		0ss	$$⊢\varnothing \subseteq 2_{𝑜}$$
88	86 87	eqsstrdi	Could not format ( a = 0s -> ( bday ` ( a /su 2s ) ) C_ 2o ) : No typesetting found for |- ( a = 0s -> ( bday ` ( a /su 2s ) ) C_ 2o ) with typecode |-
89		oveq1	Could not format ( a = 1s -> ( a /su 2s ) = ( 1s /su 2s ) ) : No typesetting found for |- ( a = 1s -> ( a /su 2s ) = ( 1s /su 2s ) ) with typecode |-
90		nohalf	Could not format ( 1s /su 2s ) = ( { 0s } |s { 1s } ) : No typesetting found for |- ( 1s /su 2s ) = ( { 0s } |s { 1s } ) with typecode |-
91	89 90	eqtrdi	Could not format ( a = 1s -> ( a /su 2s ) = ( { 0s } |s { 1s } ) ) : No typesetting found for |- ( a = 1s -> ( a /su 2s ) = ( { 0s } |s { 1s } ) ) with typecode |-
92	91	fveq2d	Could not format ( a = 1s -> ( bday ` ( a /su 2s ) ) = ( bday ` ( { 0s } |s { 1s } ) ) ) : No typesetting found for |- ( a = 1s -> ( bday ` ( a /su 2s ) ) = ( bday ` ( { 0s } |s { 1s } ) ) ) with typecode |-
93	62	a1i	$$⊢\top \to 0_s\in \mathrm{No}$$
94	2	a1i	$$⊢\top \to 1_s\in \mathrm{No}$$
95		0slt1s	$$⊢0_s{<}_s{1}_s$$
96	95	a1i	$$⊢\top \to 0_s{<}_s{1}_s$$
97	93 94 96	ssltsn	$$⊢\top \to \left\{0_s\right\}{\ll }_s\left\{1_s\right\}$$
98	97	mptru	$$⊢\left\{0_s\right\}{\ll }_s\left\{1_s\right\}$$
99		2on	$$⊢2_{𝑜}\in \mathrm{On}$$
100		df-pr	$$⊢\left\{\varnothing ,1_{𝑜}\right\}=\left\{\varnothing \right\}\cup \left\{1_{𝑜}\right\}$$
101		df2o3	$$⊢2_{𝑜}=\left\{\varnothing ,1_{𝑜}\right\}$$
102		imaundi	$$⊢\mathrm{bday}\left[\left\{0_s\right\}\cup \left\{1_s\right\}\right]=\mathrm{bday}\left[\left\{0_s\right\}\right]\cup \mathrm{bday}\left[\left\{1_s\right\}\right]$$
103		bdayfn	$$⊢\mathrm{bday}Fn\mathrm{No}$$
104		fnsnfv	$$⊢\left(\mathrm{bday}Fn\mathrm{No}\wedge 0_s\in \mathrm{No}\right)\to \left\{\mathrm{bday}\left(0_s\right)\right\}=\mathrm{bday}\left[\left\{0_s\right\}\right]$$
105	103 62 104	mp2an	$$⊢\left\{\mathrm{bday}\left(0_s\right)\right\}=\mathrm{bday}\left[\left\{0_s\right\}\right]$$
106	85	sneqi	$$⊢\left\{\mathrm{bday}\left(0_s\right)\right\}=\left\{\varnothing \right\}$$
107	105 106	eqtr3i	$$⊢\mathrm{bday}\left[\left\{0_s\right\}\right]=\left\{\varnothing \right\}$$
108		fnsnfv	$$⊢\left(\mathrm{bday}Fn\mathrm{No}\wedge 1_s\in \mathrm{No}\right)\to \left\{\mathrm{bday}\left(1_s\right)\right\}=\mathrm{bday}\left[\left\{1_s\right\}\right]$$
109	103 2 108	mp2an	$$⊢\left\{\mathrm{bday}\left(1_s\right)\right\}=\mathrm{bday}\left[\left\{1_s\right\}\right]$$
110	15	sneqi	$$⊢\left\{\mathrm{bday}\left(1_s\right)\right\}=\left\{1_{𝑜}\right\}$$
111	109 110	eqtr3i	$$⊢\mathrm{bday}\left[\left\{1_s\right\}\right]=\left\{1_{𝑜}\right\}$$
112	107 111	uneq12i	$$⊢\mathrm{bday}\left[\left\{0_s\right\}\right]\cup \mathrm{bday}\left[\left\{1_s\right\}\right]=\left\{\varnothing \right\}\cup \left\{1_{𝑜}\right\}$$
113	102 112	eqtri	$$⊢\mathrm{bday}\left[\left\{0_s\right\}\cup \left\{1_s\right\}\right]=\left\{\varnothing \right\}\cup \left\{1_{𝑜}\right\}$$
114	100 101 113	3eqtr4ri	$$⊢\mathrm{bday}\left[\left\{0_s\right\}\cup \left\{1_s\right\}\right]=2_{𝑜}$$
115		ssid	$$⊢2_{𝑜}\subseteq 2_{𝑜}$$
116	114 115	eqsstri	$$⊢\mathrm{bday}\left[\left\{0_s\right\}\cup \left\{1_s\right\}\right]\subseteq 2_{𝑜}$$
117		scutbdaybnd	$$⊢\left(\left\{0_s\right\}{\ll }_s\left\{1_s\right\}\wedge 2_{𝑜}\in \mathrm{On}\wedge \mathrm{bday}\left[\left\{0_s\right\}\cup \left\{1_s\right\}\right]\subseteq 2_{𝑜}\right)\to \mathrm{bday}\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\subseteq 2_{𝑜}$$
118	98 99 116 117	mp3an	$$⊢\mathrm{bday}\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\subseteq 2_{𝑜}$$
119	92 118	eqsstrdi	Could not format ( a = 1s -> ( bday ` ( a /su 2s ) ) C_ 2o ) : No typesetting found for |- ( a = 1s -> ( bday ` ( a /su 2s ) ) C_ 2o ) with typecode |-
120	88 119	jaoi	Could not format ( ( a = 0s \/ a = 1s ) -> ( bday ` ( a /su 2s ) ) C_ 2o ) : No typesetting found for |- ( ( a = 0s \/ a = 1s ) -> ( bday ` ( a /su 2s ) ) C_ 2o ) with typecode |-
121	76 120	biimtrdi	Could not format ( a e. NN0_s -> ( a ( bday ` ( a /su 2s ) ) C_ 2o ) ) : No typesetting found for |- ( a e. NN0_s -> ( a ( bday ` ( a /su 2s ) ) C_ 2o ) ) with typecode |-
122	121	rgen	Could not format A. a e. NN0_s ( a ( bday ` ( a /su 2s ) ) C_ 2o ) : No typesetting found for |- A. a e. NN0_s ( a ( bday ` ( a /su 2s ) ) C_ 2o ) with typecode |-
123		nfv	$$⊢Ⅎan\in {\mathbb{N}}_{\mathrm{0s}}$$
124		nfra1	Could not format F/ a A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) : No typesetting found for |- F/ a A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) with typecode |-
125	123 124	nfan	Could not format F/ a ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) : No typesetting found for |- F/ a ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) with typecode |-
126		n0seo	Could not format ( a e. NN0_s -> ( E. x e. NN0_s a = ( 2s x.s x ) \/ E. x e. NN0_s a = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( a e. NN0_s -> ( E. x e. NN0_s a = ( 2s x.s x ) \/ E. x e. NN0_s a = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |-
127		breq1	Could not format ( a = x -> ( a x ( a x
128		fvoveq1	Could not format ( a = x -> ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( a = x -> ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) ) with typecode |-
129	128	sseq1d	Could not format ( a = x -> ( ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) <-> ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) : No typesetting found for |- ( a = x -> ( ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) <-> ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) with typecode |-
130	127 129	imbi12d	Could not format ( a = x -> ( ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) <-> ( x ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( a = x -> ( ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) <-> ( x ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) ) with typecode |-
131	130	rspccv	Could not format ( A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) -> ( x e. NN0_s -> ( x ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) -> ( x e. NN0_s -> ( x ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) ) with typecode |-
132	131	adantl	Could not format ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) -> ( x e. NN0_s -> ( x ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) -> ( x e. NN0_s -> ( x ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) ) with typecode |-
133	132	imp32	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ x ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ x ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) with typecode |-
134		sssucid	$$⊢\mathrm{suc}\mathrm{bday}\left(n{+}_s{1}_s\right)\subseteq \mathrm{suc}\mathrm{suc}\mathrm{bday}\left(n{+}_s{1}_s\right)$$
135	133 134	sstrdi	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ x ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc suc ( bday ` ( n +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ x ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc suc ( bday ` ( n +s 1s ) ) ) with typecode |-
136		simpll	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> n e. NN0_s ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> n e. NN0_s ) with typecode |-
137		peano2n0s	$$⊢n\in {\mathbb{N}}_{\mathrm{0s}}\to n{+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
138	136 137	syl	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( n +s 1s ) e. NN0_s ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( n +s 1s ) e. NN0_s ) with typecode |-
139	138	adantrr	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ x ( n +s 1s ) e. NN0_s ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ x ( n +s 1s ) e. NN0_s ) with typecode |-
140		bdayn0p1	$$⊢n{+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\to \mathrm{bday}\left(\left(n{+}_s{1}_s\right){+}_s{1}_s\right)=\mathrm{suc}\mathrm{bday}\left(n{+}_s{1}_s\right)$$
141	139 140	syl	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ x ( bday ` ( ( n +s 1s ) +s 1s ) ) = suc ( bday ` ( n +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ x ( bday ` ( ( n +s 1s ) +s 1s ) ) = suc ( bday ` ( n +s 1s ) ) ) with typecode |-
142	141	suceqd	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ x suc ( bday ` ( ( n +s 1s ) +s 1s ) ) = suc suc ( bday ` ( n +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ x suc ( bday ` ( ( n +s 1s ) +s 1s ) ) = suc suc ( bday ` ( n +s 1s ) ) ) with typecode |-
143	135 142	sseqtrrd	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ x ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ x ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) with typecode |-
144	143	expr	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( x ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( x ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) with typecode |-
145		expsp1	Could not format ( ( 2s e. No /\ ( n +s 1s ) e. NN0_s ) -> ( 2s ^su ( ( n +s 1s ) +s 1s ) ) = ( ( 2s ^su ( n +s 1s ) ) x.s 2s ) ) : No typesetting found for |- ( ( 2s e. No /\ ( n +s 1s ) e. NN0_s ) -> ( 2s ^su ( ( n +s 1s ) +s 1s ) ) = ( ( 2s ^su ( n +s 1s ) ) x.s 2s ) ) with typecode |-
146	7 138 145	sylancr	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( 2s ^su ( ( n +s 1s ) +s 1s ) ) = ( ( 2s ^su ( n +s 1s ) ) x.s 2s ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( 2s ^su ( ( n +s 1s ) +s 1s ) ) = ( ( 2s ^su ( n +s 1s ) ) x.s 2s ) ) with typecode |-
147		expscl	Could not format ( ( 2s e. No /\ ( n +s 1s ) e. NN0_s ) -> ( 2s ^su ( n +s 1s ) ) e. No ) : No typesetting found for |- ( ( 2s e. No /\ ( n +s 1s ) e. NN0_s ) -> ( 2s ^su ( n +s 1s ) ) e. No ) with typecode |-
148	7 138 147	sylancr	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( 2s ^su ( n +s 1s ) ) e. No ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( 2s ^su ( n +s 1s ) ) e. No ) with typecode |-
149	7	a1i	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> 2s e. No ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> 2s e. No ) with typecode |-
150	148 149	mulscomd	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s ^su ( n +s 1s ) ) x.s 2s ) = ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s ^su ( n +s 1s ) ) x.s 2s ) = ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
151	146 150	eqtrd	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( 2s ^su ( ( n +s 1s ) +s 1s ) ) = ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( 2s ^su ( ( n +s 1s ) +s 1s ) ) = ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
152	151	breq2d	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s x.s x ) ( 2s x.s x ) ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s x.s x ) ( 2s x.s x )
153		n0sno	$$⊢x\in {\mathbb{N}}_{\mathrm{0s}}\to x\in \mathrm{No}$$
154	153	adantl	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> x e. No ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> x e. No ) with typecode |-
155		2nns	Could not format 2s e. NN_s : No typesetting found for |- 2s e. NN_s with typecode |-
156		nnsgt0	Could not format ( 2s e. NN_s -> 0s 0s
157	155 156	ax-mp	Could not format 0s
158	157	a1i	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> 0s ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> 0s
159	154 148 149 158	sltmul2d	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( x ( 2s x.s x ) ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( x ( 2s x.s x )
160	152 159	bitr4d	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s x.s x ) x ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s x.s x ) x
161	53	a1i	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> 1s e. NN0_s ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> 1s e. NN0_s ) with typecode |-
162	154 138 161	pw2divscan4d	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( x /su ( 2s ^su ( n +s 1s ) ) ) = ( ( ( 2s ^su 1s ) x.s x ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( x /su ( 2s ^su ( n +s 1s ) ) ) = ( ( ( 2s ^su 1s ) x.s x ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) with typecode |-
163	162	fveq2d	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( ( ( 2s ^su 1s ) x.s x ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( ( ( 2s ^su 1s ) x.s x ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) ) with typecode |-
164	163	sseq1d	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) <-> ( bday ` ( ( ( 2s ^su 1s ) x.s x ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) <-> ( bday ` ( ( ( 2s ^su 1s ) x.s x ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) with typecode |-
165	164	bicomd	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( bday ` ( ( ( 2s ^su 1s ) x.s x ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) <-> ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( bday ` ( ( ( 2s ^su 1s ) x.s x ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) <-> ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) with typecode |-
166	144 160 165	3imtr4d	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s x.s x ) ( bday ` ( ( ( 2s ^su 1s ) x.s x ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s x.s x ) ( bday ` ( ( ( 2s ^su 1s ) x.s x ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) with typecode |-
167		breq1	Could not format ( a = ( 2s x.s x ) -> ( a ( 2s x.s x ) ( a ( 2s x.s x )
168		id	Could not format ( a = ( 2s x.s x ) -> a = ( 2s x.s x ) ) : No typesetting found for |- ( a = ( 2s x.s x ) -> a = ( 2s x.s x ) ) with typecode |-
169	9	oveq1i	Could not format ( ( 2s ^su 1s ) x.s x ) = ( 2s x.s x ) : No typesetting found for |- ( ( 2s ^su 1s ) x.s x ) = ( 2s x.s x ) with typecode |-
170	168 169	eqtr4di	Could not format ( a = ( 2s x.s x ) -> a = ( ( 2s ^su 1s ) x.s x ) ) : No typesetting found for |- ( a = ( 2s x.s x ) -> a = ( ( 2s ^su 1s ) x.s x ) ) with typecode |-
171	170	oveq1d	Could not format ( a = ( 2s x.s x ) -> ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) = ( ( ( 2s ^su 1s ) x.s x ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) : No typesetting found for |- ( a = ( 2s x.s x ) -> ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) = ( ( ( 2s ^su 1s ) x.s x ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) with typecode |-
172	171	fveq2d	Could not format ( a = ( 2s x.s x ) -> ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) = ( bday ` ( ( ( 2s ^su 1s ) x.s x ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) ) : No typesetting found for |- ( a = ( 2s x.s x ) -> ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) = ( bday ` ( ( ( 2s ^su 1s ) x.s x ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) ) with typecode |-
173	172	sseq1d	Could not format ( a = ( 2s x.s x ) -> ( ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) <-> ( bday ` ( ( ( 2s ^su 1s ) x.s x ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) : No typesetting found for |- ( a = ( 2s x.s x ) -> ( ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) <-> ( bday ` ( ( ( 2s ^su 1s ) x.s x ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) with typecode |-
174	167 173	imbi12d	Could not format ( a = ( 2s x.s x ) -> ( ( a ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) <-> ( ( 2s x.s x ) ( bday ` ( ( ( 2s ^su 1s ) x.s x ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) ) : No typesetting found for |- ( a = ( 2s x.s x ) -> ( ( a ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) <-> ( ( 2s x.s x ) ( bday ` ( ( ( 2s ^su 1s ) x.s x ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) ) with typecode |-
175	166 174	syl5ibrcom	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( a = ( 2s x.s x ) -> ( a ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( a = ( 2s x.s x ) -> ( a ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) ) with typecode |-
176	175	rexlimdva	Could not format ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) -> ( E. x e. NN0_s a = ( 2s x.s x ) -> ( a ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) -> ( E. x e. NN0_s a = ( 2s x.s x ) -> ( a ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) ) with typecode |-
177		n0zs	$$⊢x\in {\mathbb{N}}_{\mathrm{0s}}\to x\in {\mathbb{Z}}_s$$
178	177	adantl	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> x e. ZZ_s ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> x e. ZZ_s ) with typecode |-
179	178	adantrr	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) x e. ZZ_s ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) x e. ZZ_s ) with typecode |-
180	179	znod	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) x e. No ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) x e. No ) with typecode |-
181	138	adantrr	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( n +s 1s ) e. NN0_s ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( n +s 1s ) e. NN0_s ) with typecode |-
182	180 181	pw2divscld	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( x /su ( 2s ^su ( n +s 1s ) ) ) e. No ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( x /su ( 2s ^su ( n +s 1s ) ) ) e. No ) with typecode |-
183		1zs	$$⊢1_s\in {\mathbb{Z}}_s$$
184	183	a1i	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) 1s e. ZZ_s ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) 1s e. ZZ_s ) with typecode |-
185	179 184	zaddscld	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( x +s 1s ) e. ZZ_s ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( x +s 1s ) e. ZZ_s ) with typecode |-
186	185	znod	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( x +s 1s ) e. No ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( x +s 1s ) e. No ) with typecode |-
187	186 181	pw2divscld	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. No ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. No ) with typecode |-
188	180	sltp1d	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) x ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) x
189	180 186 181	pw2sltdiv1d	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( x ( x /su ( 2s ^su ( n +s 1s ) ) ) ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( x ( x /su ( 2s ^su ( n +s 1s ) ) )
190	188 189	mpbid	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( x /su ( 2s ^su ( n +s 1s ) ) ) ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( x /su ( 2s ^su ( n +s 1s ) ) )
191	182 187 190	ssltsn	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) { ( x /su ( 2s ^su ( n +s 1s ) ) ) } < ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) { ( x /su ( 2s ^su ( n +s 1s ) ) ) } <
192		imaundi	Could not format ( bday " ( { ( x /su ( 2s ^su ( n +s 1s ) ) ) } u. { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) = ( ( bday " { ( x /su ( 2s ^su ( n +s 1s ) ) ) } ) u. ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) : No typesetting found for |- ( bday " ( { ( x /su ( 2s ^su ( n +s 1s ) ) ) } u. { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) = ( ( bday " { ( x /su ( 2s ^su ( n +s 1s ) ) ) } ) u. ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) with typecode |-
193		fnsnfv	Could not format ( ( bday Fn No /\ ( x /su ( 2s ^su ( n +s 1s ) ) ) e. No ) -> { ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) } = ( bday " { ( x /su ( 2s ^su ( n +s 1s ) ) ) } ) ) : No typesetting found for |- ( ( bday Fn No /\ ( x /su ( 2s ^su ( n +s 1s ) ) ) e. No ) -> { ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) } = ( bday " { ( x /su ( 2s ^su ( n +s 1s ) ) ) } ) ) with typecode |-
194	103 182 193	sylancr	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) { ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) } = ( bday " { ( x /su ( 2s ^su ( n +s 1s ) ) ) } ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) { ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) } = ( bday " { ( x /su ( 2s ^su ( n +s 1s ) ) ) } ) ) with typecode |-
195		oveq1	Could not format ( a = x -> ( a /su ( 2s ^su ( n +s 1s ) ) ) = ( x /su ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( a = x -> ( a /su ( 2s ^su ( n +s 1s ) ) ) = ( x /su ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
196	195	fveq2d	Could not format ( a = x -> ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( a = x -> ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) ) with typecode |-
197	196	sseq1d	Could not format ( a = x -> ( ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) <-> ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) : No typesetting found for |- ( a = x -> ( ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) <-> ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) with typecode |-
198	127 197	imbi12d	Could not format ( a = x -> ( ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) <-> ( x ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( a = x -> ( ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) <-> ( x ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) ) with typecode |-
199	198	rspccv	Could not format ( A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) -> ( x e. NN0_s -> ( x ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) -> ( x e. NN0_s -> ( x ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) ) with typecode |-
200	199	imp	Could not format ( ( A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) /\ x e. NN0_s ) -> ( x ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) /\ x e. NN0_s ) -> ( x ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) with typecode |-
201	200	adantll	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( x ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( x ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) with typecode |-
202	201	adantrr	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( x ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( x ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) with typecode |-
203	148	adantrr	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( 2s ^su ( n +s 1s ) ) e. No ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( 2s ^su ( n +s 1s ) ) e. No ) with typecode |-
204	203 203	addscld	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( ( 2s ^su ( n +s 1s ) ) +s ( 2s ^su ( n +s 1s ) ) ) e. No ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( ( 2s ^su ( n +s 1s ) ) +s ( 2s ^su ( n +s 1s ) ) ) e. No ) with typecode |-
205	154	adantrr	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> x e. No ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> x e. No ) with typecode |-
206	205 203	addscld	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( x +s ( 2s ^su ( n +s 1s ) ) ) e. No ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( x +s ( 2s ^su ( n +s 1s ) ) ) e. No ) with typecode |-
207		peano2n0s	$$⊢x\in {\mathbb{N}}_{\mathrm{0s}}\to x{+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
208	207	adantl	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( x +s 1s ) e. NN0_s ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( x +s 1s ) e. NN0_s ) with typecode |-
209	208	adantrr	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( x +s 1s ) e. NN0_s ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( x +s 1s ) e. NN0_s ) with typecode |-
210	209	n0snod	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( x +s 1s ) e. No ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( x +s 1s ) e. No ) with typecode |-
211	205 210	addscld	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( x +s ( x +s 1s ) ) e. No ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( x +s ( x +s 1s ) ) e. No ) with typecode |-
212		simprr	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( 2s ^su ( n +s 1s ) ) <_s x ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( 2s ^su ( n +s 1s ) ) <_s x ) with typecode |-
213	203 205 203	sleadd1d	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( ( 2s ^su ( n +s 1s ) ) <_s x <-> ( ( 2s ^su ( n +s 1s ) ) +s ( 2s ^su ( n +s 1s ) ) ) <_s ( x +s ( 2s ^su ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( ( 2s ^su ( n +s 1s ) ) <_s x <-> ( ( 2s ^su ( n +s 1s ) ) +s ( 2s ^su ( n +s 1s ) ) ) <_s ( x +s ( 2s ^su ( n +s 1s ) ) ) ) ) with typecode |-
214	212 213	mpbid	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( ( 2s ^su ( n +s 1s ) ) +s ( 2s ^su ( n +s 1s ) ) ) <_s ( x +s ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( ( 2s ^su ( n +s 1s ) ) +s ( 2s ^su ( n +s 1s ) ) ) <_s ( x +s ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
215	205	sltp1d	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> x ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> x
216	203 205 210 212 215	slelttrd	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( 2s ^su ( n +s 1s ) ) ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( 2s ^su ( n +s 1s ) )
217	203 210 216	sltled	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( 2s ^su ( n +s 1s ) ) <_s ( x +s 1s ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( 2s ^su ( n +s 1s ) ) <_s ( x +s 1s ) ) with typecode |-
218	203 210 205	sleadd2d	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( ( 2s ^su ( n +s 1s ) ) <_s ( x +s 1s ) <-> ( x +s ( 2s ^su ( n +s 1s ) ) ) <_s ( x +s ( x +s 1s ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( ( 2s ^su ( n +s 1s ) ) <_s ( x +s 1s ) <-> ( x +s ( 2s ^su ( n +s 1s ) ) ) <_s ( x +s ( x +s 1s ) ) ) ) with typecode |-
219	217 218	mpbid	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( x +s ( 2s ^su ( n +s 1s ) ) ) <_s ( x +s ( x +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( x +s ( 2s ^su ( n +s 1s ) ) ) <_s ( x +s ( x +s 1s ) ) ) with typecode |-
220	204 206 211 214 219	sletrd	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( ( 2s ^su ( n +s 1s ) ) +s ( 2s ^su ( n +s 1s ) ) ) <_s ( x +s ( x +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( ( 2s ^su ( n +s 1s ) ) +s ( 2s ^su ( n +s 1s ) ) ) <_s ( x +s ( x +s 1s ) ) ) with typecode |-
221	138	adantrr	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( n +s 1s ) e. NN0_s ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( n +s 1s ) e. NN0_s ) with typecode |-
222	7 221 145	sylancr	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( 2s ^su ( ( n +s 1s ) +s 1s ) ) = ( ( 2s ^su ( n +s 1s ) ) x.s 2s ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( 2s ^su ( ( n +s 1s ) +s 1s ) ) = ( ( 2s ^su ( n +s 1s ) ) x.s 2s ) ) with typecode |-
223	7	a1i	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> 2s e. No ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> 2s e. No ) with typecode |-
224	203 223	mulscomd	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( ( 2s ^su ( n +s 1s ) ) x.s 2s ) = ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( ( 2s ^su ( n +s 1s ) ) x.s 2s ) = ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
225		no2times	Could not format ( ( 2s ^su ( n +s 1s ) ) e. No -> ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) = ( ( 2s ^su ( n +s 1s ) ) +s ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( 2s ^su ( n +s 1s ) ) e. No -> ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) = ( ( 2s ^su ( n +s 1s ) ) +s ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
226	203 225	syl	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) = ( ( 2s ^su ( n +s 1s ) ) +s ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) = ( ( 2s ^su ( n +s 1s ) ) +s ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
227	222 224 226	3eqtrd	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( 2s ^su ( ( n +s 1s ) +s 1s ) ) = ( ( 2s ^su ( n +s 1s ) ) +s ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( 2s ^su ( ( n +s 1s ) +s 1s ) ) = ( ( 2s ^su ( n +s 1s ) ) +s ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
228		no2times	Could not format ( x e. No -> ( 2s x.s x ) = ( x +s x ) ) : No typesetting found for |- ( x e. No -> ( 2s x.s x ) = ( x +s x ) ) with typecode |-
229	205 228	syl	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( 2s x.s x ) = ( x +s x ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( 2s x.s x ) = ( x +s x ) ) with typecode |-
230	229	oveq1d	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( ( 2s x.s x ) +s 1s ) = ( ( x +s x ) +s 1s ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( ( 2s x.s x ) +s 1s ) = ( ( x +s x ) +s 1s ) ) with typecode |-
231	2	a1i	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> 1s e. No ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> 1s e. No ) with typecode |-
232	205 205 231	addsassd	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( ( x +s x ) +s 1s ) = ( x +s ( x +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( ( x +s x ) +s 1s ) = ( x +s ( x +s 1s ) ) ) with typecode |-
233	230 232	eqtrd	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( ( 2s x.s x ) +s 1s ) = ( x +s ( x +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( ( 2s x.s x ) +s 1s ) = ( x +s ( x +s 1s ) ) ) with typecode |-
234	220 227 233	3brtr4d	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( 2s ^su ( ( n +s 1s ) +s 1s ) ) <_s ( ( 2s x.s x ) +s 1s ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) <_s x ) ) -> ( 2s ^su ( ( n +s 1s ) +s 1s ) ) <_s ( ( 2s x.s x ) +s 1s ) ) with typecode |-
235	234	expr	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s ^su ( n +s 1s ) ) <_s x -> ( 2s ^su ( ( n +s 1s ) +s 1s ) ) <_s ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s ^su ( n +s 1s ) ) <_s x -> ( 2s ^su ( ( n +s 1s ) +s 1s ) ) <_s ( ( 2s x.s x ) +s 1s ) ) ) with typecode |-
236		slenlt	Could not format ( ( ( 2s ^su ( n +s 1s ) ) e. No /\ x e. No ) -> ( ( 2s ^su ( n +s 1s ) ) <_s x <-> -. x ( ( 2s ^su ( n +s 1s ) ) <_s x <-> -. x
237	148 154 236	syl2anc	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s ^su ( n +s 1s ) ) <_s x <-> -. x ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s ^su ( n +s 1s ) ) <_s x <-> -. x
238		peano2n0s	$$⊢n{+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\to \left(n{+}_s{1}_s\right){+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
239	138 238	syl	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( n +s 1s ) +s 1s ) e. NN0_s ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( n +s 1s ) +s 1s ) e. NN0_s ) with typecode |-
240		expscl	Could not format ( ( 2s e. No /\ ( ( n +s 1s ) +s 1s ) e. NN0_s ) -> ( 2s ^su ( ( n +s 1s ) +s 1s ) ) e. No ) : No typesetting found for |- ( ( 2s e. No /\ ( ( n +s 1s ) +s 1s ) e. NN0_s ) -> ( 2s ^su ( ( n +s 1s ) +s 1s ) ) e. No ) with typecode |-
241	7 239 240	sylancr	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( 2s ^su ( ( n +s 1s ) +s 1s ) ) e. No ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( 2s ^su ( ( n +s 1s ) +s 1s ) ) e. No ) with typecode |-
242		nnn0s	Could not format ( 2s e. NN_s -> 2s e. NN0_s ) : No typesetting found for |- ( 2s e. NN_s -> 2s e. NN0_s ) with typecode |-
243	155 242	ax-mp	Could not format 2s e. NN0_s : No typesetting found for |- 2s e. NN0_s with typecode |-
244		n0mulscl	Could not format ( ( 2s e. NN0_s /\ x e. NN0_s ) -> ( 2s x.s x ) e. NN0_s ) : No typesetting found for |- ( ( 2s e. NN0_s /\ x e. NN0_s ) -> ( 2s x.s x ) e. NN0_s ) with typecode |-
245	243 244	mpan	Could not format ( x e. NN0_s -> ( 2s x.s x ) e. NN0_s ) : No typesetting found for |- ( x e. NN0_s -> ( 2s x.s x ) e. NN0_s ) with typecode |-
246	245	adantl	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( 2s x.s x ) e. NN0_s ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( 2s x.s x ) e. NN0_s ) with typecode |-
247		n0addscl	Could not format ( ( ( 2s x.s x ) e. NN0_s /\ 1s e. NN0_s ) -> ( ( 2s x.s x ) +s 1s ) e. NN0_s ) : No typesetting found for |- ( ( ( 2s x.s x ) e. NN0_s /\ 1s e. NN0_s ) -> ( ( 2s x.s x ) +s 1s ) e. NN0_s ) with typecode |-
248	246 53 247	sylancl	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s x.s x ) +s 1s ) e. NN0_s ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s x.s x ) +s 1s ) e. NN0_s ) with typecode |-
249	248	n0snod	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s x.s x ) +s 1s ) e. No ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s x.s x ) +s 1s ) e. No ) with typecode |-
250		slenlt	Could not format ( ( ( 2s ^su ( ( n +s 1s ) +s 1s ) ) e. No /\ ( ( 2s x.s x ) +s 1s ) e. No ) -> ( ( 2s ^su ( ( n +s 1s ) +s 1s ) ) <_s ( ( 2s x.s x ) +s 1s ) <-> -. ( ( 2s x.s x ) +s 1s ) ( ( 2s ^su ( ( n +s 1s ) +s 1s ) ) <_s ( ( 2s x.s x ) +s 1s ) <-> -. ( ( 2s x.s x ) +s 1s )
251	241 249 250	syl2anc	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s ^su ( ( n +s 1s ) +s 1s ) ) <_s ( ( 2s x.s x ) +s 1s ) <-> -. ( ( 2s x.s x ) +s 1s ) ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s ^su ( ( n +s 1s ) +s 1s ) ) <_s ( ( 2s x.s x ) +s 1s ) <-> -. ( ( 2s x.s x ) +s 1s )
252	235 237 251	3imtr3d	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( -. x -. ( ( 2s x.s x ) +s 1s ) ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( -. x -. ( ( 2s x.s x ) +s 1s )
253	252	con4d	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( 2s x.s x ) +s 1s ) x ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( 2s x.s x ) +s 1s ) x
254	253	impr	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) x ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) x
255		id	Could not format ( ( x ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) -> ( x ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( x ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) -> ( x ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) with typecode |-
256	202 254 255	sylc	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) with typecode |-
257		bdayelon	Could not format ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) e. On : No typesetting found for |- ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) e. On with typecode |-
258		bdayelon	$$⊢\mathrm{bday}\left(n{+}_s{1}_s\right)\in \mathrm{On}$$
259	258	onsuci	$$⊢\mathrm{suc}\mathrm{bday}\left(n{+}_s{1}_s\right)\in \mathrm{On}$$
260		onsssuc	Could not format ( ( ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) e. On /\ suc ( bday ` ( n +s 1s ) ) e. On ) -> ( ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) <-> ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc ( bday ` ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) e. On /\ suc ( bday ` ( n +s 1s ) ) e. On ) -> ( ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) <-> ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc ( bday ` ( n +s 1s ) ) ) ) with typecode |-
261	257 259 260	mp2an	Could not format ( ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) <-> ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc ( bday ` ( n +s 1s ) ) ) : No typesetting found for |- ( ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) <-> ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc ( bday ` ( n +s 1s ) ) ) with typecode |-
262	256 261	sylib	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc ( bday ` ( n +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc ( bday ` ( n +s 1s ) ) ) with typecode |-
263	262	snssd	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) { ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) } C_ suc suc ( bday ` ( n +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) { ( bday ` ( x /su ( 2s ^su ( n +s 1s ) ) ) ) } C_ suc suc ( bday ` ( n +s 1s ) ) ) with typecode |-
264	194 263	eqsstrrd	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( bday " { ( x /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( bday " { ( x /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) ) with typecode |-
265	151	breq2d	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( 2s x.s x ) +s 1s ) ( ( 2s x.s x ) +s 1s ) ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( 2s x.s x ) +s 1s ) ( ( 2s x.s x ) +s 1s )
266		n0expscl	Could not format ( ( 2s e. NN0_s /\ ( n +s 1s ) e. NN0_s ) -> ( 2s ^su ( n +s 1s ) ) e. NN0_s ) : No typesetting found for |- ( ( 2s e. NN0_s /\ ( n +s 1s ) e. NN0_s ) -> ( 2s ^su ( n +s 1s ) ) e. NN0_s ) with typecode |-
267	243 138 266	sylancr	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( 2s ^su ( n +s 1s ) ) e. NN0_s ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( 2s ^su ( n +s 1s ) ) e. NN0_s ) with typecode |-
268		n0mulscl	Could not format ( ( 2s e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) e. NN0_s ) -> ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) e. NN0_s ) : No typesetting found for |- ( ( 2s e. NN0_s /\ ( 2s ^su ( n +s 1s ) ) e. NN0_s ) -> ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) e. NN0_s ) with typecode |-
269	243 267 268	sylancr	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) e. NN0_s ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) e. NN0_s ) with typecode |-
270		n0sltp1le	Could not format ( ( ( ( 2s x.s x ) +s 1s ) e. NN0_s /\ ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) e. NN0_s ) -> ( ( ( 2s x.s x ) +s 1s ) ( ( ( 2s x.s x ) +s 1s ) +s 1s ) <_s ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( ( ( ( 2s x.s x ) +s 1s ) e. NN0_s /\ ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) e. NN0_s ) -> ( ( ( 2s x.s x ) +s 1s ) ( ( ( 2s x.s x ) +s 1s ) +s 1s ) <_s ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) ) ) with typecode |-
271	248 269 270	syl2anc	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( 2s x.s x ) +s 1s ) ( ( ( 2s x.s x ) +s 1s ) +s 1s ) <_s ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( 2s x.s x ) +s 1s ) ( ( ( 2s x.s x ) +s 1s ) +s 1s ) <_s ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) ) ) with typecode |-
272	149 154	mulscld	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( 2s x.s x ) e. No ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( 2s x.s x ) e. No ) with typecode |-
273	2	a1i	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> 1s e. No ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> 1s e. No ) with typecode |-
274	272 273 273	addsassd	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( 2s x.s x ) +s 1s ) +s 1s ) = ( ( 2s x.s x ) +s ( 1s +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( 2s x.s x ) +s 1s ) +s 1s ) = ( ( 2s x.s x ) +s ( 1s +s 1s ) ) ) with typecode |-
275		mulsrid	Could not format ( 2s e. No -> ( 2s x.s 1s ) = 2s ) : No typesetting found for |- ( 2s e. No -> ( 2s x.s 1s ) = 2s ) with typecode |-
276	7 275	ax-mp	Could not format ( 2s x.s 1s ) = 2s : No typesetting found for |- ( 2s x.s 1s ) = 2s with typecode |-
277	276	eqcomi	Could not format 2s = ( 2s x.s 1s ) : No typesetting found for |- 2s = ( 2s x.s 1s ) with typecode |-
278	56 277	eqtri	Could not format ( 1s +s 1s ) = ( 2s x.s 1s ) : No typesetting found for |- ( 1s +s 1s ) = ( 2s x.s 1s ) with typecode |-
279	278	oveq2i	Could not format ( ( 2s x.s x ) +s ( 1s +s 1s ) ) = ( ( 2s x.s x ) +s ( 2s x.s 1s ) ) : No typesetting found for |- ( ( 2s x.s x ) +s ( 1s +s 1s ) ) = ( ( 2s x.s x ) +s ( 2s x.s 1s ) ) with typecode |-
280	149 154 273	addsdid	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( 2s x.s ( x +s 1s ) ) = ( ( 2s x.s x ) +s ( 2s x.s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( 2s x.s ( x +s 1s ) ) = ( ( 2s x.s x ) +s ( 2s x.s 1s ) ) ) with typecode |-
281	280	eqcomd	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s x.s x ) +s ( 2s x.s 1s ) ) = ( 2s x.s ( x +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s x.s x ) +s ( 2s x.s 1s ) ) = ( 2s x.s ( x +s 1s ) ) ) with typecode |-
282	279 281	eqtrid	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s x.s x ) +s ( 1s +s 1s ) ) = ( 2s x.s ( x +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s x.s x ) +s ( 1s +s 1s ) ) = ( 2s x.s ( x +s 1s ) ) ) with typecode |-
283	274 282	eqtrd	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( 2s x.s x ) +s 1s ) +s 1s ) = ( 2s x.s ( x +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( 2s x.s x ) +s 1s ) +s 1s ) = ( 2s x.s ( x +s 1s ) ) ) with typecode |-
284	283	breq1d	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( ( 2s x.s x ) +s 1s ) +s 1s ) <_s ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) <-> ( 2s x.s ( x +s 1s ) ) <_s ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( ( 2s x.s x ) +s 1s ) +s 1s ) <_s ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) <-> ( 2s x.s ( x +s 1s ) ) <_s ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) ) ) with typecode |-
285	208	n0snod	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( x +s 1s ) e. No ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( x +s 1s ) e. No ) with typecode |-
286	285 148 149 158	slemul2d	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( x +s 1s ) <_s ( 2s ^su ( n +s 1s ) ) <-> ( 2s x.s ( x +s 1s ) ) <_s ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( x +s 1s ) <_s ( 2s ^su ( n +s 1s ) ) <-> ( 2s x.s ( x +s 1s ) ) <_s ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) ) ) with typecode |-
287	286	bicomd	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s x.s ( x +s 1s ) ) <_s ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) <-> ( x +s 1s ) <_s ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s x.s ( x +s 1s ) ) <_s ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) <-> ( x +s 1s ) <_s ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
288	284 287	bitrd	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( ( 2s x.s x ) +s 1s ) +s 1s ) <_s ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) <-> ( x +s 1s ) <_s ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( ( 2s x.s x ) +s 1s ) +s 1s ) <_s ( 2s x.s ( 2s ^su ( n +s 1s ) ) ) <-> ( x +s 1s ) <_s ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
289	271 288	bitrd	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( 2s x.s x ) +s 1s ) ( x +s 1s ) <_s ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( 2s x.s x ) +s 1s ) ( x +s 1s ) <_s ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
290	265 289	bitrd	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( 2s x.s x ) +s 1s ) ( x +s 1s ) <_s ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( 2s x.s x ) +s 1s ) ( x +s 1s ) <_s ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
291		sleloe	Could not format ( ( ( x +s 1s ) e. No /\ ( 2s ^su ( n +s 1s ) ) e. No ) -> ( ( x +s 1s ) <_s ( 2s ^su ( n +s 1s ) ) <-> ( ( x +s 1s ) ( ( x +s 1s ) <_s ( 2s ^su ( n +s 1s ) ) <-> ( ( x +s 1s )
292	285 148 291	syl2anc	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( x +s 1s ) <_s ( 2s ^su ( n +s 1s ) ) <-> ( ( x +s 1s ) ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( x +s 1s ) <_s ( 2s ^su ( n +s 1s ) ) <-> ( ( x +s 1s )
293	285 138	pw2divscld	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. No ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. No ) with typecode |-
294	293	adantrr	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( x +s 1s ) ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. No ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( x +s 1s ) ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. No ) with typecode |-
295		fnsnfv	Could not format ( ( bday Fn No /\ ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. No ) -> { ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) } = ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) : No typesetting found for |- ( ( bday Fn No /\ ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) e. No ) -> { ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) } = ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) with typecode |-
296	103 294 295	sylancr	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( x +s 1s ) { ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) } = ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( x +s 1s ) { ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) } = ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) with typecode |-
297		breq1	Could not format ( a = ( x +s 1s ) -> ( a ( x +s 1s ) ( a ( x +s 1s )
298		fvoveq1	Could not format ( a = ( x +s 1s ) -> ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( a = ( x +s 1s ) -> ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) ) with typecode |-
299	298	sseq1d	Could not format ( a = ( x +s 1s ) -> ( ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) <-> ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) : No typesetting found for |- ( a = ( x +s 1s ) -> ( ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) <-> ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) with typecode |-
300	297 299	imbi12d	Could not format ( a = ( x +s 1s ) -> ( ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) <-> ( ( x +s 1s ) ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( a = ( x +s 1s ) -> ( ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) <-> ( ( x +s 1s ) ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) ) with typecode |-
301	300	rspccv	Could not format ( A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) -> ( ( x +s 1s ) e. NN0_s -> ( ( x +s 1s ) ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) -> ( ( x +s 1s ) e. NN0_s -> ( ( x +s 1s ) ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) ) with typecode |-
302	207 301	syl5	Could not format ( A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) -> ( x e. NN0_s -> ( ( x +s 1s ) ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) -> ( x e. NN0_s -> ( ( x +s 1s ) ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) ) with typecode |-
303	302	adantl	Could not format ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) -> ( x e. NN0_s -> ( ( x +s 1s ) ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) -> ( x e. NN0_s -> ( ( x +s 1s ) ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) ) with typecode |-
304	303	imp32	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( x +s 1s ) ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( x +s 1s ) ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) with typecode |-
305		bdayelon	Could not format ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. On : No typesetting found for |- ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. On with typecode |-
306		onsssuc	Could not format ( ( ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. On /\ suc ( bday ` ( n +s 1s ) ) e. On ) -> ( ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) <-> ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc ( bday ` ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. On /\ suc ( bday ` ( n +s 1s ) ) e. On ) -> ( ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) <-> ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc ( bday ` ( n +s 1s ) ) ) ) with typecode |-
307	305 259 306	mp2an	Could not format ( ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) <-> ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc ( bday ` ( n +s 1s ) ) ) : No typesetting found for |- ( ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) <-> ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc ( bday ` ( n +s 1s ) ) ) with typecode |-
308	304 307	sylib	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( x +s 1s ) ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc ( bday ` ( n +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( x +s 1s ) ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc ( bday ` ( n +s 1s ) ) ) with typecode |-
309	308	snssd	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( x +s 1s ) { ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) } C_ suc suc ( bday ` ( n +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( x +s 1s ) { ( bday ` ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) } C_ suc suc ( bday ` ( n +s 1s ) ) ) with typecode |-
310	296 309	eqsstrrd	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( x +s 1s ) ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( x +s 1s ) ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) ) with typecode |-
311	310	expr	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( x +s 1s ) ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( x +s 1s ) ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) ) ) with typecode |-
312	138	pw2divsidd	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s ^su ( n +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) = 1s ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( 2s ^su ( n +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) = 1s ) with typecode |-
313	312	sneqd	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> { ( ( 2s ^su ( n +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) } = { 1s } ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> { ( ( 2s ^su ( n +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) } = { 1s } ) with typecode |-
314	313	imaeq2d	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( bday " { ( ( 2s ^su ( n +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) } ) = ( bday " { 1s } ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( bday " { ( ( 2s ^su ( n +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) } ) = ( bday " { 1s } ) ) with typecode |-
315		df-1o	$$⊢1_{𝑜}=\mathrm{suc}\varnothing$$
316	15 315	eqtri	$$⊢\mathrm{bday}\left(1_s\right)=\mathrm{suc}\varnothing$$
317		0ss	$$⊢\varnothing \subseteq \mathrm{bday}\left(n{+}_s{1}_s\right)$$
318		ord0	$$⊢\mathrm{Ord}\varnothing$$
319	258	onordi	$$⊢\mathrm{Ord}\mathrm{bday}\left(n{+}_s{1}_s\right)$$
320		ordsucsssuc	$$⊢\left(\mathrm{Ord}\varnothing \wedge \mathrm{Ord}\mathrm{bday}\left(n{+}_s{1}_s\right)\right)\to \left(\varnothing \subseteq \mathrm{bday}\left(n{+}_s{1}_s\right)\leftrightarrow \mathrm{suc}\varnothing \subseteq \mathrm{suc}\mathrm{bday}\left(n{+}_s{1}_s\right)\right)$$
321	318 319 320	mp2an	$$⊢\varnothing \subseteq \mathrm{bday}\left(n{+}_s{1}_s\right)\leftrightarrow \mathrm{suc}\varnothing \subseteq \mathrm{suc}\mathrm{bday}\left(n{+}_s{1}_s\right)$$
322	317 321	mpbi	$$⊢\mathrm{suc}\varnothing \subseteq \mathrm{suc}\mathrm{bday}\left(n{+}_s{1}_s\right)$$
323	316 322	eqsstri	$$⊢\mathrm{bday}\left(1_s\right)\subseteq \mathrm{suc}\mathrm{bday}\left(n{+}_s{1}_s\right)$$
324		bdayelon	$$⊢\mathrm{bday}\left(1_s\right)\in \mathrm{On}$$
325		onsssuc	$$⊢\left(\mathrm{bday}\left(1_s\right)\in \mathrm{On}\wedge \mathrm{suc}\mathrm{bday}\left(n{+}_s{1}_s\right)\in \mathrm{On}\right)\to \left(\mathrm{bday}\left(1_s\right)\subseteq \mathrm{suc}\mathrm{bday}\left(n{+}_s{1}_s\right)\leftrightarrow \mathrm{bday}\left(1_s\right)\in \mathrm{suc}\mathrm{suc}\mathrm{bday}\left(n{+}_s{1}_s\right)\right)$$
326	324 259 325	mp2an	$$⊢\mathrm{bday}\left(1_s\right)\subseteq \mathrm{suc}\mathrm{bday}\left(n{+}_s{1}_s\right)\leftrightarrow \mathrm{bday}\left(1_s\right)\in \mathrm{suc}\mathrm{suc}\mathrm{bday}\left(n{+}_s{1}_s\right)$$
327	323 326	mpbi	$$⊢\mathrm{bday}\left(1_s\right)\in \mathrm{suc}\mathrm{suc}\mathrm{bday}\left(n{+}_s{1}_s\right)$$
328	327	a1i	$$⊢n\in {\mathbb{N}}_{\mathrm{0s}}\to \mathrm{bday}\left(1_s\right)\in \mathrm{suc}\mathrm{suc}\mathrm{bday}\left(n{+}_s{1}_s\right)$$
329	328	snssd	$$⊢n\in {\mathbb{N}}_{\mathrm{0s}}\to \left\{\mathrm{bday}\left(1_s\right)\right\}\subseteq \mathrm{suc}\mathrm{suc}\mathrm{bday}\left(n{+}_s{1}_s\right)$$
330	109 329	eqsstrrid	$$⊢n\in {\mathbb{N}}_{\mathrm{0s}}\to \mathrm{bday}\left[\left\{1_s\right\}\right]\subseteq \mathrm{suc}\mathrm{suc}\mathrm{bday}\left(n{+}_s{1}_s\right)$$
331	330	adantr	Could not format ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) -> ( bday " { 1s } ) C_ suc suc ( bday ` ( n +s 1s ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) -> ( bday " { 1s } ) C_ suc suc ( bday ` ( n +s 1s ) ) ) with typecode |-
332	331	adantr	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( bday " { 1s } ) C_ suc suc ( bday ` ( n +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( bday " { 1s } ) C_ suc suc ( bday ` ( n +s 1s ) ) ) with typecode |-
333	314 332	eqsstrd	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( bday " { ( ( 2s ^su ( n +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( bday " { ( ( 2s ^su ( n +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) ) with typecode |-
334		oveq1	Could not format ( ( x +s 1s ) = ( 2s ^su ( n +s 1s ) ) -> ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( 2s ^su ( n +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( x +s 1s ) = ( 2s ^su ( n +s 1s ) ) -> ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( 2s ^su ( n +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
335	334	sneqd	Could not format ( ( x +s 1s ) = ( 2s ^su ( n +s 1s ) ) -> { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } = { ( ( 2s ^su ( n +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) } ) : No typesetting found for |- ( ( x +s 1s ) = ( 2s ^su ( n +s 1s ) ) -> { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } = { ( ( 2s ^su ( n +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) } ) with typecode |-
336	335	imaeq2d	Could not format ( ( x +s 1s ) = ( 2s ^su ( n +s 1s ) ) -> ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) = ( bday " { ( ( 2s ^su ( n +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) : No typesetting found for |- ( ( x +s 1s ) = ( 2s ^su ( n +s 1s ) ) -> ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) = ( bday " { ( ( 2s ^su ( n +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) with typecode |-
337	336	sseq1d	Could not format ( ( x +s 1s ) = ( 2s ^su ( n +s 1s ) ) -> ( ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) <-> ( bday " { ( ( 2s ^su ( n +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( x +s 1s ) = ( 2s ^su ( n +s 1s ) ) -> ( ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) <-> ( bday " { ( ( 2s ^su ( n +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) ) ) with typecode |-
338	333 337	syl5ibrcom	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( x +s 1s ) = ( 2s ^su ( n +s 1s ) ) -> ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( x +s 1s ) = ( 2s ^su ( n +s 1s ) ) -> ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) ) ) with typecode |-
339	311 338	jaod	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( x +s 1s ) ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( x +s 1s ) ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) ) ) with typecode |-
340	292 339	sylbid	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( x +s 1s ) <_s ( 2s ^su ( n +s 1s ) ) -> ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( x +s 1s ) <_s ( 2s ^su ( n +s 1s ) ) -> ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) ) ) with typecode |-
341	290 340	sylbid	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( 2s x.s x ) +s 1s ) ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( 2s x.s x ) +s 1s ) ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) ) ) with typecode |-
342	341	impr	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) C_ suc suc ( bday ` ( n +s 1s ) ) ) with typecode |-
343	264 342	unssd	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( ( bday " { ( x /su ( 2s ^su ( n +s 1s ) ) ) } ) u. ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) C_ suc suc ( bday ` ( n +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( ( bday " { ( x /su ( 2s ^su ( n +s 1s ) ) ) } ) u. ( bday " { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) C_ suc suc ( bday ` ( n +s 1s ) ) ) with typecode |-
344	192 343	eqsstrid	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( bday " ( { ( x /su ( 2s ^su ( n +s 1s ) ) ) } u. { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) C_ suc suc ( bday ` ( n +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( bday " ( { ( x /su ( 2s ^su ( n +s 1s ) ) ) } u. { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) C_ suc suc ( bday ` ( n +s 1s ) ) ) with typecode |-
345	259	onsuci	$$⊢\mathrm{suc}\mathrm{suc}\mathrm{bday}\left(n{+}_s{1}_s\right)\in \mathrm{On}$$
346		scutbdaybnd	Could not format ( ( { ( x /su ( 2s ^su ( n +s 1s ) ) ) } < ( bday ` ( { ( x /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) C_ suc suc ( bday ` ( n +s 1s ) ) ) : No typesetting found for |- ( ( { ( x /su ( 2s ^su ( n +s 1s ) ) ) } < ( bday ` ( { ( x /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) C_ suc suc ( bday ` ( n +s 1s ) ) ) with typecode |-
347	345 346	mp3an2	Could not format ( ( { ( x /su ( 2s ^su ( n +s 1s ) ) ) } < ( bday ` ( { ( x /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) C_ suc suc ( bday ` ( n +s 1s ) ) ) : No typesetting found for |- ( ( { ( x /su ( 2s ^su ( n +s 1s ) ) ) } < ( bday ` ( { ( x /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) C_ suc suc ( bday ` ( n +s 1s ) ) ) with typecode |-
348	191 344 347	syl2anc	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( bday ` ( { ( x /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) C_ suc suc ( bday ` ( n +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( bday ` ( { ( x /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) C_ suc suc ( bday ` ( n +s 1s ) ) ) with typecode |-
349	179 181	pw2cutp1	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( { ( x /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( { ( x /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) with typecode |-
350	349	fveq2d	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( bday ` ( { ( x /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) = ( bday ` ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( bday ` ( { ( x /su ( 2s ^su ( n +s 1s ) ) ) } |s { ( ( x +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) } ) ) = ( bday ` ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) ) with typecode |-
351	181 140	syl	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( bday ` ( ( n +s 1s ) +s 1s ) ) = suc ( bday ` ( n +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( bday ` ( ( n +s 1s ) +s 1s ) ) = suc ( bday ` ( n +s 1s ) ) ) with typecode |-
352	351	suceqd	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) suc ( bday ` ( ( n +s 1s ) +s 1s ) ) = suc suc ( bday ` ( n +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) suc ( bday ` ( ( n +s 1s ) +s 1s ) ) = suc suc ( bday ` ( n +s 1s ) ) ) with typecode |-
353	352	eqcomd	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) suc suc ( bday ` ( n +s 1s ) ) = suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) suc suc ( bday ` ( n +s 1s ) ) = suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) with typecode |-
354	348 350 353	3sstr3d	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( bday ` ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) ( bday ` ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) with typecode |-
355	354	expr	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( 2s x.s x ) +s 1s ) ( bday ` ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( ( ( 2s x.s x ) +s 1s ) ( bday ` ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) with typecode |-
356		breq1	Could not format ( a = ( ( 2s x.s x ) +s 1s ) -> ( a ( ( 2s x.s x ) +s 1s ) ( a ( ( 2s x.s x ) +s 1s )
357		oveq1	Could not format ( a = ( ( 2s x.s x ) +s 1s ) -> ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) : No typesetting found for |- ( a = ( ( 2s x.s x ) +s 1s ) -> ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) = ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) with typecode |-
358	357	fveq2d	Could not format ( a = ( ( 2s x.s x ) +s 1s ) -> ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) = ( bday ` ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) ) : No typesetting found for |- ( a = ( ( 2s x.s x ) +s 1s ) -> ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) = ( bday ` ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) ) with typecode |-
359	358	sseq1d	Could not format ( a = ( ( 2s x.s x ) +s 1s ) -> ( ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) <-> ( bday ` ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) : No typesetting found for |- ( a = ( ( 2s x.s x ) +s 1s ) -> ( ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) <-> ( bday ` ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) with typecode |-
360	356 359	imbi12d	Could not format ( a = ( ( 2s x.s x ) +s 1s ) -> ( ( a ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) <-> ( ( ( 2s x.s x ) +s 1s ) ( bday ` ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) ) : No typesetting found for |- ( a = ( ( 2s x.s x ) +s 1s ) -> ( ( a ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) <-> ( ( ( 2s x.s x ) +s 1s ) ( bday ` ( ( ( 2s x.s x ) +s 1s ) /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) ) with typecode |-
361	355 360	syl5ibrcom	Could not format ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( a = ( ( 2s x.s x ) +s 1s ) -> ( a ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) /\ x e. NN0_s ) -> ( a = ( ( 2s x.s x ) +s 1s ) -> ( a ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) ) with typecode |-
362	361	rexlimdva	Could not format ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) -> ( E. x e. NN0_s a = ( ( 2s x.s x ) +s 1s ) -> ( a ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) -> ( E. x e. NN0_s a = ( ( 2s x.s x ) +s 1s ) -> ( a ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) ) with typecode |-
363	176 362	jaod	Could not format ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) -> ( ( E. x e. NN0_s a = ( 2s x.s x ) \/ E. x e. NN0_s a = ( ( 2s x.s x ) +s 1s ) ) -> ( a ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) -> ( ( E. x e. NN0_s a = ( 2s x.s x ) \/ E. x e. NN0_s a = ( ( 2s x.s x ) +s 1s ) ) -> ( a ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) ) with typecode |-
364	126 363	syl5	Could not format ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) -> ( a e. NN0_s -> ( a ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) -> ( a e. NN0_s -> ( a ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) ) with typecode |-
365	125 364	ralrimi	Could not format ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) -> A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) ) -> A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) with typecode |-
366	365	ex	Could not format ( n e. NN0_s -> ( A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) -> A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) ) : No typesetting found for |- ( n e. NN0_s -> ( A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( n +s 1s ) ) ) -> A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( ( n +s 1s ) +s 1s ) ) ) ) C_ suc ( bday ` ( ( n +s 1s ) +s 1s ) ) ) ) ) with typecode |-
367	22 32 42 52 122 366	n0sind	Could not format ( N e. NN0_s -> A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) ) : No typesetting found for |- ( N e. NN0_s -> A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) ) with typecode |-
368		breq1	Could not format ( a = A -> ( a A ( a A
369		oveq1	Could not format ( a = A -> ( a /su ( 2s ^su ( N +s 1s ) ) ) = ( A /su ( 2s ^su ( N +s 1s ) ) ) ) : No typesetting found for |- ( a = A -> ( a /su ( 2s ^su ( N +s 1s ) ) ) = ( A /su ( 2s ^su ( N +s 1s ) ) ) ) with typecode |-
370	369	fveq2d	Could not format ( a = A -> ( bday ` ( a /su ( 2s ^su ( N +s 1s ) ) ) ) = ( bday ` ( A /su ( 2s ^su ( N +s 1s ) ) ) ) ) : No typesetting found for |- ( a = A -> ( bday ` ( a /su ( 2s ^su ( N +s 1s ) ) ) ) = ( bday ` ( A /su ( 2s ^su ( N +s 1s ) ) ) ) ) with typecode |-
371	370	sseq1d	Could not format ( a = A -> ( ( bday ` ( a /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) <-> ( bday ` ( A /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) ) : No typesetting found for |- ( a = A -> ( ( bday ` ( a /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) <-> ( bday ` ( A /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) ) with typecode |-
372	368 371	imbi12d	Could not format ( a = A -> ( ( a ( bday ` ( a /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) <-> ( A ( bday ` ( A /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) ) ) : No typesetting found for |- ( a = A -> ( ( a ( bday ` ( a /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) <-> ( A ( bday ` ( A /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) ) ) with typecode |-
373	372	rspccv	Could not format ( A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) -> ( A e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) ) ) : No typesetting found for |- ( A. a e. NN0_s ( a ( bday ` ( a /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) -> ( A e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) ) ) with typecode |-
374	367 373	syl	Could not format ( N e. NN0_s -> ( A e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) ) ) : No typesetting found for |- ( N e. NN0_s -> ( A e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) ) ) with typecode |-
375	374	com12	Could not format ( A e. NN0_s -> ( N e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) ) ) : No typesetting found for |- ( A e. NN0_s -> ( N e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) ) ) with typecode |-
376	375	3imp	Could not format ( ( A e. NN0_s /\ N e. NN0_s /\ A ( bday ` ( A /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) : No typesetting found for |- ( ( A e. NN0_s /\ N e. NN0_s /\ A ( bday ` ( A /su ( 2s ^su ( N +s 1s ) ) ) ) C_ suc ( bday ` ( N +s 1s ) ) ) with typecode |-