---

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


∀value:Id + Atom1. ∀a:Atom1.
  ((a#tree_leaf(value):SecurityData ⇐⇒ ¬(a ∈ sdata-atoms(tree_leaf(value))))
  ∧ (¬a#tree_leaf(value):SecurityData ⇐⇒ (a ∈ sdata-atoms(tree_leaf(value)))))
BY
{ ((D 0 THENA Auto)
   THEN D -1
   THEN RepUR ``sdata-atoms`` 0
   THEN Try (Folds ``atom-sdata id-sdata`` 0)
   THEN (D 0 THENA Auto)
   THEN RWO "id-sdata-has-atom atom-sdata-has-atom member_singleton" 0
   THEN Auto
   THEN Symmetry
   THEN SupposeNot
   THEN Auto) }

---

Latex:

---

Latex:

\mforall{}value:Id  +  Atom1.  \mforall{}a:Atom1.
    ((a\#tree\_leaf(value):SecurityData  \mLeftarrow{}{}\mRightarrow{}  \mneg{}(a  \mmember{}  sdata-atoms(tree\_leaf(value))))
    \mwedge{}  (\mneg{}a\#tree\_leaf(value):SecurityData  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  sdata-atoms(tree\_leaf(value)))))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  D  -1
  THEN  RepUR  ``sdata-atoms``  0
  THEN  Try  (Folds  ``atom-sdata  id-sdata``  0)
  THEN  (D  0  THENA  Auto)
  THEN  RWO  "id-sdata-has-atom  atom-sdata-has-atom  member\_singleton"  0
  THEN  Auto
  THEN  Symmetry
  THEN  SupposeNot
  THEN  Auto)

---

Home Index