---

Step * 1 2 1 of Lemma rminimum-cases


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])))))
5. 1 ≤ d
6. x : {n..(n + d) + 1-} ⟶ ℝ
7. ¬¬(∃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]))))
⊢ ¬¬(∃a:{n..(n + d) + 1-}
      ((rmin(primrec(d - 1;x[n];λi,s. rmin(s;x[n + i + 1]));x[n + (d - 1) + 1]) = x[a])
      ∧ (∀j:{n..(n + d) + 1-}. (x[a] ≤ x[j]))))
BY
{ ((SupposeMore (-1) THENA Auto)
   THEN D -1
   THEN (StableCases ⌜x[a] < x[n + d]⌝⋅ THENA Auto)
   THEN (RemoveDoubleNegation THENA Auto)
   THEN Try ((FLemma `not-rless` [-1] THENA Auto))) }

1
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])))))
5. 1 ≤ d
6. x : {n..(n + d) + 1-} ⟶ ℝ
7. a : {n..(n + (d - 1)) + 1-}
8. (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]))
9. x[a] < x[n + d]
⊢ ∃a:{n..(n + d) + 1-}
   ((rmin(primrec(d - 1;x[n];λi,s. rmin(s;x[n + i + 1]));x[n + (d - 1) + 1]) = x[a])
   ∧ (∀j:{n..(n + d) + 1-}. (x[a] ≤ x[j])))

2
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])))))
5. 1 ≤ d
6. x : {n..(n + d) + 1-} ⟶ ℝ
7. a : {n..(n + (d - 1)) + 1-}
8. (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]))
9. ¬(x[a] < x[n + d])
10. x[n + d] ≤ x[a]
⊢ ∃a:{n..(n + d) + 1-}
   ((rmin(primrec(d - 1;x[n];λi,s. rmin(s;x[n + i + 1]));x[n + (d - 1) + 1]) = x[a])
   ∧ (∀j:{n..(n + d) + 1-}. (x[a] ≤ x[j])))

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  d  :  \mBbbZ{}
3.  0  <  d
4.  \mforall{}x:\{n..(n  +  (d  -  1))  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
          (\mneg{}\mneg{}(\mexists{}a:\{n..(n  +  (d  -  1))  +  1\msupminus{}\}
                    ((primrec(d  -  1;x[n];\mlambda{}i,s.  rmin(s;x[n  +  i  +  1]))  =  x[a])
                    \mwedge{}  (\mforall{}j:\{n..(n  +  (d  -  1))  +  1\msupminus{}\}.  (x[a]  \mleq{}  x[j])))))
5.  1  \mleq{}  d
6.  x  :  \{n..(n  +  d)  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
7.  \mneg{}\mneg{}(\mexists{}a:\{n..(n  +  (d  -  1))  +  1\msupminus{}\}
              ((primrec(d  -  1;x[n];\mlambda{}i,s.  rmin(s;x[n  +  i  +  1]))  =  x[a])
              \mwedge{}  (\mforall{}j:\{n..(n  +  (d  -  1))  +  1\msupminus{}\}.  (x[a]  \mleq{}  x[j]))))
\mvdash{}  \mneg{}\mneg{}(\mexists{}a:\{n..(n  +  d)  +  1\msupminus{}\}
            ((rmin(primrec(d  -  1;x[n];\mlambda{}i,s.  rmin(s;x[n  +  i  +  1]));x[n  +  (d  -  1)  +  1])  =  x[a])
            \mwedge{}  (\mforall{}j:\{n..(n  +  d)  +  1\msupminus{}\}.  (x[a]  \mleq{}  x[j]))))


By

---

Latex:
((SupposeMore  (-1)  THENA  Auto)
  THEN  D  -1
  THEN  (StableCases  \mkleeneopen{}x[a]  <  x[n  +  d]\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (RemoveDoubleNegation  THENA  Auto)
  THEN  Try  ((FLemma  `not-rless`  [-1]  THENA  Auto)))

---

Home Index