---

Step * 1 of Lemma ses-act-has-atom


1. s : SES@i'
2. es : EO+(Info)@i'
3. e : Act@i
4. a : Atom1@i
5. f : E ─→ ℤ
6. (↑e ∈b Send) ⇒ (1 = 2 ∈ ℤ)
7. (↑e ∈b Rcv) ⇒ (1 = 3 ∈ ℤ)
8. (↑e ∈b Sign) ⇒ (1 = 4 ∈ ℤ)
9. (↑e ∈b Verify) ⇒ (1 = 5 ∈ ℤ)
10. (↑e ∈b Encrypt) ⇒ (1 = 6 ∈ ℤ)
11. (↑e ∈b Decrypt) ⇒ (1 = 7 ∈ ℤ)
12. ↑e ∈b New
13. (f e) = 1 ∈ ℤ
14. ¬↑e ∈b Rcv
15. ¬↑e ∈b Sign
16. ¬↑e ∈b Encrypt
17. ¬↑e ∈b Decrypt
18. ↑e ∈b New
19. ¬↑e ∈b Send
20. ¬↑e ∈b Verify
⊢ ¬a#New(e):Atom1 ⇐⇒ a = New(e) ∈ Atom1
BY
{ (RWO "free-from-atom-atom" 0 THEN Auto THEN Symmetry THEN SupposeNot THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  SES@i'
2.  es  :  EO+(Info)@i'
3.  e  :  Act@i
4.  a  :  Atom1@i
5.  f  :  E  {}\mrightarrow{}  \mBbbZ{}
6.  (\muparrow{}e  \mmember{}\msubb{}  Send)  {}\mRightarrow{}  (1  =  2)
7.  (\muparrow{}e  \mmember{}\msubb{}  Rcv)  {}\mRightarrow{}  (1  =  3)
8.  (\muparrow{}e  \mmember{}\msubb{}  Sign)  {}\mRightarrow{}  (1  =  4)
9.  (\muparrow{}e  \mmember{}\msubb{}  Verify)  {}\mRightarrow{}  (1  =  5)
10.  (\muparrow{}e  \mmember{}\msubb{}  Encrypt)  {}\mRightarrow{}  (1  =  6)
11.  (\muparrow{}e  \mmember{}\msubb{}  Decrypt)  {}\mRightarrow{}  (1  =  7)
12.  \muparrow{}e  \mmember{}\msubb{}  New
13.  (f  e)  =  1
14.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  Rcv
15.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  Sign
16.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  Encrypt
17.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  Decrypt
18.  \muparrow{}e  \mmember{}\msubb{}  New
19.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  Send
20.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  Verify
\mvdash{}  \mneg{}a\#New(e):Atom1  \mLeftarrow{}{}\mRightarrow{}  a  =  New(e)


By

---

Latex:
(RWO  "free-from-atom-atom"  0  THEN  Auto  THEN  Symmetry  THEN  SupposeNot  THEN  Auto)

---

Home Index