---

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


1. b : Atom1
2. d1 : SecurityData
3. d2 : SecurityData
4. b#d1:SecurityData
5. b#d2:SecurityData
⊢ Ax ∈ b#<d1, d2>:SecurityData
BY
{ Assert ⌈b#<d1, d2>:SecurityData⌉⋅ }

1
.....assertion..... 
1. b : Atom1
2. d1 : SecurityData
3. d2 : SecurityData
4. b#d1:SecurityData
5. b#d2:SecurityData
⊢ b#<d1, d2>:SecurityData

2
1. b : Atom1
2. d1 : SecurityData
3. d2 : SecurityData
4. b#d1:SecurityData
5. b#d2:SecurityData
6. b#<d1, d2>:SecurityData
⊢ Ax ∈ b#<d1, d2>:SecurityData

---

Latex:

---

Latex:

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


By

---

Latex:
Assert  \mkleeneopen{}b\#<d1,  d2>:SecurityData\mkleeneclose{}\mcdot{}

---

Home Index