Consider the TRS R consisting of the rewrite rules 1: dx(X) -> one 2: dx(a) -> zero 3: dx(plus(ALPHA,BETA)) -> plus(dx(ALPHA),dx(BETA)) 4: dx(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA))) 5: dx(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA)) 6: dx(neg(ALPHA)) -> neg(dx(ALPHA)) 7: dx(div(ALPHA,BETA)) -> minus(div(dx(ALPHA),BETA),times(ALPHA,div(dx(BETA),exp(BETA,two)))) 8: dx(ln(ALPHA)) -> div(dx(ALPHA),ALPHA) 9: dx(exp(ALPHA,BETA)) -> plus(times(BETA,times(exp(ALPHA,minus(BETA,one)),dx(ALPHA))),times(exp(ALPHA,BETA),times(ln(ALPHA),dx(BETA)))) There are 12 dependency pairs: 10: DX(plus(ALPHA,BETA)) -> DX(ALPHA) 11: DX(plus(ALPHA,BETA)) -> DX(BETA) 12: DX(times(ALPHA,BETA)) -> DX(ALPHA) 13: DX(times(ALPHA,BETA)) -> DX(BETA) 14: DX(minus(ALPHA,BETA)) -> DX(ALPHA) 15: DX(minus(ALPHA,BETA)) -> DX(BETA) 16: DX(neg(ALPHA)) -> DX(ALPHA) 17: DX(div(ALPHA,BETA)) -> DX(ALPHA) 18: DX(div(ALPHA,BETA)) -> DX(BETA) 19: DX(ln(ALPHA)) -> DX(ALPHA) 20: DX(exp(ALPHA,BETA)) -> DX(ALPHA) 21: DX(exp(ALPHA,BETA)) -> DX(BETA) The approximated dependency graph contains one SCC: {10-21}. - Consider the SCC {10-21}. There are no usable rules. By taking the polynomial interpretation [DX](x) = [ln](x) = [neg](x) = x + 1 and [div](x,y) = [exp](x,y) = [minus](x,y) = [plus](x,y) = [times](x,y) = x + y + 1, the rules in {10-21} are strictly decreasing. Hence the TRS is terminating.