---

Step * 1 1 1 1 1 of Lemma C_Array-elem_vs_DVALp

.....wf..... 
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) ∈ ℤ
⊢ n ∈ ℕ||upto(length)||
BY
{ (RWO "length_upto" 0 THEN Auto) }

---

Latex:


.....wf..... 
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)
\mvdash{}  n  \mmember{}  \mBbbN{}||upto(length)||


By

(RWO  "length\_upto"  0  THEN  Auto)

---

Home Index