---

Step * 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(strong-continuity-test-bound(M;n;f;b))
⊢ strong-continuity-test-bound(M;n;f;b) = (inl b) ∈ (ℕn?)
BY
{ ((RWO "strong-continuity-test-bound-unroll" (-1) THENA Auto)
   THEN (SplitOnHypITE -1  THEN AllReduce THEN Try (CpltAuto))
   THEN (SplitOnHypITE -2  THEN AllReduce THEN Try (CpltAuto))
   THEN SplitOnHypITE -3 
   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. True
9. ¬(n = 0 ∈ ℤ)
10. ¬n - 1 < b
11. (n - 1) = b ∈ ℤ
⊢ strong-continuity-test-bound(M;n;f;b) = (inl b) ∈ (ℕn?)

2
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?)

---

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(strong-continuity-test-bound(M;n;f;b))
\mvdash{}  strong-continuity-test-bound(M;n;f;b)  =  (inl  b)


By

---

Latex:
((RWO  "strong-continuity-test-bound-unroll"  (-1)  THENA  Auto)
  THEN  (SplitOnHypITE  -1    THEN  AllReduce  THEN  Try  (CpltAuto))
  THEN  (SplitOnHypITE  -2    THEN  AllReduce  THEN  Try  (CpltAuto))
  THEN  SplitOnHypITE  -3 
  THEN  AllReduce
  THEN  Try  (CpltAuto))

---

Home Index