(COMMENT 
)

(VAR z  y  x)
(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))

)