---

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

.....assertion..... 
∀d:SecurityData. ∀a:Atom1.
  ((a#d:SecurityData ⇐⇒ ¬(a ∈ sdata-atoms(d))) ∧ (¬a#d:SecurityData ⇐⇒ (a ∈ sdata-atoms(d))))
BY
{ (Unfold `sdata` 0 THEN (BLemma `tree-induction` THENA Auto) THEN Fold `sdata` 0) }

1
∀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)))))

2
∀left,right:SecurityData.
  ((∀a:Atom1. ((a#left:SecurityData ⇐⇒ ¬(a ∈ sdata-atoms(left))) ∧ (¬a#left:SecurityData ⇐⇒ (a ∈ sdata-atoms(left)))))
  ⇒ (∀a:Atom1
        ((a#right:SecurityData ⇐⇒ ¬(a ∈ sdata-atoms(right))) ∧ (¬a#right:SecurityData ⇐⇒ (a ∈ sdata-atoms(right)))))
  ⇒ (∀a:Atom1
        ((a#tree_node(left;right):SecurityData ⇐⇒ ¬(a ∈ sdata-atoms(tree_node(left;right))))
        ∧ (¬a#tree_node(left;right):SecurityData ⇐⇒ (a ∈ sdata-atoms(tree_node(left;right)))))))

---

Latex:

---

Latex:
.....assertion..... 
\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))))


By

---

Latex:
(Unfold  `sdata`  0  THEN  (BLemma  `tree-induction`  THENA  Auto)  THEN  Fold  `sdata`  0)

---

Home Index