---

Step * 1 2 of Lemma swap_adjacent_decomp


1. A : Type
2. L : A List
3. 1 < ||L||
4. L = [L[0]; [L[1] / tl(tl(L))]] ∈ (A List)
⊢ swap(L;0;1) = [L[1]; [L[0] / tl(tl(L))]] ∈ (A List)
BY
{ xxx(((AssertBY ||tl(L)|| = (||L|| - 1) ∈ ℤ  (RWW "length_tl" 0 THEN Auto)
        THEN AssertBY ||tl(tl(L))|| = (||L|| - 2) ∈ ℤ  (RWW "length_tl" 0 THEN Auto)
        )
       THEN BackThruLemma `list_extensionality`
       )
      THENA Auto
      )xxx }

1
1. A : Type
2. L : A List
3. 1 < ||L||
4. L = [L[0]; [L[1] / tl(tl(L))]] ∈ (A List)
5. ||tl(L)|| = (||L|| - 1) ∈ ℤ
6. ||tl(tl(L))|| = (||L|| - 2) ∈ ℤ
⊢ ||swap(L;0;1)|| = ||[L[1]; [L[0] / tl(tl(L))]]|| ∈ ℤ

2
1. A : Type
2. L : A List
3. 1 < ||L||
4. L = [L[0]; [L[1] / tl(tl(L))]] ∈ (A List)
5. ||tl(L)|| = (||L|| - 1) ∈ ℤ
6. ||tl(tl(L))|| = (||L|| - 2) ∈ ℤ
⊢ ∀i:ℕ. (i < ||swap(L;0;1)|| ⇒ (swap(L;0;1)[i] = [L[1]; [L[0] / tl(tl(L))]][i] ∈ A))

---

Latex:

---

Latex:

1.  A  :  Type
2.  L  :  A  List
3.  1  <  ||L||
4.  L  =  [L[0];  [L[1]  /  tl(tl(L))]]
\mvdash{}  swap(L;0;1)  =  [L[1];  [L[0]  /  tl(tl(L))]]


By

---

Latex:
xxx(((AssertBY  ||tl(L)||  =  (||L||  -  1)  (RWW  "length\_tl"  0  THEN  Auto)
            THEN  AssertBY  ||tl(tl(L))||  =  (||L||  -  2)  (RWW  "length\_tl"  0  THEN  Auto)
            )
          THEN  BackThruLemma  `list\_extensionality`
          )
        THENA  Auto
        )xxx

---

Home Index