Nuprl Definition : rneq-zero-or

rneq-zero-or(x;y) ==
  eval m = find-ge-val(λp.let a,b = p 
                          in 4 <z |a| ∨b4 <z |b|;λn.eval a = x n in
                                                    eval b = y n in
                                                      <a, b>;1) in
  let v,m1 = m 
  in let v1,v2 = v 
     in if (4) < (v1)
           then inl (inr m1 )
           else if (v1) < (-4)
                   then inl inl m1
                   else if (4) < (v2)  then inr inr m1    else if (v2) < (-4)  then inr (inl m1)   else Ax


Definitions occuring in Statement :  find-ge-val: find-ge-val(test;f;n),  bor: p ∨bq,  absval: |i|,  callbyvalue: callbyvalue,  lt_int: i <z j,  less: if (a) < (b)  then c  else d,  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  inr: inr x ,  inl: inl x,  minus: -n,  natural_number: $n,  axiom: Ax
Definitions occuring in definition :  find-ge-val: find-ge-val(test;f;n),  bor: p ∨bq,  lt_int: i <z j,  absval: |i|,  lambda: λx.A[x],  callbyvalue: callbyvalue,  apply: f a,  pair: <a, b>,  spread: spread def,  less: if (a) < (b)  then c  else d,  minus: -n,  natural_number: $n,  inr: inr x ,  inl: inl x,  axiom: Ax
FDL editor aliases :  rneq-zero-or
Latex:
rneq-zero-or(x;y)  ==
    eval  m  =  find-ge-val(\mlambda{}p.let  a,b  =  p 
                                                    in  4  <z  |a|  \mvee{}\msubb{}4  <z  |b|;\mlambda{}n.eval  a  =  x  n  in
                                                                                                        eval  b  =  y  n  in
                                                                                                            <a,  b>1)  in
    let  v,m1  =  m 
    in  let  v1,v2  =  v 
          in  if  (4)  <  (v1)
                      then  inl  (inr  m1  )
                      else  if  (v1)  <  (-4)
                                      then  inl  inl  m1
                                      else  if  (4)  <  (v2)
                                                      then  inr  inr  m1   
                                                      else  if  (v2)  <  (-4)    then  inr  (inl  m1)      else  Ax


Date html generated: 2019_10_29-AM-09_36_06
Last ObjectModification: 2019_01_09-PM-05_16_18

Theory : reals


Home Index