---

Step * 1 1 of Lemma swap_adjacent_decomp


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

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

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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index