---

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


1. b : Atom1
2. d1 : SecurityData
3. d2 : SecurityData
⊢ <<Ax, Ax>, Ax> ∈ uiff(b#<d1, d2>:SecurityData;b#d1:SecurityData ∧ b#d2:SecurityData)
BY
{ (MemCD THEN Try (Complete (Auto))) }

1
.....subterm..... T:t
1:n
1. b : Atom1
2. d1 : SecurityData
3. d2 : SecurityData
⊢ <Ax, Ax> ∈ b#d1:SecurityData ∧ b#d2:SecurityData supposing b#<d1, d2>:SecurityData

2
.....subterm..... T:t
2:n
1. b : Atom1
2. d1 : SecurityData
3. d2 : SecurityData
⊢ Ax ∈ b#<d1, d2>:SecurityData supposing b#d1:SecurityData ∧ b#d2:SecurityData

---

Latex:

---

Latex:

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


By

---

Latex:
(MemCD  THEN  Try  (Complete  (Auto)))

---

Home Index