---

Step * of Lemma sdata-free-from-atom

∀[d:SecurityData]. ∀[a:Atom1].  uiff(a#d:SecurityData;¬(a ∈ sdata-atoms(d)))
BY
{ Assert ⌜∀d:SecurityData. ∀a:Atom1.
            ((a#d:SecurityData ⇐⇒ ¬(a ∈ sdata-atoms(d))) ∧ (¬a#d:SecurityData ⇐⇒ (a ∈ sdata-atoms(d))))⌝⋅ }

1
.....assertion..... 
∀d:SecurityData. ∀a:Atom1.
  ((a#d:SecurityData ⇐⇒ ¬(a ∈ sdata-atoms(d))) ∧ (¬a#d:SecurityData ⇐⇒ (a ∈ sdata-atoms(d))))

2
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)))

---

Latex:

---

Latex:
\mforall{}[d:SecurityData].  \mforall{}[a:Atom1].    uiff(a\#d:SecurityData;\mneg{}(a  \mmember{}  sdata-atoms(d)))


By

---

Latex:
Assert  \mkleeneopen{}\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))))\mkleeneclose{}\mcdot{}

---

Home Index