---

Step * 1 1 1 1 2 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. 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. length = (upper - lower) ∈ ℤ
14. length = (upper - lower) ∈ ℤ
15. ↑(C_TYPE_vs_DVALp(env;c2) (d3 (lower + upto(length)[n])))
⊢ ↑(C_TYPE_vs_DVALp(env;c2) (d3 (lower + n)))
BY
{ (RWO "select-upto" (-1) THEN Auto) }

---

Latex:



1.  store  :  C\_STOREp()@i
2.  length  :  \mBbbN{}
3.  c2  :  C\_TYPE()
4.  env  :  C\_TYPE\_env()@i
5.  lower  :  \mBbbZ{}
6.  upper  :  \mBbbZ{}
7.  d3  :  \{lower..upper\msupminus{}\}  {}\mrightarrow{}  C\_DVALUEp()
8.  n  :  \mBbbZ{}@i
9.  C\_STOREp-welltyped(env;store)@i
10.  True@i
11.  0  \mleq{}  n@i
12.  n  <  length@i
13.  length  =  (upper  -  lower)
14.  length  =  (upper  -  lower)
15.  \muparrow{}(C\_TYPE\_vs\_DVALp(env;c2)  (d3  (lower  +  upto(length)[n])))
\mvdash{}  \muparrow{}(C\_TYPE\_vs\_DVALp(env;c2)  (d3  (lower  +  n)))


By

(RWO  "select-upto"  (-1)  THEN  Auto)

---

Home Index