---

Step * of Lemma cycle-decomp

∀n:ℕ. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} .
  ∃cycles:ℕn List List
   (no_repeats(ℕn List;cycles)
   ∧ (∀c1∈cycles.(∀c2∈cycles.(c1 = c2 ∈ (ℕn List)) ∨ l_disjoint(ℕn;c1;c2)))
   ∧ (∀c∈cycles.0 < ||c|| ∧ no_repeats(ℕn;c))
   ∧ (f = reduce(λc,g. (cycle(c) o g);λx.x;cycles) ∈ (ℕn ⟶ ℕn)))
BY
{ (Auto
   THEN (InstLemma `orbit-decomp` [⌜ℕn⌝;⌜f⌝]⋅ THENA (Auto THEN Try ((BLemma `finite-type-int_seg` THEN Auto))))
   THEN Try ((D (-1) THEN Unhide THEN Auto))
   THEN ParallelLast
   THEN SplitAndHyps
   THEN (RWO "l_all_iff" (-3) THENA Auto)
   THEN RWO "l_all_iff" 0
   THEN Auto) }

1
1. n : ℕ
2. f : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
3. orbits : ℕn List List
4. ∀orbit:ℕn List
     ((orbit ∈ orbits)
     ⇒ (0 < ||orbit||
        ∧ no_repeats(ℕn;orbit)
        ∧ (∀i:ℕ||orbit||. ((f orbit[i]) = if (i =z ||orbit|| - 1) then orbit[0] else orbit[i + 1] fi  ∈ ℕn))
        ∧ (∀x∈orbit.∀n@0:ℕ. (f^n@0 x ∈ orbit))))
5. ∀a:ℕn. (∃orbit∈orbits. (a ∈ orbit))
6. (∀o1,o2∈orbits.  l_disjoint(ℕn;o1;o2))
⊢ no_repeats(ℕn List;orbits)

2
1. n : ℕ
2. f : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
3. orbits : ℕn List List
4. ∀orbit:ℕn List
     ((orbit ∈ orbits)
     ⇒ (0 < ||orbit||
        ∧ no_repeats(ℕn;orbit)
        ∧ (∀i:ℕ||orbit||. ((f orbit[i]) = if (i =z ||orbit|| - 1) then orbit[0] else orbit[i + 1] fi  ∈ ℕn))
        ∧ (∀x∈orbit.∀n@0:ℕ. (f^n@0 x ∈ orbit))))
5. ∀a:ℕn. (∃orbit∈orbits. (a ∈ orbit))
6. (∀o1,o2∈orbits.  l_disjoint(ℕn;o1;o2))
7. no_repeats(ℕn List;orbits)
8. c1 : ℕn List
9. (c1 ∈ orbits)
⊢ (∀c2∈orbits.(c1 = c2 ∈ (ℕn List)) ∨ l_disjoint(ℕn;c1;c2))

3
1. n : ℕ
2. f : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
3. orbits : ℕn List List
4. ∀orbit:ℕn List
     ((orbit ∈ orbits)
     ⇒ (0 < ||orbit||
        ∧ no_repeats(ℕn;orbit)
        ∧ (∀i:ℕ||orbit||. ((f orbit[i]) = if (i =z ||orbit|| - 1) then orbit[0] else orbit[i + 1] fi  ∈ ℕn))
        ∧ (∀x∈orbit.∀n@0:ℕ. (f^n@0 x ∈ orbit))))
5. ∀a:ℕn. (∃orbit∈orbits. (a ∈ orbit))
6. (∀o1,o2∈orbits.  l_disjoint(ℕn;o1;o2))
7. no_repeats(ℕn List;orbits)
8. ∀c1:ℕn List. ((c1 ∈ orbits) ⇒ (∀c2∈orbits.(c1 = c2 ∈ (ℕn List)) ∨ l_disjoint(ℕn;c1;c2)))
9. ∀c:ℕn List. ((c ∈ orbits) ⇒ (0 < ||c|| ∧ no_repeats(ℕn;c)))
⊢ f = reduce(λc,g. (cycle(c) o g);λx.x;orbits) ∈ (ℕn ⟶ ℕn)

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  .
    \mexists{}cycles:\mBbbN{}n  List  List
      (no\_repeats(\mBbbN{}n  List;cycles)
      \mwedge{}  (\mforall{}c1\mmember{}cycles.(\mforall{}c2\mmember{}cycles.(c1  =  c2)  \mvee{}  l\_disjoint(\mBbbN{}n;c1;c2)))
      \mwedge{}  (\mforall{}c\mmember{}cycles.0  <  ||c||  \mwedge{}  no\_repeats(\mBbbN{}n;c))
      \mwedge{}  (f  =  reduce(\mlambda{}c,g.  (cycle(c)  o  g);\mlambda{}x.x;cycles)))


By

---

Latex:
(Auto
  THEN  (InstLemma  `orbit-decomp`  [\mkleeneopen{}\mBbbN{}n\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  Try  ((BLemma  `finite-type-int\_seg`  THEN  Auto)))
              )
  THEN  Try  ((D  (-1)  THEN  Unhide  THEN  Auto))
  THEN  ParallelLast
  THEN  SplitAndHyps
  THEN  (RWO  "l\_all\_iff"  (-3)  THENA  Auto)
  THEN  RWO  "l\_all\_iff"  0
  THEN  Auto)

---

Home Index