---

Step * 1 2 of Lemma rmaximum-select

.....upcase..... 
1. n : ℤ
2. d : ℤ
3. [%1] : 0 < d
4. ∀x:{n..(n + (d - 1)) + 1-} ⟶ ℝ. ∀e:ℝ.
     ((r0 < e) ⇒ (∃i:{n..(n + (d - 1)) + 1-}. ((primrec(d - 1;x[n];λi,s. rmax(s;x[n + i + 1])) - e) < x[i])))
⊢ ∀x:{n..(n + d) + 1-} ⟶ ℝ. ∀e:ℝ.
    ((r0 < e) ⇒ (∃i:{n..(n + d) + 1-}. ((primrec(d;x[n];λi,s. rmax(s;x[n + i + 1])) - e) < x[i])))
BY
{ ((RWO "primrec-unroll" 0 THENA Auto) THEN OldAutoBoolCase ⌜d <z 1⌝⋅ THEN (ParallelOp (-2) THEN 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-}. ((primrec(d - 1;x[n];λi,s. rmax(s;x[n + i + 1])) - e) < x[i])))
5. 1 ≤ d
6. x : {n..(n + d) + 1-} ⟶ ℝ
7. ∀e:ℝ. ((r0 < e) ⇒ (∃i:{n..(n + (d - 1)) + 1-}. ((primrec(d - 1;x[n];λi,s. rmax(s;x[n + i + 1])) - e) < x[i])))
8. e : ℝ
9. r0 < e
⊢ ∃i:{n..(n + d) + 1-}. ((rmax(primrec(d - 1;x[n];λi,s. rmax(s;x[n + i + 1]));x[n + (d - 1) + 1]) - e) < x[i])

---

Latex:

---

Latex:
.....upcase..... 
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{}\}.  ((primrec(d  -  1;x[n];\mlambda{}i,s.  rmax(s;x[n  +  i  +  1]))  -  e)  <  x[i])))
\mvdash{}  \mforall{}x:\{n..(n  +  d)  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}e:\mBbbR{}.
        ((r0  <  e)  {}\mRightarrow{}  (\mexists{}i:\{n..(n  +  d)  +  1\msupminus{}\}.  ((primrec(d;x[n];\mlambda{}i,s.  rmax(s;x[n  +  i  +  1]))  -  e)  <  x[i])))


By

---

Latex:
((RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  OldAutoBoolCase  \mkleeneopen{}d  <z  1\mkleeneclose{}\mcdot{}
  THEN  (ParallelOp  (-2)  THEN  Auto)\mcdot{})\mcdot{}

---

Home Index