Theorem mulsproplem7

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