---

Step * 2 of Lemma select-mklist

.....upcase..... 
1. n : ℤ
2. 0 < n
3. ∀[f:ℕn - 1 ⟶ Top]. ∀[i:ℕn - 1].  (mklist(n - 1;f)[i] ~ f i)
⊢ ∀[f:ℕn ⟶ Top]. ∀[i:ℕn].  (mklist(n;f)[i] ~ f i)
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN Unfold `mklist` 0
   THEN RWO "primrec-unroll" 0 THENA Auto⋅
   THEN AutoSplit
   THEN Fold `mklist` 0) }

1
1. n : ℤ
2. n ≠ 0
3. 0 < n
4. ∀[f:ℕn - 1 ⟶ Top]. ∀[i:ℕn - 1].  (mklist(n - 1;f)[i] ~ f i)
5. f : ℕn ⟶ Top
6. i : ℕn
⊢ mklist(n - 1;f) @ [f (n - 1)][i] ~ f i

---

Latex:

---

Latex:
.....upcase..... 
1.  n  :  \mBbbZ{}
2.  0  <  n
3.  \mforall{}[f:\mBbbN{}n  -  1  {}\mrightarrow{}  Top].  \mforall{}[i:\mBbbN{}n  -  1].    (mklist(n  -  1;f)[i]  \msim{}  f  i)
\mvdash{}  \mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  Top].  \mforall{}[i:\mBbbN{}n].    (mklist(n;f)[i]  \msim{}  f  i)


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  Unfold  `mklist`  0
  THEN  RWO  "primrec-unroll"  0  THENA  Auto\mcdot{}
  THEN  AutoSplit
  THEN  Fold  `mklist`  0)

---

Home Index