---

Step * 2 of Lemma member-used-atoms


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

---

Latex:

---

Latex:

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


By

---

Latex:
(RWO  "member\_append"  (-1)  THEN  Auto)\mcdot{}

---

Home Index