---

Step * 2 of Lemma rmaximum-constant

.....upcase..... 
1. n : ℤ
2. d : ℤ
3. 0 < d
4. ∀x:{n..(n + (d - 1)) + 1-} ⟶ ℝ. ∀r:ℝ.
     ((∀i:{n..(n + (d - 1)) + 1-}. (x[i] = r)) ⇒ (primrec(d - 1;x[n];λi,s. rmax(s;x[n + i + 1])) = r))
⊢ ∀x:{n..(n + d) + 1-} ⟶ ℝ. ∀r:ℝ.  ((∀i:{n..(n + d) + 1-}. (x[i] = r)) ⇒ (primrec(d;x[n];λi,s. rmax(s;x[n + i + 1])) =\000C r))
BY
{ ((RWO "primrec-unroll" 0 THENA Auto)
   THEN OldAutoBoolCase ⌜d <z 1⌝⋅
   THEN (ParallelOp (-2) THEN ParallelLast THEN Auto)⋅)⋅ }

---

Latex:

---

Latex:
.....upcase..... 
1.  n  :  \mBbbZ{}
2.  d  :  \mBbbZ{}
3.  0  <  d
4.  \mforall{}x:\{n..(n  +  (d  -  1))  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}r:\mBbbR{}.
          ((\mforall{}i:\{n..(n  +  (d  -  1))  +  1\msupminus{}\}.  (x[i]  =  r))  {}\mRightarrow{}  (primrec(d  -  1;x[n];\mlambda{}i,s.  rmax(s;x[n  +  i  +  1]))  =  \000Cr))
\mvdash{}  \mforall{}x:\{n..(n  +  d)  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}r:\mBbbR{}.
        ((\mforall{}i:\{n..(n  +  d)  +  1\msupminus{}\}.  (x[i]  =  r))  {}\mRightarrow{}  (primrec(d;x[n];\mlambda{}i,s.  rmax(s;x[n  +  i  +  1]))  =  r))


By

---

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

---

Home Index