Nuprl Lemma : C_LVALUE-proper-Indexed
∀env:C_TYPE_env(). ∀lval:C_LVALUE(). ∀i:ℤ.
((↑C_LVALUE-proper(env;LV_Index(lval;i))) ⇒ (↑C_Array?(outl(C_TYPE-of-LVALUE(env;lval)))))
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(),
LV_Index: LV_Index(lval;idx),
C_LVALUE: C_LVALUE(),
C_Array?: C_Array?(v),
outl: outl(x),
assert: ↑b,
all: ∀x:A. B[x],
implies: P ⇒ Q,
int: ℤ
Lemmas :
C_LVALUE-proper-Index,
assert_wf,
C_LVALUE-proper_wf,
LV_Index_wf,
C_LVALUE_wf,
C_TYPE_env_wf
\mforall{}env:C\_TYPE\_env(). \mforall{}lval:C\_LVALUE(). \mforall{}i:\mBbbZ{}.
((\muparrow{}C\_LVALUE-proper(env;LV\_Index(lval;i))) {}\mRightarrow{} (\muparrow{}C\_Array?(outl(C\_TYPE-of-LVALUE(env;lval)))))
Date html generated:
2015_07_17-AM-07_43_52
Last ObjectModification:
2015_01_27-AM-09_45_57
Home
Index