---

Step * 1 1 2 1 of Lemma swap_adjacent_decomp


1. A : Type
2. L : A List
3. 1 < ||L||
4. ||tl(tl(L))|| = (||L|| - 2) ∈ ℤ
5. i : ℕ
6. i < ||L||
7. ¬(i = 0 ∈ ℤ)
⊢ L[i] = [L[0]; [L[1] / tl(tl(L))]][i] ∈ A
BY
{ xxx(RWO "select_cons_tl" 0 THENA (Reduce 0 THEN Auto))xxx }

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

---

Latex:

---

Latex:

1.  A  :  Type
2.  L  :  A  List
3.  1  <  ||L||
4.  ||tl(tl(L))||  =  (||L||  -  2)
5.  i  :  \mBbbN{}
6.  i  <  ||L||
7.  \mneg{}(i  =  0)
\mvdash{}  L[i]  =  [L[0];  [L[1]  /  tl(tl(L))]][i]


By

---

Latex:
xxx(RWO  "select\_cons\_tl"  0  THENA  (Reduce  0  THEN  Auto))xxx

---

Home Index