---

Step * 2 of Lemma infn_wf

.....upcase..... 
1. I : {I:Interval| icompact(I)} 
2. n : ℤ
3. 0 < n
4. primrec(n - 1;λf.(f ⋅);λi,r,f. inf{r (λa.(f a++z)) | z ∈ I}) ∈ {F:{f:I^n - 1 ⟶ ℝ| 
                                                                ∀a,b:I^n - 1.  (req-vec(n - 1;a;b) ⇒ ((f a) = (f b)))} 
                                                             ⟶ ℝ| 
                                                             ∀f,g:{f:I^n - 1 ⟶ ℝ| 
                                                                   ∀a,b:I^n - 1.
                                                                     (req-vec(n - 1;a;b) ⇒ ((f a) = (f b)))} .
                                                               ((∀x:I^n - 1. ((f x) = (g x))) ⇒ ((F f) = (F g)))} 
⊢ primrec(n;λf.(f ⋅);λi,r,f. inf{r (λa.(f a++z)) | z ∈ I}) ∈ {F:{f:I^n ⟶ ℝ| ∀a,b:I^n.  (req-vec(n;a;b) ⇒ ((f a) = (f b\000C)))} 
                                                        ⟶ ℝ| 
                                                        ∀f,g:{f:I^n ⟶ ℝ| 
                                                              ∀a,b:I^n.  (req-vec(n;a;b) ⇒ ((f a) = (f b)))} .
                                                          ((∀x:I^n. ((f x) = (g x))) ⇒ ((F f) = (F g)))} 
BY
{ (((RWO  "primrec-unroll" 0 THENM OReduce 0) THENA Auto)
   THEN (GenConclTerm ⌜primrec(n - 1;λf.(f ⋅);λi,r,f. inf{r (λa.(f a++z)) | z ∈ I})⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN Thin (-2)
   THEN D -1
   THEN RenameVar `F' (-2)) }

1
1. I : {I:Interval| icompact(I)} 
2. n : ℤ
3. 0 < n
4. F : {f:I^n - 1 ⟶ ℝ| ∀a,b:I^n - 1.  (req-vec(n - 1;a;b) ⇒ ((f a) = (f b)))}  ⟶ ℝ
5. ∀f,g:{f:I^n - 1 ⟶ ℝ| ∀a,b:I^n - 1.  (req-vec(n - 1;a;b) ⇒ ((f a) = (f b)))} .
     ((∀x:I^n - 1. ((f x) = (g x))) ⇒ ((F f) = (F g)))
⊢ λf.inf{F (λa.(f a++z)) | z ∈ I} ∈ {F:{f:I^n ⟶ ℝ| ∀a,b:I^n.  (req-vec(n;a;b) ⇒ ((f a) = (f b)))}  ⟶ ℝ| 
                                     ∀f,g:{f:I^n ⟶ ℝ| ∀a,b:I^n.  (req-vec(n;a;b) ⇒ ((f a) = (f b)))} .
                                       ((∀x:I^n. ((f x) = (g x))) ⇒ ((F f) = (F g)))} 

---

Latex:

---

Latex:
.....upcase..... 
1.  I  :  \{I:Interval|  icompact(I)\} 
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  primrec(n  -  1;\mlambda{}f.(f  \mcdot{});\mlambda{}i,r,f.  inf\{r  (\mlambda{}a.(f  a++z))  |  z  \mmember{}  I\})  \mmember{}  \{F:\{f:I\^{}n  -  1  {}\mrightarrow{}  \mBbbR{}| 
                                                                                                                                \mforall{}a,b:I\^{}n  -  1.
                                                                                                                                    (req-vec(n  -  1;a;b)
                                                                                                                                    {}\mRightarrow{}  ((f  a)  =  (f  b)))\}    {}\mrightarrow{}  \mBbbR{}| 
                                                                                                                          \mforall{}f,g:\{f:I\^{}n  -  1  {}\mrightarrow{}  \mBbbR{}| 
                                                                                                                                      \mforall{}a,b:I\^{}n  -  1.
                                                                                                                                          (req-vec(n  -  1;a;b)
                                                                                                                                          {}\mRightarrow{}  ((f  a)  =  (f  b)))\}  .
                                                                                                                              ((\mforall{}x:I\^{}n  -  1.  ((f  x)  =  (g  x)))
                                                                                                                              {}\mRightarrow{}  ((F  f)  =  (F  g)))\} 
\mvdash{}  primrec(n;\mlambda{}f.(f  \mcdot{});\mlambda{}i,r,f.  inf\{r  (\mlambda{}a.(f  a++z))  |  z  \mmember{}  I\})  \mmember{}  \{F:\{f:I\^{}n  {}\mrightarrow{}  \mBbbR{}| 
                                                                                                                      \mforall{}a,b:I\^{}n.
                                                                                                                          (req-vec(n;a;b)  {}\mRightarrow{}  ((f  a)  =  (f  b)))\} 
                                                                                                                {}\mrightarrow{}  \mBbbR{}| 
                                                                                                                \mforall{}f,g:\{f:I\^{}n  {}\mrightarrow{}  \mBbbR{}| 
                                                                                                                            \mforall{}a,b:I\^{}n.
                                                                                                                                (req-vec(n;a;b)
                                                                                                                                {}\mRightarrow{}  ((f  a)  =  (f  b)))\}  .
                                                                                                                    ((\mforall{}x:I\^{}n.  ((f  x)  =  (g  x)))
                                                                                                                    {}\mRightarrow{}  ((F  f)  =  (F  g)))\} 


By

---

Latex:
(((RWO    "primrec-unroll"  0  THENM  OReduce  0)  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}primrec(n  -  1;\mlambda{}f.(f  \mcdot{});\mlambda{}i,r,f.  inf\{r  (\mlambda{}a.(f  a++z))  |  z  \mmember{}  I\})\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  Thin  (-2)
  THEN  D  -1
  THEN  RenameVar  `F'  (-2))

---

Home Index