---

Step * of Lemma Accum-class-single-val

∀[Info,A,B:Type]. ∀[es:EO+(Info)].
  ∀X:EClass(A)
    ∀[init:Id ─→ bag(B)]. ∀[f:A ─→ B ─→ B].
      (single-valued-classrel(es;X;A)
      ⇒ (∀l:Id. single-valued-bag(init l;B))
      ⇒ single-valued-classrel(es;Accum-class(f;init;X);B))
BY
{ ((UnivCD THENA MaAuto) THEN Unfold `Accum-class` 0 THEN SingleValThm) }

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[es:EO+(Info)].
    \mforall{}X:EClass(A)
        \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].  \mforall{}[f:A  {}\mrightarrow{}  B  {}\mrightarrow{}  B].
            (single-valued-classrel(es;X;A)
            {}\mRightarrow{}  (\mforall{}l:Id.  single-valued-bag(init  l;B))
            {}\mRightarrow{}  single-valued-classrel(es;Accum-class(f;init;X);B))


By

---

Latex:
((UnivCD  THENA  MaAuto)  THEN  Unfold  `Accum-class`  0  THEN  SingleValThm)

---

Home Index