---

Step * of Lemma nth_tl-append

∀[as:Top List]. ∀[bs:Top].
  ∀n:ℕ. (nth_tl(n;as @ bs) ~ if n <z ||as|| then nth_tl(n;as) @ bs else nth_tl(n - ||as||;bs) fi )
BY
{ (InductionOnList⋅ THEN Reduce 0) }

1
∀[bs:Top]. ∀n:ℕ. (nth_tl(n;bs) ~ if n <z 0 then nth_tl(n;[]) @ bs else nth_tl(n - 0;bs) fi )

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

---

Latex:

---

Latex:
\mforall{}[as:Top  List].  \mforall{}[bs:Top].
    \mforall{}n:\mBbbN{}.  (nth\_tl(n;as  @  bs)  \msim{}  if  n  <z  ||as||  then  nth\_tl(n;as)  @  bs  else  nth\_tl(n  -  ||as||;bs)  fi  )


By

---

Latex:
(InductionOnList\mcdot{}  THEN  Reduce  0)

---

Home Index