---

Step * of Lemma ses-axioms-imply

∀s:SES. (SecurityAxioms ⇒ {ses-ordering'(s) ∧ PropertyNR ∧ PropertyNU})
BY
{ (Auto THEN D -1 THEN Auto) }

1
1. s : SES@i'
2. ActionsDisjoint@i'
3. NoncesCiphersAndKeysDisjoint@i'
4. PropertyF@i'
5. PropertyV@i'
6. PropertyR@i'
7. PropertyD@i'
8. PropertyS@i'
9. PropertyK@i'
⊢ {ses-ordering'(s) ∧ PropertyNR ∧ PropertyNU}

---

Latex:

---

Latex:
\mforall{}s:SES.  (SecurityAxioms  {}\mRightarrow{}  \{ses-ordering'(s)  \mwedge{}  PropertyNR  \mwedge{}  PropertyNU\})


By

---

Latex:
(Auto  THEN  D  -1  THEN  Auto)

---

Home Index