---

Step * 1 1 of Lemma connection-bound


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)
BY
{ (RepeatFor 2 ((D (-1))) THEN ((InstHyp [⌜i⌝] (-5))⋅ THENA 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. i : ℕ
16. i < ||L||
17. b = L[i] ∈ T
18. L[i] = (f^i a) ∈ T
⊢ ∃n:ℕk. (b = (f^n a) ∈ T)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  \mforall{}x,y:T.    Dec(x  =  y)@i
3.  k  :  \mBbbN{}@i
4.  |T|  \mleq{}  k@i
5.  f  :  T  {}\mrightarrow{}  T@i
6.  a  :  T@i
7.  b  :  T@i
8.  n  :  \mBbbN{}@i
9.  b  =  (f\^{}n  a)@i
10.  \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)))))
11.  L  :  T  List
12.  no\_repeats(T;L)
13.  \mforall{}i:\mBbbN{}||L||.  (L[i]  =  (f\^{}i  a))
14.  \mforall{}b:T.  ((b  \mmember{}  L)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}.  (b  =  (f\^{}n  a)))
15.  (b  \mmember{}  L)
\mvdash{}  \mexists{}n:\mBbbN{}k.  (b  =  (f\^{}n  a))


By

---

Latex:
(RepeatFor  2  ((D  (-1)))  THEN  ((InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  (-5))\mcdot{}  THENA  Auto))

---

Home Index