---

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


∀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)))))))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN Unfold `sdata-atoms` 0
   THEN Reduce 0
   THEN Fold `sdata-atoms` 0
   THEN Fold `sdata-pair` 0
   THEN RepeatFor 3 ((D 0 THENA Auto))
   THEN ∀h:hyp. ((InstHyp [⌜a⌝] h⋅ THENA Complete (Auto)) THEN Thin h) ) }

1
1. left : SecurityData@i
2. right : SecurityData@i
3. a : Atom1@i
4. (a#right:SecurityData ⇐⇒ ¬(a ∈ sdata-atoms(right))) ∧ (¬a#right:SecurityData ⇐⇒ (a ∈ sdata-atoms(right)))
5. (a#left:SecurityData ⇐⇒ ¬(a ∈ sdata-atoms(left))) ∧ (¬a#left:SecurityData ⇐⇒ (a ∈ sdata-atoms(left)))
⊢ (a#<left, right>:SecurityData ⇐⇒ ¬(a ∈ sdata-atoms(left) @ sdata-atoms(right)))
∧ (¬a#<left, right>:SecurityData ⇐⇒ (a ∈ sdata-atoms(left) @ sdata-atoms(right)))

---

Latex:

---

Latex:

\mforall{}left,right:SecurityData.
    ((\mforall{}a:Atom1
            ((a\#left:SecurityData  \mLeftarrow{}{}\mRightarrow{}  \mneg{}(a  \mmember{}  sdata-atoms(left)))
            \mwedge{}  (\mneg{}a\#left:SecurityData  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  sdata-atoms(left)))))
    {}\mRightarrow{}  (\mforall{}a:Atom1
                ((a\#right:SecurityData  \mLeftarrow{}{}\mRightarrow{}  \mneg{}(a  \mmember{}  sdata-atoms(right)))
                \mwedge{}  (\mneg{}a\#right:SecurityData  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  sdata-atoms(right)))))
    {}\mRightarrow{}  (\mforall{}a:Atom1
                ((a\#tree\_node(left;right):SecurityData  \mLeftarrow{}{}\mRightarrow{}  \mneg{}(a  \mmember{}  sdata-atoms(tree\_node(left;right))))
                \mwedge{}  (\mneg{}a\#tree\_node(left;right):SecurityData  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  sdata-atoms(tree\_node(left;right)))))))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  Unfold  `sdata-atoms`  0
  THEN  Reduce  0
  THEN  Fold  `sdata-atoms`  0
  THEN  Fold  `sdata-pair`  0
  THEN  RepeatFor  3  ((D  0  THENA  Auto))
  THEN  \mforall{}h:hyp.  ((InstHyp  [\mkleeneopen{}a\mkleeneclose{}]  h\mcdot{}  THENA  Complete  (Auto))  THEN  Thin  h)  )

---

Home Index