Step | Hyp | Ref
| Expression |
1 | | efgval.w |
. . 3
Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) |
2 | | efgval.r |
. . 3
~FG ![` `](backtick.gif) ![I I](_ci.gif) ![) )](rp.gif) |
3 | | efgval2.m |
. . 3
![( (](lp.gif) ![I I](_ci.gif)
![<. <.](langle.gif) ![y y](_y.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ![)
)](rp.gif) |
4 | | efgval2.t |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![( (](lp.gif) splice ![<. <.](langle.gif) ![n n](_n.gif) ![n n](_n.gif) ![< <](langle.gif) ![" "](backquote.gif) ![w w](_w.gif) ![( (](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![w w](_w.gif) ![) )](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
5 | 1, 2, 3, 4 | efgval2 18137 |
. 2
![|^| |^|](bigcap.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![[ [](lbrack.gif) ![f f](_f.gif) ![] ]](rbrack.gif) ![r r](_r.gif) ![) )](rp.gif) ![} }](rbrace.gif) |
6 | | efgcpbllem.1 |
. . . . . . 7
![{ {](lbrace.gif) ![<. <.](langle.gif) ![i i](_i.gif) ![j j](_j.gif)
![( (](lp.gif) ![{ {](lbrace.gif) ![i
i](_i.gif) ![j j](_j.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![i i](_i.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![j j](_j.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![} }](rbrace.gif) |
7 | 6 | relopabi 5245 |
. . . . . 6
![L L](_cl.gif) |
8 | 7 | a1i 11 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif) ![L L](_cl.gif) ![) )](rp.gif) |
9 | | efgred.d |
. . . . . . . . 9
![( (](lp.gif) ![U_ U_](_cupbar.gif)
![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
10 | | efgred.s |
. . . . . . . . 9
![( (](lp.gif) ![{ {](lbrace.gif) Word ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![( (](lp.gif) ![t t](_t.gif) ![` `](backtick.gif) ![0
0](0.gif) ![A. A.](forall.gif) ![( (](lp.gif) ..^![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![t t](_t.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![t t](_t.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![( (](lp.gif) ![t t](_t.gif) ![` `](backtick.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![m m](_m.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![m m](_m.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
11 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 18167 |
. . . . . . . 8
![( (](lp.gif) ![f f](_f.gif) ![L L](_cl.gif)
![( (](lp.gif)
![( (](lp.gif) ![(
(](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![g g](_g.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
12 | 11 | simp2bi 1077 |
. . . . . . 7
![( (](lp.gif) ![f f](_f.gif) ![L L](_cl.gif) ![W W](_cw.gif) ![) )](rp.gif) |
13 | 12 | adantl 482 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![f f](_f.gif) ![L L](_cl.gif) ![g
g](_g.gif) ![W W](_cw.gif) ![) )](rp.gif) |
14 | 11 | simp1bi 1076 |
. . . . . . 7
![( (](lp.gif) ![f f](_f.gif) ![L L](_cl.gif) ![W W](_cw.gif) ![) )](rp.gif) |
15 | 14 | adantl 482 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![f f](_f.gif) ![L L](_cl.gif) ![g
g](_g.gif) ![W W](_cw.gif) ![) )](rp.gif) |
16 | 1, 2 | efger 18131 |
. . . . . . . 8
![W W](_cw.gif) |
17 | 16 | a1i 11 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![f f](_f.gif) ![L L](_cl.gif) ![g
g](_g.gif) ![W W](_cw.gif) ![) )](rp.gif) |
18 | 11 | simp3bi 1078 |
. . . . . . . 8
![( (](lp.gif) ![f f](_f.gif) ![L L](_cl.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![g g](_g.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
19 | 18 | adantl 482 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![f f](_f.gif) ![L L](_cl.gif) ![g
g](_g.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![g g](_g.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
20 | 17, 19 | ersym 7754 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![f f](_f.gif) ![L L](_cl.gif) ![g
g](_g.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![g g](_g.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
21 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 18167 |
. . . . . 6
![( (](lp.gif) ![g g](_g.gif) ![L L](_cl.gif)
![( (](lp.gif)
![( (](lp.gif) ![(
(](lp.gif) ++ ![g g](_g.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
22 | 13, 15, 20, 21 | syl3anbrc 1246 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![f f](_f.gif) ![L L](_cl.gif) ![g
g](_g.gif) ![g g](_g.gif) ![L L](_cl.gif) ![f f](_f.gif) ![) )](rp.gif) |
23 | 14 | ad2antrl 764 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![( (](lp.gif) ![f f](_f.gif) ![L L](_cl.gif) ![g g](_g.gif) ![L L](_cl.gif) ![h h](_h.gif) ![) )](rp.gif) ![W W](_cw.gif) ![)
)](rp.gif) |
24 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 18167 |
. . . . . . . 8
![( (](lp.gif) ![g g](_g.gif) ![L L](_cl.gif)
![( (](lp.gif)
![( (](lp.gif) ![(
(](lp.gif) ++ ![g g](_g.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![h h](_h.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
25 | 24 | simp2bi 1077 |
. . . . . . 7
![( (](lp.gif) ![g g](_g.gif) ![L L](_cl.gif) ![W W](_cw.gif) ![) )](rp.gif) |
26 | 25 | ad2antll 765 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![( (](lp.gif) ![f f](_f.gif) ![L L](_cl.gif) ![g g](_g.gif) ![L L](_cl.gif) ![h h](_h.gif) ![) )](rp.gif) ![W W](_cw.gif) ![)
)](rp.gif) |
27 | 16 | a1i 11 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![( (](lp.gif) ![f f](_f.gif) ![L L](_cl.gif) ![g g](_g.gif) ![L L](_cl.gif) ![h h](_h.gif) ![) )](rp.gif)
![W W](_cw.gif) ![)
)](rp.gif) |
28 | 18 | ad2antrl 764 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![( (](lp.gif) ![f f](_f.gif) ![L L](_cl.gif) ![g g](_g.gif) ![L L](_cl.gif) ![h h](_h.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![g g](_g.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
29 | 24 | simp3bi 1078 |
. . . . . . . 8
![( (](lp.gif) ![g g](_g.gif) ![L L](_cl.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![g g](_g.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![h h](_h.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
30 | 29 | ad2antll 765 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![( (](lp.gif) ![f f](_f.gif) ![L L](_cl.gif) ![g g](_g.gif) ![L L](_cl.gif) ![h h](_h.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![g g](_g.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![h h](_h.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
31 | 27, 28, 30 | ertrd 7758 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![( (](lp.gif) ![f f](_f.gif) ![L L](_cl.gif) ![g g](_g.gif) ![L L](_cl.gif) ![h h](_h.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![h h](_h.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
32 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 18167 |
. . . . . 6
![( (](lp.gif) ![f f](_f.gif) ![L L](_cl.gif)
![( (](lp.gif)
![( (](lp.gif) ![(
(](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![h h](_h.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
33 | 23, 26, 31, 32 | syl3anbrc 1246 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![( (](lp.gif) ![f f](_f.gif) ![L L](_cl.gif) ![g g](_g.gif) ![L L](_cl.gif) ![h h](_h.gif) ![) )](rp.gif) ![f f](_f.gif) ![L L](_cl.gif) ![h h](_h.gif) ![) )](rp.gif) |
34 | 16 | a1i 11 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![W W](_cw.gif) ![W W](_cw.gif) ![) )](rp.gif) |
35 | | fviss 6256 |
. . . . . . . . . . . . . 14
Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) |
36 | 1, 35 | eqsstri 3635 |
. . . . . . . . . . . . 13
Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) |
37 | | simpll 790 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![W W](_cw.gif) ![W W](_cw.gif) ![) )](rp.gif) |
38 | 36, 37 | sseldi 3601 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![W W](_cw.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) |
39 | | simpr 477 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![W W](_cw.gif) ![W W](_cw.gif) ![) )](rp.gif) |
40 | 36, 39 | sseldi 3601 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![W W](_cw.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) |
41 | | ccatcl 13359 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif)
Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![(
(](lp.gif) ++ ![f f](_f.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) |
42 | 38, 40, 41 | syl2anc 693 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![W W](_cw.gif) ![( (](lp.gif) ++ ![f f](_f.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) |
43 | | simplr 792 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![W W](_cw.gif) ![W W](_cw.gif) ![) )](rp.gif) |
44 | 36, 43 | sseldi 3601 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![W W](_cw.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) |
45 | | ccatcl 13359 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif)
Word ![(
(](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) |
46 | 42, 44, 45 | syl2anc 693 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![W W](_cw.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) |
47 | 1 | efgrcl 18128 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif)
Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
48 | 47 | simprd 479 |
. . . . . . . . . . 11
![( (](lp.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) |
49 | 48 | ad2antrr 762 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![W W](_cw.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) |
50 | 46, 49 | eleqtrrd 2704 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![W W](_cw.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![W W](_cw.gif) ![)
)](rp.gif) |
51 | 34, 50 | erref 7762 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![W W](_cw.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
52 | 51 | ex 450 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
53 | 52 | pm4.71d 666 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
54 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 18167 |
. . . . . . 7
![( (](lp.gif) ![f f](_f.gif) ![L L](_cl.gif)
![( (](lp.gif)
![( (](lp.gif) ![(
(](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
55 | | df-3an 1039 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
56 | | anidm 676 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif) ![W W](_cw.gif) ![) )](rp.gif) |
57 | 56 | anbi1i 731 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif)
![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
58 | 54, 55, 57 | 3bitri 286 |
. . . . . 6
![( (](lp.gif) ![f f](_f.gif) ![L L](_cl.gif)
![( (](lp.gif)
![( (](lp.gif) ![(
(](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
59 | 53, 58 | syl6bbr 278 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif) ![( (](lp.gif) ![f f](_f.gif) ![L L](_cl.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) |
60 | 8, 22, 33, 59 | iserd 7768 |
. . . 4
![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif) ![W W](_cw.gif) ![) )](rp.gif) |
61 | 1, 2, 3, 4 | efgtf 18135 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif)
![( (](lp.gif) splice ![<. <.](langle.gif) ![a a](_a.gif) ![a a](_a.gif) ![<
<](langle.gif) ![" "](backquote.gif) ![b b](_b.gif) ![( (](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![b b](_b.gif) ![) )](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![: :](colon.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![W W](_cw.gif) ![) )](rp.gif) ![) )](rp.gif) |
62 | 61 | simprd 479 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![T T](_ct.gif) ![`
`](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![: :](colon.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![W W](_cw.gif) ![) )](rp.gif) |
63 | 62 | adantl 482 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![W W](_cw.gif) ![( (](lp.gif) ![T T](_ct.gif) ![`
`](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![: :](colon.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![W W](_cw.gif) ![) )](rp.gif) |
64 | | ffn 6045 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![: :](colon.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif) ![T T](_ct.gif) ![`
`](backtick.gif) ![f f](_f.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
65 | | ovelrn 6810 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif)
![E. E.](exists.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![( (](lp.gif) ![c c](_c.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
66 | 63, 64, 65 | 3syl 18 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![T T](_ct.gif) ![`
`](backtick.gif) ![f f](_f.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![( (](lp.gif) ![c c](_c.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
67 | | simplr 792 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![W W](_cw.gif) ![) )](rp.gif) |
68 | 62 | ad2antlr 763 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![: :](colon.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![W W](_cw.gif) ![) )](rp.gif) |
69 | | simprl 794 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
70 | | simprr 796 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif)
![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) |
71 | 68, 69, 70 | fovrnd 6806 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![c c](_c.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![u u](_u.gif) ![W W](_cw.gif) ![) )](rp.gif) |
72 | 50 | adantr 481 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![W W](_cw.gif) ![) )](rp.gif) |
73 | 37 | adantr 481 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif)
![W W](_cw.gif) ![) )](rp.gif) |
74 | 36, 73 | sseldi 3601 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif)
Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) |
75 | 40 | adantr 481 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) Word
![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) |
76 | | swrdcl 13419 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif)
![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) Word
![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) substr
![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) |
78 | | ccatcl 13359 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![( (](lp.gif)
substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif)
![( (](lp.gif) ++ ![( (](lp.gif)
substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) ![) )](rp.gif) Word ![(
(](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) |
79 | 74, 77, 78 | syl2anc 693 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) ![)
)](rp.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) |
80 | 3 | efgmf 18126 |
. . . . . . . . . . . . . . . . . 18
![M M](_cm.gif) ![: :](colon.gif) ![(
(](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![-->
-->](longrightarrow.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) |
81 | 80 | ffvelrni 6358 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif)
![( (](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) |
82 | 81 | ad2antll 765 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) |
83 | 70, 82 | s2cld 13616 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![( (](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![" "](quote.gif) Word
![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) |
84 | | ccatcl 13359 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) ![)
)](rp.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![( (](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![" "](quote.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ++ ![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![( (](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) Word ![(
(](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) |
85 | 79, 83, 84 | syl2anc 693 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>.
>.](rangle.gif) ![) )](rp.gif) ++ ![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![(
(](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![)
)](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) |
86 | | swrdcl 13419 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif)
![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![>. >.](rangle.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) |
87 | 75, 86 | syl 17 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) substr
![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![>. >.](rangle.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) |
88 | 44 | adantr 481 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif)
Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) |
89 | | ccatass 13371 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>.
>.](rangle.gif) ![) )](rp.gif) ++ ![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![(
(](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![)
)](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![>. >.](rangle.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>.
>.](rangle.gif) ![) )](rp.gif) ++ ![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![(
(](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![)
)](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ++ ![( (](lp.gif)
substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) ![)
)](rp.gif) ++ ![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![(
(](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![)
)](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ++ ![( (](lp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![>. >.](rangle.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
90 | 85, 87, 88, 89 | syl3anc 1326 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif)
![c c](_c.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ++ ![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![( (](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![#
#](octothorpe.gif) ![`
`](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif)
![c c](_c.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ++ ![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![( (](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ++ ![( (](lp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![>. >.](rangle.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
91 | | ccatcl 13359 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![( (](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![" "](quote.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>.
>.](rangle.gif) ++
![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![(
(](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![)
)](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) |
92 | 77, 83, 91 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif)
![c c](_c.gif) ![>. >.](rangle.gif) ++ ![<
<](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![( (](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) |
93 | | ccatass 13371 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![( (](lp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif)
![c c](_c.gif) ![>. >.](rangle.gif) ++ ![<
<](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![( (](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![>. >.](rangle.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif)
![c c](_c.gif) ![>. >.](rangle.gif) ++ ![<
<](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![( (](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ![) )](rp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![#
#](octothorpe.gif) ![`
`](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>.
>.](rangle.gif) ++
![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![(
(](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![)
)](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ++ ![( (](lp.gif)
substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
94 | 74, 92, 87, 93 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) ![(
(](lp.gif) substr
![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) ++ ![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![(
(](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![)
)](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ![) )](rp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) ++ ![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![( (](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
95 | | ccatass 13371 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![( (](lp.gif)
substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![( (](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![" "](quote.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ++ ![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![( (](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ![( (](lp.gif) ++ ![( (](lp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>.
>.](rangle.gif) ++
![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![(
(](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![)
)](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
96 | 74, 77, 83, 95 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>.
>.](rangle.gif) ![) )](rp.gif) ++ ![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![(
(](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![)
)](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ![( (](lp.gif) ++ ![( (](lp.gif) ![(
(](lp.gif) substr
![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) ++ ![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![(
(](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![)
)](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
97 | 96 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ++ ![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![( (](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![#
#](octothorpe.gif) ![`
`](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>.
>.](rangle.gif) ++
![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![(
(](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![)
)](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ![) )](rp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
98 | 1, 2, 3, 4 | efgtval 18136 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![( (](lp.gif) ![c
c](_c.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![u u](_u.gif) ![( (](lp.gif) splice ![<. <.](langle.gif) ![c c](_c.gif) ![c c](_c.gif) ![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![( (](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ![>. >.](rangle.gif) ![)
)](rp.gif) ![) )](rp.gif) |
99 | 67, 69, 70, 98 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![c c](_c.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![u u](_u.gif) ![( (](lp.gif) splice ![<. <.](langle.gif) ![c c](_c.gif) ![c c](_c.gif) ![<
<](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![( (](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![) )](rp.gif) |
100 | | splval 13502 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif)
![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![( (](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![" "](quote.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) splice
![<. <.](langle.gif) ![c c](_c.gif) ![c c](_c.gif) ![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![(
(](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![)
)](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>.
>.](rangle.gif) ++
![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![(
(](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![)
)](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ++ ![( (](lp.gif)
substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
101 | 67, 69, 69, 83, 100 | syl13anc 1328 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) splice
![<. <.](langle.gif) ![c c](_c.gif) ![c c](_c.gif) ![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![(
(](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![)
)](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>.
>.](rangle.gif) ++
![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![(
(](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![)
)](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ++ ![( (](lp.gif)
substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
102 | 99, 101 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![c c](_c.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![u u](_u.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) ++ ![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![( (](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
103 | 102 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ++ ![( (](lp.gif) ![c c](_c.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![u u](_u.gif) ![) )](rp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif)
![c c](_c.gif) ![>. >.](rangle.gif) ++ ![<
<](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![( (](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
104 | 94, 97, 103 | 3eqtr4rd 2667 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ++ ![( (](lp.gif) ![c c](_c.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![u u](_u.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif)
![c c](_c.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ++ ![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![( (](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![#
#](octothorpe.gif) ![`
`](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
105 | 104 | oveq1d 6665 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) ![c
c](_c.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![u u](_u.gif) ![) )](rp.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif)
![c c](_c.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ++ ![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![( (](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![#
#](octothorpe.gif) ![`
`](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
106 | | lencl 13324 |
. . . . . . . . . . . . . . . . . . 19
![( (](lp.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif)
![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![NN0 NN0](_bbn0.gif) ![) )](rp.gif) |
107 | 74, 106 | syl 17 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![NN0 NN0](_bbn0.gif) ![) )](rp.gif) |
108 | | nn0uz 11722 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![0 0](0.gif) ![) )](rp.gif) |
109 | 107, 108 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![0 0](0.gif) ![)
)](rp.gif) ![) )](rp.gif) |
110 | | elfznn0 12433 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![NN0 NN0](_bbn0.gif) ![) )](rp.gif) |
111 | 110 | ad2antrl 764 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![NN0 NN0](_bbn0.gif) ![) )](rp.gif) |
112 | | uzaddcl 11744 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![0
0](0.gif) ![NN0 NN0](_bbn0.gif) ![( (](lp.gif) ![(
(](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![0 0](0.gif) ![) )](rp.gif) ![)
)](rp.gif) |
113 | 109, 111,
112 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![0 0](0.gif) ![)
)](rp.gif) ![) )](rp.gif) |
114 | 42 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ++ ![f f](_f.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) |
115 | | ccatlen 13360 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif)
Word ![(
(](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![#
#](octothorpe.gif) ![`
`](backtick.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ![) )](rp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
116 | 114, 88, 115 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ![) )](rp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
117 | | ccatlen 13360 |
. . . . . . . . . . . . . . . . . . . 20
![( (](lp.gif) ![( (](lp.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif)
Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![(
(](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
118 | 74, 75, 117 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
119 | | elfzuz3 12339 |
. . . . . . . . . . . . . . . . . . . . . 22
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![c c](_c.gif) ![) )](rp.gif) ![)
)](rp.gif) |
120 | 119 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . 21
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![c c](_c.gif) ![)
)](rp.gif) ![) )](rp.gif) |
121 | 107 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . . 21
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
122 | | eluzadd 11716 |
. . . . . . . . . . . . . . . . . . . . 21
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![(
(](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
123 | 120, 121,
122 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
124 | | lencl 13324 |
. . . . . . . . . . . . . . . . . . . . . . 23
![( (](lp.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif)
![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![NN0 NN0](_bbn0.gif) ![) )](rp.gif) |
125 | 75, 124 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![NN0 NN0](_bbn0.gif) ![) )](rp.gif) |
126 | 125 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . . . 21
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
127 | 107 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . . . 21
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
128 | 126, 127 | addcomd 10238 |
. . . . . . . . . . . . . . . . . . . 20
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
129 | 111 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . . . . 22
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
130 | 129, 127 | addcomd 10238 |
. . . . . . . . . . . . . . . . . . . . 21
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![#
#](octothorpe.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![#
#](octothorpe.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![) )](rp.gif) ![) )](rp.gif) |
131 | 130 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
132 | 123, 128,
131 | 3eltr3d 2715 |
. . . . . . . . . . . . . . . . . . 19
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
133 | 118, 132 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ![) )](rp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
134 | | lencl 13324 |
. . . . . . . . . . . . . . . . . . 19
![( (](lp.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif)
![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![NN0 NN0](_bbn0.gif) ![) )](rp.gif) |
135 | 88, 134 | syl 17 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![NN0 NN0](_bbn0.gif) ![) )](rp.gif) |
136 | | uzaddcl 11744 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ![) )](rp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![) )](rp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![NN0 NN0](_bbn0.gif) ![(
(](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ![) )](rp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![)
)](rp.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
137 | 133, 135,
136 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ![) )](rp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![)
)](rp.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
138 | 116, 137 | eqeltrd 2701 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![)
)](rp.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
139 | | elfzuzb 12336 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![0
0](0.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
140 | 113, 138,
139 | sylanbrc 698 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
141 | 1, 2, 3, 4 | efgtval 18136 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![#
#](octothorpe.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![) )](rp.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![u u](_u.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) splice ![<. <.](langle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![) )](rp.gif) ![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![( (](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![)
)](rp.gif) |
142 | 72, 140, 70, 141 | syl3anc 1326 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![) )](rp.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![u u](_u.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) splice ![<. <.](langle.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![) )](rp.gif) ![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![(
(](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![)
)](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![)
)](rp.gif) |
143 | | wrd0 13330 |
. . . . . . . . . . . . . . . 16
Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) |
144 | 143 | a1i 11 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) |
145 | | ccatcl 13359 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![>. >.](rangle.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![#
#](octothorpe.gif) ![`
`](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ++ ![B B](_cb.gif) Word ![(
(](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) |
146 | 87, 88, 145 | syl2anc 693 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![>. >.](rangle.gif) ++ ![B B](_cb.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) |
147 | | ccatrid 13370 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif)
![c c](_c.gif) ![>. >.](rangle.gif) ![) )](rp.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![(
(](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>.
>.](rangle.gif) ![) )](rp.gif) ++ ![(/) (/)](varnothing.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
148 | 79, 147 | syl 17 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>.
>.](rangle.gif) ![) )](rp.gif) ++ ![(/) (/)](varnothing.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
149 | 148 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ++ ![(/) (/)](varnothing.gif) ++ ![( (](lp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![#
#](octothorpe.gif) ![`
`](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ++ ![( (](lp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
150 | | ccatass 13371 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) ![)
)](rp.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![>. >.](rangle.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) ![)
)](rp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>.
>.](rangle.gif) ![) )](rp.gif) ++ ![( (](lp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![#
#](octothorpe.gif) ![`
`](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
151 | 79, 87, 88, 150 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif)
![c c](_c.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ++ ![( (](lp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
152 | | ccatass 13371 |
. . . . . . . . . . . . . . . . . . 19
![( (](lp.gif) ![( (](lp.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![( (](lp.gif)
substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![>. >.](rangle.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>.
>.](rangle.gif) ++
![( (](lp.gif) substr ![<. <.](langle.gif) ![c
c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
153 | 74, 77, 87, 152 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>.
>.](rangle.gif) ![) )](rp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif)
![c c](_c.gif) ![>. >.](rangle.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
154 | 111, 108 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . . . . 22
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![0
0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
155 | | eluzfz1 12348 |
. . . . . . . . . . . . . . . . . . . . . 22
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![0 0](0.gif)
![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![c c](_c.gif) ![)
)](rp.gif) ![) )](rp.gif) |
156 | 154, 155 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![c c](_c.gif) ![) )](rp.gif) ![) )](rp.gif) |
157 | 125, 108 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . . . . 22
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![0 0](0.gif) ![)
)](rp.gif) ![) )](rp.gif) |
158 | | eluzfz2 12349 |
. . . . . . . . . . . . . . . . . . . . . 22
![( (](lp.gif) ![( (](lp.gif) ![#
#](octothorpe.gif) ![`
`](backtick.gif) ![f f](_f.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![0 0](0.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
159 | 157, 158 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
160 | | ccatswrd 13456 |
. . . . . . . . . . . . . . . . . . . . 21
![( (](lp.gif) ![( (](lp.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![c c](_c.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![) )](rp.gif) |
161 | 75, 156, 69, 159, 160 | syl13anc 1328 |
. . . . . . . . . . . . . . . . . . . 20
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif)
![c c](_c.gif) ![>. >.](rangle.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![) )](rp.gif) |
162 | | swrdid 13428 |
. . . . . . . . . . . . . . . . . . . . 21
![( (](lp.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif)
![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ![f f](_f.gif) ![) )](rp.gif) |
163 | 75, 162 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) substr
![<. <.](langle.gif) ![0 0](0.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![>. >.](rangle.gif) ![f f](_f.gif) ![) )](rp.gif) |
164 | 161, 163 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif)
![c c](_c.gif) ![>. >.](rangle.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![f f](_f.gif) ![) )](rp.gif) |
165 | 164 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ++ ![( (](lp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>.
>.](rangle.gif) ++
![( (](lp.gif) substr ![<. <.](langle.gif) ![c
c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) |
166 | 153, 165 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>.
>.](rangle.gif) ![) )](rp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) |
167 | 166 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![)
)](rp.gif) ![) )](rp.gif) |
168 | 149, 151,
167 | 3eqtr2rd 2663 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ++ ![(/) (/)](varnothing.gif) ++ ![( (](lp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![#
#](octothorpe.gif) ![`
`](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
169 | | ccatlen 13360 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![( (](lp.gif)
substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif)
![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
170 | 74, 77, 169 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
171 | | swrd0len 13422 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) Word ![( (](lp.gif) ![2o 2o](_2o.gif)
![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) ![)
)](rp.gif) ![c c](_c.gif) ![) )](rp.gif) |
172 | 75, 69, 171 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) ![)
)](rp.gif) ![c c](_c.gif) ![) )](rp.gif) |
173 | 172 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![) )](rp.gif) ![) )](rp.gif) |
174 | 170, 173 | eqtr2d 2657 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
175 | | hash0 13158 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![(/) (/)](varnothing.gif) ![0 0](0.gif) |
176 | 175 | oveq2i 6661 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![#
#](octothorpe.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![0 0](0.gif) ![) )](rp.gif) |
177 | 107, 111 | nn0addcld 11355 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![NN0 NN0](_bbn0.gif) ![) )](rp.gif) |
178 | 177 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
179 | 178 | addid1d 10236 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![0 0](0.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![) )](rp.gif) ![) )](rp.gif) |
180 | 176, 179 | syl5req 2669 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![#
#](octothorpe.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
181 | 79, 144, 146, 83, 168, 174, 180 | splval2 13508 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) splice ![<. <.](langle.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![) )](rp.gif) ![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![(
(](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![)
)](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif)
![c c](_c.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ++ ![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![( (](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ++ ![( (](lp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![>. >.](rangle.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
182 | 142, 181 | eqtrd 2656 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![) )](rp.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![u u](_u.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) substr ![<. <.](langle.gif) ![0 0](0.gif) ![c c](_c.gif) ![>.
>.](rangle.gif) ![) )](rp.gif) ++ ![< <](langle.gif) ![" "](backquote.gif) ![u u](_u.gif) ![(
(](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![u u](_u.gif) ![)
)](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ++ ![( (](lp.gif) ![( (](lp.gif) substr ![<. <.](langle.gif) ![c c](_c.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![>. >.](rangle.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
183 | 90, 105, 182 | 3eqtr4d 2666 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) ![c
c](_c.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![u u](_u.gif) ![) )](rp.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![) )](rp.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) |
184 | 1, 2, 3, 4 | efgtf 18135 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) splice ![<. <.](langle.gif) ![a a](_a.gif) ![a a](_a.gif) ![< <](langle.gif) ![" "](backquote.gif) ![b b](_b.gif) ![( (](lp.gif) ![M M](_cm.gif) ![` `](backtick.gif) ![b b](_b.gif) ![) )](rp.gif) ![" "](quote.gif) ![> >](rangle.gif) ![>. >.](rangle.gif) ![)
)](rp.gif) ![( (](lp.gif) ![T T](_ct.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![: :](colon.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![W W](_cw.gif) ![) )](rp.gif) ![) )](rp.gif) |
185 | 184 | simprd 479 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![: :](colon.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![W W](_cw.gif) ![) )](rp.gif) |
186 | | ffn 6045 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![)
)](rp.gif) ![) )](rp.gif) ![: :](colon.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif) ![T T](_ct.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
187 | 72, 185, 186 | 3syl 18 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
188 | | fnovrn 6809 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![) )](rp.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![u u](_u.gif) ![( (](lp.gif) ![T T](_ct.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
189 | 187, 140,
70, 188 | syl3anc 1326 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![c c](_c.gif) ![) )](rp.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![u u](_u.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
190 | 183, 189 | eqeltrd 2701 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) ![c
c](_c.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![u u](_u.gif) ![) )](rp.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
191 | 1, 2, 3, 4 | efgi2 18138 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) ![c c](_c.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![u u](_u.gif) ![) )](rp.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![T T](_ct.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![( (](lp.gif) ![c c](_c.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![u u](_u.gif) ![) )](rp.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
192 | 72, 190, 191 | syl2anc 693 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ++ ![( (](lp.gif) ![c
c](_c.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![u u](_u.gif) ![) )](rp.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
193 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 18167 |
. . . . . . . . . 10
![( (](lp.gif) ![f f](_f.gif) ![L L](_cl.gif) ![( (](lp.gif) ![c c](_c.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![u u](_u.gif)
![( (](lp.gif)
![( (](lp.gif) ![c
c](_c.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![u u](_u.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![f f](_f.gif) ++ ![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif) ++ ![( (](lp.gif) ![c c](_c.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![u u](_u.gif) ![) )](rp.gif) ++ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
194 | 67, 71, 192, 193 | syl3anbrc 1246 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![f
f](_f.gif) ![L L](_cl.gif) ![( (](lp.gif) ![c c](_c.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) |
195 | | vex 3203 |
. . . . . . . . . . 11
![_V
_V](rmcv.gif) |
196 | | vex 3203 |
. . . . . . . . . . 11
![_V
_V](rmcv.gif) |
197 | 195, 196 | elec 7786 |
. . . . . . . . . 10
![( (](lp.gif) ![[ [](lbrack.gif) ![f f](_f.gif) ![] ]](rbrack.gif) ![f f](_f.gif) ![L L](_cl.gif) ![a a](_a.gif) ![) )](rp.gif) |
198 | | breq2 4657 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![c c](_c.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![u u](_u.gif) ![( (](lp.gif) ![f
f](_f.gif) ![L L](_cl.gif)
![f f](_f.gif) ![L L](_cl.gif) ![(
(](lp.gif) ![c c](_c.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
199 | 197, 198 | syl5bb 272 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![c c](_c.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![u u](_u.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![f f](_f.gif) ![] ]](rbrack.gif)
![f f](_f.gif) ![L L](_cl.gif) ![(
(](lp.gif) ![c c](_c.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
200 | 194, 199 | syl5ibrcom 237 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![c c](_c.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![u u](_u.gif) ![[ [](lbrack.gif) ![f
f](_f.gif) ![] ]](rbrack.gif) ![L L](_cl.gif) ![) )](rp.gif) ![) )](rp.gif) |
201 | 200 | rexlimdvva 3038 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![W W](_cw.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![0
0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![# #](octothorpe.gif) ![` `](backtick.gif) ![f f](_f.gif) ![)
)](rp.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![( (](lp.gif) ![c c](_c.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![u u](_u.gif) ![[ [](lbrack.gif) ![f
f](_f.gif) ![] ]](rbrack.gif) ![L L](_cl.gif) ![) )](rp.gif) ![) )](rp.gif) |
202 | 66, 201 | sylbid 230 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![T T](_ct.gif) ![`
`](backtick.gif) ![f f](_f.gif) ![[ [](lbrack.gif) ![f f](_f.gif) ![] ]](rbrack.gif) ![L L](_cl.gif) ![) )](rp.gif) ![) )](rp.gif) |
203 | 202 | ssrdv 3609 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![W W](_cw.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![[ [](lbrack.gif) ![f f](_f.gif) ![] ]](rbrack.gif) ![L L](_cl.gif) ![) )](rp.gif) |
204 | 203 | ralrimiva 2966 |
. . . 4
![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif)
![[ [](lbrack.gif) ![f f](_f.gif) ![] ]](rbrack.gif) ![L L](_cl.gif) ![) )](rp.gif) |
205 | | fvex 6201 |
. . . . . . 7
Word ![( (](lp.gif) ![2o 2o](_2o.gif) ![) )](rp.gif) ![_V _V](rmcv.gif) |
206 | 1, 205 | eqeltri 2697 |
. . . . . 6
![_V
_V](rmcv.gif) |
207 | | erex 7766 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif)
![_V _V](rmcv.gif) ![) )](rp.gif) ![) )](rp.gif) |
208 | 60, 206, 207 | mpisyl 21 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
209 | | ereq1 7749 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif) ![) )](rp.gif) ![) )](rp.gif) |
210 | | eceq2 7784 |
. . . . . . . . 9
![( (](lp.gif) ![[ [](lbrack.gif) ![f f](_f.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![f
f](_f.gif) ![] ]](rbrack.gif) ![L L](_cl.gif) ![) )](rp.gif) |
211 | 210 | sseq2d 3633 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif)
![[ [](lbrack.gif) ![f f](_f.gif) ![] ]](rbrack.gif)
![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![[ [](lbrack.gif) ![f f](_f.gif) ![] ]](rbrack.gif) ![L L](_cl.gif) ![) )](rp.gif) ![) )](rp.gif) |
212 | 211 | ralbidv 2986 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif)
![[ [](lbrack.gif) ![f f](_f.gif) ![] ]](rbrack.gif)
![A. A.](forall.gif)
![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![[ [](lbrack.gif) ![f f](_f.gif) ![] ]](rbrack.gif) ![L L](_cl.gif) ![) )](rp.gif) ![) )](rp.gif) |
213 | 209, 212 | anbi12d 747 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif)
![[ [](lbrack.gif) ![f f](_f.gif) ![] ]](rbrack.gif) ![r r](_r.gif)
![( (](lp.gif)
![A. A.](forall.gif)
![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![[ [](lbrack.gif) ![f f](_f.gif) ![] ]](rbrack.gif) ![L L](_cl.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
214 | 213 | elabg 3351 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif)
![{ {](lbrace.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![[ [](lbrack.gif) ![f f](_f.gif) ![] ]](rbrack.gif) ![r r](_r.gif) ![) )](rp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![[ [](lbrack.gif) ![f f](_f.gif) ![] ]](rbrack.gif) ![L L](_cl.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
215 | 208, 214 | syl 17 |
. . . 4
![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![[ [](lbrack.gif) ![f f](_f.gif) ![] ]](rbrack.gif) ![r r](_r.gif) ![) )](rp.gif)
![( (](lp.gif)
![A. A.](forall.gif)
![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![[ [](lbrack.gif) ![f f](_f.gif) ![] ]](rbrack.gif) ![L L](_cl.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
216 | 60, 204, 215 | mpbir2and 957 |
. . 3
![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif) ![[ [](lbrack.gif) ![f f](_f.gif) ![] ]](rbrack.gif) ![r r](_r.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
217 | | intss1 4492 |
. . 3
![( (](lp.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif)
![[ [](lbrack.gif) ![f f](_f.gif) ![] ]](rbrack.gif) ![r r](_r.gif) ![) )](rp.gif) ![|^| |^|](bigcap.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif)
![[ [](lbrack.gif) ![f f](_f.gif) ![] ]](rbrack.gif) ![r r](_r.gif) ![) )](rp.gif) ![L L](_cl.gif) ![) )](rp.gif) |
218 | 216, 217 | syl 17 |
. 2
![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif) ![|^| |^|](bigcap.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![T T](_ct.gif) ![` `](backtick.gif) ![f f](_f.gif)
![[ [](lbrack.gif) ![f f](_f.gif) ![] ]](rbrack.gif) ![r r](_r.gif) ![) )](rp.gif) ![L L](_cl.gif) ![) )](rp.gif) |
219 | 5, 218 | syl5eqss 3649 |
1
![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif)
![L L](_cl.gif) ![) )](rp.gif) |