---

Step * 1 of Lemma ses-is-legal_wf


1. prvt : Atom1
2. pas : ProtocolAction List
⊢ isl(TERMOF{decidable__ses-legal-sequence:o, 1:l} prvt pas) ∈ 𝔹
BY
{ ((GenConclAtAddr [2;1] THEN D -2) THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  prvt  :  Atom1
2.  pas  :  ProtocolAction  List
\mvdash{}  isl(TERMOF\{decidable\_\_ses-legal-sequence:o,  1:l\}  prvt  pas)  \mmember{}  \mBbbB{}


By

---

Latex:
((GenConclAtAddr  [2;1]  THEN  D  -2)  THEN  Reduce  0  THEN  Auto)

---

Home Index