---

Step * 1 1 2 of Lemma rmaximum-split

.....upcase..... 
1. n : ℤ
2. i : ℕ
3. j : ℤ
4. 0 < j
5. ∀X:{n..(n + i + (j - 1)) + 2-} ⟶ ℝ. ∀v:ℝ.
     (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]))))
⊢ ∀X:{n..(n + i + j) + 2-} ⟶ ℝ. ∀v:ℝ.
    (primrec(j;rmax(v;X[n + (0 + i) + 1]);λi1,t. rmax(t;X[n + ((i1 + 1) + i) + 1]))
    = rmax(v;primrec(j;X[(n + i) + 1];λi@0,s. rmax(s;X[((n + i) + 1) + i@0 + 1]))))
BY
{ RepeatFor 2 (ParallelLast) }

1
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])))
⊢ primrec(j;rmax(v;X[n + (0 + i) + 1]);λi1,t. rmax(t;X[n + ((i1 + 1) + i) + 1]))
= rmax(v;primrec(j;X[(n + i) + 1];λi@0,s. rmax(s;X[((n + i) + 1) + i@0 + 1])))

---

Latex:

---

Latex:
.....upcase..... 
1.  n  :  \mBbbZ{}
2.  i  :  \mBbbN{}
3.  j  :  \mBbbZ{}
4.  0  <  j
5.  \mforall{}X:\{n..(n  +  i  +  (j  -  1))  +  2\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}v:\mBbbR{}.
          (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]))))
\mvdash{}  \mforall{}X:\{n..(n  +  i  +  j)  +  2\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}v:\mBbbR{}.
        (primrec(j;rmax(v;X[n  +  (0  +  i)  +  1]);\mlambda{}i1,t.  rmax(t;X[n  +  ((i1  +  1)  +  i)  +  1]))
        =  rmax(v;primrec(j;X[(n  +  i)  +  1];\mlambda{}i@0,s.  rmax(s;X[((n  +  i)  +  1)  +  i@0  +  1]))))


By

---

Latex:
RepeatFor  2  (ParallelLast)

---

Home Index