---

Step * 1 1 1 of Lemma pseudo-bounded-is-bounded


1. S : {S:Type| S ⊆r ℕ} 
2. S ⊆r ℕ
3. m : S
4. ∀f:ℕ ⟶ S. ∃k:ℕ. ∀n:{k...}. f n < n
5. F : f:(ℕ ⟶ S) ⟶ ℕ
6. ∀f:ℕ ⟶ S. ∀n:{F f...}.  f n < n
7. ∀f:ℕ ⟶ S. ∃n:ℕ. ∀g:ℕ ⟶ S. ((f = g ∈ (ℕn ⟶ S)) ⇒ ((F f) = (F g) ∈ ℕ))
8. n : ℕ
9. ∀g:ℕ ⟶ S. (((λn.m) = g ∈ (ℕn ⟶ S)) ⇒ ((F (λn.m)) = (F g) ∈ ℕ))
10. k : S
⊢ k ≤ imax(F (λn.m);n)
BY
{ (InstHyp [⌜λi.if i <z n then m else k fi ⌝] (-2)⋅ THENA Auto) }

1
1. S : {S:Type| S ⊆r ℕ} 
2. S ⊆r ℕ
3. m : S
4. ∀f:ℕ ⟶ S. ∃k:ℕ. ∀n:{k...}. f n < n
5. F : f:(ℕ ⟶ S) ⟶ ℕ
6. ∀f:ℕ ⟶ S. ∀n:{F f...}.  f n < n
7. ∀f:ℕ ⟶ S. ∃n:ℕ. ∀g:ℕ ⟶ S. ((f = g ∈ (ℕn ⟶ S)) ⇒ ((F f) = (F g) ∈ ℕ))
8. n : ℕ
9. ∀g:ℕ ⟶ S. (((λn.m) = g ∈ (ℕn ⟶ S)) ⇒ ((F (λn.m)) = (F g) ∈ ℕ))
10. k : S
11. (F (λn.m)) = (F (λi.if i <z n then m else k fi )) ∈ ℕ
⊢ k ≤ imax(F (λn.m);n)

---

Latex:

---

Latex:

1.  S  :  \{S:Type|  S  \msubseteq{}r  \mBbbN{}\} 
2.  S  \msubseteq{}r  \mBbbN{}
3.  m  :  S
4.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  S.  \mexists{}k:\mBbbN{}.  \mforall{}n:\{k...\}.  f  n  <  n
5.  F  :  f:(\mBbbN{}  {}\mrightarrow{}  S)  {}\mrightarrow{}  \mBbbN{}
6.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  S.  \mforall{}n:\{F  f...\}.    f  n  <  n
7.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  S.  \mexists{}n:\mBbbN{}.  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  S.  ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g)))
8.  n  :  \mBbbN{}
9.  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  S.  (((\mlambda{}n.m)  =  g)  {}\mRightarrow{}  ((F  (\mlambda{}n.m))  =  (F  g)))
10.  k  :  S
\mvdash{}  k  \mleq{}  imax(F  (\mlambda{}n.m);n)


By

---

Latex:
(InstHyp  [\mkleeneopen{}\mlambda{}i.if  i  <z  n  then  m  else  k  fi  \mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)

---

Home Index