---

Step * of Lemma basic-seq-1-1_wf

∀[s:SES]. ∀[pas:Id ⟶ Id ⟶ Atom1 ⟶ (ProtocolAction List)].  (A ⟶ B: pas[A;B;m] ∈ Basic1)
BY
{ (ProveWfLemma THEN Unfold `ses-basic-sequence1` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[s:SES].  \mforall{}[pas:Id  {}\mrightarrow{}  Id  {}\mrightarrow{}  Atom1  {}\mrightarrow{}  (ProtocolAction  List)].    (A  {}\mrightarrow{}  B:  pas[A;B;m]  \mmember{}  Basic1)


By

---

Latex:
(ProveWfLemma  THEN  Unfold  `ses-basic-sequence1`  0  THEN  Auto)

---

Home Index