---

Step * 1 2 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))) ∧ (¬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)))
BY
{ (SplitAndHyps THEN (RWW "sdata-pair-has-atom member_append 3 4 5 6" 0 THENA Auto)) }

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

---

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)))
\mwedge{}  (\mneg{}a\#right:SecurityData  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  sdata-atoms(right)))
5.  (a\#left:SecurityData  \mLeftarrow{}{}\mRightarrow{}  \mneg{}(a  \mmember{}  sdata-atoms(left)))
\mwedge{}  (\mneg{}a\#left:SecurityData  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  sdata-atoms(left)))
\mvdash{}  (a\#<left,  right>:SecurityData  \mLeftarrow{}{}\mRightarrow{}  \mneg{}(a  \mmember{}  sdata-atoms(left)  @  sdata-atoms(right)))
\mwedge{}  (\mneg{}a\#<left,  right>:SecurityData  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  sdata-atoms(left)  @  sdata-atoms(right)))


By

---

Latex:
(SplitAndHyps  THEN  (RWW  "sdata-pair-has-atom  member\_append  3  4  5  6"  0  THENA  Auto))

---

Home Index