Step | Hyp | Ref
| Expression |
1 | | df-evenfin 4444 |
. . 3
Evenfin ![{](lbrace.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![n](_n.gif) ![(/)](varnothing.gif) ![)](rp.gif) ![}](rbrace.gif) |
2 | | eldifsn 3839 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) k Nn ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![(](lp.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) k Nn
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
3 | | vex 2862 |
. . . . . . . 8
![_V](rmcv.gif) |
4 | 3 | elimak 4259 |
. . . . . . 7
![(](lp.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) k Nn ![E.](exists.gif)
Nn ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ∼ ![(](lp.gif)
Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) |
5 | | opkex 4113 |
. . . . . . . . . . . 12
![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![_V](rmcv.gif) |
6 | 5 | elimak 4259 |
. . . . . . . . . . 11
![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![E.](exists.gif) 1 1 1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif)
Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
7 | | elpw121c 4148 |
. . . . . . . . . . . . . . 15
![(](lp.gif) 1 1 1c ![E.](exists.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![)](rp.gif) |
8 | 7 | anbi1i 676 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) 1 1
1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
9 | | 19.41v 1901 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
10 | 8, 9 | bitr4i 243 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) 1 1
1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
11 | 10 | exbii 1582 |
. . . . . . . . . . . 12
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) 1 1 1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif)
Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
12 | | df-rex 2620 |
. . . . . . . . . . . 12
![(](lp.gif) ![E.](exists.gif)
1 1
1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif)
![E.](exists.gif) ![t](_t.gif) ![(](lp.gif)
1 1 1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
13 | | excom 1741 |
. . . . . . . . . . . 12
![(](lp.gif) ![E.](exists.gif) ![a](_a.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif)
Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif)
Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
14 | 11, 12, 13 | 3bitr4i 268 |
. . . . . . . . . . 11
![(](lp.gif) ![E.](exists.gif)
1 1
1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif)
![E.](exists.gif) ![a](_a.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif)
Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
15 | | snex 4111 |
. . . . . . . . . . . . . 14
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
16 | | opkeq1 4059 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![)](rp.gif) |
17 | 16 | eleq1d 2419 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![(](lp.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
18 | 15, 17 | ceqsexv 2894 |
. . . . . . . . . . . . 13
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
19 | | elsymdif 3223 |
. . . . . . . . . . . . 13
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif)
Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif)
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins2k Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif)
Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
20 | | snex 4111 |
. . . . . . . . . . . . . . . . 17
![{](lbrace.gif) ![a](_a.gif)
![_V](rmcv.gif) |
21 | | vex 2862 |
. . . . . . . . . . . . . . . . 17
![_V](rmcv.gif) |
22 | 20, 21, 3 | otkelins2k 4255 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif)
Ins2k Sk ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![x](_x.gif) Sk ![)](rp.gif) |
23 | | vex 2862 |
. . . . . . . . . . . . . . . . 17
![_V](rmcv.gif) |
24 | 23, 3 | elssetk 4270 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![x](_x.gif) Sk ![x](_x.gif) ![)](rp.gif) |
25 | 22, 24 | bitri 240 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif)
Ins2k Sk ![x](_x.gif) ![)](rp.gif) |
26 | | opkex 4113 |
. . . . . . . . . . . . . . . . . 18
![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![_V](rmcv.gif) |
27 | 26 | elimak 4259 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c ![E.](exists.gif) 1 1 1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif)
![(](lp.gif) ![(](lp.gif)
Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) |
28 | | df-rex 2620 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![E.](exists.gif)
1 1
1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) 1 1 1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
29 | | elpw121c 4148 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) 1 1 1c ![E.](exists.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![)](rp.gif) |
30 | 29 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) 1 1
1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif)
![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
31 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![E.](exists.gif) ![c](_c.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif)
![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
32 | 30, 31 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) 1 1
1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif)
![E.](exists.gif) ![c](_c.gif) ![(](lp.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
33 | 32 | exbii 1582 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) 1 1 1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif)
![(](lp.gif) ![(](lp.gif)
Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif)
![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![c](_c.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif)
![(](lp.gif) ![(](lp.gif)
Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
34 | | excom 1741 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![E.](exists.gif) ![c](_c.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif)
![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![c](_c.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif)
![(](lp.gif) ![(](lp.gif)
Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
35 | 33, 34 | bitr4i 243 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) 1 1 1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif)
![(](lp.gif) ![(](lp.gif)
Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif)
![E.](exists.gif) ![c](_c.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif)
![(](lp.gif) ![(](lp.gif)
Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
36 | 27, 28, 35 | 3bitri 262 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c ![E.](exists.gif) ![c](_c.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
37 | 20, 21, 3 | otkelins3k 4256 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif)
Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) |
38 | | eladdc 4398 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![E.](exists.gif)
![E.](exists.gif)
![(](lp.gif) ![(](lp.gif) ![c](_c.gif) ![(](lp.gif) ![c](_c.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
39 | | r2ex 2652 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![E.](exists.gif)
![E.](exists.gif)
![(](lp.gif) ![(](lp.gif)
![c](_c.gif)
![(](lp.gif) ![c](_c.gif) ![)](rp.gif)
![E.](exists.gif) ![b](_b.gif) ![E.](exists.gif) ![c](_c.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif)
![c](_c.gif)
![(](lp.gif) ![c](_c.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
40 | | excom 1741 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![E.](exists.gif) ![b](_b.gif) ![E.](exists.gif) ![c](_c.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![c](_c.gif) ![(](lp.gif) ![c](_c.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![c](_c.gif) ![E.](exists.gif) ![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif)
![c](_c.gif)
![(](lp.gif) ![c](_c.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
41 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . 21
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
42 | | opkeq1 4059 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![)](rp.gif) |
43 | 42 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![(](lp.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
44 | 41, 43 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif)
![(](lp.gif) ![(](lp.gif)
Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) |
45 | | opkex 4113 |
. . . . . . . . . . . . . . . . . . . . . 22
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif)
![_V](rmcv.gif) |
46 | 45 | elimak 4259 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c ![E.](exists.gif) 1 1 1 1 1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
47 | | df-rex 2620 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![E.](exists.gif)
1 1 1 1
1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif)
1 1 1 1 1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
48 | | elpw141c 4150 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
![(](lp.gif) 1 1 1 1 1c ![E.](exists.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![)](rp.gif) |
49 | 48 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![(](lp.gif) 1 1 1 1
1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
50 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![E.](exists.gif) ![b](_b.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
51 | 49, 50 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . 23
![(](lp.gif) ![(](lp.gif) 1 1 1 1
1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![b](_b.gif) ![(](lp.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
52 | 51 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) 1 1 1 1 1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![b](_b.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
53 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![E.](exists.gif) ![b](_b.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![b](_b.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
54 | 52, 53 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) 1 1 1 1 1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![b](_b.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
55 | 46, 47, 54 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c ![E.](exists.gif) ![b](_b.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
56 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . 23
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
57 | | opkeq1 4059 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![)](rp.gif) |
58 | 57 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . 23
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![(](lp.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
59 | 56, 58 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
60 | | elin 3219 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
61 | | elin 3219 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
![(](lp.gif) k Ins2k Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
62 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
63 | 62, 41, 26 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) Ins2k
Sk ![)](rp.gif) |
64 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![{](lbrace.gif) ![b](_b.gif)
![_V](rmcv.gif) |
65 | 64, 20, 21 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) Ins2k
Sk ![<<](llangle.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![n](_n.gif) Sk ![)](rp.gif) |
66 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![_V](rmcv.gif) |
67 | 66, 21 | elssetk 4270 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![n](_n.gif) Sk ![n](_n.gif) ![)](rp.gif) |
68 | 63, 65, 67 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Sk ![n](_n.gif) ![)](rp.gif) |
69 | 56, 45 | opkelxpk 4248 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
![(](lp.gif) k Ins2k Sk ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) Ins2k Sk ![)](rp.gif) ![)](rp.gif) |
70 | 56, 69 | mpbiran 884 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
![(](lp.gif) k Ins2k Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) Ins2k Sk ![)](rp.gif) |
71 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![{](lbrace.gif) ![c](_c.gif)
![_V](rmcv.gif) |
72 | 71, 20, 21 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) Ins2k
Sk ![<<](llangle.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![n](_n.gif) Sk ![)](rp.gif) |
73 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![_V](rmcv.gif) |
74 | 73, 21 | elssetk 4270 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![n](_n.gif) Sk ![n](_n.gif) ![)](rp.gif) |
75 | 70, 72, 74 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
![(](lp.gif) k Ins2k Sk ![n](_n.gif) ![)](rp.gif) |
76 | 68, 75 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
![(](lp.gif) k Ins2k Sk ![)](rp.gif)
![(](lp.gif)
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
77 | 61, 76 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . 23
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
![(](lp.gif)
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
78 | | elin 3219 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif)
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
79 | 62, 41, 26 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) |
80 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
81 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
82 | 80, 81 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif)
SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) |
83 | 64, 71 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![<<](llangle.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) |
84 | 66, 73 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif)
SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![<<](llangle.gif) ![b](_b.gif) ![c](_c.gif) ∼ ![(](lp.gif)
Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) |
85 | 66, 73 | ndisjrelk 4323 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
![(](lp.gif) ![<<](llangle.gif) ![b](_b.gif) ![c](_c.gif) ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![c](_c.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
86 | 85 | notbii 287 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
![(](lp.gif) ![<<](llangle.gif) ![b](_b.gif) ![c](_c.gif) ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![c](_c.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
87 | | opkex 4113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
![<<](llangle.gif) ![b](_b.gif) ![c](_c.gif)
![_V](rmcv.gif) |
88 | 87 | elcompl 3225 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
![(](lp.gif) ![<<](llangle.gif) ![b](_b.gif) ![c](_c.gif) ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![<<](llangle.gif) ![b](_b.gif) ![c](_c.gif) ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) |
89 | | df-ne 2518 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
![(](lp.gif) ![(](lp.gif) ![c](_c.gif)
![(](lp.gif) ![c](_c.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
90 | 89 | con2bii 322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
![(](lp.gif) ![(](lp.gif) ![c](_c.gif)
![(](lp.gif) ![c](_c.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
91 | 86, 88, 90 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![(](lp.gif) ![<<](llangle.gif) ![b](_b.gif) ![c](_c.gif) ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![c](_c.gif)
![(/)](varnothing.gif) ![)](rp.gif) |
92 | 83, 84, 91 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![c](_c.gif)
![(/)](varnothing.gif) ![)](rp.gif) |
93 | 79, 82, 92 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![c](_c.gif)
![(/)](varnothing.gif) ![)](rp.gif) |
94 | | opkex 4113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![_V](rmcv.gif) |
95 | 94 | elimak 4259 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c ![E.](exists.gif) 1 1 1 1 1 1 1 1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
96 | | elpw171c 4153 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
![(](lp.gif) 1 1 1 1 1 1 1 1c ![E.](exists.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![)](rp.gif) |
97 | 96 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
![(](lp.gif) ![(](lp.gif) 1 1 1 1 1 1 1
1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
98 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
99 | 97, 98 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
![(](lp.gif) ![(](lp.gif) 1 1 1 1 1 1 1
1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
100 | 99 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) 1 1 1 1 1 1 1 1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
101 | | df-rex 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
![(](lp.gif) ![E.](exists.gif)
1 1 1 1 1 1 1
1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif)
![E.](exists.gif) ![t](_t.gif) ![(](lp.gif)
1 1 1 1 1 1 1 1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
102 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
103 | 100, 101,
102 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
![(](lp.gif) ![E.](exists.gif)
1 1 1 1 1 1 1
1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif)
![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
104 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
105 | | opkeq1 4059 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![)](rp.gif) |
106 | 105 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![(](lp.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
107 | 104, 106 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
108 | | elsymdif 3223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif)
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Ins3k SIk Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
109 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![_V](rmcv.gif) |
110 | 109, 56, 45 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins2k Ins3k SIk Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins3k SIk Sk ![)](rp.gif) |
111 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
112 | 111, 41, 26 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins3k SIk Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif)
Ins3k SIk Sk ![)](rp.gif) |
113 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
114 | 113, 20, 21 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif)
Ins3k SIk Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) SIk Sk ![)](rp.gif) |
115 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![{](lbrace.gif) ![x](_x.gif)
![_V](rmcv.gif) |
116 | 115, 23 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) SIk Sk ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) Sk ![)](rp.gif) |
117 | 3, 23 | elssetk 4270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) Sk ![a](_a.gif) ![)](rp.gif) |
118 | 114, 116,
117 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif)
Ins3k SIk Sk ![a](_a.gif) ![)](rp.gif) |
119 | 110, 112,
118 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins2k Ins3k SIk Sk ![a](_a.gif) ![)](rp.gif) |
120 | 109, 56, 45 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins3k SIk SIk SIk SIk SIk Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) SIk SIk SIk SIk SIk Sk ![)](rp.gif) |
121 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
122 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
123 | 121, 122 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) SIk SIk SIk SIk SIk Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) SIk SIk SIk SIk Sk ![)](rp.gif) |
124 | 111, 62 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) SIk SIk SIk SIk Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
SIk SIk SIk Sk ![)](rp.gif) |
125 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
126 | 125, 80 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
SIk SIk SIk Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) SIk SIk Sk ![)](rp.gif) |
127 | 113, 64 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) SIk SIk Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) SIk Sk ![)](rp.gif) |
128 | 115, 66 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) SIk Sk ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![b](_b.gif) Sk ![)](rp.gif) |
129 | 3, 66 | elssetk 4270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![b](_b.gif) Sk ![b](_b.gif) ![)](rp.gif) |
130 | 127, 128,
129 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) SIk SIk Sk ![b](_b.gif) ![)](rp.gif) |
131 | 124, 126,
130 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) SIk SIk SIk SIk Sk ![b](_b.gif) ![)](rp.gif) |
132 | 120, 123,
131 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins3k SIk SIk SIk SIk SIk Sk ![b](_b.gif) ![)](rp.gif) |
133 | 109, 56, 45 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins3k SIk SIk SIk Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins3k SIk SIk SIk Sk ![)](rp.gif) |
134 | 111, 41, 26 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins3k SIk SIk SIk Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
SIk SIk SIk Sk ![)](rp.gif) |
135 | 125, 81 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
SIk SIk SIk Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) SIk SIk Sk ![)](rp.gif) |
136 | 113, 71 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) SIk SIk Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) SIk Sk ![)](rp.gif) |
137 | 115, 73 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) SIk Sk ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![c](_c.gif) Sk ![)](rp.gif) |
138 | 3, 73 | elssetk 4270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![c](_c.gif) Sk ![c](_c.gif) ![)](rp.gif) |
139 | 137, 138 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) SIk Sk ![c](_c.gif) ![)](rp.gif) |
140 | 135, 136,
139 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
SIk SIk SIk Sk ![c](_c.gif) ![)](rp.gif) |
141 | 133, 134,
140 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins3k SIk SIk SIk Sk ![c](_c.gif) ![)](rp.gif) |
142 | 132, 141 | orbi12i 507 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins3k SIk SIk SIk SIk SIk Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins3k SIk SIk SIk Sk ![(](lp.gif) ![c](_c.gif) ![)](rp.gif) ![)](rp.gif) |
143 | | elun 3220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins3k SIk SIk SIk SIk SIk Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) |
144 | | elun 3220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
![(](lp.gif) ![(](lp.gif) ![c](_c.gif) ![(](lp.gif) ![c](_c.gif) ![)](rp.gif) ![)](rp.gif) |
145 | 142, 143,
144 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![(](lp.gif) ![c](_c.gif) ![)](rp.gif) ![)](rp.gif) |
146 | 119, 145 | bibi12i 306 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Ins3k SIk Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif)
![(](lp.gif)
![(](lp.gif)
![c](_c.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
147 | 146 | notbii 287 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Ins3k SIk Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif)
![(](lp.gif)
![(](lp.gif) ![c](_c.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
148 | 107, 108,
147 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
![(](lp.gif) ![c](_c.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
149 | 148 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![(](lp.gif) ![(](lp.gif) ![c](_c.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
150 | 95, 103, 149 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c ![E.](exists.gif) ![(](lp.gif)
![(](lp.gif) ![c](_c.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
151 | 150 | notbii 287 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c ![E.](exists.gif) ![(](lp.gif)
![(](lp.gif) ![c](_c.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
152 | 94 | elcompl 3225 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) |
153 | | dfcleq 2347 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![(](lp.gif) ![(](lp.gif) ![c](_c.gif) ![A.](forall.gif) ![x](_x.gif) ![(](lp.gif)
![(](lp.gif) ![c](_c.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
154 | | alex 1572 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![(](lp.gif) ![A.](forall.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![c](_c.gif) ![)](rp.gif) ![E.](exists.gif) ![(](lp.gif)
![(](lp.gif) ![c](_c.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
155 | 153, 154 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![(](lp.gif) ![(](lp.gif) ![c](_c.gif) ![E.](exists.gif) ![(](lp.gif) ![(](lp.gif) ![c](_c.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
156 | 151, 152,
155 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c ![(](lp.gif) ![c](_c.gif) ![)](rp.gif) ![)](rp.gif) |
157 | 93, 156 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![c](_c.gif) ![(](lp.gif) ![c](_c.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
158 | 78, 157 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . 23
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![c](_c.gif) ![(](lp.gif) ![c](_c.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
159 | 77, 158 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![c](_c.gif) ![(](lp.gif) ![c](_c.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
160 | 59, 60, 159 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![c](_c.gif) ![(](lp.gif) ![c](_c.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
161 | 160 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![E.](exists.gif) ![b](_b.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![b](_b.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![c](_c.gif) ![(](lp.gif) ![c](_c.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
162 | 44, 55, 161 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif)
![E.](exists.gif) ![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![c](_c.gif) ![(](lp.gif) ![c](_c.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
163 | 162 | exbii 1582 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![E.](exists.gif) ![c](_c.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif)
![n](_n.gif) ![>>](rrangle.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif)
![E.](exists.gif) ![c](_c.gif) ![E.](exists.gif) ![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif)
![c](_c.gif)
![(](lp.gif) ![c](_c.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
164 | 40, 163 | bitr4i 243 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![E.](exists.gif) ![b](_b.gif) ![E.](exists.gif) ![c](_c.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![c](_c.gif) ![(](lp.gif) ![c](_c.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![c](_c.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
165 | 38, 39, 164 | 3bitri 262 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![E.](exists.gif) ![c](_c.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![c](_c.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![n](_n.gif) ![>>](rrangle.gif)
![(](lp.gif) ![(](lp.gif)
Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
166 | 36, 37, 165 | 3bitr4i 268 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif)
Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c ![(](lp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
167 | 25, 166 | bibi12i 306 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins2k Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif)
Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif)
![(](lp.gif)
![(](lp.gif)
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
168 | 167 | notbii 287 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins2k
Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif)
Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif)
![(](lp.gif)
![(](lp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
169 | 18, 19, 168 | 3bitri 262 |
. . . . . . . . . . . 12
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
![(](lp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
170 | 169 | exbii 1582 |
. . . . . . . . . . 11
![(](lp.gif) ![E.](exists.gif) ![a](_a.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![a](_a.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![>>](rrangle.gif)
Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![(](lp.gif)
![(](lp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
171 | 6, 14, 170 | 3bitri 262 |
. . . . . . . . . 10
![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![E.](exists.gif) ![(](lp.gif)
![(](lp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
172 | 171 | notbii 287 |
. . . . . . . . 9
![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![E.](exists.gif) ![(](lp.gif)
![(](lp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
173 | 5 | elcompl 3225 |
. . . . . . . . 9
![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) |
174 | | dfcleq 2347 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![A.](forall.gif) ![a](_a.gif) ![(](lp.gif)
![(](lp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
175 | | alex 1572 |
. . . . . . . . . 10
![(](lp.gif) ![A.](forall.gif) ![a](_a.gif) ![(](lp.gif)
![(](lp.gif) ![n](_n.gif) ![)](rp.gif) ![E.](exists.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
176 | 174, 175 | bitri 240 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![E.](exists.gif) ![(](lp.gif)
![(](lp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
177 | 172, 173,
176 | 3bitr4i 268 |
. . . . . . . 8
![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
178 | 177 | rexbii 2639 |
. . . . . . 7
![(](lp.gif) ![E.](exists.gif)
Nn ![<<](llangle.gif) ![n](_n.gif) ![x](_x.gif) ∼ ![(](lp.gif)
Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![E.](exists.gif) Nn ![(](lp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
179 | 4, 178 | bitri 240 |
. . . . . 6
![(](lp.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) k Nn ![E.](exists.gif)
Nn ![(](lp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
180 | 179 | anbi1i 676 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) k Nn
![(/)](varnothing.gif) ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![n](_n.gif) ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
181 | 2, 180 | bitri 240 |
. . . 4
![(](lp.gif) ![(](lp.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) k Nn ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![n](_n.gif) ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
182 | 181 | abbi2i 2464 |
. . 3
![(](lp.gif) ∼ ![(](lp.gif)
Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) k Nn ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![{](lbrace.gif)
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![n](_n.gif) ![(/)](varnothing.gif) ![)](rp.gif) ![}](rbrace.gif) |
183 | 1, 182 | eqtr4i 2376 |
. 2
Evenfin ![(](lp.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) k Nn ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) |
184 | | ssetkex 4294 |
. . . . . . . 8
Sk ![_V](rmcv.gif) |
185 | 184 | ins2kex 4307 |
. . . . . . 7
Ins2k Sk ![_V](rmcv.gif) |
186 | 185 | ins2kex 4307 |
. . . . . . . . . . . 12
Ins2k Ins2k Sk ![_V](rmcv.gif) |
187 | | vvex 4109 |
. . . . . . . . . . . . 13
![_V](rmcv.gif) |
188 | 187, 185 | xpkex 4289 |
. . . . . . . . . . . 12
![(](lp.gif) k Ins2k Sk
![_V](rmcv.gif) |
189 | 186, 188 | inex 4105 |
. . . . . . . . . . 11
Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
![_V](rmcv.gif) |
190 | 184 | ins3kex 4308 |
. . . . . . . . . . . . . . . . . . 19
Ins3k Sk ![_V](rmcv.gif) |
191 | 190, 185 | inex 4105 |
. . . . . . . . . . . . . . . . . 18
Ins3k Sk Ins2k Sk
![_V](rmcv.gif) |
192 | | 1cex 4142 |
. . . . . . . . . . . . . . . . . . . 20
1c
![_V](rmcv.gif) |
193 | 192 | pw1ex 4303 |
. . . . . . . . . . . . . . . . . . 19
1
1c
![_V](rmcv.gif) |
194 | 193 | pw1ex 4303 |
. . . . . . . . . . . . . . . . . 18
1 1
1c
![_V](rmcv.gif) |
195 | 191, 194 | imakex 4300 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c
![_V](rmcv.gif) |
196 | 195 | complex 4104 |
. . . . . . . . . . . . . . . 16
∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c
![_V](rmcv.gif) |
197 | 196 | sikex 4297 |
. . . . . . . . . . . . . . 15
SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c
![_V](rmcv.gif) |
198 | 197 | sikex 4297 |
. . . . . . . . . . . . . 14
SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c
![_V](rmcv.gif) |
199 | 198 | sikex 4297 |
. . . . . . . . . . . . 13
SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c
![_V](rmcv.gif) |
200 | 199 | ins3kex 4308 |
. . . . . . . . . . . 12
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c
![_V](rmcv.gif) |
201 | 184 | sikex 4297 |
. . . . . . . . . . . . . . . . . 18
SIk Sk ![_V](rmcv.gif) |
202 | 201 | ins3kex 4308 |
. . . . . . . . . . . . . . . . 17
Ins3k SIk Sk ![_V](rmcv.gif) |
203 | 202 | ins2kex 4307 |
. . . . . . . . . . . . . . . 16
Ins2k Ins3k SIk Sk ![_V](rmcv.gif) |
204 | 203 | ins2kex 4307 |
. . . . . . . . . . . . . . 15
Ins2k Ins2k Ins3k SIk Sk ![_V](rmcv.gif) |
205 | 201 | sikex 4297 |
. . . . . . . . . . . . . . . . . . . 20
SIk SIk Sk ![_V](rmcv.gif) |
206 | 205 | sikex 4297 |
. . . . . . . . . . . . . . . . . . 19
SIk SIk SIk Sk ![_V](rmcv.gif) |
207 | 206 | sikex 4297 |
. . . . . . . . . . . . . . . . . 18
SIk SIk SIk SIk Sk ![_V](rmcv.gif) |
208 | 207 | sikex 4297 |
. . . . . . . . . . . . . . . . 17
SIk SIk SIk SIk SIk Sk ![_V](rmcv.gif) |
209 | 208 | ins3kex 4308 |
. . . . . . . . . . . . . . . 16
Ins3k SIk SIk SIk SIk SIk Sk ![_V](rmcv.gif) |
210 | 206 | ins3kex 4308 |
. . . . . . . . . . . . . . . . 17
Ins3k SIk SIk SIk Sk ![_V](rmcv.gif) |
211 | 210 | ins2kex 4307 |
. . . . . . . . . . . . . . . 16
Ins2k Ins3k SIk SIk SIk Sk ![_V](rmcv.gif) |
212 | 209, 211 | unex 4106 |
. . . . . . . . . . . . . . 15
Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk
![_V](rmcv.gif) |
213 | 204, 212 | symdifex 4108 |
. . . . . . . . . . . . . 14
Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif)
![_V](rmcv.gif) |
214 | 194 | pw1ex 4303 |
. . . . . . . . . . . . . . . . . 18
1 1 1
1c
![_V](rmcv.gif) |
215 | 214 | pw1ex 4303 |
. . . . . . . . . . . . . . . . 17
1 1 1 1
1c
![_V](rmcv.gif) |
216 | 215 | pw1ex 4303 |
. . . . . . . . . . . . . . . 16
1 1 1 1 1
1c
![_V](rmcv.gif) |
217 | 216 | pw1ex 4303 |
. . . . . . . . . . . . . . 15
1 1 1 1 1 1
1c
![_V](rmcv.gif) |
218 | 217 | pw1ex 4303 |
. . . . . . . . . . . . . 14
1 1 1 1 1 1 1
1c
![_V](rmcv.gif) |
219 | 213, 218 | imakex 4300 |
. . . . . . . . . . . . 13
![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c
![_V](rmcv.gif) |
220 | 219 | complex 4104 |
. . . . . . . . . . . 12
∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c
![_V](rmcv.gif) |
221 | 200, 220 | inex 4105 |
. . . . . . . . . . 11
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif)
![_V](rmcv.gif) |
222 | 189, 221 | inex 4105 |
. . . . . . . . . 10
![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![_V](rmcv.gif) |
223 | 222, 215 | imakex 4300 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c
![_V](rmcv.gif) |
224 | 223, 194 | imakex 4300 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c
![_V](rmcv.gif) |
225 | 224 | ins3kex 4308 |
. . . . . . 7
Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c
![_V](rmcv.gif) |
226 | 185, 225 | symdifex 4108 |
. . . . . 6
Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif)
![_V](rmcv.gif) |
227 | 226, 194 | imakex 4300 |
. . . . 5
![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c
![_V](rmcv.gif) |
228 | 227 | complex 4104 |
. . . 4
∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c
![_V](rmcv.gif) |
229 | | nncex 4396 |
. . . 4
Nn ![_V](rmcv.gif) |
230 | 228, 229 | imakex 4300 |
. . 3
∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) k Nn ![_V](rmcv.gif) |
231 | | snex 4111 |
. . 3
![{](lbrace.gif) ![(/)](varnothing.gif) ![_V](rmcv.gif) |
232 | 230, 231 | difex 4107 |
. 2
![(](lp.gif) ∼ ![(](lp.gif)
Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins2k Ins2k Sk ![(](lp.gif) k Ins2k Sk ![)](rp.gif)
Ins3k SIk SIk SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ∼ ![(](lp.gif) Ins2k Ins2k Ins3k SIk Sk Ins3k SIk SIk SIk SIk SIk Sk Ins2k Ins3k SIk SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) k Nn ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
233 | 183, 232 | eqeltri 2423 |
1
Evenfin ![_V](rmcv.gif) |