---

Step * of Lemma imax-class-val

∀[Info,T:Type]. ∀[f:T ─→ ℤ]. ∀[es:EO+(Info)]. ∀[lb:ℤ]. ∀[X:EClass(T)]. ∀[e:E(X)].
  ((maximum f[v] ≥ lb with v from X)(e) = imax-list([lb / map(λv.f[v];X(≤(X)(e)))]) ∈ ℤ)
BY
{ (Auto
   THEN Unfold `imax-class` 0
   THEN RWO "es-interface-accum-val" 0
   THEN Auto
   THEN RWW "is-interface-accum" 0⋅
   THEN Auto
   THEN RepUR ``imax-list eclass-vals`` 0
   THEN (RWO "map-map" 0 THENA Auto)
   THEN RepUR ``compose combine-list`` 0) }

1
1. Info : Type
2. T : Type
3. f : T ─→ ℤ
4. es : EO+(Info)
5. lb : ℤ
6. X : EClass(T)
7. e : E(X)
⊢ accumulate (with value b and list item e):
   imax(b;f[X(e)])
  over list:
    ≤(X)(e)
  with starting value:
   lb)
= accumulate (with value x and list item y):
   imax(x;y)
  over list:
    map(λx.f[X(x)];≤(X)(e))
  with starting value:
   lb)
∈ ℤ

---

Latex:

---

Latex:
\mforall{}[Info,T:Type].  \mforall{}[f:T  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[es:EO+(Info)].  \mforall{}[lb:\mBbbZ{}].  \mforall{}[X:EClass(T)].  \mforall{}[e:E(X)].
    ((maximum  f[v]  \mgeq{}  lb  with  v  from  X)(e)  =  imax-list([lb  /  map(\mlambda{}v.f[v];X(\mleq{}(X)(e)))]))


By

---

Latex:
(Auto
  THEN  Unfold  `imax-class`  0
  THEN  RWO  "es-interface-accum-val"  0
  THEN  Auto
  THEN  RWW  "is-interface-accum"  0\mcdot{}
  THEN  Auto
  THEN  RepUR  ``imax-list  eclass-vals``  0
  THEN  (RWO  "map-map"  0  THENA  Auto)
  THEN  RepUR  ``compose  combine-list``  0)

---

Home Index