---

Step * 1 2 1 of Lemma restrict_perm_using_txpose


1. n : {1...}
2. p : Sym(n)
3. (txpose_perm(n - 1;p.f (n - 1)) O p.f (n - 1)) = (n - 1) ∈ ℕn
⊢ p = txpose_perm(n - 1;p.f (n - 1)) O txpose_perm(n - 1;p.f (n - 1)) O p ∈ Sym(n)
BY
{ (RewriteWith [] ``perm_assoc txpose_perm_order_2`` 0 THENA Auto) }

1
1. n : {1...}
2. p : Sym(n)
3. (txpose_perm(n - 1;p.f (n - 1)) O p.f (n - 1)) = (n - 1) ∈ ℕn
⊢ p = id_perm() O p ∈ Sym(n)

---

Latex:

---

Latex:

1.  n  :  \{1...\}
2.  p  :  Sym(n)
3.  (txpose\_perm(n  -  1;p.f  (n  -  1))  O  p.f  (n  -  1))  =  (n  -  1)
\mvdash{}  p  =  txpose\_perm(n  -  1;p.f  (n  -  1))  O  txpose\_perm(n  -  1;p.f  (n  -  1))  O  p


By

---

Latex:
(RewriteWith  []  ``perm\_assoc  txpose\_perm\_order\_2``  0  THENA  Auto)

---

Home Index