---

Step * 1 2 2 1 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) ∈ ℤ
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
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. 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[0] / tl(tl(L))][i - 1] ∈ 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)
7.  i  :  \mBbbN{}
8.  i  <  ||swap(L;0;1)||
9.  swap(L;0;1)[0]  =  L[1]
10.  swap(L;0;1)[1]  =  L[0]
11.  ||swap(L;0;1)||  =  ||L||
12.  L  =  swap(swap(L;0;1);0;1)
13.  \mforall{}[x:\mBbbN{}||swap(L;0;1)||].  (swap(L;0;1)[x]  =  L[x])  supposing  ((\mneg{}(x  =  1))  and  (\mneg{}(x  =  0)))
14.  \mneg{}(i  =  0)
\mvdash{}  swap(L;0;1)[i]  =  [L[1];  [L[0]  /  tl(tl(L))]][i]


By

---

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

---

Home Index