---

Step * 2 1 1 1 1 of Lemma ses-is-protocol-actions-fresh


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. f : SecurityData ─→ (Atom1?)@i
10. i : ℕ||thr||@i
11. ↑thr[i] ∈b Sign@i
12. (fst(snd(snd(pas[i])))) = A ∈ Id
13. pas[i](thr[i])
14. ((fst(pas[i])) = "sign" ∈ Atom) ∧ ((snd(pas[i])) = Sign(thr[i]) ∈ (SecurityData × Id × Atom1))
⊢ signer(thr[i]) = A ∈ Id
BY
{ (D (-1) THEN HypSubst' (-1) (-4)) }

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. f : SecurityData ─→ (Atom1?)@i
10. i : ℕ||thr||@i
11. ↑thr[i] ∈b Sign@i
12. (fst(snd(Sign(thr[i])))) = A ∈ Id
13. pas[i](thr[i])
14. (fst(pas[i])) = "sign" ∈ Atom
15. (snd(pas[i])) = Sign(thr[i]) ∈ (SecurityData × Id × Atom1)
⊢ signer(thr[i]) = A ∈ Id

---

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.  f  :  SecurityData  {}\mrightarrow{}  (Atom1?)@i
10.  i  :  \mBbbN{}||thr||@i
11.  \muparrow{}thr[i]  \mmember{}\msubb{}  Sign@i
12.  (fst(snd(snd(pas[i]))))  =  A
13.  pas[i](thr[i])
14.  ((fst(pas[i]))  =  "sign")  \mwedge{}  ((snd(pas[i]))  =  Sign(thr[i]))
\mvdash{}  signer(thr[i])  =  A


By

---

Latex:
(D  (-1)  THEN  HypSubst'  (-1)  (-4))

---

Home Index