---

Step * 1 1 1 of Lemma mklist-general-fun


1. T : Type
2. h : (T List) ⟶ T
3. n : ℤ
4. 0 < n
5. mklist-general(n - 1;h) ~ map(λn.mklist-general(n + 1;h)[n];upto(n - 1))
6. hide : Base
7. hide ~ λn,h. map(λn.mklist-general(n + 1;h)[n];upto(n))
⊢ [h mklist-general(n - 1;h)] ~ [(λn.mklist-general(n + 1;h)[n]) (n - 1)]
BY
{ (Reduce 0 THEN (Subst ⌜(n - 1) + 1 ~ n⌝ 0⋅ THENA Auto)) }

1
1. T : Type
2. h : (T List) ⟶ T
3. n : ℤ
4. 0 < n
5. mklist-general(n - 1;h) ~ map(λn.mklist-general(n + 1;h)[n];upto(n - 1))
6. hide : Base
7. hide ~ λn,h. map(λn.mklist-general(n + 1;h)[n];upto(n))
⊢ [h mklist-general(n - 1;h)] ~ [mklist-general(n;h)[n - 1]]

---

Latex:

---

Latex:

1.  T  :  Type
2.  h  :  (T  List)  {}\mrightarrow{}  T
3.  n  :  \mBbbZ{}
4.  0  <  n
5.  mklist-general(n  -  1;h)  \msim{}  map(\mlambda{}n.mklist-general(n  +  1;h)[n];upto(n  -  1))
6.  hide  :  Base
7.  hide  \msim{}  \mlambda{}n,h.  map(\mlambda{}n.mklist-general(n  +  1;h)[n];upto(n))
\mvdash{}  [h  mklist-general(n  -  1;h)]  \msim{}  [(\mlambda{}n.mklist-general(n  +  1;h)[n])  (n  -  1)]


By

---

Latex:
(Reduce  0  THEN  (Subst  \mkleeneopen{}(n  -  1)  +  1  \msim{}  n\mkleeneclose{}  0\mcdot{}  THENA  Auto))

---

Home Index