Step | Hyp | Ref
| Expression |
1 | | elima 4754 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif)
![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Nn ![E.](exists.gif) Nn ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif)
![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![a](_a.gif) ![)](rp.gif) |
2 | | df-br 4640 |
. . . . . 6
![(](lp.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif)
![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif)
![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![<.](langle.gif) ![n](_n.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif)
![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif)
![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
3 | | elun 3220 |
. . . . . . . . 9
![(](lp.gif) ![<.](langle.gif) ![n](_n.gif)
![a](_a.gif) ![(](lp.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif)
![(](lp.gif) ![<.](langle.gif) ![n](_n.gif)
![a](_a.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![<.](langle.gif) ![n](_n.gif) ![a](_a.gif) ![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
4 | | nncdiv3lem1 6275 |
. . . . . . . . . 10
![(](lp.gif) ![<.](langle.gif) ![n](_n.gif)
![a](_a.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
5 | | elrn2 4897 |
. . . . . . . . . . 11
![(](lp.gif) ![<.](langle.gif) ![n](_n.gif)
![a](_a.gif) ![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![E.](exists.gif) ![b](_b.gif) ![<.](langle.gif) ![b](_b.gif) ![<.](langle.gif) ![n](_n.gif) ![a](_a.gif) ![>.](rangle.gif) ![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
6 | | oteltxp 5782 |
. . . . . . . . . . . . 13
![(](lp.gif) ![<.](langle.gif) ![b](_b.gif)
![<.](langle.gif) ![n](_n.gif) ![a](_a.gif) ![>.](rangle.gif) ![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![(](lp.gif) ![<.](langle.gif) ![b](_b.gif)
![n](_n.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![<.](langle.gif) ![b](_b.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
7 | | opelcnv 4893 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![<.](langle.gif) ![b](_b.gif)
![n](_n.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![<.](langle.gif) ![n](_n.gif) ![b](_b.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
8 | | nncdiv3lem1 6275 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![<.](langle.gif) ![n](_n.gif)
![b](_b.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
9 | 7, 8 | bitri 240 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![<.](langle.gif) ![b](_b.gif)
![n](_n.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
10 | | elrn2 4897 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![<.](langle.gif) ![b](_b.gif)
![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![E.](exists.gif) ![n](_n.gif) ![<.](langle.gif) ![n](_n.gif)
![<.](langle.gif) ![b](_b.gif) ![a](_a.gif) ![>.](rangle.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) |
11 | | oteltxp 5782 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![<.](langle.gif) ![n](_n.gif)
![<.](langle.gif) ![b](_b.gif) ![a](_a.gif) ![>.](rangle.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) AddC ![(](lp.gif) ![<.](langle.gif) ![n](_n.gif) ![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) ![<.](langle.gif) ![n](_n.gif) ![a](_a.gif) AddC ![)](rp.gif) ![)](rp.gif) |
12 | | elin 3219 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![<.](langle.gif) ![n](_n.gif)
![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) ![(](lp.gif) ![<.](langle.gif) ![n](_n.gif) ![b](_b.gif) ![<.](langle.gif) ![n](_n.gif)
![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
13 | | df-br 4640 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![n](_n.gif) ![1st](_1st.gif)
![<.](langle.gif) ![n](_n.gif) ![b](_b.gif) ![1st](_1st.gif) ![)](rp.gif) |
14 | 13 | bicomi 193 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![<.](langle.gif) ![n](_n.gif)
![b](_b.gif) ![n](_n.gif) ![1st](_1st.gif) ![b](_b.gif) ![)](rp.gif) |
15 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . 23
![_V](rmcv.gif) |
16 | | opelxp 4811 |
. . . . . . . . . . . . . . . . . . . . . . 23
![(](lp.gif) ![<.](langle.gif) ![n](_n.gif)
![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) |
17 | 15, 16 | mpbiran2 885 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![<.](langle.gif) ![n](_n.gif)
![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
18 | | eliniseg 5020 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![n](_n.gif) 1c![)](rp.gif) |
19 | 17, 18 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![<.](langle.gif) ![n](_n.gif)
![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![n](_n.gif) 1c![)](rp.gif) |
20 | 14, 19 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![<.](langle.gif) ![n](_n.gif) ![b](_b.gif) ![<.](langle.gif) ![n](_n.gif) ![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) ![(](lp.gif) ![n](_n.gif) ![1st](_1st.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) |
21 | | 1cex 4142 |
. . . . . . . . . . . . . . . . . . . . 21
1c
![_V](rmcv.gif) |
22 | 15, 21 | op1st2nd 5790 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![1st](_1st.gif) ![n](_n.gif) 1c ![<.](langle.gif) ![b](_b.gif)
1c![>.](rangle.gif) ![)](rp.gif) |
23 | 12, 20, 22 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![<.](langle.gif) ![n](_n.gif)
![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) ![<.](langle.gif) ![b](_b.gif) 1c![>.](rangle.gif) ![)](rp.gif) |
24 | | df-br 4640 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) AddC ![<.](langle.gif) ![n](_n.gif) ![a](_a.gif) AddC ![)](rp.gif) |
25 | 24 | bicomi 193 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![<.](langle.gif) ![n](_n.gif)
![a](_a.gif) AddC AddC ![a](_a.gif) ![)](rp.gif) |
26 | 23, 25 | anbi12i 678 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![<.](langle.gif) ![n](_n.gif) ![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) ![<.](langle.gif) ![n](_n.gif) ![a](_a.gif) AddC ![(](lp.gif) ![<.](langle.gif) ![b](_b.gif)
1c AddC ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
27 | 11, 26 | bitri 240 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![<.](langle.gif) ![n](_n.gif)
![<.](langle.gif) ![b](_b.gif) ![a](_a.gif) ![>.](rangle.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) AddC ![(](lp.gif)
![<.](langle.gif) ![b](_b.gif)
1c AddC ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
28 | 27 | exbii 1582 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![E.](exists.gif) ![n](_n.gif) ![<.](langle.gif) ![n](_n.gif) ![<.](langle.gif) ![b](_b.gif)
![a](_a.gif) ![>.](rangle.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) AddC ![E.](exists.gif) ![n](_n.gif) ![(](lp.gif) ![<.](langle.gif) ![b](_b.gif)
1c AddC ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
29 | 10, 28 | bitri 240 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![<.](langle.gif) ![b](_b.gif)
![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![E.](exists.gif) ![n](_n.gif) ![(](lp.gif) ![<.](langle.gif) ![b](_b.gif) 1c
AddC ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
30 | 15, 21 | opex 4588 |
. . . . . . . . . . . . . . . 16
![<.](langle.gif) ![b](_b.gif) 1c ![_V](rmcv.gif) |
31 | | breq1 4642 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![<.](langle.gif) ![b](_b.gif) 1c ![(](lp.gif) AddC ![<.](langle.gif) ![b](_b.gif) 1c AddC
![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
32 | 30, 31 | ceqsexv 2894 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![E.](exists.gif) ![n](_n.gif) ![(](lp.gif) ![<.](langle.gif) ![b](_b.gif)
1c AddC ![a](_a.gif) ![<.](langle.gif) ![b](_b.gif) 1c AddC ![a](_a.gif) ![)](rp.gif) |
33 | 15, 21 | braddcfn 5826 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![<.](langle.gif) ![b](_b.gif)
1c AddC ![(](lp.gif)
1c
![a](_a.gif) ![)](rp.gif) |
34 | | eqcom 2355 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
35 | 33, 34 | bitri 240 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![<.](langle.gif) ![b](_b.gif)
1c AddC ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
36 | 29, 32, 35 | 3bitri 262 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![<.](langle.gif) ![b](_b.gif)
![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) |
37 | 9, 36 | anbi12i 678 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![<.](langle.gif) ![b](_b.gif) ![n](_n.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![<.](langle.gif) ![b](_b.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
38 | 6, 37 | bitri 240 |
. . . . . . . . . . . 12
![(](lp.gif) ![<.](langle.gif) ![b](_b.gif)
![<.](langle.gif) ![n](_n.gif) ![a](_a.gif) ![>.](rangle.gif) ![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
39 | 38 | exbii 1582 |
. . . . . . . . . . 11
![(](lp.gif) ![E.](exists.gif) ![b](_b.gif) ![<.](langle.gif) ![b](_b.gif) ![<.](langle.gif) ![n](_n.gif)
![a](_a.gif) ![>.](rangle.gif) ![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif)
![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![E.](exists.gif) ![b](_b.gif) ![(](lp.gif)
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif)
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
40 | | vex 2862 |
. . . . . . . . . . . . . 14
![_V](rmcv.gif) |
41 | 40, 40 | addcex 4394 |
. . . . . . . . . . . . 13
![(](lp.gif) ![n](_n.gif) ![_V](rmcv.gif) |
42 | 41, 40 | addcex 4394 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![_V](rmcv.gif) |
43 | | addceq1 4383 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) |
44 | 43 | eqeq2d 2364 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
45 | 42, 44 | ceqsexv 2894 |
. . . . . . . . . . 11
![(](lp.gif) ![E.](exists.gif) ![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
![(](lp.gif) 1c![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) |
46 | 5, 39, 45 | 3bitri 262 |
. . . . . . . . . 10
![(](lp.gif) ![<.](langle.gif) ![n](_n.gif)
![a](_a.gif) ![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) |
47 | 4, 46 | orbi12i 507 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![<.](langle.gif) ![n](_n.gif) ![a](_a.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![<.](langle.gif) ![n](_n.gif) ![a](_a.gif) ![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
48 | 3, 47 | bitri 240 |
. . . . . . . 8
![(](lp.gif) ![<.](langle.gif) ![n](_n.gif)
![a](_a.gif) ![(](lp.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
49 | | elrn2 4897 |
. . . . . . . . 9
![(](lp.gif) ![<.](langle.gif) ![n](_n.gif)
![a](_a.gif) ![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![E.](exists.gif) ![b](_b.gif) ![<.](langle.gif) ![b](_b.gif) ![<.](langle.gif) ![n](_n.gif) ![a](_a.gif) ![>.](rangle.gif) ![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
50 | | oteltxp 5782 |
. . . . . . . . . . 11
![(](lp.gif) ![<.](langle.gif) ![b](_b.gif)
![<.](langle.gif) ![n](_n.gif) ![a](_a.gif) ![>.](rangle.gif) ![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![(](lp.gif) ![<.](langle.gif) ![b](_b.gif)
![n](_n.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![<.](langle.gif) ![b](_b.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
51 | | elrn2 4897 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![<.](langle.gif) ![b](_b.gif)
![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![E.](exists.gif) ![n](_n.gif) ![<.](langle.gif) ![n](_n.gif)
![<.](langle.gif) ![b](_b.gif) ![a](_a.gif) ![>.](rangle.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) |
52 | | oteltxp 5782 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![<.](langle.gif) ![n](_n.gif)
![<.](langle.gif) ![b](_b.gif) ![a](_a.gif) ![>.](rangle.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) AddC ![(](lp.gif) ![<.](langle.gif) ![n](_n.gif) ![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) ![<.](langle.gif) ![n](_n.gif) ![a](_a.gif) AddC ![)](rp.gif) ![)](rp.gif) |
53 | | elin 3219 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![<.](langle.gif) ![n](_n.gif)
![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) ![(](lp.gif) ![<.](langle.gif) ![n](_n.gif) ![b](_b.gif) ![<.](langle.gif) ![n](_n.gif)
![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
54 | | opelxp 4811 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![<.](langle.gif) ![n](_n.gif)
![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) |
55 | 15, 54 | mpbiran2 885 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![<.](langle.gif) ![n](_n.gif)
![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
56 | | eliniseg 5020 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![n](_n.gif) 2c![)](rp.gif) |
57 | 55, 56 | bitri 240 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![<.](langle.gif) ![n](_n.gif)
![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![n](_n.gif) 2c![)](rp.gif) |
58 | 14, 57 | anbi12i 678 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![<.](langle.gif) ![n](_n.gif) ![b](_b.gif) ![<.](langle.gif) ![n](_n.gif) ![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) ![(](lp.gif) ![n](_n.gif) ![1st](_1st.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) |
59 | | df-2c 6104 |
. . . . . . . . . . . . . . . . . . . 20
2c
Nc ![{](lbrace.gif) ![(/)](varnothing.gif) ![_V](rmcv.gif) ![}](rbrace.gif) |
60 | | ncex 6117 |
. . . . . . . . . . . . . . . . . . . 20
Nc ![{](lbrace.gif) ![(/)](varnothing.gif) ![_V](rmcv.gif) ![_V](rmcv.gif) |
61 | 59, 60 | eqeltri 2423 |
. . . . . . . . . . . . . . . . . . 19
2c
![_V](rmcv.gif) |
62 | 15, 61 | op1st2nd 5790 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![1st](_1st.gif) ![n](_n.gif) 2c ![<.](langle.gif) ![b](_b.gif)
2c![>.](rangle.gif) ![)](rp.gif) |
63 | 53, 58, 62 | 3bitri 262 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![<.](langle.gif) ![n](_n.gif)
![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) ![<.](langle.gif) ![b](_b.gif) 2c![>.](rangle.gif) ![)](rp.gif) |
64 | 63, 25 | anbi12i 678 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) ![<.](langle.gif) ![n](_n.gif) ![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) ![<.](langle.gif) ![n](_n.gif) ![a](_a.gif) AddC ![(](lp.gif) ![<.](langle.gif) ![b](_b.gif)
2c AddC ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
65 | 52, 64 | bitri 240 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![<.](langle.gif) ![n](_n.gif)
![<.](langle.gif) ![b](_b.gif) ![a](_a.gif) ![>.](rangle.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) AddC ![(](lp.gif)
![<.](langle.gif) ![b](_b.gif)
2c AddC ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
66 | 65 | exbii 1582 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![E.](exists.gif) ![n](_n.gif) ![<.](langle.gif) ![n](_n.gif) ![<.](langle.gif) ![b](_b.gif)
![a](_a.gif) ![>.](rangle.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) AddC ![E.](exists.gif) ![n](_n.gif) ![(](lp.gif) ![<.](langle.gif) ![b](_b.gif)
2c AddC ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
67 | 15, 61 | opex 4588 |
. . . . . . . . . . . . . . 15
![<.](langle.gif) ![b](_b.gif) 2c ![_V](rmcv.gif) |
68 | | breq1 4642 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![<.](langle.gif) ![b](_b.gif) 2c ![(](lp.gif) AddC ![<.](langle.gif) ![b](_b.gif) 2c AddC
![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
69 | 67, 68 | ceqsexv 2894 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![E.](exists.gif) ![n](_n.gif) ![(](lp.gif) ![<.](langle.gif) ![b](_b.gif)
2c AddC ![a](_a.gif) ![<.](langle.gif) ![b](_b.gif) 2c AddC ![a](_a.gif) ![)](rp.gif) |
70 | 51, 66, 69 | 3bitri 262 |
. . . . . . . . . . . . 13
![(](lp.gif) ![<.](langle.gif) ![b](_b.gif)
![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![<.](langle.gif) ![b](_b.gif) 2c AddC
![a](_a.gif) ![)](rp.gif) |
71 | 15, 61 | braddcfn 5826 |
. . . . . . . . . . . . 13
![(](lp.gif) ![<.](langle.gif) ![b](_b.gif)
2c AddC ![(](lp.gif)
2c
![a](_a.gif) ![)](rp.gif) |
72 | | eqcom 2355 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif)
2c
![(](lp.gif) 2c![)](rp.gif) ![)](rp.gif) |
73 | 70, 71, 72 | 3bitri 262 |
. . . . . . . . . . . 12
![(](lp.gif) ![<.](langle.gif) ![b](_b.gif)
![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![(](lp.gif)
2c![)](rp.gif) ![)](rp.gif) |
74 | 9, 73 | anbi12i 678 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![<.](langle.gif) ![b](_b.gif) ![n](_n.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![<.](langle.gif) ![b](_b.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif)
2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
75 | 50, 74 | bitri 240 |
. . . . . . . . . 10
![(](lp.gif) ![<.](langle.gif) ![b](_b.gif)
![<.](langle.gif) ![n](_n.gif) ![a](_a.gif) ![>.](rangle.gif) ![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif)
2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
76 | 75 | exbii 1582 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif) ![b](_b.gif) ![<.](langle.gif) ![b](_b.gif) ![<.](langle.gif) ![n](_n.gif)
![a](_a.gif) ![>.](rangle.gif) ![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif)
![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![E.](exists.gif) ![b](_b.gif) ![(](lp.gif)
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif)
![(](lp.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
77 | | addceq1 4383 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) 2c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) |
78 | 77 | eqeq2d 2364 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif)
2c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
79 | 42, 78 | ceqsexv 2894 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif) ![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
![(](lp.gif) 2c![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) |
80 | 49, 76, 79 | 3bitri 262 |
. . . . . . . 8
![(](lp.gif) ![<.](langle.gif) ![n](_n.gif)
![a](_a.gif) ![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) |
81 | 48, 80 | orbi12i 507 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![<.](langle.gif) ![n](_n.gif) ![a](_a.gif) ![(](lp.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif)
![<.](langle.gif) ![n](_n.gif) ![a](_a.gif) ![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
82 | | elun 3220 |
. . . . . . 7
![(](lp.gif) ![<.](langle.gif) ![n](_n.gif)
![a](_a.gif) ![(](lp.gif) ![(](lp.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif)
![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif)
![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![<.](langle.gif) ![n](_n.gif)
![a](_a.gif) ![(](lp.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif)
![<.](langle.gif) ![n](_n.gif) ![a](_a.gif) ![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
83 | | df-3or 935 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
84 | 81, 82, 83 | 3bitr4i 268 |
. . . . . 6
![(](lp.gif) ![<.](langle.gif) ![n](_n.gif)
![a](_a.gif) ![(](lp.gif) ![(](lp.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif)
![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif)
![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
85 | 2, 84 | bitri 240 |
. . . . 5
![(](lp.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif)
![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif)
![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
86 | 85 | rexbii 2639 |
. . . 4
![(](lp.gif) ![E.](exists.gif)
Nn ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif)
![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
87 | 1, 86 | bitri 240 |
. . 3
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif)
![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Nn ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
88 | 87 | abbi2i 2464 |
. 2
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif)
![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Nn ![{](lbrace.gif)
![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) |
89 | | 1stex 4739 |
. . . . . . . . . . . . . 14
![_V](rmcv.gif) |
90 | 89 | cnvex 5102 |
. . . . . . . . . . . . 13
![`'](_cnv.gif) ![_V](rmcv.gif) |
91 | | 2ndex 5112 |
. . . . . . . . . . . . . 14
![_V](rmcv.gif) |
92 | 89, 91 | inex 4105 |
. . . . . . . . . . . . 13
![(](lp.gif) ![2nd](_2nd.gif) ![_V](rmcv.gif) |
93 | 90, 92 | txpex 5785 |
. . . . . . . . . . . 12
![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![_V](rmcv.gif) |
94 | 93 | rnex 5107 |
. . . . . . . . . . 11
![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![_V](rmcv.gif) |
95 | 94, 91 | txpex 5785 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![_V](rmcv.gif) |
96 | | addcfnex 5824 |
. . . . . . . . . 10
AddC ![_V](rmcv.gif) |
97 | 95, 96 | imaex 4747 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![_V](rmcv.gif) |
98 | 97 | cnvex 5102 |
. . . . . . . 8
![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif)
![2nd](_2nd.gif) ![)](rp.gif) AddC ![_V](rmcv.gif) |
99 | 98 | ins3ex 5798 |
. . . . . . 7
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![_V](rmcv.gif) |
100 | 89, 89 | coex 4750 |
. . . . . . . . 9
![(](lp.gif) ![1st](_1st.gif) ![_V](rmcv.gif) |
101 | 91, 89 | coex 4750 |
. . . . . . . . . 10
![(](lp.gif) ![1st](_1st.gif) ![_V](rmcv.gif) |
102 | 101, 91 | txpex 5785 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![_V](rmcv.gif) |
103 | 100, 102 | txpex 5785 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![_V](rmcv.gif) |
104 | 103, 96 | imaex 4747 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![_V](rmcv.gif) |
105 | 99, 104 | inex 4105 |
. . . . . 6
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![_V](rmcv.gif) |
106 | 105 | rnex 5107 |
. . . . 5
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif)
![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![_V](rmcv.gif) |
107 | 106 | cnvex 5102 |
. . . . . . 7
![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![_V](rmcv.gif) |
108 | 91 | cnvex 5102 |
. . . . . . . . . . . 12
![`'](_cnv.gif) ![_V](rmcv.gif) |
109 | | snex 4111 |
. . . . . . . . . . . 12
1c ![_V](rmcv.gif) |
110 | 108, 109 | imaex 4747 |
. . . . . . . . . . 11
![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) |
111 | | vvex 4109 |
. . . . . . . . . . 11
![_V](rmcv.gif) |
112 | 110, 111 | xpex 5115 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![_V](rmcv.gif) |
113 | 89, 112 | inex 4105 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
![_V](rmcv.gif) |
114 | 113, 96 | txpex 5785 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![_V](rmcv.gif) |
115 | 114 | rnex 5107 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) AddC ![_V](rmcv.gif) |
116 | 107, 115 | txpex 5785 |
. . . . . 6
![(](lp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) AddC ![)](rp.gif)
![_V](rmcv.gif) |
117 | 116 | rnex 5107 |
. . . . 5
![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![_V](rmcv.gif) |
118 | 106, 117 | unex 4106 |
. . . 4
![(](lp.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![)](rp.gif) ![_V](rmcv.gif) |
119 | | snex 4111 |
. . . . . . . . . . 11
2c ![_V](rmcv.gif) |
120 | 108, 119 | imaex 4747 |
. . . . . . . . . 10
![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) |
121 | 120, 111 | xpex 5115 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![_V](rmcv.gif) |
122 | 89, 121 | inex 4105 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
![_V](rmcv.gif) |
123 | 122, 96 | txpex 5785 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![_V](rmcv.gif) |
124 | 123 | rnex 5107 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) AddC ![_V](rmcv.gif) |
125 | 107, 124 | txpex 5785 |
. . . . 5
![(](lp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) AddC ![)](rp.gif)
![_V](rmcv.gif) |
126 | 125 | rnex 5107 |
. . . 4
![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![_V](rmcv.gif) |
127 | 118, 126 | unex 4106 |
. . 3
![(](lp.gif) ![(](lp.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif)
![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![)](rp.gif) ![_V](rmcv.gif) |
128 | | nncex 4396 |
. . 3
Nn ![_V](rmcv.gif) |
129 | 127, 128 | imaex 4747 |
. 2
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif)
![(](lp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 2c![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif)
AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Nn ![_V](rmcv.gif) |
130 | 88, 129 | eqeltrri 2424 |
1
![{](lbrace.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![_V](rmcv.gif) |