Theorem mulsproplemcbv

Description: Lemma for surreal multiplication. Change some bound variables for later use. (Contributed by Scott Fenton, 5-Mar-2025)

	Ref	Expression
Hypothesis	mulsproplem.1	No typesetting found for |- ( ph -> 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 ` 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 ) )
Assertion	mulsproplemcbv	Could not format assertion : No typesetting found for |- ( ph -> A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( ( ( ( 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. ( ( ( 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )

Proof

Step	Hyp	Ref	Expression
1		mulsproplem.1	Could not format ( ph -> 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 ` 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 ` 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 ) )
2		fveq2	$$⊢a=g\to \mathrm{bday}\left(a\right)=\mathrm{bday}\left(g\right)$$
3	2	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 |-
4	3	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 |-
5	4	eleq1d	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 ) ) ) ) ) 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 ) ) ) ) ) <-> ( ( ( 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 ) ) ) ) ) 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 |- ( 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 ) ) ) ) ) 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 ) ) ) ) ) <-> ( ( ( 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 ) ) ) ) ) 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 |-
6		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 |-
7	6	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 |-
8	7	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 ) )
9	5 8	imbi12d	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 ) ) ) ) ) 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 ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s 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 ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g 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 ` 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 ` 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 ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
10		fveq2	$$⊢b=h\to \mathrm{bday}\left(b\right)=\mathrm{bday}\left(h\right)$$
11	10	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 |-
12	11	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 |-
13	12	eleq1d	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 ) ) ) ) ) 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 ) ) ) ) ) <-> ( ( ( 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 ) ) ) ) ) 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 |- ( 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 ) ) ) ) ) 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 ) ) ) ) ) <-> ( ( ( 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 ) ) ) ) ) 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 |-
14		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 |-
15	14	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 |-
16	15	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 ) )
17	13 16	imbi12d	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 ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s 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 ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s 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 ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s 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 ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
18		fveq2	$$⊢c=i\to \mathrm{bday}\left(c\right)=\mathrm{bday}\left(i\right)$$
19	18	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 |-
20	19	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 |-
21	18	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 |-
22	21	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 |-
23	20 22	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 |-
24	23	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 |-
25	24	eleq1d	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 ) ) ) ) ) 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 ) ) ) ) ) <-> ( ( ( 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 ) ) ) ) ) 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 |- ( 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 ) ) ) ) ) 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 ) ) ) ) ) <-> ( ( ( 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 ) ) ) ) ) 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 |-
26		breq1	$$⊢c=i\to \left(c{<}_{s}d\leftrightarrow i{<}_{s}d\right)$$
27	26	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)$$
28		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 |-
29		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 |-
30	28 29	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 |-
31	30	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 ) )
32	27 31	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 ) )
33	32	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 ) )
34	25 33	imbi12d	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 ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s 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 ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s 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 ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s 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 ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s e ) )
35		fveq2	$$⊢d=j\to \mathrm{bday}\left(d\right)=\mathrm{bday}\left(j\right)$$
36	35	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 |-
37	36	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 |-
38	35	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 |-
39	38	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 |-
40	37 39	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 |-
41	40	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 |-
42	41	eleq1d	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 ) ) ) ) ) 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 ) ) ) ) ) <-> ( ( ( 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 ) ) ) ) ) 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 |- ( 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 ) ) ) ) ) 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 ) ) ) ) ) <-> ( ( ( 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 ) ) ) ) ) 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 |-
43		breq2	$$⊢d=j\to \left(i{<}_{s}d\leftrightarrow i{<}_{s}j\right)$$
44	43	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)$$
45		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 |-
46		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 |-
47	45 46	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 |-
48	47	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 ) )
49	44 48	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 ) )
50	49	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 ) )
51	42 50	imbi12d	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 ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s 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 ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s 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 ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s 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 ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s e ) )
52		fveq2	$$⊢e=k\to \mathrm{bday}\left(e\right)=\mathrm{bday}\left(k\right)$$
53	52	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 |-
54	53	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 |-
55	52	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 |-
56	55	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 |-
57	54 56	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 |-
58	57	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 |-
59	58	eleq1d	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 ) ) ) ) ) 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 ) ) ) ) ) <-> ( ( ( 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 ) ) ) ) ) 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 |- ( 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 ) ) ) ) ) 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 ) ) ) ) ) <-> ( ( ( 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 ) ) ) ) ) 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 |-
60		breq1	$$⊢e=k\to \left(e{<}_{s}f\leftrightarrow k{<}_{s}f\right)$$
61	60	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)$$
62		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 |-
63	62	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 |-
64		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 |-
65	64	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 |-
66	63 65	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 ) )
67	61 66	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 ) )
68	67	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 ) )
69	59 68	imbi12d	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 ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s 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 ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s 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 ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s 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 ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s k ) )
70		fveq2	$$⊢f=l\to \mathrm{bday}\left(f\right)=\mathrm{bday}\left(l\right)$$
71	70	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 |-
72	71	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 |-
73	70	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 |-
74	73	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 |-
75	72 74	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 |-
76	75	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 |-
77	76	eleq1d	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 ) ) ) ) ) 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 ) ) ) ) ) <-> ( ( ( 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. ( ( ( 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 |- ( 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 ) ) ) ) ) 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 ) ) ) ) ) <-> ( ( ( 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. ( ( ( 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 |-
78		breq2	$$⊢f=l\to \left(k{<}_{s}f\leftrightarrow k{<}_{s}l\right)$$
79	78	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)$$
80		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 |-
81	80	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 |-
82		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 |-
83	82	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 |-
84	81 83	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 ) )
85	79 84	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 ) )
86	85	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 ) )
87	77 86	imbi12d	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 ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s 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 ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) ) ( ( ( ( ( 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 ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s f ) -s ( i x.s 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 ) ) ) ) ) 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
88	9 17 34 51 69 87	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 ( ( ( ( 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 ` 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 ( ( ( ( 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. ( ( ( 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 ) ) ) ) ) -> ( ( 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 ( ( ( ( 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. ( ( ( 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
89	1 88	sylib	Could not format ( ph -> A. g e. No A. h e. No A. i e. No A. j e. No A. k e. No A. l e. No ( ( ( ( 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. ( ( ( 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 ) ) ) ) ) -> ( ( 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 ( ( ( ( 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. ( ( ( 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 ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )