---

Step * of Lemma l_before_swap

∀[T:Type]
  ∀L:T List. ∀i:ℕ||L|| - 1. ∀a,b:T.
    (a before b ∈ swap(L;i;i + 1) ⇒ (a before b ∈ L ∨ ((a = L[i + 1] ∈ T) ∧ (b = L[i] ∈ T))))
BY
{ xxx(Auto
      THEN All (Unfold `l_before`)
      THEN Unfold `sublist` (-1)
      THEN ExRepD
      THEN All Reduce
      THEN (InstLemma `swap_length` [T;L;i;i + 1] THENA Auto)
      THEN (RWO "swap_select" (-2) THENA Auto)
      THEN (InstHyp [0] (-2) THENA Auto)
      THEN Reduce (-1)
      THEN (InstHyp [⌜1⌝] (-3)⋅ THENA Auto)
      THEN Reduce (-1)
      THEN (InstLemma `flip_wf` [||L||;i;i + 1] THENA Auto)
      THEN WeakSubstFor a 0
      THEN WeakSubstFor b 0
      THEN (Decide (i, i + 1) (f 0) < (i, i + 1) (f 1) 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, i + 1) (f 1)]] ⊆ L
∨ ((L[(i, i + 1) (f 0)] = L[i + 1] ∈ T) ∧ (L[(i, i + 1) (f 1)] = L[i] ∈ T))

2
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))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}L:T  List.  \mforall{}i:\mBbbN{}||L||  -  1.  \mforall{}a,b:T.
        (a  before  b  \mmember{}  swap(L;i;i  +  1)  {}\mRightarrow{}  (a  before  b  \mmember{}  L  \mvee{}  ((a  =  L[i  +  1])  \mwedge{}  (b  =  L[i]))))


By

---

Latex:
xxx(Auto
        THEN  All  (Unfold  `l\_before`)
        THEN  Unfold  `sublist`  (-1)
        THEN  ExRepD
        THEN  All  Reduce
        THEN  (InstLemma  `swap\_length`  [T;L;i;i  +  1]  THENA  Auto)
        THEN  (RWO  "swap\_select"  (-2)  THENA  Auto)
        THEN  (InstHyp  [0]  (-2)  THENA  Auto)
        THEN  Reduce  (-1)
        THEN  (InstHyp  [\mkleeneopen{}1\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
        THEN  Reduce  (-1)
        THEN  (InstLemma  `flip\_wf`  [||L||;i;i  +  1]  THENA  Auto)
        THEN  WeakSubstFor  a  0
        THEN  WeakSubstFor  b  0
        THEN  (Decide  (i,  i  +  1)  (f  0)  <  (i,  i  +  1)  (f  1)  THENA  Auto))xxx

---

Home Index