---

Step * of Lemma rmaximum-split

No Annotations
∀[n,m:ℤ]. ∀[x:{n..m + 1-} ⟶ ℝ]. ∀[k:ℤ].
  (rmaximum(n;m;i.x[i]) = rmax(rmaximum(n;k;i.x[i]);rmaximum(k + 1;m;i.x[i]))) supposing (k < m and (n ≤ k))
BY
{ (Auto
   THEN Unfold `rmaximum` 0
   THEN (GenConcl ⌜(k - n) = i ∈ ℕ⌝⋅ THENA Auto')
   THEN (GenConcl ⌜(m - k + 1) = j ∈ ℕ⌝⋅ THENA Auto')
   THEN Subst' ⌜(m - n) = ((i + j) + 1) ∈ ℤ⌝ 0⋅
   THEN Subst' k = (n + i) ∈ ℤ 0
   THEN (GenConcl ⌜x = X ∈ ({n..(n + i + j) + 2-} ⟶ ℝ)⌝⋅
         THENA (Auto THEN Subst' ⌜((n + i + j) + 2) = (m + 1) ∈ ℤ⌝ 0⋅ THEN Auto')
         )
   THEN Subst' ((i + j) + 1) = ((j + 1) + i) ∈ ℤ 0) }

1
1. n : ℤ
2. m : ℤ
3. x : {n..m + 1-} ⟶ ℝ
4. k : ℤ
5. n ≤ k
6. k < m
7. i : ℕ
8. (k - n) = i ∈ ℕ
9. j : ℕ
10. (m - k + 1) = j ∈ ℕ
11. X : {n..(n + i + j) + 2-} ⟶ ℝ
12. x = X ∈ ({n..(n + i + j) + 2-} ⟶ ℝ)
⊢ primrec((j + 1) + i;X[n];λi,s. rmax(s;X[n + i + 1]))
= rmax(primrec(i;X[n];λi,s. rmax(s;X[n + i + 1]));primrec(j;X[(n + i) + 1];λi@0,s. rmax(s;X[((n + i) + 1) + i@0 + 1])))

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  Unfold  `rmaximum`  0
  THEN  (GenConcl  \mkleeneopen{}(k  -  n)  =  i\mkleeneclose{}\mcdot{}  THENA  Auto')
  THEN  (GenConcl  \mkleeneopen{}(m  -  k  +  1)  =  j\mkleeneclose{}\mcdot{}  THENA  Auto')
  THEN  Subst'  \mkleeneopen{}(m  -  n)  =  ((i  +  j)  +  1)\mkleeneclose{}  0\mcdot{}
  THEN  Subst'  k  =  (n  +  i)  0
  THEN  (GenConcl  \mkleeneopen{}x  =  X\mkleeneclose{}\mcdot{}  THENA  (Auto  THEN  Subst'  \mkleeneopen{}((n  +  i  +  j)  +  2)  =  (m  +  1)\mkleeneclose{}  0\mcdot{}  THEN  Auto'))
  THEN  Subst'  ((i  +  j)  +  1)  =  ((j  +  1)  +  i)  0)

---

Home Index