---

Step * 1 1 of Lemma swap-exists


1. n : ℕ
2. AType : array{i:l}(ℤ;n)
3. i : ℕn
4. j : ℕn
⊢ alt-swap-spec(AType;n;λi,j. simple-swap(array-model(AType);i;j))
BY
{ TACTIC:ExposeArrayOps 2 }

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. i : ℕn
9. j : ℕn
⊢ alt-swap-spec(<Arr, idx, upd, newarray, A5, A6>;n;λi,j. simple-swap(array-model(<Arr, idx, upd, newarray, A5, A6>);i;j\000C))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  AType  :  array\{i:l\}(\mBbbZ{};n)
3.  i  :  \mBbbN{}n
4.  j  :  \mBbbN{}n
\mvdash{}  alt-swap-spec(AType;n;\mlambda{}i,j.  simple-swap(array-model(AType);i;j))


By

---

Latex:
TACTIC:ExposeArrayOps  2

---

Home Index