---

Step * of Lemma accum-class-val

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[base,f:Top]. ∀[e:E].
  accum-class(a,x.f[a;x];x.base[x];X)(e) ~ accum_list(a,e.f[a;X(e)];e.base[X(e)];≤(X)(e)) 
  supposing ↑e ∈b accum-class(a,x.f[a;x];x.base[x];X)
BY
{ ((UnivCD THENA Auto)
   THEN MoveToConcl (-1)
   THEN (RepUR ``in-eclass eclass accum-class`` 0 THEN RepUR ``eclass-val`` 0)
   THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].  \mforall{}[base,f:Top].  \mforall{}[e:E].
    accum-class(a,x.f[a;x];x.base[x];X)(e)  \msim{}  accum\_list(a,e.f[a;X(e)];e.base[X(e)];\mleq{}(X)(e)) 
    supposing  \muparrow{}e  \mmember{}\msubb{}  accum-class(a,x.f[a;x];x.base[x];X)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (RepUR  ``in-eclass  eclass  accum-class``  0  THEN  RepUR  ``eclass-val``  0)
  THEN  AutoSplit)

---

Home Index