---

Step * of Lemma ses-is-legal_wf

∀[prvt:Atom1]. ∀[pas:ProtocolAction List].  (ses-is-legal(prvt; pas) ∈ 𝔹)
BY
{ ProveWfLemma }

1
1. prvt : Atom1
2. pas : ProtocolAction List
⊢ isl(TERMOF{decidable__ses-legal-sequence:o, 1:l} prvt pas) ∈ 𝔹

---

Latex:

---

Latex:
\mforall{}[prvt:Atom1].  \mforall{}[pas:ProtocolAction  List].    (ses-is-legal(prvt;  pas)  \mmember{}  \mBbbB{})


By

---

Latex:
ProveWfLemma

---

Home Index