---

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


1. a : Atom1@i
2. b : Atom1@i
3. d : SecurityData@i
4. k : Id@i
5. a#<k, b>:Id × Atom1 ∈ Type
6. a#k:Id ∈ Type
⊢ ¬((¬(a ∈ sdata-atoms(d))) ∧ True ∧ (¬(b = a ∈ Atom1))) ⇐⇒ (a = b ∈ Atom1) ∨ (a ∈ sdata-atoms(d))
BY
{ (( Decide ⌈b = a ∈ Atom1⌉⋅ THEN Auto)
   THEN  Decide ⌈(a ∈ sdata-atoms(d))⌉⋅
   THEN Auto
   THEN SplitOrHyps
   THEN Auto
   THEN D (-2)
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  a  :  Atom1@i
2.  b  :  Atom1@i
3.  d  :  SecurityData@i
4.  k  :  Id@i
5.  a\#<k,  b>:Id  \mtimes{}  Atom1  \mmember{}  Type
6.  a\#k:Id  \mmember{}  Type
\mvdash{}  \mneg{}((\mneg{}(a  \mmember{}  sdata-atoms(d)))  \mwedge{}  True  \mwedge{}  (\mneg{}(b  =  a)))  \mLeftarrow{}{}\mRightarrow{}  (a  =  b)  \mvee{}  (a  \mmember{}  sdata-atoms(d))


By

---

Latex:
((  Decide  \mkleeneopen{}b  =  a\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN    Decide  \mkleeneopen{}(a  \mmember{}  sdata-atoms(d))\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  SplitOrHyps
  THEN  Auto
  THEN  D  (-2)
  THEN  Auto)\mcdot{}

---

Home Index