---

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


1. n : ℕ+
2. ∀L:Combination(n - 1;ℕn - 1). ([n - 1 / L] ∈ Combination(n;ℕn))
3. b : cyclic-map(ℕn)
4. orbits : ℕn List List
5. (∀o∈orbits.orbit(ℕn;b;o))
6. ∀a:ℕn. (∃orbit∈orbits. (a ∈ orbit))
7. (∀o1,o2∈orbits.  l_disjoint(ℕn;o1;o2))
8. no_repeats(ℕn List;orbits)
⊢ ∃a:Combination(n - 1;ℕn - 1). (cycle([n - 1 / a]) = b ∈ cyclic-map(ℕn))
BY
{ ((InstHyp [⌜0⌝] (-3)⋅ THENA Auto)
   THEN D -1
   THEN (Assert orbit(ℕn;b;orbits[i]) BY
               Auto)
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN GenConclAtAddr [1;2]
   THEN (ThinVar `i' THEN ThinVar `orbits')
   THEN RenameVar `orbit' (-1)
   THEN Auto) }

1
1. n : ℕ+
2. ∀L:Combination(n - 1;ℕn - 1). ([n - 1 / L] ∈ Combination(n;ℕn))
3. b : cyclic-map(ℕn)
4. orbit : ℕn List
5. (0 ∈ orbit)
6. orbit(ℕn;b;orbit)
⊢ ∃a:Combination(n - 1;ℕn - 1). (cycle([n - 1 / a]) = b ∈ 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.  b  :  cyclic-map(\mBbbN{}n)
4.  orbits  :  \mBbbN{}n  List  List
5.  (\mforall{}o\mmember{}orbits.orbit(\mBbbN{}n;b;o))
6.  \mforall{}a:\mBbbN{}n.  (\mexists{}orbit\mmember{}orbits.  (a  \mmember{}  orbit))
7.  (\mforall{}o1,o2\mmember{}orbits.    l\_disjoint(\mBbbN{}n;o1;o2))
8.  no\_repeats(\mBbbN{}n  List;orbits)
\mvdash{}  \mexists{}a:Combination(n  -  1;\mBbbN{}n  -  1).  (cycle([n  -  1  /  a])  =  b)


By

---

Latex:
((InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  (Assert  orbit(\mBbbN{}n;b;orbits[i])  BY
                          Auto)
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  GenConclAtAddr  [1;2]
  THEN  (ThinVar  `i'  THEN  ThinVar  `orbits')
  THEN  RenameVar  `orbit'  (-1)
  THEN  Auto)

---

Home Index