---

Step * of 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)))))
BY
{ ((Auto THEN InstLemma `C_LVALUE-proper-Index` [⌈env⌉;⌈LV_Index(lval;i)⌉]⋅)
   THEN Try (Complete (Auto))
   THEN RepUR ``let`` -1
   THEN Auto) }

---

Latex:


\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)))))


By

((Auto  THEN  InstLemma  `C\_LVALUE-proper-Index`  [\mkleeneopen{}env\mkleeneclose{};\mkleeneopen{}LV\_Index(lval;i)\mkleeneclose{}]\mcdot{})
  THEN  Try  (Complete  (Auto))
  THEN  RepUR  ``let``  -1
  THEN  Auto)

---

Home Index