TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60000 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (50ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (1ms), PolynomialLinearRange4iUR (405ms), DependencyGraph (1ms), PolynomialLinearRange4iUR (271ms), DependencyGraph (0ms), PolynomialLinearRange8NegiUR (3273ms), DependencyGraph (0ms), ReductionPairSAT (8676ms), DependencyGraph (1ms), SizeChangePrinciple (143ms), ForwardNarrowing (0ms), BackwardInstantiation (1ms), ForwardInstantiation (1ms), Propagation (0ms)].
| – Problem 3 was processed with processor SubtermCriterion (1ms).
| | – Problem 5 was processed with processor PolynomialLinearRange4iUR (102ms).
| – Problem 4 was processed with processor SubtermCriterion (1ms).
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| h#(e(x), y) | → | h#(d(x, y), s(y)) |
Rewrite Rules
| h(e(x), y) | → | h(d(x, y), s(y)) | | d(g(g(0, x), y), s(z)) | → | g(e(x), d(g(g(0, x), y), z)) |
| d(g(g(0, x), y), 0) | → | e(y) | | d(g(0, x), y) | → | e(x) |
| d(g(x, y), z) | → | g(d(x, z), e(y)) | | g(e(x), e(y)) | → | e(g(x, y)) |
Original Signature
Termination of terms over the following signature is verified: g, d, 0, e, s, h
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| h#(e(x), y) | → | h#(d(x, y), s(y)) | | h#(e(x), y) | → | d#(x, y) |
| d#(g(g(0, x), y), s(z)) | → | g#(e(x), d(g(g(0, x), y), z)) | | d#(g(x, y), z) | → | g#(d(x, z), e(y)) |
| d#(g(x, y), z) | → | d#(x, z) | | d#(g(g(0, x), y), s(z)) | → | d#(g(g(0, x), y), z) |
| g#(e(x), e(y)) | → | g#(x, y) | | d#(g(g(0, x), y), s(z)) | → | g#(g(0, x), y) |
| d#(g(g(0, x), y), s(z)) | → | g#(0, x) |
Rewrite Rules
| h(e(x), y) | → | h(d(x, y), s(y)) | | d(g(g(0, x), y), s(z)) | → | g(e(x), d(g(g(0, x), y), z)) |
| d(g(g(0, x), y), 0) | → | e(y) | | d(g(0, x), y) | → | e(x) |
| d(g(x, y), z) | → | g(d(x, z), e(y)) | | g(e(x), e(y)) | → | e(g(x, y)) |
Original Signature
Termination of terms over the following signature is verified: g, d, e, 0, s, h
Strategy
The following SCCs where found
| h#(e(x), y) → h#(d(x, y), s(y)) |
| d#(g(x, y), z) → d#(x, z) | d#(g(g(0, x), y), s(z)) → d#(g(g(0, x), y), z) |
| g#(e(x), e(y)) → g#(x, y) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| d#(g(x, y), z) | → | d#(x, z) | | d#(g(g(0, x), y), s(z)) | → | d#(g(g(0, x), y), z) |
Rewrite Rules
| h(e(x), y) | → | h(d(x, y), s(y)) | | d(g(g(0, x), y), s(z)) | → | g(e(x), d(g(g(0, x), y), z)) |
| d(g(g(0, x), y), 0) | → | e(y) | | d(g(0, x), y) | → | e(x) |
| d(g(x, y), z) | → | g(d(x, z), e(y)) | | g(e(x), e(y)) | → | e(g(x, y)) |
Original Signature
Termination of terms over the following signature is verified: g, d, e, 0, s, h
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| d#(g(x, y), z) | → | d#(x, z) |
Problem 5: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| d#(g(g(0, x), y), s(z)) | → | d#(g(g(0, x), y), z) |
Rewrite Rules
| h(e(x), y) | → | h(d(x, y), s(y)) | | d(g(g(0, x), y), s(z)) | → | g(e(x), d(g(g(0, x), y), z)) |
| d(g(g(0, x), y), 0) | → | e(y) | | d(g(0, x), y) | → | e(x) |
| d(g(x, y), z) | → | g(d(x, z), e(y)) | | g(e(x), e(y)) | → | e(g(x, y)) |
Original Signature
Termination of terms over the following signature is verified: g, d, 0, e, s, h
Strategy
Polynomial Interpretation
- 0: 0
- d(x,y): 0
- d#(x,y): 2y
- e(x): 3x
- g(x,y): 0
- h(x,y): 0
- s(x): 2x + 1
Improved Usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| d#(g(g(0, x), y), s(z)) | → | d#(g(g(0, x), y), z) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| g#(e(x), e(y)) | → | g#(x, y) |
Rewrite Rules
| h(e(x), y) | → | h(d(x, y), s(y)) | | d(g(g(0, x), y), s(z)) | → | g(e(x), d(g(g(0, x), y), z)) |
| d(g(g(0, x), y), 0) | → | e(y) | | d(g(0, x), y) | → | e(x) |
| d(g(x, y), z) | → | g(d(x, z), e(y)) | | g(e(x), e(y)) | → | e(g(x, y)) |
Original Signature
Termination of terms over the following signature is verified: g, d, e, 0, s, h
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| g#(e(x), e(y)) | → | g#(x, y) |