---

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


1. a : Atom1@i
2. b : Atom1@i
3. d : SecurityData@i
4. k : Key@i
5. a#<k, b>:Key × Atom1 ∈ Type
6. a#b:Atom1 ∈ Type
7. a#d:SecurityData ∈ Type
8. (a ∈ sdata-atoms(d) @ encryption-key-atoms(k))@i
9. a#d:SecurityData@i
10. a#<k, b>:Key × Atom1@i
⊢ False
BY
{ ((RWO "member_append" (-3) THEN Auto)
   THEN D -3
   THEN RWW  "sdata-free-from-atom" (-2)
   THEN Auto
   THEN RWO "free-from-atom-pair-iff" (-1)
   THEN Auto
   THEN FLemma `encryption-key-free-from-atom` [-2]⋅
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  a  :  Atom1@i
2.  b  :  Atom1@i
3.  d  :  SecurityData@i
4.  k  :  Key@i
5.  a\#<k,  b>:Key  \mtimes{}  Atom1  \mmember{}  Type
6.  a\#b:Atom1  \mmember{}  Type
7.  a\#d:SecurityData  \mmember{}  Type
8.  (a  \mmember{}  sdata-atoms(d)  @  encryption-key-atoms(k))@i
9.  a\#d:SecurityData@i
10.  a\#<k,  b>:Key  \mtimes{}  Atom1@i
\mvdash{}  False


By

---

Latex:
((RWO  "member\_append"  (-3)  THEN  Auto)
  THEN  D  -3
  THEN  RWW    "sdata-free-from-atom"  (-2)
  THEN  Auto
  THEN  RWO  "free-from-atom-pair-iff"  (-1)
  THEN  Auto
  THEN  FLemma  `encryption-key-free-from-atom`  [-2]\mcdot{}
  THEN  Auto)\mcdot{}

---

Home Index