---

Step * 2 1 of Lemma strong-continuity-test-bound-prop1


1. T : Type
2. M : n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕn?)
3. n : ℤ
4. 0 < n
5. ∀f:ℕn - 1 ⟶ T. ∀b:ℕn - 1.
     ((↑isl(strong-continuity-test-bound(M;n - 1;f;b)))
     ⇒ (strong-continuity-test-bound(M;n - 1;f;b) = (inl b) ∈ (ℕn - 1?)))
6. f : ℕn ⟶ T
7. b : ℕn
8. True
9. ¬(n = 0 ∈ ℤ)
10. ¬n - 1 < b
11. (n - 1) = b ∈ ℤ
⊢ strong-continuity-test-bound(M;n;f;b) = (inl b) ∈ (ℕn?)
BY
{ ((RWO "strong-continuity-test-bound-unroll" 0 THENA Auto) THEN AutoSplit) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  M  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  (\mBbbN{}n?)
3.  n  :  \mBbbZ{}
4.  0  <  n
5.  \mforall{}f:\mBbbN{}n  -  1  {}\mrightarrow{}  T.  \mforall{}b:\mBbbN{}n  -  1.
          ((\muparrow{}isl(strong-continuity-test-bound(M;n  -  1;f;b)))
          {}\mRightarrow{}  (strong-continuity-test-bound(M;n  -  1;f;b)  =  (inl  b)))
6.  f  :  \mBbbN{}n  {}\mrightarrow{}  T
7.  b  :  \mBbbN{}n
8.  True
9.  \mneg{}(n  =  0)
10.  \mneg{}n  -  1  <  b
11.  (n  -  1)  =  b
\mvdash{}  strong-continuity-test-bound(M;n;f;b)  =  (inl  b)


By

---

Latex:
((RWO  "strong-continuity-test-bound-unroll"  0  THENA  Auto)  THEN  AutoSplit)

---

Home Index