---

Step * of Lemma rmaximum_functionality_wrt_rleq

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

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

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

---

Latex:

---

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


By

---

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

---

Home Index