YES TRS: dx(X) -> one() dx(a()) -> zero() dx(plus(ALPHA,BETA)) -> plus(dx(ALPHA),dx(BETA)) dx(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA))) dx(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA)) dx(neg(ALPHA)) -> neg(dx(ALPHA)) dx(div(ALPHA,BETA)) -> minus(div(dx(ALPHA),BETA),times(ALPHA,div(dx(BETA),exp(BETA,two())))) dx(ln(ALPHA)) -> div(dx(ALPHA),ALPHA) dx(exp(ALPHA,BETA)) -> plus(times(BETA,times(exp(ALPHA,minus(BETA,one())),dx(ALPHA))),times(exp(ALPHA,BETA),times(ln(ALPHA),dx(BETA)))) max/plus interpretations on N: dx_A(x1) = max{80, 79 + x1} dx#_A(x1) = max{5, -18 + x1} one_A = 1 one#_A = 4 a_A = 2 a#_A = 1 zero_A = 81 zero#_A = 0 plus_A(x1,x2) = max{51, 12 + x1, x2} plus#_A(x1,x2) = max{33, 33, -19} times_A(x1,x2) = max{294, 15 + x1, 2 + x2} times#_A(x1,x2) = max{211, -3, -17} minus_A(x1,x2) = max{176, x1, 25 + x2} minus#_A(x1,x2) = max{6, -20, -19} neg_A(x1) = max{81, x1} neg#_A(x1) = max{5, 5} div_A(x1,x2) = max{273, 16 + x1, 96 + x2} div#_A(x1,x2) = max{1, -1, -1} exp_A(x1,x2) = max{229, 52 + x1, 103 + x2} exp#_A(x1,x2) = max{2, 3 + x1, 7 + x2} two_A = 1 two#_A = 0 ln_A(x1) = max{194, 18 + x1} ln#_A(x1) = max{4, 4} precedence: div > neg = exp > dx > one = a = times = minus = two = ln > zero = plus