---

{ [a:Atom1]. [d1,d2:SecurityData].  uiff(<d1, d2> = data(a);False) }

{ Proof }

---

Definitions occuring in Statement :  sdata-pair: <d1, d2>,  atom-sdata: data(a),  sdata: SecurityData,  uiff: uiff(P;Q),  uall: [x:A]. B[x],  false: False,  equal: s = t,  atom: Atom$n
Definitions :  uall: [x:A]. B[x],  uiff: uiff(P;Q),  false: False,  member: t  T,  and: P  Q,  uimplies: b supposing a,  prop: ,  implies: P  Q,  iff: P  Q
Lemmas :  iff_weakening_uiff,  false_wf,  atom-sdata-not-pair,  sdata_wf,  sdata-pair_wf,  atom-sdata_wf

---

\mforall{}[a:Atom1].  \mforall{}[d1,d2:SecurityData].    uiff(<d1,  d2>  =  data(a);False)


Date html generated: 2011_08_17-PM-07_09_29
Last ObjectModification: 2011_06_18-PM-12_53_06

Home Index