---

Step * 1 of Lemma eval-mklist-sq


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]))
BY
{ Computation }

---

Latex:

---

Latex:

1.  T  :  Type
2.  value-type(T)
3.  n  :  \mBbbZ{}
4.  offset  :  \mBbbN{}
5.  f  :  \{offset..0  +  offset\msupminus{}\}  {}\mrightarrow{}  T
\mvdash{}  eval-mklist(0;f;offset)  \msim{}  primrec(0;[];\mlambda{}i,l.  (l  @  [(\mlambda{}i.(f  (i  +  offset)))  i]))


By

---

Latex:
Computation

---

Home Index