Nuprl Lemma : DVp_Int_wf

[int:ℤ]. (DVp_Int(int) ∈ C_DVALUEp())


Proof




Definitions occuring in Statement :  DVp_Int: DVp_Int(int) C_DVALUEp: C_DVALUEp() uall: [x:A]. B[x] member: t ∈ T int:
Lemmas :  C_DVALUEpco-ext eq_atom_wf bool_wf eqtt_to_assert assert_of_eq_atom unit_wf2 eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_atom C_LVALUE_wf int_seg_wf C_DVALUEpco_wf list_wf l_member_wf false_wf le_wf nat_wf has-value_wf_base set_subtype_base int_subtype_base has-value_wf-partial set-value-type int-value-type C_DVALUEpco_size_wf
\mforall{}[int:\mBbbZ{}].  (DVp\_Int(int)  \mmember{}  C\_DVALUEp())



Date html generated: 2015_07_17-AM-07_44_12
Last ObjectModification: 2015_01_27-AM-09_46_16

Home Index