---

Step * of Lemma authentication_wf

∀[s:SES]. ∀[prtcl:Id ⟶ ℙ']. ∀[bs:Basic1]. ∀[n:ℕ].  (prtcl |= bs authenticates n messages  ∈ ℙ')
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[s:SES].  \mforall{}[prtcl:Id  {}\mrightarrow{}  \mBbbP{}'].  \mforall{}[bs:Basic1].  \mforall{}[n:\mBbbN{}].    (prtcl  |=  bs  authenticates  n  messages    \mmember{}  \mBbbP{}')


By

---

Latex:
ProveWfLemma

---

Home Index