---

Step * of Lemma event-has*-transitive-encrypt

∀s:SES. ∀es:EO+(Info). ∀a:Atom1. ∀e1,e2:E.  e1 has* a ⇒ e2 has* cipherText(e1) ⇒ e2 has* a supposing ↑e1 ∈b Encrypt
BY
{ Auto }

1
1. s : SES@i'
2. es : EO+(Info)@i'
3. a : Atom1@i
4. e1 : E@i
5. e2 : E@i
6. ↑e1 ∈b Encrypt
7. e1 has* a@i
8. e2 has* cipherText(e1)@i
⊢ e2 has* a

---

Latex:

---

Latex:
\mforall{}s:SES.  \mforall{}es:EO+(Info).  \mforall{}a:Atom1.  \mforall{}e1,e2:E.
    e1  has*  a  {}\mRightarrow{}  e2  has*  cipherText(e1)  {}\mRightarrow{}  e2  has*  a  supposing  \muparrow{}e1  \mmember{}\msubb{}  Encrypt


By

---

Latex:
Auto

---

Home Index