---

Step * of Lemma C_Array-elem_vs_DVALp

∀store:C_STOREp(). ∀ctyp:C_TYPE(). ∀env:C_TYPE_env(). ∀dval:C_DVALUEp(). ∀n:ℤ.
  (C_STOREp-welltyped(env;store)
  ⇒ (↑C_Array?(ctyp))
  ⇒ (0 ≤ n)
  ⇒ n < C_Array-length(ctyp)
  ⇒ (↑(C_TYPE_vs_DVALp(env;ctyp) dval))
  ⇒ (↑(C_TYPE_vs_DVALp(env;C_Array-elems(ctyp)) (DVp_Array-arr(dval) (DVp_Array-lower(dval) + n)))))
BY
{ (RepeatFor 10 ((D 0 THENA Auto)) THEN DatatypeD 2 THEN All Reduce THEN Try (Trivial)) }

1
1. store : C_STOREp()@i
2. length : ℕ
3. c2 : C_TYPE()
4. env : C_TYPE_env()@i
5. dval : C_DVALUEp()@i
6. n : ℤ@i
7. C_STOREp-welltyped(env;store)@i
8. True@i
9. 0 ≤ n@i
10. n < length@i
11. ↑(C_TYPE_vs_DVALp(env;C_Array(length;c2)) dval)@i
⊢ ↑(C_TYPE_vs_DVALp(env;c2) (DVp_Array-arr(dval) (DVp_Array-lower(dval) + n)))

---

Latex:


\mforall{}store:C\_STOREp().  \mforall{}ctyp:C\_TYPE().  \mforall{}env:C\_TYPE\_env().  \mforall{}dval:C\_DVALUEp().  \mforall{}n:\mBbbZ{}.
    (C\_STOREp-welltyped(env;store)
    {}\mRightarrow{}  (\muparrow{}C\_Array?(ctyp))
    {}\mRightarrow{}  (0  \mleq{}  n)
    {}\mRightarrow{}  n  <  C\_Array-length(ctyp)
    {}\mRightarrow{}  (\muparrow{}(C\_TYPE\_vs\_DVALp(env;ctyp)  dval))
    {}\mRightarrow{}  (\muparrow{}(C\_TYPE\_vs\_DVALp(env;C\_Array-elems(ctyp)) 
                (DVp\_Array-arr(dval)  (DVp\_Array-lower(dval)  +  n)))))


By

(RepeatFor  10  ((D  0  THENA  Auto))  THEN  DatatypeD  2  THEN  All  Reduce  THEN  Try  (Trivial))

---

Home Index