---

Step * 3 of Lemma simple-swap-correct


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) ∈ ℤ
BY
{ ((InstHyp [⌜k⌝;⌜j⌝;⌜upd i (idx j A) A⌝;⌜idx i A⌝] 7⋅ THENA Auto) THEN SplitOnHypITE (-1) THEN Auto) }

1
.....falsecase..... 
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 ∈ ℤ)
17. (idx k (upd j (idx i A) (upd i (idx j A) A))) = (idx k (upd i (idx j A) A)) ∈ ℤ
18. ¬(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.  prog  :  A-map  Unit
9.  i  :  \mBbbN{}n
10.  j  :  \mBbbN{}n
11.  k  :  \mBbbN{}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.  \mneg{}(k  =  i)
16.  \mneg{}(k  =  j)
\mvdash{}  (idx  k  (upd  j  (idx  i  A)  (upd  i  (idx  j  A)  A)))  =  (idx  k  A)


By

---

Latex:
((InstHyp  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}upd  i  (idx  j  A)  A\mkleeneclose{};\mkleeneopen{}idx  i  A\mkleeneclose{}]  7\mcdot{}  THENA  Auto)  THEN  SplitOnHypITE  (-1)  THEN  Auto)

---

Home Index