---

Step * 1 2 1 1 of Lemma rminimum-select


1. n : ℤ
2. d : ℤ
3. [%1] : 0 < d
4. ∀x:{n..(n + (d - 1)) + 1-} ⟶ ℝ. ∀e:ℝ.
     ((r0 < e) ⇒ (∃i:{n..(n + (d - 1)) + 1-}. (x[i] < (primrec(d - 1;x[n];λi,s. rmin(s;x[n + i + 1])) + e))))
5. 1 ≤ d
6. x : {n..(n + d) + 1-} ⟶ ℝ
7. ∀e:ℝ. ((r0 < e) ⇒ (∃i:{n..(n + (d - 1)) + 1-}. (x[i] < (primrec(d - 1;x[n];λi,s. rmin(s;x[n + i + 1])) + e))))
8. e : ℝ
9. r0 < e
10. i : {n..(n + (d - 1)) + 1-}
11. v : ℝ
12. primrec(d - 1;x[n];λi,s. rmin(s;x[n + i + 1])) = v ∈ ℝ
13. x[i] < (v + e)
⊢ ∃i:{n..(n + d) + 1-}. (x[i] < (rmin(v;x[n + (d - 1) + 1]) + e))
BY
{ ((InstLemma `rless-cases` [⌜r0⌝;⌜e⌝;⌜x[i] - x[n + (d - 1) + 1]⌝]⋅ THEN Auto)
   THEN D -1
   THEN (nRAdd ⌜x[n + (d - 1) + 1]⌝ (-1)⋅ THENA Auto)) }

1
1. n : ℤ
2. d : ℤ
3. [%1] : 0 < d
4. ∀x:{n..(n + (d - 1)) + 1-} ⟶ ℝ. ∀e:ℝ.
     ((r0 < e) ⇒ (∃i:{n..(n + (d - 1)) + 1-}. (x[i] < (primrec(d - 1;x[n];λi,s. rmin(s;x[n + i + 1])) + e))))
5. 1 ≤ d
6. x : {n..(n + d) + 1-} ⟶ ℝ
7. ∀e:ℝ. ((r0 < e) ⇒ (∃i:{n..(n + (d - 1)) + 1-}. (x[i] < (primrec(d - 1;x[n];λi,s. rmin(s;x[n + i + 1])) + e))))
8. e : ℝ
9. r0 < e
10. i : {n..(n + (d - 1)) + 1-}
11. v : ℝ
12. primrec(d - 1;x[n];λi,s. rmin(s;x[n + i + 1])) = v ∈ ℝ
13. x[i] < (v + e)
14. x[n + (d - 1) + 1] < x[i]
⊢ ∃i:{n..(n + d) + 1-}. (x[i] < (rmin(v;x[n + (d - 1) + 1]) + e))

2
1. n : ℤ
2. d : ℤ
3. [%1] : 0 < d
4. ∀x:{n..(n + (d - 1)) + 1-} ⟶ ℝ. ∀e:ℝ.
     ((r0 < e) ⇒ (∃i:{n..(n + (d - 1)) + 1-}. (x[i] < (primrec(d - 1;x[n];λi,s. rmin(s;x[n + i + 1])) + e))))
5. 1 ≤ d
6. x : {n..(n + d) + 1-} ⟶ ℝ
7. ∀e:ℝ. ((r0 < e) ⇒ (∃i:{n..(n + (d - 1)) + 1-}. (x[i] < (primrec(d - 1;x[n];λi,s. rmin(s;x[n + i + 1])) + e))))
8. e : ℝ
9. r0 < e
10. i : {n..(n + (d - 1)) + 1-}
11. v : ℝ
12. primrec(d - 1;x[n];λi,s. rmin(s;x[n + i + 1])) = v ∈ ℝ
13. x[i] < (v + e)
14. x[i] < (x[n + (d - 1) + 1] + e)
⊢ ∃i:{n..(n + d) + 1-}. (x[i] < (rmin(v;x[n + (d - 1) + 1]) + e))

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  d  :  \mBbbZ{}
3.  [\%1]  :  0  <  d
4.  \mforall{}x:\{n..(n  +  (d  -  1))  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}e:\mBbbR{}.
          ((r0  <  e)
          {}\mRightarrow{}  (\mexists{}i:\{n..(n  +  (d  -  1))  +  1\msupminus{}\}.  (x[i]  <  (primrec(d  -  1;x[n];\mlambda{}i,s.  rmin(s;x[n  +  i  +  1]))  +  e))))
5.  1  \mleq{}  d
6.  x  :  \{n..(n  +  d)  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
7.  \mforall{}e:\mBbbR{}
          ((r0  <  e)
          {}\mRightarrow{}  (\mexists{}i:\{n..(n  +  (d  -  1))  +  1\msupminus{}\}.  (x[i]  <  (primrec(d  -  1;x[n];\mlambda{}i,s.  rmin(s;x[n  +  i  +  1]))  +  e))))
8.  e  :  \mBbbR{}
9.  r0  <  e
10.  i  :  \{n..(n  +  (d  -  1))  +  1\msupminus{}\}
11.  v  :  \mBbbR{}
12.  primrec(d  -  1;x[n];\mlambda{}i,s.  rmin(s;x[n  +  i  +  1]))  =  v
13.  x[i]  <  (v  +  e)
\mvdash{}  \mexists{}i:\{n..(n  +  d)  +  1\msupminus{}\}.  (x[i]  <  (rmin(v;x[n  +  (d  -  1)  +  1])  +  e))


By

---

Latex:
((InstLemma  `rless-cases`  [\mkleeneopen{}r0\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x[i]  -  x[n  +  (d  -  1)  +  1]\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  D  -1
  THEN  (nRAdd  \mkleeneopen{}x[n  +  (d  -  1)  +  1]\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto))

---

Home Index