---

Step * 2 1 3 1 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 ≤ 0)
7. ¬(n ≤ 0)
8. n < ||v|| + 1
⊢ nth_tl(n - 1;v @ bs) ~ nth_tl(n - 1;v) @ bs
BY
{ (RWO "4" 0 THEN Auto THEN AutoSplit) }

---

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  \mleq{}  0)
7.  \mneg{}(n  \mleq{}  0)
8.  n  <  ||v||  +  1
\mvdash{}  nth\_tl(n  -  1;v  @  bs)  \msim{}  nth\_tl(n  -  1;v)  @  bs


By

---

Latex:
(RWO  "4"  0  THEN  Auto  THEN  AutoSplit)

---

Home Index