---

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


1. x : ℕ
2. v : Top List@i
3. ¬x < ||v||
⊢ (||firstn(x;v)|| + ||nth_tl(x + 1;v)||) = ||v|| ∈ ℤ
BY
{ ((RWO "nth_tl_is_nil firstn_all" 0 THENM Reduce 0) THEN Auto)⋅ }

---

Latex:

---

Latex:

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


By

---

Latex:
((RWO  "nth\_tl\_is\_nil  firstn\_all"  0  THENM  Reduce  0)  THEN  Auto)\mcdot{}

---

Home Index