---

Step * of Lemma es-interface-accum-val

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[b,f:Top]. ∀[e:E].
  es-interface-accum(f;b;X)(e) ~ accumulate (with value b and list item e):
                                  f b X(e)
                                 over list:
                                   ≤(X)(e)
                                 with starting value:
                                  b) 
  supposing ↑e ∈b es-interface-accum(f;b;X)
BY
{ ((RepUR ``in-eclass eclass-val eclass es-interface-accum`` 0 THEN Auto)
   THEN MoveToConcl (-1)
   THEN AutoBoolCase ⌜(#(X es e) =z 1)⌝⋅) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].  \mforall{}[b,f:Top].  \mforall{}[e:E].
    es-interface-accum(f;b;X)(e)  \msim{}  accumulate  (with  value  b  and  list  item  e):
                                                                    f  b  X(e)
                                                                  over  list:
                                                                      \mleq{}(X)(e)
                                                                  with  starting  value:
                                                                    b) 
    supposing  \muparrow{}e  \mmember{}\msubb{}  es-interface-accum(f;b;X)


By

---

Latex:
((RepUR  ``in-eclass  eclass-val  eclass  es-interface-accum``  0  THEN  Auto)
  THEN  MoveToConcl  (-1)
  THEN  AutoBoolCase  \mkleeneopen{}(\#(X  es  e)  =\msubz{}  1)\mkleeneclose{}\mcdot{})

---

Home Index