Nuprl Lemma : C_TYPE-of-LVALUE_wf
∀env:C_TYPE_env(). ∀lval:C_LVALUE(). (C_TYPE-of-LVALUE(env;lval) ∈ C_TYPE()?)
Proof
Definitions occuring in Statement :
C_TYPE-of-LVALUE: C_TYPE-of-LVALUE(env;lval),
C_TYPE_env: C_TYPE_env(),
C_LVALUE: C_LVALUE(),
C_TYPE: C_TYPE(),
all: ∀x:A. B[x],
unit: Unit,
member: t ∈ T,
union: left + right
Lemmas :
C_LVALUE_ind_wf_simple,
C_TYPE_wf,
unit_wf2,
C_LOCATION_wf,
isl_wf,
bool_wf,
eqtt_to_assert,
C_Array?_wf,
le_int_wf,
assert_of_le_int,
lt_int_wf,
C_Array-length_wf,
nat_wf,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert_of_lt_int,
C_Array-elems_wf,
eqff_to_assert,
assert-bnot,
iff_transitivity,
assert_wf,
le_wf,
less_than_wf,
iff_weakening_uiff,
assert_of_band,
it_wf,
C_Struct?_wf,
apply-alist_wf,
atom-deq_wf,
C_Struct-fields_wf,
C_LVALUE_wf
\mforall{}env:C\_TYPE\_env(). \mforall{}lval:C\_LVALUE(). (C\_TYPE-of-LVALUE(env;lval) \mmember{} C\_TYPE()?)
Date html generated:
2015_07_17-AM-07_43_43
Last ObjectModification:
2015_01_27-AM-09_46_28
Home
Index