---

Step * 1 1 1 of Lemma restrict_perm_using_txpose


1. n : {1...}
2. p : Sym(n)
⊢ (swap(n - 1;p.f (n - 1)) (p.f (n - 1))) = (n - 1) ∈ ℕn
BY
{ Unfolds ``compose swap`` 0 THEN AbReduce 0 }

1
1. n : {1...}
2. p : Sym(n)
⊢ if (p.f (n - 1) =z n - 1) then p.f (n - 1)
if (p.f (n - 1) =z p.f (n - 1)) then n - 1
else p.f (n - 1)
fi 
= (n - 1)
∈ ℕn

---

Latex:

---

Latex:

1.  n  :  \{1...\}
2.  p  :  Sym(n)
\mvdash{}  (swap(n  -  1;p.f  (n  -  1))  (p.f  (n  -  1)))  =  (n  -  1)


By

---

Latex:
Unfolds  ``compose  swap``  0  THEN  AbReduce  0

---

Home Index