---

Step * 1 1 2 1 1 of Lemma rmaximum-split


1. n : ℤ
2. i : ℕ
3. j : ℤ
4. 0 < j
5. X : {n..(n + i + j) + 2-} ⟶ ℝ
6. v : ℝ
7. primrec(j - 1;rmax(v;X[n + (0 + i) + 1]);λi1,t. rmax(t;X[n + ((i1 + 1) + i) + 1]))
= rmax(v;primrec(j - 1;X[(n + i) + 1];λi@0,s. rmax(s;X[((n + i) + 1) + i@0 + 1])))
8. 1 ≤ j
⊢ rmax(primrec(j - 1;rmax(v;X[n + (0 + i) + 1]);λi1,t. rmax(t;X[n + ((i1 + 1) + i) + 1]));X[n + (((j - 1) + 1) + i) + 1]\000C)
= rmax(v;rmax(primrec(j - 1;X[(n + i) + 1];λi@0,s. rmax(s;X[((n + i) + 1) + i@0 + 1]));X[((n + i) + 1) + (j - 1) + 1]))
BY
{ (SubstReal (-2) 0 THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  i  :  \mBbbN{}
3.  j  :  \mBbbZ{}
4.  0  <  j
5.  X  :  \{n..(n  +  i  +  j)  +  2\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
6.  v  :  \mBbbR{}
7.  primrec(j  -  1;rmax(v;X[n  +  (0  +  i)  +  1]);\mlambda{}i1,t.  rmax(t;X[n  +  ((i1  +  1)  +  i)  +  1]))
=  rmax(v;primrec(j  -  1;X[(n  +  i)  +  1];\mlambda{}i@0,s.  rmax(s;X[((n  +  i)  +  1)  +  i@0  +  1])))
8.  1  \mleq{}  j
\mvdash{}  rmax(primrec(j  -  1;rmax(v;X[n  +  (0  +  i)  +  1]);\mlambda{}i1,t.  rmax(t;X[n  +  ((i1  +  1)  +  i)  +  1]));X[n
+  (((j  -  1)  +  1)  +  i)
+  1])
=  rmax(v;rmax(primrec(j  -  1;X[(n  +  i)  +  1];\mlambda{}i@0,s.  rmax(s;X[((n  +  i)  +  1)  +  i@0  +  1]));X[((n  +  i)  +  \000C1)
    +  (j  -  1)
    +  1]))


By

---

Latex:
(SubstReal  (-2)  0  THEN  Auto)

---

Home Index