Nuprl Lemma : id-sdata-not-pair2

[a:Id]. ∀[d1,d2:SecurityData].  uiff(<d1, d2> data(a) ∈ SecurityData;False)


Proof




Definitions occuring in Statement :  sdata-pair: <d1, d2> id-sdata: data(x) sdata: SecurityData Id: Id uiff: uiff(P;Q) uall: [x:A]. B[x] false: False equal: t ∈ T
Lemmas :  id-sdata-not-pair equal_wf sdata_wf sdata-pair_wf id-sdata_wf false_wf Id_wf

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



Date html generated: 2015_07_23-PM-00_00_59
Last ObjectModification: 2015_01_29-AM-07_43_34

Home Index