---

Step * 2 1 of Lemma mklist_select


1. T : Type
2. n : ℤ
3. 0 < n
4. ∀[f:ℕn - 1 ⟶ T]. ∀[i:ℕn - 1].  (mklist(n - 1;f)[i] = (f i) ∈ T)
5. [f] : ℕn ⟶ T
6. ∀[i:ℕn - 1]. (mklist(n - 1;f)[i] = (f i) ∈ T)
⊢ ∀[i:ℕn]. (mklist(n;f)[i] = (f i) ∈ T)
BY
{ ((Unfold `mklist` 0 THEN RWO "primrec-unroll" 0 THENA Auto) THEN AutoSplit) }

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)
⊢ ∀[i:ℕn]. (primrec(n - 1;[];λi,l. (l @ [f i])) @ [f (n - 1)][i] = (f i) ∈ T)

---

Latex:

---

Latex:

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


By

---

Latex:
((Unfold  `mklist`  0  THEN  RWO  "primrec-unroll"  0  THENA  Auto)  THEN  AutoSplit)

---

Home Index