---

Step * of Lemma loop-class-state-functional

∀[Info,B:Type]. ∀[init:Id ⟶ bag(B)]. ∀[X:EClass(B ⟶ B)]. ∀[es:EO+(Info)].
  (loop-class-state(X;init) is functional) supposing 
     ((∀l:Id. single-valued-bag(init l;B)) and 
     single-valued-classrel(es;X;B ⟶ B) and 
     (∀l:Id. (1 ≤ #(init l))))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `es-functional-class` 0
   THEN Auto
   THEN Try (ProveSingleVal)
   THEN ProveTotalClass
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,B:Type].  \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].  \mforall{}[X:EClass(B  {}\mrightarrow{}  B)].  \mforall{}[es:EO+(Info)].
    (loop-class-state(X;init)  is  functional)  supposing 
          ((\mforall{}l:Id.  single-valued-bag(init  l;B))  and 
          single-valued-classrel(es;X;B  {}\mrightarrow{}  B)  and 
          (\mforall{}l:Id.  (1  \mleq{}  \#(init  l))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `es-functional-class`  0
  THEN  Auto
  THEN  Try  (ProveSingleVal)
  THEN  ProveTotalClass
  THEN  Auto)

---

Home Index