Step
*
1
2
of Lemma
strong-continuity-test-prop2
1. [T] : Type
2. M : n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ?)
3. n : ℤ
4. [%1] : 0 < n
5. ∀f:ℕn - 1 ⟶ T. ∀b:ℕ?.
((↑isl(b))
⇒ (↑isr(strong-continuity-test(M;n - 1;f;b)))
⇒ (∃m:ℕ. (m < n - 1 ∧ (↑isl(strong-continuity-test(M;m;f;M m f))))))
6. f : ℕn ⟶ T
7. b : ℕ?
8. ↑isl(b)
9. ↑isr(strong-continuity-test(M;n;f;b))
⊢ ∃m:ℕ. (m < n ∧ (↑isl(strong-continuity-test(M;m;f;M m f))))
BY
{ ((RWO "strong-continuity-test-unroll" (-1) THENA Auto) THEN AllReduce) }
1
1. [T] : Type
2. M : n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ?)
3. n : ℤ
4. [%1] : 0 < n
5. ∀f:ℕn - 1 ⟶ T. ∀b:ℕ?.
((↑isl(b))
⇒ (↑isr(strong-continuity-test(M;n - 1;f;b)))
⇒ (∃m:ℕ. (m < n - 1 ∧ (↑isl(strong-continuity-test(M;m;f;M m f))))))
6. f : ℕn ⟶ T
7. b : ℕ?
8. ↑isl(b)
9. ↑isr(if (n =z 0) then b
if isl(M (n - 1) f) then inr Ax
else strong-continuity-test(M;n - 1;f;b)
fi )
⊢ ∃m:ℕ. (m < n ∧ (↑isl(strong-continuity-test(M;m;f;M m f))))
Latex:
Latex:
1. [T] : Type
2. M : n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} T) {}\mrightarrow{} (\mBbbN{}?)
3. n : \mBbbZ{}
4. [\%1] : 0 < n
5. \mforall{}f:\mBbbN{}n - 1 {}\mrightarrow{} T. \mforall{}b:\mBbbN{}?.
((\muparrow{}isl(b))
{}\mRightarrow{} (\muparrow{}isr(strong-continuity-test(M;n - 1;f;b)))
{}\mRightarrow{} (\mexists{}m:\mBbbN{}. (m < n - 1 \mwedge{} (\muparrow{}isl(strong-continuity-test(M;m;f;M m f))))))
6. f : \mBbbN{}n {}\mrightarrow{} T
7. b : \mBbbN{}?
8. \muparrow{}isl(b)
9. \muparrow{}isr(strong-continuity-test(M;n;f;b))
\mvdash{} \mexists{}m:\mBbbN{}. (m < n \mwedge{} (\muparrow{}isl(strong-continuity-test(M;m;f;M m f))))
By
Latex:
((RWO "strong-continuity-test-unroll" (-1) THENA Auto) THEN AllReduce)
Home
Index