---

{ [a:Atom1]. [d1,d2:SecurityData].  uiff(data(a) = <d1, d2>;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: ,  sdata: SecurityData,  atom-sdata: data(a),  sdata-pair: <d1, d2>,  tree_leaf: tree_leaf(x),  node: tree_node(<x, y>),  tree_node: tree_node(x),  tree: Tree(E),  tree_con: tree_con(E;T)
Lemmas :  sdata_wf,  atom-sdata_wf,  sdata-pair_wf,  false_wf,  tree_wf,  Id_wf

---

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


Date html generated: 2011_08_17-PM-07_09_10
Last ObjectModification: 2011_06_18-PM-12_52_27

Home Index