Step
*
2
2
of Lemma
KleeneSearch_wf
1. T : {T:Type| (T ⊆r ℕ) ∧ (↓T)}
2. F : (ℕ ⟶ T) ⟶ ℕ
3. f : ℕ ⟶ T
4. M : n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ ⋃ (ℕ × ℕ))
5. ∀f:ℕ ⟶ T
((∃n:ℕ. ((M n f) = (F f) ∈ ℕ))
∧ (∀n:ℕ. (M n f) = (F f) ∈ ℕ supposing M n f is an integer)
∧ (∀n,m:ℕ. ((n ≤ m) ⇒ M n f is an integer ⇒ M m f is an integer)))
6. n : ℕ
7. (M n f) = (F f) ∈ ℕ
8. ∀n:ℕ. (M n f) = (F f) ∈ ℕ supposing M n f is an integer
9. ∀n,m:ℕ. ((n ≤ m) ⇒ M n f is an integer ⇒ M m f is an integer)
10. d : ℕ
11. ∀d:ℕd. ∀start:ℕ.
((n ≤ (start + d))
⇒ (KleeneSearch(M;f;start) ∈ {m:ℕ| (start ≤ m) ∧ (∀g:ℕ ⟶ T. ((g = f ∈ (ℕm ⟶ T)) ⇒ ((F g) = (F f) ∈ ℤ)))} ))
12. start : ℕ
13. n ≤ (start + d)
14. a1 : ℕ × ℕ
15. (M start f) = ((λp.(snd(p))) <inr Ax , a1>) ∈ (ℕ ⋃ (ℕ × ℕ))
16. 0 < d
⊢ if a1 is an integer then start
else KleeneSearch(M;f;imax(fst(a1);start + 1)) ∈ {m:ℕ|
(start ≤ m)
∧ (∀g:ℕ ⟶ T. ((g = f ∈ (ℕm ⟶ T)) ⇒ ((F g) = (F f) ∈ ℤ)))}
BY
{ (Thin (-2)
THEN D -2
THEN Reduce 0
THEN (InstHyp [⌜d - 1⌝;⌜imax(a2;start + 1)⌝] (-6)⋅ THENA (Auto THEN RWO "imax_unfold" 0 THEN Auto))) }
1
1. T : {T:Type| (T ⊆r ℕ) ∧ (↓T)}
2. F : (ℕ ⟶ T) ⟶ ℕ
3. f : ℕ ⟶ T
4. M : n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ ⋃ (ℕ × ℕ))
5. ∀f:ℕ ⟶ T
((∃n:ℕ. ((M n f) = (F f) ∈ ℕ))
∧ (∀n:ℕ. (M n f) = (F f) ∈ ℕ supposing M n f is an integer)
∧ (∀n,m:ℕ. ((n ≤ m) ⇒ M n f is an integer ⇒ M m f is an integer)))
6. n : ℕ
7. (M n f) = (F f) ∈ ℕ
8. ∀n:ℕ. (M n f) = (F f) ∈ ℕ supposing M n f is an integer
9. ∀n,m:ℕ. ((n ≤ m) ⇒ M n f is an integer ⇒ M m f is an integer)
10. d : ℕ
11. ∀d:ℕd. ∀start:ℕ.
((n ≤ (start + d))
⇒ (KleeneSearch(M;f;start) ∈ {m:ℕ| (start ≤ m) ∧ (∀g:ℕ ⟶ T. ((g = f ∈ (ℕm ⟶ T)) ⇒ ((F g) = (F f) ∈ ℤ)))} ))
12. start : ℕ
13. n ≤ (start + d)
14. a2 : ℕ
15. a3 : ℕ
16. 0 < d
17. KleeneSearch(M;f;imax(a2;start + 1)) ∈ {m:ℕ|
(imax(a2;start + 1) ≤ m)
∧ (∀g:ℕ ⟶ T. ((g = f ∈ (ℕm ⟶ T)) ⇒ ((F g) = (F f) ∈ ℤ)))}
⊢ KleeneSearch(M;f;imax(a2;start + 1)) ∈ {m:ℕ| (start ≤ m) ∧ (∀g:ℕ ⟶ T. ((g = f ∈ (ℕm ⟶ T)) ⇒ ((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. \mforall{}f:\mBbbN{} {}\mrightarrow{} T
((\mexists{}n:\mBbbN{}. ((M n f) = (F f)))
\mwedge{} (\mforall{}n:\mBbbN{}. (M n f) = (F f) supposing M n f is an integer)
\mwedge{} (\mforall{}n,m:\mBbbN{}. ((n \mleq{} m) {}\mRightarrow{} M n f is an integer {}\mRightarrow{} M m f is an integer)))
6. n : \mBbbN{}
7. (M n f) = (F f)
8. \mforall{}n:\mBbbN{}. (M n f) = (F f) supposing M n f is an integer
9. \mforall{}n,m:\mBbbN{}. ((n \mleq{} m) {}\mRightarrow{} M n f is an integer {}\mRightarrow{} M m f is an integer)
10. d : \mBbbN{}
11. \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)
12. start : \mBbbN{}
13. n \mleq{} (start + d)
14. a1 : \mBbbN{} \mtimes{} \mBbbN{}
15. (M start f) = ((\mlambda{}p.(snd(p))) <inr Ax , a1>)
16. 0 < d
\mvdash{} if a1 is an integer then start
else KleeneSearch(M;f;imax(fst(a1);start + 1)) \mmember{} \{m:\mBbbN{}|
(start \mleq{} m)
\mwedge{} (\mforall{}g:\mBbbN{} {}\mrightarrow{} T. ((g = f) {}\mRightarrow{} ((F g) = (F f))))\}
By
Latex:
(Thin (-2)
THEN D -2
THEN Reduce 0
THEN (InstHyp [\mkleeneopen{}d - 1\mkleeneclose{};\mkleeneopen{}imax(a2;start + 1)\mkleeneclose{}] (-6)\mcdot{}
THENA (Auto THEN RWO "imax\_unfold" 0 THEN Auto)
))
Home
Index