---

Step * 1 2 1 of Lemma orbit-exists


1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)
3. finite-type(T)
4. f : T ⟶ T
5. a : T
6. k : ℕ
7. i : ℕk
8. (f^k a) = (f^i a) ∈ T
9. ∀i:ℕk. (¬(∃i@0:ℕi. ((f^i a) = (f^i@0 a) ∈ T)))
⊢ ∃L:T List. (no_repeats(T;L) ∧ (∀i:ℕ||L||. (L[i] = (f^i a) ∈ T)) ∧ (∀b:T. ((b ∈ L) ⇐⇒ ∃n:ℕ. (b = (f^n a) ∈ T))))
BY
{ ((InstConcl [⌜map(λn.(f^n a);upto(k))⌝]⋅
    THENM RWO "member_map" 0
    THENM skip{RWO "no_repeats_iff" 0}
    THENM skip{Try ((RWO "before-map" 0 THENM RWO "before-upto" 0))})
   THEN Reduce 0
   THEN Auto
   THEN ExRepD
   THEN Auto) }

1
1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)
3. finite-type(T)
4. f : T ⟶ T
5. a : T
6. k : ℕ
7. i : ℕk
8. (f^k a) = (f^i a) ∈ T
9. ∀i:ℕk. (¬(∃i@0:ℕi. ((f^i a) = (f^i@0 a) ∈ T)))
⊢ no_repeats(T;map(λn.(f^n a);upto(k)))

2
1. T : Type
2. ∀x,y:T.  Dec(x = y ∈ T)
3. finite-type(T)
4. f : T ⟶ T
5. a : T
6. k : ℕ
7. i : ℕk
8. (f^k a) = (f^i a) ∈ T
9. ∀i:ℕk. (¬(∃i@0:ℕi. ((f^i a) = (f^i@0 a) ∈ T)))
10. no_repeats(T;map(λn.(f^n a);upto(k)))
11. i1 : ℕ||map(λn.(f^n a);upto(k))||
⊢ map(λn.(f^n a);upto(k))[i1] = (f^i1 a) ∈ T

3
1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)
3. finite-type(T)
4. f : T ⟶ T
5. a : T
6. k : ℕ
7. i : ℕk
8. (f^k a) = (f^i a) ∈ T
9. ∀i:ℕk. (¬(∃i@0:ℕi. ((f^i a) = (f^i@0 a) ∈ T)))
10. no_repeats(T;map(λn.(f^n a);upto(k)))
11. ∀i:ℕ||map(λn.(f^n a);upto(k))||. (map(λn.(f^n a);upto(k))[i] = (f^i a) ∈ T)
12. b : T
13. n : ℕ
14. b = (f^n a) ∈ T
⊢ ∃y:ℕ. ((y ∈ upto(k)) ∧ (b = (f^y a) ∈ T))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  \mforall{}x,y:T.    Dec(x  =  y)
3.  finite-type(T)
4.  f  :  T  {}\mrightarrow{}  T
5.  a  :  T
6.  k  :  \mBbbN{}
7.  i  :  \mBbbN{}k
8.  (f\^{}k  a)  =  (f\^{}i  a)
9.  \mforall{}i:\mBbbN{}k.  (\mneg{}(\mexists{}i@0:\mBbbN{}i.  ((f\^{}i  a)  =  (f\^{}i@0  a))))
\mvdash{}  \mexists{}L:T  List
      (no\_repeats(T;L)  \mwedge{}  (\mforall{}i:\mBbbN{}||L||.  (L[i]  =  (f\^{}i  a)))  \mwedge{}  (\mforall{}b:T.  ((b  \mmember{}  L)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}.  (b  =  (f\^{}n  a)))))


By

---

Latex:
((InstConcl  [\mkleeneopen{}map(\mlambda{}n.(f\^{}n  a);upto(k))\mkleeneclose{}]\mcdot{}
    THENM  RWO  "member\_map"  0
    THENM  skip\{RWO  "no\_repeats\_iff"  0\}
    THENM  skip\{Try  ((RWO  "before-map"  0  THENM  RWO  "before-upto"  0))\})
  THEN  Reduce  0
  THEN  Auto
  THEN  ExRepD
  THEN  Auto)

---

Home Index