---

Step * 1 1 of Lemma A-null-property


1. Val : Type
2. n : ℕ
3. Arr : Type
4. idx : ℕn ⟶ Arr ⟶ Val
5. upd : ℕn ⟶ Val ⟶ Arr ⟶ Arr
6. newarray : Val ⟶ Arr
7. A5 : ∀[i:ℕn]. ∀[v:Val].  ((idx i (newarray v)) = v ∈ Val)
8. A6 : ∀[i,j:ℕn]. ∀[x:Arr]. ∀[v:Val].  ((idx i (upd j v x)) = if (i =z j) then v else idx i x fi  ∈ Val)
9. A : Arr@i
10. k : ℕn@i
⊢ (A-eval(array-model(<Arr, idx, upd, newarray, A5, A6>)) 
   (A-bind(array-model(<Arr, idx, upd, newarray, A5, A6>)) (A-return(array-model(<Arr, idx, upd, newarray, A5, A6>)) ⋅) 
    (λx.(A-coerce(array-model(<Arr, idx, upd, newarray, A5, A6>)) (A-fetch'(array-model(<Arr, idx, upd, newarray, A5, A6\000C>)) k)))) 
   A)
= (idx(<Arr, idx, upd, newarray, A5, A6>) k A)
∈ Val
BY
{ (ComputeArrayOps 0 THEN Auto) }

---

Latex:

---

Latex:

1.  Val  :  Type
2.  n  :  \mBbbN{}
3.  Arr  :  Type
4.  idx  :  \mBbbN{}n  {}\mrightarrow{}  Arr  {}\mrightarrow{}  Val
5.  upd  :  \mBbbN{}n  {}\mrightarrow{}  Val  {}\mrightarrow{}  Arr  {}\mrightarrow{}  Arr
6.  newarray  :  Val  {}\mrightarrow{}  Arr
7.  A5  :  \mforall{}[i:\mBbbN{}n].  \mforall{}[v:Val].    ((idx  i  (newarray  v))  =  v)
8.  A6  :  \mforall{}[i,j:\mBbbN{}n].  \mforall{}[x:Arr].  \mforall{}[v:Val].    ((idx  i  (upd  j  v  x))  =  if  (i  =\msubz{}  j)  then  v  else  idx  i  x  fi  )
9.  A  :  Arr@i
10.  k  :  \mBbbN{}n@i
\mvdash{}  (A-eval(array-model(<Arr,  idx,  upd,  newarray,  A5,  A6>)) 
      (A-bind(array-model(<Arr,  idx,  upd,  newarray,  A5,  A6>))  (A-return(array-model(<Arr,  idx,  upd,  new\000Carray,  A5,  A6>))  \mcdot{}) 
        (\mlambda{}x.(A-coerce(array-model(<Arr,  idx,  upd,  newarray,  A5,  A6>))  (A-fetch'(array-model(<Arr,  idx,  u\000Cpd,  newarray,  A5,  A6>))  k)))) 
      A)
=  (idx(<Arr,  idx,  upd,  newarray,  A5,  A6>)  k  A)


By

---

Latex:
(ComputeArrayOps  0  THEN  Auto)

---

Home Index