---

Step * of Lemma swap_adjacent_decomp

∀[A:Type]
  ∀i:ℕ. ∀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
{ InductionOnNat }

1
.....basecase..... 
1. [A] : Type
⊢ ∀L:A List
    ∃X,Y:A List
     ((L = (X @ [L[0]; L[0 + 1]] @ Y) ∈ (A List)) ∧ (swap(L;0;0 + 1) = (X @ [L[0 + 1]; L[0]] @ Y) ∈ (A List))) 
    supposing 0 + 1 < ||L||

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

---

Latex:

---

Latex:
\mforall{}[A:Type]
    \mforall{}i:\mBbbN{}.  \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:
InductionOnNat

---

Home Index