Step
*
1
2
of Lemma
rmaximum_ub
.....upcase.....
1. k : ℤ
2. n : ℤ
3. d : ℤ
4. 0 < d
5. ∀x:{n..(n + (d - 1)) + 1-} ⟶ ℝ
((n ≤ k)
⇒ (k ≤ (n + (d - 1)))
⇒ (x[k] ≤ primrec(d - 1;x[n];λi,s. rmax(s;x[n + i + 1]))))
⊢ ∀x:{n..(n + d) + 1-} ⟶ ℝ. ((n ≤ k)
⇒ (k ≤ (n + d))
⇒ (x[k] ≤ primrec(d;x[n];λi,s. rmax(s;x[n + i + 1]))))
BY
{ xxx((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)xxx }
1
1. k : ℤ
2. n : ℤ
3. d : ℤ
4. 0 < d
5. ∀x:{n..(n + (d - 1)) + 1-} ⟶ ℝ
((n ≤ k)
⇒ (k ≤ (n + (d - 1)))
⇒ (x[k] ≤ primrec(d - 1;x[n];λi,s. rmax(s;x[n + i + 1]))))
6. 1 ≤ d
7. x : {n..(n + d) + 1-} ⟶ ℝ
8. n ≤ k
9. k ≤ (n + d)
10. k ≤ (n + (d - 1))
11. x[k] ≤ primrec(d - 1;x[n];λi,s. rmax(s;x[n + i + 1]))
⊢ x[k] ≤ rmax(primrec(d - 1;x[n];λi,s. rmax(s;x[n + i + 1]));x[n + (d - 1) + 1])
2
1. k : ℤ
2. n : ℤ
3. d : ℤ
4. 0 < d
5. ∀x:{n..(n + (d - 1)) + 1-} ⟶ ℝ
((n ≤ k)
⇒ (k ≤ (n + (d - 1)))
⇒ (x[k] ≤ primrec(d - 1;x[n];λi,s. rmax(s;x[n + i + 1]))))
6. 1 ≤ d
7. x : {n..(n + d) + 1-} ⟶ ℝ
8. n ≤ k
9. k ≤ (n + d)
10. ¬(k ≤ (n + (d - 1)))
⊢ x[k] ≤ rmax(primrec(d - 1;x[n];λi,s. rmax(s;x[n + i + 1]));x[n + (d - 1) + 1])
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{} (x[k] \mleq{} primrec(d - 1;x[n];\mlambda{}i,s. rmax(s;x[n + i + 1]))))
\mvdash{} \mforall{}x:\{n..(n + d) + 1\msupminus{}\} {}\mrightarrow{} \mBbbR{}
((n \mleq{} k) {}\mRightarrow{} (k \mleq{} (n + d)) {}\mRightarrow{} (x[k] \mleq{} primrec(d;x[n];\mlambda{}i,s. rmax(s;x[n + i + 1]))))
By
Latex:
xxx((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)xxx
Home
Index