---

Step * of Lemma orbit-decomp

∀[T:Type]
  ((∀x,y:T.  Dec(x = y ∈ T))
  ⇒ finite-type(T)
  ⇒ (∀f:T ⟶ T
        ∃orbits:T List List
         ((∀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)))
         ∧ (∀a:T. (∃orbit∈orbits. (a ∈ orbit)))
         ∧ (∀o1,o2∈orbits.  l_disjoint(T;o1;o2))) 
        supposing Inj(T;T;f)))
BY
{ (Auto
   THEN (InstLemma `orbit-cover` [⌜T⌝;⌜f⌝]⋅ THENA Auto)
   THEN (ExRepD
         THEN (RWO "l_all_iff" (-3) THENA Auto)
         THEN (RWW "l_all_iff" (-1) THENA (Auto THEN D (-2) THEN Unhide THEN Auto)))
   THEN Assert ⌜(∀o1,o2∈orbits.  o1 ⊆ o2 ∨ o2 ⊆ o1 ∨ l_disjoint(T;o1;o2))⌝⋅) }

1
.....assertion..... 
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:T List
     ((orbit ∈ orbits)
     ⇒ (0 < ||orbit||
        ∧ no_repeats(T;orbit)
        ∧ (∀i:ℕ||orbit||. (orbit[i] = (f^i orbit[0]) ∈ T))
        ∧ (∀b:T. ((b ∈ orbit) ⇐⇒ ∃n:ℕ. (b = (f^n orbit[0]) ∈ T)))))
8. ∀a:T. (∃orbit∈orbits. (a ∈ orbit))
9. ∀o1:T List. ((o1 ∈ orbits) ⇒ (∀o2:T List. ((o2 ∈ orbits) ⇒ (o1[0] ∈ o2) ⇒ o1 ⊆ o2)))
⊢ (∀o1,o2∈orbits.  o1 ⊆ o2 ∨ o2 ⊆ o1 ∨ l_disjoint(T;o1;o2))

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:T List
     ((orbit ∈ orbits)
     ⇒ (0 < ||orbit||
        ∧ no_repeats(T;orbit)
        ∧ (∀i:ℕ||orbit||. (orbit[i] = (f^i orbit[0]) ∈ T))
        ∧ (∀b:T. ((b ∈ orbit) ⇐⇒ ∃n:ℕ. (b = (f^n orbit[0]) ∈ T)))))
8. ∀a:T. (∃orbit∈orbits. (a ∈ orbit))
9. ∀o1:T List. ((o1 ∈ orbits) ⇒ (∀o2:T List. ((o2 ∈ orbits) ⇒ (o1[0] ∈ o2) ⇒ o1 ⊆ o2)))
10. (∀o1,o2∈orbits.  o1 ⊆ o2 ∨ o2 ⊆ o1 ∨ l_disjoint(T;o1;o2))
⊢ ∃orbits:T List List
   ((∀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)))
   ∧ (∀a:T. (∃orbit∈orbits. (a ∈ orbit)))
   ∧ (∀o1,o2∈orbits.  l_disjoint(T;o1;o2)))

---

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{}orbit\mmember{}orbits.0  <  ||orbit||
                                  \mwedge{}  no\_repeats(T;orbit)
                                  \mwedge{}  (\mforall{}i:\mBbbN{}||orbit||
                                            ((f  orbit[i])  =  if  (i  =\msubz{}  ||orbit||  -  1)  then  orbit[0]  else  orbit[i  +  1]  fi  ))
                                  \mwedge{}  (\mforall{}x\mmember{}orbit.\mforall{}n:\mBbbN{}.  (f\^{}n  x  \mmember{}  orbit)))
                  \mwedge{}  (\mforall{}a:T.  (\mexists{}orbit\mmember{}orbits.  (a  \mmember{}  orbit)))
                  \mwedge{}  (\mforall{}o1,o2\mmember{}orbits.    l\_disjoint(T;o1;o2))) 
                supposing  Inj(T;T;f)))


By

---

Latex:
(Auto
  THEN  (InstLemma  `orbit-cover`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (ExRepD
              THEN  (RWO  "l\_all\_iff"  (-3)  THENA  Auto)
              THEN  (RWW  "l\_all\_iff"  (-1)  THENA  (Auto  THEN  D  (-2)  THEN  Unhide  THEN  Auto)))
  THEN  Assert  \mkleeneopen{}(\mforall{}o1,o2\mmember{}orbits.    o1  \msubseteq{}  o2  \mvee{}  o2  \msubseteq{}  o1  \mvee{}  l\_disjoint(T;o1;o2))\mkleeneclose{}\mcdot{})

---

Home Index