---

Step * 4 1 1 1 1 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#d:SecurityData ∧ a#<k, b>:Key × Atom1)@i
⊢ (a = b ∈ Atom1) ∨ (a ∈ sdata-atoms(d) @ encryption-key-atoms(k))
BY
{ ( Decide ⌈a = b ∈ Atom1⌉⋅
   THEN Auto
   THEN SupposeNot
   THEN D -3
   THEN RWO  "sdata-free-from-atom" 0
   THEN Auto
   THEN RWO "free-from-atom-pair-iff" 0
   THEN Auto
   THEN BLemma  `encryption-key-free-from-atom` ⋅
   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.  \mneg{}(a\#d:SecurityData  \mwedge{}  a\#<k,  b>:Key  \mtimes{}  Atom1)@i
\mvdash{}  (a  =  b)  \mvee{}  (a  \mmember{}  sdata-atoms(d)  @  encryption-key-atoms(k))


By

---

Latex:
(  Decide  \mkleeneopen{}a  =  b\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  SupposeNot
  THEN  D  -3
  THEN  RWO    "sdata-free-from-atom"  0
  THEN  Auto
  THEN  RWO  "free-from-atom-pair-iff"  0
  THEN  Auto
  THEN  BLemma    `encryption-key-free-from-atom`  \mcdot{}
  THEN  Auto)

---

Home Index