---

Step * of Lemma ses-is-protocol-actions-legal

∀s:SES
  (ActionsDisjoint
  ⇒ (∀pas:ProtocolAction List. ∀es:EO+(Info). ∀thr:Thread. ∀A:Id.
        (pas(thr) ⇒ Legal(pas) given Private(A) ⇒ Legal(thr)@A)))
BY
{ (Auto
   THEN All (Unfolds ``ses-is-protocol-actions ses-thread``)
   THEN All (Unfolds ``ses-legal-sequence ses-legal-thread``)
   THEN Auto
   THEN (InstHyp [⌜i⌝] (-2)⋅ THENA Auto)
   THEN NthHypEq (-1)
   THEN EqCD
   THEN Auto
   THEN Try ((InstLemma `ses-is-protocol-action-used` [⌜s⌝;⌜pas[i]⌝;⌜es⌝;⌜thr[i]⌝]⋅ THEN Auto)⋅)
   THEN RepeatFor 4 ((EqCD THEN Auto))⋅
   THEN D -1) }

1
1. s : SES@i'
2. ActionsDisjoint@i'
3. pas : ProtocolAction List@i
4. es : EO+(Info)@i'
5. thr : {thr:Act List| ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])} @i
6. A : Id@i
7. ||thr|| = ||pas|| ∈ ℤ@i
8. ∀i:ℕ||pas||. pas[i](thr[i])@i
9. ∀i:ℕ||pas||. pa-used(pas[i]) ⊆ [Private(A) / concat(map(λj.pa-useable(pas[j]);[0, i)))]@i
10. i : ℕ||thr||@i
11. pa-used(pas[i]) ⊆ [Private(A) / concat(map(λj.pa-useable(pas[j]);[0, i)))]
12. UsedAtoms(thr[i]) = pa-used(pas[i]) ∈ (Atom1 List)
13. j : ℤ@i
14. (0 ≤ j) ∧ j < i@i
⊢ UseableAtoms(thr[j]) = pa-useable(pas[j]) ∈ (Atom1 List)

---

Latex:

---

Latex:
\mforall{}s:SES
    (ActionsDisjoint
    {}\mRightarrow{}  (\mforall{}pas:ProtocolAction  List.  \mforall{}es:EO+(Info).  \mforall{}thr:Thread.  \mforall{}A:Id.
                (pas(thr)  {}\mRightarrow{}  Legal(pas)  given  Private(A)  {}\mRightarrow{}  Legal(thr)@A)))


By

---

Latex:
(Auto
  THEN  All  (Unfolds  ``ses-is-protocol-actions  ses-thread``)
  THEN  All  (Unfolds  ``ses-legal-sequence  ses-legal-thread``)
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  NthHypEq  (-1)
  THEN  EqCD
  THEN  Auto
  THEN  Try  ((InstLemma  `ses-is-protocol-action-used`  [\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}pas[i]\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}thr[i]\mkleeneclose{}]\mcdot{}  THEN  Auto)\mcdot{})
  THEN  RepeatFor  4  ((EqCD  THEN  Auto))\mcdot{}
  THEN  D  -1)

---

Home Index