(STRATEGY
    INNERMOST)

(VAR
    x y)
(DATATYPES
    A = µX.< t, 1, constant, 0, +(X, X), *(X, X), -(X, X), minus(X), div(X, X), pow(X, X), 2, ln(X) >)
(SIGNATURES
    D :: [A] -> A)
(RULES
    D(t()) -> 1()
    D(constant()) -> 0()
    D(+(x,y)) -> +(D(x),D(y))
    D(*(x,y)) -> +(*(y,D(x))
                  ,*(x,D(y)))
    D(-(x,y)) -> -(D(x),D(y))
    D(minus(x)) -> minus(D(x))
    D(div(x,y)) -> -(div(D(x),y)
                    ,div(*(x,D(y)),pow(y,2())))
    D(ln(x)) -> div(D(x),x)
    D(pow(x,y)) -> +(*(*(y
                        ,pow(x,-(y,1())))
                      ,D(x))
                    ,*(*(pow(x,y),ln(x)),D(y))))