---

Step * of Lemma once-classrel-weak

∀[Info,A:Type]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E].  ∀v:A. (v ∈ (X once)(e) ⇐⇒ (no X prior to e) ∧ v ∈ {X}(e))
BY
{ (Unfold `guard` 0 THEN InstLemma `once-classrel` [] THEN Repeat (ParallelLast')) }

---

Latex:

---

Latex:
\mforall{}[Info,A:Type].  \mforall{}[X:EClass(A)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
    \mforall{}v:A.  (v  \mmember{}  (X  once)(e)  \mLeftarrow{}{}\mRightarrow{}  (no  X  prior  to  e)  \mwedge{}  v  \mmember{}  \{X\}(e))


By

---

Latex:
(Unfold  `guard`  0  THEN  InstLemma  `once-classrel`  []  THEN  Repeat  (ParallelLast'))

---

Home Index