---

Step * 1 1 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. 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) ∈ ℤ) ∧ (∀i∈upto(length).↑(C_TYPE_vs_DVALp(env;c2) (d3 (lower + i))))
14. length = (upper - lower) ∈ ℤ
⊢ ↑(C_TYPE_vs_DVALp(env;c2) (d3 (lower + n)))
BY
{ Auto }

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. length = (upper - lower) ∈ ℤ
14. (∀i∈upto(length).↑(C_TYPE_vs_DVALp(env;c2) (d3 (lower + i))))
15. length = (upper - lower) ∈ ℤ
⊢ ↑(C_TYPE_vs_DVALp(env;c2) (d3 (lower + n)))

---

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))  \mwedge{}  (\mforall{}i\mmember{}upto(length).\muparrow{}(C\_TYPE\_vs\_DVALp(env;c2)  (d3  (lower  +  i))))
14.  length  =  (upper  -  lower)
\mvdash{}  \muparrow{}(C\_TYPE\_vs\_DVALp(env;c2)  (d3  (lower  +  n)))


By

Auto

---

Home Index