---

Step * 7 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 / sdata-atoms(d)])
BY
{ ((RWO "cons_member" 0 THENA Auto)
   THEN ( Decide ⌈b = a ∈ Atom1⌉⋅ THEN Auto)
   THEN  Decide ⌈(a ∈ sdata-atoms(d))⌉⋅
   THEN Auto
   THEN SplitOrHyps
   THEN Auto) }

1
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
7. ¬(b = a ∈ Atom1)
8. ¬((¬(a ∈ sdata-atoms(d))) ∧ True ∧ (¬(b = a ∈ Atom1)))@i
9. ¬(a ∈ sdata-atoms(d))
⊢ a = b ∈ Atom1

---

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  \mmember{}  [b  /  sdata-atoms(d)])


By

---

Latex:
((RWO  "cons\_member"  0  THENA  Auto)
  THEN  (  Decide  \mkleeneopen{}b  =  a\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN    Decide  \mkleeneopen{}(a  \mmember{}  sdata-atoms(d))\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  SplitOrHyps
  THEN  Auto)

---

Home Index