---

Step * of Lemma permutation-generators3

∀n:ℕ
  ∀[P:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}  ⟶ ℙ]
    (P[λx.x]
    ⇒ (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . ∀i,j:ℕn.  P[f] ⇒ P[f o (i, j)] supposing i < j)
    ⇒ (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . P[f]))
BY
{ (InstLemma `permutation-generators2` [] THEN RepeatFor 2 (ParallelLast') THEN Auto) }

1
1. n : ℕ
2. [P] : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}  ⟶ ℙ
3. P[λx.x]
4. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . ∀i,j:ℕn.  P[f] ⇒ P[f o (i, j)] supposing i < j
5. f : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
6. ∀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])
⊢ P[f]

2
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])
⊢ f o (i, j) ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}
    \mforall{}[P:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}    {}\mrightarrow{}  \mBbbP{}]
        (P[\mlambda{}x.x]
        {}\mRightarrow{}  (\mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  .  \mforall{}i,j:\mBbbN{}n.    P[f]  {}\mRightarrow{}  P[f  o  (i,  j)]  supposing  i  <  j)
        {}\mRightarrow{}  (\mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  .  P[f]))


By

---

Latex:
(InstLemma  `permutation-generators2`  []  THEN  RepeatFor  2  (ParallelLast')  THEN  Auto)

---

Home Index