Theorem mulsproplem6

Description: Lemma for surreal multiplication. Show one of the inequalities involved in surreal multiplication's cuts. (Contributed by Scott Fenton, 5-Mar-2025)

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