Theorem mulsproplem13

Description: Lemma for surreal multiplication. Remove the restriction on C and D from mulsproplem12 . (Contributed by Scott Fenton, 5-Mar-2025)

	Ref	Expression
Hypotheses	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 ) )
	mulsproplem.2	$$⊢\phi \to C\in \mathrm{No}$$
	mulsproplem.3	$$⊢\phi \to D\in \mathrm{No}$$
	mulsproplem.4	$$⊢\phi \to E\in \mathrm{No}$$
	mulsproplem.5	$$⊢\phi \to F\in \mathrm{No}$$
	mulsproplem.6	$$⊢\phi \to C{<}_{s}D$$
	mulsproplem.7	$$⊢\phi \to E{<}_{s}F$$
	mulsproplem13.1	$$⊢\phi \to \left(\mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\vee \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)$$
Assertion	mulsproplem13	Could not format assertion : No typesetting found for |- ( ph -> ( ( C x.s F ) -s ( C x.s E ) )

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		mulsproplem.2	$$⊢\phi \to C\in \mathrm{No}$$
3		mulsproplem.3	$$⊢\phi \to D\in \mathrm{No}$$
4		mulsproplem.4	$$⊢\phi \to E\in \mathrm{No}$$
5		mulsproplem.5	$$⊢\phi \to F\in \mathrm{No}$$
6		mulsproplem.6	$$⊢\phi \to C{<}_{s}D$$
7		mulsproplem.7	$$⊢\phi \to E{<}_{s}F$$
8		mulsproplem13.1	$$⊢\phi \to \left(\mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\vee \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)$$
9	1	adantr	Could not format ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) \/ ( bday ` D ) e. ( bday ` C ) ) ) -> 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 ) )
10	2	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\vee \mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\right)\right)\to C\in \mathrm{No}$$
11	3	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\vee \mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\right)\right)\to D\in \mathrm{No}$$
12	4	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\vee \mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\right)\right)\to E\in \mathrm{No}$$
13	5	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\vee \mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\right)\right)\to F\in \mathrm{No}$$
14	6	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\vee \mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\right)\right)\to C{<}_{s}D$$
15	7	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\vee \mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\right)\right)\to E{<}_{s}F$$
16		simpr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\vee \mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\right)\right)\to \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\vee \mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\right)$$
17	8	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\vee \mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\right)\right)\to \left(\mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\vee \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)$$
18	9 10 11 12 13 14 15 16 17	mulsproplem12	Could not format ( ( ph /\ ( ( bday ` C ) e. ( bday ` D ) \/ ( bday ` D ) e. ( bday ` C ) ) ) -> ( ( C x.s F ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) )
19	2	adantr	$$⊢\left(\phi \wedge \mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\right)\to C\in \mathrm{No}$$
20	3	adantr	$$⊢\left(\phi \wedge \mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\right)\to D\in \mathrm{No}$$
21		simpr	$$⊢\left(\phi \wedge \mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\right)\to \mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)$$
22	6	adantr	$$⊢\left(\phi \wedge \mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\right)\to C{<}_{s}D$$
23		nodense	$$⊢\left(\left(C\in \mathrm{No}\wedge D\in \mathrm{No}\right)\wedge \left(\mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\wedge C{<}_{s}D\right)\right)\to \exists x\in \mathrm{No}\left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(C\right)\wedge C{<}_{s}x\wedge x{<}_{s}D\right)$$
24	19 20 21 22 23	syl22anc	$$⊢\left(\phi \wedge \mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\right)\to \exists x\in \mathrm{No}\left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(C\right)\wedge C{<}_{s}x\wedge x{<}_{s}D\right)$$
25		unidm	Could not format ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) = ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) : No typesetting found for |- ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) = ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) with typecode |-
26		unidm	Could not format ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) = ( ( bday ` 0s ) +no ( bday ` 0s ) ) : No typesetting found for |- ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) = ( ( bday ` 0s ) +no ( bday ` 0s ) ) with typecode |-
27		bday0s	Could not format ( bday ` 0s ) = (/) : No typesetting found for |- ( bday ` 0s ) = (/) with typecode |-
28	27 27	oveq12i	Could not format ( ( bday ` 0s ) +no ( bday ` 0s ) ) = ( (/) +no (/) ) : No typesetting found for |- ( ( bday ` 0s ) +no ( bday ` 0s ) ) = ( (/) +no (/) ) with typecode |-
29		0elon	$$⊢\varnothing \in \mathrm{On}$$
30		naddrid	Could not format ( (/) e. On -> ( (/) +no (/) ) = (/) ) : No typesetting found for |- ( (/) e. On -> ( (/) +no (/) ) = (/) ) with typecode |-
31	29 30	ax-mp	Could not format ( (/) +no (/) ) = (/) : No typesetting found for |- ( (/) +no (/) ) = (/) with typecode |-
32	28 31	eqtri	Could not format ( ( bday ` 0s ) +no ( bday ` 0s ) ) = (/) : No typesetting found for |- ( ( bday ` 0s ) +no ( bday ` 0s ) ) = (/) with typecode |-
33	25 26 32	3eqtri	Could not format ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) = (/) : No typesetting found for |- ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) = (/) with typecode |-
34	33	uneq2i	Could not format ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( ( bday ` C ) +no ( bday ` F ) ) u. (/) ) : No typesetting found for |- ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( ( bday ` C ) +no ( bday ` F ) ) u. (/) ) with typecode |-
35		un0	Could not format ( ( ( bday ` C ) +no ( bday ` F ) ) u. (/) ) = ( ( bday ` C ) +no ( bday ` F ) ) : No typesetting found for |- ( ( ( bday ` C ) +no ( bday ` F ) ) u. (/) ) = ( ( bday ` C ) +no ( bday ` F ) ) with typecode |-
36	34 35	eqtri	Could not format ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( bday ` C ) +no ( bday ` F ) ) : No typesetting found for |- ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( bday ` C ) +no ( bday ` F ) ) with typecode |-
37		ssun1	Could not format ( ( bday ` C ) +no ( bday ` F ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) : No typesetting found for |- ( ( bday ` C ) +no ( bday ` F ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) with typecode |-
38		ssun2	Could not format ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) C_ ( ( ( ( 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 ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) C_ ( ( ( ( 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 |-
39	37 38	sstri	Could not format ( ( bday ` C ) +no ( bday ` F ) ) C_ ( ( ( ( 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 ` C ) +no ( bday ` F ) ) C_ ( ( ( ( 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 |-
40		ssun2	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 ) ) ) ) C_ ( ( ( 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 ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) C_ ( ( ( 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 |-
41	39 40	sstri	Could not format ( ( bday ` C ) +no ( bday ` F ) ) C_ ( ( ( 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 ` C ) +no ( bday ` F ) ) C_ ( ( ( 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 |-
42	36 41	eqsstri	Could not format ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) C_ ( ( ( 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 ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) C_ ( ( ( 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	42	sseli	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 ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( ( 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 ) ) ) ) ) ) : 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 ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( ( 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 ) ) ) ) ) ) with typecode |-
44	43	imim1i	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 ` 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 ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( 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 ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
45	44	6ralimi	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. 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 ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( 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 ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
46	1 45	syl	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 ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( 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 ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
47	46 2 5	mulsproplem11	Could not format ( ph -> ( C x.s F ) e. No ) : No typesetting found for |- ( ph -> ( C x.s F ) e. No ) with typecode |-
48	33	uneq2i	Could not format ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( ( bday ` C ) +no ( bday ` E ) ) u. (/) ) : No typesetting found for |- ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( ( bday ` C ) +no ( bday ` E ) ) u. (/) ) with typecode |-
49		un0	Could not format ( ( ( bday ` C ) +no ( bday ` E ) ) u. (/) ) = ( ( bday ` C ) +no ( bday ` E ) ) : No typesetting found for |- ( ( ( bday ` C ) +no ( bday ` E ) ) u. (/) ) = ( ( bday ` C ) +no ( bday ` E ) ) with typecode |-
50	48 49	eqtri	Could not format ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( bday ` C ) +no ( bday ` E ) ) : No typesetting found for |- ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( bday ` C ) +no ( bday ` E ) ) with typecode |-
51		ssun1	Could not format ( ( bday ` C ) +no ( bday ` E ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) : No typesetting found for |- ( ( bday ` C ) +no ( bday ` E ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) with typecode |-
52		ssun1	Could not format ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) C_ ( ( ( ( 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 ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) C_ ( ( ( ( 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 |-
53	51 52	sstri	Could not format ( ( bday ` C ) +no ( bday ` E ) ) C_ ( ( ( ( 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 ` C ) +no ( bday ` E ) ) C_ ( ( ( ( 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 |-
54	53 40	sstri	Could not format ( ( bday ` C ) +no ( bday ` E ) ) C_ ( ( ( 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 ` C ) +no ( bday ` E ) ) C_ ( ( ( 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 |-
55	50 54	eqsstri	Could not format ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) C_ ( ( ( 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 ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) C_ ( ( ( 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 |-
56	55	sseli	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 ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( ( 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 ) ) ) ) ) ) : 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 ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( ( 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 ) ) ) ) ) ) with typecode |-
57	56	imim1i	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 ` 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 ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( 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 ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
58	57	6ralimi	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. 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 ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( 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 ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
59	1 58	syl	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 ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( 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 ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
60	59 2 4	mulsproplem11	Could not format ( ph -> ( C x.s E ) e. No ) : No typesetting found for |- ( ph -> ( C x.s E ) e. No ) with typecode |-
61	47 60	subscld	Could not format ( ph -> ( ( C x.s F ) -s ( C x.s E ) ) e. No ) : No typesetting found for |- ( ph -> ( ( C x.s F ) -s ( C x.s E ) ) e. No ) with typecode |-
62	61	adantr	Could not format ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( C x.s F ) -s ( C x.s E ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( C x.s F ) -s ( C x.s E ) ) e. No ) with typecode |-
63	46	adantr	Could not format ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C 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 ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( 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 ` C ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
64		simprr1	$$⊢\left(\mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(C\right)\wedge C{<}_{s}x\wedge x{<}_{s}D\right)\right)\right)\to \mathrm{bday}\left(x\right)\in \mathrm{bday}\left(C\right)$$
65	64	adantl	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(C\right)\wedge C{<}_{s}x\wedge x{<}_{s}D\right)\right)\right)\right)\to \mathrm{bday}\left(x\right)\in \mathrm{bday}\left(C\right)$$
66		bdayelon	$$⊢\mathrm{bday}\left(C\right)\in \mathrm{On}$$
67		simprrl	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(C\right)\wedge C{<}_{s}x\wedge x{<}_{s}D\right)\right)\right)\right)\to x\in \mathrm{No}$$
68		oldbday	$$⊢\left(\mathrm{bday}\left(C\right)\in \mathrm{On}\wedge x\in \mathrm{No}\right)\to \left(x\in \mathrm{Old}\left(\mathrm{bday}\left(C\right)\right)\leftrightarrow \mathrm{bday}\left(x\right)\in \mathrm{bday}\left(C\right)\right)$$
69	66 67 68	sylancr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(C\right)\wedge C{<}_{s}x\wedge x{<}_{s}D\right)\right)\right)\right)\to \left(x\in \mathrm{Old}\left(\mathrm{bday}\left(C\right)\right)\leftrightarrow \mathrm{bday}\left(x\right)\in \mathrm{bday}\left(C\right)\right)$$
70	65 69	mpbird	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(C\right)\wedge C{<}_{s}x\wedge x{<}_{s}D\right)\right)\right)\right)\to x\in \mathrm{Old}\left(\mathrm{bday}\left(C\right)\right)$$
71	5	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(C\right)\wedge C{<}_{s}x\wedge x{<}_{s}D\right)\right)\right)\right)\to F\in \mathrm{No}$$
72	63 70 71	mulsproplem2	Could not format ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( x x.s F ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( x x.s F ) e. No ) with typecode |-
73	59	adantr	Could not format ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C 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 ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( 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 ` C ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
74	4	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(C\right)\wedge C{<}_{s}x\wedge x{<}_{s}D\right)\right)\right)\right)\to E\in \mathrm{No}$$
75	73 70 74	mulsproplem2	Could not format ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( x x.s E ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( x x.s E ) e. No ) with typecode |-
76	72 75	subscld	Could not format ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( x x.s F ) -s ( x x.s E ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( x x.s F ) -s ( x x.s E ) ) e. No ) with typecode |-
77	33	uneq2i	Could not format ( ( ( bday ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( ( bday ` D ) +no ( bday ` F ) ) u. (/) ) : No typesetting found for |- ( ( ( bday ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( ( bday ` D ) +no ( bday ` F ) ) u. (/) ) with typecode |-
78		un0	Could not format ( ( ( bday ` D ) +no ( bday ` F ) ) u. (/) ) = ( ( bday ` D ) +no ( bday ` F ) ) : No typesetting found for |- ( ( ( bday ` D ) +no ( bday ` F ) ) u. (/) ) = ( ( bday ` D ) +no ( bday ` F ) ) with typecode |-
79	77 78	eqtri	Could not format ( ( ( bday ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( bday ` D ) +no ( bday ` F ) ) : No typesetting found for |- ( ( ( bday ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( bday ` D ) +no ( bday ` F ) ) with typecode |-
80		ssun2	Could not format ( ( bday ` D ) +no ( bday ` F ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) : No typesetting found for |- ( ( bday ` D ) +no ( bday ` F ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) with typecode |-
81	80 52	sstri	Could not format ( ( bday ` D ) +no ( bday ` F ) ) C_ ( ( ( ( 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 ` D ) +no ( bday ` F ) ) C_ ( ( ( ( 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 |-
82	81 40	sstri	Could not format ( ( bday ` D ) +no ( bday ` F ) ) C_ ( ( ( 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 ` D ) +no ( bday ` F ) ) C_ ( ( ( 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 |-
83	79 82	eqsstri	Could not format ( ( ( bday ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) C_ ( ( ( 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 ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) C_ ( ( ( 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 |-
84	83	sseli	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 ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( ( 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 ) ) ) ) ) ) : 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 ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( ( 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 ) ) ) ) ) ) with typecode |-
85	84	imim1i	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 ` 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 ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( 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 ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
86	85	6ralimi	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. 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 ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( 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 ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
87	1 86	syl	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 ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( 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 ` D ) +no ( bday ` F ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
88	87 3 5	mulsproplem11	Could not format ( ph -> ( D x.s F ) e. No ) : No typesetting found for |- ( ph -> ( D x.s F ) e. No ) with typecode |-
89	33	uneq2i	Could not format ( ( ( bday ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( ( bday ` D ) +no ( bday ` E ) ) u. (/) ) : No typesetting found for |- ( ( ( bday ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( ( bday ` D ) +no ( bday ` E ) ) u. (/) ) with typecode |-
90		un0	Could not format ( ( ( bday ` D ) +no ( bday ` E ) ) u. (/) ) = ( ( bday ` D ) +no ( bday ` E ) ) : No typesetting found for |- ( ( ( bday ` D ) +no ( bday ` E ) ) u. (/) ) = ( ( bday ` D ) +no ( bday ` E ) ) with typecode |-
91	89 90	eqtri	Could not format ( ( ( bday ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( bday ` D ) +no ( bday ` E ) ) : No typesetting found for |- ( ( ( bday ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( bday ` D ) +no ( bday ` E ) ) with typecode |-
92		ssun2	Could not format ( ( bday ` D ) +no ( bday ` E ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) : No typesetting found for |- ( ( bday ` D ) +no ( bday ` E ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) with typecode |-
93	92 38	sstri	Could not format ( ( bday ` D ) +no ( bday ` E ) ) C_ ( ( ( ( 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 ` D ) +no ( bday ` E ) ) C_ ( ( ( ( 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 |-
94	93 40	sstri	Could not format ( ( bday ` D ) +no ( bday ` E ) ) C_ ( ( ( 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 ` D ) +no ( bday ` E ) ) C_ ( ( ( 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 |-
95	91 94	eqsstri	Could not format ( ( ( bday ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) C_ ( ( ( 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 ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) C_ ( ( ( 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 |-
96	95	sseli	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 ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( ( 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 ) ) ) ) ) ) : 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 ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( ( 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 ) ) ) ) ) ) with typecode |-
97	96	imim1i	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 ` 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 ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( 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 ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
98	97	6ralimi	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. 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 ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( 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 ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
99	1 98	syl	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 ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( 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 ` D ) +no ( bday ` E ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
100	99 3 4	mulsproplem11	Could not format ( ph -> ( D x.s E ) e. No ) : No typesetting found for |- ( ph -> ( D x.s E ) e. No ) with typecode |-
101	88 100	subscld	Could not format ( ph -> ( ( D x.s F ) -s ( D x.s E ) ) e. No ) : No typesetting found for |- ( ph -> ( ( D x.s F ) -s ( D x.s E ) ) e. No ) with typecode |-
102	101	adantr	Could not format ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( D x.s F ) -s ( D x.s E ) ) e. No ) : No typesetting found for |- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( D x.s F ) -s ( D x.s E ) ) e. No ) with typecode |-
103	1	mulsproplemcbv	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 ) )
104	103	adantr	Could not format ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C 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 ) )
105		onelss	$$⊢\mathrm{bday}\left(C\right)\in \mathrm{On}\to \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(C\right)\to \mathrm{bday}\left(x\right)\subseteq \mathrm{bday}\left(C\right)\right)$$
106	66 65 105	mpsyl	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(C\right)\wedge C{<}_{s}x\wedge x{<}_{s}D\right)\right)\right)\right)\to \mathrm{bday}\left(x\right)\subseteq \mathrm{bday}\left(C\right)$$
107		simprl	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(C\right)\wedge C{<}_{s}x\wedge x{<}_{s}D\right)\right)\right)\right)\to \mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)$$
108	106 107	sseqtrd	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(C\right)\wedge C{<}_{s}x\wedge x{<}_{s}D\right)\right)\right)\right)\to \mathrm{bday}\left(x\right)\subseteq \mathrm{bday}\left(D\right)$$
109		bdayelon	$$⊢\mathrm{bday}\left(x\right)\in \mathrm{On}$$
110		bdayelon	$$⊢\mathrm{bday}\left(D\right)\in \mathrm{On}$$
111		bdayelon	$$⊢\mathrm{bday}\left(F\right)\in \mathrm{On}$$
112		naddss1	Could not format ( ( ( bday ` x ) e. On /\ ( bday ` D ) e. On /\ ( bday ` F ) e. On ) -> ( ( bday ` x ) C_ ( bday ` D ) <-> ( ( bday ` x ) +no ( bday ` F ) ) C_ ( ( bday ` D ) +no ( bday ` F ) ) ) ) : No typesetting found for |- ( ( ( bday ` x ) e. On /\ ( bday ` D ) e. On /\ ( bday ` F ) e. On ) -> ( ( bday ` x ) C_ ( bday ` D ) <-> ( ( bday ` x ) +no ( bday ` F ) ) C_ ( ( bday ` D ) +no ( bday ` F ) ) ) ) with typecode |-
113	109 110 111 112	mp3an	Could not format ( ( bday ` x ) C_ ( bday ` D ) <-> ( ( bday ` x ) +no ( bday ` F ) ) C_ ( ( bday ` D ) +no ( bday ` F ) ) ) : No typesetting found for |- ( ( bday ` x ) C_ ( bday ` D ) <-> ( ( bday ` x ) +no ( bday ` F ) ) C_ ( ( bday ` D ) +no ( bday ` F ) ) ) with typecode |-
114	108 113	sylib	Could not format ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( bday ` x ) +no ( bday ` F ) ) C_ ( ( bday ` D ) +no ( bday ` F ) ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( bday ` x ) +no ( bday ` F ) ) C_ ( ( bday ` D ) +no ( bday ` F ) ) ) with typecode |-
115		unss2	Could not format ( ( ( bday ` x ) +no ( bday ` F ) ) C_ ( ( bday ` D ) +no ( bday ` F ) ) -> ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` x ) +no ( bday ` F ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) ) : No typesetting found for |- ( ( ( bday ` x ) +no ( bday ` F ) ) C_ ( ( bday ` D ) +no ( bday ` F ) ) -> ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` x ) +no ( bday ` F ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) ) with typecode |-
116	114 115	syl	Could not format ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` x ) +no ( bday ` F ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` x ) +no ( bday ` F ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) ) with typecode |-
117		bdayelon	$$⊢\mathrm{bday}\left(E\right)\in \mathrm{On}$$
118		naddss1	Could not format ( ( ( bday ` x ) e. On /\ ( bday ` D ) e. On /\ ( bday ` E ) e. On ) -> ( ( bday ` x ) C_ ( bday ` D ) <-> ( ( bday ` x ) +no ( bday ` E ) ) C_ ( ( bday ` D ) +no ( bday ` E ) ) ) ) : No typesetting found for |- ( ( ( bday ` x ) e. On /\ ( bday ` D ) e. On /\ ( bday ` E ) e. On ) -> ( ( bday ` x ) C_ ( bday ` D ) <-> ( ( bday ` x ) +no ( bday ` E ) ) C_ ( ( bday ` D ) +no ( bday ` E ) ) ) ) with typecode |-
119	109 110 117 118	mp3an	Could not format ( ( bday ` x ) C_ ( bday ` D ) <-> ( ( bday ` x ) +no ( bday ` E ) ) C_ ( ( bday ` D ) +no ( bday ` E ) ) ) : No typesetting found for |- ( ( bday ` x ) C_ ( bday ` D ) <-> ( ( bday ` x ) +no ( bday ` E ) ) C_ ( ( bday ` D ) +no ( bday ` E ) ) ) with typecode |-
120	108 119	sylib	Could not format ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( bday ` x ) +no ( bday ` E ) ) C_ ( ( bday ` D ) +no ( bday ` E ) ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( bday ` x ) +no ( bday ` E ) ) C_ ( ( bday ` D ) +no ( bday ` E ) ) ) with typecode |-
121		unss2	Could not format ( ( ( bday ` x ) +no ( bday ` E ) ) C_ ( ( bday ` D ) +no ( bday ` E ) ) -> ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +no ( bday ` E ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) : No typesetting found for |- ( ( ( bday ` x ) +no ( bday ` E ) ) C_ ( ( bday ` D ) +no ( bday ` E ) ) -> ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +no ( bday ` E ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) with typecode |-
122	120 121	syl	Could not format ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +no ( bday ` E ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +no ( bday ` E ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) with typecode |-
123		unss12	Could not format ( ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` x ) +no ( bday ` F ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) /\ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +no ( bday ` E ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) -> ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` x ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +no ( bday ` E ) ) ) ) C_ ( ( ( ( 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 ` C ) +no ( bday ` E ) ) u. ( ( bday ` x ) +no ( bday ` F ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) /\ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +no ( bday ` E ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) -> ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` x ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +no ( bday ` E ) ) ) ) C_ ( ( ( ( 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 |-
124	116 122 123	syl2anc	Could not format ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` x ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +no ( bday ` E ) ) ) ) C_ ( ( ( ( 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 |- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` x ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +no ( bday ` E ) ) ) ) C_ ( ( ( ( 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 |-
125		unss2	Could not format ( ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` x ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +no ( bday ` E ) ) ) ) C_ ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) -> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` x ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +no ( bday ` E ) ) ) ) ) C_ ( ( ( 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 ` C ) +no ( bday ` E ) ) u. ( ( bday ` x ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +no ( bday ` E ) ) ) ) C_ ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) -> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` x ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +no ( bday ` E ) ) ) ) ) C_ ( ( ( 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 |-
126	124 125	syl	Could not format ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` x ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +no ( bday ` E ) ) ) ) ) C_ ( ( ( 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 |- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` x ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +no ( bday ` E ) ) ) ) ) C_ ( ( ( 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 |-
127	126	sseld	Could not format ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( ( 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 ` x ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +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 |- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( ( 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 ` x ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +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 |-
128	127	imim1d	Could not format ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( ( ( 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 ` 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 ` x ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +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 ` 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 ` 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 ` x ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +no ( bday ` E ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
129	128	ralimd6v	Could not format ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( 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 ` x ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +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 ) ) 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 ` x ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +no ( bday ` E ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
130	104 129	mpd	Could not format ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C 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 ` x ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +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 ` x ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` x ) +no ( bday ` E ) ) ) ) ) -> ( ( g x.s h ) e. No /\ ( ( i ( ( i x.s l ) -s ( i x.s k ) )
131	2	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(C\right)\wedge C{<}_{s}x\wedge x{<}_{s}D\right)\right)\right)\right)\to C\in \mathrm{No}$$
132		simprr2	$$⊢\left(\mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(C\right)\wedge C{<}_{s}x\wedge x{<}_{s}D\right)\right)\right)\to C{<}_{s}x$$
133	132	adantl	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(C\right)\wedge C{<}_{s}x\wedge x{<}_{s}D\right)\right)\right)\right)\to C{<}_{s}x$$
134	7	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(C\right)\wedge C{<}_{s}x\wedge x{<}_{s}D\right)\right)\right)\right)\to E{<}_{s}F$$
135	65	olcd	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(C\right)\wedge C{<}_{s}x\wedge x{<}_{s}D\right)\right)\right)\right)\to \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(x\right)\vee \mathrm{bday}\left(x\right)\in \mathrm{bday}\left(C\right)\right)$$
136	8	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(C\right)\wedge C{<}_{s}x\wedge x{<}_{s}D\right)\right)\right)\right)\to \left(\mathrm{bday}\left(E\right)\in \mathrm{bday}\left(F\right)\vee \mathrm{bday}\left(F\right)\in \mathrm{bday}\left(E\right)\right)$$
137	130 131 67 74 71 133 134 135 136	mulsproplem12	Could not format ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( C x.s F ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) )
138		naddss1	Could not format ( ( ( bday ` x ) e. On /\ ( bday ` C ) e. On /\ ( bday ` E ) e. On ) -> ( ( bday ` x ) C_ ( bday ` C ) <-> ( ( bday ` x ) +no ( bday ` E ) ) C_ ( ( bday ` C ) +no ( bday ` E ) ) ) ) : No typesetting found for |- ( ( ( bday ` x ) e. On /\ ( bday ` C ) e. On /\ ( bday ` E ) e. On ) -> ( ( bday ` x ) C_ ( bday ` C ) <-> ( ( bday ` x ) +no ( bday ` E ) ) C_ ( ( bday ` C ) +no ( bday ` E ) ) ) ) with typecode |-
139	109 66 117 138	mp3an	Could not format ( ( bday ` x ) C_ ( bday ` C ) <-> ( ( bday ` x ) +no ( bday ` E ) ) C_ ( ( bday ` C ) +no ( bday ` E ) ) ) : No typesetting found for |- ( ( bday ` x ) C_ ( bday ` C ) <-> ( ( bday ` x ) +no ( bday ` E ) ) C_ ( ( bday ` C ) +no ( bday ` E ) ) ) with typecode |-
140	106 139	sylib	Could not format ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( bday ` x ) +no ( bday ` E ) ) C_ ( ( bday ` C ) +no ( bday ` E ) ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( bday ` x ) +no ( bday ` E ) ) C_ ( ( bday ` C ) +no ( bday ` E ) ) ) with typecode |-
141		unss1	Could not format ( ( ( bday ` x ) +no ( bday ` E ) ) C_ ( ( bday ` C ) +no ( bday ` E ) ) -> ( ( ( bday ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) ) : No typesetting found for |- ( ( ( bday ` x ) +no ( bday ` E ) ) C_ ( ( bday ` C ) +no ( bday ` E ) ) -> ( ( ( bday ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) ) with typecode |-
142	140 141	syl	Could not format ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( bday ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( bday ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) ) with typecode |-
143		naddss1	Could not format ( ( ( bday ` x ) e. On /\ ( bday ` C ) e. On /\ ( bday ` F ) e. On ) -> ( ( bday ` x ) C_ ( bday ` C ) <-> ( ( bday ` x ) +no ( bday ` F ) ) C_ ( ( bday ` C ) +no ( bday ` F ) ) ) ) : No typesetting found for |- ( ( ( bday ` x ) e. On /\ ( bday ` C ) e. On /\ ( bday ` F ) e. On ) -> ( ( bday ` x ) C_ ( bday ` C ) <-> ( ( bday ` x ) +no ( bday ` F ) ) C_ ( ( bday ` C ) +no ( bday ` F ) ) ) ) with typecode |-
144	109 66 111 143	mp3an	Could not format ( ( bday ` x ) C_ ( bday ` C ) <-> ( ( bday ` x ) +no ( bday ` F ) ) C_ ( ( bday ` C ) +no ( bday ` F ) ) ) : No typesetting found for |- ( ( bday ` x ) C_ ( bday ` C ) <-> ( ( bday ` x ) +no ( bday ` F ) ) C_ ( ( bday ` C ) +no ( bday ` F ) ) ) with typecode |-
145	106 144	sylib	Could not format ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( bday ` x ) +no ( bday ` F ) ) C_ ( ( bday ` C ) +no ( bday ` F ) ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( bday ` x ) +no ( bday ` F ) ) C_ ( ( bday ` C ) +no ( bday ` F ) ) ) with typecode |-
146		unss1	Could not format ( ( ( bday ` x ) +no ( bday ` F ) ) C_ ( ( bday ` C ) +no ( bday ` F ) ) -> ( ( ( bday ` x ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) : No typesetting found for |- ( ( ( bday ` x ) +no ( bday ` F ) ) C_ ( ( bday ` C ) +no ( bday ` F ) ) -> ( ( ( bday ` x ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) with typecode |-
147	145 146	syl	Could not format ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( bday ` x ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) : No typesetting found for |- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( bday ` x ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) with typecode |-
148		unss12	Could not format ( ( ( ( ( bday ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) /\ ( ( ( bday ` x ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) -> ( ( ( ( bday ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` x ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) C_ ( ( ( ( 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 ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) /\ ( ( ( bday ` x ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) C_ ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) -> ( ( ( ( bday ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` x ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) C_ ( ( ( ( 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 |-
149	142 147 148	syl2anc	Could not format ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( ( bday ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` x ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) C_ ( ( ( ( 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 |- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( ( bday ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` x ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) C_ ( ( ( ( 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 |-
150		unss2	Could not format ( ( ( ( ( bday ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` x ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) C_ ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) -> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` x ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) C_ ( ( ( 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 ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` x ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) C_ ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) -> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` x ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) C_ ( ( ( 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 |-
151	149 150	syl	Could not format ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` x ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) C_ ( ( ( 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 |- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` x ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) C_ ( ( ( 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 |-
152	151	sseld	Could not format ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( ( 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 ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` x ) +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 |- ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( ( 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 ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` x ) +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 |-
153	152	imim1d	Could not format ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( ( ( ( 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 ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` x ) +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 ` 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 ` l ) ) ) u. ( ( ( bday ` i ) +no ( bday ` l ) ) u. ( ( bday ` j ) +no ( bday ` k ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` x ) +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 ) )
154	153	ralimd6v	Could not format ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( 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 ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` x ) +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 ) ) 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 ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` x ) +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 ) )
155	104 154	mpd	Could not format ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C 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 ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` x ) +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 ` x ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` x ) +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 ) )
156	3	adantr	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(C\right)\wedge C{<}_{s}x\wedge x{<}_{s}D\right)\right)\right)\right)\to D\in \mathrm{No}$$
157		simprr3	$$⊢\left(\mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(C\right)\wedge C{<}_{s}x\wedge x{<}_{s}D\right)\right)\right)\to x{<}_{s}D$$
158	157	adantl	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(C\right)\wedge C{<}_{s}x\wedge x{<}_{s}D\right)\right)\right)\right)\to x{<}_{s}D$$
159	65 107	eleqtrd	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(C\right)\wedge C{<}_{s}x\wedge x{<}_{s}D\right)\right)\right)\right)\to \mathrm{bday}\left(x\right)\in \mathrm{bday}\left(D\right)$$
160	159	orcd	$$⊢\left(\phi \wedge \left(\mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\wedge \left(x\in \mathrm{No}\wedge \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(C\right)\wedge C{<}_{s}x\wedge x{<}_{s}D\right)\right)\right)\right)\to \left(\mathrm{bday}\left(x\right)\in \mathrm{bday}\left(D\right)\vee \mathrm{bday}\left(D\right)\in \mathrm{bday}\left(x\right)\right)$$
161	155 67 156 74 71 158 134 160 136	mulsproplem12	Could not format ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( x x.s F ) -s ( x x.s E ) ) ( ( x x.s F ) -s ( x x.s E ) )
162	62 76 102 137 161	slttrd	Could not format ( ( ph /\ ( ( bday ` C ) = ( bday ` D ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( C x.s F ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) )
163	162	anassrs	Could not format ( ( ( ph /\ ( bday ` C ) = ( bday ` D ) ) /\ ( x e. No /\ ( ( bday ` x ) e. ( bday ` C ) /\ C ( ( C x.s F ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) )
164	24 163	rexlimddv	Could not format ( ( ph /\ ( bday ` C ) = ( bday ` D ) ) -> ( ( C x.s F ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) )
165	66	onordi	$$⊢\mathrm{Ord}\mathrm{bday}\left(C\right)$$
166	110	onordi	$$⊢\mathrm{Ord}\mathrm{bday}\left(D\right)$$
167		ordtri3or	$$⊢\left(\mathrm{Ord}\mathrm{bday}\left(C\right)\wedge \mathrm{Ord}\mathrm{bday}\left(D\right)\right)\to \left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\vee \mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\vee \mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\right)$$
168	165 166 167	mp2an	$$⊢\left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\vee \mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\vee \mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\right)$$
169		df-3or	$$⊢\left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\vee \mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\vee \mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\right)\leftrightarrow \left(\left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\vee \mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\right)\vee \mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\right)$$
170		or32	$$⊢\left(\left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\vee \mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\right)\vee \mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\right)\leftrightarrow \left(\left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\vee \mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\right)\vee \mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\right)$$
171	169 170	bitri	$$⊢\left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\vee \mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\vee \mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\right)\leftrightarrow \left(\left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\vee \mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\right)\vee \mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\right)$$
172	168 171	mpbi	$$⊢\left(\left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\vee \mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\right)\vee \mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\right)$$
173	172	a1i	$$⊢\phi \to \left(\left(\mathrm{bday}\left(C\right)\in \mathrm{bday}\left(D\right)\vee \mathrm{bday}\left(D\right)\in \mathrm{bday}\left(C\right)\right)\vee \mathrm{bday}\left(C\right)=\mathrm{bday}\left(D\right)\right)$$
174	18 164 173	mpjaodan	Could not format ( ph -> ( ( C x.s F ) -s ( C x.s E ) ) ( ( C x.s F ) -s ( C x.s E ) )