Nuprl Lemma : C_STOREp-welltyped_wf
∀env:C_TYPE_env(). ∀store:C_STOREp(). (C_STOREp-welltyped(env;store) ∈ ℙ)
Proof
Definitions occuring in Statement :
C_STOREp-welltyped: C_STOREp-welltyped(env;store),
C_STOREp: C_STOREp(),
C_TYPE_env: C_TYPE_env(),
prop: ℙ,
all: ∀x:A. B[x],
member: t ∈ T
Lemmas :
all_wf,
C_LOCATION_wf,
isl_wf,
C_TYPE_wf,
unit_wf2,
bool_wf,
eqtt_to_assert,
assert_wf,
C_DVALUEp_wf,
C_TYPE_vs_DVALp_wf,
assert_elim,
bfalse_wf,
and_wf,
equal_wf,
btrue_neq_bfalse,
eqff_to_assert,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
isr_wf,
C_STOREp_wf,
C_TYPE_env_wf
\mforall{}env:C\_TYPE\_env(). \mforall{}store:C\_STOREp(). (C\_STOREp-welltyped(env;store) \mmember{} \mBbbP{})
Date html generated:
2015_07_17-AM-07_45_15
Last ObjectModification:
2015_01_27-AM-09_45_01
Home
Index