Nuprl Lemma : C_LVALUE-proper-Scomp
∀env:C_TYPE_env(). ∀lval:C_LVALUE().
((↑LV_Scomp?(lval))
⇒ (↑C_LVALUE-proper(env;lval))
⇒ let lval' = LV_Scomp-lval(lval) in
let a = LV_Scomp-comp(lval) in
let typ = outl(C_TYPE-of-LVALUE(env;lval')) in
(↑C_LVALUE-proper(env;lval')) ∧ (↑C_Struct?(typ)) ∧ (↑C_field_of(a;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(),
C_field_of: C_field_of(a;ctyp),
LV_Scomp-comp: LV_Scomp-comp(v),
LV_Scomp-lval: LV_Scomp-lval(v),
LV_Scomp?: LV_Scomp?(v),
C_LVALUE: C_LVALUE(),
C_Struct?: C_Struct?(v),
outl: outl(x),
assert: ↑b,
let: let,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q
Lemmas :
C_LVALUE-induction,
assert_wf,
LV_Scomp?_wf,
C_LVALUE-proper_wf,
LV_Scomp-lval_wf,
C_Struct?_wf,
outl_wf,
C_TYPE-of-LVALUE_wf,
C_field_of_wf,
LV_Scomp-comp_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_Scomp_wf,
true_wf,
C_TYPE_env_wf,
isl-apply-alist,
C_TYPE_wf,
atom-deq_wf,
C_Struct-fields_wf,
assert-deq-member,
map_wf
\mforall{}env:C\_TYPE\_env(). \mforall{}lval:C\_LVALUE().
((\muparrow{}LV\_Scomp?(lval))
{}\mRightarrow{} (\muparrow{}C\_LVALUE-proper(env;lval))
{}\mRightarrow{} let lval' = LV\_Scomp-lval(lval) in
let a = LV\_Scomp-comp(lval) in
let typ = outl(C\_TYPE-of-LVALUE(env;lval')) in
(\muparrow{}C\_LVALUE-proper(env;lval')) \mwedge{} (\muparrow{}C\_Struct?(typ)) \mwedge{} (\muparrow{}C\_field\_of(a;typ)))
Date html generated:
2015_07_17-AM-07_43_53
Last ObjectModification:
2015_01_27-AM-09_46_20
Home
Index