(STRATEGY
    INNERMOST)

(VAR
    x y z)
(DATATYPES
    A = µX.< t, s(X), h, constant, c(X, X), m(X, X), opp(X), div(X, X), pow(X, X), 2, ln(X), 1 >)
(SIGNATURES
    D :: [A] -> A
    b :: [A x A] -> A)
(RULES
    D(t()) -> s(h())
    D(constant()) -> h()
    D(b(x,y)) -> b(D(x),D(y))
    D(c(x,y)) -> b(c(y,D(x))
                  ,c(x,D(y)))
    D(m(x,y)) -> m(D(x),D(y))
    D(opp(x)) -> opp(D(x))
    D(div(x,y)) -> m(div(D(x),y)
                    ,div(c(x,D(y)),pow(y,2())))
    D(ln(x)) -> div(D(x),x)
    D(pow(x,y)) -> b(c(c(y
                        ,pow(x,m(y,1())))
                      ,D(x))
                    ,c(c(pow(x,y),ln(x)),D(y)))
    b(h(),x) -> x
    b(x,h()) -> x
    b(s(x),s(y)) -> s(s(b(x,y)))
    b(b(x,y),z) -> b(x,b(y,z)))