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

---

Theorem xdp43 1205

Description: Part of proof (4)=>(3) in Day/Pickering 1982.

Hypotheses

Ref	Expression
xxxdp.c0	c0 a1 a2 b1 b2
xxxdp.c1	c1 a0 a2 b0 b2
xxxdp.c2	c2 a0 a1 b0 b1
xxxdp.d	a2 a0 a1 b1
xxxdp.e	b0 a0 p0
xxxdp.p	a0 b0 a1 b1 a2 b2
xxxdp.p0	p0 a1 b1 a2 b2
xxxdp.p2	p2 a0 b0 a1 b1

Assertion

Ref	Expression
xdp43	a0 b0 b1 c2 c0 c1

---

Proof of Theorem xdp43

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