---

Step * 1 2 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)
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))
BY
{ xxx(((((Auto THEN InstLemma `swapped_select` [A;L;swap(L;0;1);0;1]) THEN Auto) THEN CaseNat 0 `i') THEN Reduce 0)
      THEN 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) ∈ ℤ
7. i : ℕ
8. i < ||swap(L;0;1)||
9. swap(L;0;1)[0] = L[1] ∈ A
10. swap(L;0;1)[1] = L[0] ∈ A
11. ||swap(L;0;1)|| = ||L|| ∈ ℤ
12. L = swap(swap(L;0;1);0;1) ∈ (A List)
13. ∀[x:ℕ||swap(L;0;1)||]. (swap(L;0;1)[x] = L[x] ∈ A) supposing ((¬(x = 1 ∈ ℤ)) and (¬(x = 0 ∈ ℤ)))
14. ¬(i = 0 ∈ ℤ)
⊢ 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))]]
5.  ||tl(L)||  =  (||L||  -  1)
6.  ||tl(tl(L))||  =  (||L||  -  2)
\mvdash{}  \mforall{}i:\mBbbN{}.  (i  <  ||swap(L;0;1)||  {}\mRightarrow{}  (swap(L;0;1)[i]  =  [L[1];  [L[0]  /  tl(tl(L))]][i]))


By

---

Latex:
xxx(((((Auto  THEN  InstLemma  `swapped\_select`  [A;L;swap(L;0;1);0;1])  THEN  Auto)  THEN  CaseNat  0  `i')
          THEN  Reduce  0
          )
        THEN  Auto
        )xxx

---

Home Index