---

Step * 1 of Lemma rmaximum-split


1. n : ℤ
2. m : ℤ
3. x : {n..m + 1-} ⟶ ℝ
4. k : ℤ
5. n ≤ k
6. k < m
7. i : ℕ
8. (k - n) = i ∈ ℕ
9. j : ℕ
10. (m - k + 1) = j ∈ ℕ
11. X : {n..(n + i + j) + 2-} ⟶ ℝ
12. x = X ∈ ({n..(n + i + j) + 2-} ⟶ ℝ)
⊢ primrec((j + 1) + i;X[n];λi,s. rmax(s;X[n + i + 1]))
= rmax(primrec(i;X[n];λi,s. rmax(s;X[n + i + 1]));primrec(j;X[(n + i) + 1];λi@0,s. rmax(s;X[((n + i) + 1) + i@0 + 1])))
BY
{ ((RWO "primrec_add" 0 THENA Auto')
   THEN Reduce 0
   THEN (RWO "primrec_add" 0 THENA Auto')
   THEN (Reduce 0 THEN Try ((DoSubsume THEN Auto)))
   THEN (((GenConclAtAddrType ⌜ℝ⌝ [2; 1])⋅ THENA (Auto THEN Auto'))
         THEN ThinVar `k'
         THEN ThinVar `x'
         THEN ThinVar `m'
         THEN Thin (-1))⋅) }

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

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  m  :  \mBbbZ{}
3.  x  :  \{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
4.  k  :  \mBbbZ{}
5.  n  \mleq{}  k
6.  k  <  m
7.  i  :  \mBbbN{}
8.  (k  -  n)  =  i
9.  j  :  \mBbbN{}
10.  (m  -  k  +  1)  =  j
11.  X  :  \{n..(n  +  i  +  j)  +  2\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
12.  x  =  X
\mvdash{}  primrec((j  +  1)  +  i;X[n];\mlambda{}i,s.  rmax(s;X[n  +  i  +  1]))
=  rmax(primrec(i;X[n];\mlambda{}i,s.  rmax(s;X[n  +  i  +  1]));primrec(j;X[(n  +  i)  +  1];
                                                                                                            \mlambda{}i@0,s.  rmax(s;X[((n  +  i)  +  1)  +  i@0  +  1])))


By

---

Latex:
((RWO  "primrec\_add"  0  THENA  Auto')
  THEN  Reduce  0
  THEN  (RWO  "primrec\_add"  0  THENA  Auto')
  THEN  (Reduce  0  THEN  Try  ((DoSubsume  THEN  Auto)))
  THEN  (((GenConclAtAddrType  \mkleeneopen{}\mBbbR{}\mkleeneclose{}  [2;  1])\mcdot{}  THENA  (Auto  THEN  Auto'))
              THEN  ThinVar  `k'
              THEN  ThinVar  `x'
              THEN  ThinVar  `m'
              THEN  Thin  (-1))\mcdot{})

---

Home Index