Nuprl Definition : q

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