---

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


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)
BY
{ (InstLemma `ses-is-protocol-action-useable` [⌈s⌉;⌈pas[j]⌉;⌈es⌉;⌈thr[j]⌉]⋅ THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  s  :  SES@i'
2.  ActionsDisjoint@i'
3.  pas  :  ProtocolAction  List@i
4.  es  :  EO+(Info)@i'
5.  thr  :  \{thr:Act  List|  \mforall{}i:\mBbbN{}||thr||  -  1.  (thr[i]  <loc  thr[i  +  1])\}  @i
6.  A  :  Id@i
7.  ||thr||  =  ||pas||@i
8.  \mforall{}i:\mBbbN{}||pas||.  pas[i](thr[i])@i
9.  \mforall{}i:\mBbbN{}||pas||.  pa-used(pas[i])  \msubseteq{}  [Private(A)  /  concat(map(\mlambda{}j.pa-useable(pas[j]);[0,  i)))]@i
10.  i  :  \mBbbN{}||thr||@i
11.  pa-used(pas[i])  \msubseteq{}  [Private(A)  /  concat(map(\mlambda{}j.pa-useable(pas[j]);[0,  i)))]
12.  UsedAtoms(thr[i])  =  pa-used(pas[i])
13.  j  :  \mBbbZ{}@i
14.  (0  \mleq{}  j)  \mwedge{}  j  <  i@i
\mvdash{}  UseableAtoms(thr[j])  =  pa-useable(pas[j])


By

---

Latex:
(InstLemma  `ses-is-protocol-action-useable`  [\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}pas[j]\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}thr[j]\mkleeneclose{}]\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index