---

Step * of Lemma decidable__pa-is-sign-implies

∀a:ProtocolAction. ∀P:(SecurityData × Id × Atom1) ⟶ ℙ.
  ((∀v:SecurityData × Id × Atom1. Dec(P[v])) ⇒ Dec(pa-is-sign-implies(a;v.P[v])))
BY
{ (Auto
   THEN Unfold `pa-is-sign-implies` 0
   THEN D 1
   THEN Reduce 0
   THEN ( Decide ⌜n = "sign" ∈ Atom⌝⋅ THENA Auto)
   THEN Try ((HypSubst' (-1) 2 THEN Reduce 2 THEN Auto))
   THEN OrLeft
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}a:ProtocolAction.  \mforall{}P:(SecurityData  \mtimes{}  Id  \mtimes{}  Atom1)  {}\mrightarrow{}  \mBbbP{}.
    ((\mforall{}v:SecurityData  \mtimes{}  Id  \mtimes{}  Atom1.  Dec(P[v]))  {}\mRightarrow{}  Dec(pa-is-sign-implies(a;v.P[v])))


By

---

Latex:
(Auto
  THEN  Unfold  `pa-is-sign-implies`  0
  THEN  D  1
  THEN  Reduce  0
  THEN  (  Decide  \mkleeneopen{}n  =  "sign"\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  ((HypSubst'  (-1)  2  THEN  Reduce  2  THEN  Auto))
  THEN  OrLeft
  THEN  Auto)

---

Home Index