MAYBE 0.08/0.18 MAYBE 0.08/0.18 0.08/0.18 Problem: 0.08/0.18 dx(X) -> one() 0.08/0.18 dx(a()) -> zero() 0.08/0.18 dx(plus(ALPHA,BETA)) -> plus(dx(ALPHA),dx(BETA)) 0.08/0.18 dx(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA))) 0.08/0.18 dx(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA)) 0.08/0.18 dx(neg(ALPHA)) -> neg(dx(ALPHA)) 0.08/0.18 dx(div(ALPHA,BETA)) -> minus(div(dx(ALPHA),BETA),times(ALPHA,div(dx(BETA),exp(BETA,two())))) 0.08/0.18 dx(ln(ALPHA)) -> div(dx(ALPHA),ALPHA) 0.08/0.18 dx(exp(ALPHA,BETA)) -> 0.08/0.18 plus(times(BETA,times(exp(ALPHA,minus(BETA,one())),dx(ALPHA))),times 0.08/0.18 (exp(ALPHA,BETA), 0.08/0.18 times 0.08/0.18 (ln(ALPHA),dx(BETA)))) 0.08/0.18 0.08/0.18 Proof: 0.08/0.18 Open 0.08/0.19 EOF