---

Step * 1 1 1 1 of Lemma restrict_perm_using_txpose


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
BY
{ SplitOnConclITEs 
THEN Auto }

---

Latex:

---

Latex:

1.  n  :  \{1...\}
2.  p  :  Sym(n)
\mvdash{}  if  (p.f  (n  -  1)  =\msubz{}  n  -  1)  then  p.f  (n  -  1)
if  (p.f  (n  -  1)  =\msubz{}  p.f  (n  -  1))  then  n  -  1
else  p.f  (n  -  1)
fi 
=  (n  -  1)


By

---

Latex:
SplitOnConclITEs 
THEN  Auto

---

Home Index