---

Step * 1 2 1 of Lemma permutation-generators


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. ∀c:ℕn List. (no_repeats(ℕn;c) ⇒ (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P[f] ⇒ P[cycle(c) o f])))
8. cycles : ℕn List List
9. no_repeats(ℕn List;cycles)
10. (∀c1∈cycles.(∀c2∈cycles.(c1 = c2 ∈ (ℕn List)) ∨ l_disjoint(ℕn;c1;c2)))
11. (∀c∈cycles.0 < ||c|| ∧ no_repeats(ℕn;c))
12. f = reduce(λc,g. (cycle(c) o g);λx.x;cycles) ∈ (ℕn ⟶ ℕn)
⊢ P[f]
BY
{ ((Assert Inj(ℕn;ℕn;reduce(λc,g. (cycle(c) o g);λx.x;cycles)) BY
          (RevHypSubst' (-1) 0 THEN Auto))
   THEN PromoteHyp (-1) (-5)
   THEN Assert ⌜P[reduce(λc,g. (cycle(c) o g);λx.x;cycles)]⌝⋅) }

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)} 
7. ∀c:ℕn List. (no_repeats(ℕn;c) ⇒ (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P[f] ⇒ P[cycle(c) o f])))
8. cycles : ℕn List List
9. Inj(ℕn;ℕn;reduce(λc,g. (cycle(c) o g);λx.x;cycles))
10. no_repeats(ℕn List;cycles)
11. (∀c1∈cycles.(∀c2∈cycles.(c1 = c2 ∈ (ℕn List)) ∨ l_disjoint(ℕn;c1;c2)))
12. (∀c∈cycles.0 < ||c|| ∧ no_repeats(ℕn;c))
13. f = reduce(λc,g. (cycle(c) o g);λx.x;cycles) ∈ (ℕn ⟶ ℕn)
⊢ P[reduce(λc,g. (cycle(c) o g);λx.x;cycles)]

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. ∀c:ℕn List. (no_repeats(ℕn;c) ⇒ (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P[f] ⇒ P[cycle(c) o f])))
8. cycles : ℕn List List
9. Inj(ℕn;ℕn;reduce(λc,g. (cycle(c) o g);λx.x;cycles))
10. no_repeats(ℕn List;cycles)
11. (∀c1∈cycles.(∀c2∈cycles.(c1 = c2 ∈ (ℕn List)) ∨ l_disjoint(ℕn;c1;c2)))
12. (∀c∈cycles.0 < ||c|| ∧ no_repeats(ℕn;c))
13. f = reduce(λc,g. (cycle(c) o g);λx.x;cycles) ∈ (ℕn ⟶ ℕn)
14. P[reduce(λc,g. (cycle(c) o g);λx.x;cycles)]
⊢ P[f]

---

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:\{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)\} 
7.  \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])))
8.  cycles  :  \mBbbN{}n  List  List
9.  no\_repeats(\mBbbN{}n  List;cycles)
10.  (\mforall{}c1\mmember{}cycles.(\mforall{}c2\mmember{}cycles.(c1  =  c2)  \mvee{}  l\_disjoint(\mBbbN{}n;c1;c2)))
11.  (\mforall{}c\mmember{}cycles.0  <  ||c||  \mwedge{}  no\_repeats(\mBbbN{}n;c))
12.  f  =  reduce(\mlambda{}c,g.  (cycle(c)  o  g);\mlambda{}x.x;cycles)
\mvdash{}  P[f]


By

---

Latex:
((Assert  Inj(\mBbbN{}n;\mBbbN{}n;reduce(\mlambda{}c,g.  (cycle(c)  o  g);\mlambda{}x.x;cycles))  BY
                (RevHypSubst'  (-1)  0  THEN  Auto))
  THEN  PromoteHyp  (-1)  (-5)
  THEN  Assert  \mkleeneopen{}P[reduce(\mlambda{}c,g.  (cycle(c)  o  g);\mlambda{}x.x;cycles)]\mkleeneclose{}\mcdot{})

---

Home Index