Step * 1 2 of Lemma rmaximum_ub

.....upcase..... 
1. : ℤ
2. : ℤ
3. : ℤ
4. 0 < d
5. ∀x:{n..(n (d 1)) 1-} ⟶ ℝ
     ((n ≤ k)  (k ≤ (n (d 1)))  (x[k] ≤ primrec(d 1;x[n];λi,s. rmax(s;x[n 1]))))
⊢ ∀x:{n..(n d) 1-} ⟶ ℝ((n ≤ k)  (k ≤ (n d))  (x[k] ≤ primrec(d;x[n];λi,s. rmax(s;x[n 1]))))
BY
xxx((RWO "primrec-unroll" THENA Auto)
      THEN OldAutoBoolCase ⌜d <1⌝⋅
      THEN (ParallelOp (-2))
      THEN ParallelLast
      THEN Auto
      THEN (Decide k ≤ (n (d 1)) THENA Auto)
      THEN ThinTrivial)xxx }

1
1. : ℤ
2. : ℤ
3. : ℤ
4. 0 < d
5. ∀x:{n..(n (d 1)) 1-} ⟶ ℝ
     ((n ≤ k)  (k ≤ (n (d 1)))  (x[k] ≤ primrec(d 1;x[n];λi,s. rmax(s;x[n 1]))))
6. 1 ≤ d
7. {n..(n d) 1-} ⟶ ℝ
8. n ≤ k
9. k ≤ (n d)
10. k ≤ (n (d 1))
11. x[k] ≤ primrec(d 1;x[n];λi,s. rmax(s;x[n 1]))
⊢ x[k] ≤ rmax(primrec(d 1;x[n];λi,s. rmax(s;x[n 1]));x[n (d 1) 1])

2
1. : ℤ
2. : ℤ
3. : ℤ
4. 0 < d
5. ∀x:{n..(n (d 1)) 1-} ⟶ ℝ
     ((n ≤ k)  (k ≤ (n (d 1)))  (x[k] ≤ primrec(d 1;x[n];λi,s. rmax(s;x[n 1]))))
6. 1 ≤ d
7. {n..(n d) 1-} ⟶ ℝ
8. n ≤ k
9. k ≤ (n d)
10. ¬(k ≤ (n (d 1)))
⊢ x[k] ≤ rmax(primrec(d 1;x[n];λi,s. rmax(s;x[n 1]));x[n (d 1) 1])


Latex:


Latex:
.....upcase..... 
1.  k  :  \mBbbZ{}
2.  n  :  \mBbbZ{}
3.  d  :  \mBbbZ{}
4.  0  <  d
5.  \mforall{}x:\{n..(n  +  (d  -  1))  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
          ((n  \mleq{}  k)  {}\mRightarrow{}  (k  \mleq{}  (n  +  (d  -  1)))  {}\mRightarrow{}  (x[k]  \mleq{}  primrec(d  -  1;x[n];\mlambda{}i,s.  rmax(s;x[n  +  i  +  1]))))
\mvdash{}  \mforall{}x:\{n..(n  +  d)  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
        ((n  \mleq{}  k)  {}\mRightarrow{}  (k  \mleq{}  (n  +  d))  {}\mRightarrow{}  (x[k]  \mleq{}  primrec(d;x[n];\mlambda{}i,s.  rmax(s;x[n  +  i  +  1]))))


By


Latex:
xxx((RWO  "primrec-unroll"  0  THENA  Auto)
        THEN  OldAutoBoolCase  \mkleeneopen{}d  <z  1\mkleeneclose{}\mcdot{}
        THEN  (ParallelOp  (-2))
        THEN  ParallelLast
        THEN  Auto
        THEN  (Decide  k  \mleq{}  (n  +  (d  -  1))  THENA  Auto)
        THEN  ThinTrivial)xxx




Home Index