---

Step * 5 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
⊢ ¬(a#d:SecurityData ∧ a#<k, b>:Key × Atom1) ⇐⇒ (a ∈ sdata-atoms(d)) ∨ (a ∈ [b / encryption-key-atoms(k)])
BY
{ ((RWO "cons_member sdata-free-from-atom free-from-atom-pair-iff" 0 THENA Auto)⋅
   THEN (RWW "free-from-atom-atom encryption-key-free-from-atom<" 0⋅ THENA Auto)⋅
   ) }

1
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
⊢ ¬((¬(a ∈ sdata-atoms(d))) ∧ (¬(a ∈ encryption-key-atoms(k))) ∧ (¬(b = a ∈ Atom1)))
⇐⇒ (a ∈ sdata-atoms(d)) ∨ (a = b ∈ Atom1) ∨ (a ∈ encryption-key-atoms(k))

---

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
\mvdash{}  \mneg{}(a\#d:SecurityData  \mwedge{}  a\#<k,  b>:Key  \mtimes{}  Atom1)
\mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  sdata-atoms(d))  \mvee{}  (a  \mmember{}  [b  /  encryption-key-atoms(k)])


By

---

Latex:
((RWO  "cons\_member  sdata-free-from-atom  free-from-atom-pair-iff"  0  THENA  Auto)\mcdot{}
  THEN  (RWW  "free-from-atom-atom  encryption-key-free-from-atom<"  0\mcdot{}  THENA  Auto)\mcdot{}
  )

---

Home Index