%------------------------------------------------------------------------------
fof(abs,axiom,
    ! [X] :
      ( ( less(0,X)
      <=> abs_int(X) = X )
      & ( X = 0
      <=> abs_int(X) = 0 )
      & ( less(X,0)
      <=> abs_int(X) = $uminus_int(X) ) )   ).

fof(greater,axiom,
    ! [X,Y] :
      ( greater_int(X,Y)
    <=> $less_int(Y,X) )   ).

fof(greater_or_equal,axiom,
    ! [X,Y] :
      ( greatereq_int(X,Y)
    <=> $lesseq_int(Y,X) )   ).

fof(succ,axiom,
    ! [X] : succ_int(X) = $plus_int(X,1)   ).

fof(pred,axiom,
    ! [X] : pred_int(X) = $minus_int(X,1)   ).

%----This is broken - case 0^0
fof(power,axiom,
    ! [B,E,R] :
      ( power_int(B,0) = 1
      & ( $less_int(0,E)
       => power_int(B,E) = $times_int(B,power_int(B,$minus_int(E,1))) )
      & ( $less_int(E,0)
       => power_int(B,E) = $divided_by(1,power_int(B,$uminus_int(E))) )   ).

%------------------------------------------------------------------------------