---

Step * 1 1 1 2 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
10. ¬i < n
⊢ mklist(n + m;f)[i] = mklist(m;λi.(f (n + i)))[i - n] ∈ T
BY
{ (Thin 6
   THEN ((RWW "mklist_select" 0⋅ THEN Reduce 0) THEN Auto THEN Try (Complete ((RWW "mklist_length" 0⋅ THEN Auto')))⋅)⋅
   ) }

---

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
10.  \mneg{}i  <  n
\mvdash{}  mklist(n  +  m;f)[i]  =  mklist(m;\mlambda{}i.(f  (n  +  i)))[i  -  n]


By

---

Latex:
(Thin  6
  THEN  ((RWW  "mklist\_select"  0\mcdot{}  THEN  Reduce  0)
              THEN  Auto
              THEN  Try  (Complete  ((RWW  "mklist\_length"  0\mcdot{}  THEN  Auto')))\mcdot{})\mcdot{}
  )

---

Home Index