---

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


1. left : SecurityData@i
2. right : SecurityData@i
3. a : Atom1@i
4. a#right:SecurityData ⇐⇒ ¬(a ∈ sdata-atoms(right))
5. ¬a#right:SecurityData ⇐⇒ (a ∈ sdata-atoms(right))
6. a#left:SecurityData ⇐⇒ ¬(a ∈ sdata-atoms(left))
7. ¬a#left:SecurityData ⇐⇒ (a ∈ sdata-atoms(left))
⊢ ((¬(a ∈ sdata-atoms(left))) ∧ (¬(a ∈ sdata-atoms(right))) ⇐⇒ ¬((a ∈ sdata-atoms(left)) ∨ (a ∈ sdata-atoms(right))))
∧ (¬((¬(a ∈ sdata-atoms(left))) ∧ (¬(a ∈ sdata-atoms(right)))) ⇐⇒ (a ∈ sdata-atoms(left)) ∨ (a ∈ sdata-atoms(right)))
BY
{ ((  Decide ⌜(a ∈ sdata-atoms(left))⌝⋅ THENA Auto) THEN   Decide ⌜(a ∈ sdata-atoms(right))⌝⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  left  :  SecurityData@i
2.  right  :  SecurityData@i
3.  a  :  Atom1@i
4.  a\#right:SecurityData  \mLeftarrow{}{}\mRightarrow{}  \mneg{}(a  \mmember{}  sdata-atoms(right))
5.  \mneg{}a\#right:SecurityData  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  sdata-atoms(right))
6.  a\#left:SecurityData  \mLeftarrow{}{}\mRightarrow{}  \mneg{}(a  \mmember{}  sdata-atoms(left))
7.  \mneg{}a\#left:SecurityData  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  sdata-atoms(left))
\mvdash{}  ((\mneg{}(a  \mmember{}  sdata-atoms(left)))  \mwedge{}  (\mneg{}(a  \mmember{}  sdata-atoms(right)))
\mLeftarrow{}{}\mRightarrow{}  \mneg{}((a  \mmember{}  sdata-atoms(left))  \mvee{}  (a  \mmember{}  sdata-atoms(right))))
\mwedge{}  (\mneg{}((\mneg{}(a  \mmember{}  sdata-atoms(left)))  \mwedge{}  (\mneg{}(a  \mmember{}  sdata-atoms(right))))
    \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  sdata-atoms(left))  \mvee{}  (a  \mmember{}  sdata-atoms(right)))


By

---

Latex:
((    Decide  \mkleeneopen{}(a  \mmember{}  sdata-atoms(left))\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN      Decide  \mkleeneopen{}(a  \mmember{}  sdata-atoms(right))\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index