---

Step * 1 of Lemma mklist-general-fun

.....upcase..... 
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))
⊢ mklist-general(n;h) ~ map(λn.mklist-general(n + 1;h)[n];upto(n))
BY
{ (AbbreviateTerm map(λn.mklist-general(n + 1;h)[n];upto(n)) `hide'⋅
   THEN RWO "mklist-general_add1" 0
   THEN Auto
   THEN HypSubst' (-1) 0
   THEN Reduce 0
   THEN (RWO "map-upto" 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))
⊢ mklist-general(n - 1;h) @ [h mklist-general(n - 1;h)] ~ map(λn.mklist-general(n + 1;h)[n];upto(n - 1))
@ [(λn.mklist-general(n + 1;h)[n]) (n - 1)]

---

Latex:

---

Latex:
.....upcase..... 
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))
\mvdash{}  mklist-general(n;h)  \msim{}  map(\mlambda{}n.mklist-general(n  +  1;h)[n];upto(n))


By

---

Latex:
(AbbreviateTerm  map(\mlambda{}n.mklist-general(n  +  1;h)[n];upto(n))  `hide'\mcdot{}
  THEN  RWO  "mklist-general\_add1"  0
  THEN  Auto
  THEN  HypSubst'  (-1)  0
  THEN  Reduce  0
  THEN  (RWO  "map-upto"  0  THENA  Auto))

---

Home Index