---

Step * of Lemma imax-list-as-reduce

∀[L:ℤ List]
  imax-list(L) = outl(reduce(λx,y. case y of inl(z) => inl imax(x;z) | inr(z) => inl x;inr ⋅ ;L)) ∈ ℤ supposing 0 < ||L|\000C|
BY
{ (Auto
   THEN (InstLemma `combine-list-as-reduce` [⌜ℤ⌝;⌜λx,y. imax(x;y)⌝;⌜L⌝]⋅
         THENA (Auto
                THEN RepUR ``assoc comm so_apply`` 0
                THEN Auto
                THEN (BLemma `imax_assoc`⋅ ORELSE BLemma `imax_com`)
                THEN Auto)
         )
   THEN RepUR ``so_apply`` -1
   THEN RevHypSubst' (-1) 0
   THEN Fold `imax-list` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[L:\mBbbZ{}  List]
    imax-list(L)  =  outl(reduce(\mlambda{}x,y.  case  y  of  inl(z)  =>  inl  imax(x;z)  |  inr(z)  =>  inl  x;inr  \mcdot{}  ;L)) 
    supposing  0  <  ||L||


By

---

Latex:
(Auto
  THEN  (InstLemma  `combine-list-as-reduce`  [\mkleeneopen{}\mBbbZ{}\mkleeneclose{};\mkleeneopen{}\mlambda{}x,y.  imax(x;y)\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}
              THENA  (Auto
                            THEN  RepUR  ``assoc  comm  so\_apply``  0
                            THEN  Auto
                            THEN  (BLemma  `imax\_assoc`\mcdot{}  ORELSE  BLemma  `imax\_com`)
                            THEN  Auto)
              )
  THEN  RepUR  ``so\_apply``  -1
  THEN  RevHypSubst'  (-1)  0
  THEN  Fold  `imax-list`  0
  THEN  Auto)

---

Home Index