---

Step * 1 2 of Lemma rminimum_lb

.....upcase..... 
1. k : ℤ
2. n : ℤ
3. d : ℤ
4. 0 < d
5. ∀x:{n..(n + (d - 1)) + 1-} ⟶ ℝ
     ((n ≤ k) ⇒ (k ≤ (n + (d - 1))) ⇒ (primrec(d - 1;x[n];λi,s. rmin(s;x[n + i + 1])) ≤ x[k]))
⊢ ∀x:{n..(n + d) + 1-} ⟶ ℝ. ((n ≤ k) ⇒ (k ≤ (n + d)) ⇒ (primrec(d;x[n];λi,s. rmin(s;x[n + i + 1])) ≤ x[k]))
BY
{ ((RWO "primrec-unroll" 0 THENA Auto)
   THEN OldAutoBoolCase ⌜d <z 1⌝⋅
   THEN (ParallelOp (-2))
   THEN ParallelLast
   THEN Auto
   THEN (Decide k ≤ (n + (d - 1)) THENA Auto)
   THEN ThinTrivial) }

1
1. k : ℤ
2. n : ℤ
3. d : ℤ
4. 0 < d
5. ∀x:{n..(n + (d - 1)) + 1-} ⟶ ℝ
     ((n ≤ k) ⇒ (k ≤ (n + (d - 1))) ⇒ (primrec(d - 1;x[n];λi,s. rmin(s;x[n + i + 1])) ≤ x[k]))
6. 1 ≤ d
7. x : {n..(n + d) + 1-} ⟶ ℝ
8. n ≤ k
9. k ≤ (n + d)
10. k ≤ (n + (d - 1))
11. primrec(d - 1;x[n];λi,s. rmin(s;x[n + i + 1])) ≤ x[k]
⊢ rmin(primrec(d - 1;x[n];λi,s. rmin(s;x[n + i + 1]));x[n + (d - 1) + 1]) ≤ x[k]

2
1. k : ℤ
2. n : ℤ
3. d : ℤ
4. 0 < d
5. ∀x:{n..(n + (d - 1)) + 1-} ⟶ ℝ
     ((n ≤ k) ⇒ (k ≤ (n + (d - 1))) ⇒ (primrec(d - 1;x[n];λi,s. rmin(s;x[n + i + 1])) ≤ x[k]))
6. 1 ≤ d
7. x : {n..(n + d) + 1-} ⟶ ℝ
8. n ≤ k
9. k ≤ (n + d)
10. ¬(k ≤ (n + (d - 1)))
⊢ rmin(primrec(d - 1;x[n];λi,s. rmin(s;x[n + i + 1]));x[n + (d - 1) + 1]) ≤ x[k]

---

Latex:

---

Latex:
.....upcase..... 
1.  k  :  \mBbbZ{}
2.  n  :  \mBbbZ{}
3.  d  :  \mBbbZ{}
4.  0  <  d
5.  \mforall{}x:\{n..(n  +  (d  -  1))  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
          ((n  \mleq{}  k)  {}\mRightarrow{}  (k  \mleq{}  (n  +  (d  -  1)))  {}\mRightarrow{}  (primrec(d  -  1;x[n];\mlambda{}i,s.  rmin(s;x[n  +  i  +  1]))  \mleq{}  x[k]))
\mvdash{}  \mforall{}x:\{n..(n  +  d)  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
        ((n  \mleq{}  k)  {}\mRightarrow{}  (k  \mleq{}  (n  +  d))  {}\mRightarrow{}  (primrec(d;x[n];\mlambda{}i,s.  rmin(s;x[n  +  i  +  1]))  \mleq{}  x[k]))


By

---

Latex:
((RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  OldAutoBoolCase  \mkleeneopen{}d  <z  1\mkleeneclose{}\mcdot{}
  THEN  (ParallelOp  (-2))
  THEN  ParallelLast
  THEN  Auto
  THEN  (Decide  k  \mleq{}  (n  +  (d  -  1))  THENA  Auto)
  THEN  ThinTrivial)

---

Home Index