---

Step * 1 1 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. i : ℤ
16. 0 ≤ i
17. i < ||L||
18. b = L[i] ∈ T
19. L[i] = (f^i a) ∈ T
⊢ i < k
BY
{ (Assert ⌜||L|| ≤ k⌝⋅ THEN Auto') }

1
.....assertion..... 
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. 0 ≤ i
17. i < ||L||
18. b = L[i] ∈ T
19. L[i] = (f^i a) ∈ T
⊢ ||L|| ≤ k

---

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.  i  :  \mBbbZ{}
16.  0  \mleq{}  i
17.  i  <  ||L||
18.  b  =  L[i]
19.  L[i]  =  (f\^{}i  a)
\mvdash{}  i  <  k


By

---

Latex:
(Assert  \mkleeneopen{}||L||  \mleq{}  k\mkleeneclose{}\mcdot{}  THEN  Auto')

---

Home Index