Nuprl Lemma : sdata-left_wf

[p:SecurityData]. sdata-left(p) ∈ SecurityData supposing ↑sdata-pair?(p)


Proof




Definitions occuring in Statement :  sdata-left: sdata-left(p) sdata-pair?: sdata-pair?(d) sdata: SecurityData assert: b uimplies: supposing a uall: [x:A]. B[x] member: t ∈ T
Lemmas :  tree_node-left_wf Id_wf assert_wf sdata-pair?_wf tree_wf

Latex:
\mforall{}[p:SecurityData].  sdata-left(p)  \mmember{}  SecurityData  supposing  \muparrow{}sdata-pair?(p)



Date html generated: 2015_07_23-PM-00_00_37
Last ObjectModification: 2015_01_29-AM-07_41_52

Home Index