Nuprl Definition : real-cont-br

real-cont-br(a; b; f; k; N) ==

  FAN(λn,s. if primrec(n;eval v = Kleene-M(λf@0.int2nat(f cantor-to-interval(a;b;λx.if f@0 x=0 then ff else tt)

                                                        (N * k)))

                                  n
                                  (λx.if s x then 1 else 0 fi ) in
                         if v is an integer then inl v
                         else inr v ;λi,r. eval v = Kleene-M(λf@0.int2nat(f

                                                                        cantor-to-interval(a;b;λx.if f@0 x=0

                                                                                                  then ff

                                                                                                  else tt)

                                                                        (N * k)))

i

                                                  (λx.if s x then 1 else 0 fi ) in

                                         if v is an integer then ff
                                         else r)
           then tt
           else inr (λx.⋅)
           fi )

Definitions occuring in Statement : cantor-to-interval: cantor-to-interval(a;b;f), int2nat: int2nat(i), Kleene-M: Kleene-M(F), FAN: FAN(d), primrec: primrec(n;b;c), callbyvalue: callbyvalue, ifthenelse: if b then t else f fi , bfalse: ff, btrue: tt, it: ⋅, isint: isint def, int_eq: if a=b then c else d, apply: f a, lambda: λx.A[x], inr: inr x , inl: inl x, multiply: n * m, natural_number: $n
Definitions occuring in definition : FAN: FAN(d), primrec: primrec(n;b;c), inl: inl x, callbyvalue: callbyvalue, Kleene-M: Kleene-M(F), int2nat: int2nat(i), cantor-to-interval: cantor-to-interval(a;b;f), int_eq: if a=b then c else d, multiply: n * m, ifthenelse: if b then t else f fi , apply: f a, natural_number: $n, isint: isint def, bfalse: ff, btrue: tt, inr: inr x , lambda: λx.A[x], it: ⋅

Latex:
real-cont-br(a; b; f; k; N) == FAN(\mlambda{}n,s. if primrec(n;eval v = Kleene-M(\mlambda{}f@0.int2nat(f cantor-to-interval(a;b;\mlambda{}x.if f@0 x=0 then ff else tt) (N * k))) n (\mlambda{}x.if s x then 1 else 0 fi ) in if v is an integer then inl v else inr v ; \mlambda{}i,r. eval v = Kleene-M(\mlambda{}f@0.int2nat(f cantor-to-interval(a;b;\mlambda{}x.if f@0 x=0 then ff else tt) (N * k))) i (\mlambda{}x.if s x then 1 else 0 fi ) in if v is an integer then ff else r) then tt else inr (\mlambda{}x.\mcdot{}) fi ) Date html generated: 2019_10_30-AM-07_43_32 Last ObjectModification: 2019_02_07-PM-05_58_30 Theory : reals Home Index