---

Step * 2 of Lemma nth_tl-append


1. u : Top
2. v : Top List
3. ∀[bs:Top]. ∀n:ℕ. (nth_tl(n;v @ bs) ~ if n <z ||v|| then nth_tl(n;v) @ bs else nth_tl(n - ||v||;bs) fi )
⊢ ∀[bs:Top]
    ∀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
{ (ParallelLast THEN Auto) }

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 : ℕ
⊢ 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 

---

Latex:

---

Latex:

1.  u  :  Top
2.  v  :  Top  List
3.  \mforall{}[bs:Top]
          \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  )
\mvdash{}  \mforall{}[bs:Top]
        \mforall{}n:\mBbbN{}
            (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:
(ParallelLast  THEN  Auto)

---

Home Index