---

Step * 2 1 2 of Lemma nth_tl-append


1. u : Top
2. v : Top List
3. [bs] : Top
4. ∀n:ℕ. (nth_tl(n;v @ bs) ~ if n <z ||v|| then nth_tl(n;v) @ bs else nth_tl(n - ||v||;bs) fi )
5. n : ℕ
6. ¬n < ||v|| + 1
7. n ≤ 0
⊢ [u / (v @ bs)] ~ nth_tl(n - ||v|| + 1;bs)
BY
{ Auto' }

---

Latex:

---

Latex:

1.  u  :  Top
2.  v  :  Top  List
3.  [bs]  :  Top
4.  \mforall{}n:\mBbbN{}.  (nth\_tl(n;v  @  bs)  \msim{}  if  n  <z  ||v||  then  nth\_tl(n;v)  @  bs  else  nth\_tl(n  -  ||v||;bs)  fi  )
5.  n  :  \mBbbN{}
6.  \mneg{}n  <  ||v||  +  1
7.  n  \mleq{}  0
\mvdash{}  [u  /  (v  @  bs)]  \msim{}  nth\_tl(n  -  ||v||  +  1;bs)


By

---

Latex:
Auto'

---

Home Index