---

Step * 2 2 2 1 of Lemma orbit-decomp

.....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)))
10. (∀o1,o2∈orbits.  o1 ⊆ o2 ∨ o2 ⊆ o1 ∨ l_disjoint(T;o1;o2))
11. (∀o1∈orbits.(f last(o1)) = o1[0] ∈ T)
12. (∀o1∈orbits.∀i:ℕ||o1||. ((f o1[i]) = if (i =z ||o1|| - 1) then o1[0] else o1[i + 1] fi  ∈ T))
⊢ (∀o1∈orbits.(∀x∈o1.∀n:ℕ. (f^n x ∈ o1)))
BY
{ (All (RWW "l_all_iff") THENA 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: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))
11. (∀o1∈orbits.(f last(o1)) = o1[0] ∈ T)
12. ∀o1:T List. ((o1 ∈ orbits) ⇒ (∀i:ℕ||o1||. ((f o1[i]) = if (i =z ||o1|| - 1) then o1[0] else o1[i + 1] fi  ∈ T)))
13. ∀x:T List. ((x ∈ orbits) ∈ Type)
14. o1 : T List
15. (o1 ∈ orbits)
⊢ ¬↑null(o1)

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))
11. ∀o1:T List. ((o1 ∈ orbits) ⇒ ((f last(o1)) = o1[0] ∈ T))
12. ∀o1:T List. ((o1 ∈ orbits) ⇒ (∀i:ℕ||o1||. ((f o1[i]) = if (i =z ||o1|| - 1) then o1[0] else o1[i + 1] fi  ∈ T)))
⊢ ∀o1:T List. ((o1 ∈ orbits) ⇒ (∀x:T. ((x ∈ o1) ⇒ (∀n:ℕ. (f^n x ∈ o1)))))

---

Latex:

---

Latex:
.....assertion..... 
1.  [T]  :  Type
2.  \mforall{}x,y:T.    Dec(x  =  y)
3.  finite-type(T)
4.  f  :  T  {}\mrightarrow{}  T
5.  Inj(T;T;f)
6.  orbits  :  T  List  List
7.  \mforall{}orbit:T  List
          ((orbit  \mmember{}  orbits)
          {}\mRightarrow{}  (0  <  ||orbit||
                \mwedge{}  no\_repeats(T;orbit)
                \mwedge{}  (\mforall{}i:\mBbbN{}||orbit||.  (orbit[i]  =  (f\^{}i  orbit[0])))
                \mwedge{}  (\mforall{}b:T.  ((b  \mmember{}  orbit)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}.  (b  =  (f\^{}n  orbit[0]))))))
8.  \mforall{}a:T.  (\mexists{}orbit\mmember{}orbits.  (a  \mmember{}  orbit))
9.  \mforall{}o1:T  List.  ((o1  \mmember{}  orbits)  {}\mRightarrow{}  (\mforall{}o2:T  List.  ((o2  \mmember{}  orbits)  {}\mRightarrow{}  (o1[0]  \mmember{}  o2)  {}\mRightarrow{}  o1  \msubseteq{}  o2)))
10.  (\mforall{}o1,o2\mmember{}orbits.    o1  \msubseteq{}  o2  \mvee{}  o2  \msubseteq{}  o1  \mvee{}  l\_disjoint(T;o1;o2))
11.  (\mforall{}o1\mmember{}orbits.(f  last(o1))  =  o1[0])
12.  (\mforall{}o1\mmember{}orbits.\mforall{}i:\mBbbN{}||o1||.  ((f  o1[i])  =  if  (i  =\msubz{}  ||o1||  -  1)  then  o1[0]  else  o1[i  +  1]  fi  ))
\mvdash{}  (\mforall{}o1\mmember{}orbits.(\mforall{}x\mmember{}o1.\mforall{}n:\mBbbN{}.  (f\^{}n  x  \mmember{}  o1)))


By

---

Latex:
(All  (RWW  "l\_all\_iff")  THENA  Auto)

---

Home Index