---

Step * 1 of Lemma rmaximum-lub


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
BY
{ (InstHyp [⌜n1⌝;⌜m1 - 1⌝;⌜x1⌝] 9⋅ THEN Auto') }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  m  :  \mBbbZ{}
3.  x  :  \{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
4.  r  :  \mBbbR{}
5.  n  \mleq{}  m
6.  \mforall{}k:\{n..m  +  1\msupminus{}\}.  (x[k]  \mleq{}  r)
7.  d  :  \mBbbZ{}
8.  0  <  d
9.  \mforall{}n,m:\mBbbZ{}.  \mforall{}x:\{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}.
          (((m  -  n)  \mleq{}  (d  -  1))
          {}\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))
10.  n1  :  \mBbbZ{}
11.  m1  :  \mBbbZ{}
12.  \mneg{}m1  -  n1  <  1
13.  x1  :  \{n1..m1  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
14.  (m1  -  n1)  \mleq{}  d
15.  n1  \mleq{}  m1
16.  \mforall{}k:\{n1..m1  +  1\msupminus{}\}.  (x1[k]  \mleq{}  r)
\mvdash{}  primrec(m1  -  n1  -  1;x1[n1];\mlambda{}i,s.  rmax(s;x1[n1  +  i  +  1]))  \mleq{}  r


By

---

Latex:
(InstHyp  [\mkleeneopen{}n1\mkleeneclose{};\mkleeneopen{}m1  -  1\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{}]  9\mcdot{}  THEN  Auto')

---

Home Index