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(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: Polynomial ordering with Polynomial interpretation:
  POL(exp(x1, x2))=  x1 + x2  
  POL(plus(x1, x2))=  1 + x1 + x2  
  POL(DX(x1))=  x1  
  POL(times(x1, x2))=  x1 + x2  
  POL(neg(x1))=  x1  
  POL(minus(x1, x2))=  x1 + x2  
  POL(div(x1, x2))=  x1 + x2  
  POL(ln(x1))=  x1  

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


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(minus(ALPHA, BETA)) -> DX(BETA)
DX(minus(ALPHA, BETA)) -> DX(ALPHA)


There are no usable rules for innermost w.r.t. to the AFS that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(exp(x1, x2))=  x1 + x2  
  POL(DX(x1))=  x1  
  POL(times(x1, x2))=  x1 + x2  
  POL(neg(x1))=  x1  
  POL(minus(x1, x2))=  1 + x1 + x2  
  POL(div(x1, x2))=  x1 + x2  
  POL(ln(x1))=  x1  

resulting in one new DP problem.
Used Argument Filtering System:
DX(x1) -> DX(x1)
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
AFS
             ...
               →DP Problem 3
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(times(ALPHA, BETA)) -> DX(BETA)
DX(times(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)


There are no usable rules for innermost w.r.t. to the AFS that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(exp(x1, x2))=  1 + x1 + x2  
  POL(DX(x1))=  x1  
  POL(times(x1, x2))=  x1 + x2  
  POL(neg(x1))=  x1  
  POL(div(x1, x2))=  x1 + x2  
  POL(ln(x1))=  x1  

resulting in one new DP problem.
Used Argument Filtering System:
DX(x1) -> DX(x1)
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
AFS
             ...
               →DP Problem 4
Argument Filtering and Ordering


Dependency Pairs:

DX(ln(ALPHA)) -> DX(ALPHA)
DX(div(ALPHA, BETA)) -> DX(BETA)
DX(div(ALPHA, BETA)) -> DX(ALPHA)
DX(neg(ALPHA)) -> DX(ALPHA)
DX(times(ALPHA, BETA)) -> DX(BETA)
DX(times(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 pair can be strictly oriented:

DX(ln(ALPHA)) -> DX(ALPHA)


There are no usable rules for innermost w.r.t. to the AFS that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(DX(x1))=  x1  
  POL(times(x1, x2))=  x1 + x2  
  POL(neg(x1))=  x1  
  POL(div(x1, x2))=  x1 + x2  
  POL(ln(x1))=  1 + x1  

resulting in one new DP problem.
Used Argument Filtering System:
DX(x1) -> DX(x1)
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
AFS
             ...
               →DP Problem 5
Argument Filtering and Ordering


Dependency Pairs:

DX(div(ALPHA, BETA)) -> DX(BETA)
DX(div(ALPHA, BETA)) -> DX(ALPHA)
DX(neg(ALPHA)) -> DX(ALPHA)
DX(times(ALPHA, BETA)) -> DX(BETA)
DX(times(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(times(ALPHA, BETA)) -> DX(BETA)
DX(times(ALPHA, BETA)) -> DX(ALPHA)


There are no usable rules for innermost w.r.t. to the AFS that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(DX(x1))=  x1  
  POL(times(x1, x2))=  1 + x1 + x2  
  POL(neg(x1))=  x1  
  POL(div(x1, x2))=  x1 + x2  

resulting in one new DP problem.
Used Argument Filtering System:
DX(x1) -> DX(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
AFS
             ...
               →DP Problem 6
Argument Filtering and Ordering


Dependency Pairs:

DX(div(ALPHA, BETA)) -> DX(BETA)
DX(div(ALPHA, BETA)) -> DX(ALPHA)
DX(neg(ALPHA)) -> 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(div(ALPHA, BETA)) -> DX(BETA)
DX(div(ALPHA, BETA)) -> DX(ALPHA)


There are no usable rules for innermost w.r.t. to the AFS that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(DX(x1))=  x1  
  POL(neg(x1))=  x1  
  POL(div(x1, x2))=  1 + x1 + x2  

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


   R
DPs
       →DP Problem 1
AFS
           →DP Problem 2
AFS
             ...
               →DP Problem 7
Argument Filtering and Ordering


Dependency Pair:

DX(neg(ALPHA)) -> 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 pair can be strictly oriented:

DX(neg(ALPHA)) -> DX(ALPHA)


There are no usable rules for innermost w.r.t. to the AFS that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(DX(x1))=  x1  
  POL(neg(x1))=  1 + x1  

resulting in one new DP problem.
Used Argument Filtering System:
DX(x1) -> DX(x1)
neg(x1) -> neg(x1)


   R
DPs
       →DP Problem 1
AFS
           →DP Problem 2
AFS
             ...
               →DP Problem 8
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:05 minutes