---

Step * 1 1 of Lemma restrict_perm_using_txpose

.....assertion..... 
1. n : {1...}
2. p : Sym(n)
⊢ (txpose_perm(n - 1;p.f (n - 1)) O p.f (n - 1)) = (n - 1) ∈ ℕn
BY
{ Unfold `txpose_perm` 0 THEN AbReduce 0 }

1
1. n : {1...}
2. p : Sym(n)
⊢ (swap(n - 1;p.f (n - 1)) (p.f (n - 1))) = (n - 1) ∈ ℕn

---

Latex:

---

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


By

---

Latex:
Unfold  `txpose\_perm`  0  THEN  AbReduce  0

---

Home Index