Step * 3 of Lemma member-used-atoms


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


Latex:



Latex:

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


By


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




Home Index