Theorem mulsproplem5

Description: Lemma for surreal multiplication. Show one of the inequalities involved in surreal multiplication's cuts. (Contributed by Scott Fenton, 4-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 ) )
	mulsproplem5.1	$$⊢\phi \to A\in \mathrm{No}$$
	mulsproplem5.2	$$⊢\phi \to B\in \mathrm{No}$$
	mulsproplem5.3	No typesetting found for |- ( ph -> P e. ( _Left ` A ) ) with typecode |-
	mulsproplem5.4	No typesetting found for |- ( ph -> Q e. ( _Left ` B ) ) with typecode |-
	mulsproplem5.5	No typesetting found for |- ( ph -> T e. ( _Left ` A ) ) with typecode |-
	mulsproplem5.6	No typesetting found for |- ( ph -> U e. ( _Right ` B ) ) with typecode |-
Assertion	mulsproplem5	Could not format assertion : No typesetting found for |- ( ph -> ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) )

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		mulsproplem5.1	$$⊢\phi \to A\in \mathrm{No}$$
3		mulsproplem5.2	$$⊢\phi \to B\in \mathrm{No}$$
4		mulsproplem5.3	Could not format ( ph -> P e. ( _Left ` A ) ) : No typesetting found for |- ( ph -> P e. ( _Left ` A ) ) with typecode |-
5		mulsproplem5.4	Could not format ( ph -> Q e. ( _Left ` B ) ) : No typesetting found for |- ( ph -> Q e. ( _Left ` B ) ) with typecode |-
6		mulsproplem5.5	Could not format ( ph -> T e. ( _Left ` A ) ) : No typesetting found for |- ( ph -> T e. ( _Left ` A ) ) with typecode |-
7		mulsproplem5.6	Could not format ( ph -> U e. ( _Right ` B ) ) : No typesetting found for |- ( ph -> U e. ( _Right ` B ) ) with typecode |-
8		leftssno	Could not format ( _Left ` A ) C_ No : No typesetting found for |- ( _Left ` A ) C_ No with typecode |-
9	8 4	sselid	$$⊢\phi \to P\in \mathrm{No}$$
10	8 6	sselid	$$⊢\phi \to T\in \mathrm{No}$$
11		sltlin	$$⊢\left(P\in \mathrm{No}\wedge T\in \mathrm{No}\right)\to \left(P{<}_{s}T\vee P=T\vee T{<}_{s}P\right)$$
12	9 10 11	syl2anc	$$⊢\phi \to \left(P{<}_{s}T\vee P=T\vee T{<}_{s}P\right)$$
13		leftssold	Could not format ( _Left ` A ) C_ ( _Old ` ( bday ` A ) ) : No typesetting found for |- ( _Left ` A ) C_ ( _Old ` ( bday ` A ) ) with typecode |-
14	13 4	sselid	$$⊢\phi \to P\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)$$
15	1 14 3	mulsproplem2	Could not format ( ph -> ( P x.s B ) e. No ) : No typesetting found for |- ( ph -> ( P x.s B ) e. No ) with typecode |-
16		leftssold	Could not format ( _Left ` B ) C_ ( _Old ` ( bday ` B ) ) : No typesetting found for |- ( _Left ` B ) C_ ( _Old ` ( bday ` B ) ) with typecode |-
17	16 5	sselid	$$⊢\phi \to Q\in \mathrm{Old}\left(\mathrm{bday}\left(B\right)\right)$$
18	1 2 17	mulsproplem3	Could not format ( ph -> ( A x.s Q ) e. No ) : No typesetting found for |- ( ph -> ( A x.s Q ) e. No ) with typecode |-
19	15 18	addscld	Could not format ( ph -> ( ( P x.s B ) +s ( A x.s Q ) ) e. No ) : No typesetting found for |- ( ph -> ( ( P x.s B ) +s ( A x.s Q ) ) e. No ) with typecode |-
20	1 14 17	mulsproplem4	Could not format ( ph -> ( P x.s Q ) e. No ) : No typesetting found for |- ( ph -> ( P x.s Q ) e. No ) with typecode |-
21	19 20	subscld	Could not format ( ph -> ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) ) e. No ) : No typesetting found for |- ( ph -> ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) ) e. No ) with typecode |-
22	21	adantr	Could not format ( ( ph /\ P ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) ) e. No ) : No typesetting found for |- ( ( ph /\ P ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) ) e. No ) with typecode |-
23	13 6	sselid	$$⊢\phi \to T\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)$$
24	1 23 3	mulsproplem2	Could not format ( ph -> ( T x.s B ) e. No ) : No typesetting found for |- ( ph -> ( T x.s B ) e. No ) with typecode |-
25	24 18	addscld	Could not format ( ph -> ( ( T x.s B ) +s ( A x.s Q ) ) e. No ) : No typesetting found for |- ( ph -> ( ( T x.s B ) +s ( A x.s Q ) ) e. No ) with typecode |-
26	1 23 17	mulsproplem4	Could not format ( ph -> ( T x.s Q ) e. No ) : No typesetting found for |- ( ph -> ( T x.s Q ) e. No ) with typecode |-
27	25 26	subscld	Could not format ( ph -> ( ( ( T x.s B ) +s ( A x.s Q ) ) -s ( T x.s Q ) ) e. No ) : No typesetting found for |- ( ph -> ( ( ( T x.s B ) +s ( A x.s Q ) ) -s ( T x.s Q ) ) e. No ) with typecode |-
28	27	adantr	Could not format ( ( ph /\ P ( ( ( T x.s B ) +s ( A x.s Q ) ) -s ( T x.s Q ) ) e. No ) : No typesetting found for |- ( ( ph /\ P ( ( ( T x.s B ) +s ( A x.s Q ) ) -s ( T x.s Q ) ) e. No ) with typecode |-
29		rightssold	Could not format ( _Right ` B ) C_ ( _Old ` ( bday ` B ) ) : No typesetting found for |- ( _Right ` B ) C_ ( _Old ` ( bday ` B ) ) with typecode |-
30	29 7	sselid	$$⊢\phi \to U\in \mathrm{Old}\left(\mathrm{bday}\left(B\right)\right)$$
31	1 2 30	mulsproplem3	Could not format ( ph -> ( A x.s U ) e. No ) : No typesetting found for |- ( ph -> ( A x.s U ) e. No ) with typecode |-
32	24 31	addscld	Could not format ( ph -> ( ( T x.s B ) +s ( A x.s U ) ) e. No ) : No typesetting found for |- ( ph -> ( ( T x.s B ) +s ( A x.s U ) ) e. No ) with typecode |-
33	1 23 30	mulsproplem4	Could not format ( ph -> ( T x.s U ) e. No ) : No typesetting found for |- ( ph -> ( T x.s U ) e. No ) with typecode |-
34	32 33	subscld	Could not format ( ph -> ( ( ( T x.s B ) +s ( A x.s U ) ) -s ( T x.s U ) ) e. No ) : No typesetting found for |- ( ph -> ( ( ( T x.s B ) +s ( A x.s U ) ) -s ( T x.s U ) ) e. No ) with typecode |-
35	34	adantr	Could not format ( ( ph /\ P ( ( ( T x.s B ) +s ( A x.s U ) ) -s ( T x.s U ) ) e. No ) : No typesetting found for |- ( ( ph /\ P ( ( ( T x.s B ) +s ( A x.s U ) ) -s ( T x.s U ) ) e. No ) with typecode |-
36		ssltleft	Could not format ( B e. No -> ( _Left ` B ) < ( _Left ` B ) <
37	3 36	syl	Could not format ( ph -> ( _Left ` B ) < ( _Left ` B ) <
38		snidg	$$⊢B\in \mathrm{No}\to B\in \left\{B\right\}$$
39	3 38	syl	$$⊢\phi \to B\in \left\{B\right\}$$
40	37 5 39	ssltsepcd	$$⊢\phi \to Q{<}_{s}B$$
41		0sno	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
42	41	a1i	Could not format ( ph -> 0s e. No ) : No typesetting found for |- ( ph -> 0s e. No ) with typecode |-
43		leftssno	Could not format ( _Left ` B ) C_ No : No typesetting found for |- ( _Left ` B ) C_ No with typecode |-
44	43 5	sselid	$$⊢\phi \to Q\in \mathrm{No}$$
45		bday0s	Could not format ( bday ` 0s ) = (/) : No typesetting found for |- ( bday ` 0s ) = (/) with typecode |-
46	45 45	oveq12i	Could not format ( ( bday ` 0s ) +no ( bday ` 0s ) ) = ( (/) +no (/) ) : No typesetting found for |- ( ( bday ` 0s ) +no ( bday ` 0s ) ) = ( (/) +no (/) ) with typecode |-
47		0elon	$$⊢\varnothing \in \mathrm{On}$$
48		naddrid	Could not format ( (/) e. On -> ( (/) +no (/) ) = (/) ) : No typesetting found for |- ( (/) e. On -> ( (/) +no (/) ) = (/) ) with typecode |-
49	47 48	ax-mp	Could not format ( (/) +no (/) ) = (/) : No typesetting found for |- ( (/) +no (/) ) = (/) with typecode |-
50	46 49	eqtri	Could not format ( ( bday ` 0s ) +no ( bday ` 0s ) ) = (/) : No typesetting found for |- ( ( bday ` 0s ) +no ( bday ` 0s ) ) = (/) with typecode |-
51	50	uneq1i	Could not format ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) u. ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) ) ) = ( (/) u. ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) u. ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) ) ) : No typesetting found for |- ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) u. ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) ) ) = ( (/) u. ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) u. ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) ) ) with typecode |-
52		0un	Could not format ( (/) u. ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) u. ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) ) ) = ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) u. ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) ) : No typesetting found for |- ( (/) u. ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) u. ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) ) ) = ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) u. ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) ) with typecode |-
53	51 52	eqtri	Could not format ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) u. ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) ) ) = ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) u. ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) ) : No typesetting found for |- ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) u. ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) ) ) = ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) u. ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) ) with typecode |-
54		oldbdayim	$$⊢P\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\to \mathrm{bday}\left(P\right)\in \mathrm{bday}\left(A\right)$$
55	14 54	syl	$$⊢\phi \to \mathrm{bday}\left(P\right)\in \mathrm{bday}\left(A\right)$$
56		oldbdayim	$$⊢Q\in \mathrm{Old}\left(\mathrm{bday}\left(B\right)\right)\to \mathrm{bday}\left(Q\right)\in \mathrm{bday}\left(B\right)$$
57	17 56	syl	$$⊢\phi \to \mathrm{bday}\left(Q\right)\in \mathrm{bday}\left(B\right)$$
58		bdayelon	$$⊢\mathrm{bday}\left(A\right)\in \mathrm{On}$$
59		bdayelon	$$⊢\mathrm{bday}\left(B\right)\in \mathrm{On}$$
60		naddel12	Could not format ( ( ( bday ` A ) e. On /\ ( bday ` B ) e. On ) -> ( ( ( bday ` P ) e. ( bday ` A ) /\ ( bday ` Q ) e. ( bday ` B ) ) -> ( ( bday ` P ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ( ( bday ` A ) e. On /\ ( bday ` B ) e. On ) -> ( ( ( bday ` P ) e. ( bday ` A ) /\ ( bday ` Q ) e. ( bday ` B ) ) -> ( ( bday ` P ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
61	58 59 60	mp2an	Could not format ( ( ( bday ` P ) e. ( bday ` A ) /\ ( bday ` Q ) e. ( bday ` B ) ) -> ( ( bday ` P ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ( ( bday ` P ) e. ( bday ` A ) /\ ( bday ` Q ) e. ( bday ` B ) ) -> ( ( bday ` P ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
62	55 57 61	syl2anc	Could not format ( ph -> ( ( bday ` P ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ph -> ( ( bday ` P ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
63		oldbdayim	$$⊢T\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\to \mathrm{bday}\left(T\right)\in \mathrm{bday}\left(A\right)$$
64	23 63	syl	$$⊢\phi \to \mathrm{bday}\left(T\right)\in \mathrm{bday}\left(A\right)$$
65		bdayelon	$$⊢\mathrm{bday}\left(T\right)\in \mathrm{On}$$
66		naddel1	Could not format ( ( ( bday ` T ) e. On /\ ( bday ` A ) e. On /\ ( bday ` B ) e. On ) -> ( ( bday ` T ) e. ( bday ` A ) <-> ( ( bday ` T ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ( ( bday ` T ) e. On /\ ( bday ` A ) e. On /\ ( bday ` B ) e. On ) -> ( ( bday ` T ) e. ( bday ` A ) <-> ( ( bday ` T ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
67	65 58 59 66	mp3an	Could not format ( ( bday ` T ) e. ( bday ` A ) <-> ( ( bday ` T ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ( bday ` T ) e. ( bday ` A ) <-> ( ( bday ` T ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
68	64 67	sylib	Could not format ( ph -> ( ( bday ` T ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ph -> ( ( bday ` T ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
69	62 68	jca	Could not format ( ph -> ( ( ( bday ` P ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` T ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( bday ` P ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` T ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
70		bdayelon	$$⊢\mathrm{bday}\left(P\right)\in \mathrm{On}$$
71		naddel1	Could not format ( ( ( bday ` P ) e. On /\ ( bday ` A ) e. On /\ ( bday ` B ) e. On ) -> ( ( bday ` P ) e. ( bday ` A ) <-> ( ( bday ` P ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ( ( bday ` P ) e. On /\ ( bday ` A ) e. On /\ ( bday ` B ) e. On ) -> ( ( bday ` P ) e. ( bday ` A ) <-> ( ( bday ` P ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
72	70 58 59 71	mp3an	Could not format ( ( bday ` P ) e. ( bday ` A ) <-> ( ( bday ` P ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ( bday ` P ) e. ( bday ` A ) <-> ( ( bday ` P ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
73	55 72	sylib	Could not format ( ph -> ( ( bday ` P ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ph -> ( ( bday ` P ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
74		naddel12	Could not format ( ( ( bday ` A ) e. On /\ ( bday ` B ) e. On ) -> ( ( ( bday ` T ) e. ( bday ` A ) /\ ( bday ` Q ) e. ( bday ` B ) ) -> ( ( bday ` T ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ( ( bday ` A ) e. On /\ ( bday ` B ) e. On ) -> ( ( ( bday ` T ) e. ( bday ` A ) /\ ( bday ` Q ) e. ( bday ` B ) ) -> ( ( bday ` T ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
75	58 59 74	mp2an	Could not format ( ( ( bday ` T ) e. ( bday ` A ) /\ ( bday ` Q ) e. ( bday ` B ) ) -> ( ( bday ` T ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ( ( bday ` T ) e. ( bday ` A ) /\ ( bday ` Q ) e. ( bday ` B ) ) -> ( ( bday ` T ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
76	64 57 75	syl2anc	Could not format ( ph -> ( ( bday ` T ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ph -> ( ( bday ` T ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
77	73 76	jca	Could not format ( ph -> ( ( ( bday ` P ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` T ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( bday ` P ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` T ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
78		bdayelon	$$⊢\mathrm{bday}\left(Q\right)\in \mathrm{On}$$
79		naddcl	Could not format ( ( ( bday ` P ) e. On /\ ( bday ` Q ) e. On ) -> ( ( bday ` P ) +no ( bday ` Q ) ) e. On ) : No typesetting found for |- ( ( ( bday ` P ) e. On /\ ( bday ` Q ) e. On ) -> ( ( bday ` P ) +no ( bday ` Q ) ) e. On ) with typecode |-
80	70 78 79	mp2an	Could not format ( ( bday ` P ) +no ( bday ` Q ) ) e. On : No typesetting found for |- ( ( bday ` P ) +no ( bday ` Q ) ) e. On with typecode |-
81		naddcl	Could not format ( ( ( bday ` T ) e. On /\ ( bday ` B ) e. On ) -> ( ( bday ` T ) +no ( bday ` B ) ) e. On ) : No typesetting found for |- ( ( ( bday ` T ) e. On /\ ( bday ` B ) e. On ) -> ( ( bday ` T ) +no ( bday ` B ) ) e. On ) with typecode |-
82	65 59 81	mp2an	Could not format ( ( bday ` T ) +no ( bday ` B ) ) e. On : No typesetting found for |- ( ( bday ` T ) +no ( bday ` B ) ) e. On with typecode |-
83	80 82	onun2i	Could not format ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) e. On : No typesetting found for |- ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) e. On with typecode |-
84		naddcl	Could not format ( ( ( bday ` P ) e. On /\ ( bday ` B ) e. On ) -> ( ( bday ` P ) +no ( bday ` B ) ) e. On ) : No typesetting found for |- ( ( ( bday ` P ) e. On /\ ( bday ` B ) e. On ) -> ( ( bday ` P ) +no ( bday ` B ) ) e. On ) with typecode |-
85	70 59 84	mp2an	Could not format ( ( bday ` P ) +no ( bday ` B ) ) e. On : No typesetting found for |- ( ( bday ` P ) +no ( bday ` B ) ) e. On with typecode |-
86		naddcl	Could not format ( ( ( bday ` T ) e. On /\ ( bday ` Q ) e. On ) -> ( ( bday ` T ) +no ( bday ` Q ) ) e. On ) : No typesetting found for |- ( ( ( bday ` T ) e. On /\ ( bday ` Q ) e. On ) -> ( ( bday ` T ) +no ( bday ` Q ) ) e. On ) with typecode |-
87	65 78 86	mp2an	Could not format ( ( bday ` T ) +no ( bday ` Q ) ) e. On : No typesetting found for |- ( ( bday ` T ) +no ( bday ` Q ) ) e. On with typecode |-
88	85 87	onun2i	Could not format ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) e. On : No typesetting found for |- ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) e. On with typecode |-
89		naddcl	Could not format ( ( ( bday ` A ) e. On /\ ( bday ` B ) e. On ) -> ( ( bday ` A ) +no ( bday ` B ) ) e. On ) : No typesetting found for |- ( ( ( bday ` A ) e. On /\ ( bday ` B ) e. On ) -> ( ( bday ` A ) +no ( bday ` B ) ) e. On ) with typecode |-
90	58 59 89	mp2an	Could not format ( ( bday ` A ) +no ( bday ` B ) ) e. On : No typesetting found for |- ( ( bday ` A ) +no ( bday ` B ) ) e. On with typecode |-
91		onunel	Could not format ( ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) e. On /\ ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) u. ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) : No typesetting found for |- ( ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) e. On /\ ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) u. ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) with typecode |-
92	83 88 90 91	mp3an	Could not format ( ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) u. ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) u. ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
93		onunel	Could not format ( ( ( ( bday ` P ) +no ( bday ` Q ) ) e. On /\ ( ( bday ` T ) +no ( bday ` B ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` P ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` T ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` P ) +no ( bday ` Q ) ) e. On /\ ( ( bday ` T ) +no ( bday ` B ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` P ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` T ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) with typecode |-
94	80 82 90 93	mp3an	Could not format ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` P ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` T ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` P ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` T ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
95		onunel	Could not format ( ( ( ( bday ` P ) +no ( bday ` B ) ) e. On /\ ( ( bday ` T ) +no ( bday ` Q ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` P ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` T ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` P ) +no ( bday ` B ) ) e. On /\ ( ( bday ` T ) +no ( bday ` Q ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` P ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` T ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) with typecode |-
96	85 87 90 95	mp3an	Could not format ( ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` P ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` T ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` P ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` T ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
97	94 96	anbi12i	Could not format ( ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) <-> ( ( ( ( bday ` P ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` T ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) /\ ( ( ( bday ` P ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` T ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) : No typesetting found for |- ( ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) <-> ( ( ( ( bday ` P ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` T ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) /\ ( ( ( bday ` P ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` T ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) with typecode |-
98	92 97	bitri	Could not format ( ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) u. ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` P ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` T ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) /\ ( ( ( bday ` P ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` T ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) : No typesetting found for |- ( ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) u. ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` P ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` T ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) /\ ( ( ( bday ` P ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` T ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) with typecode |-
99	69 77 98	sylanbrc	Could not format ( ph -> ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) u. ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ph -> ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) u. ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
100		elun1	Could not format ( ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) u. ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) -> ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) u. ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) ) 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 ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) u. ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) -> ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) u. ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) ) 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 |-
101	99 100	syl	Could not format ( ph -> ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) u. ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) ) 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 ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) u. ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) ) 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 |-
102	53 101	eqeltrid	Could not format ( ph -> ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) u. ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) ) ) 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 ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` T ) +no ( bday ` B ) ) ) u. ( ( ( bday ` P ) +no ( bday ` B ) ) u. ( ( bday ` T ) +no ( bday ` Q ) ) ) ) ) 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 |-
103	1 42 42 9 10 44 3 102	mulsproplem1	Could not format ( ph -> ( ( 0s x.s 0s ) e. No /\ ( ( P ( ( P x.s B ) -s ( P x.s Q ) ) ( ( 0s x.s 0s ) e. No /\ ( ( P ( ( P x.s B ) -s ( P x.s Q ) )
104	103	simprd	Could not format ( ph -> ( ( P ( ( P x.s B ) -s ( P x.s Q ) ) ( ( P ( ( P x.s B ) -s ( P x.s Q ) )
105	40 104	mpan2d	Could not format ( ph -> ( P ( ( P x.s B ) -s ( P x.s Q ) ) ( P ( ( P x.s B ) -s ( P x.s Q ) )
106	105	imp	Could not format ( ( ph /\ P ( ( P x.s B ) -s ( P x.s Q ) ) ( ( P x.s B ) -s ( P x.s Q ) )
107	15 20	subscld	Could not format ( ph -> ( ( P x.s B ) -s ( P x.s Q ) ) e. No ) : No typesetting found for |- ( ph -> ( ( P x.s B ) -s ( P x.s Q ) ) e. No ) with typecode |-
108	24 26	subscld	Could not format ( ph -> ( ( T x.s B ) -s ( T x.s Q ) ) e. No ) : No typesetting found for |- ( ph -> ( ( T x.s B ) -s ( T x.s Q ) ) e. No ) with typecode |-
109	107 108 18	sltadd1d	Could not format ( ph -> ( ( ( P x.s B ) -s ( P x.s Q ) ) ( ( ( P x.s B ) -s ( P x.s Q ) ) +s ( A x.s Q ) ) ( ( ( P x.s B ) -s ( P x.s Q ) ) ( ( ( P x.s B ) -s ( P x.s Q ) ) +s ( A x.s Q ) )
110	109	adantr	Could not format ( ( ph /\ P ( ( ( P x.s B ) -s ( P x.s Q ) ) ( ( ( P x.s B ) -s ( P x.s Q ) ) +s ( A x.s Q ) ) ( ( ( P x.s B ) -s ( P x.s Q ) ) ( ( ( P x.s B ) -s ( P x.s Q ) ) +s ( A x.s Q ) )
111	106 110	mpbid	Could not format ( ( ph /\ P ( ( ( P x.s B ) -s ( P x.s Q ) ) +s ( A x.s Q ) ) ( ( ( P x.s B ) -s ( P x.s Q ) ) +s ( A x.s Q ) )
112	15 18 20	addsubsd	Could not format ( ph -> ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) ) = ( ( ( P x.s B ) -s ( P x.s Q ) ) +s ( A x.s Q ) ) ) : No typesetting found for |- ( ph -> ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) ) = ( ( ( P x.s B ) -s ( P x.s Q ) ) +s ( A x.s Q ) ) ) with typecode |-
113	112	adantr	Could not format ( ( ph /\ P ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) ) = ( ( ( P x.s B ) -s ( P x.s Q ) ) +s ( A x.s Q ) ) ) : No typesetting found for |- ( ( ph /\ P ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) ) = ( ( ( P x.s B ) -s ( P x.s Q ) ) +s ( A x.s Q ) ) ) with typecode |-
114	24 18 26	addsubsd	Could not format ( ph -> ( ( ( T x.s B ) +s ( A x.s Q ) ) -s ( T x.s Q ) ) = ( ( ( T x.s B ) -s ( T x.s Q ) ) +s ( A x.s Q ) ) ) : No typesetting found for |- ( ph -> ( ( ( T x.s B ) +s ( A x.s Q ) ) -s ( T x.s Q ) ) = ( ( ( T x.s B ) -s ( T x.s Q ) ) +s ( A x.s Q ) ) ) with typecode |-
115	114	adantr	Could not format ( ( ph /\ P ( ( ( T x.s B ) +s ( A x.s Q ) ) -s ( T x.s Q ) ) = ( ( ( T x.s B ) -s ( T x.s Q ) ) +s ( A x.s Q ) ) ) : No typesetting found for |- ( ( ph /\ P ( ( ( T x.s B ) +s ( A x.s Q ) ) -s ( T x.s Q ) ) = ( ( ( T x.s B ) -s ( T x.s Q ) ) +s ( A x.s Q ) ) ) with typecode |-
116	111 113 115	3brtr4d	Could not format ( ( ph /\ P ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) ) ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) )
117		ssltleft	Could not format ( A e. No -> ( _Left ` A ) < ( _Left ` A ) <
118	2 117	syl	Could not format ( ph -> ( _Left ` A ) < ( _Left ` A ) <
119		snidg	$$⊢A\in \mathrm{No}\to A\in \left\{A\right\}$$
120	2 119	syl	$$⊢\phi \to A\in \left\{A\right\}$$
121	118 6 120	ssltsepcd	$$⊢\phi \to T{<}_{s}A$$
122		lltropt	Could not format ( _Left ` B ) <
123	122	a1i	Could not format ( ph -> ( _Left ` B ) < ( _Left ` B ) <
124	123 5 7	ssltsepcd	$$⊢\phi \to Q{<}_{s}U$$
125		rightssno	Could not format ( _Right ` B ) C_ No : No typesetting found for |- ( _Right ` B ) C_ No with typecode |-
126	125 7	sselid	$$⊢\phi \to U\in \mathrm{No}$$
127	50	uneq1i	Could not format ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) ) = ( (/) u. ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) ) : No typesetting found for |- ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) ) = ( (/) u. ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) ) with typecode |-
128		0un	Could not format ( (/) u. ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) ) = ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) : No typesetting found for |- ( (/) u. ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) ) = ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) with typecode |-
129	127 128	eqtri	Could not format ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) ) = ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) : No typesetting found for |- ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) ) = ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) with typecode |-
130		oldbdayim	$$⊢U\in \mathrm{Old}\left(\mathrm{bday}\left(B\right)\right)\to \mathrm{bday}\left(U\right)\in \mathrm{bday}\left(B\right)$$
131	30 130	syl	$$⊢\phi \to \mathrm{bday}\left(U\right)\in \mathrm{bday}\left(B\right)$$
132		bdayelon	$$⊢\mathrm{bday}\left(U\right)\in \mathrm{On}$$
133		naddel2	Could not format ( ( ( bday ` U ) e. On /\ ( bday ` B ) e. On /\ ( bday ` A ) e. On ) -> ( ( bday ` U ) e. ( bday ` B ) <-> ( ( bday ` A ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ( ( bday ` U ) e. On /\ ( bday ` B ) e. On /\ ( bday ` A ) e. On ) -> ( ( bday ` U ) e. ( bday ` B ) <-> ( ( bday ` A ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
134	132 59 58 133	mp3an	Could not format ( ( bday ` U ) e. ( bday ` B ) <-> ( ( bday ` A ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ( bday ` U ) e. ( bday ` B ) <-> ( ( bday ` A ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
135	131 134	sylib	Could not format ( ph -> ( ( bday ` A ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ph -> ( ( bday ` A ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
136	76 135	jca	Could not format ( ph -> ( ( ( bday ` T ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( bday ` T ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
137		naddel12	Could not format ( ( ( bday ` A ) e. On /\ ( bday ` B ) e. On ) -> ( ( ( bday ` T ) e. ( bday ` A ) /\ ( bday ` U ) e. ( bday ` B ) ) -> ( ( bday ` T ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ( ( bday ` A ) e. On /\ ( bday ` B ) e. On ) -> ( ( ( bday ` T ) e. ( bday ` A ) /\ ( bday ` U ) e. ( bday ` B ) ) -> ( ( bday ` T ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
138	58 59 137	mp2an	Could not format ( ( ( bday ` T ) e. ( bday ` A ) /\ ( bday ` U ) e. ( bday ` B ) ) -> ( ( bday ` T ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ( ( bday ` T ) e. ( bday ` A ) /\ ( bday ` U ) e. ( bday ` B ) ) -> ( ( bday ` T ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
139	64 131 138	syl2anc	Could not format ( ph -> ( ( bday ` T ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ph -> ( ( bday ` T ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
140		naddel2	Could not format ( ( ( bday ` Q ) e. On /\ ( bday ` B ) e. On /\ ( bday ` A ) e. On ) -> ( ( bday ` Q ) e. ( bday ` B ) <-> ( ( bday ` A ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ( ( bday ` Q ) e. On /\ ( bday ` B ) e. On /\ ( bday ` A ) e. On ) -> ( ( bday ` Q ) e. ( bday ` B ) <-> ( ( bday ` A ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
141	78 59 58 140	mp3an	Could not format ( ( bday ` Q ) e. ( bday ` B ) <-> ( ( bday ` A ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ( bday ` Q ) e. ( bday ` B ) <-> ( ( bday ` A ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
142	57 141	sylib	Could not format ( ph -> ( ( bday ` A ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ph -> ( ( bday ` A ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
143	139 142	jca	Could not format ( ph -> ( ( ( bday ` T ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( bday ` T ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
144		naddcl	Could not format ( ( ( bday ` A ) e. On /\ ( bday ` U ) e. On ) -> ( ( bday ` A ) +no ( bday ` U ) ) e. On ) : No typesetting found for |- ( ( ( bday ` A ) e. On /\ ( bday ` U ) e. On ) -> ( ( bday ` A ) +no ( bday ` U ) ) e. On ) with typecode |-
145	58 132 144	mp2an	Could not format ( ( bday ` A ) +no ( bday ` U ) ) e. On : No typesetting found for |- ( ( bday ` A ) +no ( bday ` U ) ) e. On with typecode |-
146	87 145	onun2i	Could not format ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) e. On : No typesetting found for |- ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) e. On with typecode |-
147		naddcl	Could not format ( ( ( bday ` T ) e. On /\ ( bday ` U ) e. On ) -> ( ( bday ` T ) +no ( bday ` U ) ) e. On ) : No typesetting found for |- ( ( ( bday ` T ) e. On /\ ( bday ` U ) e. On ) -> ( ( bday ` T ) +no ( bday ` U ) ) e. On ) with typecode |-
148	65 132 147	mp2an	Could not format ( ( bday ` T ) +no ( bday ` U ) ) e. On : No typesetting found for |- ( ( bday ` T ) +no ( bday ` U ) ) e. On with typecode |-
149		naddcl	Could not format ( ( ( bday ` A ) e. On /\ ( bday ` Q ) e. On ) -> ( ( bday ` A ) +no ( bday ` Q ) ) e. On ) : No typesetting found for |- ( ( ( bday ` A ) e. On /\ ( bday ` Q ) e. On ) -> ( ( bday ` A ) +no ( bday ` Q ) ) e. On ) with typecode |-
150	58 78 149	mp2an	Could not format ( ( bday ` A ) +no ( bday ` Q ) ) e. On : No typesetting found for |- ( ( bday ` A ) +no ( bday ` Q ) ) e. On with typecode |-
151	148 150	onun2i	Could not format ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) e. On : No typesetting found for |- ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) e. On with typecode |-
152		onunel	Could not format ( ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) e. On /\ ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) : No typesetting found for |- ( ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) e. On /\ ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) with typecode |-
153	146 151 90 152	mp3an	Could not format ( ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
154		onunel	Could not format ( ( ( ( bday ` T ) +no ( bday ` Q ) ) e. On /\ ( ( bday ` A ) +no ( bday ` U ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` T ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` T ) +no ( bday ` Q ) ) e. On /\ ( ( bday ` A ) +no ( bday ` U ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` T ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) with typecode |-
155	87 145 90 154	mp3an	Could not format ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` T ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` T ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
156		onunel	Could not format ( ( ( ( bday ` T ) +no ( bday ` U ) ) e. On /\ ( ( bday ` A ) +no ( bday ` Q ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` T ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` T ) +no ( bday ` U ) ) e. On /\ ( ( bday ` A ) +no ( bday ` Q ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` T ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) with typecode |-
157	148 150 90 156	mp3an	Could not format ( ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` T ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` T ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
158	155 157	anbi12i	Could not format ( ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) <-> ( ( ( ( bday ` T ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) /\ ( ( ( bday ` T ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) : No typesetting found for |- ( ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) <-> ( ( ( ( bday ` T ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) /\ ( ( ( bday ` T ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) with typecode |-
159	153 158	bitri	Could not format ( ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` T ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) /\ ( ( ( bday ` T ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) : No typesetting found for |- ( ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` T ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) /\ ( ( ( bday ` T ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) with typecode |-
160	136 143 159	sylanbrc	Could not format ( ph -> ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ph -> ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
161		elun1	Could not format ( ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) -> ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) 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 ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) -> ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) 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 |-
162	160 161	syl	Could not format ( ph -> ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) 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 ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) 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 |-
163	129 162	eqeltrid	Could not format ( ph -> ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) ) 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 ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` T ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) ) 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 |-
164	1 42 42 10 2 44 126 163	mulsproplem1	Could not format ( ph -> ( ( 0s x.s 0s ) e. No /\ ( ( T ( ( T x.s U ) -s ( T x.s Q ) ) ( ( 0s x.s 0s ) e. No /\ ( ( T ( ( T x.s U ) -s ( T x.s Q ) )
165	164	simprd	Could not format ( ph -> ( ( T ( ( T x.s U ) -s ( T x.s Q ) ) ( ( T ( ( T x.s U ) -s ( T x.s Q ) )
166	121 124 165	mp2and	Could not format ( ph -> ( ( T x.s U ) -s ( T x.s Q ) ) ( ( T x.s U ) -s ( T x.s Q ) )
167	33 31 26 18	sltsubsub3bd	Could not format ( ph -> ( ( ( T x.s U ) -s ( T x.s Q ) ) ( ( A x.s Q ) -s ( T x.s Q ) ) ( ( ( T x.s U ) -s ( T x.s Q ) ) ( ( A x.s Q ) -s ( T x.s Q ) )
168	18 26	subscld	Could not format ( ph -> ( ( A x.s Q ) -s ( T x.s Q ) ) e. No ) : No typesetting found for |- ( ph -> ( ( A x.s Q ) -s ( T x.s Q ) ) e. No ) with typecode |-
169	31 33	subscld	Could not format ( ph -> ( ( A x.s U ) -s ( T x.s U ) ) e. No ) : No typesetting found for |- ( ph -> ( ( A x.s U ) -s ( T x.s U ) ) e. No ) with typecode |-
170	168 169 24	sltadd2d	Could not format ( ph -> ( ( ( A x.s Q ) -s ( T x.s Q ) ) ( ( T x.s B ) +s ( ( A x.s Q ) -s ( T x.s Q ) ) ) ( ( ( A x.s Q ) -s ( T x.s Q ) ) ( ( T x.s B ) +s ( ( A x.s Q ) -s ( T x.s Q ) ) )
171	167 170	bitrd	Could not format ( ph -> ( ( ( T x.s U ) -s ( T x.s Q ) ) ( ( T x.s B ) +s ( ( A x.s Q ) -s ( T x.s Q ) ) ) ( ( ( T x.s U ) -s ( T x.s Q ) ) ( ( T x.s B ) +s ( ( A x.s Q ) -s ( T x.s Q ) ) )
172	166 171	mpbid	Could not format ( ph -> ( ( T x.s B ) +s ( ( A x.s Q ) -s ( T x.s Q ) ) ) ( ( T x.s B ) +s ( ( A x.s Q ) -s ( T x.s Q ) ) )
173	24 18 26	addsubsassd	Could not format ( ph -> ( ( ( T x.s B ) +s ( A x.s Q ) ) -s ( T x.s Q ) ) = ( ( T x.s B ) +s ( ( A x.s Q ) -s ( T x.s Q ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( T x.s B ) +s ( A x.s Q ) ) -s ( T x.s Q ) ) = ( ( T x.s B ) +s ( ( A x.s Q ) -s ( T x.s Q ) ) ) ) with typecode |-
174	24 31 33	addsubsassd	Could not format ( ph -> ( ( ( T x.s B ) +s ( A x.s U ) ) -s ( T x.s U ) ) = ( ( T x.s B ) +s ( ( A x.s U ) -s ( T x.s U ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( T x.s B ) +s ( A x.s U ) ) -s ( T x.s U ) ) = ( ( T x.s B ) +s ( ( A x.s U ) -s ( T x.s U ) ) ) ) with typecode |-
175	172 173 174	3brtr4d	Could not format ( ph -> ( ( ( T x.s B ) +s ( A x.s Q ) ) -s ( T x.s Q ) ) ( ( ( T x.s B ) +s ( A x.s Q ) ) -s ( T x.s Q ) )
176	175	adantr	Could not format ( ( ph /\ P ( ( ( T x.s B ) +s ( A x.s Q ) ) -s ( T x.s Q ) ) ( ( ( T x.s B ) +s ( A x.s Q ) ) -s ( T x.s Q ) )
177	22 28 35 116 176	slttrd	Could not format ( ( ph /\ P ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) ) ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) )
178	177	ex	Could not format ( ph -> ( P ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) ) ( P ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) )
179		oveq1	Could not format ( P = T -> ( P x.s B ) = ( T x.s B ) ) : No typesetting found for |- ( P = T -> ( P x.s B ) = ( T x.s B ) ) with typecode |-
180	179	oveq1d	Could not format ( P = T -> ( ( P x.s B ) +s ( A x.s Q ) ) = ( ( T x.s B ) +s ( A x.s Q ) ) ) : No typesetting found for |- ( P = T -> ( ( P x.s B ) +s ( A x.s Q ) ) = ( ( T x.s B ) +s ( A x.s Q ) ) ) with typecode |-
181		oveq1	Could not format ( P = T -> ( P x.s Q ) = ( T x.s Q ) ) : No typesetting found for |- ( P = T -> ( P x.s Q ) = ( T x.s Q ) ) with typecode |-
182	180 181	oveq12d	Could not format ( P = T -> ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) ) = ( ( ( T x.s B ) +s ( A x.s Q ) ) -s ( T x.s Q ) ) ) : No typesetting found for |- ( P = T -> ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) ) = ( ( ( T x.s B ) +s ( A x.s Q ) ) -s ( T x.s Q ) ) ) with typecode |-
183	182	breq1d	Could not format ( P = T -> ( ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) ) ( ( ( T x.s B ) +s ( A x.s Q ) ) -s ( T x.s Q ) ) ( ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) ) ( ( ( T x.s B ) +s ( A x.s Q ) ) -s ( T x.s Q ) )
184	175 183	syl5ibrcom	Could not format ( ph -> ( P = T -> ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) ) ( P = T -> ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) )
185	21	adantr	Could not format ( ( ph /\ T ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) ) e. No ) : No typesetting found for |- ( ( ph /\ T ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) ) e. No ) with typecode |-
186	15 31	addscld	Could not format ( ph -> ( ( P x.s B ) +s ( A x.s U ) ) e. No ) : No typesetting found for |- ( ph -> ( ( P x.s B ) +s ( A x.s U ) ) e. No ) with typecode |-
187	1 14 30	mulsproplem4	Could not format ( ph -> ( P x.s U ) e. No ) : No typesetting found for |- ( ph -> ( P x.s U ) e. No ) with typecode |-
188	186 187	subscld	Could not format ( ph -> ( ( ( P x.s B ) +s ( A x.s U ) ) -s ( P x.s U ) ) e. No ) : No typesetting found for |- ( ph -> ( ( ( P x.s B ) +s ( A x.s U ) ) -s ( P x.s U ) ) e. No ) with typecode |-
189	188	adantr	Could not format ( ( ph /\ T ( ( ( P x.s B ) +s ( A x.s U ) ) -s ( P x.s U ) ) e. No ) : No typesetting found for |- ( ( ph /\ T ( ( ( P x.s B ) +s ( A x.s U ) ) -s ( P x.s U ) ) e. No ) with typecode |-
190	34	adantr	Could not format ( ( ph /\ T ( ( ( T x.s B ) +s ( A x.s U ) ) -s ( T x.s U ) ) e. No ) : No typesetting found for |- ( ( ph /\ T ( ( ( T x.s B ) +s ( A x.s U ) ) -s ( T x.s U ) ) e. No ) with typecode |-
191	118 4 120	ssltsepcd	$$⊢\phi \to P{<}_{s}A$$
192	50	uneq1i	Could not format ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) ) = ( (/) u. ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) ) : No typesetting found for |- ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) ) = ( (/) u. ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) ) with typecode |-
193		0un	Could not format ( (/) u. ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) ) = ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) : No typesetting found for |- ( (/) u. ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) ) = ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) with typecode |-
194	192 193	eqtri	Could not format ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) ) = ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) : No typesetting found for |- ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) ) = ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) with typecode |-
195	62 135	jca	Could not format ( ph -> ( ( ( bday ` P ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( bday ` P ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
196		naddel12	Could not format ( ( ( bday ` A ) e. On /\ ( bday ` B ) e. On ) -> ( ( ( bday ` P ) e. ( bday ` A ) /\ ( bday ` U ) e. ( bday ` B ) ) -> ( ( bday ` P ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ( ( bday ` A ) e. On /\ ( bday ` B ) e. On ) -> ( ( ( bday ` P ) e. ( bday ` A ) /\ ( bday ` U ) e. ( bday ` B ) ) -> ( ( bday ` P ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
197	58 59 196	mp2an	Could not format ( ( ( bday ` P ) e. ( bday ` A ) /\ ( bday ` U ) e. ( bday ` B ) ) -> ( ( bday ` P ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ( ( bday ` P ) e. ( bday ` A ) /\ ( bday ` U ) e. ( bday ` B ) ) -> ( ( bday ` P ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
198	55 131 197	syl2anc	Could not format ( ph -> ( ( bday ` P ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ph -> ( ( bday ` P ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
199	198 142	jca	Could not format ( ph -> ( ( ( bday ` P ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( bday ` P ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
200	80 145	onun2i	Could not format ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) e. On : No typesetting found for |- ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) e. On with typecode |-
201		naddcl	Could not format ( ( ( bday ` P ) e. On /\ ( bday ` U ) e. On ) -> ( ( bday ` P ) +no ( bday ` U ) ) e. On ) : No typesetting found for |- ( ( ( bday ` P ) e. On /\ ( bday ` U ) e. On ) -> ( ( bday ` P ) +no ( bday ` U ) ) e. On ) with typecode |-
202	70 132 201	mp2an	Could not format ( ( bday ` P ) +no ( bday ` U ) ) e. On : No typesetting found for |- ( ( bday ` P ) +no ( bday ` U ) ) e. On with typecode |-
203	202 150	onun2i	Could not format ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) e. On : No typesetting found for |- ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) e. On with typecode |-
204		onunel	Could not format ( ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) e. On /\ ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) : No typesetting found for |- ( ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) e. On /\ ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) with typecode |-
205	200 203 90 204	mp3an	Could not format ( ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
206		onunel	Could not format ( ( ( ( bday ` P ) +no ( bday ` Q ) ) e. On /\ ( ( bday ` A ) +no ( bday ` U ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` P ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` P ) +no ( bday ` Q ) ) e. On /\ ( ( bday ` A ) +no ( bday ` U ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` P ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) with typecode |-
207	80 145 90 206	mp3an	Could not format ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` P ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` P ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
208		onunel	Could not format ( ( ( ( bday ` P ) +no ( bday ` U ) ) e. On /\ ( ( bday ` A ) +no ( bday ` Q ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` P ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` P ) +no ( bday ` U ) ) e. On /\ ( ( bday ` A ) +no ( bday ` Q ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` P ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) with typecode |-
209	202 150 90 208	mp3an	Could not format ( ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` P ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` P ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
210	207 209	anbi12i	Could not format ( ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) <-> ( ( ( ( bday ` P ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) /\ ( ( ( bday ` P ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) : No typesetting found for |- ( ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) <-> ( ( ( ( bday ` P ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) /\ ( ( ( bday ` P ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) with typecode |-
211	205 210	bitri	Could not format ( ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` P ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) /\ ( ( ( bday ` P ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) : No typesetting found for |- ( ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` P ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) /\ ( ( ( bday ` P ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` A ) +no ( bday ` Q ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) with typecode |-
212	195 199 211	sylanbrc	Could not format ( ph -> ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ph -> ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
213		elun1	Could not format ( ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) -> ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) 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 ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) -> ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) 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 |-
214	212 213	syl	Could not format ( ph -> ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) 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 ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) 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 |-
215	194 214	eqeltrid	Could not format ( ph -> ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) ) 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 ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` P ) +no ( bday ` Q ) ) u. ( ( bday ` A ) +no ( bday ` U ) ) ) u. ( ( ( bday ` P ) +no ( bday ` U ) ) u. ( ( bday ` A ) +no ( bday ` Q ) ) ) ) ) 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 |-
216	1 42 42 9 2 44 126 215	mulsproplem1	Could not format ( ph -> ( ( 0s x.s 0s ) e. No /\ ( ( P ( ( P x.s U ) -s ( P x.s Q ) ) ( ( 0s x.s 0s ) e. No /\ ( ( P ( ( P x.s U ) -s ( P x.s Q ) )
217	216	simprd	Could not format ( ph -> ( ( P ( ( P x.s U ) -s ( P x.s Q ) ) ( ( P ( ( P x.s U ) -s ( P x.s Q ) )
218	191 124 217	mp2and	Could not format ( ph -> ( ( P x.s U ) -s ( P x.s Q ) ) ( ( P x.s U ) -s ( P x.s Q ) )
219	187 31 20 18	sltsubsub3bd	Could not format ( ph -> ( ( ( P x.s U ) -s ( P x.s Q ) ) ( ( A x.s Q ) -s ( P x.s Q ) ) ( ( ( P x.s U ) -s ( P x.s Q ) ) ( ( A x.s Q ) -s ( P x.s Q ) )
220	18 20	subscld	Could not format ( ph -> ( ( A x.s Q ) -s ( P x.s Q ) ) e. No ) : No typesetting found for |- ( ph -> ( ( A x.s Q ) -s ( P x.s Q ) ) e. No ) with typecode |-
221	31 187	subscld	Could not format ( ph -> ( ( A x.s U ) -s ( P x.s U ) ) e. No ) : No typesetting found for |- ( ph -> ( ( A x.s U ) -s ( P x.s U ) ) e. No ) with typecode |-
222	220 221 15	sltadd2d	Could not format ( ph -> ( ( ( A x.s Q ) -s ( P x.s Q ) ) ( ( P x.s B ) +s ( ( A x.s Q ) -s ( P x.s Q ) ) ) ( ( ( A x.s Q ) -s ( P x.s Q ) ) ( ( P x.s B ) +s ( ( A x.s Q ) -s ( P x.s Q ) ) )
223	219 222	bitrd	Could not format ( ph -> ( ( ( P x.s U ) -s ( P x.s Q ) ) ( ( P x.s B ) +s ( ( A x.s Q ) -s ( P x.s Q ) ) ) ( ( ( P x.s U ) -s ( P x.s Q ) ) ( ( P x.s B ) +s ( ( A x.s Q ) -s ( P x.s Q ) ) )
224	218 223	mpbid	Could not format ( ph -> ( ( P x.s B ) +s ( ( A x.s Q ) -s ( P x.s Q ) ) ) ( ( P x.s B ) +s ( ( A x.s Q ) -s ( P x.s Q ) ) )
225	15 18 20	addsubsassd	Could not format ( ph -> ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) ) = ( ( P x.s B ) +s ( ( A x.s Q ) -s ( P x.s Q ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) ) = ( ( P x.s B ) +s ( ( A x.s Q ) -s ( P x.s Q ) ) ) ) with typecode |-
226	15 31 187	addsubsassd	Could not format ( ph -> ( ( ( P x.s B ) +s ( A x.s U ) ) -s ( P x.s U ) ) = ( ( P x.s B ) +s ( ( A x.s U ) -s ( P x.s U ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( P x.s B ) +s ( A x.s U ) ) -s ( P x.s U ) ) = ( ( P x.s B ) +s ( ( A x.s U ) -s ( P x.s U ) ) ) ) with typecode |-
227	224 225 226	3brtr4d	Could not format ( ph -> ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) ) ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) )
228	227	adantr	Could not format ( ( ph /\ T ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) ) ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) )
229		ssltright	Could not format ( B e. No -> { B } < { B } <
230	3 229	syl	Could not format ( ph -> { B } < { B } <
231	230 39 7	ssltsepcd	$$⊢\phi \to B{<}_{s}U$$
232	50	uneq1i	Could not format ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) ) ) = ( (/) u. ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) ) ) : No typesetting found for |- ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) ) ) = ( (/) u. ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) ) ) with typecode |-
233		0un	Could not format ( (/) u. ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) ) ) = ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( (/) u. ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) ) ) = ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) ) with typecode |-
234	232 233	eqtri	Could not format ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) ) ) = ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) ) ) = ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) ) with typecode |-
235		onunel	Could not format ( ( ( ( bday ` T ) +no ( bday ` B ) ) e. On /\ ( ( bday ` P ) +no ( bday ` U ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` T ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` P ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` T ) +no ( bday ` B ) ) e. On /\ ( ( bday ` P ) +no ( bday ` U ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` T ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` P ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) with typecode |-
236	82 202 90 235	mp3an	Could not format ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` T ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` P ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` T ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` P ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
237	68 198 236	sylanbrc	Could not format ( ph -> ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ph -> ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
238	139 73	jca	Could not format ( ph -> ( ( ( bday ` T ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` P ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( bday ` T ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` P ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
239	82 202	onun2i	Could not format ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) e. On : No typesetting found for |- ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) e. On with typecode |-
240	148 85	onun2i	Could not format ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) e. On : No typesetting found for |- ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) e. On with typecode |-
241		onunel	Could not format ( ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) e. On /\ ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) : No typesetting found for |- ( ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) e. On /\ ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) with typecode |-
242	239 240 90 241	mp3an	Could not format ( ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
243		onunel	Could not format ( ( ( ( bday ` T ) +no ( bday ` U ) ) e. On /\ ( ( bday ` P ) +no ( bday ` B ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` T ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` P ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` T ) +no ( bday ` U ) ) e. On /\ ( ( bday ` P ) +no ( bday ` B ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` T ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` P ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) with typecode |-
244	148 85 90 243	mp3an	Could not format ( ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` T ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` P ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( bday ` T ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` P ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
245	244	anbi2i	Could not format ( ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) <-> ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` T ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` P ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) : No typesetting found for |- ( ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) <-> ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` T ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` P ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) with typecode |-
246	242 245	bitri	Could not format ( ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` T ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` P ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) : No typesetting found for |- ( ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( ( bday ` T ) +no ( bday ` U ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) /\ ( ( bday ` P ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) ) with typecode |-
247	237 238 246	sylanbrc	Could not format ( ph -> ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ph -> ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
248		elun1	Could not format ( ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) -> ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) ) 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 ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) -> ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) ) 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 |-
249	247 248	syl	Could not format ( ph -> ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) ) 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 ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) ) 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 |-
250	234 249	eqeltrid	Could not format ( ph -> ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) ) ) 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 ` 0s ) +no ( bday ` 0s ) ) u. ( ( ( ( bday ` T ) +no ( bday ` B ) ) u. ( ( bday ` P ) +no ( bday ` U ) ) ) u. ( ( ( bday ` T ) +no ( bday ` U ) ) u. ( ( bday ` P ) +no ( bday ` B ) ) ) ) ) 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 |-
251	1 42 42 10 9 3 126 250	mulsproplem1	Could not format ( ph -> ( ( 0s x.s 0s ) e. No /\ ( ( T ( ( T x.s U ) -s ( T x.s B ) ) ( ( 0s x.s 0s ) e. No /\ ( ( T ( ( T x.s U ) -s ( T x.s B ) )
252	251	simprd	Could not format ( ph -> ( ( T ( ( T x.s U ) -s ( T x.s B ) ) ( ( T ( ( T x.s U ) -s ( T x.s B ) )
253	231 252	mpan2d	Could not format ( ph -> ( T ( ( T x.s U ) -s ( T x.s B ) ) ( T ( ( T x.s U ) -s ( T x.s B ) )
254	253	imp	Could not format ( ( ph /\ T ( ( T x.s U ) -s ( T x.s B ) ) ( ( T x.s U ) -s ( T x.s B ) )
255	33 24 187 15	sltsubsub2bd	Could not format ( ph -> ( ( ( T x.s U ) -s ( T x.s B ) ) ( ( P x.s B ) -s ( P x.s U ) ) ( ( ( T x.s U ) -s ( T x.s B ) ) ( ( P x.s B ) -s ( P x.s U ) )
256	15 187	subscld	Could not format ( ph -> ( ( P x.s B ) -s ( P x.s U ) ) e. No ) : No typesetting found for |- ( ph -> ( ( P x.s B ) -s ( P x.s U ) ) e. No ) with typecode |-
257	24 33	subscld	Could not format ( ph -> ( ( T x.s B ) -s ( T x.s U ) ) e. No ) : No typesetting found for |- ( ph -> ( ( T x.s B ) -s ( T x.s U ) ) e. No ) with typecode |-
258	256 257 31	sltadd1d	Could not format ( ph -> ( ( ( P x.s B ) -s ( P x.s U ) ) ( ( ( P x.s B ) -s ( P x.s U ) ) +s ( A x.s U ) ) ( ( ( P x.s B ) -s ( P x.s U ) ) ( ( ( P x.s B ) -s ( P x.s U ) ) +s ( A x.s U ) )
259	255 258	bitrd	Could not format ( ph -> ( ( ( T x.s U ) -s ( T x.s B ) ) ( ( ( P x.s B ) -s ( P x.s U ) ) +s ( A x.s U ) ) ( ( ( T x.s U ) -s ( T x.s B ) ) ( ( ( P x.s B ) -s ( P x.s U ) ) +s ( A x.s U ) )
260	259	adantr	Could not format ( ( ph /\ T ( ( ( T x.s U ) -s ( T x.s B ) ) ( ( ( P x.s B ) -s ( P x.s U ) ) +s ( A x.s U ) ) ( ( ( T x.s U ) -s ( T x.s B ) ) ( ( ( P x.s B ) -s ( P x.s U ) ) +s ( A x.s U ) )
261	254 260	mpbid	Could not format ( ( ph /\ T ( ( ( P x.s B ) -s ( P x.s U ) ) +s ( A x.s U ) ) ( ( ( P x.s B ) -s ( P x.s U ) ) +s ( A x.s U ) )
262	15 31 187	addsubsd	Could not format ( ph -> ( ( ( P x.s B ) +s ( A x.s U ) ) -s ( P x.s U ) ) = ( ( ( P x.s B ) -s ( P x.s U ) ) +s ( A x.s U ) ) ) : No typesetting found for |- ( ph -> ( ( ( P x.s B ) +s ( A x.s U ) ) -s ( P x.s U ) ) = ( ( ( P x.s B ) -s ( P x.s U ) ) +s ( A x.s U ) ) ) with typecode |-
263	262	adantr	Could not format ( ( ph /\ T ( ( ( P x.s B ) +s ( A x.s U ) ) -s ( P x.s U ) ) = ( ( ( P x.s B ) -s ( P x.s U ) ) +s ( A x.s U ) ) ) : No typesetting found for |- ( ( ph /\ T ( ( ( P x.s B ) +s ( A x.s U ) ) -s ( P x.s U ) ) = ( ( ( P x.s B ) -s ( P x.s U ) ) +s ( A x.s U ) ) ) with typecode |-
264	24 31 33	addsubsd	Could not format ( ph -> ( ( ( T x.s B ) +s ( A x.s U ) ) -s ( T x.s U ) ) = ( ( ( T x.s B ) -s ( T x.s U ) ) +s ( A x.s U ) ) ) : No typesetting found for |- ( ph -> ( ( ( T x.s B ) +s ( A x.s U ) ) -s ( T x.s U ) ) = ( ( ( T x.s B ) -s ( T x.s U ) ) +s ( A x.s U ) ) ) with typecode |-
265	264	adantr	Could not format ( ( ph /\ T ( ( ( T x.s B ) +s ( A x.s U ) ) -s ( T x.s U ) ) = ( ( ( T x.s B ) -s ( T x.s U ) ) +s ( A x.s U ) ) ) : No typesetting found for |- ( ( ph /\ T ( ( ( T x.s B ) +s ( A x.s U ) ) -s ( T x.s U ) ) = ( ( ( T x.s B ) -s ( T x.s U ) ) +s ( A x.s U ) ) ) with typecode |-
266	261 263 265	3brtr4d	Could not format ( ( ph /\ T ( ( ( P x.s B ) +s ( A x.s U ) ) -s ( P x.s U ) ) ( ( ( P x.s B ) +s ( A x.s U ) ) -s ( P x.s U ) )
267	185 189 190 228 266	slttrd	Could not format ( ( ph /\ T ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) ) ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) )
268	267	ex	Could not format ( ph -> ( T ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) ) ( T ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) )
269	178 184 268	3jaod	Could not format ( ph -> ( ( P ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) ) ( ( P ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) )
270	12 269	mpd	Could not format ( ph -> ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) ) ( ( ( P x.s B ) +s ( A x.s Q ) ) -s ( P x.s Q ) )