YES
The TRS could be proven terminating. The proof took 37 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (23ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor SubtermCriterion (4ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| g#(h2(x, y, h1(z, u))) | → | h2#(s(x), y, h1(z, u)) | | f#(x, h1(y, z)) | → | h2#(0, x, h1(y, z)) |
| f#(j(x, y), y) | → | f#(x, k(y)) | | f#(j(x, y), y) | → | k#(y) |
| h2#(x, j(y, h1(z, u)), h1(z, u)) | → | h2#(s(x), y, h1(s(z), u)) | | f#(j(x, y), y) | → | g#(f(x, k(y))) |
Rewrite Rules
| f(j(x, y), y) | → | g(f(x, k(y))) | | f(x, h1(y, z)) | → | h2(0, x, h1(y, z)) |
| g(h2(x, y, h1(z, u))) | → | h2(s(x), y, h1(z, u)) | | h2(x, j(y, h1(z, u)), h1(z, u)) | → | h2(s(x), y, h1(s(z), u)) |
| i(f(x, h(y))) | → | y | | i(h2(s(x), y, h1(x, z))) | → | z |
| k(h(x)) | → | h1(0, x) | | k(h1(x, y)) | → | h1(s(x), y) |
Original Signature
Termination of terms over the following signature is verified: f, g, 0, s, j, h1, k, h, h2, i
Strategy
The following SCCs where found
| f#(j(x, y), y) → f#(x, k(y)) |
| h2#(x, j(y, h1(z, u)), h1(z, u)) → h2#(s(x), y, h1(s(z), u)) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| h2#(x, j(y, h1(z, u)), h1(z, u)) | → | h2#(s(x), y, h1(s(z), u)) |
Rewrite Rules
| f(j(x, y), y) | → | g(f(x, k(y))) | | f(x, h1(y, z)) | → | h2(0, x, h1(y, z)) |
| g(h2(x, y, h1(z, u))) | → | h2(s(x), y, h1(z, u)) | | h2(x, j(y, h1(z, u)), h1(z, u)) | → | h2(s(x), y, h1(s(z), u)) |
| i(f(x, h(y))) | → | y | | i(h2(s(x), y, h1(x, z))) | → | z |
| k(h(x)) | → | h1(0, x) | | k(h1(x, y)) | → | h1(s(x), y) |
Original Signature
Termination of terms over the following signature is verified: f, g, 0, s, j, h1, k, h, h2, i
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| h2#(x, j(y, h1(z, u)), h1(z, u)) | → | h2#(s(x), y, h1(s(z), u)) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| f#(j(x, y), y) | → | f#(x, k(y)) |
Rewrite Rules
| f(j(x, y), y) | → | g(f(x, k(y))) | | f(x, h1(y, z)) | → | h2(0, x, h1(y, z)) |
| g(h2(x, y, h1(z, u))) | → | h2(s(x), y, h1(z, u)) | | h2(x, j(y, h1(z, u)), h1(z, u)) | → | h2(s(x), y, h1(s(z), u)) |
| i(f(x, h(y))) | → | y | | i(h2(s(x), y, h1(x, z))) | → | z |
| k(h(x)) | → | h1(0, x) | | k(h1(x, y)) | → | h1(s(x), y) |
Original Signature
Termination of terms over the following signature is verified: f, g, 0, s, j, h1, k, h, h2, i
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| f#(j(x, y), y) | → | f#(x, k(y)) |