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

Theorem dfswap2 4733
Description: Express the Swap function via set construction operators. (Contributed by SF, 6-Jan-2015.)
Assertion
Ref Expression
dfswap2 Swap Ins2k Ins2k SSetk Ins2k Ins2k Ins3k SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk ImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k1 1 1 1 1 1 1c Ins2k Ins3k SIk SIk SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins3k Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1 1 1 1 1ck1 1 1 1 1ck1 1ck

Proof of Theorem dfswap2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opkex 4113 . . . . . . 7
21elimak 4259 . . . . . 6 Ins2k Ins2k SSetk Ins2k Ins2k Ins3k SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk ImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k1 1 1 1 1 1 1c Ins2k Ins3k SIk SIk SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins3k Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1 1 1 1 1ck1 1 1 1 1ck1 1c 1 1c Ins2k Ins2k SSetk Ins2k Ins2k Ins3k SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk ImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k1 1 1 1 1 1 1c Ins2k Ins3k SIk SIk SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins3k Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1 1 1 1 1ck1 1 1 1 1c
3 df-rex 2620 . . . . . 6 1 1c Ins2k Ins2k SSetk Ins2k Ins2k Ins3k SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk ImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k1 1 1 1 1 1 1c Ins2k Ins3k SIk SIk SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins3k Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1 1 1 1 1ck1 1 1 1 1c 1 1c Ins2k Ins2k SSetk Ins2k Ins2k Ins3k SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk ImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k1 1 1 1 1 1 1c Ins2k Ins3k SIk SIk SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins3k Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1 1 1 1 1ck1 1 1 1 1c
4 elpw11c 4147 . . . . . . . . . 10 1 1c
54anbi1i 676 . . . . . . . . 9 1 1c Ins2k Ins2k SSetk Ins2k Ins2k Ins3k SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk ImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k1 1 1 1 1 1 1c Ins2k Ins3k SIk SIk SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins3k Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Ins2k SSetk Ins2k Ins2k Ins3k SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk ImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k1 1 1 1 1 1 1c Ins2k Ins3k SIk SIk SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins3k Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1 1 1 1 1ck1 1 1 1 1c
6 19.41v 1901 . . . . . . . . 9 Ins2k Ins2k SSetk Ins2k Ins2k Ins3k SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk ImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k1 1 1 1 1 1 1c Ins2k Ins3k SIk SIk SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins3k Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Ins2k SSetk Ins2k Ins2k Ins3k SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk ImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k1 1 1 1 1 1 1c Ins2k Ins3k SIk SIk SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins3k Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1 1 1 1 1ck1 1 1 1 1c
75, 6bitr4i 243 . . . . . . . 8 1 1c Ins2k Ins2k SSetk Ins2k Ins2k Ins3k SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk ImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k1 1 1 1 1 1 1c Ins2k Ins3k SIk SIk SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins3k Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Ins2k SSetk Ins2k Ins2k Ins3k SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk ImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k1 1 1 1 1 1 1c Ins2k Ins3k SIk SIk SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins3k Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1 1 1 1 1ck1 1 1 1 1c
87exbii 1582 . . . . . . 7 1 1c Ins2k Ins2k SSetk Ins2k Ins2k Ins3k SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk ImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k1 1 1 1 1 1 1c Ins2k Ins3k SIk SIk SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins3k Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Ins2k SSetk Ins2k Ins2k Ins3k SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk ImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k1 1 1 1 1 1 1c Ins2k Ins3k SIk SIk SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins3k Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1 1 1 1 1ck1 1 1 1 1c
9 excom 1741 . . . . . . 7 Ins2k Ins2k SSetk Ins2k Ins2k Ins3k SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk ImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k1 1 1 1 1 1 1c Ins2k Ins3k SIk SIk SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins3k Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Ins2k SSetk Ins2k Ins2k Ins3k SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk ImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k1 1 1 1 1 1 1c Ins2k Ins3k SIk SIk SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins3k Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1 1 1 1 1ck1 1 1 1 1c
108, 9bitr4i 243 . . . . . 6 1 1c Ins2k Ins2k SSetk Ins2k Ins2k Ins3k SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk ImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k1 1 1 1 1 1 1c Ins2k Ins3k SIk SIk SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins3k Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Ins2k SSetk Ins2k Ins2k Ins3k SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk ImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k1 1 1 1 1 1 1c Ins2k Ins3k SIk SIk SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins3k Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1 1 1 1 1ck1 1 1 1 1c
112, 3, 103bitri 262 . . . . 5 Ins2k Ins2k SSetk Ins2k Ins2k Ins3k SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk ImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k1 1 1 1 1 1 1c Ins2k Ins3k SIk SIk SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins3k Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1 1 1 1 1ck1 1 1 1 1ck1 1c Ins2k Ins2k SSetk Ins2k Ins2k Ins3k SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk ImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k1 1 1 1 1 1 1c Ins2k Ins3k SIk SIk SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins3k Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1 1 1 1 1ck1 1 1 1 1c
12 snex 4111 . . . . . . . 8
13 opkeq1 4059 . . . . . . . . 9
1413eleq1d 2419 . . . . . . . 8 Ins2k Ins2k SSetk Ins2k Ins2k Ins3k SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk ImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k1 1 1 1 1 1 1c Ins2k Ins3k SIk SIk SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins3k Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Ins2k SSetk Ins2k Ins2k Ins3k SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk ImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k1 1 1 1 1 1 1c Ins2k Ins3k SIk SIk SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins3k Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1 1 1 1 1ck1 1 1 1 1c
1512, 14ceqsexv 2894 . . . . . . 7 Ins2k Ins2k SSetk Ins2k Ins2k Ins3k SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk ImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k1 1 1 1 1 1 1c Ins2k Ins3k SIk SIk SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins3k Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1 1 1 1 1ck1 1 1 1 1c Ins2k Ins2k SSetk Ins2k Ins2k Ins3k SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk ImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k1 1 1 1 1 1 1c Ins2k Ins3k SIk SIk SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins3k Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1 1 1 1 1ck1 1 1 1 1c
16 opkex 4113 . . . . . . . . . . . 12
1716elimak 4259 . . . . . . . . . . 11 Ins2k Ins2k SSetk Ins2k Ins2k Ins3k SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk ImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k1 1 1 1 1 1 1c Ins2k Ins3k SIk SIk SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins3k Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1 1 1 1 1ck1 1 1 1 1c 1 1 1 1 1c Ins2k Ins2k SSetk Ins2k Ins2k Ins3k SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk ImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k1 1 1 1 1 1 1c Ins2k Ins3k SIk SIk SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins3k Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1 1 1 1 1c
18 df-rex 2620 . . . . . . . . . . 11 1 1 1 1 1c Ins2k Ins2k SSetk Ins2k Ins2k Ins3k SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk ImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k1 1 1 1 1 1 1c Ins2k Ins3k SIk SIk SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins3k Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1 1 1 1 1c 1 1 1 1 1c Ins2k Ins2k SSetk Ins2k Ins2k Ins3k SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk ImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k1 1 1 1 1 1 1c Ins2k Ins3k SIk SIk SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins3k Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1 1 1 1 1c
19 elpw141c 4150 . . . . . . . . . . . . . . 15 1 1 1 1 1c
2019anbi1i 676 . . . . . . . . . . . . . 14 1 1 1 1 1c Ins2k Ins2k SSetk Ins2k Ins2k Ins3k SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk ImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k1 1 1 1 1 1 1c Ins2k Ins3k SIk SIk SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins2k Ins3k Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1c Ins3k SIk SIk SIk SIk SIk Ins2k SSetk Ins3k kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k k SSetk 0c k k1 1 1ck1 1 1 1 1 1 1c Ins2k Ins2k SSetk Ins2k Ins2k Ins3k SSetk k SIk kImagekImagek Ins3k Ins3k SSetk Ins2k SSetk k1 1 1c Ins2k Ins2k SSetk Ins2k Ins3k SSetk Ins3k SIk SIk SSetk k1 1 1 1 1ck1 1 1c Nn k k Nn k Ins3k SIk SIk Ins2k SSetk Ins3k SIk Ins2k SSetk Ins3k kImagekImagek Ins3k