---

Step * 1 2 2 of Lemma rmaximum_ub


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])
BY
{ (Subst ⌜n + (d - 1) + 1 ~ k⌝ 0⋅ THEN Auto)⋅ }

---

Latex:

---

Latex:

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]))))
6.  1  \mleq{}  d
7.  x  :  \{n..(n  +  d)  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
8.  n  \mleq{}  k
9.  k  \mleq{}  (n  +  d)
10.  \mneg{}(k  \mleq{}  (n  +  (d  -  1)))
\mvdash{}  x[k]  \mleq{}  rmax(primrec(d  -  1;x[n];\mlambda{}i,s.  rmax(s;x[n  +  i  +  1]));x[n  +  (d  -  1)  +  1])


By

---

Latex:
(Subst  \mkleeneopen{}n  +  (d  -  1)  +  1  \msim{}  k\mkleeneclose{}  0\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index