---

Step * 2 of Lemma l_before_swap


1. [T] : Type
2. L : T List
3. i : ℕ||L|| - 1
4. a : T
5. b : T
6. f : ℕ2 ⟶ ℕ||swap(L;i;i + 1)||
7. increasing(f;2)
8. ∀j:ℕ2. ([a; b][j] = L[(i, i + 1) (f j)] ∈ T)
9. ||swap(L;i;i + 1)|| = ||L|| ∈ ℤ
10. a = L[(i, i + 1) (f 0)] ∈ T
11. b = L[(i, i + 1) (f 1)] ∈ T
12. (i, i + 1) ∈ ℕ||L|| ⟶ ℕ||L||
13. ¬(i, i + 1) (f 0) < (i, i + 1) (f 1)
⊢ [L[(i, i + 1) (f 0)]; L[(i, i + 1) (f 1)]] ⊆ L
∨ ((L[(i, i + 1) (f 0)] = L[i + 1] ∈ T) ∧ (L[(i, i + 1) (f 1)] = L[i] ∈ T))
BY
{ xxx(OrRight THENA Auto)xxx }

1
1. [T] : Type
2. L : T List
3. i : ℕ||L|| - 1
4. a : T
5. b : T
6. f : ℕ2 ⟶ ℕ||swap(L;i;i + 1)||
7. increasing(f;2)
8. ∀j:ℕ2. ([a; b][j] = L[(i, i + 1) (f j)] ∈ T)
9. ||swap(L;i;i + 1)|| = ||L|| ∈ ℤ
10. a = L[(i, i + 1) (f 0)] ∈ T
11. b = L[(i, i + 1) (f 1)] ∈ T
12. (i, i + 1) ∈ ℕ||L|| ⟶ ℕ||L||
13. ¬(i, i + 1) (f 0) < (i, i + 1) (f 1)
⊢ (L[(i, i + 1) (f 0)] = L[i + 1] ∈ T) ∧ (L[(i, i + 1) (f 1)] = L[i] ∈ T)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L  :  T  List
3.  i  :  \mBbbN{}||L||  -  1
4.  a  :  T
5.  b  :  T
6.  f  :  \mBbbN{}2  {}\mrightarrow{}  \mBbbN{}||swap(L;i;i  +  1)||
7.  increasing(f;2)
8.  \mforall{}j:\mBbbN{}2.  ([a;  b][j]  =  L[(i,  i  +  1)  (f  j)])
9.  ||swap(L;i;i  +  1)||  =  ||L||
10.  a  =  L[(i,  i  +  1)  (f  0)]
11.  b  =  L[(i,  i  +  1)  (f  1)]
12.  (i,  i  +  1)  \mmember{}  \mBbbN{}||L||  {}\mrightarrow{}  \mBbbN{}||L||
13.  \mneg{}(i,  i  +  1)  (f  0)  <  (i,  i  +  1)  (f  1)
\mvdash{}  [L[(i,  i  +  1)  (f  0)];  L[(i,  i  +  1)  (f  1)]]  \msubseteq{}  L
\mvee{}  ((L[(i,  i  +  1)  (f  0)]  =  L[i  +  1])  \mwedge{}  (L[(i,  i  +  1)  (f  1)]  =  L[i]))


By

---

Latex:
xxx(OrRight  THENA  Auto)xxx

---

Home Index