Nuprl Definition : find-real-neq

find-real-neq(a;b) ==
  eval in
  eval in
    mu-ge-print(λn.eval xn in
                   eval yn in
                   eval xn yn in
                     1 <|d|;0)



Definitions occuring in Statement :  mu-ge-print: mu-ge-print(f;n) absval: |i| callbyvalue: callbyvalue lt_int: i <j apply: a lambda: λx.A[x] subtract: m natural_number: $n
Definitions occuring in definition :  mu-ge-print: mu-ge-print(f;n) lambda: λx.A[x] apply: a callbyvalue: callbyvalue subtract: m lt_int: i <j absval: |i| natural_number: $n
FDL editor aliases :  find-real-neq

Latex:
find-real-neq(a;b)  ==
    eval  x  =  a  in
    eval  y  =  b  in
        mu-ge-print(\mlambda{}n.eval  xn  =  x  n  in
                                      eval  yn  =  y  n  in
                                      eval  d  =  xn  -  yn  in
                                          1  <z  |d|;0)



Date html generated: 2016_05_18-AM-09_35_23
Last ObjectModification: 2015_09_23-AM-09_11_46

Theory : reals


Home Index