---

Step * 1 1 2 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])))
⊢ 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
{ ((RWO "primrec-unroll" 0 THENA Auto) THEN OldAutoBoolCase ⌜j <z 1⌝⋅) }

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

---

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])))
\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:
((RWO  "primrec-unroll"  0  THENA  Auto)  THEN  OldAutoBoolCase  \mkleeneopen{}j  <z  1\mkleeneclose{}\mcdot{})

---

Home Index