YES
The TRS could be proven terminating. The proof took 862 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (307ms).
| – Problem 2 was processed with processor PolynomialLinearRange4 (46ms).
| – Problem 3 was processed with processor PolynomialLinearRange4 (72ms).
| – Problem 4 was processed with processor PolynomialLinearRange4 (15ms).
| – Problem 5 was processed with processor PolynomialLinearRange4 (283ms).
| | – Problem 6 was processed with processor DependencyGraph (1ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U91#(pair(ys, zs), xs, x) | → | qsort#(zs) | | qsort#(cons(x, xs)) | → | split#(x, xs) |
| app#(cons(x, xs), ys) | → | app#(xs, ys) | | U71#(pairs(xs, zs), ys, y, x) | → | le#(x, y) |
| U61#(pairs(xs, zs), ys, y, x) | → | le#(x, y) | | qsort#(cons(x, xs)) | → | U91#(split(x, xs), xs, x) |
| U91#(pair(ys, zs), xs, x) | → | app#(qsort(ys), cons(x, qsort(zs))) | | U91#(pair(ys, zs), xs, x) | → | qsort#(ys) |
| U72#(false, ys, y, x, zs, xs) | → | T(zs) | | split#(x, cons(y, ys)) | → | split#(x, ys) |
| U62#(true, ys, y, x, zs, xs) | → | T(y) | | U61#(pairs(xs, zs), ys, y, x) | → | U62#(le(x, y), ys, y, x, zs, xs) |
| U62#(true, ys, y, x, zs, xs) | → | T(xs) | | U61#(pairs(xs, zs), ys, y, x) | → | T(x) |
| U71#(pairs(xs, zs), ys, y, x) | → | T(y) | | U71#(pairs(xs, zs), ys, y, x) | → | U72#(le(x, y), ys, y, x, zs, xs) |
| U61#(pairs(xs, zs), ys, y, x) | → | T(y) | | U72#(false, ys, y, x, zs, xs) | → | T(xs) |
| U91#(pair(ys, zs), xs, x) | → | T(x) | | U62#(true, ys, y, x, zs, xs) | → | T(zs) |
| split#(x, cons(y, ys)) | → | U61#(split(x, ys), ys, y, x) | | U72#(false, ys, y, x, zs, xs) | → | T(y) |
| split#(x, cons(y, ys)) | → | U71#(split(x, ys), ys, y, x) | | le#(s(x), s(y)) | → | le#(x, y) |
| U71#(pairs(xs, zs), ys, y, x) | → | T(x) |
Rewrite Rules
| le(0, x) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | app(nil, x) | → | x |
| app(cons(x, xs), ys) | → | cons(x, app(xs, ys)) | | split(x, nil) | → | pair(nil, nil) |
| split(x, cons(y, ys)) | → | U61(split(x, ys), ys, y, x) | | U61(pairs(xs, zs), ys, y, x) | → | U62(le(x, y), ys, y, x, zs, xs) |
| U62(true, ys, y, x, zs, xs) | → | pair(xs, cons(y, zs)) | | split(x, cons(y, ys)) | → | U71(split(x, ys), ys, y, x) |
| U71(pairs(xs, zs), ys, y, x) | → | U72(le(x, y), ys, y, x, zs, xs) | | U72(false, ys, y, x, zs, xs) | → | pair(cons(y, xs), zs) |
| qsort(nil) | → | nil | | qsort(cons(x, xs)) | → | U91(split(x, xs), xs, x) |
| U91(pair(ys, zs), xs, x) | → | app(qsort(ys), cons(x, qsort(zs))) |
Original Signature
Termination of terms over the following signature is verified: app, 0, le, s, pairs, pair, true, false, split, qsort, nil, cons
Strategy
Context-sensitive strategy:
μ(T) = μ(false) = μ(true) = μ(0) = μ(nil) = ∅
μ(U91#) = μ(U62#) = μ(U62) = μ(qsort#) = μ(U61) = μ(U91) = μ(U72#) = μ(qsort) = μ(U61#) = μ(U71) = μ(U72) = μ(U71#) = μ(s) = {1}
μ(pair) = μ(split#) = μ(le#) = μ(cons) = μ(app) = μ(app#) = μ(pairs) = μ(le) = μ(split) = {1, 2}
The following SCCs where found
| qsort#(cons(x, xs)) → U91#(split(x, xs), xs, x) | U91#(pair(ys, zs), xs, x) → qsort#(zs) |
| U91#(pair(ys, zs), xs, x) → qsort#(ys) |
| le#(s(x), s(y)) → le#(x, y) |
| app#(cons(x, xs), ys) → app#(xs, ys) |
| split#(x, cons(y, ys)) → split#(x, ys) |
Problem 2: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| split#(x, cons(y, ys)) | → | split#(x, ys) |
Rewrite Rules
| le(0, x) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | app(nil, x) | → | x |
| app(cons(x, xs), ys) | → | cons(x, app(xs, ys)) | | split(x, nil) | → | pair(nil, nil) |
| split(x, cons(y, ys)) | → | U61(split(x, ys), ys, y, x) | | U61(pairs(xs, zs), ys, y, x) | → | U62(le(x, y), ys, y, x, zs, xs) |
| U62(true, ys, y, x, zs, xs) | → | pair(xs, cons(y, zs)) | | split(x, cons(y, ys)) | → | U71(split(x, ys), ys, y, x) |
| U71(pairs(xs, zs), ys, y, x) | → | U72(le(x, y), ys, y, x, zs, xs) | | U72(false, ys, y, x, zs, xs) | → | pair(cons(y, xs), zs) |
| qsort(nil) | → | nil | | qsort(cons(x, xs)) | → | U91(split(x, xs), xs, x) |
| U91(pair(ys, zs), xs, x) | → | app(qsort(ys), cons(x, qsort(zs))) |
Original Signature
Termination of terms over the following signature is verified: app, 0, le, s, pairs, pair, true, false, split, qsort, nil, cons
Strategy
Context-sensitive strategy:
μ(T) = μ(false) = μ(true) = μ(0) = μ(nil) = ∅
μ(U91#) = μ(U62#) = μ(U62) = μ(U61) = μ(qsort#) = μ(U72#) = μ(U91) = μ(qsort) = μ(U61#) = μ(U71) = μ(U72) = μ(U71#) = μ(s) = {1}
μ(pair) = μ(split#) = μ(le#) = μ(cons) = μ(app) = μ(app#) = μ(pairs) = μ(le) = μ(split) = {1, 2}
Polynomial Interpretation
- 0: 0
- U61(x1,x2,x3,x4): 0
- U62(x1,x2,x3,x4,x5,x6): 0
- U71(x1,x2,x3,x4): 0
- U72(x1,x2,x3,x4,x5,x6): 0
- U91(x,y,z): 0
- app(x,y): 0
- cons(x,y): y + 2
- false: 0
- le(x,y): 0
- nil: 0
- pair(x,y): 0
- pairs(x,y): 0
- qsort(x): 0
- s(x): 0
- split(x,y): 0
- split#(x,y): y + x
- 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:
| split#(x, cons(y, ys)) | → | split#(x, ys) |
Problem 3: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| app#(cons(x, xs), ys) | → | app#(xs, ys) |
Rewrite Rules
| le(0, x) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | app(nil, x) | → | x |
| app(cons(x, xs), ys) | → | cons(x, app(xs, ys)) | | split(x, nil) | → | pair(nil, nil) |
| split(x, cons(y, ys)) | → | U61(split(x, ys), ys, y, x) | | U61(pairs(xs, zs), ys, y, x) | → | U62(le(x, y), ys, y, x, zs, xs) |
| U62(true, ys, y, x, zs, xs) | → | pair(xs, cons(y, zs)) | | split(x, cons(y, ys)) | → | U71(split(x, ys), ys, y, x) |
| U71(pairs(xs, zs), ys, y, x) | → | U72(le(x, y), ys, y, x, zs, xs) | | U72(false, ys, y, x, zs, xs) | → | pair(cons(y, xs), zs) |
| qsort(nil) | → | nil | | qsort(cons(x, xs)) | → | U91(split(x, xs), xs, x) |
| U91(pair(ys, zs), xs, x) | → | app(qsort(ys), cons(x, qsort(zs))) |
Original Signature
Termination of terms over the following signature is verified: app, 0, le, s, pairs, pair, true, false, split, qsort, nil, cons
Strategy
Context-sensitive strategy:
μ(T) = μ(false) = μ(true) = μ(0) = μ(nil) = ∅
μ(U91#) = μ(U62#) = μ(U62) = μ(U61) = μ(qsort#) = μ(U72#) = μ(U91) = μ(qsort) = μ(U61#) = μ(U71) = μ(U72) = μ(U71#) = μ(s) = {1}
μ(pair) = μ(split#) = μ(le#) = μ(cons) = μ(app) = μ(app#) = μ(pairs) = μ(le) = μ(split) = {1, 2}
Polynomial Interpretation
- 0: 0
- U61(x1,x2,x3,x4): 0
- U62(x1,x2,x3,x4,x5,x6): 0
- U71(x1,x2,x3,x4): 0
- U72(x1,x2,x3,x4,x5,x6): 0
- U91(x,y,z): 0
- app(x,y): 0
- app#(x,y): y + x
- cons(x,y): y + 2
- false: 0
- le(x,y): 0
- nil: 0
- pair(x,y): 0
- pairs(x,y): 0
- qsort(x): 0
- s(x): 0
- split(x,y): 0
- 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:
| app#(cons(x, xs), ys) | → | app#(xs, ys) |
Problem 4: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| le#(s(x), s(y)) | → | le#(x, y) |
Rewrite Rules
| le(0, x) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | app(nil, x) | → | x |
| app(cons(x, xs), ys) | → | cons(x, app(xs, ys)) | | split(x, nil) | → | pair(nil, nil) |
| split(x, cons(y, ys)) | → | U61(split(x, ys), ys, y, x) | | U61(pairs(xs, zs), ys, y, x) | → | U62(le(x, y), ys, y, x, zs, xs) |
| U62(true, ys, y, x, zs, xs) | → | pair(xs, cons(y, zs)) | | split(x, cons(y, ys)) | → | U71(split(x, ys), ys, y, x) |
| U71(pairs(xs, zs), ys, y, x) | → | U72(le(x, y), ys, y, x, zs, xs) | | U72(false, ys, y, x, zs, xs) | → | pair(cons(y, xs), zs) |
| qsort(nil) | → | nil | | qsort(cons(x, xs)) | → | U91(split(x, xs), xs, x) |
| U91(pair(ys, zs), xs, x) | → | app(qsort(ys), cons(x, qsort(zs))) |
Original Signature
Termination of terms over the following signature is verified: app, 0, le, s, pairs, pair, true, false, split, qsort, nil, cons
Strategy
Context-sensitive strategy:
μ(T) = μ(false) = μ(true) = μ(0) = μ(nil) = ∅
μ(U91#) = μ(U62#) = μ(U62) = μ(U61) = μ(qsort#) = μ(U72#) = μ(U91) = μ(qsort) = μ(U61#) = μ(U71) = μ(U72) = μ(U71#) = μ(s) = {1}
μ(pair) = μ(split#) = μ(le#) = μ(cons) = μ(app) = μ(app#) = μ(pairs) = μ(le) = μ(split) = {1, 2}
Polynomial Interpretation
- 0: 0
- U61(x1,x2,x3,x4): 0
- U62(x1,x2,x3,x4,x5,x6): 0
- U71(x1,x2,x3,x4): 0
- U72(x1,x2,x3,x4,x5,x6): 0
- U91(x,y,z): 0
- app(x,y): 0
- cons(x,y): 0
- false: 0
- le(x,y): 0
- le#(x,y): y + 1
- nil: 0
- pair(x,y): 0
- pairs(x,y): 0
- qsort(x): 0
- s(x): 2x + 2
- split(x,y): 0
- 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:
| le#(s(x), s(y)) | → | le#(x, y) |
Problem 5: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| qsort#(cons(x, xs)) | → | U91#(split(x, xs), xs, x) | | U91#(pair(ys, zs), xs, x) | → | qsort#(zs) |
| U91#(pair(ys, zs), xs, x) | → | qsort#(ys) |
Rewrite Rules
| le(0, x) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | app(nil, x) | → | x |
| app(cons(x, xs), ys) | → | cons(x, app(xs, ys)) | | split(x, nil) | → | pair(nil, nil) |
| split(x, cons(y, ys)) | → | U61(split(x, ys), ys, y, x) | | U61(pairs(xs, zs), ys, y, x) | → | U62(le(x, y), ys, y, x, zs, xs) |
| U62(true, ys, y, x, zs, xs) | → | pair(xs, cons(y, zs)) | | split(x, cons(y, ys)) | → | U71(split(x, ys), ys, y, x) |
| U71(pairs(xs, zs), ys, y, x) | → | U72(le(x, y), ys, y, x, zs, xs) | | U72(false, ys, y, x, zs, xs) | → | pair(cons(y, xs), zs) |
| qsort(nil) | → | nil | | qsort(cons(x, xs)) | → | U91(split(x, xs), xs, x) |
| U91(pair(ys, zs), xs, x) | → | app(qsort(ys), cons(x, qsort(zs))) |
Original Signature
Termination of terms over the following signature is verified: app, 0, le, s, pairs, pair, true, false, split, qsort, nil, cons
Strategy
Context-sensitive strategy:
μ(T) = μ(false) = μ(true) = μ(0) = μ(nil) = ∅
μ(U91#) = μ(U62#) = μ(U62) = μ(U61) = μ(qsort#) = μ(U72#) = μ(U91) = μ(qsort) = μ(U61#) = μ(U71) = μ(U72) = μ(U71#) = μ(s) = {1}
μ(pair) = μ(split#) = μ(le#) = μ(cons) = μ(app) = μ(app#) = μ(pairs) = μ(le) = μ(split) = {1, 2}
Polynomial Interpretation
- 0: 3
- U61(x1,x2,x3,x4): x1
- U62(x1,x2,x3,x4,x5,x6): 2x6 + 3
- U71(x1,x2,x3,x4): x1
- U72(x1,x2,x3,x4,x5,x6): 2x5 + 3
- U91(x,y,z): x + 1
- U91#(x,y,z): x
- app(x,y): 2y + x
- cons(x,y): 1
- false: 0
- le(x,y): 0
- nil: 0
- pair(x,y): 2y + 2x + 1
- pairs(x,y): 2y + 3x + 3
- qsort(x): 2x
- qsort#(x): 2x + 1
- s(x): 2x + 3
- split(x,y): 1
- true: 0
Standard Usable rules
| le(s(x), s(y)) | → | le(x, y) | | U71(pairs(xs, zs), ys, y, x) | → | U72(le(x, y), ys, y, x, zs, xs) |
| app(cons(x, xs), ys) | → | cons(x, app(xs, ys)) | | app(nil, x) | → | x |
| qsort(nil) | → | nil | | qsort(cons(x, xs)) | → | U91(split(x, xs), xs, x) |
| split(x, cons(y, ys)) | → | U61(split(x, ys), ys, y, x) | | le(0, x) | → | true |
| le(s(x), 0) | → | false | | U62(true, ys, y, x, zs, xs) | → | pair(xs, cons(y, zs)) |
| split(x, cons(y, ys)) | → | U71(split(x, ys), ys, y, x) | | U61(pairs(xs, zs), ys, y, x) | → | U62(le(x, y), ys, y, x, zs, xs) |
| split(x, nil) | → | pair(nil, nil) | | U72(false, ys, y, x, zs, xs) | → | pair(cons(y, xs), zs) |
| U91(pair(ys, zs), xs, x) | → | app(qsort(ys), cons(x, qsort(zs))) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| qsort#(cons(x, xs)) | → | U91#(split(x, xs), xs, x) |
Problem 6: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U91#(pair(ys, zs), xs, x) | → | qsort#(zs) | | U91#(pair(ys, zs), xs, x) | → | qsort#(ys) |
Rewrite Rules
| le(0, x) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | app(nil, x) | → | x |
| app(cons(x, xs), ys) | → | cons(x, app(xs, ys)) | | split(x, nil) | → | pair(nil, nil) |
| split(x, cons(y, ys)) | → | U61(split(x, ys), ys, y, x) | | U61(pairs(xs, zs), ys, y, x) | → | U62(le(x, y), ys, y, x, zs, xs) |
| U62(true, ys, y, x, zs, xs) | → | pair(xs, cons(y, zs)) | | split(x, cons(y, ys)) | → | U71(split(x, ys), ys, y, x) |
| U71(pairs(xs, zs), ys, y, x) | → | U72(le(x, y), ys, y, x, zs, xs) | | U72(false, ys, y, x, zs, xs) | → | pair(cons(y, xs), zs) |
| qsort(nil) | → | nil | | qsort(cons(x, xs)) | → | U91(split(x, xs), xs, x) |
| U91(pair(ys, zs), xs, x) | → | app(qsort(ys), cons(x, qsort(zs))) |
Original Signature
Termination of terms over the following signature is verified: app, 0, pairs, s, le, pair, false, true, qsort, split, cons, nil
Strategy
Context-sensitive strategy:
μ(T) = μ(false) = μ(true) = μ(0) = μ(nil) = ∅
μ(U91#) = μ(U62#) = μ(U62) = μ(qsort#) = μ(U61) = μ(U91) = μ(U72#) = μ(qsort) = μ(U61#) = μ(U71) = μ(U72) = μ(U71#) = μ(s) = {1}
μ(pair) = μ(split#) = μ(le#) = μ(cons) = μ(app) = μ(app#) = μ(pairs) = μ(le) = μ(split) = {1, 2}
There are no SCCs!