Proof of Nuprl Lemma : rminimum-cases

Step * 1 2 of Lemma rminimum-cases

.....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])))))

{ ((RWO "primrec-unroll" 0 THENA Auto) THEN OldAutoBoolCase ⌜d <z 1⌝⋅ THEN (ParallelOp (-2) THEN 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^-}

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

Latex:

Latex:
.....upcase..... 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]))))) \mvdash{} \mforall{}x:\{n..(n + d) + 1\msupminus{}\} {}\mrightarrow{} \mBbbR{} (\mneg{}\mneg{}(\mexists{}a:\{n..(n + d) + 1\msupminus{}\} ((primrec(d;x[n];\mlambda{}i,s. rmin(s;x[n + i + 1])) = x[a]) \mwedge{} (\mforall{}j:\{n..(n + d) + 1\msupminus{}\}. (x[a] \mleq{} x[j])\000C)))) By Latex: ((RWO "primrec-unroll" 0 THENA Auto) THEN OldAutoBoolCase \mkleeneopen{}d <z 1\mkleeneclose{}\mcdot{} THEN (ParallelOp (-2) THEN Auto)\mcdot{})\mcdot{} Home Index