---

Step * 3 of Lemma sdata-pair-has-atom


1. d1 : SecurityData
2. d2 : SecurityData
3. b : Atom1
4. b#d1:SecurityData
5. b#d2:SecurityData
⊢ b#<d1, d2>:SecurityData
BY
{ (FreeFromAtomApElim ⌈d1⌉⋅ THEN FreeFromAtomApElim ⌈d2⌉⋅) }

---

Latex:

---

Latex:

1.  d1  :  SecurityData
2.  d2  :  SecurityData
3.  b  :  Atom1
4.  b\#d1:SecurityData
5.  b\#d2:SecurityData
\mvdash{}  b\#<d1,  d2>:SecurityData


By

---

Latex:
(FreeFromAtomApElim  \mkleeneopen{}d1\mkleeneclose{}\mcdot{}  THEN  FreeFromAtomApElim  \mkleeneopen{}d2\mkleeneclose{}\mcdot{})

---

Home Index