---

Step * of Lemma decidable__exists-unit-ball-approx-1-ext

∀k,n:ℕ.  ∀[P:unit-ball-approx(n;k) ⟶ ℙ]. ((∀p:unit-ball-approx(n;k). Dec(P[p])) ⇒ Dec(∃p:unit-ball-approx(n;k). P[p]))
BY
{ Extract of Obid: decidable__exists-unit-ball-approx-1
  not unfolding  primrec sum
  finishing with Auto
  normalizes to:
  
  λk,n. primrec(n;λ%.case % Ax of inl(%) => inl <Ax, %> | inr(%6) => inr (λ%.Ax) ;
                λi,x,%2. case x 
                              (λp.eval i' = -k in
                                  eval j' = k + 1 in
                                    letrec G(x)=if (x) < (j')
                                                   then if (k * k) < (Σ((p i) * (p i) | i < (i + 1) - 1) + (x * x))
                                                           then G (x + 1)
                                                           else case %2 
                                                                     (λi@0.if (i@0) < ((i + 1) - 1)  then p i@0  else x)
                                                                 of inl(x1) =>
                                                                 inl <x, <λ%.Ax, Ax, Ax>, x1>
                                                                 | inr(x1) =>
                                                                 G (x + 1)
                                                   else (inr (λx.Ax) ) in
                                     G(i'))
                         of inl(%3) =>
                         inl let p,z,%6,%7 = %3 
                             in <λi@0.if (i@0) < ((i + 1) - 1)  then p i@0  else z, %7>  
                         | inr(%4) =>
                         inr (λ%.Ax) ) }

---

Latex:

---

Latex:
\mforall{}k,n:\mBbbN{}.
    \mforall{}[P:unit-ball-approx(n;k)  {}\mrightarrow{}  \mBbbP{}]
        ((\mforall{}p:unit-ball-approx(n;k).  Dec(P[p]))  {}\mRightarrow{}  Dec(\mexists{}p:unit-ball-approx(n;k).  P[p]))


By

---

Latex:
Extract  of  Obid:  decidable\_\_exists-unit-ball-approx-1
not  unfolding    primrec  sum
finishing  with  Auto
normalizes  to:

\mlambda{}k,n.  primrec(n;\mlambda{}\%.case  \%  Ax  of  inl(\%)  =>  inl  <Ax,  \%>  |  inr(\%6)  =>  inr  (\mlambda{}\%.Ax)  ;
                            \mlambda{}i,x,\%2.  case  x 
                                                        (\mlambda{}p.eval  i'  =  -k  in
                                                                eval  j'  =  k  +  1  in
                                                                    letrec  G(x)=if  (x)  <  (j')
                                                                                                  then  if  (k  *  k)  <  (\mSigma{}((p  i)  *  (p  i)  |  i  <  (i  +  1) 
                                                                                                                -  1)
                                                                                                                +  (x  *  x))
                                                                                                                  then  G  (x  +  1)
                                                                                                                  else  case  \%2 
                                                                                                                                      (\mlambda{}i@0.if  (i@0)  <  ((i  +  1)  -  1)
                                                                                                                                                        then  p  i@0
                                                                                                                                                        else  x)
                                                                                                                              of  inl(x1)  =>
                                                                                                                              inl  <x,  <\mlambda{}\%.Ax,  Ax,  Ax>,  x1>
                                                                                                                              |  inr(x1)  =>
                                                                                                                              G  (x  +  1)
                                                                                                  else  (inr  (\mlambda{}x.Ax)  )  in
                                                                      G(i'))
                                              of  inl(\%3)  =>
                                              inl  let  p,z,\%6,\%7  =  \%3 
                                                      in  <\mlambda{}i@0.if  (i@0)  <  ((i  +  1)  -  1)    then  p  i@0    else  z,  \%7>   
                                              |  inr(\%4)  =>
                                              inr  (\mlambda{}\%.Ax)  )

---

Home Index