---

Step * 2 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 : ℕ
⊢ nth_tl(n;[u / (v @ bs)]) ~ if n <z ||v|| + 1 then nth_tl(n;[u / v]) @ bs else nth_tl(n - ||v|| + 1;bs) fi 
BY
{ (RW (AddrC [1] RecUnfoldTopAbC) 0 THEN Reduce 0 THEN RepeatFor 2 (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 < ||v|| + 1
⊢ [u / (v @ bs)] ~ nth_tl(n;[u / v]) @ bs

2
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)

3
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

4
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)
⊢ nth_tl(n - 1;v @ bs) ~ nth_tl(n - ||v|| + 1;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{}
\mvdash{}  nth\_tl(n;[u  /  (v  @  bs)])  \msim{}  if  n  <z  ||v||  +  1
then  nth\_tl(n;[u  /  v])  @  bs
else  nth\_tl(n  -  ||v||  +  1;bs)
fi 


By

---

Latex:
(RW  (AddrC  [1]  RecUnfoldTopAbC)  0  THEN  Reduce  0  THEN  RepeatFor  2  (AutoSplit))

---

Home Index