Quantum Logic Explorer		< Previous   Next > Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  3dp43		Unicode version

---

Theorem 3dp43 1206

Description: "3OA" version of xdp43 1205. Changed a2 to a1 and b2 to b1.

Hypotheses

Ref	Expression
3dp.c0	c0 a1 a1 b1 b1
3dp.c1	c1 a0 a1 b0 b1
3dp.c2	c2 a0 a1 b0 b1
3dp.d	a1 a0 a1 b1
3dp.e	b0 a0 p0
3dp.p	a0 b0 a1 b1 a1 b1
3dp.p0	p0 a1 b1 a1 b1
3dp.p2	p2 a0 b0 a1 b1

Assertion

Ref	Expression
3dp43	a0 b0 b1 c2 c0 c1

---

Proof of Theorem 3dp43

Step	Hyp	Ref	Expression
1		leor 159	. 2 a0
2		leo 158	. . 3 a0 a0 b0 b1 c2 c0 c1
3		3dp.p	. . . . . . . 8 a0 b0 a1 b1 a1 b1
4		anass 76	. . . . . . . 8 a0 b0 a1 b1 a1 b1 a0 b0 a1 b1 a1 b1
5	3, 4	tr 62	. . . . . . 7 a0 b0 a1 b1 a1 b1
6		3dp.p0	. . . . . . . . . . 11 p0 a1 b1 a1 b1
7	6	lan 77	. . . . . . . . . 10 a0 b0 p0 a0 b0 a1 b1 a1 b1
8	7	cm 61	. . . . . . . . 9 a0 b0 a1 b1 a1 b1 a0 b0 p0
9		leao4 165	. . . . . . . . 9 a0 b0 p0 a0 p0
10	8, 9	bltr 138	. . . . . . . 8 a0 b0 a1 b1 a1 b1 a0 p0
11		lea 160	. . . . . . . . 9 a0 b0 a1 b1 a1 b1 a0 b0
12		orcom 73	. . . . . . . . 9 a0 b0 b0 a0
13	11, 12	lbtr 139	. . . . . . . 8 a0 b0 a1 b1 a1 b1 b0 a0
14	10, 13	ler2an 173	. . . . . . 7 a0 b0 a1 b1 a1 b1 a0 p0 b0 a0
15	5, 14	bltr 138	. . . . . 6 a0 p0 b0 a0
16		leo 158	. . . . . . . 8 a0 a0 p0
17	16	mldual2i 1125	. . . . . . 7 a0 p0 b0 a0 a0 p0 b0 a0
18		ancom 74	. . . . . . . 8 a0 p0 b0 b0 a0 p0
19	18	ror 71	. . . . . . 7 a0 p0 b0 a0 b0 a0 p0 a0
20	17, 19	tr 62	. . . . . 6 a0 p0 b0 a0 b0 a0 p0 a0
21	15, 20	lbtr 139	. . . . 5 b0 a0 p0 a0
22	2	lelor 166	. . . . 5 b0 a0 p0 a0 b0 a0 p0 a0 b0 b1 c2 c0 c1
23	21, 22	letr 137	. . . 4 b0 a0 p0 a0 b0 b1 c2 c0 c1
24		lea 160	. . . . . . . 8 b0 a0 p0 b0
25		leor 159	. . . . . . . . 9 b0 a0 p0 b1 b0 a0 p0
26		leo 158	. . . . . . . . . 10 b1 b1 a0 a1 c0 c1
27		leo 158	. . . . . . . . . . . . . 14 b0 a0 p0 b0 a0 p0 b1
28	6	lor 70	. . . . . . . . . . . . . . . 16 a0 p0 a0 a1 b1 a1 b1
29	28	lan 77	. . . . . . . . . . . . . . 15 b0 a0 p0 b0 a0 a1 b1 a1 b1
30		lear 161	. . . . . . . . . . . . . . . 16 b0 a0 a1 b1 a1 b1 a0 a1 b1 a1 b1
31		lea 160	. . . . . . . . . . . . . . . . . 18 a1 b1 a1 b1 a1 b1
32	31	lelor 166	. . . . . . . . . . . . . . . . 17 a0 a1 b1 a1 b1 a0 a1 b1
33		ax-a3 32	. . . . . . . . . . . . . . . . . 18 a0 a1 b1 a0 a1 b1
34	33	cm 61	. . . . . . . . . . . . . . . . 17 a0 a1 b1 a0 a1 b1
35	32, 34	lbtr 139	. . . . . . . . . . . . . . . 16 a0 a1 b1 a1 b1 a0 a1 b1
36	30, 35	letr 137	. . . . . . . . . . . . . . 15 b0 a0 a1 b1 a1 b1 a0 a1 b1
37	29, 36	bltr 138	. . . . . . . . . . . . . 14 b0 a0 p0 a0 a1 b1
38	27, 37	ler2an 173	. . . . . . . . . . . . 13 b0 a0 p0 b0 a0 p0 b1 a0 a1 b1
39		leor 159	. . . . . . . . . . . . . . 15 b1 b0 a0 p0 b1
40	39	mldual2i 1125	. . . . . . . . . . . . . 14 b0 a0 p0 b1 a0 a1 b1 b0 a0 p0 b1 a0 a1 b1
41		ancom 74	. . . . . . . . . . . . . . 15 b0 a0 p0 b1 a0 a1 a0 a1 b0 a0 p0 b1
42	41	ror 71	. . . . . . . . . . . . . 14 b0 a0 p0 b1 a0 a1 b1 a0 a1 b0 a0 p0 b1 b1
43	40, 42	tr 62	. . . . . . . . . . . . 13 b0 a0 p0 b1 a0 a1 b1 a0 a1 b0 a0 p0 b1 b1
44	38, 43	lbtr 139	. . . . . . . . . . . 12 b0 a0 p0 a0 a1 b0 a0 p0 b1 b1
45	26	lelor 166	. . . . . . . . . . . 12 a0 a1 b0 a0 p0 b1 b1 a0 a1 b0 a0 p0 b1 b1 a0 a1 c0 c1
46	44, 45	letr 137	. . . . . . . . . . 11 b0 a0 p0 a0 a1 b0 a0 p0 b1 b1 a0 a1 c0 c1
47		lea 160	. . . . . . . . . . . . . . . 16 a0 a1 b0 a0 p0 b1 a0 a1
48		ax-a2 31	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 a0 a1 a1 a0
49		ax-a2 31	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 b1 b1
50	48, 49	2an 79	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 a0 a1 b1 a1 a0 b1
51		ancom 74	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 a1 a0 b1 b1 a1 a0
52	50, 51	tr 62	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 a0 a1 b1 b1 a1 a0
53		leor 159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 b1 a1 b1
54	53	leror 152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 b1 a1 b1
55		leo 158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 a1 a0 a1 a0
56	54, 55	le2an 169	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 b1 a1 a0 a1 b1 a1 a0
57	52, 56	bltr 138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 a0 a1 b1 a1 b1 a1 a0
58	57	df2le2 136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 a0 a1 b1 a1 b1 a1 a0 a0 a1 b1
59	58	cm 61	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 a0 a1 b1 a0 a1 b1 a1 b1 a1 a0
60		anass 76	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 a0 a1 b1 a1 b1 a1 a0 a0 a1 b1 a1 b1 a1 a0
61	60	cm 61	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 a0 a1 b1 a1 b1 a1 a0 a0 a1 b1 a1 b1 a1 a0
62	59, 61	tr 62	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 a0 a1 b1 a0 a1 b1 a1 b1 a1 a0
63		ax-a2 31	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 a1 a0 a0 a1
64	63	ror 71	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 a1 a0 a0 a1
65		or32 82	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 a0 a1 a0 a1
66	64, 65	tr 62	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 a1 a0 a0 a1
67	66	lan 77	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 a1 b1 a1 a0 a1 b1 a0 a1
68		ancom 74	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 a1 b1 a0 a1 a0 a1 a1 b1
69	67, 68	tr 62	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 a1 b1 a1 a0 a0 a1 a1 b1
70		leor 159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 a0
71	70	ler 149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 a0 a1
72	71	mldual2i 1125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 a0 a1 a1 b1 a0 a1 a1 b1
73		ancom 74	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 a0 a1 a1 b1 a1 b1 a0 a1
74		leo 158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 a1 a1 b1
75	74	mldual2i 1125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 a1 b1 a0 a1 a1 b1 a0 a1
76	73, 75	tr 62	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 a0 a1 a1 b1 a1 b1 a0 a1
77	76	ror 71	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 a0 a1 a1 b1 a1 b1 a0 a1
78	69, 72, 77	3tr 65	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 a1 b1 a1 a0 a1 b1 a0 a1
79		orass 75	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 a1 b1 a0 a1 a1 b1 a0 a1
80		orcom 73	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 a1 b1 a0 a1 a1 a1 b1 a0
81	78, 79, 80	3tr 65	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 a1 b1 a1 a0 a1 a1 b1 a0
82		leo 158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 a1 a1 a0 a1 b1 a0 b1 a1 b1 b1
83		ancom 74	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 a0 a1 b1 a1 b1 a0
84	83	cm 61	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 a1 b1 a0 a0 a1 b1
85		3dp.e	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 b0 a0 p0
86	85, 29	tr 62	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 b0 a0 a1 b1 a1 b1
87	86	lor 70	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 a0 a0 b0 a0 a1 b1 a1 b1
88	87	ran 78	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 a0 a1 b1 a0 b0 a0 a1 b1 a1 b1 a1 b1
89		le1 146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 b0
90	89	leran 153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 b0 a0 a1 b1 a1 b1 a0 a1 b1 a1 b1
91	90	lelor 166	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 a0 b0 a0 a1 b1 a1 b1 a0 a0 a1 b1 a1 b1
92	91	leran 153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 a0 b0 a0 a1 b1 a1 b1 a1 b1 a0 a0 a1 b1 a1 b1 a1 b1
93		an1r 107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 a0 a1 b1 a1 b1 a0 a1 b1 a1 b1
94	93	lor 70	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 a0 a0 a1 b1 a1 b1 a0 a0 a1 b1 a1 b1
95		orass 75	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 a0 a0 a1 b1 a1 b1 a0 a0 a1 b1 a1 b1
96	95	cm 61	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 a0 a0 a1 b1 a1 b1 a0 a0 a1 b1 a1 b1
97		oridm 110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 a0 a0 a0
98	97	ror 71	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 a0 a0 a1 b1 a1 b1 a0 a1 b1 a1 b1
99		orcom 73	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 a0 a1 b1 a1 b1 a1 b1 a1 b1 a0
100	98, 99	tr 62	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 a0 a0 a1 b1 a1 b1 a1 b1 a1 b1 a0
101	94, 96, 100	3tr 65	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 a0 a0 a1 b1 a1 b1 a1 b1 a1 b1 a0
102	101	ran 78	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 a0 a0 a1 b1 a1 b1 a1 b1 a1 b1 a1 b1 a0 a1 b1
103	31	mlduali 1126	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 a1 b1 a1 b1 a0 a1 b1 a1 b1 a1 b1 a0 a1 b1
104	102, 103	tr 62	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 a0 a0 a1 b1 a1 b1 a1 b1 a1 b1 a1 b1 a0 a1 b1
105		lear 161	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 a1 b1 a1 b1 a1 b1
106	105	leror 152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 a1 b1 a1 b1 a0 a1 b1 a1 b1 a0 a1 b1
107	104, 106	bltr 138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 a0 a0 a1 b1 a1 b1 a1 b1 a1 b1 a0 a1 b1
108		or32 82	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 a1 b1 a0 a1 b1 a1 a0 a1 b1 b1
109		3dp.d	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 a1 a0 a1 b1
110	109	ror 71	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 b1 a1 a0 a1 b1 b1
111	110	cm 61	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 a1 a0 a1 b1 b1 b1
112	108, 111	tr 62	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 a1 b1 a0 a1 b1 b1
113	107, 112	lbtr 139	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 a0 a0 a1 b1 a1 b1 a1 b1 b1
114	92, 113	letr 137	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 a0 b0 a0 a1 b1 a1 b1 a1 b1 b1
115	88, 114	bltr 138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 a0 a1 b1 b1
116	84, 115	bltr 138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 a1 b1 a0 b1
117	116	df2le2 136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 a1 b1 a0 b1 a1 b1 a0
118	117	cm 61	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 a1 b1 a0 a1 b1 a0 b1
119		id 59	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 a1 b1 a0 b1 a1 b1 a0 b1
120	119	cm 61	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 a1 b1 a0 b1 a1 b1 a0 b1
121	118, 120	tr 62	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 a1 b1 a0 a1 b1 a0 b1
122		id 59	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 a0 b1 a0 b1
123		id 59	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 a1 b1 b1 a1 b1 b1
124		orcom 73	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 a0 a1 a1 a0
125		orcom 73	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 b1 b1
126	124, 125	2an 79	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 a0 a1 b1 a1 a0 b1
127	122, 123, 126, 119	dp34 1179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 a1 b1 a0 b1 a1 a0 a1 b1 a0 b1 a1 b1 b1
128	121, 127	bltr 138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 a1 b1 a0 a1 a0 a1 b1 a0 b1 a1 b1 b1
129	82, 128	lel2or 170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 a1 a1 b1 a0 a1 a0 a1 b1 a0 b1 a1 b1 b1
130	81, 129	bltr 138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 a1 b1 a1 a0 a1 a0 a1 b1 a0 b1 a1 b1 b1
131	130	lelan 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 a0 a1 b1 a1 b1 a1 a0 a0 a1 b1 a1 a0 a1 b1 a0 b1 a1 b1 b1
132	60, 131	bltr 138	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 a0 a1 b1 a1 b1 a1 a0 a0 a1 b1 a1 a0 a1 b1 a0 b1 a1 b1 b1
133	62, 132	bltr 138	. . . . . . . . . . . . . . . . . . . . . . . . . 26 a0 a1 b1 a0 a1 b1 a1 a0 a1 b1 a0 b1 a1 b1 b1
134		mldual 1122	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 a0 a1 b1 a1 a0 a1 b1 a0 b1 a1 b1 b1 a0 a1 b1 a1 a0 a1 b1 a0 b1 a1 b1 b1
135		ancom 74	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 a0 a1 b1 a0 b1 a1 b1 b1 a0 b1 a1 b1 b1 a0 a1 b1
136	135	lor 70	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 a0 a1 b1 a1 a0 a1 b1 a0 b1 a1 b1 b1 a0 a1 b1 a1 a0 b1 a1 b1 b1 a0 a1 b1
137		lea 160	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 a0 a1 b1 a1 a0 a1 b1
138	137	ml2i 1123	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 a0 a1 b1 a1 a0 b1 a1 b1 b1 a0 a1 b1 a0 a1 b1 a1 a0 b1 a1 b1 b1 a0 a1 b1
139		ancom 74	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 a0 a1 b1 a1 a0 b1 a1 b1 b1 a0 a1 b1 a0 a1 b1 a0 a1 b1 a1 a0 b1 a1 b1 b1
140		ax-a2 31	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 a0 a1 b1 a1 a0 b1 a1 b1 b1 a0 b1 a1 b1 b1 a0 a1 b1 a1
141	140	lan 77	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 a0 a1 b1 a0 a1 b1 a1 a0 b1 a1 b1 b1 a0 a1 b1 a0 b1 a1 b1 b1 a0 a1 b1 a1
142	138, 139, 141	3tr 65	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 a0 a1 b1 a1 a0 b1 a1 b1 b1 a0 a1 b1 a0 a1 b1 a0 b1 a1 b1 b1 a0 a1 b1 a1
143	134, 136, 142	3tr 65	. . . . . . . . . . . . . . . . . . . . . . . . . 26 a0 a1 b1 a1 a0 a1 b1 a0 b1 a1 b1 b1 a0 a1 b1 a0 b1 a1 b1 b1 a0 a1 b1 a1
144	133, 143	lbtr 139	. . . . . . . . . . . . . . . . . . . . . . . . 25 a0 a1 b1 a0 a1 b1 a0 b1 a1 b1 b1 a0 a1 b1 a1
145		mldual 1122	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 a0 a1 b1 a0 b1 a1 b1 b1 a0 a1 b1 a1 a0 a1 b1 a0 b1 a1 b1 b1 a0 a1 b1 a1
146	50	ran 78	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 a0 a1 b1 a1 a1 a0 b1 a1
147		anass 76	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 a1 a0 b1 a1 a1 a0 b1 a1
148		leor 159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 b1
149	148	mldual2i 1125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 b1 a1 b1 a1
150		orcom 73	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 b1 a1 b1 a1
151		ancom 74	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 b1 a1 a1 b1
152	151	lor 70	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 b1 a1 a1 b1
153	149, 150, 152	3tr 65	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 b1 a1 a1 b1
154	153	lan 77	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 a1 a0 b1 a1 a1 a0 a1 b1
155		leao1 162	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 a1 b1 a1 a0
156	155	mldual2i 1125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 a1 a0 a1 b1 a1 a0 a1 b1
157		orcom 73	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 a1 a0 a1 b1 a1 b1 a1 a0
158		ancom 74	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 a1 a0 a1 a0
159	158	lor 70	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 a1 b1 a1 a0 a1 b1 a1 a0
160	157, 159	tr 62	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 a1 a0 a1 b1 a1 b1 a1 a0
161	154, 156, 160	3tr 65	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 a1 a0 b1 a1 a1 b1 a1 a0
162	146, 147, 161	3tr 65	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 a0 a1 b1 a1 a1 b1 a1 a0
163	162	lor 70	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 a0 a1 b1 a0 b1 a1 b1 b1 a0 a1 b1 a1 a0 a1 b1 a0 b1 a1 b1 b1 a1 b1 a1 a0
164	145, 163	tr 62	. . . . . . . . . . . . . . . . . . . . . . . . . 26 a0 a1 b1 a0 b1 a1 b1 b1 a0 a1 b1 a1 a0 a1 b1 a0 b1 a1 b1 b1 a1 b1 a1 a0
165		lear 161	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 a0 a1 b1 a0 b1 a1 b1 b1 a0 b1 a1 b1 b1
166	165	leror 152	. . . . . . . . . . . . . . . . . . . . . . . . . 26 a0 a1 b1 a0 b1 a1 b1 b1 a1 b1 a1 a0 a0 b1 a1 b1 b1 a1 b1 a1 a0
167	164, 166	bltr 138	. . . . . . . . . . . . . . . . . . . . . . . . 25 a0 a1 b1 a0 b1 a1 b1 b1 a0 a1 b1 a1 a0 b1 a1 b1 b1 a1 b1 a1 a0
168	144, 167	letr 137	. . . . . . . . . . . . . . . . . . . . . . . 24 a0 a1 b1 a0 b1 a1 b1 b1 a1 b1 a1 a0
169		orcom 73	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 a1 b1 a1 a0 a1 a0 a1 b1
170	169	lor 70	. . . . . . . . . . . . . . . . . . . . . . . . . 26 a0 b1 a1 b1 b1 a1 b1 a1 a0 a0 b1 a1 b1 b1 a1 a0 a1 b1
171		or4 84	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 a0 b1 a1 b1 b1 a1 a0 a1 b1 a0 b1 a1 a0 a1 b1 b1 a1 b1
172		ancom 74	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 a0 b1 b1 a0
173	122, 172	tr 62	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 a0 b1 b1 a0
174	173	ror 71	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 a0 b1 a1 a0 b1 a0 a1 a0
175	123	ror 71	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 a1 b1 b1 a1 b1 a1 b1 b1 a1 b1
176	174, 175	2or 72	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 a0 b1 a1 a0 a1 b1 b1 a1 b1 b1 a0 a1 a0 a1 b1 b1 a1 b1
177	171, 176	tr 62	. . . . . . . . . . . . . . . . . . . . . . . . . 26 a0 b1 a1 b1 b1 a1 a0 a1 b1 b1 a0 a1 a0 a1 b1 b1 a1 b1
178		leao1 162	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 a1 a0 b1
179	178	mli 1124	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 b1 a0 a1 a0 b1 a0 a1 a0
180		leao1 162	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 a1 b1 a1
181	180	mli 1124	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 a1 b1 b1 a1 b1 a1 b1 b1 a1 b1
182	179, 181	2or 72	. . . . . . . . . . . . . . . . . . . . . . . . . 26 b1 a0 a1 a0 a1 b1 b1 a1 b1 b1 a0 a1 a0 a1 b1 b1 a1 b1
183	170, 177, 182	3tr 65	. . . . . . . . . . . . . . . . . . . . . . . . 25 a0 b1 a1 b1 b1 a1 b1 a1 a0 b1 a0 a1 a0 a1 b1 b1 a1 b1
184		or32 82	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 a0 a1 a0 a0 a1 a0
185		ml3 1128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 a0 a1 a0 a0 a1 a0
186		orcom 73	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 a0 a0
187	186	lan 77	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 a1 a0 a1 a0
188	187	lor 70	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 a0 a1 a0 a0 a1 a0
189	185, 188	tr 62	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 a0 a1 a0 a0 a1 a0
190	189	ror 71	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 a0 a1 a0 a0 a1 a0
191		or32 82	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 a0 a1 a0 a0 a1 a0
192	184, 190, 191	3tr 65	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 a0 a1 a0 a0 a1 a0
193	192	lan 77	. . . . . . . . . . . . . . . . . . . . . . . . . 26 b1 a0 a1 a0 b1 a0 a1 a0
194		or32 82	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 b1 b1 a1 b1 b1 a1 b1 b1
195		orcom 73	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 b1 b1
196	195	lan 77	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 a1 b1 a1 b1
197	196	lor 70	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 b1 a1 b1 b1 a1 b1
198		ml3 1128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 b1 a1 b1 b1 a1 b1
199	197, 198	tr 62	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 b1 a1 b1 b1 a1 b1
200	199	ror 71	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 b1 a1 b1 b1 b1 a1 b1 b1
201		or32 82	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 b1 a1 b1 b1 b1 b1 a1 b1
202	194, 200, 201	3tr 65	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 b1 b1 a1 b1 b1 b1 a1 b1
203	202	lan 77	. . . . . . . . . . . . . . . . . . . . . . . . . 26 a1 b1 b1 a1 b1 a1 b1 b1 a1 b1
204	193, 203	2or 72	. . . . . . . . . . . . . . . . . . . . . . . . 25 b1 a0 a1 a0 a1 b1 b1 a1 b1 b1 a0 a1 a0 a1 b1 b1 a1 b1
205	183, 204	tr 62	. . . . . . . . . . . . . . . . . . . . . . . 24 a0 b1 a1 b1 b1 a1 b1 a1 a0 b1 a0 a1 a0 a1 b1 b1 a1 b1
206	168, 205	lbtr 139	. . . . . . . . . . . . . . . . . . . . . . 23 a0 a1 b1 b1 a0 a1 a0 a1 b1 b1 a1 b1
207		lea 160	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 a1 a0 a1
208	74	leran 153	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 a1 a0 a1 b1 a0
209	208, 116	letr 137	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 a1 a0 b1
210	207, 209	ler2an 173	. . . . . . . . . . . . . . . . . . . . . . . . . 26 a1 a0 a1 b1
211	210	lelor 166	. . . . . . . . . . . . . . . . . . . . . . . . 25 a0 a1 a0 a0 a1 b1
212	211	lelan 167	. . . . . . . . . . . . . . . . . . . . . . . 24 b1 a0 a1 a0 b1 a0 a1 b1
213		lea 160	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 a1 b1
214		lear 161	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 a1 b1 a1 b1
215		leao3 164	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 a1 b1 a0
216	214, 215	ler2an 173	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 a1 b1 a1 b1 a0
217	216, 116	letr 137	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 a1 b1 b1
218	213, 217	ler2an 173	. . . . . . . . . . . . . . . . . . . . . . . . . 26 a1 b1 b1
219	218	lelor 166	. . . . . . . . . . . . . . . . . . . . . . . . 25 b1 b1 a1 b1 b1 b1 b1
220	219	lelan 167	. . . . . . . . . . . . . . . . . . . . . . . 24 a1 b1 b1 a1 b1 a1 b1 b1 b1
221	212, 220	le2or 168	. . . . . . . . . . . . . . . . . . . . . . 23 b1 a0 a1 a0 a1 b1 b1 a1 b1 b1 a0 a1 b1 a1 b1 b1 b1
222	206, 221	letr 137	. . . . . . . . . . . . . . . . . . . . . 22 a0 a1 b1 b1 a0 a1 b1 a1 b1 b1 b1
223		ax-a2 31	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 b1 b1
224	223	lan 77	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 a1 b1 a1 b1
225	224	lor 70	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 a1 b1 a1 b1
226		ml3 1128	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 a1 b1 b1 a1
227	225, 226	tr 62	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 a1 b1 b1 a1
228	227	lor 70	. . . . . . . . . . . . . . . . . . . . . . . . . 26 a0 a1 b1 a0 b1 a1
229		orass 75	. . . . . . . . . . . . . . . . . . . . . . . . . 26 a0 a1 b1 a0 a1 b1
230		orass 75	. . . . . . . . . . . . . . . . . . . . . . . . . 26 a0 b1 a1 a0 b1 a1
231	228, 229, 230	3tr1 63	. . . . . . . . . . . . . . . . . . . . . . . . 25 a0 a1 b1 a0 b1 a1
232	231	lan 77	. . . . . . . . . . . . . . . . . . . . . . . 24 b1 a0 a1 b1 b1 a0 b1 a1
233		ml3 1128	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 b1 b1 b1 b1
234	233	lor 70	. . . . . . . . . . . . . . . . . . . . . . . . . 26 b1 b1 b1 b1 b1 b1
235		orass 75	. . . . . . . . . . . . . . . . . . . . . . . . . 26 b1 b1 b1 b1 b1 b1
236		orass 75	. . . . . . . . . . . . . . . . . . . . . . . . . 26 b1 b1 b1 b1 b1 b1
237	234, 235, 236	3tr1 63	. . . . . . . . . . . . . . . . . . . . . . . . 25 b1 b1 b1 b1 b1 b1
238	237	lan 77	. . . . . . . . . . . . . . . . . . . . . . . 24 a1 b1 b1 b1 a1 b1 b1 b1
239	232, 238	2or 72	. . . . . . . . . . . . . . . . . . . . . . 23 b1 a0 a1 b1 a1 b1 b1 b1 b1 a0 b1 a1 a1 b1 b1 b1
240		leao3 164	. . . . . . . . . . . . . . . . . . . . . . . . . 26 b1 a1 b1
241	240	mldual2i 1125	. . . . . . . . . . . . . . . . . . . . . . . . 25 b1 a0 b1 a1 b1 a0 b1 a1
242	173	ror 71	. . . . . . . . . . . . . . . . . . . . . . . . . 26 a0 b1 b1 a1 b1 a0 b1 a1
243	242	cm 61	. . . . . . . . . . . . . . . . . . . . . . . . 25 b1 a0 b1 a1 a0 b1 b1 a1
244	241, 243	tr 62	. . . . . . . . . . . . . . . . . . . . . . . 24 b1 a0 b1 a1 a0 b1 b1 a1
245		leao3 164	. . . . . . . . . . . . . . . . . . . . . . . . . 26 b1 a1
246	245	mldual2i 1125	. . . . . . . . . . . . . . . . . . . . . . . . 25 a1 b1 b1 b1 a1 b1 b1 b1
247	123	ror 71	. . . . . . . . . . . . . . . . . . . . . . . . . 26 a1 b1 b1 b1 a1 b1 b1 b1
248	247	cm 61	. . . . . . . . . . . . . . . . . . . . . . . . 25 a1 b1 b1 b1 a1 b1 b1 b1
249	246, 248	tr 62	. . . . . . . . . . . . . . . . . . . . . . . 24 a1 b1 b1 b1 a1 b1 b1 b1
250	244, 249	2or 72	. . . . . . . . . . . . . . . . . . . . . . 23 b1 a0 b1 a1 a1 b1 b1 b1 a0 b1 b1 a1 a1 b1 b1 b1
251		or4 84	. . . . . . . . . . . . . . . . . . . . . . . 24 a0 b1 b1 a1 a1 b1 b1 b1 a0 b1 a1 b1 b1 b1 a1 b1
252		orcom 73	. . . . . . . . . . . . . . . . . . . . . . . 24 a0 b1 a1 b1 b1 b1 a1 b1 b1 a1 b1 a0 b1 a1 b1 b1
253		ancom 74	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 b1 a1 a1 b1
254		leor 159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 b1 b1 b1
255	254	lelan 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 a1 b1 a1 b1 b1
256	253, 255	bltr 138	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 b1 a1 a1 b1 b1
257		leor 159	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 a0
258	257	leran 153	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 b1 a0 b1
259	256, 258	le2or 168	. . . . . . . . . . . . . . . . . . . . . . . . . 26 b1 a1 b1 a1 b1 b1 a0 b1
260	123, 122	2or 72	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 a1 b1 b1 a0 b1 a1 b1 b1 a0 b1
261	260	cm 61	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 a1 b1 b1 a0 b1 a1 b1 b1 a0 b1
262		orcom 73	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 a1 b1 b1 a0 b1 a0 b1 a1 b1 b1
263	261, 262	tr 62	. . . . . . . . . . . . . . . . . . . . . . . . . 26 a1 b1 b1 a0 b1 a0 b1 a1 b1 b1
264	259, 263	lbtr 139	. . . . . . . . . . . . . . . . . . . . . . . . 25 b1 a1 b1 a0 b1 a1 b1 b1
265	264	df-le2 131	. . . . . . . . . . . . . . . . . . . . . . . 24 b1 a1 b1 a0 b1 a1 b1 b1 a0 b1 a1 b1 b1
266	251, 252, 265	3tr 65	. . . . . . . . . . . . . . . . . . . . . . 23 a0 b1 b1 a1 a1 b1 b1 b1 a0 b1 a1 b1 b1
267	239, 250, 266	3tr 65	. . . . . . . . . . . . . . . . . . . . . 22 b1 a0 a1 b1 a1 b1 b1 b1 a0 b1 a1 b1 b1
268	222, 267	lbtr 139	. . . . . . . . . . . . . . . . . . . . 21 a0 a1 b1 a0 b1 a1 b1 b1
269	85	ror 71	. . . . . . . . . . . . . . . . . . . . . 22 b1 b0 a0 p0 b1
270	269	lan 77	. . . . . . . . . . . . . . . . . . . . 21 a0 a1 b1 a0 a1 b0 a0 p0 b1
271	109	lor 70	. . . . . . . . . . . . . . . . . . . . . . 23 a0 a0 a1 a0 a1 b1
272	271, 269	2an 79	. . . . . . . . . . . . . . . . . . . . . 22 a0 b1 a0 a1 a0 a1 b1 b0 a0 p0 b1
273	109	lor 70	. . . . . . . . . . . . . . . . . . . . . . 23 a1 a1 a1 a0 a1 b1
274	273	ran 78	. . . . . . . . . . . . . . . . . . . . . 22 a1 b1 b1 a1 a1 a0 a1 b1 b1 b1
275	272, 274	2or 72	. . . . . . . . . . . . . . . . . . . . 21 a0 b1 a1 b1 b1 a0 a1 a0 a1 b1 b0 a0 p0 b1 a1 a1 a0 a1 b1 b1 b1
276	268, 270, 275	le3tr2 141	. . . . . . . . . . . . . . . . . . . 20 a0 a1 b0 a0 p0 b1 a0 a1 a0 a1 b1 b0 a0 p0 b1 a1 a1 a0 a1 b1 b1 b1
277		or12 80	. . . . . . . . . . . . . . . . . . . . . . 23 a0 a1 a0 a1 b1 a1 a0 a0 a1 b1
278		orabs 120	. . . . . . . . . . . . . . . . . . . . . . . 24 a0 a0 a1 b1 a0
279	278	lor 70	. . . . . . . . . . . . . . . . . . . . . . 23 a1 a0 a0 a1 b1 a1 a0
280		orcom 73	. . . . . . . . . . . . . . . . . . . . . . 23 a1 a0 a0 a1
281	277, 279, 280	3tr 65	. . . . . . . . . . . . . . . . . . . . . 22 a0 a1 a0 a1 b1 a0 a1
282	281	ran 78	. . . . . . . . . . . . . . . . . . . . 21 a0 a1 a0 a1 b1 b0 a0 p0 b1 a0 a1 b0 a0 p0 b1
283		orass 75	. . . . . . . . . . . . . . . . . . . . . . 23 a1 a1 a0 a1 b1 a1 a1 a0 a1 b1
284	283	ran 78	. . . . . . . . . . . . . . . . . . . . . 22 a1 a1 a0 a1 b1 b1 b1 a1 a1 a0 a1 b1 b1 b1
285	284	cm 61	. . . . . . . . . . . . . . . . . . . . 21 a1 a1 a0 a1 b1 b1 b1 a1 a1 a0 a1 b1 b1 b1
286	282, 285	2or 72	. . . . . . . . . . . . . . . . . . . 20 a0 a1 a0 a1 b1 b0 a0 p0 b1 a1 a1 a0 a1 b1 b1 b1 a0 a1 b0 a0 p0 b1 a1 a1 a0 a1 b1 b1 b1
287	276, 286	lbtr 139	. . . . . . . . . . . . . . . . . . 19 a0 a1 b0 a0 p0 b1 a0 a1 b0 a0 p0 b1 a1 a1 a0 a1 b1 b1 b1
288		ax-a2 31	. . . . . . . . . . . . . . . . . . . . . . . . 25 a1 a1 a1 a1
289		ax-a2 31	. . . . . . . . . . . . . . . . . . . . . . . . . 26 a1 b1 b1 a1
290	289	lan 77	. . . . . . . . . . . . . . . . . . . . . . . . 25 a0 a1 b1 a0 b1 a1
291	288, 290	2or 72	. . . . . . . . . . . . . . . . . . . . . . . 24 a1 a1 a0 a1 b1 a1 a1 a0 b1 a1
292		orass 75	. . . . . . . . . . . . . . . . . . . . . . . 24 a1 a1 a0 b1 a1 a1 a1 a0 b1 a1
293	291, 292	tr 62	. . . . . . . . . . . . . . . . . . . . . . 23 a1 a1 a0 a1 b1 a1 a1 a0 b1 a1
294		ml3le 1127	. . . . . . . . . . . . . . . . . . . . . . . 24 a1 a0 b1 a1 a1 b1 a0 a1
295	294	lelor 166	. . . . . . . . . . . . . . . . . . . . . . 23 a1 a1 a0 b1 a1 a1 a1 b1 a0 a1
296	293, 295	bltr 138	. . . . . . . . . . . . . . . . . . . . . 22 a1 a1 a0 a1 b1 a1 a1 b1 a0 a1
297		orass 75	. . . . . . . . . . . . . . . . . . . . . . . 24 a1 a1 b1 a0 a1 a1 a1 b1 a0 a1
298	297	cm 61	. . . . . . . . . . . . . . . . . . . . . . 23 a1 a1 b1 a0 a1 a1 a1 b1 a0 a1
299	288	ror 71	. . . . . . . . . . . . . . . . . . . . . . 23 a1 a1 b1 a0 a1 a1 a1 b1 a0 a1
300	298, 299	tr 62	. . . . . . . . . . . . . . . . . . . . . 22 a1 a1 b1 a0 a1 a1 a1 b1 a0 a1
301	296, 300	lbtr 139	. . . . . . . . . . . . . . . . . . . . 21 a1 a1 a0 a1 b1 a1 a1 b1 a0 a1
302	301	leran 153	. . . . . . . . . . . . . . . . . . . 20 a1 a1 a0 a1 b1 b1 b1 a1 a1 b1 a0 a1 b1 b1
303	302	lelor 166	. . . . . . . . . . . . . . . . . . 19 a0 a1 b0 a0 p0 b1 a1 a1 a0 a1 b1 b1 b1 a0 a1 b0 a0 p0 b1 a1 a1 b1 a0 a1 b1 b1
304	287, 303	letr 137	. . . . . . . . . . . . . . . . . 18 a0 a1 b0 a0 p0 b1 a0 a1 b0 a0 p0 b1 a1 a1 b1 a0 a1 b1 b1
305	24	leror 152	. . . . . . . . . . . . . . . . . . . . 21 b0 a0 p0 b1 b0 b1
306	305	lelan 167	. . . . . . . . . . . . . . . . . . . 20 a0 a1 b0 a0 p0 b1 a0 a1 b0 b1
307		leao1 162	. . . . . . . . . . . . . . . . . . . . . . 23 b1 a0 a1 b1 b1
308	307	mldual2i 1125	. . . . . . . . . . . . . . . . . . . . . 22 b1 b1 a1 a1 b1 a0 a1 b1 b1 a1 a1 b1 a0 a1
309		ancom 74	. . . . . . . . . . . . . . . . . . . . . 22 b1 b1 a1 a1 b1 a0 a1 a1 a1 b1 a0 a1 b1 b1
310		ancom 74	. . . . . . . . . . . . . . . . . . . . . . 23 b1 b1 a1 a1 a1 a1 b1 b1
311	310	ror 71	. . . . . . . . . . . . . . . . . . . . . 22 b1 b1 a1 a1 b1 a0 a1 a1 a1 b1 b1 b1 a0 a1
312	308, 309, 311	3tr2 64	. . . . . . . . . . . . . . . . . . . . 21 a1 a1 b1 a0 a1 b1 b1 a1 a1 b1 b1 b1 a0 a1
313	312	bile 142	. . . . . . . . . . . . . . . . . . . 20 a1 a1 b1 a0 a1 b1 b1 a1 a1 b1 b1 b1 a0 a1
314	306, 313	le2or 168	. . . . . . . . . . . . . . . . . . 19 a0 a1 b0 a0 p0 b1 a1 a1 b1 a0 a1 b1 b1 a0 a1 b0 b1 a1 a1 b1 b1 b1 a0 a1
315		or12 80	. . . . . . . . . . . . . . . . . . 19 a0 a1 b0 b1 a1 a1 b1 b1 b1 a0 a1 a1 a1 b1 b1 a0 a1 b0 b1 b1 a0 a1
316	314, 315	lbtr 139	. . . . . . . . . . . . . . . . . 18 a0 a1 b0 a0 p0 b1 a1 a1 b1 a0 a1 b1 b1 a1 a1 b1 b1 a0 a1 b0 b1 b1 a0 a1
317	304, 316	letr 137	. . . . . . . . . . . . . . . . 17 a0 a1 b0 a0 p0 b1 a1 a1 b1 b1 a0 a1 b0 b1 b1 a0 a1
318		3dp.c0	. . . . . . . . . . . . . . . . . . . 20 c0 a1 a1 b1 b1
319		3dp.c1	. . . . . . . . . . . . . . . . . . . . 21 c1 a0 a1 b0 b1
320	319	ror 71	. . . . . . . . . . . . . . . . . . . 20 c1 b1 a0 a1 a0 a1 b0 b1 b1 a0 a1
321	318, 320	2or 72	. . . . . . . . . . . . . . . . . . 19 c0 c1 b1 a0 a1 a1 a1 b1 b1 a0 a1 b0 b1 b1 a0 a1
322	321	cm 61	. . . . . . . . . . . . . . . . . 18 a1 a1 b1 b1 a0 a1 b0 b1 b1 a0 a1 c0 c1 b1 a0 a1
323		orass 75	. . . . . . . . . . . . . . . . . . 19 c0 c1 b1 a0 a1 c0 c1 b1 a0 a1
324	323	cm 61	. . . . . . . . . . . . . . . . . 18 c0 c1 b1 a0 a1 c0 c1 b1 a0 a1
325	322, 324	tr 62	. . . . . . . . . . . . . . . . 17 a1 a1 b1 b1 a0 a1 b0 b1 b1 a0 a1 c0 c1 b1 a0 a1
326	317, 325	lbtr 139	. . . . . . . . . . . . . . . 16 a0 a1 b0 a0 p0 b1 c0 c1 b1 a0 a1
327	47, 326	ler2an 173	. . . . . . . . . . . . . . 15 a0 a1 b0 a0 p0 b1 a0 a1 c0 c1 b1 a0 a1
328		lear 161	. . . . . . . . . . . . . . . 16 b1 a0 a1 a0 a1
329	328	mldual2i 1125	. . . . . . . . . . . . . . 15 a0 a1 c0 c1 b1 a0 a1 a0 a1 c0 c1 b1 a0 a1
330	327, 329	lbtr 139	. . . . . . . . . . . . . 14 a0 a1 b0 a0 p0 b1 a0 a1 c0 c1 b1 a0 a1
331		lea 160	. . . . . . . . . . . . . . 15 b1 a0 a1 b1
332	331	lelor 166	. . . . . . . . . . . . . 14 a0 a1 c0 c1 b1 a0 a1 a0 a1 c0 c1 b1
333	330, 332	letr 137	. . . . . . . . . . . . 13 a0 a1 b0 a0 p0 b1 a0 a1 c0 c1 b1
334		orcom 73	. . . . . . . . . . . . 13 a0 a1 c0 c1 b1 b1 a0 a1 c0 c1
335	333, 334	lbtr 139	. . . . . . . . . . . 12 a0 a1 b0 a0 p0 b1 b1 a0 a1 c0 c1
336		leid 148	. . . . . . . . . . . 12 b1 a0 a1 c0 c1 b1 a0 a1 c0 c1
337	335, 336	lel2or 170	. . . . . . . . . . 11 a0 a1 b0 a0 p0 b1 b1 a0 a1 c0 c1 b1 a0 a1 c0 c1
338	46, 337	letr 137	. . . . . . . . . 10 b0 a0 p0 b1 a0 a1 c0 c1
339	26, 338	lel2or 170	. . . . . . . . 9 b1 b0 a0 p0 b1 a0 a1 c0 c1
340	25, 339	letr 137	. . . . . . . 8 b0 a0 p0 b1 a0 a1 c0 c1
341	24, 340	ler2an 173	. . . . . . 7 b0 a0 p0 b0 b1 a0 a1 c0 c1
342		or32 82	. . . . . . . . . . 11 a0 b0 b1 c2 c0 c1 a0 b0 c2 c0 c1 b1
343		orcom 73	. . . . . . . . . . 11 a0 b0 c2 c0 c1 b1 b1 a0 b0 c2 c0 c1
344		leo 158	. . . . . . . . . . . . . . . 16 a0 a0 a1
345		leo 158	. . . . . . . . . . . . . . . 16 b0 b0 b1
346	344, 345	le2an 169	. . . . . . . . . . . . . . 15 a0 b0 a0 a1 b0 b1
347		3dp.c2	. . . . . . . . . . . . . . . 16 c2 a0 a1 b0 b1
348	347	cm 61	. . . . . . . . . . . . . . 15 a0 a1 b0 b1 c2
349	346, 348	lbtr 139	. . . . . . . . . . . . . 14 a0 b0 c2
350	319	cm 61	. . . . . . . . . . . . . . . 16 a0 a1 b0 b1 c1
351	346, 350	lbtr 139	. . . . . . . . . . . . . . 15 a0 b0 c1
352	351	lerr 150	. . . . . . . . . . . . . 14 a0 b0 c0 c1
353	349, 352	ler2an 173	. . . . . . . . . . . . 13 a0 b0 c2 c0 c1
354	353	df-le2 131	. . . . . . . . . . . 12 a0 b0 c2 c0 c1 c2 c0 c1
355	354	lor 70	. . . . . . . . . . 11 b1 a0 b0 c2 c0 c1 b1 c2 c0 c1
356	342, 343, 355	3tr 65	. . . . . . . . . 10 a0 b0 b1 c2 c0 c1 b1 c2 c0 c1
357	356	lan 77	. . . . . . . . 9 b0 a0 b0 b1 c2 c0 c1 b0 b1 c2 c0 c1
358	347	ran 78	. . . . . . . . . . . . . 14 c2 c0 c1 a0 a1 b0 b1 c0 c1
359		an32 83	. . . . . . . . . . . . . 14 a0 a1 b0 b1 c0 c1 a0 a1 c0 c1 b0 b1
360	358, 359	tr 62	. . . . . . . . . . . . 13 c2 c0 c1 a0 a1 c0 c1 b0 b1
361	360	lor 70	. . . . . . . . . . . 12 b1 c2 c0 c1 b1 a0 a1 c0 c1 b0 b1
362		leor 159	. . . . . . . . . . . . 13 b1 b0 b1
363	362	ml2i 1123	. . . . . . . . . . . 12 b1 a0 a1 c0 c1 b0 b1 b1 a0 a1 c0 c1 b0 b1
364		ancom 74	. . . . . . . . . . . 12 b1 a0 a1 c0 c1 b0 b1 b0 b1 b1 a0 a1 c0 c1
365	361, 363, 364	3tr 65	. . . . . . . . . . 11 b1 c2 c0 c1 b0 b1 b1 a0 a1 c0 c1
366	365	lan 77	. . . . . . . . . 10 b0 b1 c2 c0 c1 b0 b0 b1 b1 a0 a1 c0 c1
367		anass 76	. . . . . . . . . . 11 b0 b0 b1 b1 a0 a1 c0 c1 b0 b0 b1 b1 a0 a1 c0 c1
368	367	cm 61	. . . . . . . . . 10 b0 b0 b1 b1 a0 a1 c0 c1 b0 b0 b1 b1 a0 a1 c0 c1
369		anabs 121	. . . . . . . . . . 11 b0 b0 b1 b0
370	369	ran 78	. . . . . . . . . 10 b0 b0 b1 b1 a0 a1 c0 c1 b0 b1 a0 a1 c0 c1
371	366, 368, 370	3tr 65	. . . . . . . . 9 b0 b1 c2 c0 c1 b0 b1 a0 a1 c0 c1
372	357, 371	tr 62	. . . . . . . 8 b0 a0 b0 b1 c2 c0 c1 b0 b1 a0 a1 c0 c1
373	372	cm 61	. . . . . . 7 b0 b1 a0 a1 c0 c1 b0 a0 b0 b1 c2 c0 c1
374	341, 373	lbtr 139	. . . . . 6 b0 a0 p0 b0 a0 b0 b1 c2 c0 c1
375		orass 75	. . . . . . . . . 10 a0 b0 b1 c2 c0 c1 a0 b0 b1 c2 c0 c1
376		orcom 73	. . . . . . . . . 10 a0 b0 b1 c2 c0 c1 b1 c2 c0 c1 a0 b0
377	375, 376	tr 62	. . . . . . . . 9 a0 b0 b1 c2 c0 c1 b1 c2 c0 c1 a0 b0
378	377	lan 77	. . . . . . . 8 b0 a0 b0 b1 c2 c0 c1 b0 b1 c2 c0 c1 a0 b0
379		lear 161	. . . . . . . . 9 a0 b0 b0
380	379	mldual2i 1125	. . . . . . . 8 b0 b1 c2 c0 c1 a0 b0 b0 b1 c2 c0 c1 a0 b0
381		orcom 73	. . . . . . . 8 b0 b1 c2 c0 c1 a0 b0 a0 b0 b0 b1 c2 c0 c1
382	378, 380, 381	3tr 65	. . . . . . 7 b0 a0 b0 b1 c2 c0 c1 a0 b0 b0 b1 c2 c0 c1
383		lea 160	. . . . . . . 8 a0 b0 a0
384	383	leror 152	. . . . . . 7 a0 b0 b0 b1 c2 c0 c1 a0 b0 b1 c2 c0 c1
385	382, 384	bltr 138	. . . . . 6 b0 a0 b0 b1 c2 c0 c1 a0 b0 b1 c2 c0 c1
386	374, 385	letr 137	. . . . 5 b0 a0 p0 a0 b0 b1 c2 c0 c1
387	386	df-le2 131	. . . 4 b0 a0 p0 a0 b0 b1 c2 c0 c1 a0 b0 b1 c2 c0 c1
388	23, 387	lbtr 139	. . 3 a0 b0 b1 c2 c0 c1
389	2, 388	lel2or 170	. 2 a0 a0 b0 b1 c2 c0 c1
390	1, 389	letr 137	1 a0 b0 b1 c2 c0 c1

Colors of variables: term

Syntax hints:   wb 1   wle 2   wo 6   wa 7  wt 8

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-ml 1120  ax-arg 1151

This theorem depends on definitions:  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131

This theorem is referenced by: (None)

Copyright terms: Public domain

W3C validator