Nuprl Lemma : C_Array-elem_vs_DVALp
∀store:C_STOREp(). ∀ctyp:C_TYPE(). ∀env:C_TYPE_env(). ∀dval:C_DVALUEp(). ∀n:ℤ.
(C_STOREp-welltyped(env;store)
⇒ (↑C_Array?(ctyp))
⇒ (0 ≤ n)
⇒ n < C_Array-length(ctyp)
⇒ (↑(C_TYPE_vs_DVALp(env;ctyp) dval))
⇒ (↑(C_TYPE_vs_DVALp(env;C_Array-elems(ctyp)) (DVp_Array-arr(dval) (DVp_Array-lower(dval) + n)))))
Proof
Definitions occuring in Statement :
C_STOREp-welltyped: C_STOREp-welltyped(env;store),
C_STOREp: C_STOREp(),
C_TYPE_vs_DVALp: C_TYPE_vs_DVALp(env;ctyp),
DVp_Array-arr: DVp_Array-arr(v),
DVp_Array-lower: DVp_Array-lower(v),
C_DVALUEp: C_DVALUEp(),
C_TYPE_env: C_TYPE_env(),
C_Array-elems: C_Array-elems(v),
C_Array-length: C_Array-length(v),
C_Array?: C_Array?(v),
C_TYPE: C_TYPE(),
assert: ↑b,
less_than: a < b,
le: A ≤ B,
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a,
add: n + m,
natural_number: $n,
int: ℤ
Lemmas :
C_TYPE-ext,
eq_atom_wf,
bool_wf,
eqtt_to_assert,
assert_of_eq_atom,
subtype_base_sq,
atom_subtype_base,
unit_wf2,
unit_subtype_base,
it_wf,
eqff_to_assert,
equal_wf,
bool_cases_sqequal,
bool_subtype_base,
assert-bnot,
neg_assert_of_eq_atom,
assert_wf,
C_TYPE_vs_DVALp_wf,
less_than_wf,
C_Array-length_wf,
nat_wf,
le_wf,
C_Array?_wf,
C_STOREp-welltyped_wf,
C_DVALUEp_wf,
C_TYPE_env_wf,
C_TYPE_wf,
C_STOREp_wf,
C_DVALUEp-ext,
eq_int_wf,
subtract_wf,
assert_of_eq_int,
bl-all_wf,
int_seg_wf,
upto_wf,
l_member_wf,
lelt_wf,
equal-wf-T-base,
int_subtype_base,
l_all_wf2,
iff_transitivity,
iff_weakening_uiff,
assert_of_band,
assert-bl-all,
length_upto,
select-upto
\mforall{}store:C\_STOREp(). \mforall{}ctyp:C\_TYPE(). \mforall{}env:C\_TYPE\_env(). \mforall{}dval:C\_DVALUEp(). \mforall{}n:\mBbbZ{}.
(C\_STOREp-welltyped(env;store)
{}\mRightarrow{} (\muparrow{}C\_Array?(ctyp))
{}\mRightarrow{} (0 \mleq{} n)
{}\mRightarrow{} n < C\_Array-length(ctyp)
{}\mRightarrow{} (\muparrow{}(C\_TYPE\_vs\_DVALp(env;ctyp) dval))
{}\mRightarrow{} (\muparrow{}(C\_TYPE\_vs\_DVALp(env;C\_Array-elems(ctyp))
(DVp\_Array-arr(dval) (DVp\_Array-lower(dval) + n)))))
Date html generated:
2015_07_17-AM-07_45_20
Last ObjectModification:
2015_01_27-AM-09_46_13
Home
Index