---

Step * of Lemma ses-is-protocol-action_wf

∀[s:SES]. ∀[pa:ProtocolAction]. ∀[es:EO+(Info)]. ∀[e:E].  (pa(e) ∈ ℙ)
BY
{ (Auto
   THEN Unfold `ses-is-protocol-action` 0
   THEN D -3
   THEN Reduce 0
   THEN MoveToConcl (-3)
   THEN RepeatFor 6 (AutoSplit)
   THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[s:SES].  \mforall{}[pa:ProtocolAction].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].    (pa(e)  \mmember{}  \mBbbP{})


By

---

Latex:
(Auto
  THEN  Unfold  `ses-is-protocol-action`  0
  THEN  D  -3
  THEN  Reduce  0
  THEN  MoveToConcl  (-3)
  THEN  RepeatFor  6  (AutoSplit)
  THEN  AutoSplit)

---

Home Index