---

Step * 1 of Lemma ses-ordering-implies


1. s : SES@i'
2. ActionsDisjoint@i'
3. PropertyO@i'
4. PropertyN
⊢ {PropertyNU ∧ PropertyNR}
BY
{ ((FLemma `ses-nonce-release` [-1] THENA Auto) THEN (FLemma `ses-nonce-unique` [-2] THENM D 0) THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  SES@i'
2.  ActionsDisjoint@i'
3.  PropertyO@i'
4.  PropertyN
\mvdash{}  \{PropertyNU  \mwedge{}  PropertyNR\}


By

---

Latex:
((FLemma  `ses-nonce-release`  [-1]  THENA  Auto)
  THEN  (FLemma  `ses-nonce-unique`  [-2]  THENM  D  0)
  THEN  Auto)

---

Home Index