---

Step * 1 of Lemma ses-axioms-imply


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}
BY
{ (((FLemma `ses-flow-axiom-ordering` [4] THEN Auto) THEN FLemma `ses-ordering-implies` [-1] THEN Auto)
   THEN FLemma `ses-ordering-ordering\'` [-3]
   THEN Auto
   THEN D 0
   THEN Auto) }

---

Latex:

---

Latex:

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'
\mvdash{}  \{ses-ordering'(s)  \mwedge{}  PropertyNR  \mwedge{}  PropertyNU\}


By

---

Latex:
(((FLemma  `ses-flow-axiom-ordering`  [4]  THEN  Auto)
    THEN  FLemma  `ses-ordering-implies`  [-1]
    THEN  Auto)
  THEN  FLemma  `ses-ordering-ordering\mbackslash{}'`  [-3]
  THEN  Auto
  THEN  D  0
  THEN  Auto)

---

Home Index