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