---

Step * 1 of Lemma imax-class-val


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)
∈ ℤ
BY
{ ((RWO "list_accum-map" 0 THENM Reduce 0) THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  T  :  Type
3.  f  :  T  {}\mrightarrow{}  \mBbbZ{}
4.  es  :  EO+(Info)
5.  lb  :  \mBbbZ{}
6.  X  :  EClass(T)
7.  e  :  E(X)
\mvdash{}  accumulate  (with  value  b  and  list  item  e):
      imax(b;f[X(e)])
    over  list:
        \mleq{}(X)(e)
    with  starting  value:
      lb)
=  accumulate  (with  value  x  and  list  item  y):
      imax(x;y)
    over  list:
        map(\mlambda{}x.f[X(x)];\mleq{}(X)(e))
    with  starting  value:
      lb)


By

---

Latex:
((RWO  "list\_accum-map"  0  THENM  Reduce  0)  THEN  Auto)\mcdot{}

---

Home Index