Nuprl Definition : q_less
q_less(r;s) ==
  if isint(r)
  then if isint(s) then r <z s else let i,j = s in if 0 <z j then j * r <z i else i <z j * r fi  fi 
  else let p,q = r 
       in if isint(s)
          then if 0 <z q then p <z q * s else q * s <z p fi 
          else let i,j = s 
               in if 0 <z q * j then j * p <z q * i else q * i <z j * p fi 
          fi 
  fi 
Definitions occuring in Statement : 
ifthenelse: if b then t else f fi 
, 
lt_int: i <z j
, 
bfalse: ff
, 
btrue: tt
, 
isint: isint def, 
spread: spread def, 
multiply: n * m
, 
natural_number: $n
Definitions occuring in definition : 
isint: isint def, 
btrue: tt
, 
bfalse: ff
, 
spread: spread def, 
ifthenelse: if b then t else f fi 
, 
natural_number: $n
, 
lt_int: i <z j
, 
multiply: n * m
FDL editor aliases : 
q_less
Latex:
q\_less(r;s)  ==
    if  isint(r)
    then  if  isint(s)  then  r  <z  s  else  let  i,j  =  s  in  if  0  <z  j  then  j  *  r  <z  i  else  i  <z  j  *  r  fi    fi 
    else  let  p,q  =  r 
              in  if  isint(s)
                    then  if  0  <z  q  then  p  <z  q  *  s  else  q  *  s  <z  p  fi 
                    else  let  i,j  =  s 
                              in  if  0  <z  q  *  j  then  j  *  p  <z  q  *  i  else  q  *  i  <z  j  *  p  fi 
                    fi 
    fi 
Date html generated:
2016_05_15-PM-10_57_19
Last ObjectModification:
2015_09_23-AM-08_27_23
Theory : rationals
Home
Index