---

Step * 7 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
7. ¬(b = a ∈ Atom1)
8. ¬((¬(a ∈ sdata-atoms(d))) ∧ True ∧ (¬(b = a ∈ Atom1)))@i
9. ¬(a ∈ sdata-atoms(d))
⊢ a = b ∈ Atom1
BY
{ (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
7.  \mneg{}(b  =  a)
8.  \mneg{}((\mneg{}(a  \mmember{}  sdata-atoms(d)))  \mwedge{}  True  \mwedge{}  (\mneg{}(b  =  a)))@i
9.  \mneg{}(a  \mmember{}  sdata-atoms(d))
\mvdash{}  a  =  b


By

---

Latex:
(D  (-2)  THEN  Auto)

---

Home Index