---

Step * 2 1 of Lemma rmaximum_functionality_wrt_rleq


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])))
BY
{ (ParallelOp (-2)
   THEN RepeatFor 2 (ParallelLast)
   THEN Try ((BLemma `rmax_functionality_wrt_rleq` THEN Auto))
   THEN RepeatFor 3 (ParallelLast)
   THEN Auto') }

---

Latex:

---

Latex:

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]))))
5.  1  \mleq{}  k
\mvdash{}  \mforall{}x,y@0:\{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@0[k@0])))
        {}\mRightarrow{}  (rmax(primrec(k  -  1;x[n];\mlambda{}i,s.  rmax(s;x[n  +  i  +  1]));x[n
              +  (k  -  1)
              +  1])  \mleq{}  rmax(primrec(k  -  1;y@0[n];\mlambda{}i,s.  rmax(s;y@0[n  +  i  +  1]));y@0[n  +  (k  -  1)  +  1])))


By

---

Latex:
(ParallelOp  (-2)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  Try  ((BLemma  `rmax\_functionality\_wrt\_rleq`  THEN  Auto))
  THEN  RepeatFor  3  (ParallelLast)
  THEN  Auto')

---

Home Index