---

Step * 1 1 1 of Lemma swap-exists


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))
BY
{ (RepUR ``alt-swap-spec A-post-val A-pre-val simple-swap`` 0 THEN ComputeArrayOps 0)⋅ }

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
⊢ ∀A:Arr. ∀i,j,k:ℕn.
    ((((idx j (upd j (idx i A) (upd i (idx j A) A))) = (idx i A) ∈ ℤ)
    ∧ ((idx i (upd j (idx i A) (upd i (idx j A) A))) = (idx j A) ∈ ℤ))
    ∧ (((¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))) ⇒ ((idx k (upd j (idx i A) (upd i (idx j A) A))) = (idx k A) ∈ ℤ)))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  Arr  :  Type
3.  idx  :  \mBbbN{}n  {}\mrightarrow{}  Arr  {}\mrightarrow{}  \mBbbZ{}
4.  upd  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}  {}\mrightarrow{}  Arr  {}\mrightarrow{}  Arr
5.  newarray  :  \mBbbZ{}  {}\mrightarrow{}  Arr
6.  A5  :  \mforall{}[i:\mBbbN{}n].  \mforall{}[v:\mBbbZ{}].    ((idx  i  (newarray  v))  =  v)
7.  A6  :  \mforall{}[i,j:\mBbbN{}n].  \mforall{}[x:Arr].  \mforall{}[v:\mBbbZ{}].    ((idx  i  (upd  j  v  x))  =  if  (i  =\msubz{}  j)  then  v  else  idx  i  x  fi  )
8.  i  :  \mBbbN{}n
9.  j  :  \mBbbN{}n
\mvdash{}  alt-swap-spec(<Arr,  idx,  upd,  newarray,  A5,  A6>n;\mlambda{}i,j.  simple-swap(array-model(<Arr,  idx,  upd,  ne\000Cwarray,  A5,  A6>);i;j))


By

---

Latex:
(RepUR  ``alt-swap-spec  A-post-val  A-pre-val  simple-swap``  0  THEN  ComputeArrayOps  0)\mcdot{}

---

Home Index