Nuprl Lemma : C_TYPE_vs_DVALp_wf
∀env:C_TYPE_env(). ∀ctyp:C_TYPE().  (C_TYPE_vs_DVALp(env;ctyp) ∈ C_DVALUEp() ─→ 𝔹)
Proof
Definitions occuring in Statement : 
C_TYPE_vs_DVALp: C_TYPE_vs_DVALp(env;ctyp)
, 
C_DVALUEp: C_DVALUEp()
, 
C_TYPE_env: C_TYPE_env()
, 
C_TYPE: C_TYPE()
, 
bool: 𝔹
, 
all: ∀x:A. B[x]
, 
member: t ∈ T
, 
function: x:A ─→ B[x]
Lemmas : 
C_TYPE_ind_wf_simple, 
C_DVALUEp_wf, 
bool_wf, 
bfalse_wf, 
DVp_Int?_wf, 
l_all_wf2, 
C_TYPE_wf, 
l_member_wf, 
list_wf, 
nat_wf, 
DVp_Pointer?_wf, 
eqtt_to_assert, 
let_wf, 
C_LVALUE_wf, 
unit_wf2, 
isl_wf, 
C_TYPE-of-LVALUE_wf, 
C_TYPE_eq_wf, 
and_wf, 
equal_wf, 
assert_elim, 
btrue_neq_bfalse, 
eqff_to_assert, 
bool_cases_sqequal, 
subtype_base_sq, 
bool_subtype_base, 
assert-bnot, 
btrue_wf, 
DVp_Pointer-ptr_wf, 
C_DVALUEp-ext, 
eq_atom_wf, 
assert_of_eq_atom, 
atom_subtype_base, 
unit_subtype_base, 
it_wf, 
neg_assert_of_eq_atom, 
bdd-all_wf, 
length_wf_nat, 
value-type-has-value, 
atom-value-type, 
select_wf, 
sq_stable__le, 
deq-member_wf, 
atom-deq_wf, 
assert-deq-member, 
int_seg_wf, 
length_wf, 
pi1_wf_top, 
subtype_rel_product, 
top_wf, 
subtype_top, 
eq_int_wf, 
subtract_wf, 
assert_of_eq_int, 
bl-all_wf, 
upto_wf, 
lelt_wf
\mforall{}env:C\_TYPE\_env().  \mforall{}ctyp:C\_TYPE().    (C\_TYPE\_vs\_DVALp(env;ctyp)  \mmember{}  C\_DVALUEp()  {}\mrightarrow{}  \mBbbB{})
Date html generated:
2015_07_17-AM-07_45_09
Last ObjectModification:
2015_01_27-AM-09_46_36
Home
Index