---

Step * of Lemma C_LVALUE-proper-Index

∀env:C_TYPE_env(). ∀lval:C_LVALUE().
  ((↑LV_Index?(lval))
  ⇒ (↑C_LVALUE-proper(env;lval))
  ⇒ let lval' = LV_Index-lval(lval) in
      let i = LV_Index-idx(lval) in
      let typ = outl(C_TYPE-of-LVALUE(env;lval')) in
      (↑C_LVALUE-proper(env;lval')) ∧ (↑C_Array?(typ)) ∧ (0 ≤ i) ∧ i < C_Array-length(typ))
BY
{ ((D 0 THENA Auto)
   THEN BLemma `C_LVALUE-induction`
   THEN RepUR ``let`` 0
   THEN Auto
   THEN OnMaybeHyp 6 (\h. ((RepUR ``C_LVALUE-proper C_TYPE-of-LVALUE`` h
                            THEN Fold `C_TYPE-of-LVALUE` h
                            THEN Fold `C_LVALUE-proper` h)
                           THEN RepeatFor 3 ((SplitOnHypITE h  THEN Auto))
                           ))) }

---

Latex:


\mforall{}env:C\_TYPE\_env().  \mforall{}lval:C\_LVALUE().
    ((\muparrow{}LV\_Index?(lval))
    {}\mRightarrow{}  (\muparrow{}C\_LVALUE-proper(env;lval))
    {}\mRightarrow{}  let  lval'  =  LV\_Index-lval(lval)  in
            let  i  =  LV\_Index-idx(lval)  in
            let  typ  =  outl(C\_TYPE-of-LVALUE(env;lval'))  in
            (\muparrow{}C\_LVALUE-proper(env;lval'))  \mwedge{}  (\muparrow{}C\_Array?(typ))  \mwedge{}  (0  \mleq{}  i)  \mwedge{}  i  <  C\_Array-length(typ))


By

((D  0  THENA  Auto)
  THEN  BLemma  `C\_LVALUE-induction`
  THEN  RepUR  ``let``  0
  THEN  Auto
  THEN  OnMaybeHyp  6  (\mbackslash{}h.  ((RepUR  ``C\_LVALUE-proper  C\_TYPE-of-LVALUE``  h
                                                    THEN  Fold  `C\_TYPE-of-LVALUE`  h
                                                    THEN  Fold  `C\_LVALUE-proper`  h)
                                                  THEN  RepeatFor  3  ((SplitOnHypITE  h    THEN  Auto))
                                                  )))

---

Home Index