---

Step * 2 1 3 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 < ||v|| + 1
⊢ nth_tl(n - 1;v @ bs) ~ nth_tl(n;[u / v]) @ bs
BY
{ (RW (AddrC [2;1] RecUnfoldTopAbC) 0 THEN AutoSplit)⋅ }

1
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

---

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.  n  <  ||v||  +  1
\mvdash{}  nth\_tl(n  -  1;v  @  bs)  \msim{}  nth\_tl(n;[u  /  v])  @  bs


By

---

Latex:
(RW  (AddrC  [2;1]  RecUnfoldTopAbC)  0  THEN  AutoSplit)\mcdot{}

---

Home Index