YES
The TRS could be proven terminating. The proof took 412 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (315ms).
| – Problem 2 was processed with processor SubtermCriterion (25ms).
| – Problem 3 was processed with processor SubtermCriterion (1ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| D#(m(x, y)) | → | D#(x) | | D#(opp(x)) | → | D#(x) |
| D#(b(x, y)) | → | D#(x) | | D#(ln(x)) | → | D#(x) |
| b#(s(x), s(y)) | → | b#(x, y) | | D#(c(x, y)) | → | D#(x) |
| D#(pow(x, y)) | → | D#(x) | | D#(div(x, y)) | → | D#(x) |
| D#(div(x, y)) | → | D#(y) | | D#(c(x, y)) | → | b#(c(y, D(x)), c(x, D(y))) |
| D#(m(x, y)) | → | D#(y) | | D#(pow(x, y)) | → | b#(c(c(y, pow(x, m(y, 1))), D(x)), c(c(pow(x, y), ln(x)), D(y))) |
| D#(b(x, y)) | → | b#(D(x), D(y)) | | b#(b(x, y), z) | → | b#(x, b(y, z)) |
| D#(c(x, y)) | → | D#(y) | | D#(b(x, y)) | → | D#(y) |
| b#(b(x, y), z) | → | b#(y, z) | | D#(pow(x, y)) | → | D#(y) |
Rewrite Rules
| D(t) | → | s(h) | | D(constant) | → | h |
| D(b(x, y)) | → | b(D(x), D(y)) | | D(c(x, y)) | → | b(c(y, D(x)), c(x, D(y))) |
| D(m(x, y)) | → | m(D(x), D(y)) | | D(opp(x)) | → | opp(D(x)) |
| D(div(x, y)) | → | m(div(D(x), y), div(c(x, D(y)), pow(y, 2))) | | D(ln(x)) | → | div(D(x), x) |
| D(pow(x, y)) | → | b(c(c(y, pow(x, m(y, 1))), D(x)), c(c(pow(x, y), ln(x)), D(y))) | | b(h, x) | → | x |
| b(x, h) | → | x | | b(s(x), s(y)) | → | s(s(b(x, y))) |
| b(b(x, y), z) | → | b(x, b(y, z)) |
Original Signature
Termination of terms over the following signature is verified: D, ln, constant, opp, pow, b, c, div, m, h, 2, 1, t, s
Strategy
The following SCCs where found
| b#(b(x, y), z) → b#(x, b(y, z)) | b#(s(x), s(y)) → b#(x, y) |
| b#(b(x, y), z) → b#(y, z) |
| D#(opp(x)) → D#(x) | D#(m(x, y)) → D#(x) |
| D#(b(x, y)) → D#(x) | D#(ln(x)) → D#(x) |
| D#(c(x, y)) → D#(x) | D#(pow(x, y)) → D#(x) |
| D#(c(x, y)) → D#(y) | D#(div(x, y)) → D#(y) |
| D#(div(x, y)) → D#(x) | D#(b(x, y)) → D#(y) |
| D#(m(x, y)) → D#(y) | D#(pow(x, y)) → D#(y) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| b#(b(x, y), z) | → | b#(x, b(y, z)) | | b#(s(x), s(y)) | → | b#(x, y) |
| b#(b(x, y), z) | → | b#(y, z) |
Rewrite Rules
| D(t) | → | s(h) | | D(constant) | → | h |
| D(b(x, y)) | → | b(D(x), D(y)) | | D(c(x, y)) | → | b(c(y, D(x)), c(x, D(y))) |
| D(m(x, y)) | → | m(D(x), D(y)) | | D(opp(x)) | → | opp(D(x)) |
| D(div(x, y)) | → | m(div(D(x), y), div(c(x, D(y)), pow(y, 2))) | | D(ln(x)) | → | div(D(x), x) |
| D(pow(x, y)) | → | b(c(c(y, pow(x, m(y, 1))), D(x)), c(c(pow(x, y), ln(x)), D(y))) | | b(h, x) | → | x |
| b(x, h) | → | x | | b(s(x), s(y)) | → | s(s(b(x, y))) |
| b(b(x, y), z) | → | b(x, b(y, z)) |
Original Signature
Termination of terms over the following signature is verified: D, ln, constant, opp, pow, b, c, div, m, h, 2, 1, t, s
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| b#(b(x, y), z) | → | b#(x, b(y, z)) | | b#(s(x), s(y)) | → | b#(x, y) |
| b#(b(x, y), z) | → | b#(y, z) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| D#(opp(x)) | → | D#(x) | | D#(m(x, y)) | → | D#(x) |
| D#(b(x, y)) | → | D#(x) | | D#(ln(x)) | → | D#(x) |
| D#(c(x, y)) | → | D#(x) | | D#(c(x, y)) | → | D#(y) |
| D#(pow(x, y)) | → | D#(x) | | D#(div(x, y)) | → | D#(y) |
| D#(div(x, y)) | → | D#(x) | | D#(b(x, y)) | → | D#(y) |
| D#(m(x, y)) | → | D#(y) | | D#(pow(x, y)) | → | D#(y) |
Rewrite Rules
| D(t) | → | s(h) | | D(constant) | → | h |
| D(b(x, y)) | → | b(D(x), D(y)) | | D(c(x, y)) | → | b(c(y, D(x)), c(x, D(y))) |
| D(m(x, y)) | → | m(D(x), D(y)) | | D(opp(x)) | → | opp(D(x)) |
| D(div(x, y)) | → | m(div(D(x), y), div(c(x, D(y)), pow(y, 2))) | | D(ln(x)) | → | div(D(x), x) |
| D(pow(x, y)) | → | b(c(c(y, pow(x, m(y, 1))), D(x)), c(c(pow(x, y), ln(x)), D(y))) | | b(h, x) | → | x |
| b(x, h) | → | x | | b(s(x), s(y)) | → | s(s(b(x, y))) |
| b(b(x, y), z) | → | b(x, b(y, z)) |
Original Signature
Termination of terms over the following signature is verified: D, ln, constant, opp, pow, b, c, div, m, h, 2, 1, t, s
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| D#(m(x, y)) | → | D#(x) | | D#(opp(x)) | → | D#(x) |
| D#(b(x, y)) | → | D#(x) | | D#(ln(x)) | → | D#(x) |
| D#(c(x, y)) | → | D#(x) | | D#(c(x, y)) | → | D#(y) |
| D#(pow(x, y)) | → | D#(x) | | D#(div(x, y)) | → | D#(x) |
| D#(div(x, y)) | → | D#(y) | | D#(m(x, y)) | → | D#(y) |
| D#(b(x, y)) | → | D#(y) | | D#(pow(x, y)) | → | D#(y) |