---

Step * 1 1 2 2 of Lemma orbit-decomp

.....upcase..... 
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. i : ℕ||orbits||
11. j : ℕi
12. ¬(orbits[j][0] ∈ orbits[i])
13. ¬(orbits[i][0] ∈ orbits[j])
14. x : T
15. (x ∈ orbits[j])
16. (x ∈ orbits[i])
17. n : ℤ
18. 0 < n
19. ∀m:ℕ. (¬((f^n - 1 orbits[i][0]) = (f^m orbits[j][0]) ∈ T))
20. m : ℤ
21. 0 < m
22. ¬((f^n orbits[i][0]) = (f^m - 1 orbits[j][0]) ∈ T)
⊢ ¬((f^n orbits[i][0]) = (f^m orbits[j][0]) ∈ T)
BY
{ ((RWO "fun_exp_unroll" 0 THENA Auto)
   THEN RepeatFor 2 ((SplitOnConclITE THEN Auto))
   THEN Reduce 0
   THEN (D 0 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. i : ℕ||orbits||
11. j : ℕi
12. ¬(orbits[j][0] ∈ orbits[i])
13. ¬(orbits[i][0] ∈ orbits[j])
14. x : T
15. (x ∈ orbits[j])
16. (x ∈ orbits[i])
17. n : ℤ
18. 0 < n
19. ∀m:ℕ. (¬((f^n - 1 orbits[i][0]) = (f^m orbits[j][0]) ∈ T))
20. m : ℤ
21. 0 < m
22. ¬((f^n orbits[i][0]) = (f^m - 1 orbits[j][0]) ∈ T)
23. ¬(n = 0 ∈ ℤ)
24. ¬(m = 0 ∈ ℤ)
25. (f (f^n - 1 orbits[i][0])) = (f (f^m - 1 orbits[j][0])) ∈ T
⊢ False

---

Latex:

---

Latex:
.....upcase..... 
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.  i  :  \mBbbN{}||orbits||
11.  j  :  \mBbbN{}i
12.  \mneg{}(orbits[j][0]  \mmember{}  orbits[i])
13.  \mneg{}(orbits[i][0]  \mmember{}  orbits[j])
14.  x  :  T
15.  (x  \mmember{}  orbits[j])
16.  (x  \mmember{}  orbits[i])
17.  n  :  \mBbbZ{}
18.  0  <  n
19.  \mforall{}m:\mBbbN{}.  (\mneg{}((f\^{}n  -  1  orbits[i][0])  =  (f\^{}m  orbits[j][0])))
20.  m  :  \mBbbZ{}
21.  0  <  m
22.  \mneg{}((f\^{}n  orbits[i][0])  =  (f\^{}m  -  1  orbits[j][0]))
\mvdash{}  \mneg{}((f\^{}n  orbits[i][0])  =  (f\^{}m  orbits[j][0]))


By

---

Latex:
((RWO  "fun\_exp\_unroll"  0  THENA  Auto)
  THEN  RepeatFor  2  ((SplitOnConclITE  THEN  Auto))
  THEN  Reduce  0
  THEN  (D  0  THENA  Auto))

---

Home Index