---

Step * of Lemma KleeneSearch_wf

∀[T:{T:Type| (T ⊆r ℕ) ∧ (↓T)} ]. ∀[F:(ℕ ⟶ T) ⟶ ℕ]. ∀[M:⇃(basic-strong-continuity(T;F))]. ∀[f:ℕ ⟶ T]. ∀[start:ℕ].
  (KleeneSearch(M;f;start) ∈ ⇃({m:ℕ| (start ≤ m) ∧ (∀g:ℕ ⟶ T. ((g = f ∈ (ℕm ⟶ T)) ⇒ ((F g) = (F f) ∈ ℤ)))} ))
BY
{ (Auto
   THEN (Assert ⌜∀M:basic-strong-continuity(T;F)
                   (KleeneSearch(M;f;start) ∈ {m:ℕ| 
                                               (start ≤ m) ∧ (∀g:ℕ ⟶ T. ((g = f ∈ (ℕm ⟶ T)) ⇒ ((F g) = (F f) ∈ ℤ)))} \000C)⌝⋅
   THENM (D 3 THEN EqTypeCD THEN Auto)
   )
   THEN Thin (-3)
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN DupHyp (-1)
   THEN (D -1 With ⌜f⌝  THENA Auto)
   THEN ExRepD
   THEN MoveToConcl 4
   THEN (Assert ⌜∀d,start:ℕ.
                   ((n ≤ (start + d))
                   ⇒ (KleeneSearch(M;f;start) ∈ {m:ℕ| 
                                                  (start ≤ m)
                                                  ∧ (∀g:ℕ ⟶ T. ((g = f ∈ (ℕm ⟶ T)) ⇒ ((F g) = (F f) ∈ ℤ)))} ))⌝⋅
   THENM ((D -1 With ⌜n⌝  THENA Auto) THEN ParallelLast THEN BHyp -1 THEN Auto)
   )
   THEN CompleteInductionOnNat
   THEN Intros
   THEN Unfold `KleeneSearch` 0
   THEN GenConclAtAddr [2;1]
   THEN (CallByValueReduce 0 THENA Auto)
   THEN D -2
   THEN Reduce 0
   THEN Try ((Fold `member` 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. a1 : ℕ
15. (M start f) = ((λp.(snd(p))) <inl Ax, a1>) ∈ (ℕ ⋃ (ℕ × ℕ))
⊢ start ∈ {m:ℕ| (start ≤ m) ∧ (∀g:ℕ ⟶ T. ((g = f ∈ (ℕm ⟶ T)) ⇒ ((F g) = (F f) ∈ ℤ)))} 

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>) ∈ (ℕ ⋃ (ℕ × ℕ))
⊢ 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:
\mforall{}[T:\{T:Type|  (T  \msubseteq{}r  \mBbbN{})  \mwedge{}  (\mdownarrow{}T)\}  ].  \mforall{}[F:(\mBbbN{}  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[M:\00D9(basic-strong-continuity(T;F))].
\mforall{}[f:\mBbbN{}  {}\mrightarrow{}  T].  \mforall{}[start:\mBbbN{}].
    (KleeneSearch(M;f;start)  \mmember{}  \00D9(\{m:\mBbbN{}|  (start  \mleq{}  m)  \mwedge{}  (\mforall{}g:\mBbbN{}  {}\mrightarrow{}  T.  ((g  =  f)  {}\mRightarrow{}  ((F  g)  =  (F  f))))\}  ))


By

---

Latex:
(Auto
  THEN  (Assert  \mkleeneopen{}\mforall{}M:basic-strong-continuity(T;F)
                                  (KleeneSearch(M;f;start)  \mmember{}  \{m:\mBbbN{}| 
                                                                                          (start  \mleq{}  m)
                                                                                          \mwedge{}  (\mforall{}g:\mBbbN{}  {}\mrightarrow{}  T.  ((g  =  f)  {}\mRightarrow{}  ((F  g)  =  (F  f))))\}  )\mkleeneclose{}\mcdot{}
  THENM  (D  3  THEN  EqTypeCD  THEN  Auto)
  )
  THEN  Thin  (-3)
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  DupHyp  (-1)
  THEN  (D  -1  With  \mkleeneopen{}f\mkleeneclose{}    THENA  Auto)
  THEN  ExRepD
  THEN  MoveToConcl  4
  THEN  (Assert  \mkleeneopen{}\mforall{}d,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))))\}  ))\mkleeneclose{}\mcdot{}
  THENM  ((D  -1  With  \mkleeneopen{}n\mkleeneclose{}    THENA  Auto)  THEN  ParallelLast  THEN  BHyp  -1  THEN  Auto)
  )
  THEN  CompleteInductionOnNat
  THEN  Intros
  THEN  Unfold  `KleeneSearch`  0
  THEN  GenConclAtAddr  [2;1]
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  D  -2
  THEN  Reduce  0
  THEN  Try  ((Fold  `member`  0  THEN  Auto)))

---

Home Index