---

Step * of Lemma eval-mklist-sq

∀[T:Type]
  ∀[n,offset:ℕ]. ∀[f:{offset..n + offset-} ⟶ T].  (eval-mklist(n;f;offset) ~ mklist(n;λi.(f (i + offset)))) 
  supposing value-type(T)
BY
{ (Unfold `mklist` 0 THEN InductionOnNat THEN Auto) }

1
1. T : Type
2. value-type(T)
3. n : ℤ
4. offset : ℕ
5. f : {offset..0 + offset-} ⟶ T
⊢ eval-mklist(0;f;offset) ~ primrec(0;[];λi,l. (l @ [(λi.(f (i + offset))) i]))

2
1. T : Type
2. value-type(T)
3. n : ℤ
4. 0 < n
5. ∀[offset:ℕ]. ∀[f:{offset..(n - 1) + offset-} ⟶ T].
     (eval-mklist(n - 1;f;offset) ~ primrec(n - 1;[];λi,l. (l @ [(λi.(f (i + offset))) i])))
6. offset : ℕ
7. f : {offset..n + offset-} ⟶ T
⊢ eval-mklist(n;f;offset) ~ primrec(n;[];λi,l. (l @ [(λi.(f (i + offset))) i]))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}[n,offset:\mBbbN{}].  \mforall{}[f:\{offset..n  +  offset\msupminus{}\}  {}\mrightarrow{}  T].
        (eval-mklist(n;f;offset)  \msim{}  mklist(n;\mlambda{}i.(f  (i  +  offset)))) 
    supposing  value-type(T)


By

---

Latex:
(Unfold  `mklist`  0  THEN  InductionOnNat  THEN  Auto)

---

Home Index