Theorem mulsproplem8

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 ) )
	mulsproplem8.1	$$⊢\phi \to A\in \mathrm{No}$$
	mulsproplem8.2	$$⊢\phi \to B\in \mathrm{No}$$
	mulsproplem8.3	No typesetting found for |- ( ph -> R e. ( _Right ` A ) ) with typecode |-
	mulsproplem8.4	No typesetting found for |- ( ph -> S e. ( _Right ` B ) ) with typecode |-
	mulsproplem8.5	No typesetting found for |- ( ph -> V e. ( _Right ` A ) ) with typecode |-
	mulsproplem8.6	No typesetting found for |- ( ph -> W e. ( _Left ` B ) ) with typecode |-
Assertion	mulsproplem8	Could not format assertion : No typesetting found for |- ( ph -> ( ( ( R x.s B ) +s ( A x.s S ) ) -s ( R x.s S ) )

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