The rewrite relation of the following equational TRS is considered.
| dx(X) | → | 1 | (1) |
| dx(0) | → | 0 | (2) |
| dx(1) | → | 0 | (3) |
| dx(a) | → | 0 | (4) |
| dx(+(f,g)) | → | +(dx(f),dx(g)) | (5) |
| dx(*(f,g)) | → | +(*(dx(f),g),*(dx(g),f)) | (6) |
| dx(-(f,g)) | → | -(dx(f),dx(g)) | (7) |
| dx(neg(f)) | → | neg(dx(f)) | (8) |
| dx(/(f,g)) | → | -(/(dx(f),g),/(*(dx(g),f),exp(g,2))) | (9) |
| dx(ln(f)) | → | /(dx(f),f) | (10) |
| dx(exp(f,g)) | → | +(*(dx(f),*(exp(f,-(g,1)),g)),*(dx(g),*(exp(f,g),ln(f)))) | (11) |
Associative symbols: +, *
Commutative symbols: +, *
The following set of (strict) dependency pairs is constructed for the TRS.
| dx#(*(f,g)) | → | dx#(g) | (16) |
| dx#(exp(f,g)) | → | dx#(g) | (17) |
| dx#(ln(f)) | → | dx#(f) | (18) |
| dx#(+(f,g)) | → | dx#(g) | (19) |
| dx#(neg(f)) | → | dx#(f) | (20) |
| dx#(-(f,g)) | → | dx#(f) | (21) |
| dx#(+(f,g)) | → | dx#(f) | (22) |
| dx#(exp(f,g)) | → | dx#(f) | (23) |
| dx#(/(f,g)) | → | dx#(f) | (24) |
| dx#(*(f,g)) | → | dx#(f) | (25) |
| dx#(-(f,g)) | → | dx#(g) | (26) |
| dx#(/(f,g)) | → | dx#(g) | (27) |
The dependency pairs are split into 1 component.
| dx#(/(f,g)) | → | dx#(g) | (27) |
| dx#(neg(f)) | → | dx#(f) | (20) |
| dx#(-(f,g)) | → | dx#(g) | (26) |
| dx#(*(f,g)) | → | dx#(f) | (25) |
| dx#(/(f,g)) | → | dx#(f) | (24) |
| dx#(+(f,g)) | → | dx#(g) | (19) |
| dx#(ln(f)) | → | dx#(f) | (18) |
| dx#(exp(f,g)) | → | dx#(g) | (17) |
| dx#(exp(f,g)) | → | dx#(f) | (23) |
| dx#(+(f,g)) | → | dx#(f) | (22) |
| dx#(-(f,g)) | → | dx#(f) | (21) |
| dx#(*(f,g)) | → | dx#(g) | (16) |
| [a] | = | 0 |
| [1] | = | 0 |
| [ln(x1)] | = | x1 + 1 |
| [/(x1, x2)] | = | x1 + x2 + 1 |
| [dx#(x1)] | = | x1 + 0 |
| [dx(x1)] | = | 0 |
| [0] | = | 0 |
| [-(x1, x2)] | = | x1 + x2 + 1 |
| [neg(x1)] | = | x1 + 1 |
| [2] | = | 0 |
| [exp(x1, x2)] | = | x1 + x2 + 1 |
| [+(x1, x2)] | = | x1 + x2 + 1 |
| [X] | = | 0 |
| [*(x1, x2)] | = | x1 + x2 + 1 |
| dx#(*(f,g)) | → | dx#(g) | (16) |
| dx#(-(f,g)) | → | dx#(f) | (21) |
| dx#(+(f,g)) | → | dx#(f) | (22) |
| dx#(exp(f,g)) | → | dx#(f) | (23) |
| dx#(exp(f,g)) | → | dx#(g) | (17) |
| dx#(ln(f)) | → | dx#(f) | (18) |
| dx#(+(f,g)) | → | dx#(g) | (19) |
| dx#(/(f,g)) | → | dx#(f) | (24) |
| dx#(*(f,g)) | → | dx#(f) | (25) |
| dx#(-(f,g)) | → | dx#(g) | (26) |
| dx#(neg(f)) | → | dx#(f) | (20) |
| dx#(/(f,g)) | → | dx#(g) | (27) |
The dependency pairs are split into 0 components.