---

Step * of Lemma strong-continuity-test-bound-prop3

∀[M:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕn?)]. ∀[n,m:ℕ]. ∀[f:ℕ ⟶ ℕ]. ∀[b:ℕn].
  (b < m
  ⇒ (↑isl(M n f))
  ⇒ (↑isl(M m f))
  ⇒ (↑isl(strong-continuity-test-bound(M;n;f;b)))
  ⇒ (↑isl(strong-continuity-test-bound(M;m;f;b)))
  ⇒ (m = n ∈ ℕ))
BY
{ (UnivCD THENA Auto) }

1
1. M : n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕn?)
2. n : ℕ
3. m : ℕ
4. f : ℕ ⟶ ℕ
5. b : ℕn
6. b < m@i
7. ↑isl(M n f)@i
8. ↑isl(M m f)@i
9. ↑isl(strong-continuity-test-bound(M;n;f;b))@i
10. ↑isl(strong-continuity-test-bound(M;m;f;b))@i
⊢ m = n ∈ ℕ

---

Latex:

---

Latex:
\mforall{}[M:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  (\mBbbN{}n?)].  \mforall{}[n,m:\mBbbN{}].  \mforall{}[f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[b:\mBbbN{}n].
    (b  <  m
    {}\mRightarrow{}  (\muparrow{}isl(M  n  f))
    {}\mRightarrow{}  (\muparrow{}isl(M  m  f))
    {}\mRightarrow{}  (\muparrow{}isl(strong-continuity-test-bound(M;n;f;b)))
    {}\mRightarrow{}  (\muparrow{}isl(strong-continuity-test-bound(M;m;f;b)))
    {}\mRightarrow{}  (m  =  n))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index