sqrt_derivative: THEORY
%------------------------------------------------------------------------------
%
% Derivative of sqrt function
%
% Author: David Lester (Manchester University)
%
%------------------------------------------------------------------------------

BEGIN

  IMPORTING reals@sq, reals@sqrt, derivatives
%  IMPORTING derivative_inverse

  sqrt_derivable_fun: AXIOM derivable?[posreal](sqrt)

  deriv_sqrt_fun :  AXIOM deriv[posreal](sqrt)
                             = (LAMBDA (x:posreal): 1/(2*sqrt(x)))

  deriv_sqrt     : AXIOM derivable?[posreal](sqrt) AND
                           deriv[posreal](sqrt)
                                = (LAMBDA (x:posreal): 1/(2*sqrt(x)))

  sqrt_continuous: LEMMA continuous?[posreal](sqrt)

END sqrt_derivative