---

Step * 1 2 1 1 1 1 1 1 of Lemma KleeneSearch_wf

.....antecedent..... 
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)
⊢ M start g is an integer
BY
{ ((Assert F f is an integer BY
          (GenConclAtAddr [1] THEN Reduce 0 THEN Auto))
   THEN RenameVar `x' (-1)
   THEN UseWitness ⌜x⌝⋅
   THEN DoSubsume
   THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
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)
\mvdash{}  M  start  g  is  an  integer


By

---

Latex:
((Assert  F  f  is  an  integer  BY
                (GenConclAtAddr  [1]  THEN  Reduce  0  THEN  Auto))
  THEN  RenameVar  `x'  (-1)
  THEN  UseWitness  \mkleeneopen{}x\mkleeneclose{}\mcdot{}
  THEN  DoSubsume
  THEN  Auto)

---

Home Index