---

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

∀[b:Atom1]. ∀[d1,d2:SecurityData].  uiff(b#<d1, d2>:SecurityData;b#d1:SecurityData ∧ b#d2:SecurityData)
BY
{ (BasicUniformUnivCD Auto THEN UseWitness ⌈<<Ax, Ax>, Ax>⌉⋅) }

1
1. b : Atom1
2. d1 : SecurityData
3. d2 : SecurityData
⊢ <<Ax, Ax>, Ax> ∈ uiff(b#<d1, d2>:SecurityData;b#d1:SecurityData ∧ b#d2:SecurityData)

---

Latex:

---

Latex:
\mforall{}[b:Atom1].  \mforall{}[d1,d2:SecurityData].
    uiff(b\#<d1,  d2>:SecurityData;b\#d1:SecurityData  \mwedge{}  b\#d2:SecurityData)


By

---

Latex:
(BasicUniformUnivCD  Auto  THEN  UseWitness  \mkleeneopen{}<<Ax,  Ax>,  Ax>\mkleeneclose{}\mcdot{})

---

Home Index