---

Step * of Lemma state-class1-state1-classrel

∀[Info,B,A:Type]. ∀[f:Id ─→ A ─→ B ─→ B]. ∀[init:Id ─→ B]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:B].
  uiff(v ∈ State1(init;f;X)(e);v ∈ state-class1(init;f;X)(e))
BY
{ ((UnivCD THENA Auto) THEN RWO "State1-state-class1" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,B,A:Type].  \mforall{}[f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[init:Id  {}\mrightarrow{}  B].  \mforall{}[X:EClass(A)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
\mforall{}[v:B].
    uiff(v  \mmember{}  State1(init;f;X)(e);v  \mmember{}  state-class1(init;f;X)(e))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RWO  "State1-state-class1"  0  THEN  Auto)

---

Home Index