---

Step * of Lemma fetch'-commutes

∀[Val,S:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. ∀[prog:Val ⟶ Val ⟶ (A-map'(array-model(AType)) S)].
  ∀j,k:ℕn.
    ((A-bind'(array-model(AType)) (A-fetch'(array-model(AType)) k) 
      (λval@k.(A-bind'(array-model(AType)) (A-fetch'(array-model(AType)) j) (λval@j.(prog val@k val@j)))))
    = (A-bind'(array-model(AType)) (A-fetch'(array-model(AType)) j) 
       (λval@j.(A-bind'(array-model(AType)) (A-fetch'(array-model(AType)) k) (λval@k.(prog val@k val@j)))))
    ∈ (A-map'(array-model(AType)) S))
BY
{ (Auto THEN ExposeArrayOps 4 THEN ComputeArrayOps 0) }

1
1. Val : Type
2. S : Type
3. n : ℕ
4. Arr : Type
5. idx : ℕn ⟶ Arr ⟶ Val
6. upd : ℕn ⟶ Val ⟶ Arr ⟶ Arr
7. newarray : Val ⟶ Arr
8. A5 : ∀[i:ℕn]. ∀[v:Val].  ((idx i (newarray v)) = v ∈ Val)
9. 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)
10. prog : Val ⟶ Val ⟶ (A-map'(array-model(<Arr, idx, upd, newarray, A5, A6>)) S)
11. j : ℕn
12. k : ℕn
⊢ (λA.(prog (idx k A) (idx j A) A)) = (λA.(prog (idx k A) (idx j A) A)) ∈ (Arr ⟶ S)

---

Latex:

---

Latex:
\mforall{}[Val,S:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[AType:array\{i:l\}(Val;n)].  \mforall{}[prog:Val
                                                                                                                    {}\mrightarrow{}  Val
                                                                                                                    {}\mrightarrow{}  (A-map'(array-model(AType))  S)].
    \mforall{}j,k:\mBbbN{}n.
        ((A-bind'(array-model(AType))  (A-fetch'(array-model(AType))  k) 
            (\mlambda{}val@k.(A-bind'(array-model(AType))  (A-fetch'(array-model(AType))  j) 
                              (\mlambda{}val@j.(prog  val@k  val@j)))))
        =  (A-bind'(array-model(AType))  (A-fetch'(array-model(AType))  j) 
              (\mlambda{}val@j.(A-bind'(array-model(AType))  (A-fetch'(array-model(AType))  k) 
                                (\mlambda{}val@k.(prog  val@k  val@j))))))


By

---

Latex:
(Auto  THEN  ExposeArrayOps  4  THEN  ComputeArrayOps  0)

---

Home Index