---

Step * 2 1 of Lemma swap_adjacent_decomp


1. [A] : Type
2. i : ℤ
3. [%1] : 0 < i
4. ∀L:A List
     ∃X,Y:A List
      ((L = (X @ [L[i - 1]; L[(i - 1) + 1]] @ Y) ∈ (A List))
      ∧ (swap(L;i - 1;(i - 1) + 1) = (X @ [L[(i - 1) + 1]; L[i - 1]] @ Y) ∈ (A List))) 
     supposing (i - 1) + 1 < ||L||
5. L : A List
6. i + 1 < ||L||
7. ||tl(L)|| = (||L|| - 1) ∈ ℤ
8. ∃X,Y:A List
    ((tl(L) = (X @ [tl(L)[i - 1]; tl(L)[(i - 1) + 1]] @ Y) ∈ (A List))
    ∧ (swap(tl(L);i - 1;(i - 1) + 1) = (X @ [tl(L)[(i - 1) + 1]; tl(L)[i - 1]] @ Y) ∈ (A List)))
⊢ ∃X,Y:A List
   (([hd(L) / tl(L)] = (X @ [L[i]; L[i + 1]] @ Y) ∈ (A List))
   ∧ (swap([hd(L) / tl(L)];i;i + 1) = (X @ [L[i + 1]; L[i]] @ Y) ∈ (A List)))
BY
{ (((ExRepD THEN InstConcl [[hd(L) / X];Y]) THEN Reduce 0) THEN Auto) }

1
1. A : Type
2. i : ℤ
3. 0 < i
4. ∀L:A List
     ∃X,Y:A List
      ((L = (X @ [L[i - 1]; L[(i - 1) + 1]] @ Y) ∈ (A List))
      ∧ (swap(L;i - 1;(i - 1) + 1) = (X @ [L[(i - 1) + 1]; L[i - 1]] @ Y) ∈ (A List))) 
     supposing (i - 1) + 1 < ||L||
5. L : A List
6. i + 1 < ||L||
7. ||tl(L)|| = (||L|| - 1) ∈ ℤ
8. X : A List
9. Y : A List
10. tl(L) = (X @ [tl(L)[i - 1]; tl(L)[(i - 1) + 1]] @ Y) ∈ (A List)
11. swap(tl(L);i - 1;(i - 1) + 1) = (X @ [tl(L)[(i - 1) + 1]; tl(L)[i - 1]] @ Y) ∈ (A List)
⊢ [hd(L) / tl(L)] = [hd(L) / (X @ [L[i]; [L[i + 1] / Y]])] ∈ (A List)

2
1. A : Type
2. i : ℤ
3. 0 < i
4. ∀L:A List
     ∃X,Y:A List
      ((L = (X @ [L[i - 1]; L[(i - 1) + 1]] @ Y) ∈ (A List))
      ∧ (swap(L;i - 1;(i - 1) + 1) = (X @ [L[(i - 1) + 1]; L[i - 1]] @ Y) ∈ (A List))) 
     supposing (i - 1) + 1 < ||L||
5. L : A List
6. i + 1 < ||L||
7. ||tl(L)|| = (||L|| - 1) ∈ ℤ
8. X : A List
9. Y : A List
10. tl(L) = (X @ [tl(L)[i - 1]; tl(L)[(i - 1) + 1]] @ Y) ∈ (A List)
11. swap(tl(L);i - 1;(i - 1) + 1) = (X @ [tl(L)[(i - 1) + 1]; tl(L)[i - 1]] @ Y) ∈ (A List)
12. [hd(L) / tl(L)] = [hd(L) / (X @ [L[i]; [L[i + 1] / Y]])] ∈ (A List)
⊢ swap([hd(L) / tl(L)];i;i + 1) = [hd(L) / (X @ [L[i + 1]; [L[i] / Y]])] ∈ (A List)

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  i  :  \mBbbZ{}
3.  [\%1]  :  0  <  i
4.  \mforall{}L:A  List
          \mexists{}X,Y:A  List
            ((L  =  (X  @  [L[i  -  1];  L[(i  -  1)  +  1]]  @  Y))
            \mwedge{}  (swap(L;i  -  1;(i  -  1)  +  1)  =  (X  @  [L[(i  -  1)  +  1];  L[i  -  1]]  @  Y))) 
          supposing  (i  -  1)  +  1  <  ||L||
5.  L  :  A  List
6.  i  +  1  <  ||L||
7.  ||tl(L)||  =  (||L||  -  1)
8.  \mexists{}X,Y:A  List
        ((tl(L)  =  (X  @  [tl(L)[i  -  1];  tl(L)[(i  -  1)  +  1]]  @  Y))
        \mwedge{}  (swap(tl(L);i  -  1;(i  -  1)  +  1)  =  (X  @  [tl(L)[(i  -  1)  +  1];  tl(L)[i  -  1]]  @  Y)))
\mvdash{}  \mexists{}X,Y:A  List
      (([hd(L)  /  tl(L)]  =  (X  @  [L[i];  L[i  +  1]]  @  Y))
      \mwedge{}  (swap([hd(L)  /  tl(L)];i;i  +  1)  =  (X  @  [L[i  +  1];  L[i]]  @  Y)))


By

---

Latex:
(((ExRepD  THEN  InstConcl  [[hd(L)  /  X];Y])  THEN  Reduce  0)  THEN  Auto)

---

Home Index