---

Step * of Lemma ses-encrypt_wf

∀[s:SES]. (Encrypt ∈ EClass(SecurityData × Key × Atom1))
BY
{ (Unfolds ``security-event-structure ses-info`` 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[s:SES].  (Encrypt  \mmember{}  EClass(SecurityData  \mtimes{}  Key  \mtimes{}  Atom1))


By

---

Latex:
(Unfolds  ``security-event-structure  ses-info``  0  THEN  ProveWfLemma)

---

Home Index