NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  evenodddisjlem1 Unicode version

Theorem evenodddisjlem1 4516
Description: Lemma for evenodddisj 4517. Establish stratification for induction. (Contributed by SF, 25-Jan-2015.)
Assertion
Ref Expression
evenodddisjlem1 Nn 1c 1c
Distinct variable group:   ,

Proof of Theorem evenodddisjlem1
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-or 359 . . . 4 Nn 1c 1c Nn 1c 1c
2 vex 2863 . . . . . 6
32elimakv 4261 . . . . 5 Ins3k Sk Ins2k Ins2k Sk Ins2k 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 1ck1 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k k Ins3k Sk Ins2k Ins2k Sk Ins2k 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 1ck1 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k
4 elin 3220 . . . . . . 7 Ins3k Sk Ins2k Ins2k Sk Ins2k 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 1ck1 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k Ins3k Sk Ins2k Ins2k Sk Ins2k 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 1ck1 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k
5 opkex 4114 . . . . . . . . . . . . 13
65elimak 4260 . . . . . . . . . . . 12 Ins3k Sk Ins2k Ins2k Sk Ins2k 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 1ck1 1 1c 1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k 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
7 elpw121c 4149 . . . . . . . . . . . . . . . 16 1 1 1c
87anbi1i 676 . . . . . . . . . . . . . . 15 1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k 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 Sk Ins2k Ins2k Sk Ins2k 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
9 19.41v 1901 . . . . . . . . . . . . . . 15 Ins3k Sk Ins2k Ins2k Sk Ins2k 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 Sk Ins2k Ins2k Sk Ins2k 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
108, 9bitr4i 243 . . . . . . . . . . . . . 14 1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k 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 Sk Ins2k Ins2k Sk Ins2k 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
1110exbii 1582 . . . . . . . . . . . . 13 1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k 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 Sk Ins2k Ins2k Sk Ins2k 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
12 df-rex 2621 . . . . . . . . . . . . 13 1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k 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 Ins3k Sk Ins2k Ins2k Sk Ins2k 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
13 excom 1741 . . . . . . . . . . . . 13 Ins3k Sk Ins2k Ins2k Sk Ins2k 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 Sk Ins2k Ins2k Sk Ins2k 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
1411, 12, 133bitr4i 268 . . . . . . . . . . . 12 1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k 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 Sk Ins2k Ins2k Sk Ins2k 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
15 snex 4112 . . . . . . . . . . . . . . 15
16 opkeq1 4060 . . . . . . . . . . . . . . . 16
1716eleq1d 2419 . . . . . . . . . . . . . . 15 Ins3k Sk Ins2k Ins2k Sk Ins2k 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 Sk Ins2k Ins2k Sk Ins2k 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
1815, 17ceqsexv 2895 . . . . . . . . . . . . . 14 Ins3k Sk Ins2k Ins2k Sk Ins2k 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 Sk Ins2k Ins2k Sk Ins2k 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
19 elsymdif 3224 . . . . . . . . . . . . . 14 Ins3k Sk Ins2k Ins2k Sk Ins2k 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 Sk Ins2k Ins2k Sk Ins2k 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
20 snex 4112 . . . . . . . . . . . . . . . . . 18
21 vex 2863 . . . . . . . . . . . . . . . . . 18
2220, 21, 2otkelins3k 4257 . . . . . . . . . . . . . . . . 17 Ins3k Sk Sk
23 vex 2863 . . . . . . . . . . . . . . . . . 18
2423, 21elssetk 4271 . . . . . . . . . . . . . . . . 17 Sk
2522, 24bitri 240 . . . . . . . . . . . . . . . 16 Ins3k Sk
2620, 21, 2otkelins2k 4256 . . . . . . . . . . . . . . . . 17 Ins2k Ins2k Sk Ins2k 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 Sk Ins2k 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
27 opkex 4114 . . . . . . . . . . . . . . . . . . . 20
2827elimak 4260 . . . . . . . . . . . . . . . . . . 19 Ins2k Sk Ins2k 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 Sk Ins2k 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
29 elpw121c 4149 . . . . . . . . . . . . . . . . . . . . . . 23 1 1 1c
3029anbi1i 676 . . . . . . . . . . . . . . . . . . . . . 22 1 1 1c Ins2k Sk Ins2k 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 Sk Ins2k 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
31 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . 22 Ins2k Sk Ins2k 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 Sk Ins2k 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
3230, 31bitr4i 243 . . . . . . . . . . . . . . . . . . . . 21 1 1 1c Ins2k Sk Ins2k 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 Sk Ins2k 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
3332exbii 1582 . . . . . . . . . . . . . . . . . . . 20 1 1 1c Ins2k Sk Ins2k 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 Sk Ins2k 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
34 df-rex 2621 . . . . . . . . . . . . . . . . . . . 20 1 1 1c Ins2k Sk Ins2k 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 Sk Ins2k 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
35 excom 1741 . . . . . . . . . . . . . . . . . . . 20 Ins2k Sk Ins2k 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 Sk Ins2k 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
3633, 34, 353bitr4i 268 . . . . . . . . . . . . . . . . . . 19 1 1 1c Ins2k Sk Ins2k 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 Sk Ins2k 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
37 snex 4112 . . . . . . . . . . . . . . . . . . . . . 22
38 opkeq1 4060 . . . . . . . . . . . . . . . . . . . . . . 23
3938eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . 22 Ins2k Sk Ins2k 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 Sk Ins2k 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
4037, 39ceqsexv 2895 . . . . . . . . . . . . . . . . . . . . 21 Ins2k Sk Ins2k 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 Sk Ins2k 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
41 elin 3220 . . . . . . . . . . . . . . . . . . . . 21 Ins2k Sk Ins2k 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 Sk Ins2k 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
42 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . 24
4342, 20, 2otkelins2k 4256 . . . . . . . . . . . . . . . . . . . . . . 23 Ins2k Sk Sk
44 vex 2863 . . . . . . . . . . . . . . . . . . . . . . . 24
4544, 2elssetk 4271 . . . . . . . . . . . . . . . . . . . . . . 23 Sk
4643, 45bitri 240 . . . . . . . . . . . . . . . . . . . . . 22 Ins2k Sk
47 opkex 4114 . . . . . . . . . . . . . . . . . . . . . . . . 25
4847elimak 4260 . . . . . . . . . . . . . . . . . . . . . . . 24 Ins2k 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 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
49 elpw141c 4151 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1 1 1 1 1c
5049anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 1 1 1 1 1c Ins2k 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 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
51 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins2k 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 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
5250, 51bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 1 1 1 1c Ins2k 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 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
5352exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 1 1 1 1c Ins2k 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 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
54 df-rex 2621 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 1 1 1 1c Ins2k 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 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
55 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ins2k 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 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
5653, 54, 553bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . 24 1 1 1 1 1c Ins2k 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 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
57 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
58 opkeq1 4060 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
5958eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins2k 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 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
6057, 59ceqsexv 2895 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins2k 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 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
61 elin 3220 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins2k 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 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
62 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
6362, 37, 27otkelins2k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins2k Ins2k Sk Ins2k Sk
64 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
6564, 20, 2otkelins2k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins2k Sk Sk
66 vex 2863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
6766, 2elssetk 4271 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Sk
6863, 65, 673bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins2k Ins2k Sk
69 elin 3220 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 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
7062, 37, 27otkelins3k 4257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
71 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
72 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
7371, 72opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
7464, 42opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 SIk SIk Ins3k Sk Ins2k Sk k1 1 1c SIk Ins3k Sk Ins2k Sk k1 1 1c
7566, 44opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 SIk Ins3k Sk Ins2k Sk k1 1 1c Ins3k Sk Ins2k Sk k1 1 1c
7666, 44ndisjrelk 4324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Ins3k Sk Ins2k Sk k1 1 1c
7776notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Ins3k Sk Ins2k Sk k1 1 1c
78 opkex 4114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
7978elcompl 3226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Ins3k Sk Ins2k Sk k1 1 1c Ins3k Sk Ins2k Sk k1 1 1c
80 df-ne 2519 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
8180con2bii 322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
8277, 79, 813bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Ins3k Sk Ins2k Sk k1 1 1c
8374, 75, 823bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
8470, 73, 833bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
85 opkex 4114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
8685elimak 4260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 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
87 elpw171c 4154 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 1 1 1 1 1 1 1 1c
8887anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 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
89 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 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
9088, 89bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 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
9190exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 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
92 df-rex 2621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 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
93 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 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
9491, 92, 933bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 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
95 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
96 opkeq1 4060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
9796eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 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
9895, 97ceqsexv 2895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 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
99 elsymdif 3224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 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
100 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
101100, 57, 47otkelins2k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk Sk
102 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
103102, 37, 27otkelins2k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Ins2k Ins3k SIk Sk Ins3k SIk Sk
104 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
105104, 20, 2otkelins3k 4257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Ins3k SIk Sk SIk Sk
106 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
107106, 23opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 SIk Sk Sk
10821, 23elssetk 4271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Sk
109105, 107, 1083bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Ins3k SIk Sk
110101, 103, 1093bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 Ins2k Ins2k Ins3k SIk Sk
111100, 57, 47otkelins3k 4257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Ins3k SIk SIk SIk SIk SIk Sk SIk SIk SIk SIk SIk Sk
112 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
113 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
114112, 113opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 SIk SIk SIk SIk SIk Sk SIk SIk SIk SIk Sk
115102, 62opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 SIk SIk SIk SIk Sk SIk SIk SIk Sk
116 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
117116, 71opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 SIk SIk SIk Sk SIk SIk Sk
118104, 64opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 SIk SIk Sk SIk Sk
119106, 66opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 SIk Sk Sk
12021, 66elssetk 4271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 Sk
121118, 119, 1203bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 SIk SIk Sk
122115, 117, 1213bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 SIk SIk SIk SIk Sk
123111, 114, 1223bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Ins3k SIk SIk SIk SIk SIk Sk
124100, 57, 47otkelins2k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk Sk
125102, 37, 27otkelins3k 4257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Ins3k SIk SIk SIk Sk SIk SIk SIk Sk
126116, 72opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 SIk SIk SIk Sk SIk SIk Sk
127104, 42opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 SIk SIk Sk SIk Sk
128106, 44opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 SIk Sk Sk
12921, 44elssetk 4271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 Sk
130128, 129bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 SIk Sk
131126, 127, 1303bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 SIk SIk SIk Sk
132124, 125, 1313bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Ins2k Ins3k SIk SIk SIk Sk
133123, 132orbi12i 507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
134 elun 3221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 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
135 elun 3221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
136133, 134, 1353bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
137110, 136bibi12i 306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
138137notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
13998, 99, 1383bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
140139exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
14186, 94, 1403bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 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
142141notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 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
14385elcompl 3226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 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
144 dfcleq 2347 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
145 alex 1572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
146144, 145bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
147142, 143, 1463bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 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
14884, 147anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 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
14969, 148bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 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
15068, 149anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins2k 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
15160, 61, 1503bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ins2k 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
152151exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . 24 Ins2k 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
15348, 56, 1523bitri 262 . . . . . . . . . . . . . . . . . . . . . . 23 Ins2k 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
154 df-rex 2621 . . . . . . . . . . . . . . . . . . . . . . 23
155153, 154bitr4i 243 . . . . . . . . . . . . . . . . . . . . . 22 Ins2k 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
15646, 155anbi12i 678 . . . . . . . . . . . . . . . . . . . . 21 Ins2k Sk Ins2k 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
15740, 41, 1563bitri 262 . . . . . . . . . . . . . . . . . . . 20 Ins2k Sk Ins2k 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
158157exbii 1582 . . . . . . . . . . . . . . . . . . 19 Ins2k Sk Ins2k 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
15928, 36, 1583bitri 262 . . . . . . . . . . . . . . . . . 18 Ins2k Sk Ins2k 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
160 df-rex 2621 . . . . . . . . . . . . . . . . . 18
161159, 160bitr4i 243 . . . . . . . . . . . . . . . . 17 Ins2k Sk Ins2k 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
162 rexcom 2773 . . . . . . . . . . . . . . . . 17
16326, 161, 1623bitri 262 . . . . . . . . . . . . . . . 16 Ins2k Ins2k Sk Ins2k 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
16425, 163bibi12i 306 . . . . . . . . . . . . . . 15 Ins3k Sk Ins2k Ins2k Sk Ins2k 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
165164notbii 287 . . . . . . . . . . . . . 14 Ins3k Sk Ins2k Ins2k Sk Ins2k 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
16618, 19, 1653bitri 262 . . . . . . . . . . . . 13 Ins3k Sk Ins2k Ins2k Sk Ins2k 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
167166exbii 1582 . . . . . . . . . . . 12 Ins3k Sk Ins2k Ins2k Sk Ins2k 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
1686, 14, 1673bitri 262 . . . . . . . . . . 11 Ins3k Sk Ins2k Ins2k Sk Ins2k 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 1ck1 1 1c
169168notbii 287 . . . . . . . . . 10 Ins3k Sk Ins2k Ins2k Sk Ins2k 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 1ck1 1 1c
1705elcompl 3226 . . . . . . . . . 10 Ins3k Sk Ins2k Ins2k Sk Ins2k 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 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k 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 1ck1 1 1c
171 alex 1572 . . . . . . . . . 10
172169, 170, 1713bitr4i 268 . . . . . . . . 9 Ins3k Sk Ins2k Ins2k Sk Ins2k 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 1ck1 1 1c
173 df-addc 4379 . . . . . . . . . . 11
174173eqeq2i 2363 . . . . . . . . . 10
175 abeq2 2459 . . . . . . . . . 10
176174, 175bitri 240 . . . . . . . . 9
177172, 176bitr4i 243 . . . . . . . 8 Ins3k Sk Ins2k Ins2k Sk Ins2k 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 1ck1 1 1c
17821, 2opkelxpk 4249 . . . . . . . . . 10 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn
1792, 178mpbiran2 885 . . . . . . . . 9 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn
180 elun 3221 . . . . . . . . 9 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn
18121elsnc 3757 . . . . . . . . . 10
18221elimak 4260 . . . . . . . . . . . . 13 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn Nn Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1c
183 opkex 4114 . . . . . . . . . . . . . . . . 17
184183elimak 4260 . . . . . . . . . . . . . . . 16 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1c 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k
185 elpw11c 4148 . . . . . . . . . . . . . . . . . . . 20 1 1c
186185anbi1i 676 . . . . . . . . . . . . . . . . . . 19 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k
187 19.41v 1901 . . . . . . . . . . . . . . . . . . 19 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k
188186, 187bitr4i 243 . . . . . . . . . . . . . . . . . 18 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k
189188exbii 1582 . . . . . . . . . . . . . . . . 17 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k
190 df-rex 2621 . . . . . . . . . . . . . . . . 17 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k
191 excom 1741 . . . . . . . . . . . . . . . . 17 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k
192189, 190, 1913bitr4i 268 . . . . . . . . . . . . . . . 16 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k
193 snex 4112 . . . . . . . . . . . . . . . . . . 19
194 opkeq1 4060 . . . . . . . . . . . . . . . . . . . 20
195194eleq1d 2419 . . . . . . . . . . . . . . . . . . 19 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k
196193, 195ceqsexv 2895 . . . . . . . . . . . . . . . . . 18 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k
197 elin 3220 . . . . . . . . . . . . . . . . . 18 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k
198 vex 2863 . . . . . . . . . . . . . . . . . . . . 21
19923, 198, 21otkelins3k 4257 . . . . . . . . . . . . . . . . . . . 20 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c
200 opkex 4114 . . . . . . . . . . . . . . . . . . . . . 22
201200elimak 4260 . . . . . . . . . . . . . . . . . . . . 21 Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
202 elpw11c 4148 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 1c
203202anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . 24 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
204 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . 24 Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
205203, 204bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . 23 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
206205exbii 1582 . . . . . . . . . . . . . . . . . . . . . 22 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
207 df-rex 2621 . . . . . . . . . . . . . . . . . . . . . 22 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
208 excom 1741 . . . . . . . . . . . . . . . . . . . . . 22 Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
209206, 207, 2083bitr4i 268 . . . . . . . . . . . . . . . . . . . . 21 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
210 opkeq1 4060 . . . . . . . . . . . . . . . . . . . . . . . . 25
211210eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . 24 Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
212104, 211ceqsexv 2895 . . . . . . . . . . . . . . . . . . . . . . 23 Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
213 elin 3220 . . . . . . . . . . . . . . . . . . . . . . 23 Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
214 opkex 4114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
215214elimak 4260 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c 1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
2167anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
217 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
218216, 217bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
219218exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
220 df-rex 2621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c 1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
221 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
222219, 220, 2213bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
223 opkeq1 4060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
224223eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
22515, 224ceqsexv 2895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
226 elsymdif 3224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
22720, 21, 198otkelins3k 4257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Ins3k Sk Sk
228227, 24bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Ins3k Sk
229 opkex 4114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
230229elimak 4260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
231 elpw121c 4149 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 1 1 1c
232231anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
233 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
234232, 233bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
235234exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
236 df-rex 2621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
237 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
238235, 236, 2373bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
239 opkeq1 4060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
240239eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
24162, 240ceqsexv 2895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
242 elin 3220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
24364, 20, 198otkelins2k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Ins2k Sk Sk
24466, 198elssetk 4271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Sk
245243, 244bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Ins2k Sk
246 opkex 4114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
247246elimak 4260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
248 elpw141c 4151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 1 1 1 1 1c
249248anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
250 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
251249, 250bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
252251exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
253 df-rex 2621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
254 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
255252, 253, 2543bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
256 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
257 opkeq1 4060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
258257eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
259256, 258ceqsexv 2895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
260 elin 3220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
26137, 62, 229otkelins2k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 Ins2k Ins2k Sk Ins2k Sk
26242, 20, 198otkelins2k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 Ins2k Sk Sk
26344, 198elssetk 4271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 Sk
264261, 262, 2633bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Ins2k Ins2k Sk
265 elin 3220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
26637, 62, 229otkelins3k 4257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
26737, 62opkelcnvk 4251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
26871, 72opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
26964, 42opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 SIk SIk Ins3k Sk Ins2k Sk k1 1 1c SIk Ins3k Sk Ins2k Sk k1 1 1c
27066, 44opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 SIk Ins3k Sk Ins2k Sk k1 1 1c Ins3k Sk Ins2k Sk k1 1 1c
271270, 76bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 SIk Ins3k Sk Ins2k Sk k1 1 1c
272268, 269, 2713bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
273266, 267, 2723bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
274273notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
275 opkex 4114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
276275elcompl 3226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
277274, 276, 813bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
278275elimak 4260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk 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 Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
27987anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 1 1 1 1 1 1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
280 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
281279, 280bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 1 1 1 1 1 1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
282281exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 1 1 1 1 1 1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
283 df-rex 2621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 1 1 1 1 1 1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk 1 1 1 1 1 1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
284 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
285282, 283, 2843bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 1 1 1 1 1 1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
286 opkeq1 4060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
287286eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
28895, 287ceqsexv 2895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
289 elsymdif 3224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
290100, 256, 246otkelins2k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk Sk
291102, 62, 229otkelins2k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 Ins2k Ins3k SIk Sk Ins3k SIk Sk
292104, 20, 198otkelins3k 4257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 Ins3k SIk Sk SIk Sk
293292, 107, 1083bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 Ins3k SIk Sk
294290, 291, 2933bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 Ins2k Ins2k Ins3k SIk Sk
295100, 256, 246otkelins2k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk Sk
296102, 62, 229otkelins3k 4257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 Ins3k SIk SIk SIk Sk SIk SIk SIk Sk
297119, 120bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 SIk Sk
298117, 118, 2973bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 SIk SIk SIk Sk
299295, 296, 2983bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 Ins2k Ins3k SIk SIk SIk Sk
300100, 256, 246otkelins3k 4257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 Ins3k SIk SIk SIk SIk SIk Sk SIk SIk SIk SIk SIk Sk
301 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
302112, 301opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 SIk SIk SIk SIk SIk Sk SIk SIk SIk SIk Sk
303102, 37opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 SIk SIk SIk SIk Sk SIk SIk SIk Sk
304127, 128, 1293bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 SIk SIk Sk
305303, 126, 3043bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 SIk SIk SIk SIk Sk
306300, 302, 3053bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 Ins3k SIk SIk SIk SIk SIk Sk
307299, 306orbi12i 507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
308 elun 3221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
309307, 308, 1353bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
310294, 309bibi12i 306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
311310notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
312288, 289, 3113bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
313312exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
314278, 285, 3133bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
315314notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
316275elcompl 3226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
317315, 316, 1463bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
318277, 317anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
319265, 318bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
320264, 319anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
321259, 260, 3203bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
322321exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
323247, 255, 3223bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
324 df-rex 2621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
325323, 324bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
326245, 325anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
327241, 242, 3263bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
328327exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
329230, 238, 3283bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
33020, 21, 198otkelins2k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
331 df-rex 2621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
332329, 330, 3313bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
333228, 332bibi12i 306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
334333notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
335225, 226, 3343bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
336335exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
337215, 222, 3363bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c
338337notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c
339214elcompl 3226 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c
340 alex 1572 . . . . . . . . . . . . . . . . . . . . . . . . . 26
341338, 339, 3403bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c
34221, 23, 198otkelins2k 4256 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c
343 df-addc 4379 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
344343eqeq2i 2363 . . . . . . . . . . . . . . . . . . . . . . . . . 26
345 abeq2 2459 . . . . . . . . . . . . . . . . . . . . . . . . . 26
346344, 345bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . 25
347341, 342, 3463bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . 24 Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c
34821, 23opkelimagek 4273 . . . . . . . . . . . . . . . . . . . . . . . . 25 Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck
34921, 23, 198otkelins3k 4257 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
350 dfaddc2 4382 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1c Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck
351350eqeq2i 2363 . . . . . . . . . . . . . . . . . . . . . . . . 25 1c Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck
352348, 349, 3513bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . 24 Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c 1c
353347, 352anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . 23 Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c 1c
354212, 213, 3533bitri 262 . . . . . . . . . . . . . . . . . . . . . 22 Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c 1c
355354exbii 1582 . . . . . . . . . . . . . . . . . . . . 21 Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c 1c
356201, 209, 3553bitri 262 . . . . . . . . . . . . . . . . . . . 20 Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c 1c
357198, 198addcex 4395 . . . . . . . . . . . . . . . . . . . . 21
358 addceq1 4384 . . . . . . . . . . . . . . . . . . . . . 22 1c 1c
359358eqeq2d 2364 . . . . . . . . . . . . . . . . . . . . 21 1c 1c
360357, 359ceqsexv 2895 . . . . . . . . . . . . . . . . . . . 20 1c 1c
361199, 356, 3603bitri 262 . . . . . . . . . . . . . . . . . . 19 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c 1c
36223, 198, 21otkelins2k 4256 . . . . . . . . . . . . . . . . . . . 20 Ins2k k k k k
363 eldif 3222 . . . . . . . . . . . . . . . . . . . 20 k k k k
364 opkelidkg 4275 . . . . . . . . . . . . . . . . . . . . . . 23 k
36523, 21, 364mp2an 653 . . . . . . . . . . . . . . . . . . . . . 22 k
366 equcom 1680 . . . . . . . . . . . . . . . . . . . . . 22
367365, 366bitri 240 . . . . . . . . . . . . . . . . . . . . 21 k
36823, 21opkelxpk 4249 . . . . . . . . . . . . . . . . . . . . . . . 24 k
36921, 368mpbiran2 885 . . . . . . . . . . . . . . . . . . . . . . 23 k
37023elsnc 3757 . . . . . . . . . . . . . . . . . . . . . . 23
371369, 370bitri 240 . . . . . . . . . . . . . . . . . . . . . 22 k
372371notbii 287 . . . . . . . . . . . . . . . . . . . . 21 k
373367, 372anbi12i 678 . . . . . . . . . . . . . . . . . . . 20 k k
374362, 363, 3733bitri 262 . . . . . . . . . . . . . . . . . . 19 Ins2k k k
375361, 374anbi12i 678 . . . . . . . . . . . . . . . . . 18 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k 1c
376196, 197, 3753bitri 262 . . . . . . . . . . . . . . . . 17 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k 1c
377376exbii 1582 . . . . . . . . . . . . . . . 16 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k 1c
378184, 192, 3773bitri 262 . . . . . . . . . . . . . . 15 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1c 1c
379 1cex 4143 . . . . . . . . . . . . . . . . 17 1c
380357, 379addcex 4395 . . . . . . . . . . . . . . . 16 1c
381 eqeq2 2362 . . . . . . . . . . . . . . . . 17 1c 1c
382 eqeq1 2359 . . . . . . . . . . . . . . . . . 18 1c 1c
383382notbid 285 . . . . . . . . . . . . . . . . 17 1c 1c
384381, 383anbi12d 691 . . . . . . . . . . . . . . . 16 1c 1c 1c
385380, 384ceqsexv 2895 . . . . . . . . . . . . . . 15 1c 1c 1c
386 annim 414 . . . . . . . . . . . . . . 15 1c 1c 1c 1c
387378, 385, 3863bitri 262 . . . . . . . . . . . . . 14 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1c 1c 1c
388387rexbii 2640 . . . . . . . . . . . . 13 Nn Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1c Nn 1c 1c
389182, 388bitri 240 . . . . . . . . . . . 12 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn Nn 1c 1c
390389notbii 287 . . . . . . . . . . 11 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn Nn 1c 1c
39121elcompl 3226 . . . . . . . . . . 11 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn
392 df-ne 2519 . . . . . . . . . . . . . . 15 1c 1c
393 df-ne 2519 . . . . . . . . . . . . . . 15 1c 1c
394392, 393imbi12i 316 . . . . . . . . . . . . . 14 1c 1c 1c 1c
395 con34b 283 . . . . . . . . . . . . . 14 1c 1c 1c 1c
396394, 395bitr4i 243 . . . . . . . . . . . . 13 1c 1c 1c 1c
397396ralbii 2639 . . . . . . . . . . . 12 Nn 1c 1c Nn 1c 1c
398 dfral2 2627 . . . . . . . . . . . 12 Nn 1c 1c Nn 1c 1c
399397, 398bitri 240 . . . . . . . . . . 11 Nn 1c 1c Nn 1c 1c
400390, 391, 3993bitr4i 268 . . . . . . . . . 10 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn Nn 1c 1c
401181, 400orbi12i 507 . . . . . . . . 9 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn Nn 1c 1c
402179, 180, 4013bitri 262 . . . . . . . 8 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k Nn 1c 1c
403177, 402anbi12i 678 . . . . . . 7 Ins3k Sk Ins2k Ins2k Sk Ins2k 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 1ck1 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k Nn 1c 1c
4044, 403bitri 240 . . . . . 6 Ins3k Sk Ins2k Ins2k Sk Ins2k 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 1ck1 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k Nn 1c 1c
405404exbii 1582 . . . . 5 Ins3k Sk Ins2k Ins2k Sk Ins2k 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 1ck1 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k Nn 1c 1c
4062, 2addcex 4395 . . . . . 6
407 eqeq1 2359 . . . . . . 7
408 neeq1 2525 . . . . . . . . 9 1c 1c
409408imbi2d 307 . . . . . . . 8 1c 1c 1c 1c
410409ralbidv 2635 . . . . . . 7 Nn 1c 1c Nn 1c 1c
411407, 410orbi12d 690 . . . . . 6 Nn 1c 1c Nn 1c 1c
412406, 411ceqsexv 2895 . . . . 5 Nn 1c 1c Nn 1c 1c
4133, 405, 4123bitri 262 . . . 4 Ins3k Sk Ins2k Ins2k Sk Ins2k 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 1ck1 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k k Nn 1c 1c
414 df-ne 2519 . . . . 5
415414imbi1i 315 . . . 4 Nn 1c 1c Nn 1c 1c
4161, 413, 4153bitr4i 268 . . 3 Ins3k Sk Ins2k Ins2k Sk Ins2k 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 1ck1 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k k Nn 1c 1c
417416abbi2i 2465 . 2 Ins3k Sk Ins2k Ins2k Sk Ins2k 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 1ck1 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k k Nn 1c 1c
418 ssetkex 4295 . . . . . . . 8 Sk
419418ins3kex 4309 . . . . . . 7 Ins3k Sk
420418ins2kex 4308 . . . . . . . . . 10 Ins2k Sk
421420ins2kex 4308 . . . . . . . . . . . 12 Ins2k Ins2k Sk
422419, 420inex 4106 . . . . . . . . . . . . . . . . . . 19 Ins3k Sk Ins2k Sk
423379pw1ex 4304 . . . . . . . . . . . . . . . . . . . 20 1 1c
424423pw1ex 4304 . . . . . . . . . . . . . . . . . . 19 1 1 1c
425422, 424imakex 4301 . . . . . . . . . . . . . . . . . 18 Ins3k Sk Ins2k Sk k1 1 1c
426425complex 4105 . . . . . . . . . . . . . . . . 17 Ins3k Sk Ins2k Sk k1 1 1c
427426sikex 4298 . . . . . . . . . . . . . . . 16 SIk Ins3k Sk Ins2k Sk k1 1 1c
428427sikex 4298 . . . . . . . . . . . . . . 15 SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
429428sikex 4298 . . . . . . . . . . . . . 14 SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
430429ins3kex 4309 . . . . . . . . . . . . 13 Ins3k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
431418sikex 4298 . . . . . . . . . . . . . . . . . . 19 SIk Sk
432431ins3kex 4309 . . . . . . . . . . . . . . . . . 18 Ins3k SIk Sk
433432ins2kex 4308 . . . . . . . . . . . . . . . . 17 Ins2k Ins3k SIk Sk
434433ins2kex 4308 . . . . . . . . . . . . . . . 16 Ins2k Ins2k Ins3k SIk Sk
435431sikex 4298 . . . . . . . . . . . . . . . . . . . . 21 SIk SIk Sk
436435sikex 4298 . . . . . . . . . . . . . . . . . . . 20 SIk SIk SIk Sk
437436sikex 4298 . . . . . . . . . . . . . . . . . . 19 SIk SIk SIk SIk Sk
438437sikex 4298 . . . . . . . . . . . . . . . . . 18 SIk SIk SIk SIk SIk Sk
439438ins3kex 4309 . . . . . . . . . . . . . . . . 17 Ins3k SIk SIk SIk SIk SIk Sk
440436ins3kex 4309 . . . . . . . . . . . . . . . . . 18 Ins3k SIk SIk SIk Sk
441440ins2kex 4308 . . . . . . . . . . . . . . . . 17 Ins2k Ins3k SIk SIk SIk Sk
442439, 441unex 4107 . . . . . . . . . . . . . . . 16 Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
443434, 442symdifex 4109 . . . . . . . . . . . . . . 15 Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
444424pw1ex 4304 . . . . . . . . . . . . . . . . . . 19 1 1 1 1c
445444pw1ex 4304 . . . . . . . . . . . . . . . . . 18 1 1 1 1 1c
446445pw1ex 4304 . . . . . . . . . . . . . . . . 17 1 1 1 1 1 1c
447446pw1ex 4304 . . . . . . . . . . . . . . . 16 1 1 1 1 1 1 1c
448447pw1ex 4304 . . . . . . . . . . . . . . 15 1 1 1 1 1 1 1 1c
449443, 448imakex 4301 . . . . . . . . . . . . . 14 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
450449complex 4105 . . . . . . . . . . . . 13 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
451430, 450inex 4106 . . . . . . . . . . . 12 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
452421, 451inex 4106 . . . . . . . . . . 11 Ins2k 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
453452, 445imakex 4301 . . . . . . . . . 10 Ins2k 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
454420, 453inex 4106 . . . . . . . . 9 Ins2k Sk Ins2k 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
455454, 424imakex 4301 . . . . . . . 8 Ins2k Sk Ins2k 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
456455ins2kex 4308 . . . . . . 7 Ins2k Ins2k Sk Ins2k 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
457419, 456symdifex 4109 . . . . . 6 Ins3k Sk Ins2k Ins2k Sk Ins2k 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
458457, 424imakex 4301 . . . . 5 Ins3k Sk Ins2k Ins2k Sk Ins2k 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 1ck1 1 1c
459458complex 4105 . . . 4 Ins3k Sk Ins2k Ins2k Sk Ins2k 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 1ck1 1 1c
460 snex 4112 . . . . . 6
461425sikex 4298 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 SIk Ins3k Sk Ins2k Sk k1 1 1c
462461sikex 4298 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
463462sikex 4298 . . . . . . . . . . . . . . . . . . . . . . . . . 26 SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
464463cnvkex 4288 . . . . . . . . . . . . . . . . . . . . . . . . 25 k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
465464ins3kex 4309 . . . . . . . . . . . . . . . . . . . . . . . 24 Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
466465complex 4105 . . . . . . . . . . . . . . . . . . . . . . 23 Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c
467441, 439unex 4107 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
468434, 467symdifex 4109 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk
469468, 448imakex 4301 . . . . . . . . . . . . . . . . . . . . . . . 24 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
470469complex 4105 . . . . . . . . . . . . . . . . . . . . . . 23 Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
471466, 470inex 4106 . . . . . . . . . . . . . . . . . . . . . 22 Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
472421, 471inex 4106 . . . . . . . . . . . . . . . . . . . . 21 Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1c
473472, 445imakex 4301 . . . . . . . . . . . . . . . . . . . 20 Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
474420, 473inex 4106 . . . . . . . . . . . . . . . . . . 19 Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1c
475474, 424imakex 4301 . . . . . . . . . . . . . . . . . 18 Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
476475ins2kex 4308 . . . . . . . . . . . . . . . . 17 Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
477419, 476symdifex 4109 . . . . . . . . . . . . . . . 16 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1c
478477, 424imakex 4301 . . . . . . . . . . . . . . 15 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c
479478complex 4105 . . . . . . . . . . . . . 14 Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c
480479ins2kex 4308 . . . . . . . . . . . . 13 Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c
481 addcexlem 4383 . . . . . . . . . . . . . . . 16 Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1c
482481, 424imakex 4301 . . . . . . . . . . . . . . 15 Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
483482imagekex 4313 . . . . . . . . . . . . . 14 Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
484483ins3kex 4309 . . . . . . . . . . . . 13 Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
485480, 484inex 4106 . . . . . . . . . . . 12 Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
486485, 423imakex 4301 . . . . . . . . . . 11 Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c
487486ins3kex 4309 . . . . . . . . . 10 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c
488 idkex 4315 . . . . . . . . . . . 12 k
489 vvex 4110 . . . . . . . . . . . . 13
490460, 489xpkex 4290 . . . . . . . . . . . 12 k
491488, 490difex 4108 . . . . . . . . . . 11 k k
492491ins2kex 4308 . . . . . . . . . 10 Ins2k k k
493487, 492inex 4106 . . . . . . . . 9 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k
494493, 423imakex 4301 . . . . . . . 8 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1c
495 nncex 4397 . . . . . . . 8 Nn
496494, 495imakex 4301 . . . . . . 7 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn
497496complex 4105 . . . . . 6 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn
498460, 497unex 4107 . . . . 5 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn
499498, 489xpkex 4290 . . . 4 Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k
500459, 499inex 4106 . . 3 Ins3k Sk Ins2k Ins2k Sk Ins2k 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 1ck1 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k
501500, 489imakex 4301 . 2 Ins3k Sk Ins2k Ins2k Sk Ins2k 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 1ck1 1 1c Ins3k Ins2k Ins3k Sk Ins2k Ins2k Sk Ins2k Ins2k Sk Ins3k k SIk SIk SIk Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Ins3k SIk Sk Ins2k Ins3k SIk SIk SIk Sk Ins3k SIk SIk SIk SIk SIk Sk k1 1 1 1 1 1 1 1ck1 1 1 1 1ck1 1 1ck1 1 1c Ins3k Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1 1c Ins2k k k k1 1ck Nn k k
502417, 501eqeltrri 2424 1 Nn 1c 1c
Colors of variables: wff setvar class
Syntax hints:   wn 3   wi 4   wb 176   wo 357   wa 358  wal 1540  wex 1541   wceq 1642   wcel 1710  cab 2339   wne 2517  wral 2615  wrex 2616  cvv 2860   ∼ ccompl 3206   cdif 3207   cun 3208   cin 3209   csymdif 3210  c0 3551  csn 3738  copk 4058  1cc1c 4135  1 cpw1 4136   k cxpk 4175  kccnvk 4176   Ins2k cins2k 4177   Ins3k cins3k 4178  kcimak 4180   SIk csik 4182  Imagekcimagek 4183   Sk cssetk 4184   k cidk 4185   Nn cnnc 4374   cplc 4376
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4079  ax-xp 4080  ax-cnv 4081  ax-1c 4082  ax-sset 4083  ax-si 4084  ax-ins2 4085  ax-ins3 4086  ax-typlower 4087  ax-sn 4088
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-v 2862  df-sbc 3048  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-symdif 3217  df-ss 3260  df-nul 3552  df-if 3664  df-pw 3725  df-sn 3742  df-pr 3743  df-uni 3893  df-int 3928  df-opk 4059  df-1c 4137  df-pw1 4138  df-uni1 4139  df-xpk 4186  df-cnvk 4187  df-ins2k 4188  df-ins3k 4189  df-imak 4190  df-cok 4191  df-p6 4192  df-sik 4193  df-ssetk 4194  df-imagek 4195  df-idk 4196  df-addc 4379  df-nnc 4380
This theorem is referenced by:  evenodddisj  4517
  Copyright terms: Public domain W3C validator