---

Step * 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>) ∈ (ℕ ⋃ (ℕ × ℕ))
⊢ 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
{ (Assert 0 < d BY
         (SupposeNot
          THEN (Assert n ≤ start BY
                      Auto)
          THEN FHyp 9 [-1]
          THEN Auto
          THEN Try ((HypSubst' 7 0 THEN GenConclAtAddr [1] THEN Reduce 0 THEN Auto)))) }

1
.....aux..... 
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
17. n ≤ start
18. M start f is an integer
19. v : ℤ
20. 0 = v ∈ ℤ
⊢ v < d

2
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) ∈ ℤ)))} 

---

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>)
\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:
(Assert  0  <  d  BY
              (SupposeNot
                THEN  (Assert  n  \mleq{}  start  BY
                                        Auto)
                THEN  FHyp  9  [-1]
                THEN  Auto
                THEN  Try  ((HypSubst'  7  0  THEN  GenConclAtAddr  [1]  THEN  Reduce  0  THEN  Auto))))

---

Home Index