---

Step * 2 of Lemma rminimum-positive


1. n : ℤ
2. m : ℤ
3. n ≤ m
4. x : {n..m + 1-} ⟶ ℝ
5. ∀i:{n..m + 1-}. (r0 < x[i])
⊢ r0 < rminimum(n;m;i.x[i])
BY
{ ((RepeatFor 2 (MoveToConcl (-1)) THEN Unfold `so_apply` 0)
   THEN Unfold `rminimum` 0
   THEN (GenConcl ⌜(m - n) = d ∈ ℕ⌝⋅ THENA Auto')
   THEN (Subst ⌜m ~ n + d⌝ 0⋅
         THENL [Auto'
               ; (ThinVar `m'
                  THEN (NatInd (-1))
                  THEN Reduce 0
                  THEN Auto
                  THEN (RWO "primrec-unroll" 0 THENA Auto)
                  THEN (OReduce 0 THENA Auto))]
   )) }

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

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  m  :  \mBbbZ{}
3.  n  \mleq{}  m
4.  x  :  \{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
5.  \mforall{}i:\{n..m  +  1\msupminus{}\}.  (r0  <  x[i])
\mvdash{}  r0  <  rminimum(n;m;i.x[i])


By

---

Latex:
((RepeatFor  2  (MoveToConcl  (-1))  THEN  Unfold  `so\_apply`  0)
  THEN  Unfold  `rminimum`  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
                                THEN  Auto
                                THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
                                THEN  (OReduce  0  THENA  Auto))]
  ))

---

Home Index