Step | Hyp | Ref
| Expression |
1 | | df-addc 4378 |
. 2
![(](lp.gif) ![B](_cb.gif) ![{](lbrace.gif)
![E.](exists.gif) ![E.](exists.gif) ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) ![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) |
2 | | vex 2862 |
. . . . 5
![_V](rmcv.gif) |
3 | 2 | elimak 4259 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![B](_cb.gif) ![)](rp.gif) k![A](_ca.gif) ![E.](exists.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
4 | | opkex 4113 |
. . . . . . 7
![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif)
![_V](rmcv.gif) |
5 | 4 | elimak 4259 |
. . . . . 6
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![B](_cb.gif) ![E.](exists.gif) 1 1 ![B](_cb.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
6 | | elpw12 4145 |
. . . . . . . . . 10
![(](lp.gif) 1 1 ![E.](exists.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![)](rp.gif) |
7 | 6 | anbi1i 676 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) 1 1 ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif)
Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
8 | | r19.41v 2764 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif)
![(](lp.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif)
Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
9 | 7, 8 | bitr4i 243 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) 1 1 ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif)
Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
10 | 9 | exbii 1582 |
. . . . . . 7
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) 1 1 ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif)
![(](lp.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif)
Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
11 | | df-rex 2620 |
. . . . . . 7
![(](lp.gif) ![E.](exists.gif)
1 1 ![B](_cb.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif)
![E.](exists.gif) ![t](_t.gif) ![(](lp.gif)
1 1 ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
12 | | rexcom4 2878 |
. . . . . . 7
![(](lp.gif) ![E.](exists.gif)
![E.](exists.gif) ![t](_t.gif) ![(](lp.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif)
Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif)
![(](lp.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif)
Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
13 | 10, 11, 12 | 3bitr4i 268 |
. . . . . 6
![(](lp.gif) ![E.](exists.gif)
1 1 ![B](_cb.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif)
![E.](exists.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
14 | | snex 4111 |
. . . . . . . . 9
![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
15 | | opkeq1 4059 |
. . . . . . . . . 10
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![)](rp.gif) |
16 | 15 | eleq1d 2419 |
. . . . . . . . 9
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![(](lp.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
17 | 14, 16 | ceqsexv 2894 |
. . . . . . . 8
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif)
Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
18 | | eldif 3221 |
. . . . . . . 8
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif)
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
19 | | opkex 4113 |
. . . . . . . . . . . 12
![<<](llangle.gif) ![z](_z.gif) ![y](_y.gif)
![_V](rmcv.gif) |
20 | 19 | elcompl 3225 |
. . . . . . . . . . 11
![(](lp.gif) ![<<](llangle.gif) ![z](_z.gif) ![y](_y.gif) ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![<<](llangle.gif) ![z](_z.gif) ![y](_y.gif) ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) |
21 | | vex 2862 |
. . . . . . . . . . . . 13
![_V](rmcv.gif) |
22 | | vex 2862 |
. . . . . . . . . . . . 13
![_V](rmcv.gif) |
23 | 21, 22 | ndisjrelk 4323 |
. . . . . . . . . . . 12
![(](lp.gif) ![<<](llangle.gif) ![z](_z.gif) ![y](_y.gif) ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![y](_y.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
24 | 23 | necon2bbii 2572 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![y](_y.gif)
![<<](llangle.gif) ![z](_z.gif) ![y](_y.gif)
![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) |
25 | 20, 24 | bitr4i 243 |
. . . . . . . . . 10
![(](lp.gif) ![<<](llangle.gif) ![z](_z.gif) ![y](_y.gif) ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![y](_y.gif)
![(/)](varnothing.gif) ![)](rp.gif) |
26 | 21, 22, 2 | otkelins3k 4256 |
. . . . . . . . . 10
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![<<](llangle.gif) ![z](_z.gif) ![y](_y.gif) ∼ ![(](lp.gif)
Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) |
27 | | incom 3448 |
. . . . . . . . . . 11
![(](lp.gif) ![z](_z.gif) ![(](lp.gif) ![y](_y.gif) ![)](rp.gif) |
28 | 27 | eqeq1i 2360 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![z](_z.gif)
![(](lp.gif) ![y](_y.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
29 | 25, 26, 28 | 3bitr4i 268 |
. . . . . . . . 9
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![z](_z.gif)
![(/)](varnothing.gif) ![)](rp.gif) |
30 | | dfcleq 2347 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![z](_z.gif) ![A.](forall.gif) ![w](_w.gif) ![(](lp.gif)
![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
31 | | opkex 4113 |
. . . . . . . . . . . . . 14
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![_V](rmcv.gif) |
32 | 31 | elimak 4259 |
. . . . . . . . . . . . 13
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](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) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
33 | | df-rex 2620 |
. . . . . . . . . . . . 13
![(](lp.gif) ![E.](exists.gif)
1 1 1 1
1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](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) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
34 | | elpw141c 4150 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) 1 1 1 1 1c ![E.](exists.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![)](rp.gif) |
35 | 34 | anbi1i 676 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) 1 1 1 1
1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
36 | | 19.41v 1901 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![E.](exists.gif) ![w](_w.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
37 | 35, 36 | bitr4i 243 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) 1 1 1 1
1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![w](_w.gif) ![(](lp.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
38 | 37 | exbii 1582 |
. . . . . . . . . . . . . 14
![(](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) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![w](_w.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
39 | | excom 1741 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![E.](exists.gif) ![w](_w.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![w](_w.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
40 | 38, 39 | bitr4i 243 |
. . . . . . . . . . . . 13
![(](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) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![w](_w.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
41 | 32, 33, 40 | 3bitri 262 |
. . . . . . . . . . . 12
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c ![E.](exists.gif) ![w](_w.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
42 | | snex 4111 |
. . . . . . . . . . . . . . 15
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
43 | | opkeq1 4059 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![)](rp.gif) |
44 | 43 | eleq1d 2419 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![(](lp.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
45 | 42, 44 | ceqsexv 2894 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
46 | | elsymdif 3223 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif)
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins2k Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
47 | | snex 4111 |
. . . . . . . . . . . . . . . . . 18
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
48 | 47, 14, 4 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins2k Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif)
Ins2k Sk ![)](rp.gif) |
49 | | snex 4111 |
. . . . . . . . . . . . . . . . . 18
![{](lbrace.gif) ![w](_w.gif)
![_V](rmcv.gif) |
50 | 49, 22, 2 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif)
Ins2k Sk ![<<](llangle.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![x](_x.gif) Sk ![)](rp.gif) |
51 | | vex 2862 |
. . . . . . . . . . . . . . . . . 18
![_V](rmcv.gif) |
52 | 51, 2 | elssetk 4270 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![x](_x.gif) Sk ![x](_x.gif) ![)](rp.gif) |
53 | 48, 50, 52 | 3bitri 262 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins2k Sk ![x](_x.gif) ![)](rp.gif) |
54 | 47, 14, 4 | otkelins2k 4255 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins3k Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif)
Ins3k Sk ![)](rp.gif) |
55 | 49, 22, 2 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif)
Ins3k Sk ![<<](llangle.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![y](_y.gif) Sk ![)](rp.gif) |
56 | 51, 22 | elssetk 4270 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![y](_y.gif) Sk ![y](_y.gif) ![)](rp.gif) |
57 | 54, 55, 56 | 3bitri 262 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins3k Sk ![y](_y.gif) ![)](rp.gif) |
58 | 47, 14, 4 | otkelins3k 4256 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins3k SIk SIk Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) SIk SIk Sk ![)](rp.gif) |
59 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . 20
![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
60 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . 20
![{](lbrace.gif) ![z](_z.gif)
![_V](rmcv.gif) |
61 | 59, 60 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) SIk SIk Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) SIk Sk ![)](rp.gif) |
62 | 49, 21 | opksnelsik 4265 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) SIk Sk ![<<](llangle.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![z](_z.gif) Sk ![)](rp.gif) |
63 | 51, 21 | elssetk 4270 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![z](_z.gif) Sk ![z](_z.gif) ![)](rp.gif) |
64 | 62, 63 | bitri 240 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) SIk Sk ![z](_z.gif) ![)](rp.gif) |
65 | 58, 61, 64 | 3bitri 262 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins3k SIk SIk Sk ![z](_z.gif) ![)](rp.gif) |
66 | 57, 65 | orbi12i 507 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins3k Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins3k SIk SIk Sk ![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
67 | | elun 3220 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins3k Sk Ins3k SIk SIk Sk ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins3k Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) |
68 | | elun 3220 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![z](_z.gif) ![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
69 | 66, 67, 68 | 3bitr4i 268 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins3k Sk Ins3k SIk SIk Sk ![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
70 | 53, 69 | bibi12i 306 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins2k Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif)
![(](lp.gif)
![(](lp.gif)
![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
71 | 70 | notbii 287 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins2k Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif)
![(](lp.gif)
![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
72 | 45, 46, 71 | 3bitri 262 |
. . . . . . . . . . . . 13
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
73 | 72 | exbii 1582 |
. . . . . . . . . . . 12
![(](lp.gif) ![E.](exists.gif) ![w](_w.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![>>](rrangle.gif)
Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![(](lp.gif)
![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
74 | | exnal 1574 |
. . . . . . . . . . . 12
![(](lp.gif) ![E.](exists.gif) ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![A.](forall.gif) ![w](_w.gif) ![(](lp.gif)
![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
75 | 41, 73, 74 | 3bitri 262 |
. . . . . . . . . . 11
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c ![A.](forall.gif) ![w](_w.gif) ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
76 | 75 | con2bii 322 |
. . . . . . . . . 10
![(](lp.gif) ![A.](forall.gif) ![w](_w.gif) ![(](lp.gif)
![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) |
77 | 30, 76 | bitr2i 241 |
. . . . . . . . 9
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif)
![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c ![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
78 | 29, 77 | anbi12i 678 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif)
Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif) ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![z](_z.gif) ![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
79 | 17, 18, 78 | 3bitri 262 |
. . . . . . 7
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif)
Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![z](_z.gif)
![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
80 | 79 | rexbii 2639 |
. . . . . 6
![(](lp.gif) ![E.](exists.gif)
![E.](exists.gif) ![t](_t.gif) ![(](lp.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![>>](rrangle.gif)
Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) ![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
81 | 5, 13, 80 | 3bitri 262 |
. . . . 5
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![B](_cb.gif) ![E.](exists.gif) ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) ![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
82 | 81 | rexbii 2639 |
. . . 4
![(](lp.gif) ![E.](exists.gif)
![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif)
![(](lp.gif) Ins3k ∼
![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![B](_cb.gif) ![E.](exists.gif) ![E.](exists.gif) ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) ![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
83 | 3, 82 | bitri 240 |
. . 3
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![B](_cb.gif) ![)](rp.gif) k![A](_ca.gif) ![E.](exists.gif) ![E.](exists.gif) ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) ![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
84 | 83 | abbi2i 2464 |
. 2
![(](lp.gif) ![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![B](_cb.gif) ![)](rp.gif) k![A](_ca.gif) ![{](lbrace.gif)
![E.](exists.gif) ![E.](exists.gif) ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) ![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) |
85 | 1, 84 | eqtr4i 2376 |
1
![(](lp.gif) ![B](_cb.gif) ![(](lp.gif) ![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![B](_cb.gif) ![)](rp.gif) k![A](_ca.gif) ![)](rp.gif) |