---

Step * 1 1 2 1 2 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. ∀i,j:ℕn. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} .  (P[f] ⇒ P[(i, j) o f])
8. c : ℕn List
9. no_repeats(ℕn;c)
10. f1 : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
11. P[f1]
12. flips : (ℕn × ℕn) List
13. cycle(c) = compose-flips(flips) ∈ (ℕn ⟶ ℕn)
14. cycle(c) = compose-flips(flips) ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
⊢ P[cycle(c) o f1]
BY
{ (HypSubst (-1) 0 ⋅ 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)} . (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])
8. c : ℕn List
9. no_repeats(ℕn;c)
10. f1 : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
11. P[f1]
12. flips : (ℕn × ℕn) List
13. cycle(c) = compose-flips(flips) ∈ (ℕn ⟶ ℕn)
14. cycle(c) = compose-flips(flips) ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
⊢ P[compose-flips(flips) o f1]

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])
8. c : ℕn List
9. no_repeats(ℕn;c)
10. f1 : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
11. P[f1]
12. flips : (ℕn × ℕn) List
13. cycle(c) = compose-flips(flips) ∈ (ℕn ⟶ ℕn)
14. cycle(c) = compose-flips(flips) ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
15. z : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
⊢ z o f1 ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;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{}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])
8.  c  :  \mBbbN{}n  List
9.  no\_repeats(\mBbbN{}n;c)
10.  f1  :  \{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\} 
11.  P[f1]
12.  flips  :  (\mBbbN{}n  \mtimes{}  \mBbbN{}n)  List
13.  cycle(c)  =  compose-flips(flips)
14.  cycle(c)  =  compose-flips(flips)
\mvdash{}  P[cycle(c)  o  f1]


By

---

Latex:
(HypSubst  (-1)  0  \mcdot{}  THEN  Auto)

---

Home Index