---

Step * of Lemma sdata-pair-one-one

∀[x1,x2,y1,y2:SecurityData].
  uiff(<x1, x2> = <y1, y2> ∈ SecurityData;{(x1 = y1 ∈ SecurityData) ∧ (x2 = y2 ∈ SecurityData)})
BY
{ (Unfold `guard` 0 THEN Auto) }

1
1. x1 : SecurityData
2. x2 : SecurityData
3. y1 : SecurityData
4. y2 : SecurityData
5. <x1, x2> = <y1, y2> ∈ SecurityData
⊢ x1 = y1 ∈ SecurityData

2
1. x1 : SecurityData
2. x2 : SecurityData
3. y1 : SecurityData
4. y2 : SecurityData
5. <x1, x2> = <y1, y2> ∈ SecurityData
⊢ x2 = y2 ∈ SecurityData

---

Latex:

---

Latex:
\mforall{}[x1,x2,y1,y2:SecurityData].    uiff(<x1,  x2>  =  <y1,  y2>\{(x1  =  y1)  \mwedge{}  (x2  =  y2)\})


By

---

Latex:
(Unfold  `guard`  0  THEN  Auto)

---

Home Index