---

Step * 1 of Lemma C_Array-elem_vs_DVALp


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)))
BY
{ (RepUR ``C_TYPE_vs_DVALp`` (-1)
   THEN Fold `C_TYPE_vs_DVALp` (-1)
   THEN DatatypeD 5
   THEN Reduce (-1)
   THEN Try (Trivial)) }

1
1. store : C_STOREp()@i
2. length : ℕ
3. c2 : C_TYPE()
4. env : C_TYPE_env()@i
5. lower : ℤ
6. upper : ℤ
7. d3 : {lower..upper-} ─→ C_DVALUEp()
8. n : ℤ@i
9. C_STOREp-welltyped(env;store)@i
10. True@i
11. 0 ≤ n@i
12. n < length@i
13. ↑let a = lower in
      let b = upper in
      let f = d3 in
      (length =z b - a) ∧b (∀i∈upto(length).C_TYPE_vs_DVALp(env;c2) (f (a + i)))_b@i
⊢ ↑(C_TYPE_vs_DVALp(env;c2) (DVp_Array-arr(DVp_Array(lower;upper;d3)) (DVp_Array-lower(DVp_Array(lower;upper;d3)) + n)))

---

Latex:



1.  store  :  C\_STOREp()@i
2.  length  :  \mBbbN{}
3.  c2  :  C\_TYPE()
4.  env  :  C\_TYPE\_env()@i
5.  dval  :  C\_DVALUEp()@i
6.  n  :  \mBbbZ{}@i
7.  C\_STOREp-welltyped(env;store)@i
8.  True@i
9.  0  \mleq{}  n@i
10.  n  <  length@i
11.  \muparrow{}(C\_TYPE\_vs\_DVALp(env;C\_Array(length;c2))  dval)@i
\mvdash{}  \muparrow{}(C\_TYPE\_vs\_DVALp(env;c2)  (DVp\_Array-arr(dval)  (DVp\_Array-lower(dval)  +  n)))


By

(RepUR  ``C\_TYPE\_vs\_DVALp``  (-1)
  THEN  Fold  `C\_TYPE\_vs\_DVALp`  (-1)
  THEN  DatatypeD  5
  THEN  Reduce  (-1)
  THEN  Try  (Trivial))

---

Home Index