Nuprl Definition : unit-ball-ex-decider

unit-ball-ex-decider(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) )


Definitions occuring in Statement :  sum: Σ(f[x] | x < k),  genrec-ap: genrec-ap,  primrec: primrec(n;b;c),  callbyvalue: callbyvalue,  spreadn: spread4,  less: if (a) < (b)  then c  else d,  apply: f a,  lambda: λx.A[x],  pair: <a, b>,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inr: inr x ,  inl: inl x,  multiply: n * m,  subtract: n - m,  add: n + m,  minus: -n,  natural_number: $n,  axiom: Ax
Definitions occuring in definition :  primrec: primrec(n;b;c),  minus: -n,  callbyvalue: callbyvalue,  genrec-ap: genrec-ap,  sum: Σ(f[x] | x < k),  multiply: n * m,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inl: inl x,  spreadn: spread4,  pair: <a, b>,  less: if (a) < (b)  then c  else d,  subtract: n - m,  add: n + m,  natural_number: $n,  apply: f a,  inr: inr x ,  lambda: λx.A[x],  axiom: Ax
FDL editor aliases :  unit-ball-ex-decider
Latex:
unit-ball-ex-decider(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)  )


Date html generated: 2019_10_30-AM-11_28_27
Last ObjectModification: 2019_07_30-AM-11_31_07

Theory : real!vectors


Home Index