---

Step * of Lemma sdata-has-atom

∀d:SecurityData. ∀a:Atom1.  (¬a#d:SecurityData ⇐⇒ (a ∈ sdata-atoms(d)))
BY
{ (InstLemma `sdata-free-from-atom` [] THEN RepeatFor 2 (ParallelLast')) }

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

---

Latex:

---

Latex:
\mforall{}d:SecurityData.  \mforall{}a:Atom1.    (\mneg{}a\#d:SecurityData  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  sdata-atoms(d)))


By

---

Latex:
(InstLemma  `sdata-free-from-atom`  []  THEN  RepeatFor  2  (ParallelLast'))

---

Home Index