YES
The TRS could be proven terminating. The proof took 1045 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (139ms).
| – Problem 2 was processed with processor PolynomialLinearRange4 (46ms).
| – Problem 3 was processed with processor PolynomialLinearRange4 (34ms).
| – Problem 4 was processed with processor PolynomialLinearRange4 (270ms).
| | – Problem 5 was processed with processor PolynomialLinearRange4 (189ms).
| | | – Problem 6 was processed with processor DependencyGraph (17ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U101#(true, y, x) | → | gcd#(s(x), minus(y, x)) | | gcd#(s(x), s(y)) | → | U101#(less(x, y), y, x) |
| U101#(true, y, x) | → | T(x) | | U91#(true, y, x) | → | T(x) |
| U91#(true, y, x) | → | minus#(x, y) | | gcd#(s(x), s(y)) | → | less#(x, y) |
| U91#(true, y, x) | → | T(y) | | gcd#(s(x), s(y)) | → | U91#(less(y, x), y, x) |
| minus#(s(x), s(y)) | → | minus#(x, y) | | less#(s(x), s(y)) | → | less#(x, y) |
| gcd#(s(x), s(y)) | → | less#(y, x) | | U101#(true, y, x) | → | T(y) |
| U101#(true, y, x) | → | minus#(y, x) | | U91#(true, y, x) | → | gcd#(minus(x, y), s(y)) |
Rewrite Rules
| less(x, 0) | → | false | | less(0, s(x)) | → | true |
| less(s(x), s(y)) | → | less(x, y) | | minus(0, s(y)) | → | 0 |
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| gcd(x, x) | → | x | | gcd(s(x), 0) | → | s(x) |
| gcd(0, s(y)) | → | s(y) | | gcd(s(x), s(y)) | → | U91(less(y, x), y, x) |
| U91(true, y, x) | → | gcd(minus(x, y), s(y)) | | gcd(s(x), s(y)) | → | U101(less(x, y), y, x) |
| U101(true, y, x) | → | gcd(s(x), minus(y, x)) |
Original Signature
Termination of terms over the following signature is verified: 0, minus, s, false, true, less, gcd
Strategy
Context-sensitive strategy:
μ(true) = μ(T) = μ(0) = μ(false) = ∅
μ(U101#) = μ(U91#) = μ(s) = μ(U91) = μ(U101) = {1}
μ(minus) = μ(minus#) = μ(less#) = μ(gcd#) = μ(less) = μ(gcd) = {1, 2}
The following SCCs where found
| minus#(s(x), s(y)) → minus#(x, y) |
| less#(s(x), s(y)) → less#(x, y) |
| U101#(true, y, x) → gcd#(s(x), minus(y, x)) | gcd#(s(x), s(y)) → U101#(less(x, y), y, x) |
| gcd#(s(x), s(y)) → U91#(less(y, x), y, x) | U91#(true, y, x) → gcd#(minus(x, y), s(y)) |
Problem 2: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| minus#(s(x), s(y)) | → | minus#(x, y) |
Rewrite Rules
| less(x, 0) | → | false | | less(0, s(x)) | → | true |
| less(s(x), s(y)) | → | less(x, y) | | minus(0, s(y)) | → | 0 |
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| gcd(x, x) | → | x | | gcd(s(x), 0) | → | s(x) |
| gcd(0, s(y)) | → | s(y) | | gcd(s(x), s(y)) | → | U91(less(y, x), y, x) |
| U91(true, y, x) | → | gcd(minus(x, y), s(y)) | | gcd(s(x), s(y)) | → | U101(less(x, y), y, x) |
| U101(true, y, x) | → | gcd(s(x), minus(y, x)) |
Original Signature
Termination of terms over the following signature is verified: 0, minus, s, false, true, less, gcd
Strategy
Context-sensitive strategy:
μ(true) = μ(T) = μ(0) = μ(false) = ∅
μ(U101#) = μ(U91#) = μ(s) = μ(U91) = μ(U101) = {1}
μ(minus) = μ(minus#) = μ(less#) = μ(gcd#) = μ(less) = μ(gcd) = {1, 2}
Polynomial Interpretation
- 0: 0
- U101(x,y,z): 0
- U91(x,y,z): 0
- false: 0
- gcd(x,y): 0
- less(x,y): 0
- minus(x,y): 0
- minus#(x,y): x
- s(x): 2x + 1
- true: 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:
| minus#(s(x), s(y)) | → | minus#(x, y) |
Problem 3: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| less#(s(x), s(y)) | → | less#(x, y) |
Rewrite Rules
| less(x, 0) | → | false | | less(0, s(x)) | → | true |
| less(s(x), s(y)) | → | less(x, y) | | minus(0, s(y)) | → | 0 |
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| gcd(x, x) | → | x | | gcd(s(x), 0) | → | s(x) |
| gcd(0, s(y)) | → | s(y) | | gcd(s(x), s(y)) | → | U91(less(y, x), y, x) |
| U91(true, y, x) | → | gcd(minus(x, y), s(y)) | | gcd(s(x), s(y)) | → | U101(less(x, y), y, x) |
| U101(true, y, x) | → | gcd(s(x), minus(y, x)) |
Original Signature
Termination of terms over the following signature is verified: 0, minus, s, false, true, less, gcd
Strategy
Context-sensitive strategy:
μ(true) = μ(T) = μ(0) = μ(false) = ∅
μ(U101#) = μ(U91#) = μ(s) = μ(U91) = μ(U101) = {1}
μ(minus) = μ(minus#) = μ(less#) = μ(gcd#) = μ(less) = μ(gcd) = {1, 2}
Polynomial Interpretation
- 0: 0
- U101(x,y,z): 0
- U91(x,y,z): 0
- false: 0
- gcd(x,y): 0
- less(x,y): 0
- less#(x,y): y + 1
- minus(x,y): 0
- s(x): 2x + 2
- true: 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:
| less#(s(x), s(y)) | → | less#(x, y) |
Problem 4: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| U101#(true, y, x) | → | gcd#(s(x), minus(y, x)) | | gcd#(s(x), s(y)) | → | U101#(less(x, y), y, x) |
| gcd#(s(x), s(y)) | → | U91#(less(y, x), y, x) | | U91#(true, y, x) | → | gcd#(minus(x, y), s(y)) |
Rewrite Rules
| less(x, 0) | → | false | | less(0, s(x)) | → | true |
| less(s(x), s(y)) | → | less(x, y) | | minus(0, s(y)) | → | 0 |
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| gcd(x, x) | → | x | | gcd(s(x), 0) | → | s(x) |
| gcd(0, s(y)) | → | s(y) | | gcd(s(x), s(y)) | → | U91(less(y, x), y, x) |
| U91(true, y, x) | → | gcd(minus(x, y), s(y)) | | gcd(s(x), s(y)) | → | U101(less(x, y), y, x) |
| U101(true, y, x) | → | gcd(s(x), minus(y, x)) |
Original Signature
Termination of terms over the following signature is verified: 0, minus, s, false, true, less, gcd
Strategy
Context-sensitive strategy:
μ(true) = μ(T) = μ(0) = μ(false) = ∅
μ(U101#) = μ(U91#) = μ(s) = μ(U91) = μ(U101) = {1}
μ(minus) = μ(minus#) = μ(less#) = μ(gcd#) = μ(less) = μ(gcd) = {1, 2}
Polynomial Interpretation
- 0: 1
- U101(x,y,z): 3z + 3y + 3
- U101#(x,y,z): 3z + y + x + 1
- U91(x,y,z): 3z + 3y + 3
- U91#(x,y,z): 2z + 3y + 2
- false: 1
- gcd(x,y): y + x + 1
- gcd#(x,y): y + x
- less(x,y): 2y
- minus(x,y): x + 1
- s(x): 3x + 1
- true: 2
Standard Usable rules
| minus(s(x), s(y)) | → | minus(x, y) | | less(x, 0) | → | false |
| U91(true, y, x) | → | gcd(minus(x, y), s(y)) | | gcd(0, s(y)) | → | s(y) |
| gcd(s(x), s(y)) | → | U101(less(x, y), y, x) | | minus(0, s(y)) | → | 0 |
| minus(x, 0) | → | x | | less(0, s(x)) | → | true |
| gcd(s(x), 0) | → | s(x) | | gcd(s(x), s(y)) | → | U91(less(y, x), y, x) |
| U101(true, y, x) | → | gcd(s(x), minus(y, x)) | | gcd(x, x) | → | x |
| less(s(x), s(y)) | → | less(x, y) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| U101#(true, y, x) | → | gcd#(s(x), minus(y, x)) | | gcd#(s(x), s(y)) | → | U101#(less(x, y), y, x) |
Problem 5: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| gcd#(s(x), s(y)) | → | U91#(less(y, x), y, x) | | U91#(true, y, x) | → | gcd#(minus(x, y), s(y)) |
Rewrite Rules
| less(x, 0) | → | false | | less(0, s(x)) | → | true |
| less(s(x), s(y)) | → | less(x, y) | | minus(0, s(y)) | → | 0 |
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| gcd(x, x) | → | x | | gcd(s(x), 0) | → | s(x) |
| gcd(0, s(y)) | → | s(y) | | gcd(s(x), s(y)) | → | U91(less(y, x), y, x) |
| U91(true, y, x) | → | gcd(minus(x, y), s(y)) | | gcd(s(x), s(y)) | → | U101(less(x, y), y, x) |
| U101(true, y, x) | → | gcd(s(x), minus(y, x)) |
Original Signature
Termination of terms over the following signature is verified: minus, 0, s, true, false, less, gcd
Strategy
Context-sensitive strategy:
μ(true) = μ(T) = μ(0) = μ(false) = ∅
μ(U101#) = μ(U91#) = μ(s) = μ(U91) = μ(U101) = {1}
μ(minus) = μ(minus#) = μ(less#) = μ(gcd#) = μ(less) = μ(gcd) = {1, 2}
Polynomial Interpretation
- 0: 1
- U101(x,y,z): z + y + 1
- U91(x,y,z): z + y + 2
- U91#(x,y,z): 2z + 2
- false: 0
- gcd(x,y): y + x
- gcd#(x,y): 2x
- less(x,y): 0
- minus(x,y): x
- s(x): x + 1
- true: 0
Standard Usable rules
| minus(s(x), s(y)) | → | minus(x, y) | | less(x, 0) | → | false |
| U91(true, y, x) | → | gcd(minus(x, y), s(y)) | | gcd(0, s(y)) | → | s(y) |
| gcd(s(x), s(y)) | → | U101(less(x, y), y, x) | | minus(0, s(y)) | → | 0 |
| minus(x, 0) | → | x | | less(0, s(x)) | → | true |
| gcd(s(x), 0) | → | s(x) | | gcd(s(x), s(y)) | → | U91(less(y, x), y, x) |
| U101(true, y, x) | → | gcd(s(x), minus(y, x)) | | gcd(x, x) | → | x |
| less(s(x), s(y)) | → | less(x, y) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| U91#(true, y, x) | → | gcd#(minus(x, y), s(y)) |
Problem 6: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| gcd#(s(x), s(y)) | → | U91#(less(y, x), y, x) |
Rewrite Rules
| less(x, 0) | → | false | | less(0, s(x)) | → | true |
| less(s(x), s(y)) | → | less(x, y) | | minus(0, s(y)) | → | 0 |
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| gcd(x, x) | → | x | | gcd(s(x), 0) | → | s(x) |
| gcd(0, s(y)) | → | s(y) | | gcd(s(x), s(y)) | → | U91(less(y, x), y, x) |
| U91(true, y, x) | → | gcd(minus(x, y), s(y)) | | gcd(s(x), s(y)) | → | U101(less(x, y), y, x) |
| U101(true, y, x) | → | gcd(s(x), minus(y, x)) |
Original Signature
Termination of terms over the following signature is verified: 0, minus, s, false, true, less, gcd
Strategy
Context-sensitive strategy:
μ(true) = μ(T) = μ(0) = μ(false) = ∅
μ(U101#) = μ(U91#) = μ(s) = μ(U91) = μ(U101) = {1}
μ(minus) = μ(minus#) = μ(less#) = μ(gcd#) = μ(less) = μ(gcd) = {1, 2}
There are no SCCs!