---

Step * 1 of Lemma connection-bound


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)
BY
{ ((D 3 THENA (UnfoldTopAb 0 THEN Fold `cardinality-le` 0 THEN Auto))
   THEN ((InstHyp [⌜f⌝; ⌜a⌝] (-1))⋅ THENA Auto)
   THEN ExRepD
   THEN (Assert (b ∈ L) BY
               (BHyp -1  THEN Auto))) }

1
1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)@i
3. k : ℕ@i
4. |T| ≤ k@i
5. f : T ⟶ T@i
6. a : T@i
7. b : T@i
8. n : ℕ@i
9. b = (f^n a) ∈ T@i
10. ∀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))))
11. L : T List
12. no_repeats(T;L)
13. ∀i:ℕ||L||. (L[i] = (f^i a) ∈ T)
14. ∀b:T. ((b ∈ L) ⇐⇒ ∃n:ℕ. (b = (f^n a) ∈ T))
15. (b ∈ L)
⊢ ∃n:ℕk. (b = (f^n a) ∈ T)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  \mforall{}x,y:T.    Dec(x  =  y)@i
3.  finite-type(T)
{}\mRightarrow{}  (\mforall{}f:T  {}\mrightarrow{}  T.  \mforall{}a:T.
            \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))))))
4.  k  :  \mBbbN{}@i
5.  |T|  \mleq{}  k@i
6.  f  :  T  {}\mrightarrow{}  T@i
7.  a  :  T@i
8.  b  :  T@i
9.  \mexists{}n:\mBbbN{}.  (b  =  (f\^{}n  a))@i
\mvdash{}  \mexists{}n:\mBbbN{}k.  (b  =  (f\^{}n  a))


By

---

Latex:
((D  3  THENA  (UnfoldTopAb  0  THEN  Fold  `cardinality-le`  0  THEN  Auto))
  THEN  ((InstHyp  [\mkleeneopen{}f\mkleeneclose{};  \mkleeneopen{}a\mkleeneclose{}]  (-1))\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (Assert  (b  \mmember{}  L)  BY
                          (BHyp  -1    THEN  Auto)))

---

Home Index