YES
The TRS could be proven terminating. The proof took 715 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (106ms).
| – Problem 2 was processed with processor PolynomialLinearRange4 (51ms).
| – Problem 3 was processed with processor PolynomialLinearRange4 (190ms).
| | – Problem 5 was processed with processor DependencyGraph (0ms).
| – Problem 4 was processed with processor PolynomialLinearRange4 (34ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| quotrem#(s(x), s(y)) | → | U81#(less(x, y), y, x) | | quotrem#(s(x), s(y)) | → | less#(x, y) |
| U81#(false, y, x) | → | U82#(quotrem(minus(x, y), s(y)), y, x) | | U81#(false, y, x) | → | quotrem#(minus(x, y), s(y)) |
| minus#(s(x), s(y)) | → | minus#(x, y) | | U71#(true, y, x) | → | T(x) |
| U81#(false, y, x) | → | minus#(x, y) | | less#(s(x), s(y)) | → | less#(x, y) |
| quotrem#(s(x), s(y)) | → | U71#(less(x, y), y, x) | | U81#(false, y, x) | → | T(y) |
| U81#(false, y, x) | → | T(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) |
| quotrem(0, s(y)) | → | pair(0, 0) | | quotrem(s(x), s(y)) | → | U71(less(x, y), y, x) |
| U71(true, y, x) | → | pair(0, s(x)) | | quotrem(s(x), s(y)) | → | U81(less(x, y), y, x) |
| U81(false, y, x) | → | U82(quotrem(minus(x, y), s(y)), y, x) | | U82(pair(q, r), y, x) | → | pair(s(q), r) |
Original Signature
Termination of terms over the following signature is verified: 0, minus, s, pair, false, true, quotrem, less
Strategy
Context-sensitive strategy:
μ(true) = μ(T) = μ(0) = μ(false) = ∅
μ(U81#) = μ(U82#) = μ(U71) = μ(U71#) = μ(s) = μ(U82) = μ(U81) = {1}
μ(minus) = μ(pair) = μ(minus#) = μ(quotrem) = μ(less#) = μ(less) = μ(quotrem#) = {1, 2}
The following SCCs where found
| quotrem#(s(x), s(y)) → U81#(less(x, y), y, x) | U81#(false, y, x) → quotrem#(minus(x, y), s(y)) |
| minus#(s(x), s(y)) → minus#(x, y) |
| less#(s(x), s(y)) → less#(x, y) |
Problem 2: 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) |
| quotrem(0, s(y)) | → | pair(0, 0) | | quotrem(s(x), s(y)) | → | U71(less(x, y), y, x) |
| U71(true, y, x) | → | pair(0, s(x)) | | quotrem(s(x), s(y)) | → | U81(less(x, y), y, x) |
| U81(false, y, x) | → | U82(quotrem(minus(x, y), s(y)), y, x) | | U82(pair(q, r), y, x) | → | pair(s(q), r) |
Original Signature
Termination of terms over the following signature is verified: 0, minus, s, pair, false, true, quotrem, less
Strategy
Context-sensitive strategy:
μ(true) = μ(T) = μ(0) = μ(false) = ∅
μ(U81#) = μ(U82#) = μ(U71) = μ(U71#) = μ(s) = μ(U82) = μ(U81) = {1}
μ(minus) = μ(pair) = μ(minus#) = μ(quotrem) = μ(less#) = μ(less) = μ(quotrem#) = {1, 2}
Polynomial Interpretation
- 0: 0
- U71(x,y,z): 0
- U81(x,y,z): 0
- U82(x,y,z): 0
- false: 0
- less(x,y): 0
- less#(x,y): y + 1
- minus(x,y): 0
- pair(x,y): 0
- quotrem(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 3: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| quotrem#(s(x), s(y)) | → | U81#(less(x, y), y, x) | | U81#(false, y, x) | → | quotrem#(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) |
| quotrem(0, s(y)) | → | pair(0, 0) | | quotrem(s(x), s(y)) | → | U71(less(x, y), y, x) |
| U71(true, y, x) | → | pair(0, s(x)) | | quotrem(s(x), s(y)) | → | U81(less(x, y), y, x) |
| U81(false, y, x) | → | U82(quotrem(minus(x, y), s(y)), y, x) | | U82(pair(q, r), y, x) | → | pair(s(q), r) |
Original Signature
Termination of terms over the following signature is verified: 0, minus, s, pair, false, true, quotrem, less
Strategy
Context-sensitive strategy:
μ(true) = μ(T) = μ(0) = μ(false) = ∅
μ(U81#) = μ(U82#) = μ(U71) = μ(U71#) = μ(s) = μ(U82) = μ(U81) = {1}
μ(minus) = μ(pair) = μ(minus#) = μ(quotrem) = μ(less#) = μ(less) = μ(quotrem#) = {1, 2}
Polynomial Interpretation
- 0: 1
- U71(x,y,z): x + 2
- U81(x,y,z): x + 1
- U81#(x,y,z): z
- U82(x,y,z): 1
- false: 0
- less(x,y): x + 1
- minus(x,y): x
- pair(x,y): 1
- quotrem(x,y): x + 1
- quotrem#(x,y): x
- s(x): x + 2
- true: 0
Standard Usable rules
| minus(s(x), s(y)) | → | minus(x, y) | | less(0, s(x)) | → | true |
| U81(false, y, x) | → | U82(quotrem(minus(x, y), s(y)), y, x) | | less(x, 0) | → | false |
| quotrem(s(x), s(y)) | → | U71(less(x, y), y, x) | | quotrem(s(x), s(y)) | → | U81(less(x, y), y, x) |
| minus(0, s(y)) | → | 0 | | quotrem(0, s(y)) | → | pair(0, 0) |
| minus(x, 0) | → | x | | U82(pair(q, r), y, x) | → | pair(s(q), r) |
| U71(true, y, x) | → | pair(0, s(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:
| quotrem#(s(x), s(y)) | → | U81#(less(x, y), y, x) |
Problem 5: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U81#(false, y, x) | → | quotrem#(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) |
| quotrem(0, s(y)) | → | pair(0, 0) | | quotrem(s(x), s(y)) | → | U71(less(x, y), y, x) |
| U71(true, y, x) | → | pair(0, s(x)) | | quotrem(s(x), s(y)) | → | U81(less(x, y), y, x) |
| U81(false, y, x) | → | U82(quotrem(minus(x, y), s(y)), y, x) | | U82(pair(q, r), y, x) | → | pair(s(q), r) |
Original Signature
Termination of terms over the following signature is verified: minus, 0, s, pair, true, false, quotrem, less
Strategy
Context-sensitive strategy:
μ(true) = μ(T) = μ(0) = μ(false) = ∅
μ(U81#) = μ(U82#) = μ(U71) = μ(U71#) = μ(s) = μ(U82) = μ(U81) = {1}
μ(minus) = μ(pair) = μ(minus#) = μ(quotrem) = μ(less#) = μ(less) = μ(quotrem#) = {1, 2}
There are no SCCs!
Problem 4: 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) |
| quotrem(0, s(y)) | → | pair(0, 0) | | quotrem(s(x), s(y)) | → | U71(less(x, y), y, x) |
| U71(true, y, x) | → | pair(0, s(x)) | | quotrem(s(x), s(y)) | → | U81(less(x, y), y, x) |
| U81(false, y, x) | → | U82(quotrem(minus(x, y), s(y)), y, x) | | U82(pair(q, r), y, x) | → | pair(s(q), r) |
Original Signature
Termination of terms over the following signature is verified: 0, minus, s, pair, false, true, quotrem, less
Strategy
Context-sensitive strategy:
μ(true) = μ(T) = μ(0) = μ(false) = ∅
μ(U81#) = μ(U82#) = μ(U71) = μ(U71#) = μ(s) = μ(U82) = μ(U81) = {1}
μ(minus) = μ(pair) = μ(minus#) = μ(quotrem) = μ(less#) = μ(less) = μ(quotrem#) = {1, 2}
Polynomial Interpretation
- 0: 0
- U71(x,y,z): 0
- U81(x,y,z): 0
- U82(x,y,z): 0
- false: 0
- less(x,y): 0
- minus(x,y): 0
- minus#(x,y): x
- pair(x,y): 0
- quotrem(x,y): 0
- 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) |