---

Step * of Lemma decidable__pa-is-new-and

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

---

Latex:

---

Latex:
\mforall{}a:ProtocolAction.  \mforall{}P:Atom1  {}\mrightarrow{}  \mBbbP{}.    ((\mforall{}v:Atom1.  Dec(P[v]))  {}\mRightarrow{}  Dec(pa-is-new-and(a;v.P[v])))


By

---

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

---

Home Index