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
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),
so_apply: x[s],
LV_Ground: LV_Ground(loc),
LV_Scomp?: LV_Scomp?(v),
pi1: fst(t),
LV_Scomp-lval: LV_Scomp-lval(v),
pi2: snd(t),
LV_Scomp-comp: LV_Scomp-comp(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),
LV_Scomp: LV_Scomp(lval;comp),
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,
iff: P ⇐⇒ Q,
C_field_of: C_field_of(a;ctyp),
rev_implies: P ⇐ Q
Lemmas referenced :
C_LVALUE-induction,
assert_wf,
LV_Scomp?_wf,
C_LVALUE-proper_wf,
LV_Scomp-lval_wf,
C_Struct?_wf,
outl_wf,
C_TYPE_wf,
unit_wf2,
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,
it_wf,
bfalse_wf,
btrue_neq_bfalse,
LV_Scomp_wf,
true_wf,
C_TYPE_env_wf,
isl-apply-alist,
atom-deq_wf,
C_Struct-fields_wf,
assert-deq-member,
map_wf
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,
dependent_set_memberEquality,
independent_functionElimination,
voidElimination,
intEquality,
unionElimination,
instantiate,
cumulativity,
equalityTransitivity,
equalitySymmetry,
productElimination,
addLevel,
voidEquality,
inrEquality,
levelHypothesis,
independent_pairFormation,
atomEquality
Latex:
\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:
2016_05_16-AM-08_48_33
Last ObjectModification:
2015_12_28-PM-06_56_49
Theory : C-semantics
Home
Index