---

Step * of Lemma rmaximum-constant

No Annotations
∀[n,m:ℤ].  ∀[x:{n..m + 1-} ⟶ ℝ]. ∀[r:ℝ].  rmaximum(n;m;i.x[i]) = r supposing ∀i:{n..m + 1-}. (x[i] = r) supposing n ≤ m
BY
{ (Auto
   THEN RepeatFor 3 (MoveToConcl (-1))
   THEN 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)])) }

1
1. n : ℤ
2. d : ℤ
⊢ ∀x:{n..(n + 0) + 1-} ⟶ ℝ. ∀r:ℝ.  ((∀i:{n..(n + 0) + 1-}. (x[i] = r)) ⇒ (x[n] = r))

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

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  RepeatFor  3  (MoveToConcl  (-1))
  THEN  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)]))

---

Home Index