YES
The TRS could be proven terminating. The proof took 4688 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (56ms).
| – Problem 2 was processed with processor SubtermCriterion (3ms).
| – Problem 3 was processed with processor SubtermCriterion (2ms).
| – Problem 4 was processed with processor PolynomialLinearRange4iUR (441ms).
| | – Problem 5 was processed with processor ReductionPairSAT (460ms).
| | | – Problem 6 was processed with processor ReductionPairSAT (543ms).
| | | | – Problem 7 was processed with processor ReductionPairSAT (466ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| plus#(s(x), y) | → | double#(y) | | plus#(s(x), y) | → | plus#(x, y) |
| plus#(s(x), y) | → | minus#(x, y) | | plus#(s(plus(x, y)), z) | → | plus#(plus(x, y), z) |
| minus#(s(x), s(y)) | → | minus#(x, y) | | double#(s(x)) | → | double#(x) |
| plus#(s(plus(x, y)), z) | → | plus#(x, y) | | plus#(s(x), y) | → | plus#(minus(x, y), double(y)) |
| plus#(s(x), y) | → | plus#(x, s(y)) |
Rewrite Rules
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| double(0) | → | 0 | | double(s(x)) | → | s(s(double(x))) |
| plus(0, y) | → | y | | plus(s(x), y) | → | s(plus(x, y)) |
| plus(s(x), y) | → | plus(x, s(y)) | | plus(s(x), y) | → | s(plus(minus(x, y), double(y))) |
| plus(s(plus(x, y)), z) | → | s(plus(plus(x, y), z)) |
Original Signature
Termination of terms over the following signature is verified: plus, minus, 0, s, double
Strategy
The following SCCs where found
| plus#(s(x), y) → plus#(x, y) | plus#(s(plus(x, y)), z) → plus#(plus(x, y), z) |
| plus#(s(plus(x, y)), z) → plus#(x, y) | plus#(s(x), y) → plus#(minus(x, y), double(y)) |
| plus#(s(x), y) → plus#(x, s(y)) |
| minus#(s(x), s(y)) → minus#(x, y) |
| double#(s(x)) → double#(x) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| double#(s(x)) | → | double#(x) |
Rewrite Rules
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| double(0) | → | 0 | | double(s(x)) | → | s(s(double(x))) |
| plus(0, y) | → | y | | plus(s(x), y) | → | s(plus(x, y)) |
| plus(s(x), y) | → | plus(x, s(y)) | | plus(s(x), y) | → | s(plus(minus(x, y), double(y))) |
| plus(s(plus(x, y)), z) | → | s(plus(plus(x, y), z)) |
Original Signature
Termination of terms over the following signature is verified: plus, minus, 0, s, double
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| double#(s(x)) | → | double#(x) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| minus#(s(x), s(y)) | → | minus#(x, y) |
Rewrite Rules
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| double(0) | → | 0 | | double(s(x)) | → | s(s(double(x))) |
| plus(0, y) | → | y | | plus(s(x), y) | → | s(plus(x, y)) |
| plus(s(x), y) | → | plus(x, s(y)) | | plus(s(x), y) | → | s(plus(minus(x, y), double(y))) |
| plus(s(plus(x, y)), z) | → | s(plus(plus(x, y), z)) |
Original Signature
Termination of terms over the following signature is verified: plus, minus, 0, s, double
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| minus#(s(x), s(y)) | → | minus#(x, y) |
Problem 4: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| plus#(s(x), y) | → | plus#(x, y) | | plus#(s(plus(x, y)), z) | → | plus#(plus(x, y), z) |
| plus#(s(plus(x, y)), z) | → | plus#(x, y) | | plus#(s(x), y) | → | plus#(minus(x, y), double(y)) |
| plus#(s(x), y) | → | plus#(x, s(y)) |
Rewrite Rules
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| double(0) | → | 0 | | double(s(x)) | → | s(s(double(x))) |
| plus(0, y) | → | y | | plus(s(x), y) | → | s(plus(x, y)) |
| plus(s(x), y) | → | plus(x, s(y)) | | plus(s(x), y) | → | s(plus(minus(x, y), double(y))) |
| plus(s(plus(x, y)), z) | → | s(plus(plus(x, y), z)) |
Original Signature
Termination of terms over the following signature is verified: plus, minus, 0, s, double
Strategy
Polynomial Interpretation
- 0: 0
- double(x): 0
- minus(x,y): x
- plus(x,y): y + x + 1
- plus#(x,y): y + x
- s(x): x
Improved Usable rules
| plus(s(x), y) | → | plus(x, s(y)) | | double(0) | → | 0 |
| minus(s(x), s(y)) | → | minus(x, y) | | plus(s(x), y) | → | s(plus(x, y)) |
| plus(s(x), y) | → | s(plus(minus(x, y), double(y))) | | plus(s(plus(x, y)), z) | → | s(plus(plus(x, y), z)) |
| double(s(x)) | → | s(s(double(x))) | | plus(0, y) | → | y |
| minus(x, 0) | → | x |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| plus#(s(plus(x, y)), z) | → | plus#(x, y) |
Problem 5: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| plus#(s(x), y) | → | plus#(x, y) | | plus#(s(plus(x, y)), z) | → | plus#(plus(x, y), z) |
| plus#(s(x), y) | → | plus#(minus(x, y), double(y)) | | plus#(s(x), y) | → | plus#(x, s(y)) |
Rewrite Rules
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| double(0) | → | 0 | | double(s(x)) | → | s(s(double(x))) |
| plus(0, y) | → | y | | plus(s(x), y) | → | s(plus(x, y)) |
| plus(s(x), y) | → | plus(x, s(y)) | | plus(s(x), y) | → | s(plus(minus(x, y), double(y))) |
| plus(s(plus(x, y)), z) | → | s(plus(plus(x, y), z)) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, minus, s, double
Strategy
Function Precedence
plus < double < 0 < s = plus# < minus
Argument Filtering
plus: 1 2
minus: 1
0: all arguments are removed from 0
s: 1
plus#: 1
double: 1
Status
plus: lexicographic with permutation 1 → 1 2 → 2
minus: multiset
0: multiset
s: multiset
plus#: multiset
double: lexicographic with permutation 1 → 1
Usable Rules
| plus(s(x), y) → plus(x, s(y)) | double(0) → 0 |
| minus(s(x), s(y)) → minus(x, y) | plus(s(x), y) → s(plus(x, y)) |
| plus(s(x), y) → s(plus(minus(x, y), double(y))) | plus(s(plus(x, y)), z) → s(plus(plus(x, y), z)) |
| double(s(x)) → s(s(double(x))) | plus(0, y) → y |
| minus(x, 0) → x |
The dependency pairs and usable rules are stronlgy conservative!
Eliminated dependency pairs
The following dependency pairs (at least) can be eliminated according to the given precedence.
| plus#(s(x), y) → plus#(x, y) | plus#(s(x), y) → plus#(x, s(y)) |
Problem 6: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| plus#(s(plus(x, y)), z) | → | plus#(plus(x, y), z) | | plus#(s(x), y) | → | plus#(minus(x, y), double(y)) |
Rewrite Rules
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| double(0) | → | 0 | | double(s(x)) | → | s(s(double(x))) |
| plus(0, y) | → | y | | plus(s(x), y) | → | s(plus(x, y)) |
| plus(s(x), y) | → | plus(x, s(y)) | | plus(s(x), y) | → | s(plus(minus(x, y), double(y))) |
| plus(s(plus(x, y)), z) | → | s(plus(plus(x, y), z)) |
Original Signature
Termination of terms over the following signature is verified: plus, minus, 0, s, double
Strategy
Function Precedence
plus = 0 < double < minus = s = plus#
Argument Filtering
plus: 1 2
minus: collapses to 1
0: all arguments are removed from 0
s: 1
plus#: collapses to 1
double: 1
Status
plus: lexicographic with permutation 1 → 1 2 → 2
0: multiset
s: lexicographic with permutation 1 → 1
double: lexicographic with permutation 1 → 1
Usable Rules
| plus(s(x), y) → plus(x, s(y)) | double(0) → 0 |
| minus(s(x), s(y)) → minus(x, y) | plus(s(x), y) → s(plus(x, y)) |
| plus(s(x), y) → s(plus(minus(x, y), double(y))) | plus(s(plus(x, y)), z) → s(plus(plus(x, y), z)) |
| double(s(x)) → s(s(double(x))) | plus(0, y) → y |
| minus(x, 0) → x |
The dependency pairs and usable rules are stronlgy conservative!
Eliminated dependency pairs
The following dependency pairs (at least) can be eliminated according to the given precedence.
| plus#(s(x), y) → plus#(minus(x, y), double(y)) |
Problem 7: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| plus#(s(plus(x, y)), z) | → | plus#(plus(x, y), z) |
Rewrite Rules
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| double(0) | → | 0 | | double(s(x)) | → | s(s(double(x))) |
| plus(0, y) | → | y | | plus(s(x), y) | → | s(plus(x, y)) |
| plus(s(x), y) | → | plus(x, s(y)) | | plus(s(x), y) | → | s(plus(minus(x, y), double(y))) |
| plus(s(plus(x, y)), z) | → | s(plus(plus(x, y), z)) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, minus, s, double
Strategy
Function Precedence
plus = 0 < double < s = plus# < minus
Argument Filtering
plus: 1 2
minus: 1
0: all arguments are removed from 0
s: 1
plus#: 1
double: 1
Status
plus: lexicographic with permutation 1 → 1 2 → 2
minus: multiset
0: multiset
s: multiset
plus#: multiset
double: lexicographic with permutation 1 → 1
Usable Rules
| double(0) → 0 | plus(s(x), y) → plus(x, s(y)) |
| minus(s(x), s(y)) → minus(x, y) | plus(s(x), y) → s(plus(x, y)) |
| plus(s(x), y) → s(plus(minus(x, y), double(y))) | double(s(x)) → s(s(double(x))) |
| plus(s(plus(x, y)), z) → s(plus(plus(x, y), z)) | minus(x, 0) → x |
| plus(0, y) → y |
The dependency pairs and usable rules are stronlgy conservative!
Eliminated dependency pairs
The following dependency pairs (at least) can be eliminated according to the given precedence.
| plus#(s(plus(x, y)), z) → plus#(plus(x, y), z) |