Nuprl Lemma : pDVmsg?_wf

[x:PiDataVal()]. (pDVmsg?(x) ∈ 𝔹)


Proof




Definitions occuring in Statement :  pDVmsg?: pDVmsg?(x) PiDataVal: PiDataVal() bool: 𝔹 uall: [x:A]. B[x] member: t ∈ T
Lemmas :  PiDataVal_ind_wf bool_wf bfalse_wf Id_wf name_wf list_wf pi_prefix_wf btrue_wf nat_wf PiDataVal_wf

Latex:
\mforall{}[x:PiDataVal()].  (pDVmsg?(x)  \mmember{}  \mBbbB{})



Date html generated: 2015_07_23-AM-11_35_40
Last ObjectModification: 2015_01_29-AM-07_39_25

Home Index