---

Step * 1 of Lemma mklist-add


1. T : Type
2. n : ℕ
3. m : ℕ
4. f : ℕn + m ⟶ T
5. λi.(f (n + i)) ∈ ℕm ⟶ T
6. f ∈ ℕn ⟶ T
⊢ ∀i:ℕ. (i < ||mklist(n + m;f)|| ⇒ (mklist(n + m;f)[i] = mklist(n;f) @ mklist(m;λi.(f (n + i)))[i] ∈ T))
BY
{ Auto' }

1
1. T : Type
2. n : ℕ
3. m : ℕ
4. f : ℕn + m ⟶ T
5. λi.(f (n + i)) ∈ ℕm ⟶ T
6. f ∈ ℕn ⟶ T
7. i : ℕ
8. i < ||mklist(n + m;f)||
⊢ mklist(n + m;f)[i] = mklist(n;f) @ mklist(m;λi.(f (n + i)))[i] ∈ T

---

Latex:

---

Latex:

1.  T  :  Type
2.  n  :  \mBbbN{}
3.  m  :  \mBbbN{}
4.  f  :  \mBbbN{}n  +  m  {}\mrightarrow{}  T
5.  \mlambda{}i.(f  (n  +  i))  \mmember{}  \mBbbN{}m  {}\mrightarrow{}  T
6.  f  \mmember{}  \mBbbN{}n  {}\mrightarrow{}  T
\mvdash{}  \mforall{}i:\mBbbN{}
        (i  <  ||mklist(n  +  m;f)||  {}\mRightarrow{}  (mklist(n  +  m;f)[i]  =  mklist(n;f)  @  mklist(m;\mlambda{}i.(f  (n  +  i)))[i]))


By

---

Latex:
Auto'

---

Home Index