---

Step * 2 1 1 1 of Lemma lg-remove_wf


1. x : ℕ
2. v : Top List@i
⊢ (||firstn(x;v)|| + ||nth_tl(x + 1;v)||) = if x <z ||v|| then ||v|| - 1 else ||v|| fi  ∈ ℤ
BY
{ AutoSplit }

1
1. x : ℕ
2. v : Top List@i
3. x < ||v||
⊢ (||firstn(x;v)|| + ||nth_tl(x + 1;v)||) = (||v|| - 1) ∈ ℤ

2
1. x : ℕ
2. v : Top List@i
3. ¬x < ||v||
⊢ (||firstn(x;v)|| + ||nth_tl(x + 1;v)||) = ||v|| ∈ ℤ

---

Latex:

---

Latex:

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


By

---

Latex:
AutoSplit

---

Home Index