---

Step * of Lemma ses-ordering-implies

∀s:SES. (ActionsDisjoint ⇒ PropertyO ⇒ {PropertyNU ∧ PropertyNR})
BY
{ (Auto THEN (FLemma `ses-nonce-from-ordering` [2;3] THENA Auto)) }

1
1. s : SES@i'
2. ActionsDisjoint@i'
3. PropertyO@i'
4. PropertyN
⊢ {PropertyNU ∧ PropertyNR}

---

Latex:

---

Latex:
\mforall{}s:SES.  (ActionsDisjoint  {}\mRightarrow{}  PropertyO  {}\mRightarrow{}  \{PropertyNU  \mwedge{}  PropertyNR\})


By

---

Latex:
(Auto  THEN  (FLemma  `ses-nonce-from-ordering`  [2;3]  THENA  Auto))

---

Home Index