---

{ [x1,x2,y1,y2:SecurityData].
    uiff(<x1, x2> = <y1, y2>;{(x1 = y1)  (x2 = y2)}) }

{ Proof }

---

Definitions occuring in Statement :  sdata-pair: <d1, d2>,  sdata: SecurityData,  uiff: uiff(P;Q),  uall: [x:A]. B[x],  guard: {T},  and: P  Q,  equal: s = t
Definitions :  uall: [x:A]. B[x],  uiff: uiff(P;Q),  guard: {T},  and: P  Q,  member: t  T,  uimplies: b supposing a,  prop: ,  sdata: SecurityData,  Id: Id,  sq_type: SQType(T),  all: x:A. B[x],  implies: P  Q
Lemmas :  sdata_wf,  sdata-pair_wf,  subtype_base_sq,  tree_subtype_base,  Id_wf,  union_subtype_base,  atom2_subtype_base,  atom1_subtype_base,  sdata-left_wf,  sdata-right_wf

---

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


Date html generated: 2011_08_17-PM-07_07_40
Last ObjectModification: 2011_06_18-PM-12_51_37

Home Index