---

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


1. b : Atom1
2. d1 : SecurityData
3. d2 : SecurityData
⊢ <Ax, Ax> ∈ ∩:b#<d1, d2>:SecurityData. (b#d1:SecurityData ∧ b#d2:SecurityData)
BY
{ (Assert ⌈<Ax, Ax> ∈ ∩%:b#<d1, d2>:SecurityData. (b#d1:SecurityData ∧ b#d2:SecurityData)⌉⋅
   THEN Try (Trivial)
   THEN At ⌈Type⌉ (ISectMemTypeCD THEN Auto)⋅) }

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

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

---

Latex:

---

Latex:

1.  b  :  Atom1
2.  d1  :  SecurityData
3.  d2  :  SecurityData
\mvdash{}  <Ax,  Ax>  \mmember{}  \mcap{}:b\#<d1,  d2>:SecurityData.  (b\#d1:SecurityData  \mwedge{}  b\#d2:SecurityData)


By

---

Latex:
(Assert  \mkleeneopen{}<Ax,  Ax>  \mmember{}  \mcap{}\%:b\#<d1,  d2>:SecurityData.  (b\#d1:SecurityData  \mwedge{}  b\#d2:SecurityData)\mkleeneclose{}\mcdot{}
  THEN  Try  (Trivial)
  THEN  At  \mkleeneopen{}Type\mkleeneclose{}  (ISectMemTypeCD  THEN  Auto)\mcdot{})

---

Home Index