---

Step * 1 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)] ~ [mklist-general(n;h)[n - 1]]
BY
{ ((Subst ⌜mklist-general(n;h)[n - 1] ~ mklist-general(n;h)[||mklist-general(n;h)|| - 1]⌝ 0⋅
    THENA (RWO "mklist-general-length" 0 THEN Auto)
    )
   THEN Fold `last` 0
   ) }

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)] ~ [last(mklist-general(n;h))]

---

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{}  [mklist-general(n;h)[n  -  1]]


By

---

Latex:
((Subst  \mkleeneopen{}mklist-general(n;h)[n  -  1]  \msim{}  mklist-general(n;h)[||mklist-general(n;h)||  -  1]\mkleeneclose{}  0\mcdot{}
    THENA  (RWO  "mklist-general-length"  0  THEN  Auto)
    )
  THEN  Fold  `last`  0
  )

---

Home Index