---

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

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

---

Latex:

---

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


By

---

Latex:
(FLemma  `sdata-free-from-atom`  [-2]
  THEN  Auto
  THEN  FLemma  `sdata-free-from-atom`  [-2]
  THEN  Auto
  THEN  BLemma  `sdata-free-from-atom`
  THEN  Auto
  THEN  Reduce  0
  THEN  (RWO  "member\_append"  0  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  Auto)\mcdot{}

---

Home Index