---

Step * 5 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
⊢ ¬((¬(a ∈ sdata-atoms(d))) ∧ (¬(a ∈ encryption-key-atoms(k))) ∧ (¬(b = a ∈ Atom1)))
⇐⇒ (a ∈ sdata-atoms(d)) ∨ (a = b ∈ Atom1) ∨ (a ∈ encryption-key-atoms(k))
BY
{ ((Decide ⌈a = b ∈ Atom1⌉⋅ THENA Auto)
   THEN (Decide ⌈(a ∈ sdata-atoms(d))⌉⋅ THENA Auto)
   THEN Decide ⌈(a ∈ encryption-key-atoms(k))⌉⋅
   THEN Auto
   THEN ((SplitOrHyps THEN Auto) THEN D (-1) 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
\mvdash{}  \mneg{}((\mneg{}(a  \mmember{}  sdata-atoms(d)))  \mwedge{}  (\mneg{}(a  \mmember{}  encryption-key-atoms(k)))  \mwedge{}  (\mneg{}(b  =  a)))
\mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  sdata-atoms(d))  \mvee{}  (a  =  b)  \mvee{}  (a  \mmember{}  encryption-key-atoms(k))


By

---

Latex:
((Decide  \mkleeneopen{}a  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Decide  \mkleeneopen{}(a  \mmember{}  sdata-atoms(d))\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Decide  \mkleeneopen{}(a  \mmember{}  encryption-key-atoms(k))\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  ((SplitOrHyps  THEN  Auto)  THEN  D  (-1)  THEN  Auto)\mcdot{})

---

Home Index