---

Step * of Lemma C_Array_vs_DVALp

∀store:C_STOREp(). ∀ctyp:C_TYPE(). ∀env:C_TYPE_env(). ∀dval:C_DVALUEp().
  (C_STOREp-welltyped(env;store)
  ⇒ (↑C_Array?(ctyp))
  ⇒ C_TYPE_vs_DVALp(env;ctyp) dval 
     = if DVp_Array?(dval)
       then let a = DVp_Array-lower(dval) in
             let b = DVp_Array-upper(dval) in
             let f = DVp_Array-arr(dval) in
             (C_Array-length(ctyp) =z b - a)
             ∧b (∀i∈upto(C_Array-length(ctyp)).C_TYPE_vs_DVALp(env;C_Array-elems(ctyp)) (f (a + i)))_b
       else ff
       fi )
BY
{ ((D 0 THENA Auto)
   THEN RepUR ``let`` 0
   THEN (BLemma `C_TYPE-induction` THEN Reduce 0)
   THEN Auto
   THEN Unfold `C_TYPE_vs_DVALp` 0
   THEN Reduce 0
   THEN Fold `C_TYPE_vs_DVALp` 0
   THEN RepUR ``let`` 0
   THEN Auto) }

---

Latex:


\mforall{}store:C\_STOREp().  \mforall{}ctyp:C\_TYPE().  \mforall{}env:C\_TYPE\_env().  \mforall{}dval:C\_DVALUEp().
    (C\_STOREp-welltyped(env;store)
    {}\mRightarrow{}  (\muparrow{}C\_Array?(ctyp))
    {}\mRightarrow{}  C\_TYPE\_vs\_DVALp(env;ctyp)  dval 
          =  if  DVp\_Array?(dval)
              then  let  a  =  DVp\_Array-lower(dval)  in
                          let  b  =  DVp\_Array-upper(dval)  in
                          let  f  =  DVp\_Array-arr(dval)  in
                          (C\_Array-length(ctyp)  =\msubz{}  b  -  a)
                          \mwedge{}\msubb{}  (\mforall{}i\mmember{}upto(C\_Array-length(ctyp)).C\_TYPE\_vs\_DVALp(env;C\_Array-elems(ctyp)) 
                                                                                              (f  (a  +  i)))\_b
              else  ff
              fi  )


By

((D  0  THENA  Auto)
  THEN  RepUR  ``let``  0
  THEN  (BLemma  `C\_TYPE-induction`  THEN  Reduce  0)
  THEN  Auto
  THEN  Unfold  `C\_TYPE\_vs\_DVALp`  0
  THEN  Reduce  0
  THEN  Fold  `C\_TYPE\_vs\_DVALp`  0
  THEN  RepUR  ``let``  0
  THEN  Auto)

---

Home Index