Step
*
1
2
1
1
1
1
1
2
of Lemma
KleeneSearch_wf
1. T : {T:Type| (T ⊆r ℕ) ∧ (↓T)}
2. F : (ℕ ⟶ T) ⟶ ℕ
3. f : ℕ ⟶ T
4. M : n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ ⋃ (ℕ × ℕ))
5. n : ℕ
6. (M n f) = (F f) ∈ ℕ
7. ∀n:ℕ. (M n f) = (F f) ∈ ℕ supposing M n f is an integer
8. ∀n,m:ℕ. ((n ≤ m) ⇒ M n f is an integer ⇒ M m f is an integer)
9. d : ℕ
10. ∀d:ℕd. ∀start:ℕ.
((n ≤ (start + d))
⇒ (KleeneSearch(M;f;start) ∈ {m:ℕ| (start ≤ m) ∧ (∀g:ℕ ⟶ T. ((g = f ∈ (ℕm ⟶ T)) ⇒ ((F g) = (F f) ∈ ℤ)))} ))
11. start : ℕ
12. n ≤ (start + d)
13. a1 : ℕ
14. (M start f) = a1 ∈ (ℕ ⋃ (ℕ × ℕ))
15. (M start f) = (F f) ∈ ℕ
16. start ≤ start
17. g : ℕ ⟶ T
18. g = f ∈ (ℕstart ⟶ T)
19. (F f) = (M start g) ∈ (ℕ ⋃ (ℕ × ℕ))
20. (F f) = (M start g) ∈ (ℕ ⋃ (ℕ × ℕ))
21. F f is an integer = M start g is an integer ∈ ℙ
22. n1 : ℕ
23. (M n1 g) = (F g) ∈ ℕ
24. ∀n:ℕ. (M n g) = (F g) ∈ ℕ supposing M n g is an integer
25. ∀n,m:ℕ. ((n ≤ m) ⇒ M n g is an integer ⇒ M m g is an integer)
26. (M start g) = (F g) ∈ ℕ
⊢ (F g) = (F f) ∈ ℤ
BY
{ (HypSubst' (-1) (-8) THEN (Assert F f ~ F g BY MoveToConcl (-8))) }
1
.....aux.....
1. T : {T:Type| (T ⊆r ℕ) ∧ (↓T)}
2. F : (ℕ ⟶ T) ⟶ ℕ
3. f : ℕ ⟶ T
4. M : n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ ⋃ (ℕ × ℕ))
5. n : ℕ
6. (M n f) = (F f) ∈ ℕ
7. ∀n:ℕ. (M n f) = (F f) ∈ ℕ supposing M n f is an integer
8. ∀n,m:ℕ. ((n ≤ m) ⇒ M n f is an integer ⇒ M m f is an integer)
9. d : ℕ
10. ∀d:ℕd. ∀start:ℕ.
((n ≤ (start + d))
⇒ (KleeneSearch(M;f;start) ∈ {m:ℕ| (start ≤ m) ∧ (∀g:ℕ ⟶ T. ((g = f ∈ (ℕm ⟶ T)) ⇒ ((F g) = (F f) ∈ ℤ)))} ))
11. start : ℕ
12. n ≤ (start + d)
13. a1 : ℕ
14. (M start f) = a1 ∈ (ℕ ⋃ (ℕ × ℕ))
15. (M start f) = (F f) ∈ ℕ
16. start ≤ start
17. g : ℕ ⟶ T
18. g = f ∈ (ℕstart ⟶ T)
19. (F f) = (M start g) ∈ (ℕ ⋃ (ℕ × ℕ))
20. F f is an integer = M start g is an integer ∈ ℙ
21. n1 : ℕ
22. (M n1 g) = (F g) ∈ ℕ
23. ∀n:ℕ. (M n g) = (F g) ∈ ℕ supposing M n g is an integer
24. ∀n,m:ℕ. ((n ≤ m) ⇒ M n g is an integer ⇒ M m g is an integer)
25. (M start g) = (F g) ∈ ℕ
⊢ ((F f) = (F g) ∈ (ℕ ⋃ (ℕ × ℕ))) ⇒ (F f ~ F g)
2
1. T : {T:Type| (T ⊆r ℕ) ∧ (↓T)}
2. F : (ℕ ⟶ T) ⟶ ℕ
3. f : ℕ ⟶ T
4. M : n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ ⋃ (ℕ × ℕ))
5. n : ℕ
6. (M n f) = (F f) ∈ ℕ
7. ∀n:ℕ. (M n f) = (F f) ∈ ℕ supposing M n f is an integer
8. ∀n,m:ℕ. ((n ≤ m) ⇒ M n f is an integer ⇒ M m f is an integer)
9. d : ℕ
10. ∀d:ℕd. ∀start:ℕ.
((n ≤ (start + d))
⇒ (KleeneSearch(M;f;start) ∈ {m:ℕ| (start ≤ m) ∧ (∀g:ℕ ⟶ T. ((g = f ∈ (ℕm ⟶ T)) ⇒ ((F g) = (F f) ∈ ℤ)))} ))
11. start : ℕ
12. n ≤ (start + d)
13. a1 : ℕ
14. (M start f) = a1 ∈ (ℕ ⋃ (ℕ × ℕ))
15. (M start f) = (F f) ∈ ℕ
16. start ≤ start
17. g : ℕ ⟶ T
18. g = f ∈ (ℕstart ⟶ T)
19. (F f) = (F g) ∈ (ℕ ⋃ (ℕ × ℕ))
20. (F f) = (M start g) ∈ (ℕ ⋃ (ℕ × ℕ))
21. F f is an integer = M start g is an integer ∈ ℙ
22. n1 : ℕ
23. (M n1 g) = (F g) ∈ ℕ
24. ∀n:ℕ. (M n g) = (F g) ∈ ℕ supposing M n g is an integer
25. ∀n,m:ℕ. ((n ≤ m) ⇒ M n g is an integer ⇒ M m g is an integer)
26. (M start g) = (F g) ∈ ℕ
27. F f ~ F g
⊢ (F g) = (F f) ∈ ℤ
Latex:
Latex:
1. T : \{T:Type| (T \msubseteq{}r \mBbbN{}) \mwedge{} (\mdownarrow{}T)\}
2. F : (\mBbbN{} {}\mrightarrow{} T) {}\mrightarrow{} \mBbbN{}
3. f : \mBbbN{} {}\mrightarrow{} T
4. M : n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} T) {}\mrightarrow{} (\mBbbN{} \mcup{} (\mBbbN{} \mtimes{} \mBbbN{}))
5. n : \mBbbN{}
6. (M n f) = (F f)
7. \mforall{}n:\mBbbN{}. (M n f) = (F f) supposing M n f is an integer
8. \mforall{}n,m:\mBbbN{}. ((n \mleq{} m) {}\mRightarrow{} M n f is an integer {}\mRightarrow{} M m f is an integer)
9. d : \mBbbN{}
10. \mforall{}d:\mBbbN{}d. \mforall{}start:\mBbbN{}.
((n \mleq{} (start + d))
{}\mRightarrow{} (KleeneSearch(M;f;start) \mmember{} \{m:\mBbbN{}| (start \mleq{} m) \mwedge{} (\mforall{}g:\mBbbN{} {}\mrightarrow{} T. ((g = f) {}\mRightarrow{} ((F g) = (F f))))\} )\000C)
11. start : \mBbbN{}
12. n \mleq{} (start + d)
13. a1 : \mBbbN{}
14. (M start f) = a1
15. (M start f) = (F f)
16. start \mleq{} start
17. g : \mBbbN{} {}\mrightarrow{} T
18. g = f
19. (F f) = (M start g)
20. (F f) = (M start g)
21. F f is an integer = M start g is an integer
22. n1 : \mBbbN{}
23. (M n1 g) = (F g)
24. \mforall{}n:\mBbbN{}. (M n g) = (F g) supposing M n g is an integer
25. \mforall{}n,m:\mBbbN{}. ((n \mleq{} m) {}\mRightarrow{} M n g is an integer {}\mRightarrow{} M m g is an integer)
26. (M start g) = (F g)
\mvdash{} (F g) = (F f)
By
Latex:
(HypSubst' (-1) (-8) THEN (Assert F f \msim{} F g BY MoveToConcl (-8)))
Home
Index