---

Step * 2 of Lemma sdata-free-from-atom


1. ∀d:SecurityData. ∀a:Atom1.
     ((a#d:SecurityData ⇐⇒ ¬(a ∈ sdata-atoms(d))) ∧ (¬a#d:SecurityData ⇐⇒ (a ∈ sdata-atoms(d))))
⊢ ∀[d:SecurityData]. ∀[a:Atom1].  uiff(a#d:SecurityData;¬(a ∈ sdata-atoms(d)))
BY
{ (RepeatFor 2 (ParallelLast') THEN D -1 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  \mforall{}d:SecurityData.  \mforall{}a:Atom1.
          ((a\#d:SecurityData  \mLeftarrow{}{}\mRightarrow{}  \mneg{}(a  \mmember{}  sdata-atoms(d)))  \mwedge{}  (\mneg{}a\#d:SecurityData  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  sdata-atoms(d))))
\mvdash{}  \mforall{}[d:SecurityData].  \mforall{}[a:Atom1].    uiff(a\#d:SecurityData;\mneg{}(a  \mmember{}  sdata-atoms(d)))


By

---

Latex:
(RepeatFor  2  (ParallelLast')  THEN  D  -1  THEN  Auto)\mcdot{}

---

Home Index