---

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

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

---

Latex:

---

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


By

---

Latex:
(ProveWfLemma  THEN  Unfold  `ses-basic-sequence1`  0  THEN  Auto)\mcdot{}

---

Home Index