---

Step * of Lemma simple-swap-correct

∀[n:ℕ]. ∀[AType:array{i:l}(ℤ;n)]. ∀[prog:A-map Unit].
  ∀i,j:ℕn.  simple-swap-specification(AType;n;simple-swap(array-model(AType);i;j);i;j)
BY
{ (Auto
   THEN Unfold `simple-swap-specification` 0
   THEN Auto
   THEN Unfolds ``simple-swap-test2 simple-swap`` 0
   THEN (RepUR ``A-eval array-model A-bind mk_monad array-monad
   let M-bind M-map A-coerce A-fetch' M-return A-return A-assign`` 0)⋅
   THEN ((Unfold `array` -6 THEN RepeatFor 5 (D -6)) THEN RepUR ``Arr`` -1)
   THEN RepUR ``idx upd`` 0
   THEN RW assert_pushdownC 0
   THEN Auto
   THEN Try ((Unfold `uimplies` 0 THEN Auto))) }

1
1. n : ℕ
2. Arr : Type
3. idx : ℕn ⟶ Arr ⟶ ℤ
4. upd : ℕn ⟶ ℤ ⟶ Arr ⟶ Arr
5. newarray : ℤ ⟶ Arr
6. A5 : ∀[i:ℕn]. ∀[v:ℤ].  ((idx i (newarray v)) = v ∈ ℤ)
7. A6 : ∀[i,j:ℕn]. ∀[x:Arr]. ∀[v:ℤ].  ((idx i (upd j v x)) = if (i =z j) then v else idx i x fi  ∈ ℤ)
8. prog : A-map Unit
9. i : ℕn
10. j : ℕn
11. k : ℕn
12. A : Arr
⊢ (idx i (upd j (idx i A) (upd i (idx j A) A))) = (idx j A) ∈ ℤ

2
1. n : ℕ
2. Arr : Type
3. idx : ℕn ⟶ Arr ⟶ ℤ
4. upd : ℕn ⟶ ℤ ⟶ Arr ⟶ Arr
5. newarray : ℤ ⟶ Arr
6. A5 : ∀[i:ℕn]. ∀[v:ℤ].  ((idx i (newarray v)) = v ∈ ℤ)
7. A6 : ∀[i,j:ℕn]. ∀[x:Arr]. ∀[v:ℤ].  ((idx i (upd j v x)) = if (i =z j) then v else idx i x fi  ∈ ℤ)
8. prog : A-map Unit
9. i : ℕn
10. j : ℕn
11. k : ℕn
12. A : Arr
13. (idx i (upd j (idx i A) (upd i (idx j A) A))) = (idx j A) ∈ ℤ
⊢ (idx j (upd j (idx i A) (upd i (idx j A) A))) = (idx i A) ∈ ℤ

3
1. n : ℕ
2. Arr : Type
3. idx : ℕn ⟶ Arr ⟶ ℤ
4. upd : ℕn ⟶ ℤ ⟶ Arr ⟶ Arr
5. newarray : ℤ ⟶ Arr
6. A5 : ∀[i:ℕn]. ∀[v:ℤ].  ((idx i (newarray v)) = v ∈ ℤ)
7. A6 : ∀[i,j:ℕn]. ∀[x:Arr]. ∀[v:ℤ].  ((idx i (upd j v x)) = if (i =z j) then v else idx i x fi  ∈ ℤ)
8. prog : A-map Unit
9. i : ℕn
10. j : ℕn
11. k : ℕn
12. A : Arr
13. (idx i (upd j (idx i A) (upd i (idx j A) A))) = (idx j A) ∈ ℤ
14. (idx j (upd j (idx i A) (upd i (idx j A) A))) = (idx i A) ∈ ℤ
15. ¬(k = i ∈ ℤ)
16. ¬(k = j ∈ ℤ)
⊢ (idx k (upd j (idx i A) (upd i (idx j A) A))) = (idx k A) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[AType:array\{i:l\}(\mBbbZ{};n)].  \mforall{}[prog:A-map  Unit].
    \mforall{}i,j:\mBbbN{}n.    simple-swap-specification(AType;n;simple-swap(array-model(AType);i;j);i;j)


By

---

Latex:
(Auto
  THEN  Unfold  `simple-swap-specification`  0
  THEN  Auto
  THEN  Unfolds  ``simple-swap-test2  simple-swap``  0
  THEN  (RepUR  ``A-eval  array-model  A-bind  mk\_monad  array-monad
  let  M-bind  M-map  A-coerce  A-fetch'  M-return  A-return  A-assign``  0)\mcdot{}
  THEN  ((Unfold  `array`  -6  THEN  RepeatFor  5  (D  -6))  THEN  RepUR  ``Arr``  -1)
  THEN  RepUR  ``idx  upd``  0
  THEN  RW  assert\_pushdownC  0
  THEN  Auto
  THEN  Try  ((Unfold  `uimplies`  0  THEN  Auto)))

---

Home Index