---

Step * 1 1 2 of Lemma swap_adjacent_decomp


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))
BY
{ xxx(((Auto THEN CaseNat 0 `i') THEN 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[0]; [L[1] / tl(tl(L))]][i] ∈ A

---

Latex:

---

Latex:

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


By

---

Latex:
xxx(((Auto  THEN  CaseNat  0  `i')  THEN  Reduce  0)  THEN  Auto)xxx

---

Home Index