Nuprl Lemma : C_LVALUE-proper-Ground
∀env:C_TYPE_env(). ∀lval:C_LVALUE().
((↑LV_Ground?(lval)) ⇒ (↑C_LVALUE-proper(env;lval)) ⇒ (↑isl(env LV_Ground-loc(lval))))
Proof
Definitions occuring in Statement :
C_LVALUE-proper: C_LVALUE-proper(env;lval),
C_TYPE_env: C_TYPE_env(),
LV_Ground-loc: LV_Ground-loc(v),
LV_Ground?: LV_Ground?(v),
C_LVALUE: C_LVALUE(),
assert: ↑b,
isl: isl(x),
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a
Lemmas :
C_LVALUE-induction,
assert_wf,
LV_Ground?_wf,
C_LVALUE-proper_wf,
isl_wf,
C_TYPE_wf,
unit_wf2,
LV_Ground-loc_wf,
C_LVALUE_wf,
LV_Ground_wf,
C_LOCATION_wf,
assert_elim,
LV_Index_wf,
bfalse_wf,
btrue_neq_bfalse,
LV_Scomp_wf,
C_TYPE_env_wf
\mforall{}env:C\_TYPE\_env(). \mforall{}lval:C\_LVALUE().
((\muparrow{}LV\_Ground?(lval)) {}\mRightarrow{} (\muparrow{}C\_LVALUE-proper(env;lval)) {}\mRightarrow{} (\muparrow{}isl(env LV\_Ground-loc(lval))))
Date html generated:
2015_07_17-AM-07_43_46
Last ObjectModification:
2015_01_27-AM-09_46_02
Home
Index