---

Step * 2 1 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 + 1] ∈ T) ∧ (L[(i, i + 1) (f 1)] = L[i] ∈ T)
BY
{ xxx(((MoveToConcl (-1) THEN Unfold `flip` 0) THEN Reduce 0)
      THEN AssertBY f 0 < f 1
           (AllHyps (\h. (((FwdThruLemma `increasing_implies` [h] THENA Auto) THEN BackThruHyp (-1)) THEN Auto)))
      THEN RepeatFor 4 (AutoSplit))xxx }

---

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  +  1])  \mwedge{}  (L[(i,  i  +  1)  (f  1)]  =  L[i])


By

---

Latex:
xxx(((MoveToConcl  (-1)  THEN  Unfold  `flip`  0)  THEN  Reduce  0)
        THEN  AssertBY  f  0  <  f  1
                  (AllHyps  (\mbackslash{}h.  (((FwdThruLemma  `increasing\_implies`  [h]  THENA  Auto)  THEN  BackThruHyp  (-1))
                                                THEN  Auto
                                                )))
        THEN  RepeatFor  4  (AutoSplit))xxx

---

Home Index