---

Step * 2 1 1 1 1 of Lemma lg-remove_wf


1. x : ℕ
2. v : Top List@i
3. x < ||v||
⊢ (||firstn(x;v)|| + ||nth_tl(x + 1;v)||) = (||v|| - 1) ∈ ℤ
BY
{ (RWW "length_append length_firstn length_nth_tl" 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}
2.  v  :  Top  List@i
3.  x  <  ||v||
\mvdash{}  (||firstn(x;v)||  +  ||nth\_tl(x  +  1;v)||)  =  (||v||  -  1)


By

---

Latex:
(RWW  "length\_append  length\_firstn  length\_nth\_tl"  0  THEN  Auto)\mcdot{}

---

Home Index