---

Step * of Lemma nth_tl-mklist

∀[n:ℕ]. ∀[f:Top]. ∀[k:ℕ].  (nth_tl(k;mklist(n;f)) ~ mklist(n - k;λi.(f (i + k))))
BY
{ InductionOnNat }

1
.....basecase..... 
1. n : ℤ
⊢ ∀[f:Top]. ∀[k:ℕ].  (nth_tl(k;mklist(0;f)) ~ mklist(0 - k;λi.(f (i + k))))

2
.....upcase..... 
1. n : ℤ
2. 0 < n
3. ∀[f:Top]. ∀[k:ℕ].  (nth_tl(k;mklist(n - 1;f)) ~ mklist(n - 1 - k;λi.(f (i + k))))
⊢ ∀[f:Top]. ∀[k:ℕ].  (nth_tl(k;mklist(n;f)) ~ mklist(n - k;λi.(f (i + k))))

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f:Top].  \mforall{}[k:\mBbbN{}].    (nth\_tl(k;mklist(n;f))  \msim{}  mklist(n  -  k;\mlambda{}i.(f  (i  +  k))))


By

---

Latex:
InductionOnNat

---

Home Index