---

Step * 2 of Lemma rmaximum_functionality_wrt_rleq

.....upcase..... 
1. n : ℤ
2. k : ℤ
3. 0 < k
4. ∀x,y:{n..(n + (k - 1)) + 1-} ⟶ ℝ.
     ((∀k@0:ℤ. ((n ≤ k@0) ⇒ (k@0 ≤ (n + (k - 1))) ⇒ (x[k@0] ≤ y[k@0])))
     ⇒ (primrec(k - 1;x[n];λi,s. rmax(s;x[n + i + 1])) ≤ primrec(k - 1;y[n];λi,s. rmax(s;y[n + i + 1]))))
⊢ ∀x,y:{n..(n + k) + 1-} ⟶ ℝ.
    ((∀k@0:ℤ. ((n ≤ k@0) ⇒ (k@0 ≤ (n + k)) ⇒ (x[k@0] ≤ y[k@0])))
    ⇒ (primrec(k;x[n];λi,s. rmax(s;x[n + i + 1])) ≤ primrec(k;y[n];λi,s. rmax(s;y[n + i + 1]))))
BY
{ ((RWO "primrec-unroll" 0 THENA Auto) THEN OldAutoBoolCase ⌜k <z 1⌝⋅)⋅ }

1
1. n : ℤ
2. k : ℤ
3. 0 < k
4. ∀x,y:{n..(n + (k - 1)) + 1-} ⟶ ℝ.
     ((∀k@0:ℤ. ((n ≤ k@0) ⇒ (k@0 ≤ (n + (k - 1))) ⇒ (x[k@0] ≤ y[k@0])))
     ⇒ (primrec(k - 1;x[n];λi,s. rmax(s;x[n + i + 1])) ≤ primrec(k - 1;y[n];λi,s. rmax(s;y[n + i + 1]))))
5. 1 ≤ k
⊢ ∀x,y@0:{n..(n + k) + 1-} ⟶ ℝ.
    ((∀k@0:ℤ. ((n ≤ k@0) ⇒ (k@0 ≤ (n + k)) ⇒ (x[k@0] ≤ y@0[k@0])))
    ⇒ (rmax(primrec(k - 1;x[n];λi,s. rmax(s;x[n + i + 1]));x[n
       + (k - 1)
       + 1]) ≤ rmax(primrec(k - 1;y@0[n];λi,s. rmax(s;y@0[n + i + 1]));y@0[n + (k - 1) + 1])))

---

Latex:

---

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


By

---

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

---

Home Index