---

Step * 2 2 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)
⊢ ∃a:Combination(n - 1;ℕn - 1). (cycle([n - 1 / a]) = b ∈ cyclic-map(ℕn))
BY
{ xxx((InstLemma `orbit-decomp2` [⌜ℕn⌝;⌜b⌝]⋅
       THENA (Auto
              THEN Try ((BLemma `finite-type-int_seg` THEN Auto))
              THEN RepeatFor 2 (DVar `b')
              THEN Try (Unhide)
              THEN Auto)
       )
      THEN ExRepD
      )xxx }

1
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))

---

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)
\mvdash{}  \mexists{}a:Combination(n  -  1;\mBbbN{}n  -  1).  (cycle([n  -  1  /  a])  =  b)


By

---

Latex:
xxx((InstLemma  `orbit-decomp2`  [\mkleeneopen{}\mBbbN{}n\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}
          THENA  (Auto
                        THEN  Try  ((BLemma  `finite-type-int\_seg`  THEN  Auto))
                        THEN  RepeatFor  2  (DVar  `b')
                        THEN  Try  (Unhide)
                        THEN  Auto)
          )
        THEN  ExRepD
        )xxx

---

Home Index