---

Step * of Lemma rmaximum-lub

No Annotations
∀n,m:ℤ. ∀x:{n..m + 1-} ⟶ ℝ. ∀r:ℝ.  (∀k:{n..m + 1-}. (x[k] ≤ r)) ⇒ (rmaximum(n;m;i.x[i]) ≤ r) supposing n ≤ m
BY
{ ((Unfold `rmaximum` 0 THEN Auto)
   THEN (Assert ⌜∀d:ℕ. ∀n,m:ℤ. ∀x:{n..m + 1-} ⟶ ℝ.
                   (((m - n) ≤ d)
                   ⇒ (n ≤ m)
                   ⇒ (∀k:{n..m + 1-}. (x[k] ≤ r))
                   ⇒ (primrec(m - n;x[n];λi,s. rmax(s;x[n + i + 1])) ≤ r))⌝⋅
   THENM (InstHyp [⌜m - n⌝;⌜n⌝;⌜m⌝;⌜x⌝] (-1)⋅ THEN Auto THEN Auto')
   )
   THEN InductionOnNat
   THEN Auto
   THEN RWO "primrec-unroll" 0
   THEN Auto
   THEN AutoSplit
   THEN Auto'
   THEN BLemma `rmax_lb`
   THEN Auto
   THEN Auto') }

1
1. n : ℤ
2. m : ℤ
3. x : {n..m + 1-} ⟶ ℝ
4. r : ℝ
5. n ≤ m
6. ∀k:{n..m + 1-}. (x[k] ≤ r)
7. d : ℤ
8. 0 < d
9. ∀n,m:ℤ. ∀x:{n..m + 1-} ⟶ ℝ.
     (((m - n) ≤ (d - 1))
     ⇒ (n ≤ m)
     ⇒ (∀k:{n..m + 1-}. (x[k] ≤ r))
     ⇒ (primrec(m - n;x[n];λi,s. rmax(s;x[n + i + 1])) ≤ r))
10. n1 : ℤ
11. m1 : ℤ
12. ¬m1 - n1 < 1
13. x1 : {n1..m1 + 1-} ⟶ ℝ
14. (m1 - n1) ≤ d
15. n1 ≤ m1
16. ∀k:{n1..m1 + 1-}. (x1[k] ≤ r)
⊢ primrec(m1 - n1 - 1;x1[n1];λi,s. rmax(s;x1[n1 + i + 1])) ≤ r

---

Latex:

---

Latex:
No  Annotations
\mforall{}n,m:\mBbbZ{}.  \mforall{}x:\{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}r:\mBbbR{}.
    (\mforall{}k:\{n..m  +  1\msupminus{}\}.  (x[k]  \mleq{}  r))  {}\mRightarrow{}  (rmaximum(n;m;i.x[i])  \mleq{}  r)  supposing  n  \mleq{}  m


By

---

Latex:
((Unfold  `rmaximum`  0  THEN  Auto)
  THEN  (Assert  \mkleeneopen{}\mforall{}d:\mBbbN{}.  \mforall{}n,m:\mBbbZ{}.  \mforall{}x:\{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}.
                                  (((m  -  n)  \mleq{}  d)
                                  {}\mRightarrow{}  (n  \mleq{}  m)
                                  {}\mRightarrow{}  (\mforall{}k:\{n..m  +  1\msupminus{}\}.  (x[k]  \mleq{}  r))
                                  {}\mRightarrow{}  (primrec(m  -  n;x[n];\mlambda{}i,s.  rmax(s;x[n  +  i  +  1]))  \mleq{}  r))\mkleeneclose{}\mcdot{}
  THENM  (InstHyp  [\mkleeneopen{}m  -  n\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto  THEN  Auto')
  )
  THEN  InductionOnNat
  THEN  Auto
  THEN  RWO  "primrec-unroll"  0
  THEN  Auto
  THEN  AutoSplit
  THEN  Auto'
  THEN  BLemma  `rmax\_lb`
  THEN  Auto
  THEN  Auto')

---

Home Index