Step
*
1
1
of Lemma
permutation-generators
.....assertion..... 
1. n : ℕ
2. [P] : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}  ⟶ ℙ
3. P[λx.x]
4. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P[f] 
⇒ P[(0, 1) o f]) supposing 1 < n
5. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P[f] 
⇒ P[rot(n) o f])
6. f : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
⊢ ∀c:ℕn List. (no_repeats(ℕn;c) 
⇒ (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P[f] 
⇒ P[cycle(c) o f])))
BY
{ Assert ⌜∀i,j:ℕn. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} .  (P[f] 
⇒ P[(i, j) o f])⌝⋅ }
1
.....assertion..... 
1. n : ℕ
2. [P] : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}  ⟶ ℙ
3. P[λx.x]
4. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P[f] 
⇒ P[(0, 1) o f]) supposing 1 < n
5. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P[f] 
⇒ P[rot(n) o f])
6. f : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
⊢ ∀i,j:ℕn. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} .  (P[f] 
⇒ P[(i, j) o f])
2
1. n : ℕ
2. [P] : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}  ⟶ ℙ
3. P[λx.x]
4. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P[f] 
⇒ P[(0, 1) o f]) supposing 1 < n
5. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P[f] 
⇒ P[rot(n) o f])
6. f : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
7. ∀i,j:ℕn. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} .  (P[f] 
⇒ P[(i, j) o f])
⊢ ∀c:ℕn List. (no_repeats(ℕn;c) 
⇒ (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P[f] 
⇒ P[cycle(c) o f])))
Latex:
Latex:
.....assertion..... 
1.  n  :  \mBbbN{}
2.  [P]  :  \{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}    {}\mrightarrow{}  \mBbbP{}
3.  P[\mlambda{}x.x]
4.  \mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  .  (P[f]  {}\mRightarrow{}  P[(0,  1)  o  f])  supposing  1  <  n
5.  \mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  .  (P[f]  {}\mRightarrow{}  P[rot(n)  o  f])
6.  f  :  \{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\} 
\mvdash{}  \mforall{}c:\mBbbN{}n  List.  (no\_repeats(\mBbbN{}n;c)  {}\mRightarrow{}  (\mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  .  (P[f]  {}\mRightarrow{}  P[cycle(c)  o  f])))
By
Latex:
Assert  \mkleeneopen{}\mforall{}i,j:\mBbbN{}n.  \mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  .    (P[f]  {}\mRightarrow{}  P[(i,  j)  o  f])\mkleeneclose{}\mcdot{}
Home
Index