---

Step * 2 1 2 1 1 of Lemma nth_tl-mklist


1. f : Top
2. N : ℕ
⊢ mklist(N;f) ~ mklist(N - 0;λi.(f (i + 0)))
BY
{ (Unfold `mklist` 0 THEN NatInd (-1) THEN Reduce 0) }

1
1. f : Top
2. N : ℤ
⊢ [] ~ []

2
1. f : Top
2. N : ℤ
3. 0 < N
4. primrec(N - 1;[];λi,l. (l @ [f i])) ~ primrec(N - 1 - 0;[];λi,l. (l @ [(λi.(f (i + 0))) i]))
⊢ primrec(N;[];λi,l. (l @ [f i])) ~ primrec(N - 0;[];λi,l. (l @ [f (i + 0)]))

---

Latex:

---

Latex:

1.  f  :  Top
2.  N  :  \mBbbN{}
\mvdash{}  mklist(N;f)  \msim{}  mklist(N  -  0;\mlambda{}i.(f  (i  +  0)))


By

---

Latex:
(Unfold  `mklist`  0  THEN  NatInd  (-1)  THEN  Reduce  0)

---

Home Index