Step * 2 1 of Lemma permutation-generators3


1. : ℕ
2. {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}  ⟶ ℙ
3. P[λx.x]
4. ∀f:ℕn ⟶ ℕn. (Inj(ℕn;ℕn;f) ∈ 𝕌{[1 0]})
5. : ℕn ⟶ ℕn
6. Inj(ℕn;ℕn;f)
7. : ℕn
8. : ℕn
9. i < j
10. P[f]
11. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} (P[f]  P[f (0, 1)]) supposing 1 < n
 (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} (P[f]  P[f rot(n)]))
 (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} P[f])
12. {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
13. (i, j) g ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
⊢ g ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
BY
(D -2 THEN MemTypeCD THEN EAuto 1) }


Latex:


Latex:

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:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n.  (Inj(\mBbbN{}n;\mBbbN{}n;f)  \mmember{}  \mBbbU{}\{[1  |  i  0]\})
5.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n
6.  Inj(\mBbbN{}n;\mBbbN{}n;f)
7.  i  :  \mBbbN{}n
8.  j  :  \mBbbN{}n
9.  i  <  j
10.  P[f]
11.  \mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  .  (P[f]  {}\mRightarrow{}  P[f  o  (0,  1)])  supposing  1  <  n
{}\mRightarrow{}  (\mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  .  (P[f]  {}\mRightarrow{}  P[f  o  rot(n)]))
{}\mRightarrow{}  (\mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  .  P[f])
12.  g  :  \{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\} 
13.  (i,  j)  =  g
\mvdash{}  f  o  g  \mmember{}  \{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\} 


By


Latex:
(D  -2  THEN  MemTypeCD  THEN  EAuto  1)




Home Index