Step | Hyp | Ref
| Expression |
1 | | df-oddfin 4445 |
. . 3
Oddfin
Nn 1c |
2 | | eldifsn 3839 |
. . . . 5
∼ Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1ck1 1 1ck Nn ∼ Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1ck1 1 1ck Nn
|
3 | | vex 2862 |
. . . . . . . 8
|
4 | 3 | elimak 4259 |
. . . . . . 7
∼ Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1ck1 1 1ck Nn
Nn ∼
Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1ck1 1 1c |
5 | | opkex 4113 |
. . . . . . . . . . . 12
|
6 | 5 | elimak 4259 |
. . . . . . . . . . 11
Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1ck1 1 1c 1 1 1c
Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c |
7 | | elpw121c 4148 |
. . . . . . . . . . . . . . 15
1 1 1c |
8 | 7 | anbi1i 676 |
. . . . . . . . . . . . . 14
1 1
1c Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c
Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c |
9 | | 19.41v 1901 |
. . . . . . . . . . . . . 14
Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c
Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c |
10 | 8, 9 | bitr4i 243 |
. . . . . . . . . . . . 13
1 1
1c Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c
Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c |
11 | 10 | exbii 1582 |
. . . . . . . . . . . 12
1 1 1c Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c
Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c |
12 | | df-rex 2620 |
. . . . . . . . . . . 12
1 1
1c Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c
1 1 1c Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c |
13 | | excom 1741 |
. . . . . . . . . . . 12
Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c
Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c |
14 | 11, 12, 13 | 3bitr4i 268 |
. . . . . . . . . . 11
1 1
1c Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c
Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c |
15 | | snex 4111 |
. . . . . . . . . . . . . 14
|
16 | | opkeq1 4059 |
. . . . . . . . . . . . . . 15
|
17 | 16 | eleq1d 2419 |
. . . . . . . . . . . . . 14
Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c
Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c |
18 | 15, 17 | ceqsexv 2894 |
. . . . . . . . . . . . 13
Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c |
19 | | elsymdif 3223 |
. . . . . . . . . . . . 13
Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c
Ins2k Sk
Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c |
20 | | snex 4111 |
. . . . . . . . . . . . . . . . 17
|
21 | | vex 2862 |
. . . . . . . . . . . . . . . . 17
|
22 | 20, 21, 3 | otkelins2k 4255 |
. . . . . . . . . . . . . . . 16
Ins2k Sk Sk |
23 | | vex 2862 |
. . . . . . . . . . . . . . . . 17
|
24 | 23, 3 | elssetk 4270 |
. . . . . . . . . . . . . . . 16
Sk |
25 | 22, 24 | bitri 240 |
. . . . . . . . . . . . . . 15
Ins2k Sk |
26 | | opkex 4113 |
. . . . . . . . . . . . . . . . . 18
|
27 | 26 | elimak 4259 |
. . . . . . . . . . . . . . . . 17
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c 1 1 1 1c
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1c |
28 | | df-rex 2620 |
. . . . . . . . . . . . . . . . . 18
1 1 1
1c Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1c 1 1 1 1c
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1c |
29 | | elpw131c 4149 |
. . . . . . . . . . . . . . . . . . . . 21
1 1 1 1c |
30 | 29 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . 20
1 1 1
1c Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1c
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1c |
31 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . 20
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1c
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1c |
32 | 30, 31 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . 19
1 1 1
1c Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1c
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1c |
33 | 32 | exbii 1582 |
. . . . . . . . . . . . . . . . . 18
1 1 1 1c
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1c
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1c |
34 | | excom 1741 |
. . . . . . . . . . . . . . . . . 18
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1c
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1c |
35 | 28, 33, 34 | 3bitri 262 |
. . . . . . . . . . . . . . . . 17
1 1 1
1c Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1c
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1c |
36 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . 20
|
37 | | opkeq1 4059 |
. . . . . . . . . . . . . . . . . . . . 21
|
38 | 37 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . 20
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1c
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1c |
39 | 36, 38 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . 19
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1c
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1c |
40 | | opkex 4113 |
. . . . . . . . . . . . . . . . . . . . 21
|
41 | 40 | elimak 4259 |
. . . . . . . . . . . . . . . . . . . 20
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1c 1 1 1 1 1c
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c |
42 | | df-rex 2620 |
. . . . . . . . . . . . . . . . . . . 20
1 1 1 1
1c
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c
1 1 1 1 1c
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c |
43 | | elpw141c 4150 |
. . . . . . . . . . . . . . . . . . . . . . . 24
1 1 1 1 1c |
44 | 43 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . 23
1 1 1 1
1c
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c |
45 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . . 23
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c |
46 | 44, 45 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . 22
1 1 1 1
1c
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c |
47 | 46 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . 21
1 1 1 1 1c
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c |
48 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . . 21
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c |
49 | 47, 48 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . 20
1 1 1 1 1c
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c |
50 | 41, 42, 49 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . 19
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1c
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c |
51 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . 22
|
52 | | opkeq1 4059 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
53 | 52 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . 22
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c |
54 | 51, 53 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . . 21
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c |
55 | | elin 3219 |
. . . . . . . . . . . . . . . . . . . . 21
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk
∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c |
56 | | elin 3219 |
. . . . . . . . . . . . . . . . . . . . . . 23
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
Ins3k k SIk SIk SIk ∼ Sk |
57 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
58 | 57, 36, 26 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c |
59 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
60 | 59, 20, 21 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c |
61 | | opkex 4113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
62 | 61 | elimak 4259 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c 1 1 1c
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c |
63 | | elpw121c 4148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
1 1 1c |
64 | 63 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
1 1
1c Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c |
65 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c |
66 | 64, 65 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
1 1
1c Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c |
67 | 66 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
1 1 1c
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c |
68 | | df-rex 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
1 1
1c Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c 1 1 1c
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c |
69 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c |
70 | 67, 68, 69 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
1 1
1c Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c |
71 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
72 | | opkeq1 4059 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
73 | 72 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c |
74 | 71, 73 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c |
75 | | opkex 4113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
76 | 75 | elimak 4259 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c 1 1 1 1 1c Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c |
77 | | df-rex 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
1 1 1 1
1c
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
1 1 1 1 1c
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c |
78 | | elpw141c 4150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
1 1 1 1 1c |
79 | 78 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
1 1 1 1
1c
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c |
80 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c |
81 | 79, 80 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
1 1 1 1
1c
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c |
82 | 81 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
1 1 1 1 1c
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c |
83 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c |
84 | 82, 83 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
1 1 1 1 1c
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c |
85 | 76, 77, 84 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c |
86 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
87 | | opkeq1 4059 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
88 | 87 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c |
89 | 86, 88 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c |
90 | | elin 3219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c |
91 | | elin 3219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
Ins2k Ins2k Sk k Ins2k Sk
Ins2k Ins2k Sk
k Ins2k Sk |
92 | 15, 71, 61 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
Ins2k Ins2k Sk
Ins2k
Sk |
93 | 20, 59, 21 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
Ins2k
Sk Sk |
94 | 23, 21 | elssetk 4270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
Sk |
95 | 92, 93, 94 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
Ins2k Ins2k Sk |
96 | 86, 75 | opkelxpk 4248 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
k Ins2k Sk Ins2k Sk |
97 | 86, 96 | mpbiran 884 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
k Ins2k Sk Ins2k Sk |
98 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
99 | 98, 59, 21 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
Ins2k
Sk Sk |
100 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
101 | 100, 21 | elssetk 4270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
Sk |
102 | 97, 99, 101 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
k Ins2k Sk |
103 | 95, 102 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
Ins2k Ins2k Sk
k Ins2k Sk
|
104 | 91, 103 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
Ins2k Ins2k Sk k Ins2k Sk
|
105 | | elin 3219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c
∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c |
106 | 15, 71, 61 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c |
107 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
108 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
109 | 107, 108 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c
SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c |
110 | 20, 98 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c |
111 | 23, 100 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼
Ins3k Sk Ins2k Sk k1 1 1c |
112 | 23, 100 | ndisjrelk 4323 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
Ins3k Sk Ins2k Sk k1 1 1c |
113 | 112 | notbii 287 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
Ins3k Sk Ins2k Sk k1 1 1c |
114 | | opkex 4113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
115 | 114 | elcompl 3225 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
∼ Ins3k Sk Ins2k Sk k1 1 1c Ins3k Sk Ins2k Sk k1 1 1c |
116 | | df-ne 2518 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
117 | 116 | con2bii 322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
118 | 113, 115,
117 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
∼ Ins3k Sk Ins2k Sk k1 1 1c
|
119 | 110, 111,
118 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c
|
120 | 106, 109,
119 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c
|
121 | | opkex 4113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
122 | 121 | elimak 4259 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c 1 1 1 1 1 1 1 1c
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk |
123 | | elpw171c 4153 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
1 1 1 1 1 1 1 1c |
124 | 123 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
1 1 1 1 1 1 1
1c
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk |
125 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk |
126 | 124, 125 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
1 1 1 1 1 1 1
1c
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk |
127 | 126 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
1 1 1 1 1 1 1 1c
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk |
128 | | df-rex 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
1 1 1 1 1 1 1
1c
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
1 1 1 1 1 1 1 1c
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk |
129 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk |
130 | 127, 128,
129 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
1 1 1 1 1 1 1
1c
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk |
131 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
|
132 | | opkeq1 4059 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
|
133 | 132 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk |
134 | 131, 133 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk |
135 | | elsymdif 3223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk |
136 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
|
137 | 136, 86, 75 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
Ins2k Ins2k Ins3k SIk Sk
Ins2k Ins3k SIk Sk |
138 | 36, 71, 61 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
Ins2k Ins3k SIk Sk
Ins3k SIk Sk |
139 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
|
140 | 139, 59, 21 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
Ins3k SIk Sk SIk Sk |
141 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
|
142 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
|
143 | 141, 142 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
SIk Sk Sk |
144 | 3, 142 | elssetk 4270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
Sk |
145 | 140, 143,
144 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
Ins3k SIk Sk |
146 | 137, 138,
145 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
Ins2k Ins2k Ins3k SIk Sk |
147 | 136, 86, 75 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
Ins3k SIk SIk SIk SIk SIk Sk SIk SIk SIk SIk SIk Sk |
148 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
|
149 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
|
150 | 148, 149 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
SIk SIk SIk SIk SIk Sk
SIk SIk SIk SIk Sk |
151 | 36, 15 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
SIk SIk SIk SIk Sk
SIk SIk SIk Sk |
152 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
|
153 | 152, 107 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
SIk SIk SIk Sk SIk SIk Sk |
154 | 139, 20 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
SIk SIk Sk SIk Sk |
155 | 141, 23 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
SIk Sk Sk |
156 | 3, 23 | elssetk 4270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
Sk |
157 | 154, 155,
156 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
SIk SIk Sk |
158 | 151, 153,
157 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
SIk SIk SIk SIk Sk |
159 | 147, 150,
158 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
Ins3k SIk SIk SIk SIk SIk Sk |
160 | 136, 86, 75 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
Ins2k Ins3k SIk SIk SIk Sk
Ins3k SIk SIk SIk Sk |
161 | 36, 71, 61 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
Ins3k SIk SIk SIk Sk
SIk SIk SIk Sk |
162 | 152, 108 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
SIk SIk SIk Sk SIk SIk Sk |
163 | 139, 98 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
SIk SIk Sk SIk Sk |
164 | 141, 100 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
SIk Sk Sk |
165 | 3, 100 | elssetk 4270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
Sk |
166 | 164, 165 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
SIk Sk |
167 | 162, 163,
166 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
SIk SIk SIk Sk |
168 | 160, 161,
167 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
Ins2k Ins3k SIk SIk SIk Sk |
169 | 159, 168 | orbi12i 507 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
Ins3k SIk SIk SIk SIk SIk Sk
Ins2k Ins3k SIk SIk SIk Sk |
170 | | elun 3220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
Ins3k SIk SIk SIk SIk SIk Sk
Ins2k Ins3k SIk SIk SIk Sk |
171 | | elun 3220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
|
172 | 169, 170,
171 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk |
173 | 146, 172 | bibi12i 306 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
|
174 | 173 | notbii 287 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
|
175 | 134, 135,
174 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
|
176 | 175 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk |
177 | 122, 130,
176 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
|
178 | 177 | notbii 287 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
|
179 | 121 | elcompl 3225 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c |
180 | | dfcleq 2347 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
181 | | alex 1572 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
182 | 180, 181 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
183 | 178, 179,
182 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c |
184 | 120, 183 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c
∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
|
185 | 105, 184 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
|
186 | 104, 185 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
|
187 | 89, 90, 186 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
|
188 | 187 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
|
189 | 74, 85, 188 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
|
190 | 189 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
|
191 | 62, 70, 190 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
|
192 | | eladdc 4398 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
193 | | r2ex 2652 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
194 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
195 | 192, 193,
194 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
196 | 191, 195 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c |
197 | 58, 60, 196 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c |
198 | 57, 36, 26 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Ins3k k
SIk SIk SIk ∼ Sk
k SIk SIk SIk ∼ Sk |
199 | 57, 36 | opkelcnvk 4250 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
k SIk SIk SIk ∼ Sk
SIk SIk SIk ∼ Sk |
200 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
201 | 152, 200 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
SIk SIk SIk ∼ Sk SIk SIk ∼ Sk |
202 | 139, 59 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
SIk SIk ∼ Sk SIk ∼ Sk |
203 | 141, 142 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
SIk ∼ Sk ∼ Sk |
204 | 144 | notbii 287 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Sk |
205 | | opkex 4113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
206 | 205 | elcompl 3225 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
∼ Sk Sk |
207 | 3 | elcompl 3225 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
∼ |
208 | 204, 206,
207 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
∼ Sk ∼ |
209 | 203, 208 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
SIk ∼ Sk ∼ |
210 | 201, 202,
209 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
SIk SIk SIk ∼ Sk ∼ |
211 | 198, 199,
210 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Ins3k k
SIk SIk SIk ∼ Sk ∼ |
212 | 197, 211 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . 23
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
Ins3k k SIk SIk SIk ∼ Sk
∼ |
213 | 56, 212 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . 22
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk
∼ |
214 | | opkex 4113 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
215 | 214 | elimak 4259 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c 1 1 1 1 1 1 1 1c
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k |
216 | | elpw171c 4153 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
1 1 1 1 1 1 1 1c |
217 | 216 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
1 1 1 1 1 1 1
1c
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k |
218 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k |
219 | 217, 218 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
1 1 1 1 1 1 1
1c
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k |
220 | 219 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
1 1 1 1 1 1 1 1c
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k |
221 | | df-rex 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
1 1 1 1 1 1 1
1c
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k 1 1 1 1 1 1 1
1c
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k |
222 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k |
223 | 220, 221,
222 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
1 1 1 1 1 1 1
1c
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k |
224 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
225 | | opkeq1 4059 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
226 | 225 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k |
227 | 224, 226 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k |
228 | | elsymdif 3223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k
Ins2k Ins2k Ins3k SIk Sk
Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k |
229 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
230 | 229, 51, 40 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
Ins2k Ins2k Ins3k SIk Sk
Ins2k Ins3k SIk Sk |
231 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
232 | 231, 36, 26 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
Ins2k Ins3k SIk Sk
Ins3k SIk Sk |
233 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
234 | 233, 20, 21 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
Ins3k SIk Sk SIk Sk |
235 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
236 | 235, 23 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
SIk Sk Sk |
237 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
238 | 237, 23 | elssetk 4270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
Sk |
239 | 234, 236,
238 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
Ins3k SIk Sk |
240 | 230, 232,
239 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
Ins2k Ins2k Ins3k SIk Sk |
241 | 229, 51, 40 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
Ins3k SIk SIk SIk SIk SIk Sk SIk SIk SIk SIk SIk Sk |
242 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
243 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
244 | 242, 243 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
SIk SIk SIk SIk SIk Sk
SIk SIk SIk SIk Sk |
245 | 231, 57 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
SIk SIk SIk SIk Sk
SIk SIk SIk Sk |
246 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
247 | 246, 200 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
SIk SIk SIk Sk SIk SIk Sk |
248 | 233, 59 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
SIk SIk Sk SIk Sk |
249 | 235, 142 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
SIk Sk Sk |
250 | 237, 142 | elssetk 4270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
Sk |
251 | 248, 249,
250 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
SIk SIk Sk |
252 | 245, 247,
251 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
SIk SIk SIk SIk Sk |
253 | 241, 244,
252 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
Ins3k SIk SIk SIk SIk SIk Sk |
254 | 229, 51, 40 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
Ins2k Ins3k k
Ins3k k
|
255 | 231, 36, 26 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
Ins3k k
k |
256 | 246 | sneqb 3876 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
257 | 233 | sneqb 3876 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
258 | 235 | sneqb 3876 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
259 | 237 | sneqb 3876 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
260 | 258, 259 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
261 | 256, 257,
260 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
262 | | opkelidkg 4274 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
k
|
263 | 231, 36, 262 | mp2an 653 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
k |
264 | 237 | elsnc 3756 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
265 | 261, 263,
264 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
k |
266 | 254, 255,
265 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
Ins2k Ins3k k |
267 | 253, 266 | orbi12i 507 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
Ins3k SIk SIk SIk SIk SIk Sk
Ins2k Ins3k k |
268 | | elun 3220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k
Ins3k SIk SIk SIk SIk SIk Sk
Ins2k Ins3k k |
269 | | elun 3220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
270 | 267, 268,
269 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k |
271 | 240, 270 | bibi12i 306 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Ins2k Ins2k Ins3k SIk Sk
Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k |
272 | 271 | notbii 287 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Ins2k Ins2k Ins3k SIk Sk
Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k |
273 | 227, 228,
272 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k
|
274 | 273 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k |
275 | 215, 223,
274 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c
|
276 | 275 | notbii 287 |
. . . . . . . . . . . . . . . . . . . . . . 23
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c
|
277 | 214 | elcompl 3225 |
. . . . . . . . . . . . . . . . . . . . . . 23
∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c |
278 | | dfcleq 2347 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
279 | | alex 1572 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
280 | 278, 279 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
281 | 276, 277,
280 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . 22
∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c |
282 | 213, 281 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . 21
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk
∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c
∼ |
283 | 54, 55, 282 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . 20
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c ∼ |
284 | 283 | exbii 1582 |
. . . . . . . . . . . . . . . . . . 19
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c
∼
|
285 | 39, 50, 284 | 3bitri 262 |
. . . . . . . . . . . . . . . . . 18
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1c
∼
|
286 | 285 | exbii 1582 |
. . . . . . . . . . . . . . . . 17
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1c
∼ |
287 | 27, 35, 286 | 3bitri 262 |
. . . . . . . . . . . . . . . 16
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c
∼
|
288 | 20, 21, 3 | otkelins3k 4256 |
. . . . . . . . . . . . . . . 16
Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c |
289 | | elsuc 4413 |
. . . . . . . . . . . . . . . . 17
1c
∼
|
290 | | r2ex 2652 |
. . . . . . . . . . . . . . . . 17
∼
∼ |
291 | | excom 1741 |
. . . . . . . . . . . . . . . . 17
∼
∼ |
292 | 289, 290,
291 | 3bitri 262 |
. . . . . . . . . . . . . . . 16
1c
∼ |
293 | 287, 288,
292 | 3bitr4i 268 |
. . . . . . . . . . . . . . 15
Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c 1c |
294 | 25, 293 | bibi12i 306 |
. . . . . . . . . . . . . 14
Ins2k Sk
Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c
1c |
295 | 294 | notbii 287 |
. . . . . . . . . . . . 13
Ins2k
Sk
Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c
1c |
296 | 18, 19, 295 | 3bitri 262 |
. . . . . . . . . . . 12
Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c
1c |
297 | 296 | exbii 1582 |
. . . . . . . . . . 11
Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c
1c |
298 | 6, 14, 297 | 3bitri 262 |
. . . . . . . . . 10
Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1ck1 1 1c
1c |
299 | 298 | notbii 287 |
. . . . . . . . 9
Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1ck1 1 1c
1c |
300 | 5 | elcompl 3225 |
. . . . . . . . 9
∼ Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1ck1 1 1c Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1ck1 1 1c |
301 | | dfcleq 2347 |
. . . . . . . . . 10
1c
1c |
302 | | alex 1572 |
. . . . . . . . . 10
1c
1c |
303 | 301, 302 | bitri 240 |
. . . . . . . . 9
1c
1c |
304 | 299, 300,
303 | 3bitr4i 268 |
. . . . . . . 8
∼ Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1ck1 1 1c 1c |
305 | 304 | rexbii 2639 |
. . . . . . 7
Nn ∼
Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1ck1 1 1c Nn 1c |
306 | 4, 305 | bitri 240 |
. . . . . 6
∼ Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1ck1 1 1ck Nn
Nn 1c |
307 | 306 | anbi1i 676 |
. . . . 5
∼ Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1ck1 1 1ck Nn
Nn 1c |
308 | 2, 307 | bitri 240 |
. . . 4
∼ Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1ck1 1 1ck Nn
Nn 1c |
309 | 308 | abbi2i 2464 |
. . 3
∼
Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1ck1 1 1ck Nn
Nn 1c |
310 | 1, 309 | eqtr4i 2376 |
. 2
Oddfin ∼ Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1ck1 1 1ck Nn |
311 | | ssetkex 4294 |
. . . . . . . 8
Sk |
312 | 311 | ins2kex 4307 |
. . . . . . 7
Ins2k Sk |
313 | 312 | ins2kex 4307 |
. . . . . . . . . . . . . . . . . 18
Ins2k Ins2k Sk |
314 | | vvex 4109 |
. . . . . . . . . . . . . . . . . . 19
|
315 | 314, 312 | xpkex 4289 |
. . . . . . . . . . . . . . . . . 18
k Ins2k Sk
|
316 | 313, 315 | inex 4105 |
. . . . . . . . . . . . . . . . 17
Ins2k Ins2k Sk k Ins2k Sk
|
317 | 311 | ins3kex 4308 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Ins3k Sk |
318 | 317, 312 | inex 4105 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Ins3k Sk Ins2k Sk
|
319 | | 1cex 4142 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
1c
|
320 | 319 | pw1ex 4303 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
1
1c
|
321 | 320 | pw1ex 4303 |
. . . . . . . . . . . . . . . . . . . . . . . 24
1 1
1c
|
322 | 318, 321 | imakex 4300 |
. . . . . . . . . . . . . . . . . . . . . . 23
Ins3k Sk Ins2k Sk k1 1 1c
|
323 | 322 | complex 4104 |
. . . . . . . . . . . . . . . . . . . . . 22
∼ Ins3k Sk Ins2k Sk k1 1 1c
|
324 | 323 | sikex 4297 |
. . . . . . . . . . . . . . . . . . . . 21
SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c
|
325 | 324 | sikex 4297 |
. . . . . . . . . . . . . . . . . . . 20
SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c
|
326 | 325 | sikex 4297 |
. . . . . . . . . . . . . . . . . . 19
SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c
|
327 | 326 | ins3kex 4308 |
. . . . . . . . . . . . . . . . . 18
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c
|
328 | 311 | sikex 4297 |
. . . . . . . . . . . . . . . . . . . . . . . 24
SIk Sk |
329 | 328 | ins3kex 4308 |
. . . . . . . . . . . . . . . . . . . . . . 23
Ins3k SIk Sk |
330 | 329 | ins2kex 4307 |
. . . . . . . . . . . . . . . . . . . . . 22
Ins2k Ins3k SIk Sk |
331 | 330 | ins2kex 4307 |
. . . . . . . . . . . . . . . . . . . . 21
Ins2k Ins2k Ins3k SIk Sk |
332 | 328 | sikex 4297 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
SIk SIk Sk |
333 | 332 | sikex 4297 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
SIk SIk SIk Sk |
334 | 333 | sikex 4297 |
. . . . . . . . . . . . . . . . . . . . . . . 24
SIk SIk SIk SIk Sk |
335 | 334 | sikex 4297 |
. . . . . . . . . . . . . . . . . . . . . . 23
SIk SIk SIk SIk SIk Sk |
336 | 335 | ins3kex 4308 |
. . . . . . . . . . . . . . . . . . . . . 22
Ins3k SIk SIk SIk SIk SIk Sk |
337 | 333 | ins3kex 4308 |
. . . . . . . . . . . . . . . . . . . . . . 23
Ins3k SIk SIk SIk Sk |
338 | 337 | ins2kex 4307 |
. . . . . . . . . . . . . . . . . . . . . 22
Ins2k Ins3k SIk SIk SIk Sk |
339 | 336, 338 | unex 4106 |
. . . . . . . . . . . . . . . . . . . . 21
Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
|
340 | 331, 339 | symdifex 4108 |
. . . . . . . . . . . . . . . . . . . 20
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
|
341 | 321 | pw1ex 4303 |
. . . . . . . . . . . . . . . . . . . . . . . 24
1 1 1
1c
|
342 | 341 | pw1ex 4303 |
. . . . . . . . . . . . . . . . . . . . . . 23
1 1 1 1
1c
|
343 | 342 | pw1ex 4303 |
. . . . . . . . . . . . . . . . . . . . . 22
1 1 1 1 1
1c
|
344 | 343 | pw1ex 4303 |
. . . . . . . . . . . . . . . . . . . . 21
1 1 1 1 1 1
1c
|
345 | 344 | pw1ex 4303 |
. . . . . . . . . . . . . . . . . . . 20
1 1 1 1 1 1 1
1c
|
346 | 340, 345 | imakex 4300 |
. . . . . . . . . . . . . . . . . . 19
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
|
347 | 346 | complex 4104 |
. . . . . . . . . . . . . . . . . 18
∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
|
348 | 327, 347 | inex 4105 |
. . . . . . . . . . . . . . . . 17
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
|
349 | 316, 348 | inex 4105 |
. . . . . . . . . . . . . . . 16
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1c |
350 | 349, 342 | imakex 4300 |
. . . . . . . . . . . . . . 15
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
|
351 | 350, 321 | imakex 4300 |
. . . . . . . . . . . . . 14
Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
|
352 | 351 | ins2kex 4307 |
. . . . . . . . . . . . 13
Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
|
353 | 352 | ins2kex 4307 |
. . . . . . . . . . . 12
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
|
354 | 311 | complex 4104 |
. . . . . . . . . . . . . . . . 17
∼ Sk |
355 | 354 | sikex 4297 |
. . . . . . . . . . . . . . . 16
SIk ∼ Sk |
356 | 355 | sikex 4297 |
. . . . . . . . . . . . . . 15
SIk SIk ∼ Sk |
357 | 356 | sikex 4297 |
. . . . . . . . . . . . . 14
SIk SIk SIk ∼ Sk |
358 | 357 | cnvkex 4287 |
. . . . . . . . . . . . 13
k
SIk SIk SIk ∼ Sk |
359 | 358 | ins3kex 4308 |
. . . . . . . . . . . 12
Ins3k k SIk SIk SIk ∼ Sk |
360 | 353, 359 | inex 4105 |
. . . . . . . . . . 11
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk
|
361 | | idkex 4314 |
. . . . . . . . . . . . . . . . 17
k
|
362 | 361 | ins3kex 4308 |
. . . . . . . . . . . . . . . 16
Ins3k k |
363 | 362 | ins2kex 4307 |
. . . . . . . . . . . . . . 15
Ins2k Ins3k k |
364 | 336, 363 | unex 4106 |
. . . . . . . . . . . . . 14
Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k |
365 | 331, 364 | symdifex 4108 |
. . . . . . . . . . . . 13
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k |
366 | 365, 345 | imakex 4300 |
. . . . . . . . . . . 12
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c
|
367 | 366 | complex 4104 |
. . . . . . . . . . 11
∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c
|
368 | 360, 367 | inex 4105 |
. . . . . . . . . 10
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1c
|
369 | 368, 342 | imakex 4300 |
. . . . . . . . 9
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1c
|
370 | 369, 341 | imakex 4300 |
. . . . . . . 8
Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c
|
371 | 370 | ins3kex 4308 |
. . . . . . 7
Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c
|
372 | 312, 371 | symdifex 4108 |
. . . . . 6
Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1c
|
373 | 372, 321 | imakex 4300 |
. . . . 5
Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1ck1 1 1c
|
374 | 373 | complex 4104 |
. . . 4
∼ Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1ck1 1 1c
|
375 | | nncex 4396 |
. . . 4
Nn |
376 | 374, 375 | imakex 4300 |
. . 3
∼ Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1ck1 1 1ck Nn |
377 | | snex 4111 |
. . 3
|
378 | 376, 377 | difex 4107 |
. 2
∼
Ins2k Sk Ins3k Ins2k Ins2k Ins2k Ins2k Sk k Ins2k Sk
Ins3k SIk SIk SIk ∼ Ins3k Sk Ins2k Sk k1 1 1c ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k k
SIk SIk SIk ∼ Sk ∼ Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k k k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1 1ck1 1 1ck Nn |
379 | 310, 378 | eqeltri 2423 |
1
Oddfin |