---

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


1. M : n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕn?)
2. n : ℕ
3. m : ℕ
4. f : ℕ ⟶ ℕ
5. b : ℕn
6. b < m@i
7. ↑isl(M n f)@i
8. ↑isl(M m f)@i
9. ↑isl(strong-continuity-test-bound(M;n;f;b))@i
10. ↑isl(strong-continuity-test-bound(M;m;f;b))@i
11. ¬n < m
12. m < n
⊢ m = n ∈ ℕ
BY
{ ((InstLemma `strong-continuity-test-bound-prop2` [⌜ℕ⌝;⌜M⌝;⌜n⌝;⌜f⌝;⌜b⌝]⋅ THENA Auto)
   THEN InstHyp [⌜m⌝] (-1)⋅
   THEN Auto
   THEN Assert ⌜¬↑isl(M m f)⌝⋅
   THEN Auto
   THEN (FLemma `isr-not-isl` [-1] THENA Auto)
   THEN HypSubst' (-1) 0
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  M  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  (\mBbbN{}n?)
2.  n  :  \mBbbN{}
3.  m  :  \mBbbN{}
4.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
5.  b  :  \mBbbN{}n
6.  b  <  m@i
7.  \muparrow{}isl(M  n  f)@i
8.  \muparrow{}isl(M  m  f)@i
9.  \muparrow{}isl(strong-continuity-test-bound(M;n;f;b))@i
10.  \muparrow{}isl(strong-continuity-test-bound(M;m;f;b))@i
11.  \mneg{}n  <  m
12.  m  <  n
\mvdash{}  m  =  n


By

---

Latex:
((InstLemma  `strong-continuity-test-bound-prop2`  [\mkleeneopen{}\mBbbN{}\mkleeneclose{};\mkleeneopen{}M\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  InstHyp  [\mkleeneopen{}m\mkleeneclose{}]  (-1)\mcdot{}
  THEN  Auto
  THEN  Assert  \mkleeneopen{}\mneg{}\muparrow{}isl(M  m  f)\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  (FLemma  `isr-not-isl`  [-1]  THENA  Auto)
  THEN  HypSubst'  (-1)  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index