---

Step * 1 of Lemma swap_order_2


1. n : ℕ
2. i : ℕn
3. j : ℕn
⊢ (swap(i;j) o swap(i;j)) = Id ∈ (ℕn ⟶ ℕn)
BY
{ (((Unfolds ``compose identity`` 0 THEN ExtWith [] [ℕn ⟶ ℕn]) THENM AbReduce 0) THENA Auto) }

1
1. n : ℕ
2. i : ℕn
3. j : ℕn
4. x : ℕn
⊢ (swap(i;j) (swap(i;j) x)) = x ∈ ℕn

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  i  :  \mBbbN{}n
3.  j  :  \mBbbN{}n
\mvdash{}  (swap(i;j)  o  swap(i;j))  =  Id


By

---

Latex:
(((Unfolds  ``compose  identity``  0  THEN  ExtWith  []  [\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n])  THENM  AbReduce  0)  THENA  Auto)

---

Home Index