---

Step * 1 of Lemma sdata-has-atom


1. d : SecurityData@i
2. a : Atom1@i
3. uiff(a#d:SecurityData;¬(a ∈ sdata-atoms(d)))
⊢ ¬a#d:SecurityData ⇐⇒ (a ∈ sdata-atoms(d))
BY
{ Auto }

1
1. d : SecurityData@i
2. a : Atom1@i
3. ¬(a ∈ sdata-atoms(d)) supposing a#d:SecurityData
4. a#d:SecurityData supposing ¬(a ∈ sdata-atoms(d))
5. ¬a#d:SecurityData@i
⊢ (a ∈ sdata-atoms(d))

---

Latex:

---

Latex:

1.  d  :  SecurityData@i
2.  a  :  Atom1@i
3.  uiff(a\#d:SecurityData;\mneg{}(a  \mmember{}  sdata-atoms(d)))
\mvdash{}  \mneg{}a\#d:SecurityData  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  sdata-atoms(d))


By

---

Latex:
Auto

---

Home Index