---

Step * of Lemma decidable__connection

∀[T:Type]. ((∀x,y:T.  Dec(x = y ∈ T)) ⇒ finite-type(T) ⇒ (∀f:T ⟶ T. ∀a,b:T.  Dec(∃n:ℕ. (b = (f^n a) ∈ T))))
BY
{ (InstLemma `orbit-exists` []⋅ THEN RepeatFor 5 ((ParallelLast' THENA Auto)) THEN (ExRepD THENA Auto)) }

1
1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)@i
3. finite-type(T)@i
4. f : T ⟶ T@i
5. a : T@i
6. L : T List
7. no_repeats(T;L)
8. ∀i:ℕ||L||. (L[i] = (f^i a) ∈ T)
9. ∀b:T. ((b ∈ L) ⇐⇒ ∃n:ℕ. (b = (f^n a) ∈ T))
10. b : T@i
⊢ Dec(∃n:ℕ. (b = (f^n a) ∈ T))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    ((\mforall{}x,y:T.    Dec(x  =  y))  {}\mRightarrow{}  finite-type(T)  {}\mRightarrow{}  (\mforall{}f:T  {}\mrightarrow{}  T.  \mforall{}a,b:T.    Dec(\mexists{}n:\mBbbN{}.  (b  =  (f\^{}n  a)))))


By

---

Latex:
(InstLemma  `orbit-exists`  []\mcdot{}
  THEN  RepeatFor  5  ((ParallelLast'  THENA  Auto))
  THEN  (ExRepD  THENA  Auto))

---

Home Index