Step
*
1
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])
⊢ ∀c:ℕn List. (no_repeats(ℕn;c) ⇒ (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P[f] ⇒ P[cycle(c) o f])))
BY
{ (Auto THEN (InstLemma `cycle-as-flips` [⌜n⌝;⌜c⌝]⋅ THENA Auto) THEN ExRepD) }
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)
⊢ P[cycle(c) o f1]
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])
\mvdash{} \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])))
By
Latex:
(Auto THEN (InstLemma `cycle-as-flips` [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{} THENA Auto) THEN ExRepD)
Home
Index