---

Step * 1 1 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
7. i : ℕ
8. i < ||mklist(n + m;f)||
9. i < n + m
⊢ mklist(n + m;f)[i] = mklist(n;f) @ mklist(m;λi.(f (n + i)))[i] ∈ T
BY
{ (Decide i < n THENA 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)||
9. i < n + m
10. i < n
⊢ mklist(n + m;f)[i] = mklist(n;f) @ mklist(m;λi.(f (n + i)))[i] ∈ T

2
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)||
9. i < n + m
10. ¬i < n
⊢ 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
7.  i  :  \mBbbN{}
8.  i  <  ||mklist(n  +  m;f)||
9.  i  <  n  +  m
\mvdash{}  mklist(n  +  m;f)[i]  =  mklist(n;f)  @  mklist(m;\mlambda{}i.(f  (n  +  i)))[i]


By

---

Latex:
(Decide  i  <  n  THENA  Auto)

---

Home Index