---

Step * of Lemma coerce-fetch'-commutes

∀[Val,S:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. ∀[prog:Val ⟶ Val ⟶ (A-map S)].
  ∀j,k:ℕn.
    ((A-bind(array-model(AType)) (A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) k)) 
      (λval@k.(A-bind(array-model(AType)) (A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) j)) 
               (λval@j.(prog val@k val@j)))))
    = (A-bind(array-model(AType)) (A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) j)) 
       (λval@j.(A-bind(array-model(AType)) (A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) k)) 
                (λval@k.(prog val@k val@j)))))
    ∈ (A-map 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 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 × Arr))

---

Latex:

---

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