---

Step * of Lemma ses-info-flow_functionality

∀s:SES. (ActionsDisjoint ⇒ (∀es:EO+(Info). ∀x,y:E.  (same-action(x;y) ⇒ (∀e:E. ((e ->> x) ⇒ (e ->> y))))))
BY
{ (RepUR ``ses-info-flow`` 0 THEN Auto THEN FLemma `event-has_functionality` [(-5);(-2)]⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}s:SES
    (ActionsDisjoint
    {}\mRightarrow{}  (\mforall{}es:EO+(Info).  \mforall{}x,y:E.    (same-action(x;y)  {}\mRightarrow{}  (\mforall{}e:E.  ((e  ->>  x)  {}\mRightarrow{}  (e  ->>  y))))))


By

---

Latex:
(RepUR  ``ses-info-flow``  0  THEN  Auto  THEN  FLemma  `event-has\_functionality`  [(-5);(-2)]\mcdot{}  THEN  Auto)

---

Home Index