Theorem mulsprop

Description: Surreals are closed under multiplication and obey a particular ordering law. Theorem 3.4 of Gonshor p. 17. (Contributed by Scott Fenton, 5-Mar-2025)

	Ref	Expression
Assertion	mulsprop	Could not format assertion : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ ( C e. No /\ D e. No ) /\ ( E e. No /\ F e. No ) ) -> ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s F ) -s ( C x.s E ) )

Proof

Step	Hyp	Ref	Expression
1		bdayelon	$$⊢\mathrm{bday}\left(A\right)\in \mathrm{On}$$
2		bdayelon	$$⊢\mathrm{bday}\left(B\right)\in \mathrm{On}$$
3		naddcl	Could not format ( ( ( bday ` A ) e. On /\ ( bday ` B ) e. On ) -> ( ( bday ` A ) +no ( bday ` B ) ) e. On ) : No typesetting found for |- ( ( ( bday ` A ) e. On /\ ( bday ` B ) e. On ) -> ( ( bday ` A ) +no ( bday ` B ) ) e. On ) with typecode |-
4	1 2 3	mp2an	Could not format ( ( bday ` A ) +no ( bday ` B ) ) e. On : No typesetting found for |- ( ( bday ` A ) +no ( bday ` B ) ) e. On with typecode |-
5		bdayelon	$$⊢\mathrm{bday}\left(C\right)\in \mathrm{On}$$
6		bdayelon	$$⊢\mathrm{bday}\left(E\right)\in \mathrm{On}$$
7		naddcl	Could not format ( ( ( bday ` C ) e. On /\ ( bday ` E ) e. On ) -> ( ( bday ` C ) +no ( bday ` E ) ) e. On ) : No typesetting found for |- ( ( ( bday ` C ) e. On /\ ( bday ` E ) e. On ) -> ( ( bday ` C ) +no ( bday ` E ) ) e. On ) with typecode |-
8	5 6 7	mp2an	Could not format ( ( bday ` C ) +no ( bday ` E ) ) e. On : No typesetting found for |- ( ( bday ` C ) +no ( bday ` E ) ) e. On with typecode |-
9		bdayelon	$$⊢\mathrm{bday}\left(D\right)\in \mathrm{On}$$
10		bdayelon	$$⊢\mathrm{bday}\left(F\right)\in \mathrm{On}$$
11		naddcl	Could not format ( ( ( bday ` D ) e. On /\ ( bday ` F ) e. On ) -> ( ( bday ` D ) +no ( bday ` F ) ) e. On ) : No typesetting found for |- ( ( ( bday ` D ) e. On /\ ( bday ` F ) e. On ) -> ( ( bday ` D ) +no ( bday ` F ) ) e. On ) with typecode |-
12	9 10 11	mp2an	Could not format ( ( bday ` D ) +no ( bday ` F ) ) e. On : No typesetting found for |- ( ( bday ` D ) +no ( bday ` F ) ) e. On with typecode |-
13	8 12	onun2i	Could not format ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) e. On : No typesetting found for |- ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) e. On with typecode |-
14		naddcl	Could not format ( ( ( bday ` C ) e. On /\ ( bday ` F ) e. On ) -> ( ( bday ` C ) +no ( bday ` F ) ) e. On ) : No typesetting found for |- ( ( ( bday ` C ) e. On /\ ( bday ` F ) e. On ) -> ( ( bday ` C ) +no ( bday ` F ) ) e. On ) with typecode |-
15	5 10 14	mp2an	Could not format ( ( bday ` C ) +no ( bday ` F ) ) e. On : No typesetting found for |- ( ( bday ` C ) +no ( bday ` F ) ) e. On with typecode |-
16		naddcl	Could not format ( ( ( bday ` D ) e. On /\ ( bday ` E ) e. On ) -> ( ( bday ` D ) +no ( bday ` E ) ) e. On ) : No typesetting found for |- ( ( ( bday ` D ) e. On /\ ( bday ` E ) e. On ) -> ( ( bday ` D ) +no ( bday ` E ) ) e. On ) with typecode |-
17	9 6 16	mp2an	Could not format ( ( bday ` D ) +no ( bday ` E ) ) e. On : No typesetting found for |- ( ( bday ` D ) +no ( bday ` E ) ) e. On with typecode |-
18	15 17	onun2i	Could not format ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) e. On : No typesetting found for |- ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) e. On with typecode |-
19	13 18	onun2i	Could not format ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) e. On : No typesetting found for |- ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) e. On with typecode |-
20	4 19	onun2i	Could not format ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) e. On : No typesetting found for |- ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) e. On with typecode |-
21		risset	Could not format ( ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) e. On <-> E. x e. On x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) e. On <-> E. x e. On x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) ) with typecode |-
22	20 21	mpbi	Could not format E. x e. On x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) : No typesetting found for |- E. x e. On x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) with typecode |-
23		fveq2	$$⊢a=g\to \mathrm{bday}\left(a\right)=\mathrm{bday}\left(g\right)$$
24	23	oveq1d	Could not format ( a = g -> ( ( bday ` a ) +no ( bday ` b ) ) = ( ( bday ` g ) +no ( bday ` b ) ) ) : No typesetting found for |- ( a = g -> ( ( bday ` a ) +no ( bday ` b ) ) = ( ( bday ` g ) +no ( bday ` b ) ) ) with typecode |-
25	24	uneq1d	Could not format ( a = g -> ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) = ( ( ( bday ` g ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) ) : No typesetting found for |- ( a = g -> ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) = ( ( ( bday ` g ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) ) with typecode |-
26	25	eqeq2d	Could not format ( a = g -> ( x = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) <-> x = ( ( ( bday ` g ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) ) ) : No typesetting found for |- ( a = g -> ( x = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) <-> x = ( ( ( bday ` g ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) ) ) with typecode |-
27		oveq1	Could not format ( a = g -> ( a x.s b ) = ( g x.s b ) ) : No typesetting found for |- ( a = g -> ( a x.s b ) = ( g x.s b ) ) with typecode |-
28	27	eleq1d	Could not format ( a = g -> ( ( a x.s b ) e. No <-> ( g x.s b ) e. No ) ) : No typesetting found for |- ( a = g -> ( ( a x.s b ) e. No <-> ( g x.s b ) e. No ) ) with typecode |-
29	28	anbi1d	Could not format ( a = g -> ( ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( g x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( g x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
30	26 29	imbi12d	Could not format ( a = g -> ( ( x = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( x = ( ( ( bday ` g ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( g x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( x = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( x = ( ( ( bday ` g ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( g x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
31		fveq2	$$⊢b=h\to \mathrm{bday}\left(b\right)=\mathrm{bday}\left(h\right)$$
32	31	oveq2d	Could not format ( b = h -> ( ( bday ` g ) +no ( bday ` b ) ) = ( ( bday ` g ) +no ( bday ` h ) ) ) : No typesetting found for |- ( b = h -> ( ( bday ` g ) +no ( bday ` b ) ) = ( ( bday ` g ) +no ( bday ` h ) ) ) with typecode |-
33	32	uneq1d	Could not format ( b = h -> ( ( ( bday ` g ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) ) : No typesetting found for |- ( b = h -> ( ( ( bday ` g ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) ) with typecode |-
34	33	eqeq2d	Could not format ( b = h -> ( x = ( ( ( bday ` g ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) <-> x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) ) ) : No typesetting found for |- ( b = h -> ( x = ( ( ( bday ` g ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) <-> x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) ) ) with typecode |-
35		oveq2	Could not format ( b = h -> ( g x.s b ) = ( g x.s h ) ) : No typesetting found for |- ( b = h -> ( g x.s b ) = ( g x.s h ) ) with typecode |-
36	35	eleq1d	Could not format ( b = h -> ( ( g x.s b ) e. No <-> ( g x.s h ) e. No ) ) : No typesetting found for |- ( b = h -> ( ( g x.s b ) e. No <-> ( g x.s h ) e. No ) ) with typecode |-
37	36	anbi1d	Could not format ( b = h -> ( ( ( g x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( g x.s h ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( ( g x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( g x.s h ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
38	34 37	imbi12d	Could not format ( b = h -> ( ( x = ( ( ( bday ` g ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( g x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( x = ( ( ( bday ` g ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( g x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
39		fveq2	$$⊢c=i\to \mathrm{bday}\left(c\right)=\mathrm{bday}\left(i\right)$$
40	39	oveq1d	Could not format ( c = i -> ( ( bday ` c ) +no ( bday ` e ) ) = ( ( bday ` i ) +no ( bday ` e ) ) ) : No typesetting found for |- ( c = i -> ( ( bday ` c ) +no ( bday ` e ) ) = ( ( bday ` i ) +no ( bday ` e ) ) ) with typecode |-
41	40	uneq1d	Could not format ( c = i -> ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) = ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) ) : No typesetting found for |- ( c = i -> ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) = ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) ) with typecode |-
42	39	oveq1d	Could not format ( c = i -> ( ( bday ` c ) +no ( bday ` f ) ) = ( ( bday ` i ) +no ( bday ` f ) ) ) : No typesetting found for |- ( c = i -> ( ( bday ` c ) +no ( bday ` f ) ) = ( ( bday ` i ) +no ( bday ` f ) ) ) with typecode |-
43	42	uneq1d	Could not format ( c = i -> ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) = ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) : No typesetting found for |- ( c = i -> ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) = ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) with typecode |-
44	41 43	uneq12d	Could not format ( c = i -> ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) = ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) : No typesetting found for |- ( c = i -> ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) = ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) with typecode |-
45	44	uneq2d	Could not format ( c = i -> ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) ) : No typesetting found for |- ( c = i -> ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) ) with typecode |-
46	45	eqeq2d	Could not format ( c = i -> ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) <-> x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) ) ) : No typesetting found for |- ( c = i -> ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) <-> x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) ) ) with typecode |-
47		breq1	$$⊢c=i\to \left(c{<}_{s}d\leftrightarrow i{<}_{s}d\right)$$
48	47	anbi1d	$$⊢c=i\to \left(\left(c{<}_{s}d\wedge e{<}_{s}f\right)\leftrightarrow \left(i{<}_{s}d\wedge e{<}_{s}f\right)\right)$$
49		oveq1	Could not format ( c = i -> ( c x.s f ) = ( i x.s f ) ) : No typesetting found for |- ( c = i -> ( c x.s f ) = ( i x.s f ) ) with typecode |-
50		oveq1	Could not format ( c = i -> ( c x.s e ) = ( i x.s e ) ) : No typesetting found for |- ( c = i -> ( c x.s e ) = ( i x.s e ) ) with typecode |-
51	49 50	oveq12d	Could not format ( c = i -> ( ( c x.s f ) -s ( c x.s e ) ) = ( ( i x.s f ) -s ( i x.s e ) ) ) : No typesetting found for |- ( c = i -> ( ( c x.s f ) -s ( c x.s e ) ) = ( ( i x.s f ) -s ( i x.s e ) ) ) with typecode |-
52	51	breq1d	Could not format ( c = i -> ( ( ( c x.s f ) -s ( c x.s e ) ) ( ( i x.s f ) -s ( i x.s e ) ) ( ( ( c x.s f ) -s ( c x.s e ) ) ( ( i x.s f ) -s ( i x.s e ) )
53	48 52	imbi12d	Could not format ( c = i -> ( ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( i ( ( i x.s f ) -s ( i x.s e ) ) ( ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( i ( ( i x.s f ) -s ( i x.s e ) )
54	53	anbi2d	Could not format ( c = i -> ( ( ( g x.s h ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s e ) ) ( ( ( g x.s h ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s e ) )
55	46 54	imbi12d	Could not format ( c = i -> ( ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s e ) ) ( ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s e ) )
56		fveq2	$$⊢d=j\to \mathrm{bday}\left(d\right)=\mathrm{bday}\left(j\right)$$
57	56	oveq1d	Could not format ( d = j -> ( ( bday ` d ) +no ( bday ` f ) ) = ( ( bday ` j ) +no ( bday ` f ) ) ) : No typesetting found for |- ( d = j -> ( ( bday ` d ) +no ( bday ` f ) ) = ( ( bday ` j ) +no ( bday ` f ) ) ) with typecode |-
58	57	uneq2d	Could not format ( d = j -> ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) = ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) ) : No typesetting found for |- ( d = j -> ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) = ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) ) with typecode |-
59	56	oveq1d	Could not format ( d = j -> ( ( bday ` d ) +no ( bday ` e ) ) = ( ( bday ` j ) +no ( bday ` e ) ) ) : No typesetting found for |- ( d = j -> ( ( bday ` d ) +no ( bday ` e ) ) = ( ( bday ` j ) +no ( bday ` e ) ) ) with typecode |-
60	59	uneq2d	Could not format ( d = j -> ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) = ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` e ) ) ) ) : No typesetting found for |- ( d = j -> ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) = ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` e ) ) ) ) with typecode |-
61	58 60	uneq12d	Could not format ( d = j -> ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) = ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` e ) ) ) ) ) : No typesetting found for |- ( d = j -> ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) = ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` e ) ) ) ) ) with typecode |-
62	61	uneq2d	Could not format ( d = j -> ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` e ) ) ) ) ) ) : No typesetting found for |- ( d = j -> ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` e ) ) ) ) ) ) with typecode |-
63	62	eqeq2d	Could not format ( d = j -> ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) <-> x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` e ) ) ) ) ) ) ) : No typesetting found for |- ( d = j -> ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) <-> x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` e ) ) ) ) ) ) ) with typecode |-
64		breq2	$$⊢d=j\to \left(i{<}_{s}d\leftrightarrow i{<}_{s}j\right)$$
65	64	anbi1d	$$⊢d=j\to \left(\left(i{<}_{s}d\wedge e{<}_{s}f\right)\leftrightarrow \left(i{<}_{s}j\wedge e{<}_{s}f\right)\right)$$
66		oveq1	Could not format ( d = j -> ( d x.s f ) = ( j x.s f ) ) : No typesetting found for |- ( d = j -> ( d x.s f ) = ( j x.s f ) ) with typecode |-
67		oveq1	Could not format ( d = j -> ( d x.s e ) = ( j x.s e ) ) : No typesetting found for |- ( d = j -> ( d x.s e ) = ( j x.s e ) ) with typecode |-
68	66 67	oveq12d	Could not format ( d = j -> ( ( d x.s f ) -s ( d x.s e ) ) = ( ( j x.s f ) -s ( j x.s e ) ) ) : No typesetting found for |- ( d = j -> ( ( d x.s f ) -s ( d x.s e ) ) = ( ( j x.s f ) -s ( j x.s e ) ) ) with typecode |-
69	68	breq2d	Could not format ( d = j -> ( ( ( i x.s f ) -s ( i x.s e ) ) ( ( i x.s f ) -s ( i x.s e ) ) ( ( ( i x.s f ) -s ( i x.s e ) ) ( ( i x.s f ) -s ( i x.s e ) )
70	65 69	imbi12d	Could not format ( d = j -> ( ( ( i ( ( i x.s f ) -s ( i x.s e ) ) ( ( i ( ( i x.s f ) -s ( i x.s e ) ) ( ( ( i ( ( i x.s f ) -s ( i x.s e ) ) ( ( i ( ( i x.s f ) -s ( i x.s e ) )
71	70	anbi2d	Could not format ( d = j -> ( ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s e ) ) ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s e ) ) ( ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s e ) ) ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s e ) )
72	63 71	imbi12d	Could not format ( d = j -> ( ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s e ) ) ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` e ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s e ) ) ( ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s e ) ) ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` e ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s e ) )
73		fveq2	$$⊢e=k\to \mathrm{bday}\left(e\right)=\mathrm{bday}\left(k\right)$$
74	73	oveq2d	Could not format ( e = k -> ( ( bday ` i ) +no ( bday ` e ) ) = ( ( bday ` i ) +no ( bday ` k ) ) ) : No typesetting found for |- ( e = k -> ( ( bday ` i ) +no ( bday ` e ) ) = ( ( bday ` i ) +no ( bday ` k ) ) ) with typecode |-
75	74	uneq1d	Could not format ( e = k -> ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) = ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) ) : No typesetting found for |- ( e = k -> ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) = ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) ) with typecode |-
76	73	oveq2d	Could not format ( e = k -> ( ( bday ` j ) +no ( bday ` e ) ) = ( ( bday ` j ) +no ( bday ` k ) ) ) : No typesetting found for |- ( e = k -> ( ( bday ` j ) +no ( bday ` e ) ) = ( ( bday ` j ) +no ( bday ` k ) ) ) with typecode |-
77	76	uneq2d	Could not format ( e = k -> ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` e ) ) ) = ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) : No typesetting found for |- ( e = k -> ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` e ) ) ) = ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) with typecode |-
78	75 77	uneq12d	Could not format ( e = k -> ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` e ) ) ) ) = ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) : No typesetting found for |- ( e = k -> ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` e ) ) ) ) = ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) with typecode |-
79	78	uneq2d	Could not format ( e = k -> ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` e ) ) ) ) ) = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ) : No typesetting found for |- ( e = k -> ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` e ) ) ) ) ) = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ) with typecode |-
80	79	eqeq2d	Could not format ( e = k -> ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` e ) ) ) ) ) <-> x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ) ) : No typesetting found for |- ( e = k -> ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` e ) ) ) ) ) <-> x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ) ) with typecode |-
81		breq1	$$⊢e=k\to \left(e{<}_{s}f\leftrightarrow k{<}_{s}f\right)$$
82	81	anbi2d	$$⊢e=k\to \left(\left(i{<}_{s}j\wedge e{<}_{s}f\right)\leftrightarrow \left(i{<}_{s}j\wedge k{<}_{s}f\right)\right)$$
83		oveq2	Could not format ( e = k -> ( i x.s e ) = ( i x.s k ) ) : No typesetting found for |- ( e = k -> ( i x.s e ) = ( i x.s k ) ) with typecode |-
84	83	oveq2d	Could not format ( e = k -> ( ( i x.s f ) -s ( i x.s e ) ) = ( ( i x.s f ) -s ( i x.s k ) ) ) : No typesetting found for |- ( e = k -> ( ( i x.s f ) -s ( i x.s e ) ) = ( ( i x.s f ) -s ( i x.s k ) ) ) with typecode |-
85		oveq2	Could not format ( e = k -> ( j x.s e ) = ( j x.s k ) ) : No typesetting found for |- ( e = k -> ( j x.s e ) = ( j x.s k ) ) with typecode |-
86	85	oveq2d	Could not format ( e = k -> ( ( j x.s f ) -s ( j x.s e ) ) = ( ( j x.s f ) -s ( j x.s k ) ) ) : No typesetting found for |- ( e = k -> ( ( j x.s f ) -s ( j x.s e ) ) = ( ( j x.s f ) -s ( j x.s k ) ) ) with typecode |-
87	84 86	breq12d	Could not format ( e = k -> ( ( ( i x.s f ) -s ( i x.s e ) ) ( ( i x.s f ) -s ( i x.s k ) ) ( ( ( i x.s f ) -s ( i x.s e ) ) ( ( i x.s f ) -s ( i x.s k ) )
88	82 87	imbi12d	Could not format ( e = k -> ( ( ( i ( ( i x.s f ) -s ( i x.s e ) ) ( ( i ( ( i x.s f ) -s ( i x.s k ) ) ( ( ( i ( ( i x.s f ) -s ( i x.s e ) ) ( ( i ( ( i x.s f ) -s ( i x.s k ) )
89	88	anbi2d	Could not format ( e = k -> ( ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s e ) ) ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s k ) ) ( ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s e ) ) ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s k ) )
90	80 89	imbi12d	Could not format ( e = k -> ( ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` e ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s e ) ) ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s k ) ) ( ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` e ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` e ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s e ) ) ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s k ) )
91		fveq2	$$⊢f=l\to \mathrm{bday}\left(f\right)=\mathrm{bday}\left(l\right)$$
92	91	oveq2d	Could not format ( f = l -> ( ( bday ` j ) +no ( bday ` f ) ) = ( ( bday ` j ) +no ( bday ` l ) ) ) : No typesetting found for |- ( f = l -> ( ( bday ` j ) +no ( bday ` f ) ) = ( ( bday ` j ) +no ( bday ` l ) ) ) with typecode |-
93	92	uneq2d	Could not format ( f = l -> ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) = ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) ) : No typesetting found for |- ( f = l -> ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) = ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) ) with typecode |-
94	91	oveq2d	Could not format ( f = l -> ( ( bday ` i ) +no ( bday ` f ) ) = ( ( bday ` i ) +no ( bday ` l ) ) ) : No typesetting found for |- ( f = l -> ( ( bday ` i ) +no ( bday ` f ) ) = ( ( bday ` i ) +no ( bday ` l ) ) ) with typecode |-
95	94	uneq1d	Could not format ( f = l -> ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) = ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) : No typesetting found for |- ( f = l -> ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) = ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) with typecode |-
96	93 95	uneq12d	Could not format ( f = l -> ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) = ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) : No typesetting found for |- ( f = l -> ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) = ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) with typecode |-
97	96	uneq2d	Could not format ( f = l -> ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ) : No typesetting found for |- ( f = l -> ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ) with typecode |-
98	97	eqeq2d	Could not format ( f = l -> ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) <-> x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ) ) : No typesetting found for |- ( f = l -> ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) <-> x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ) ) with typecode |-
99		breq2	$$⊢f=l\to \left(k{<}_{s}f\leftrightarrow k{<}_{s}l\right)$$
100	99	anbi2d	$$⊢f=l\to \left(\left(i{<}_{s}j\wedge k{<}_{s}f\right)\leftrightarrow \left(i{<}_{s}j\wedge k{<}_{s}l\right)\right)$$
101		oveq2	Could not format ( f = l -> ( i x.s f ) = ( i x.s l ) ) : No typesetting found for |- ( f = l -> ( i x.s f ) = ( i x.s l ) ) with typecode |-
102	101	oveq1d	Could not format ( f = l -> ( ( i x.s f ) -s ( i x.s k ) ) = ( ( i x.s l ) -s ( i x.s k ) ) ) : No typesetting found for |- ( f = l -> ( ( i x.s f ) -s ( i x.s k ) ) = ( ( i x.s l ) -s ( i x.s k ) ) ) with typecode |-
103		oveq2	Could not format ( f = l -> ( j x.s f ) = ( j x.s l ) ) : No typesetting found for |- ( f = l -> ( j x.s f ) = ( j x.s l ) ) with typecode |-
104	103	oveq1d	Could not format ( f = l -> ( ( j x.s f ) -s ( j x.s k ) ) = ( ( j x.s l ) -s ( j x.s k ) ) ) : No typesetting found for |- ( f = l -> ( ( j x.s f ) -s ( j x.s k ) ) = ( ( j x.s l ) -s ( j x.s k ) ) ) with typecode |-
105	102 104	breq12d	Could not format ( f = l -> ( ( ( i x.s f ) -s ( i x.s k ) ) ( ( i x.s l ) -s ( i x.s k ) ) ( ( ( i x.s f ) -s ( i x.s k ) ) ( ( i x.s l ) -s ( i x.s k ) )
106	100 105	imbi12d	Could not format ( f = l -> ( ( ( i ( ( i x.s f ) -s ( i x.s k ) ) ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( ( ( i ( ( i x.s f ) -s ( i x.s k ) ) ( ( i ( ( i x.s l ) -s ( i x.s k ) )
107	106	anbi2d	Could not format ( f = l -> ( ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s k ) ) ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s k ) ) ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
108	98 107	imbi12d	Could not format ( f = l -> ( ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s k ) ) ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` f ) ) ) u. ( ( ( bday ` i ) +no ( bday ` f ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s k ) ) ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
109	30 38 55 72 90 108	cbvral6vw	Could not format ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( x = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
110		eqeq1	Could not format ( x = y -> ( x = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) <-> y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) ) ) : No typesetting found for |- ( x = y -> ( x = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) <-> y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) ) ) with typecode |-
111	110	imbi1d	Could not format ( x = y -> ( ( x = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( x = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
112	111	6ralbidv	Could not format ( x = y -> ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( x = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( x = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
113	109 112	bitr3id	Could not format ( x = y -> ( A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
114		raleq	Could not format ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( A. y e. x A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( A. y e. x A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
115		ralrot3	Could not format ( A. a e. No A. b e. No A. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
116		ralrot3	Could not format ( A. c e. No A. d e. No A. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
117		ralrot3	Could not format ( A. e e. No A. f e. No A. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
118		r19.23v	Could not format ( A. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( E. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( E. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
119		risset	Could not format ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) <-> E. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) <-> E. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) ) with typecode |-
120	119	imbi1i	Could not format ( ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( E. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( E. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
121	118 120	bitr4i	Could not format ( A. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
122	121	2ralbii	Could not format ( A. e e. No A. f e. No A. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
123	117 122	bitr3i	Could not format ( A. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
124	123	2ralbii	Could not format ( A. c e. No A. d e. No A. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
125	116 124	bitr3i	Could not format ( A. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
126	125	2ralbii	Could not format ( A. a e. No A. b e. No A. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
127	115 126	bitr3i	Could not format ( A. y e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
128	114 127	bitrdi	Could not format ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( A. y e. x A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( A. y e. x A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
129		simpl	Could not format ( ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
130		simprl1	Could not format ( ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) g e. No ) : No typesetting found for |- ( ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) g e. No ) with typecode |-
131		simprl2	Could not format ( ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) h e. No ) : No typesetting found for |- ( ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) h e. No ) with typecode |-
132	129 130 131	mulsproplem11	Could not format ( ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( g x.s h ) e. No ) : No typesetting found for |- ( ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( g x.s h ) e. No ) with typecode |-
133	129	adantr	Could not format ( ( ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
134		simprl3	Could not format ( ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) i e. No ) : No typesetting found for |- ( ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) i e. No ) with typecode |-
135	134	adantr	Could not format ( ( ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) i e. No ) : No typesetting found for |- ( ( ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) i e. No ) with typecode |-
136		simprr1	Could not format ( ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) j e. No ) : No typesetting found for |- ( ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) j e. No ) with typecode |-
137	136	adantr	Could not format ( ( ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) j e. No ) : No typesetting found for |- ( ( ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) j e. No ) with typecode |-
138		simprr2	Could not format ( ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) k e. No ) : No typesetting found for |- ( ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) k e. No ) with typecode |-
139	138	adantr	Could not format ( ( ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) k e. No ) : No typesetting found for |- ( ( ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) k e. No ) with typecode |-
140		simprr3	Could not format ( ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) l e. No ) : No typesetting found for |- ( ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) l e. No ) with typecode |-
141	140	adantr	Could not format ( ( ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) l e. No ) : No typesetting found for |- ( ( ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) l e. No ) with typecode |-
142		simprl	Could not format ( ( ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) i ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) i
143		simprr	Could not format ( ( ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) k ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) k
144	133 135 137 139 141 142 143	mulsproplem14	Could not format ( ( ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( i x.s l ) -s ( i x.s k ) ) ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( i x.s l ) -s ( i x.s k ) )
145	144	ex	Could not format ( ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( i ( ( i x.s l ) -s ( i x.s k ) )
146	132 145	jca	Could not format ( ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
147	146	ex	Could not format ( A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( ( g e. No /\ h e. No /\ i e. No ) /\ ( j e. No /\ k e. No /\ l e. No ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( ( g e. No /\ h e. No /\ i e. No ) /\ ( j e. No /\ k e. No /\ l e. No ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
148	128 147	biimtrdi	Could not format ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( A. y e. x A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( ( g e. No /\ h e. No /\ i e. No ) /\ ( j e. No /\ k e. No /\ l e. No ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( A. y e. x A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( ( g e. No /\ h e. No /\ i e. No ) /\ ( j e. No /\ k e. No /\ l e. No ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
149	148	impd	Could not format ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( A. y e. x A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( ( A. y e. x A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
150	149	com12	Could not format ( ( A. y e. x A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
151	150	anassrs	Could not format ( ( ( A. y e. x A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
152	151	ralrimivvva	Could not format ( ( A. y e. x A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. j e. No A. k e. No A. l e. No ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. j e. No A. k e. No A. l e. No ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
153	152	ralrimivvva	Could not format ( A. y e. x A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
154	153	a1i	Could not format ( x e. On -> ( A. y e. x A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( A. y e. x A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( y = ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
155	113 154	tfis2	Could not format ( x e. On -> A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
156		fveq2	$$⊢g=A\to \mathrm{bday}\left(g\right)=\mathrm{bday}\left(A\right)$$
157	156	oveq1d	Could not format ( g = A -> ( ( bday ` g ) +no ( bday ` h ) ) = ( ( bday ` A ) +no ( bday ` h ) ) ) : No typesetting found for |- ( g = A -> ( ( bday ` g ) +no ( bday ` h ) ) = ( ( bday ` A ) +no ( bday ` h ) ) ) with typecode |-
158	157	uneq1d	Could not format ( g = A -> ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) = ( ( ( bday ` A ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ) : No typesetting found for |- ( g = A -> ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) = ( ( ( bday ` A ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ) with typecode |-
159	158	eqeq2d	Could not format ( g = A -> ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) <-> x = ( ( ( bday ` A ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ) ) : No typesetting found for |- ( g = A -> ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) <-> x = ( ( ( bday ` A ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ) ) with typecode |-
160		oveq1	Could not format ( g = A -> ( g x.s h ) = ( A x.s h ) ) : No typesetting found for |- ( g = A -> ( g x.s h ) = ( A x.s h ) ) with typecode |-
161	160	eleq1d	Could not format ( g = A -> ( ( g x.s h ) e. No <-> ( A x.s h ) e. No ) ) : No typesetting found for |- ( g = A -> ( ( g x.s h ) e. No <-> ( A x.s h ) e. No ) ) with typecode |-
162	161	anbi1d	Could not format ( g = A -> ( ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( ( A x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( ( A x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
163	159 162	imbi12d	Could not format ( g = A -> ( ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( x = ( ( ( bday ` A ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( A x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( x = ( ( ( bday ` A ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( A x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
164		fveq2	$$⊢h=B\to \mathrm{bday}\left(h\right)=\mathrm{bday}\left(B\right)$$
165	164	oveq2d	Could not format ( h = B -> ( ( bday ` A ) +no ( bday ` h ) ) = ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( h = B -> ( ( bday ` A ) +no ( bday ` h ) ) = ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
166	165	uneq1d	Could not format ( h = B -> ( ( ( bday ` A ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ) : No typesetting found for |- ( h = B -> ( ( ( bday ` A ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ) with typecode |-
167	166	eqeq2d	Could not format ( h = B -> ( x = ( ( ( bday ` A ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) <-> x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ) ) : No typesetting found for |- ( h = B -> ( x = ( ( ( bday ` A ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) <-> x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ) ) with typecode |-
168		oveq2	Could not format ( h = B -> ( A x.s h ) = ( A x.s B ) ) : No typesetting found for |- ( h = B -> ( A x.s h ) = ( A x.s B ) ) with typecode |-
169	168	eleq1d	Could not format ( h = B -> ( ( A x.s h ) e. No <-> ( A x.s B ) e. No ) ) : No typesetting found for |- ( h = B -> ( ( A x.s h ) e. No <-> ( A x.s B ) e. No ) ) with typecode |-
170	169	anbi1d	Could not format ( h = B -> ( ( ( A x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( ( A x.s B ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( ( ( A x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( ( A x.s B ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
171	167 170	imbi12d	Could not format ( h = B -> ( ( x = ( ( ( bday ` A ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( A x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( A x.s B ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( ( x = ( ( ( bday ` A ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( A x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( A x.s B ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
172		fveq2	$$⊢i=C\to \mathrm{bday}\left(i\right)=\mathrm{bday}\left(C\right)$$
173	172	oveq1d	Could not format ( i = C -> ( ( bday ` i ) +no ( bday ` k ) ) = ( ( bday ` C ) +no ( bday ` k ) ) ) : No typesetting found for |- ( i = C -> ( ( bday ` i ) +no ( bday ` k ) ) = ( ( bday ` C ) +no ( bday ` k ) ) ) with typecode |-
174	173	uneq1d	Could not format ( i = C -> ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) = ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) ) : No typesetting found for |- ( i = C -> ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) = ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) ) with typecode |-
175	172	oveq1d	Could not format ( i = C -> ( ( bday ` i ) +no ( bday ` l ) ) = ( ( bday ` C ) +no ( bday ` l ) ) ) : No typesetting found for |- ( i = C -> ( ( bday ` i ) +no ( bday ` l ) ) = ( ( bday ` C ) +no ( bday ` l ) ) ) with typecode |-
176	175	uneq1d	Could not format ( i = C -> ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) = ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) : No typesetting found for |- ( i = C -> ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) = ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) with typecode |-
177	174 176	uneq12d	Could not format ( i = C -> ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) = ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) : No typesetting found for |- ( i = C -> ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) = ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) with typecode |-
178	177	uneq2d	Could not format ( i = C -> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ) : No typesetting found for |- ( i = C -> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ) with typecode |-
179	178	eqeq2d	Could not format ( i = C -> ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) <-> x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ) ) : No typesetting found for |- ( i = C -> ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) <-> x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) ) ) with typecode |-
180		breq1	$$⊢i=C\to \left(i{<}_{s}j\leftrightarrow C{<}_{s}j\right)$$
181	180	anbi1d	$$⊢i=C\to \left(\left(i{<}_{s}j\wedge k{<}_{s}l\right)\leftrightarrow \left(C{<}_{s}j\wedge k{<}_{s}l\right)\right)$$
182		oveq1	Could not format ( i = C -> ( i x.s l ) = ( C x.s l ) ) : No typesetting found for |- ( i = C -> ( i x.s l ) = ( C x.s l ) ) with typecode |-
183		oveq1	Could not format ( i = C -> ( i x.s k ) = ( C x.s k ) ) : No typesetting found for |- ( i = C -> ( i x.s k ) = ( C x.s k ) ) with typecode |-
184	182 183	oveq12d	Could not format ( i = C -> ( ( i x.s l ) -s ( i x.s k ) ) = ( ( C x.s l ) -s ( C x.s k ) ) ) : No typesetting found for |- ( i = C -> ( ( i x.s l ) -s ( i x.s k ) ) = ( ( C x.s l ) -s ( C x.s k ) ) ) with typecode |-
185	184	breq1d	Could not format ( i = C -> ( ( ( i x.s l ) -s ( i x.s k ) ) ( ( C x.s l ) -s ( C x.s k ) ) ( ( ( i x.s l ) -s ( i x.s k ) ) ( ( C x.s l ) -s ( C x.s k ) )
186	181 185	imbi12d	Could not format ( i = C -> ( ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( ( C ( ( C x.s l ) -s ( C x.s k ) ) ( ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( ( C ( ( C x.s l ) -s ( C x.s k ) )
187	186	anbi2d	Could not format ( i = C -> ( ( ( A x.s B ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s l ) -s ( C x.s k ) ) ( ( ( A x.s B ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s l ) -s ( C x.s k ) )
188	179 187	imbi12d	Could not format ( i = C -> ( ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( A x.s B ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s l ) -s ( C x.s k ) ) ( ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( A x.s B ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s l ) -s ( C x.s k ) )
189		fveq2	$$⊢j=D\to \mathrm{bday}\left(j\right)=\mathrm{bday}\left(D\right)$$
190	189	oveq1d	Could not format ( j = D -> ( ( bday ` j ) +no ( bday ` l ) ) = ( ( bday ` D ) +no ( bday ` l ) ) ) : No typesetting found for |- ( j = D -> ( ( bday ` j ) +no ( bday ` l ) ) = ( ( bday ` D ) +no ( bday ` l ) ) ) with typecode |-
191	190	uneq2d	Could not format ( j = D -> ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) = ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) ) : No typesetting found for |- ( j = D -> ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) = ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) ) with typecode |-
192	189	oveq1d	Could not format ( j = D -> ( ( bday ` j ) +no ( bday ` k ) ) = ( ( bday ` D ) +no ( bday ` k ) ) ) : No typesetting found for |- ( j = D -> ( ( bday ` j ) +no ( bday ` k ) ) = ( ( bday ` D ) +no ( bday ` k ) ) ) with typecode |-
193	192	uneq2d	Could not format ( j = D -> ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) = ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` k ) ) ) ) : No typesetting found for |- ( j = D -> ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) = ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` k ) ) ) ) with typecode |-
194	191 193	uneq12d	Could not format ( j = D -> ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) = ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` k ) ) ) ) ) : No typesetting found for |- ( j = D -> ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) = ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` k ) ) ) ) ) with typecode |-
195	194	uneq2d	Could not format ( j = D -> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` k ) ) ) ) ) ) : No typesetting found for |- ( j = D -> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` k ) ) ) ) ) ) with typecode |-
196	195	eqeq2d	Could not format ( j = D -> ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) <-> x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` k ) ) ) ) ) ) ) : No typesetting found for |- ( j = D -> ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) <-> x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` k ) ) ) ) ) ) ) with typecode |-
197		breq2	$$⊢j=D\to \left(C{<}_{s}j\leftrightarrow C{<}_{s}D\right)$$
198	197	anbi1d	$$⊢j=D\to \left(\left(C{<}_{s}j\wedge k{<}_{s}l\right)\leftrightarrow \left(C{<}_{s}D\wedge k{<}_{s}l\right)\right)$$
199		oveq1	Could not format ( j = D -> ( j x.s l ) = ( D x.s l ) ) : No typesetting found for |- ( j = D -> ( j x.s l ) = ( D x.s l ) ) with typecode |-
200		oveq1	Could not format ( j = D -> ( j x.s k ) = ( D x.s k ) ) : No typesetting found for |- ( j = D -> ( j x.s k ) = ( D x.s k ) ) with typecode |-
201	199 200	oveq12d	Could not format ( j = D -> ( ( j x.s l ) -s ( j x.s k ) ) = ( ( D x.s l ) -s ( D x.s k ) ) ) : No typesetting found for |- ( j = D -> ( ( j x.s l ) -s ( j x.s k ) ) = ( ( D x.s l ) -s ( D x.s k ) ) ) with typecode |-
202	201	breq2d	Could not format ( j = D -> ( ( ( C x.s l ) -s ( C x.s k ) ) ( ( C x.s l ) -s ( C x.s k ) ) ( ( ( C x.s l ) -s ( C x.s k ) ) ( ( C x.s l ) -s ( C x.s k ) )
203	198 202	imbi12d	Could not format ( j = D -> ( ( ( C ( ( C x.s l ) -s ( C x.s k ) ) ( ( C ( ( C x.s l ) -s ( C x.s k ) ) ( ( ( C ( ( C x.s l ) -s ( C x.s k ) ) ( ( C ( ( C x.s l ) -s ( C x.s k ) )
204	203	anbi2d	Could not format ( j = D -> ( ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s l ) -s ( C x.s k ) ) ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s l ) -s ( C x.s k ) ) ( ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s l ) -s ( C x.s k ) ) ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s l ) -s ( C x.s k ) )
205	196 204	imbi12d	Could not format ( j = D -> ( ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s l ) -s ( C x.s k ) ) ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` k ) ) ) ) ) -> ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s l ) -s ( C x.s k ) ) ( ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s l ) -s ( C x.s k ) ) ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` k ) ) ) ) ) -> ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s l ) -s ( C x.s k ) )
206		fveq2	$$⊢k=E\to \mathrm{bday}\left(k\right)=\mathrm{bday}\left(E\right)$$
207	206	oveq2d	Could not format ( k = E -> ( ( bday ` C ) +no ( bday ` k ) ) = ( ( bday ` C ) +no ( bday ` E ) ) ) : No typesetting found for |- ( k = E -> ( ( bday ` C ) +no ( bday ` k ) ) = ( ( bday ` C ) +no ( bday ` E ) ) ) with typecode |-
208	207	uneq1d	Could not format ( k = E -> ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) = ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) ) : No typesetting found for |- ( k = E -> ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) = ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) ) with typecode |-
209	206	oveq2d	Could not format ( k = E -> ( ( bday ` D ) +no ( bday ` k ) ) = ( ( bday ` D ) +no ( bday ` E ) ) ) : No typesetting found for |- ( k = E -> ( ( bday ` D ) +no ( bday ` k ) ) = ( ( bday ` D ) +no ( bday ` E ) ) ) with typecode |-
210	209	uneq2d	Could not format ( k = E -> ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` k ) ) ) = ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) : No typesetting found for |- ( k = E -> ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` k ) ) ) = ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) with typecode |-
211	208 210	uneq12d	Could not format ( k = E -> ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` k ) ) ) ) = ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) : No typesetting found for |- ( k = E -> ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` k ) ) ) ) = ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) with typecode |-
212	211	uneq2d	Could not format ( k = E -> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` k ) ) ) ) ) = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) ) : No typesetting found for |- ( k = E -> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` k ) ) ) ) ) = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) ) with typecode |-
213	212	eqeq2d	Could not format ( k = E -> ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` k ) ) ) ) ) <-> x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) ) ) : No typesetting found for |- ( k = E -> ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` k ) ) ) ) ) <-> x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) ) ) with typecode |-
214		breq1	$$⊢k=E\to \left(k{<}_{s}l\leftrightarrow E{<}_{s}l\right)$$
215	214	anbi2d	$$⊢k=E\to \left(\left(C{<}_{s}D\wedge k{<}_{s}l\right)\leftrightarrow \left(C{<}_{s}D\wedge E{<}_{s}l\right)\right)$$
216		oveq2	Could not format ( k = E -> ( C x.s k ) = ( C x.s E ) ) : No typesetting found for |- ( k = E -> ( C x.s k ) = ( C x.s E ) ) with typecode |-
217	216	oveq2d	Could not format ( k = E -> ( ( C x.s l ) -s ( C x.s k ) ) = ( ( C x.s l ) -s ( C x.s E ) ) ) : No typesetting found for |- ( k = E -> ( ( C x.s l ) -s ( C x.s k ) ) = ( ( C x.s l ) -s ( C x.s E ) ) ) with typecode |-
218		oveq2	Could not format ( k = E -> ( D x.s k ) = ( D x.s E ) ) : No typesetting found for |- ( k = E -> ( D x.s k ) = ( D x.s E ) ) with typecode |-
219	218	oveq2d	Could not format ( k = E -> ( ( D x.s l ) -s ( D x.s k ) ) = ( ( D x.s l ) -s ( D x.s E ) ) ) : No typesetting found for |- ( k = E -> ( ( D x.s l ) -s ( D x.s k ) ) = ( ( D x.s l ) -s ( D x.s E ) ) ) with typecode |-
220	217 219	breq12d	Could not format ( k = E -> ( ( ( C x.s l ) -s ( C x.s k ) ) ( ( C x.s l ) -s ( C x.s E ) ) ( ( ( C x.s l ) -s ( C x.s k ) ) ( ( C x.s l ) -s ( C x.s E ) )
221	215 220	imbi12d	Could not format ( k = E -> ( ( ( C ( ( C x.s l ) -s ( C x.s k ) ) ( ( C ( ( C x.s l ) -s ( C x.s E ) ) ( ( ( C ( ( C x.s l ) -s ( C x.s k ) ) ( ( C ( ( C x.s l ) -s ( C x.s E ) )
222	221	anbi2d	Could not format ( k = E -> ( ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s l ) -s ( C x.s k ) ) ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s l ) -s ( C x.s E ) ) ( ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s l ) -s ( C x.s k ) ) ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s l ) -s ( C x.s E ) )
223	213 222	imbi12d	Could not format ( k = E -> ( ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` k ) ) ) ) ) -> ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s l ) -s ( C x.s k ) ) ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s l ) -s ( C x.s E ) ) ( ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` k ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` k ) ) ) ) ) -> ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s l ) -s ( C x.s k ) ) ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s l ) -s ( C x.s E ) )
224		fveq2	$$⊢l=F\to \mathrm{bday}\left(l\right)=\mathrm{bday}\left(F\right)$$
225	224	oveq2d	Could not format ( l = F -> ( ( bday ` D ) +no ( bday ` l ) ) = ( ( bday ` D ) +no ( bday ` F ) ) ) : No typesetting found for |- ( l = F -> ( ( bday ` D ) +no ( bday ` l ) ) = ( ( bday ` D ) +no ( bday ` F ) ) ) with typecode |-
226	225	uneq2d	Could not format ( l = F -> ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) = ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) ) : No typesetting found for |- ( l = F -> ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) = ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) ) with typecode |-
227	224	oveq2d	Could not format ( l = F -> ( ( bday ` C ) +no ( bday ` l ) ) = ( ( bday ` C ) +no ( bday ` F ) ) ) : No typesetting found for |- ( l = F -> ( ( bday ` C ) +no ( bday ` l ) ) = ( ( bday ` C ) +no ( bday ` F ) ) ) with typecode |-
228	227	uneq1d	Could not format ( l = F -> ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) = ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) : No typesetting found for |- ( l = F -> ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) = ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) with typecode |-
229	226 228	uneq12d	Could not format ( l = F -> ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) = ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) : No typesetting found for |- ( l = F -> ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) = ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) with typecode |-
230	229	uneq2d	Could not format ( l = F -> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) ) : No typesetting found for |- ( l = F -> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) ) with typecode |-
231	230	eqeq2d	Could not format ( l = F -> ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) <-> x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) ) ) : No typesetting found for |- ( l = F -> ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) <-> x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) ) ) with typecode |-
232		breq2	$$⊢l=F\to \left(E{<}_{s}l\leftrightarrow E{<}_{s}F\right)$$
233	232	anbi2d	$$⊢l=F\to \left(\left(C{<}_{s}D\wedge E{<}_{s}l\right)\leftrightarrow \left(C{<}_{s}D\wedge E{<}_{s}F\right)\right)$$
234		oveq2	Could not format ( l = F -> ( C x.s l ) = ( C x.s F ) ) : No typesetting found for |- ( l = F -> ( C x.s l ) = ( C x.s F ) ) with typecode |-
235	234	oveq1d	Could not format ( l = F -> ( ( C x.s l ) -s ( C x.s E ) ) = ( ( C x.s F ) -s ( C x.s E ) ) ) : No typesetting found for |- ( l = F -> ( ( C x.s l ) -s ( C x.s E ) ) = ( ( C x.s F ) -s ( C x.s E ) ) ) with typecode |-
236		oveq2	Could not format ( l = F -> ( D x.s l ) = ( D x.s F ) ) : No typesetting found for |- ( l = F -> ( D x.s l ) = ( D x.s F ) ) with typecode |-
237	236	oveq1d	Could not format ( l = F -> ( ( D x.s l ) -s ( D x.s E ) ) = ( ( D x.s F ) -s ( D x.s E ) ) ) : No typesetting found for |- ( l = F -> ( ( D x.s l ) -s ( D x.s E ) ) = ( ( D x.s F ) -s ( D x.s E ) ) ) with typecode |-
238	235 237	breq12d	Could not format ( l = F -> ( ( ( C x.s l ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) ) ( ( ( C x.s l ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) )
239	233 238	imbi12d	Could not format ( l = F -> ( ( ( C ( ( C x.s l ) -s ( C x.s E ) ) ( ( C ( ( C x.s F ) -s ( C x.s E ) ) ( ( ( C ( ( C x.s l ) -s ( C x.s E ) ) ( ( C ( ( C x.s F ) -s ( C x.s E ) )
240	239	anbi2d	Could not format ( l = F -> ( ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s l ) -s ( C x.s E ) ) ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s F ) -s ( C x.s E ) ) ( ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s l ) -s ( C x.s E ) ) ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s F ) -s ( C x.s E ) )
241	231 240	imbi12d	Could not format ( l = F -> ( ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s l ) -s ( C x.s E ) ) ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s F ) -s ( C x.s E ) ) ( ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` l ) ) ) u. ( ( ( bday ` C ) +no ( bday ` l ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s l ) -s ( C x.s E ) ) ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s F ) -s ( C x.s E ) )
242	163 171 188 205 223 241	rspc6v	Could not format ( ( ( A e. No /\ B e. No ) /\ ( C e. No /\ D e. No ) /\ ( E e. No /\ F e. No ) ) -> ( A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s F ) -s ( C x.s E ) ) ( A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( x = ( ( ( bday ` g ) +no ( bday ` h ) ) u. ( ( ( ( bday ` i ) +no ( bday ` k ) ) u. ( ( bday ` j ) +no ( bday ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s F ) -s ( C x.s E ) )
243	155 242	syl5com	Could not format ( x e. On -> ( ( ( A e. No /\ B e. No ) /\ ( C e. No /\ D e. No ) /\ ( E e. No /\ F e. No ) ) -> ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s F ) -s ( C x.s E ) ) ( ( ( A e. No /\ B e. No ) /\ ( C e. No /\ D e. No ) /\ ( E e. No /\ F e. No ) ) -> ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s F ) -s ( C x.s E ) )
244	243	com23	Could not format ( x e. On -> ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( ( A e. No /\ B e. No ) /\ ( C e. No /\ D e. No ) /\ ( E e. No /\ F e. No ) ) -> ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s F ) -s ( C x.s E ) ) ( x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( ( A e. No /\ B e. No ) /\ ( C e. No /\ D e. No ) /\ ( E e. No /\ F e. No ) ) -> ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s F ) -s ( C x.s E ) )
245	244	rexlimiv	Could not format ( E. x e. On x = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( ( A e. No /\ B e. No ) /\ ( C e. No /\ D e. No ) /\ ( E e. No /\ F e. No ) ) -> ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s F ) -s ( C x.s E ) ) ( ( ( A e. No /\ B e. No ) /\ ( C e. No /\ D e. No ) /\ ( E e. No /\ F e. No ) ) -> ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s F ) -s ( C x.s E ) )
246	22 245	ax-mp	Could not format ( ( ( A e. No /\ B e. No ) /\ ( C e. No /\ D e. No ) /\ ( E e. No /\ F e. No ) ) -> ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s F ) -s ( C x.s E ) ) ( ( A x.s B ) e. No /\ ( ( C ( ( C x.s F ) -s ( C x.s E ) )