---

Step * of Lemma State-class-single-val

∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[f:A ─→ B ─→ B]. ∀[X:EClass(A)]. ∀[init:Id ─→ bag(B)].
  (single-valued-classrel(es;State-class(init;f;X);B)) supposing 
     ((∀l:Id. single-valued-bag(init l;B)) and 
     single-valued-classrel(es;X;A))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `single-valued-classrel` 0
   THEN Auto
   THEN FLemma `State-class-single-val0` [-2;-1]
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `single-valued-classrel`  0
  THEN  Auto
  THEN  FLemma  `State-class-single-val0`  [-2;-1]
  THEN  Auto)

---

Home Index