---

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

.....assertion..... 
1. b : Atom1
2. d1 : SecurityData
3. d2 : SecurityData
4. b#<d1, d2>:SecurityData
⊢ b#d2:SecurityData
BY
{ (FLemma `sdata-free-from-atom` [-1] THEN Auto THEN BLemma `sdata-free-from-atom` THEN Auto)⋅ }

---

Latex:

---

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


By

---

Latex:
(FLemma  `sdata-free-from-atom`  [-1]  THEN  Auto  THEN  BLemma  `sdata-free-from-atom`  THEN  Auto)\mcdot{}

---

Home Index