---

Step * 1 of Lemma restrict_perm_using_txpose


1. n : {1...}
2. p : Sym(n)
⊢ ∃q:Sym(n - 1). ∃i,j:ℕn. (p = txpose_perm(i;j) O ↑{n - 1}(q) ∈ Sym(n))
BY
{ ((Assert (txpose_perm(n - 1;p.f (n - 1)) O p.f (n - 1)) = (n - 1) ∈ ℕn
   THENM InstConcl [restrict_perm(txpose_perm(n - 1
                                              ;p.f (n - 1))
                                   O p;n - 1); n - 1; p.f (n - 1)]
   )
   THENW Auto
   ) }

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

2
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 ↑{n - 1}(restrict_perm(txpose_perm(n - 1;p.f (n - 1)) O p;n - 1)) ∈ Sym(n)

---

Latex:

---

Latex:

1.  n  :  \{1...\}
2.  p  :  Sym(n)
\mvdash{}  \mexists{}q:Sym(n  -  1).  \mexists{}i,j:\mBbbN{}n.  (p  =  txpose\_perm(i;j)  O  \muparrow{}\{n  -  1\}(q))


By

---

Latex:
((Assert  (txpose\_perm(n  -  1;p.f  (n  -  1))  O  p.f  (n  -  1))  =  (n  -  1)
  THENM  InstConcl  [restrict\_perm(txpose\_perm(n  -  1
                                                                                        ;p.f  (n  -  1))
                                                                  O  p;n  -  1);  n  -  1;  p.f  (n  -  1)]
  )
  THENW  Auto
  )

---

Home Index