---

Step * 1 of Lemma A-null-property


1. Val : Type
2. n : ℕ
3. AType : array{i:l}(Val;n)
4. A : Arr(AType)@i
5. k : ℕn@i
⊢ (A-eval(array-model(AType)) 
   (A-bind(array-model(AType)) (A-return(array-model(AType)) ⋅) 
    (λx.(A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) k)))) 
   A)
= (idx(AType) k A)
∈ Val
BY
{ ExposeArrayOps (-3) }

1
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

---

Latex:

---

Latex:

1.  Val  :  Type
2.  n  :  \mBbbN{}
3.  AType  :  array\{i:l\}(Val;n)
4.  A  :  Arr(AType)@i
5.  k  :  \mBbbN{}n@i
\mvdash{}  (A-eval(array-model(AType)) 
      (A-bind(array-model(AType))  (A-return(array-model(AType))  \mcdot{}) 
        (\mlambda{}x.(A-coerce(array-model(AType))  (A-fetch'(array-model(AType))  k)))) 
      A)
=  (idx(AType)  k  A)


By

---

Latex:
ExposeArrayOps  (-3)

---

Home Index