---

Step * 1 of Lemma rminimum-cases


1. n : ℤ
2. m : ℤ
3. n ≤ m
⊢ ∀x:{n..m + 1-} ⟶ ℝ. (¬¬(∃a:{n..m + 1-}. ((rminimum(n;m;i.x[i]) = x[a]) ∧ (∀j:{n..m + 1-}. (x[a] ≤ x[j])))))
BY
{ (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)])) }

1
1. n : ℤ
2. d : ℤ
⊢ ∀x:{n..(n + 0) + 1-} ⟶ ℝ. (¬¬(∃a:{n..(n + 0) + 1-}. ((x[n] = x[a]) ∧ (∀j:{n..(n + 0) + 1-}. (x[a] ≤ x[j])))))

2
.....upcase..... 
1. n : ℤ
2. d : ℤ
3. 0 < d
4. ∀x:{n..(n + (d - 1)) + 1-} ⟶ ℝ
     (¬¬(∃a:{n..(n + (d - 1)) + 1-}
          ((primrec(d - 1;x[n];λi,s. rmin(s;x[n + i + 1])) = x[a]) ∧ (∀j:{n..(n + (d - 1)) + 1-}. (x[a] ≤ x[j])))))
⊢ ∀x:{n..(n + d) + 1-} ⟶ ℝ
    (¬¬(∃a:{n..(n + d) + 1-}
         ((primrec(d;x[n];λi,s. rmin(s;x[n + i + 1])) = x[a]) ∧ (∀j:{n..(n + d) + 1-}. (x[a] ≤ x[j])))))

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  m  :  \mBbbZ{}
3.  n  \mleq{}  m
\mvdash{}  \mforall{}x:\{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
        (\mneg{}\mneg{}(\mexists{}a:\{n..m  +  1\msupminus{}\}.  ((rminimum(n;m;i.x[i])  =  x[a])  \mwedge{}  (\mforall{}j:\{n..m  +  1\msupminus{}\}.  (x[a]  \mleq{}  x[j])))))


By

---

Latex:
(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)]))

---

Home Index