---

Step * 1 of Lemma rmaximum_ub


1. k : ℤ
2. n : ℤ
3. m : ℤ
4. n ≤ m
⊢ ∀x:{n..m + 1-} ⟶ ℝ. ((n ≤ k) ⇒ (k ≤ m) ⇒ (x[k] ≤ rmaximum(n;m;i.x[i])))
BY
{ xxx(Unfold `rmaximum` 0
      THEN (GenConcl ⌜(m - n) = d ∈ ℕ⌝⋅ THENA Auto')
      THEN (Subst ⌜m ~ n + d⌝ 0⋅ THENL [Auto'; (ThinVar `m' THEN (NatInd (-1)) THEN Reduce 0)]))xxx }

1
1. k : ℤ
2. n : ℤ
3. d : ℤ
⊢ ∀x:{n..(n + 0) + 1-} ⟶ ℝ. ((n ≤ k) ⇒ (k ≤ (n + 0)) ⇒ (x[k] ≤ x[n]))

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

---

Latex:

---

Latex:

1.  k  :  \mBbbZ{}
2.  n  :  \mBbbZ{}
3.  m  :  \mBbbZ{}
4.  n  \mleq{}  m
\mvdash{}  \mforall{}x:\{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}.  ((n  \mleq{}  k)  {}\mRightarrow{}  (k  \mleq{}  m)  {}\mRightarrow{}  (x[k]  \mleq{}  rmaximum(n;m;i.x[i])))


By

---

Latex:
xxx(Unfold  `rmaximum`  0
        THEN  (GenConcl  \mkleeneopen{}(m  -  n)  =  d\mkleeneclose{}\mcdot{}  THENA  Auto')
        THEN  (Subst  \mkleeneopen{}m  \msim{}  n  +  d\mkleeneclose{}  0\mcdot{}  THENL  [Auto';  (ThinVar  `m'  THEN  (NatInd  (-1))  THEN  Reduce  0)]))xxx

---

Home Index