---

Step * 2 1 of Lemma permutation-generators3


1. n : ℕ
2. P : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}  ⟶ ℙ
3. P[λx.x]
4. ∀f:ℕn ⟶ ℕn. (Inj(ℕn;ℕn;f) ∈ 𝕌{[1 | i 0]})
5. f : ℕn ⟶ ℕn
6. Inj(ℕn;ℕn;f)
7. i : ℕn
8. j : ℕn
9. i < j
10. P[f]
11. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P[f] ⇒ P[f o (0, 1)]) supposing 1 < n
⇒ (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P[f] ⇒ P[f o rot(n)]))
⇒ (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . P[f])
12. g : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
13. (i, j) = g ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
⊢ f o 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