---

Step * 1 of Lemma swap_swap


1. T : Type
2. L1 : T List
3. i : ℕ||L1||
4. j : ℕ||L1||
5. ||swap(L1;i;j)|| = ||L1|| ∈ ℤ
6. ||swap(swap(L1;i;j);i;j)|| = ||swap(L1;i;j)|| ∈ ℤ
7. i1 : ℕ
8. i1 < ||swap(swap(L1;i;j);i;j)||
⊢ swap(swap(L1;i;j);i;j)[i1] = L1[i1] ∈ T
BY
{ (((RWW "swap_select" 0 THENA Auto') THEN RWO "flip_twice" 0) THEN Auto') }

1
1. T : Type
2. L1 : T List
3. i : ℕ||L1||
4. j : ℕ||L1||
5. ||swap(L1;i;j)|| = ||L1|| ∈ ℤ
6. ||swap(swap(L1;i;j);i;j)|| = ||swap(L1;i;j)|| ∈ ℤ
7. i1 : ℕ
8. i1 < ||swap(swap(L1;i;j);i;j)||
9. 0 ≤ ((i, j) ((i, j) i1))
⊢ (i, j) ((i, j) i1) < ||L1||

---

Latex:

---

Latex:

1.  T  :  Type
2.  L1  :  T  List
3.  i  :  \mBbbN{}||L1||
4.  j  :  \mBbbN{}||L1||
5.  ||swap(L1;i;j)||  =  ||L1||
6.  ||swap(swap(L1;i;j);i;j)||  =  ||swap(L1;i;j)||
7.  i1  :  \mBbbN{}
8.  i1  <  ||swap(swap(L1;i;j);i;j)||
\mvdash{}  swap(swap(L1;i;j);i;j)[i1]  =  L1[i1]


By

---

Latex:
(((RWW  "swap\_select"  0  THENA  Auto')  THEN  RWO  "flip\_twice"  0)  THEN  Auto')

---

Home Index