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
Definitions unfolded in proof :
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
so_lambda: λ2x.t[x],
member: t ∈ T,
let: let,
implies: P ⇒ Q,
prop: ℙ,
and: P ∧ Q,
uimplies: b supposing a,
C_LVALUE-proper: C_LVALUE-proper(env;lval),
le: A ≤ B,
subtype_rel: A ⊆r B,
nat: ℕ,
so_apply: x[s],
LV_Ground: LV_Ground(loc),
LV_Index?: LV_Index?(v),
pi1: fst(t),
LV_Index-lval: LV_Index-lval(v),
pi2: snd(t),
LV_Index-idx: LV_Index-idx(v),
eq_atom: x =a y,
assert: ↑b,
ifthenelse: if b then t else f fi ,
bfalse: ff,
false: False,
LV_Index: LV_Index(lval;idx),
btrue: tt,
cand: A c∧ B,
C_TYPE-of-LVALUE: C_TYPE-of-LVALUE(env;lval),
C_LVALUE_ind: C_LVALUE_ind,
or: P ∨ Q,
sq_type: SQType(T),
guard: {T},
uiff: uiff(P;Q),
isl: isl(x),
not: ¬A,
LV_Scomp: LV_Scomp(lval;comp),
bool: 𝔹,
unit: Unit,
it: ⋅,
band: p ∧b q,
less_than: a < b,
outl: outl(x),
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q
Lemmas referenced :
C_LVALUE-induction,
assert_wf,
LV_Index?_wf,
C_LVALUE-proper_wf,
LV_Index-lval_wf,
C_Array?_wf,
outl_wf,
C_TYPE_wf,
unit_wf2,
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,
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,
not_wf,
and_wf,
equal_wf,
iff_transitivity,
iff_weakening_uiff,
assert_of_band,
assert_of_lt_int
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
sqequalRule,
lambdaEquality,
functionEquality,
hypothesisEquality,
hypothesis,
dependent_functionElimination,
because_Cache,
productEquality,
independent_isectElimination,
natural_numberEquality,
productElimination,
applyEquality,
setElimination,
rename,
independent_functionElimination,
voidElimination,
unionElimination,
instantiate,
cumulativity,
equalityTransitivity,
equalitySymmetry,
addLevel,
voidEquality,
inrEquality,
levelHypothesis,
independent_pairFormation,
intEquality,
atomEquality,
equalityElimination,
equalityEquality,
dependent_set_memberEquality,
unionEquality,
setEquality,
impliesFunctionality
Latex:
\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:
2016_05_16-AM-08_48_27
Last ObjectModification:
2015_12_28-PM-06_58_23
Theory : C-semantics
Home
Index