---

Step * of Lemma ses-sign-is-protocol-action

∀[s:SES]
  ∀[pa:ProtocolAction]. ∀[es:EO+(Info)]. ∀[e:E].
    ({((fst(pa)) = "sign" ∈ Atom) ∧ ((snd(pa)) = Sign(e) ∈ (SecurityData × Id × Atom1))}) supposing 
       ((↑e ∈b Sign) and 
       pa(e)) 
  supposing ActionsDisjoint
BY
{ ((UnivCD THENA Auto)
   THEN MoveToConcl (-2)
   THEN DVar `pa'
   THEN RepUR ``ses-is-protocol-action`` 0
   THEN MoveToConcl (-4)
   THEN (With ⌜es⌝ (D 2)⋅ THENA Auto)
   THEN (D -1 THEN (InstHyp [⌜e⌝] (-1)⋅ THENA Auto) THEN SplitAndHyps)
   THEN Repeat ((WeakAutoSplit THENL [Auto; Id]))
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[s:SES]
    \mforall{}[pa:ProtocolAction].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
        (\{((fst(pa))  =  "sign")  \mwedge{}  ((snd(pa))  =  Sign(e))\})  supposing  ((\muparrow{}e  \mmember{}\msubb{}  Sign)  and  pa(e)) 
    supposing  ActionsDisjoint


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  MoveToConcl  (-2)
  THEN  DVar  `pa'
  THEN  RepUR  ``ses-is-protocol-action``  0
  THEN  MoveToConcl  (-4)
  THEN  (With  \mkleeneopen{}es\mkleeneclose{}  (D  2)\mcdot{}  THENA  Auto)
  THEN  (D  -1  THEN  (InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)  THEN  SplitAndHyps)
  THEN  Repeat  ((WeakAutoSplit  THENL  [Auto;  Id]))
  THEN  Auto)

---

Home Index