---

Step * of Lemma connection-bound

∀[T:Type]
  ((∀x,y:T.  Dec(x = y ∈ T))
  ⇒ (∀k:ℕ. (|T| ≤ k ⇒ (∀f:T ⟶ T. ∀a,b:T.  (∃n:ℕ. (b = (f^n a) ∈ T) ⇐⇒ ∃n:ℕk. (b = (f^n a) ∈ T))))))
BY
{ (InstLemma `orbit-exists` []⋅
   THEN RepeatFor 2 ((ParallelLast' THENA Auto))
   THEN Auto
   THEN Try (Complete (ParallelLast))) }

1
1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)@i
3. finite-type(T)
⇒ (∀f:T ⟶ T. ∀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)))))
4. k : ℕ@i
5. |T| ≤ k@i
6. f : T ⟶ T@i
7. a : T@i
8. b : T@i
9. ∃n:ℕ. (b = (f^n a) ∈ T)@i
⊢ ∃n:ℕk. (b = (f^n a) ∈ T)

---

Latex:

---

Latex:
\mforall{}[T:Type]
    ((\mforall{}x,y:T.    Dec(x  =  y))
    {}\mRightarrow{}  (\mforall{}k:\mBbbN{}.  (|T|  \mleq{}  k  {}\mRightarrow{}  (\mforall{}f:T  {}\mrightarrow{}  T.  \mforall{}a,b:T.    (\mexists{}n:\mBbbN{}.  (b  =  (f\^{}n  a))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}k.  (b  =  (f\^{}n  a)))))))


By

---

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

---

Home Index