---

Step * 1 of Lemma strong-continuity-test-bound-prop2


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))) ⇒ (∀i:ℕ. (b < i ⇒ i < n - 1 ⇒ (↑isr(M i f)))))
6. f : ℕn ⟶ T
7. b : ℕn
8. ↑isl(strong-continuity-test-bound(M;n;f;b))@i
9. i : ℕ@i
10. b < i@i
11. i < n@i
⊢ ↑isr(M i f)
BY
{ ((RWO "strong-continuity-test-bound-unroll" (-4) THENA Auto)
   THEN ((SplitOnHypITE (-4) THENA Auto) THEN AllReduce THEN Try (CpltAuto))
   THEN ((SplitOnHypITE (-5) THENA Auto) THEN AllReduce THEN Try (CpltAuto))
   THEN ((SplitOnHypITE (-6) THENA Auto) THEN AllReduce THEN Try (CpltAuto))
   THEN ((SplitOnHypITE (-7) THENA Auto) THEN AllReduce THEN Try (CpltAuto))
   THEN (InstHyp [⌜f⌝;⌜b⌝] (-11)⋅ THENA Auto)) }

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))) ⇒ (∀i:ℕ. (b < i ⇒ i < n - 1 ⇒ (↑isr(M i f)))))
6. f : ℕn ⟶ T
7. b : ℕn
8. ↑isl(strong-continuity-test-bound(M;n - 1;f;b))@i
9. i : ℕ@i
10. b < i@i
11. i < n@i
12. ¬(n = 0 ∈ ℤ)
13. ¬n - 1 < b
14. ¬((n - 1) = b ∈ ℤ)
15. ¬↑isl(M (n - 1) f)
16. ∀i:ℕ. (b < i ⇒ i < n - 1 ⇒ (↑isr(M i f)))
⊢ ↑isr(M i f)

---

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{}  (\mforall{}i:\mBbbN{}.  (b  <  i  {}\mRightarrow{}  i  <  n  -  1  {}\mRightarrow{}  (\muparrow{}isr(M  i  f)))))
6.  f  :  \mBbbN{}n  {}\mrightarrow{}  T
7.  b  :  \mBbbN{}n
8.  \muparrow{}isl(strong-continuity-test-bound(M;n;f;b))@i
9.  i  :  \mBbbN{}@i
10.  b  <  i@i
11.  i  <  n@i
\mvdash{}  \muparrow{}isr(M  i  f)


By

---

Latex:
((RWO  "strong-continuity-test-bound-unroll"  (-4)  THENA  Auto)
  THEN  ((SplitOnHypITE  (-4)  THENA  Auto)  THEN  AllReduce  THEN  Try  (CpltAuto))
  THEN  ((SplitOnHypITE  (-5)  THENA  Auto)  THEN  AllReduce  THEN  Try  (CpltAuto))
  THEN  ((SplitOnHypITE  (-6)  THENA  Auto)  THEN  AllReduce  THEN  Try  (CpltAuto))
  THEN  ((SplitOnHypITE  (-7)  THENA  Auto)  THEN  AllReduce  THEN  Try  (CpltAuto))
  THEN  (InstHyp  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]  (-11)\mcdot{}  THENA  Auto))

---

Home Index