---

Step * 2 2 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. ↑isl(if isl(M (n - 1) f) then inr Ax  else strong-continuity-test-bound(M;n - 1;f;b) fi )
9. ¬(n = 0 ∈ ℤ)
10. ¬n - 1 < b
11. ¬((n - 1) = b ∈ ℤ)
⊢ strong-continuity-test-bound(M;n;f;b) = (inl b) ∈ (ℕn?)
BY
{ (SplitOnHypITE -4  THEN AllReduce THEN Try (CpltAuto)) }

1
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. ↑isl(strong-continuity-test-bound(M;n - 1;f;b))
9. ¬(n = 0 ∈ ℤ)
10. ¬n - 1 < b
11. ¬((n - 1) = b ∈ ℤ)
12. ¬↑isl(M (n - 1) f)
⊢ strong-continuity-test-bound(M;n;f;b) = (inl b) ∈ (ℕn?)

---

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.  \muparrow{}isl(if  isl(M  (n  -  1)  f)  then  inr  Ax    else  strong-continuity-test-bound(M;n  -  1;f;b)  fi  )
9.  \mneg{}(n  =  0)
10.  \mneg{}n  -  1  <  b
11.  \mneg{}((n  -  1)  =  b)
\mvdash{}  strong-continuity-test-bound(M;n;f;b)  =  (inl  b)


By

---

Latex:
(SplitOnHypITE  -4    THEN  AllReduce  THEN  Try  (CpltAuto))

---

Home Index