---

Step * 1 of Lemma fetch'-commutes


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)
BY
{ xxx(Fold `member` 0 THEN ExtWith [`B'][⌜Top ⟶ Top⌝]⋅ THEN Try (Complete (Auto)) THEN Reduce 0)xxx }

---

Latex:

---

Latex:

1.  Val  :  Type
2.  S  :  Type
3.  n  :  \mBbbN{}
4.  Arr  :  Type
5.  idx  :  \mBbbN{}n  {}\mrightarrow{}  Arr  {}\mrightarrow{}  Val
6.  upd  :  \mBbbN{}n  {}\mrightarrow{}  Val  {}\mrightarrow{}  Arr  {}\mrightarrow{}  Arr
7.  newarray  :  Val  {}\mrightarrow{}  Arr
8.  A5  :  \mforall{}[i:\mBbbN{}n].  \mforall{}[v:Val].    ((idx  i  (newarray  v))  =  v)
9.  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  )
10.  prog  :  Val  {}\mrightarrow{}  Val  {}\mrightarrow{}  (A-map'(array-model(<Arr,  idx,  upd,  newarray,  A5,  A6>))  S)
11.  j  :  \mBbbN{}n
12.  k  :  \mBbbN{}n
\mvdash{}  (\mlambda{}A.(prog  (idx  k  A)  (idx  j  A)  A))  =  (\mlambda{}A.(prog  (idx  k  A)  (idx  j  A)  A))


By

---

Latex:
xxx(Fold  `member`  0  THEN  ExtWith  [`B'][\mkleeneopen{}Top  {}\mrightarrow{}  Top\mkleeneclose{}]\mcdot{}  THEN  Try  (Complete  (Auto))  THEN  Reduce  0)xxx

---

Home Index