---

Step * 2 1 1 of Lemma mklist_select


1. T : Type
2. n : ℤ
3. ¬n < 1
4. 0 < n
5. ∀[f:ℕn - 1 ⟶ T]. ∀[i:ℕn - 1].  (mklist(n - 1;f)[i] = (f i) ∈ T)
6. [f] : ℕn ⟶ T
7. ∀[i:ℕn - 1]. (mklist(n - 1;f)[i] = (f i) ∈ T)
⊢ ∀[i:ℕn]. (primrec(n - 1;[];λi,l. (l @ [f i])) @ [f (n - 1)][i] = (f i) ∈ T)
BY
{ (Fold `mklist` 0 THEN Intro) }

1
1. T : Type
2. n : ℤ
3. ¬n < 1
4. 0 < n
5. ∀[f:ℕn - 1 ⟶ T]. ∀[i:ℕn - 1].  (mklist(n - 1;f)[i] = (f i) ∈ T)
6. f : ℕn ⟶ T
7. ∀[i:ℕn - 1]. (mklist(n - 1;f)[i] = (f i) ∈ T)
8. i : ℕn
⊢ mklist(n - 1;f) @ [f (n - 1)][i] = (f i) ∈ T

---

Latex:

---

Latex:

1.  T  :  Type
2.  n  :  \mBbbZ{}
3.  \mneg{}n  <  1
4.  0  <  n
5.  \mforall{}[f:\mBbbN{}n  -  1  {}\mrightarrow{}  T].  \mforall{}[i:\mBbbN{}n  -  1].    (mklist(n  -  1;f)[i]  =  (f  i))
6.  [f]  :  \mBbbN{}n  {}\mrightarrow{}  T
7.  \mforall{}[i:\mBbbN{}n  -  1].  (mklist(n  -  1;f)[i]  =  (f  i))
\mvdash{}  \mforall{}[i:\mBbbN{}n].  (primrec(n  -  1;[];\mlambda{}i,l.  (l  @  [f  i]))  @  [f  (n  -  1)][i]  =  (f  i))


By

---

Latex:
(Fold  `mklist`  0  THEN  Intro)

---

Home Index