---

Step * of Lemma decidable__ses-legal-sequence

∀prvt:Atom1. ∀pas:ProtocolAction List.  Dec(Legal(pas) given prvt)
BY
{ (Unfold `ses-legal-sequence` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}prvt:Atom1.  \mforall{}pas:ProtocolAction  List.    Dec(Legal(pas)  given  prvt)


By

---

Latex:
(Unfold  `ses-legal-sequence`  0  THEN  Auto)

---

Home Index