---

Step * 2 2 1 1 1 2 1 1 1 of Lemma cyclic-map-equipollent


1. n : ℕ+
2. ∀L:Combination(n - 1;ℕn - 1). ([n - 1 / L] ∈ Combination(n;ℕn))
3. orbit : ℕn List
4. 0 < ||orbit||
5. no_repeats(ℕn;orbit)
6. ∀y:ℕn. (y ∈ orbit)
7. (n - 1 ∈ orbit)
⊢ ∃a:Combination(n - 1;ℕn - 1). (cycle([n - 1 / a]) = cycle(orbit) ∈ cyclic-map(ℕn))
BY
{ xxx((RWO "l_member_decomp" (-1) THENA Auto) THEN ExRepD)xxx }

1
1. n : ℕ+
2. ∀L:Combination(n - 1;ℕn - 1). ([n - 1 / L] ∈ Combination(n;ℕn))
3. orbit : ℕn List
4. 0 < ||orbit||
5. no_repeats(ℕn;orbit)
6. ∀y:ℕn. (y ∈ orbit)
7. l1 : ℕn List
8. l2 : ℕn List
9. orbit = (l1 @ [n - 1] @ l2) ∈ (ℕn List)
⊢ ∃a:Combination(n - 1;ℕn - 1). (cycle([n - 1 / a]) = cycle(orbit) ∈ cyclic-map(ℕn))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  \mforall{}L:Combination(n  -  1;\mBbbN{}n  -  1).  ([n  -  1  /  L]  \mmember{}  Combination(n;\mBbbN{}n))
3.  orbit  :  \mBbbN{}n  List
4.  0  <  ||orbit||
5.  no\_repeats(\mBbbN{}n;orbit)
6.  \mforall{}y:\mBbbN{}n.  (y  \mmember{}  orbit)
7.  (n  -  1  \mmember{}  orbit)
\mvdash{}  \mexists{}a:Combination(n  -  1;\mBbbN{}n  -  1).  (cycle([n  -  1  /  a])  =  cycle(orbit))


By

---

Latex:
xxx((RWO  "l\_member\_decomp"  (-1)  THENA  Auto)  THEN  ExRepD)xxx

---

Home Index