---

Step * 2 of Lemma swap_adjacent_decomp

.....upcase..... 
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||
⊢ ∀L:A List
    ∃X,Y:A List
     ((L = (X @ [L[i]; L[i + 1]] @ Y) ∈ (A List)) ∧ (swap(L;i;i + 1) = (X @ [L[i + 1]; L[i]] @ Y) ∈ (A List))) 
    supposing i + 1 < ||L||
BY
{ (((((((Auto THEN AssertBY ||tl(L)|| = (||L|| - 1) ∈ ℤ  (RWW "length_tl" 0 THEN Auto)) THEN ListDecomp [2;2;1;2] 0)
       THENA Auto
       )
      THEN ListDecomp [2;2;2;2;1] 0
      )
     THENA Auto
     )
    THEN InstHyp [tl(L)] 4
    )
   THENA Auto
   ) }

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

---

Latex:

---

Latex:
.....upcase..... 
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||
\mvdash{}  \mforall{}L:A  List
        \mexists{}X,Y:A  List
          ((L  =  (X  @  [L[i];  L[i  +  1]]  @  Y))  \mwedge{}  (swap(L;i;i  +  1)  =  (X  @  [L[i  +  1];  L[i]]  @  Y))) 
        supposing  i  +  1  <  ||L||


By

---

Latex:
(((((((Auto  THEN  AssertBY  ||tl(L)||  =  (||L||  -  1)  (RWW  "length\_tl"  0  THEN  Auto))
            THEN  ListDecomp  [2;2;1;2]  0
            )
          THENA  Auto
          )
        THEN  ListDecomp  [2;2;2;2;1]  0
        )
      THENA  Auto
      )
    THEN  InstHyp  [tl(L)]  4
    )
  THENA  Auto
  )

---

Home Index