---

Step * 2 1 2 1 of Lemma swap_adjacent_decomp

.....subterm..... T:t
2:n
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(tl(L);i - 1;(i + 1) - 1) = (X @ [L[i + 1]; [L[i] / Y]]) ∈ (A List)
BY
{ xxx(RWO "select_tl" (-2) THENA Auto)xxx }

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 @ [L[((i - 1) + 1) + 1]; L[(i - 1) + 1]] @ Y) ∈ (A List)
12. [hd(L) / tl(L)] = [hd(L) / (X @ [L[i]; [L[i + 1] / Y]])] ∈ (A List)
⊢ swap(tl(L);i - 1;(i + 1) - 1) = (X @ [L[i + 1]; [L[i] / Y]]) ∈ (A List)

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  A  :  Type
2.  i  :  \mBbbZ{}
3.  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.  X  :  A  List
9.  Y  :  A  List
10.  tl(L)  =  (X  @  [tl(L)[i  -  1];  tl(L)[(i  -  1)  +  1]]  @  Y)
11.  swap(tl(L);i  -  1;(i  -  1)  +  1)  =  (X  @  [tl(L)[(i  -  1)  +  1];  tl(L)[i  -  1]]  @  Y)
12.  [hd(L)  /  tl(L)]  =  [hd(L)  /  (X  @  [L[i];  [L[i  +  1]  /  Y]])]
\mvdash{}  swap(tl(L);i  -  1;(i  +  1)  -  1)  =  (X  @  [L[i  +  1];  [L[i]  /  Y]])


By

---

Latex:
xxx(RWO  "select\_tl"  (-2)  THENA  Auto)xxx

---

Home Index