---

Step * 1 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)||
9. 0 ≤ ((i, j) ((i, j) i1))
⊢ (i, j) ((i, j) i1) < ||L1||
BY
{ (RWO "flip_twice" 0 THEN Auto) }

---

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)||
9.  0  \mleq{}  ((i,  j)  ((i,  j)  i1))
\mvdash{}  (i,  j)  ((i,  j)  i1)  <  ||L1||


By

---

Latex:
(RWO  "flip\_twice"  0  THEN  Auto)

---

Home Index