---

Step * of Lemma swap_swap

∀[T:Type]. ∀[L1:T List]. ∀[i,j:ℕ||L1||].  (swap(swap(L1;i;j);i;j) = L1 ∈ (T List))
BY
{ ((((((Auto THEN InstLemma `swap_length` [T;L1;i;j]) THENA Auto) THEN InstLemma `swap_length` [T;swap(L1;i;j);i;j])
     THENA Auto'
     )
    THEN BackThruLemma `list_extensionality`
    )
   THEN Auto
   ) }

1
1. T : Type
2. L1 : T List
3. i : ℕ||L1||
4. j : ℕ||L1||
5. ||swap(L1;i;j)|| = ||L1|| ∈ ℤ
6. ||swap(swap(L1;i;j);i;j)|| = ||swap(L1;i;j)|| ∈ ℤ
7. i1 : ℕ
8. i1 < ||swap(swap(L1;i;j);i;j)||
⊢ swap(swap(L1;i;j);i;j)[i1] = L1[i1] ∈ T

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L1:T  List].  \mforall{}[i,j:\mBbbN{}||L1||].    (swap(swap(L1;i;j);i;j)  =  L1)


By

---

Latex:
((((((Auto  THEN  InstLemma  `swap\_length`  [T;L1;i;j])  THENA  Auto)
        THEN  InstLemma  `swap\_length`  [T;swap(L1;i;j);i;j]
        )
      THENA  Auto'
      )
    THEN  BackThruLemma  `list\_extensionality`
    )
  THEN  Auto
  )

---

Home Index