Nuprl Lemma : C_TYPE-of-LVALUE_wf
∀env:C_TYPE_env(). ∀lval:C_LVALUE(). (C_TYPE-of-LVALUE(env;lval) ∈ C_TYPE()?)
Proof
Definitions occuring in Statement :
C_TYPE-of-LVALUE: C_TYPE-of-LVALUE(env;lval),
C_TYPE_env: C_TYPE_env(),
C_LVALUE: C_LVALUE(),
C_TYPE: C_TYPE(),
all: ∀x:A. B[x],
unit: Unit,
member: t ∈ T,
union: left + right
Definitions unfolded in proof :
C_TYPE_env: C_TYPE_env(),
all: ∀x:A. B[x],
member: t ∈ T,
C_TYPE-of-LVALUE: C_TYPE-of-LVALUE(env;lval),
uall: ∀[x:A]. B[x],
so_lambda: λ2x.t[x],
so_apply: x[s],
so_lambda: so_lambda(x,y,z.t[x; y; z]),
implies: P ⇒ Q,
exposed-bfalse: exposed-bfalse,
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
ifthenelse: if b then t else f fi ,
uiff: uiff(P;Q),
and: P ∧ Q,
uimplies: b supposing a,
outl: outl(x),
isl: isl(x),
assert: ↑b,
bfalse: ff,
false: False,
band: p ∧b q,
subtype_rel: A ⊆r B,
nat: ℕ,
exists: ∃x:A. B[x],
prop: ℙ,
or: P ∨ Q,
sq_type: SQType(T),
guard: {T},
bnot: ¬bb,
not: ¬A,
le: A ≤ B,
less_than: a < b,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
so_apply: x[s1;s2;s3]
Lemmas referenced :
C_LVALUE_ind_wf_simple,
C_TYPE_wf,
unit_wf2,
C_LOCATION_wf,
isl_wf,
bool_wf,
eqtt_to_assert,
C_Array?_wf,
le_int_wf,
assert_of_le_int,
lt_int_wf,
C_Array-length_wf,
nat_wf,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert_of_lt_int,
C_Array-elems_wf,
eqff_to_assert,
assert-bnot,
iff_transitivity,
assert_wf,
le_wf,
less_than_wf,
iff_weakening_uiff,
assert_of_band,
it_wf,
C_LVALUE_wf,
C_Struct?_wf,
apply-alist_wf,
atom-deq_wf,
C_Struct-fields_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
sqequalRule,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
unionEquality,
hypothesis,
hypothesisEquality,
lambdaEquality,
applyEquality,
because_Cache,
unionElimination,
equalityElimination,
productElimination,
independent_isectElimination,
voidElimination,
natural_numberEquality,
setElimination,
rename,
equalityTransitivity,
equalitySymmetry,
equalityEquality,
dependent_functionElimination,
independent_functionElimination,
dependent_pairFormation,
promote_hyp,
instantiate,
cumulativity,
inlEquality,
productEquality,
independent_pairFormation,
inrEquality,
intEquality,
atomEquality,
functionEquality
Latex:
\mforall{}env:C\_TYPE\_env(). \mforall{}lval:C\_LVALUE(). (C\_TYPE-of-LVALUE(env;lval) \mmember{} C\_TYPE()?)
Date html generated:
2016_05_16-AM-08_48_11
Last ObjectModification:
2015_12_28-PM-06_56_54
Theory : C-semantics
Home
Index