Nuprl Lemma : C_LVALUE-proper-Index
∀env:C_TYPE_env(). ∀lval:C_LVALUE().
((↑LV_Index?(lval))
⇒ (↑C_LVALUE-proper(env;lval))
⇒ let lval' = LV_Index-lval(lval) in
let i = LV_Index-idx(lval) in
let typ = outl(C_TYPE-of-LVALUE(env;lval')) in
(↑C_LVALUE-proper(env;lval')) ∧ (↑C_Array?(typ)) ∧ (0 ≤ i) ∧ i < C_Array-length(typ))
Proof
Definitions occuring in Statement :
C_LVALUE-proper: C_LVALUE-proper(env;lval),
C_TYPE-of-LVALUE: C_TYPE-of-LVALUE(env;lval),
C_TYPE_env: C_TYPE_env(),
LV_Index-idx: LV_Index-idx(v),
LV_Index-lval: LV_Index-lval(v),
LV_Index?: LV_Index?(v),
C_LVALUE: C_LVALUE(),
C_Array-length: C_Array-length(v),
C_Array?: C_Array?(v),
outl: outl(x),
assert: ↑b,
less_than: a < b,
let: let,
le: A ≤ B,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
natural_number: $n
Lemmas :
C_LVALUE-induction,
assert_wf,
LV_Index?_wf,
C_LVALUE-proper_wf,
LV_Index-lval_wf,
C_Array?_wf,
outl_wf,
C_TYPE-of-LVALUE_wf,
le_wf,
LV_Index-idx_wf,
less_than_wf,
C_Array-length_wf,
nat_wf,
C_LVALUE_wf,
false_wf,
C_LOCATION_wf,
bool_cases,
subtype_base_sq,
bool_wf,
bool_subtype_base,
eqtt_to_assert,
eqff_to_assert,
assert_of_bnot,
assert_elim,
isl_wf,
unit_wf2,
it_wf,
bfalse_wf,
btrue_neq_bfalse,
LV_Index_wf,
true_wf,
C_TYPE_env_wf,
le_int_wf,
assert_of_le_int,
lt_int_wf,
bnot_wf,
C_TYPE_wf,
void_wf,
and_wf,
equal_wf,
not_wf,
iff_transitivity,
iff_weakening_uiff,
assert_of_band,
assert_of_lt_int
\mforall{}env:C\_TYPE\_env(). \mforall{}lval:C\_LVALUE().
((\muparrow{}LV\_Index?(lval))
{}\mRightarrow{} (\muparrow{}C\_LVALUE-proper(env;lval))
{}\mRightarrow{} let lval' = LV\_Index-lval(lval) in
let i = LV\_Index-idx(lval) in
let typ = outl(C\_TYPE-of-LVALUE(env;lval')) in
(\muparrow{}C\_LVALUE-proper(env;lval')) \mwedge{} (\muparrow{}C\_Array?(typ)) \mwedge{} (0 \mleq{} i) \mwedge{} i < C\_Array-length(typ))
Date html generated:
2015_07_17-AM-07_43_51
Last ObjectModification:
2015_01_27-AM-09_47_31
Home
Index