Term Rewriting System R:
[X, ALPHA, BETA]
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))))

Innermost Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

DX(plus(ALPHA, BETA)) -> DX(ALPHA)
DX(plus(ALPHA, BETA)) -> DX(BETA)
DX(times(ALPHA, BETA)) -> DX(ALPHA)
DX(times(ALPHA, BETA)) -> DX(BETA)
DX(minus(ALPHA, BETA)) -> DX(ALPHA)
DX(minus(ALPHA, BETA)) -> DX(BETA)
DX(neg(ALPHA)) -> DX(ALPHA)
DX(div(ALPHA, BETA)) -> DX(ALPHA)
DX(div(ALPHA, BETA)) -> DX(BETA)
DX(ln(ALPHA)) -> DX(ALPHA)
DX(exp(ALPHA, BETA)) -> DX(ALPHA)
DX(exp(ALPHA, BETA)) -> DX(BETA)

Furthermore, R contains one SCC. 


   R
     ↳DPs
       →DP Problem 1
         ↳Argument Filtering and Ordering


Dependency Pairs:

DX(exp(ALPHA, BETA)) -> DX(BETA)
DX(exp(ALPHA, BETA)) -> DX(ALPHA)
DX(ln(ALPHA)) -> DX(ALPHA)
DX(div(ALPHA, BETA)) -> DX(BETA)
DX(div(ALPHA, BETA)) -> DX(ALPHA)
DX(neg(ALPHA)) -> DX(ALPHA)
DX(minus(ALPHA, BETA)) -> DX(BETA)
DX(minus(ALPHA, BETA)) -> DX(ALPHA)
DX(times(ALPHA, BETA)) -> DX(BETA)
DX(times(ALPHA, BETA)) -> DX(ALPHA)
DX(plus(ALPHA, BETA)) -> DX(BETA)
DX(plus(ALPHA, BETA)) -> DX(ALPHA)


Rules:


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))))


Strategy:

innermost




The following dependency pairs can be strictly oriented:

DX(exp(ALPHA, BETA)) -> DX(BETA)
DX(exp(ALPHA, BETA)) -> DX(ALPHA)
DX(ln(ALPHA)) -> DX(ALPHA)
DX(div(ALPHA, BETA)) -> DX(BETA)
DX(div(ALPHA, BETA)) -> DX(ALPHA)
DX(neg(ALPHA)) -> DX(ALPHA)
DX(minus(ALPHA, BETA)) -> DX(BETA)
DX(minus(ALPHA, BETA)) -> DX(ALPHA)
DX(times(ALPHA, BETA)) -> DX(BETA)
DX(times(ALPHA, BETA)) -> DX(ALPHA)
DX(plus(ALPHA, BETA)) -> DX(BETA)
DX(plus(ALPHA, BETA)) -> DX(ALPHA)


There are no usable rules for innermost w.r.t. to the AFS that need to be oriented.
Used ordering: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:
trivial

resulting in one new DP problem.
Used Argument Filtering System:
DX(x1) -> DX(x1)
plus(x1, x2) -> plus(x1, x2)
minus(x1, x2) -> minus(x1, x2)
exp(x1, x2) -> exp(x1, x2)
ln(x1) -> ln(x1)
times(x1, x2) -> times(x1, x2)
div(x1, x2) -> div(x1, x2)
neg(x1) -> neg(x1)


   R
     ↳DPs
       →DP Problem 1
         ↳AFS
           →DP Problem 2
             ↳Dependency Graph


Dependency Pair:


Rules:


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))))


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.

Innermost Termination of R successfully shown.
Duration:
0:00 minutes