---

Step * of Lemma orbit-decomp2

∀[T:Type]
  ((∀x,y:T.  Dec(x = y ∈ T))
  ⇒ finite-type(T)
  ⇒ (∀f:T ⟶ T
        ∃orbits:T List List
         ((∀o∈orbits.orbit(T;f;o))
         ∧ (∀a:T. (∃orbit∈orbits. (a ∈ orbit)))
         ∧ (∀o1,o2∈orbits.  l_disjoint(T;o1;o2))
         ∧ no_repeats(T List;orbits)) 
        supposing Inj(T;T;f)))
BY
{ (InstLemma `orbit-decomp` [] THEN RepeatFor 6 ((ParallelLast' THENA Auto)) THEN Auto) }

1
1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)
3. finite-type(T)
4. f : T ⟶ T
5. Inj(T;T;f)
6. orbits : T List List
7. (∀orbit∈orbits.0 < ||orbit||
          ∧ no_repeats(T;orbit)
          ∧ (∀i:ℕ||orbit||. ((f orbit[i]) = if (i =z ||orbit|| - 1) then orbit[0] else orbit[i + 1] fi  ∈ T))
          ∧ (∀x∈orbit.∀n:ℕ. (f^n x ∈ orbit)))
8. ∀a:T. (∃orbit∈orbits. (a ∈ orbit))
9. (∀o1,o2∈orbits.  l_disjoint(T;o1;o2))
⊢ (∀o∈orbits.orbit(T;f;o))

2
1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)
3. finite-type(T)
4. f : T ⟶ T
5. Inj(T;T;f)
6. orbits : T List List
7. (∀orbit∈orbits.0 < ||orbit||
          ∧ no_repeats(T;orbit)
          ∧ (∀i:ℕ||orbit||. ((f orbit[i]) = if (i =z ||orbit|| - 1) then orbit[0] else orbit[i + 1] fi  ∈ T))
          ∧ (∀x∈orbit.∀n:ℕ. (f^n x ∈ orbit)))
8. ∀a:T. (∃orbit∈orbits. (a ∈ orbit))
9. (∀o1,o2∈orbits.  l_disjoint(T;o1;o2))
10. (∀o∈orbits.orbit(T;f;o))
11. ∀a:T. (∃orbit∈orbits. (a ∈ orbit))
12. (∀o1,o2∈orbits.  l_disjoint(T;o1;o2))
⊢ no_repeats(T List;orbits)

---

Latex:

---

Latex:
\mforall{}[T:Type]
    ((\mforall{}x,y:T.    Dec(x  =  y))
    {}\mRightarrow{}  finite-type(T)
    {}\mRightarrow{}  (\mforall{}f:T  {}\mrightarrow{}  T
                \mexists{}orbits:T  List  List
                  ((\mforall{}o\mmember{}orbits.orbit(T;f;o))
                  \mwedge{}  (\mforall{}a:T.  (\mexists{}orbit\mmember{}orbits.  (a  \mmember{}  orbit)))
                  \mwedge{}  (\mforall{}o1,o2\mmember{}orbits.    l\_disjoint(T;o1;o2))
                  \mwedge{}  no\_repeats(T  List;orbits)) 
                supposing  Inj(T;T;f)))


By

---

Latex:
(InstLemma  `orbit-decomp`  []  THEN  RepeatFor  6  ((ParallelLast'  THENA  Auto))  THEN  Auto)

---

Home Index