YES
The TRS could be proven terminating. The proof took 170 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (7ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (133ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| implies#(not(x), not(y)) | → | implies#(y, and(x, y)) | | implies#(false, y) | → | not#(false) |
| implies#(x, false) | → | not#(x) | | implies#(not(x), not(y)) | → | and#(x, y) |
Rewrite Rules
| and(x, false) | → | false | | and(x, not(false)) | → | x |
| not(not(x)) | → | x | | implies(false, y) | → | not(false) |
| implies(x, false) | → | not(x) | | implies(not(x), not(y)) | → | implies(y, and(x, y)) |
Original Signature
Termination of terms over the following signature is verified: not, implies, false, and
Strategy
The following SCCs where found
| implies#(not(x), not(y)) → implies#(y, and(x, y)) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| implies#(not(x), not(y)) | → | implies#(y, and(x, y)) |
Rewrite Rules
| and(x, false) | → | false | | and(x, not(false)) | → | x |
| not(not(x)) | → | x | | implies(false, y) | → | not(false) |
| implies(x, false) | → | not(x) | | implies(not(x), not(y)) | → | implies(y, and(x, y)) |
Original Signature
Termination of terms over the following signature is verified: not, implies, false, and
Strategy
Polynomial Interpretation
- and(x,y): x
- false: 0
- implies(x,y): 0
- implies#(x,y): y + x + 1
- not(x): x + 1
Improved Usable rules
| and(x, false) | → | false | | and(x, not(false)) | → | x |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| implies#(not(x), not(y)) | → | implies#(y, and(x, y)) |