Nuprl Lemma : pDVfire?_wf

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


Proof




Definitions occuring in Statement :  pDVfire?: pDVfire?(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 nat_wf btrue_wf PiDataVal_wf

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



Date html generated: 2015_07_23-AM-11_35_50
Last ObjectModification: 2015_01_29-AM-07_39_16

Home Index