Proof of Theorem dp41lemg
Step | Hyp | Ref
| Expression |
1 | | or32 82 |
. . . 4
a1
a2
b1 a0 a1 a1 b1 a0 a1 a2 |
2 | | ml3 1128 |
. . . . . 6
a1 b1 a0 a1 a1 a0 b1
a1 |
3 | | orcom 73 |
. . . . . . . 8
b1 a1 a1 b1 |
4 | 3 | lan 77 |
. . . . . . 7
a0 b1 a1 a0
a1 b1 |
5 | 4 | lor 70 |
. . . . . 6
a1 a0 b1 a1 a1 a0 a1
b1 |
6 | 2, 5 | tr 62 |
. . . . 5
a1 b1 a0 a1 a1 a0 a1
b1 |
7 | 6 | ror 71 |
. . . 4
a1
b1 a0 a1 a2 a1
a0 a1 b1 a2 |
8 | | or32 82 |
. . . 4
a1
a0 a1 b1 a2 a1
a2
a0 a1 b1 |
9 | 1, 7, 8 | 3tr 65 |
. . 3
a1
a2
b1 a0 a1 a1 a2 a0 a1 b1 |
10 | 9 | lan 77 |
. 2
b1
b2
a1
a2
b1 a0 a1 b1 b2 a1 a2 a0 a1 b1 |
11 | | or32 82 |
. . . 4
b0
b2
a0 b0 b1 b0 a0 b0 b1 b2 |
12 | | orcom 73 |
. . . . . . . 8
b0 b1 b1 b0 |
13 | 12 | lan 77 |
. . . . . . 7
a0 b0 b1 a0
b1 b0 |
14 | 13 | lor 70 |
. . . . . 6
b0 a0 b0 b1 b0 a0 b1
b0 |
15 | | ml3 1128 |
. . . . . 6
b0 a0 b1 b0 b0 b1 a0
b0 |
16 | 14, 15 | tr 62 |
. . . . 5
b0 a0 b0 b1 b0 b1 a0
b0 |
17 | 16 | ror 71 |
. . . 4
b0
a0 b0 b1 b2 b0
b1 a0 b0 b2 |
18 | | or32 82 |
. . . 4
b0
b1 a0 b0 b2 b0
b2
b1 a0 b0 |
19 | 11, 17, 18 | 3tr 65 |
. . 3
b0
b2
a0 b0 b1 b0 b2 b1 a0 b0 |
20 | 19 | lan 77 |
. 2
a0
a2
b0
b2
a0 b0 b1 a0 a2 b0 b2 b1 a0 b0 |
21 | 10, 20 | 2or 72 |
1
b1 b2
a1
a2
b1 a0 a1 a0 a2 b0 b2 a0 b0 b1 b1 b2
a1
a2
a0 a1 b1 a0 a2 b0 b2 b1 a0 b0 |