---

Step * 2 2 1 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. 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))
BY
{ xxx(Assert ∀y:ℕn. (y ∈ orbit) BY
            ((InstLemma `cyclic-map-transitive` [⌜n⌝;⌜b⌝;⌜0⌝]⋅ THENA Auto)
             THEN ParallelLast
             THEN ExRepD
             THEN RevHypSubst' -1 0
             THEN Auto
             THEN FLemma `orbit-closed` [6]
             THEN Auto
             THEN RWO "l_all_iff" (-1)
             THEN Auto))xxx }

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)
7. ∀y:ℕn. (y ∈ 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.  orbit  :  \mBbbN{}n  List
5.  (0  \mmember{}  orbit)
6.  orbit(\mBbbN{}n;b;orbit)
\mvdash{}  \mexists{}a:Combination(n  -  1;\mBbbN{}n  -  1).  (cycle([n  -  1  /  a])  =  b)


By

---

Latex:
xxx(Assert  \mforall{}y:\mBbbN{}n.  (y  \mmember{}  orbit)  BY
                    ((InstLemma  `cyclic-map-transitive`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{}]\mcdot{}  THENA  Auto)
                      THEN  ParallelLast
                      THEN  ExRepD
                      THEN  RevHypSubst'  -1  0
                      THEN  Auto
                      THEN  FLemma  `orbit-closed`  [6]
                      THEN  Auto
                      THEN  RWO  "l\_all\_iff"  (-1)
                      THEN  Auto))xxx

---

Home Index