---

Step * 1 1 of Lemma rmaximum-split


1. n : ℤ
2. i : ℕ
3. j : ℕ
4. X : {n..(n + i + j) + 2-} ⟶ ℝ
5. 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 (MoveToConcl (-1)) THEN NatInd (-1) THEN Reduce 0)⋅ }

1
1. n : ℤ
2. i : ℕ
3. j : ℤ
⊢ ∀X:{n..(n + i + 0) + 2-} ⟶ ℝ. ∀v:ℝ.  (rmax(v;X[n + (0 + i) + 1]) = rmax(v;X[(n + i) + 1]))

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

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  i  :  \mBbbN{}
3.  j  :  \mBbbN{}
4.  X  :  \{n..(n  +  i  +  j)  +  2\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
5.  v  :  \mBbbR{}
\mvdash{}  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  (MoveToConcl  (-1))  THEN  NatInd  (-1)  THEN  Reduce  0)\mcdot{}

---

Home Index