---

Step * 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. ↑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)))
BY
{ (RepUR ``let`` -1
   THEN Reduce 0
   THEN (BoolCase ⌈(length =z upper - lower)⌉⋅ THENA Auto)
   THEN (RW assert_pushdownC (-2) THENA 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) ∈ ℤ) ∧ (∀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)))

---

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.  \muparrow{}let  a  =  lower  in
            let  b  =  upper  in
            let  f  =  d3  in
            (length  =\msubz{}  b  -  a)  \mwedge{}\msubb{}  (\mforall{}i\mmember{}upto(length).C\_TYPE\_vs\_DVALp(env;c2)  (f  (a  +  i)))\_b@i
\mvdash{}  \muparrow{}(C\_TYPE\_vs\_DVALp(env;c2) 
        (DVp\_Array-arr(DVp\_Array(lower;upper;d3))  (DVp\_Array-lower(DVp\_Array(lower;upper;d3))  +  n)))


By

(RepUR  ``let``  -1
  THEN  Reduce  0
  THEN  (BoolCase  \mkleeneopen{}(length  =\msubz{}  upper  -  lower)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (RW  assert\_pushdownC  (-2)  THENA  Auto))

---

Home Index