YES
The TRS could be proven terminating. The proof took 118 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (7ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (59ms).
| | – Problem 3 was processed with processor DependencyGraph (1ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| a__g#(X) | → | a__h#(X) | | mark#(c) | → | a__c# |
| a__h#(d) | → | a__g#(c) | | mark#(g(X)) | → | a__g#(X) |
| mark#(h(X)) | → | a__h#(X) |
Rewrite Rules
| a__g(X) | → | a__h(X) | | a__c | → | d |
| a__h(d) | → | a__g(c) | | mark(g(X)) | → | a__g(X) |
| mark(h(X)) | → | a__h(X) | | mark(c) | → | a__c |
| mark(d) | → | d | | a__g(X) | → | g(X) |
| a__h(X) | → | h(X) | | a__c | → | c |
Original Signature
Termination of terms over the following signature is verified: g, d, c, a__c, mark, a__h, a__g, h
Strategy
The following SCCs where found
| a__g#(X) → a__h#(X) | a__h#(d) → a__g#(c) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| a__g#(X) | → | a__h#(X) | | a__h#(d) | → | a__g#(c) |
Rewrite Rules
| a__g(X) | → | a__h(X) | | a__c | → | d |
| a__h(d) | → | a__g(c) | | mark(g(X)) | → | a__g(X) |
| mark(h(X)) | → | a__h(X) | | mark(c) | → | a__c |
| mark(d) | → | d | | a__g(X) | → | g(X) |
| a__h(X) | → | h(X) | | a__c | → | c |
Original Signature
Termination of terms over the following signature is verified: g, d, c, a__c, mark, a__h, a__g, h
Strategy
Polynomial Interpretation
- a__c: 0
- a__g(x): 0
- a__g#(x): x + 1
- a__h(x): 0
- a__h#(x): x + 1
- c: 0
- d: 2
- g(x): 0
- h(x): 0
- mark(x): 0
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
Problem 3: DependencyGraph
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| a__g(X) | → | a__h(X) | | a__c | → | d |
| a__h(d) | → | a__g(c) | | mark(g(X)) | → | a__g(X) |
| mark(h(X)) | → | a__h(X) | | mark(c) | → | a__c |
| mark(d) | → | d | | a__g(X) | → | g(X) |
| a__h(X) | → | h(X) | | a__c | → | c |
Original Signature
Termination of terms over the following signature is verified: g, d, c, a__c, mark, a__h, a__g, h
Strategy
There are no SCCs!