---

Step * of Lemma ses-secrecy_wf

∀[s:SES]. ∀[agents:Id List]. ∀[secrets:Atom1 List]. ∀[es:EO+(Info)].  (Only agents in agents have atoms in secrets ∈ ℙ)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[s:SES].  \mforall{}[agents:Id  List].  \mforall{}[secrets:Atom1  List].  \mforall{}[es:EO+(Info)].
    (Only  agents  in  agents  have  atoms  in  secrets  \mmember{}  \mBbbP{})


By

---

Latex:
ProveWfLemma

---

Home Index