---

Step * 2 1 1 of Lemma swap_adjacent_decomp


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)
BY
{ ((((WeakSubstFor tl(L) 0 THEN Reduce 0) THEN Auto) THEN RWO "select_tl" 0) THEN Auto) }

---

Latex:

---

Latex:

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)
\mvdash{}  [hd(L)  /  tl(L)]  =  [hd(L)  /  (X  @  [L[i];  [L[i  +  1]  /  Y]])]


By

---

Latex:
((((WeakSubstFor  tl(L)  0  THEN  Reduce  0)  THEN  Auto)  THEN  RWO  "select\_tl"  0)  THEN  Auto)

---

Home Index