---

Step * 1 of Lemma member-used-atoms


1. s : SES@i'
2. es : EO+(Info)@i'
3. e : E@i
4. ¬↑e ∈b Sign
5. ¬↑e ∈b Send
6. a : Atom1@i
7. f : E ─→ ℤ
8. (↑e ∈b New) ⇒ ((f e) = 1 ∈ ℤ)
9. (↑e ∈b Rcv) ⇒ ((f e) = 3 ∈ ℤ)
10. (↑e ∈b Encrypt) ⇒ ((f e) = 6 ∈ ℤ)
11. (↑e ∈b Decrypt) ⇒ ((f e) = 7 ∈ ℤ)
12. ↑e ∈b Verify
13. (f e) = 5 ∈ ℤ
14. (a ∈ [signature(e) / sdata-atoms(signed(e))])@i
⊢ ((↑e ∈b Decrypt) ∧ ((a = cipherText(e) ∈ Atom1) ∨ (a ∈ encryption-key-atoms(key(e)))))
∨ (True ∧ ((a = signature(e) ∈ Atom1) ∨ (a ∈ sdata-atoms(signed(e)))))
∨ (False ∧ (a ∈ sdata-atoms(signed(e))))
∨ ((↑e ∈b Encrypt) ∧ ((a ∈ sdata-atoms(plainText(e))) ∨ (a ∈ encryption-key-atoms(key(e)))))
BY
{ (RWO "cons_member" (-1) THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  s  :  SES@i'
2.  es  :  EO+(Info)@i'
3.  e  :  E@i
4.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  Sign
5.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  Send
6.  a  :  Atom1@i
7.  f  :  E  {}\mrightarrow{}  \mBbbZ{}
8.  (\muparrow{}e  \mmember{}\msubb{}  New)  {}\mRightarrow{}  ((f  e)  =  1)
9.  (\muparrow{}e  \mmember{}\msubb{}  Rcv)  {}\mRightarrow{}  ((f  e)  =  3)
10.  (\muparrow{}e  \mmember{}\msubb{}  Encrypt)  {}\mRightarrow{}  ((f  e)  =  6)
11.  (\muparrow{}e  \mmember{}\msubb{}  Decrypt)  {}\mRightarrow{}  ((f  e)  =  7)
12.  \muparrow{}e  \mmember{}\msubb{}  Verify
13.  (f  e)  =  5
14.  (a  \mmember{}  [signature(e)  /  sdata-atoms(signed(e))])@i
\mvdash{}  ((\muparrow{}e  \mmember{}\msubb{}  Decrypt)  \mwedge{}  ((a  =  cipherText(e))  \mvee{}  (a  \mmember{}  encryption-key-atoms(key(e)))))
\mvee{}  (True  \mwedge{}  ((a  =  signature(e))  \mvee{}  (a  \mmember{}  sdata-atoms(signed(e)))))
\mvee{}  (False  \mwedge{}  (a  \mmember{}  sdata-atoms(signed(e))))
\mvee{}  ((\muparrow{}e  \mmember{}\msubb{}  Encrypt)  \mwedge{}  ((a  \mmember{}  sdata-atoms(plainText(e)))  \mvee{}  (a  \mmember{}  encryption-key-atoms(key(e)))))


By

---

Latex:
(RWO  "cons\_member"  (-1)  THEN  Auto)\mcdot{}

---

Home Index