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 (202ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor SubtermCriterion (0ms).
| – Problem 4 was processed with processor SubtermCriterion (34ms).
| | – Problem 6 was processed with processor DependencyGraph (17ms).
| – Problem 5 was processed with processor PolynomialLinearRange4iUR (394ms).
| | – Problem 7 was processed with processor PolynomialLinearRange4iUR (61ms).
| | | – Problem 8 was processed with processor PolynomialLinearRange4iUR (69ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| inter#(app(l1, l2), l3) | → | inter#(l2, l3) | | inter#(cons(x, l1), l2) | → | ifinter#(mem(x, l2), x, l1, l2) |
| app#(app(l1, l2), l3) | → | app#(l1, app(l2, l3)) | | inter#(l1, app(l2, l3)) | → | app#(inter(l1, l2), inter(l1, l3)) |
| inter#(l1, app(l2, l3)) | → | inter#(l1, l3) | | inter#(l1, cons(x, l2)) | → | mem#(x, l1) |
| app#(cons(x, l1), l2) | → | app#(l1, l2) | | app#(app(l1, l2), l3) | → | app#(l2, l3) |
| ifmem#(false, x, l) | → | mem#(x, l) | | inter#(app(l1, l2), l3) | → | app#(inter(l1, l3), inter(l2, l3)) |
| inter#(l1, app(l2, l3)) | → | inter#(l1, l2) | | ifinter#(true, x, l1, l2) | → | inter#(l1, l2) |
| mem#(x, cons(y, l)) | → | ifmem#(eq(x, y), x, l) | | inter#(cons(x, l1), l2) | → | mem#(x, l2) |
| inter#(l1, cons(x, l2)) | → | ifinter#(mem(x, l1), x, l2, l1) | | ifinter#(false, x, l1, l2) | → | inter#(l1, l2) |
| inter#(app(l1, l2), l3) | → | inter#(l1, l3) | | mem#(x, cons(y, l)) | → | eq#(x, y) |
| eq#(s(x), s(y)) | → | eq#(x, y) |
Rewrite Rules
| if(true, x, y) | → | x | | if(false, x, y) | → | y |
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), 0) | → | false | | eq(s(x), s(y)) | → | eq(x, y) |
| app(nil, l) | → | l | | app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) |
| app(app(l1, l2), l3) | → | app(l1, app(l2, l3)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | ifmem(eq(x, y), x, l) | | ifmem(true, x, l) | → | true |
| ifmem(false, x, l) | → | mem(x, l) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, ifmem, true, inter, 0, s, if, mem, false, ifinter, eq, nil, cons
Strategy
The following SCCs where found
| app#(app(l1, l2), l3) → app#(l2, l3) | app#(cons(x, l1), l2) → app#(l1, l2) |
| app#(app(l1, l2), l3) → app#(l1, app(l2, l3)) |
| ifmem#(false, x, l) → mem#(x, l) | mem#(x, cons(y, l)) → ifmem#(eq(x, y), x, l) |
| eq#(s(x), s(y)) → eq#(x, y) |
| inter#(l1, app(l2, l3)) → inter#(l1, l3) | inter#(l1, app(l2, l3)) → inter#(l1, l2) |
| ifinter#(true, x, l1, l2) → inter#(l1, l2) | inter#(l1, cons(x, l2)) → ifinter#(mem(x, l1), x, l2, l1) |
| inter#(app(l1, l2), l3) → inter#(l2, l3) | ifinter#(false, x, l1, l2) → inter#(l1, l2) |
| inter#(cons(x, l1), l2) → ifinter#(mem(x, l2), x, l1, l2) | inter#(app(l1, l2), l3) → inter#(l1, l3) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| eq#(s(x), s(y)) | → | eq#(x, y) |
Rewrite Rules
| if(true, x, y) | → | x | | if(false, x, y) | → | y |
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), 0) | → | false | | eq(s(x), s(y)) | → | eq(x, y) |
| app(nil, l) | → | l | | app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) |
| app(app(l1, l2), l3) | → | app(l1, app(l2, l3)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | ifmem(eq(x, y), x, l) | | ifmem(true, x, l) | → | true |
| ifmem(false, x, l) | → | mem(x, l) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, ifmem, true, inter, 0, s, if, mem, false, ifinter, eq, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| eq#(s(x), s(y)) | → | eq#(x, y) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| app#(app(l1, l2), l3) | → | app#(l2, l3) | | app#(cons(x, l1), l2) | → | app#(l1, l2) |
| app#(app(l1, l2), l3) | → | app#(l1, app(l2, l3)) |
Rewrite Rules
| if(true, x, y) | → | x | | if(false, x, y) | → | y |
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), 0) | → | false | | eq(s(x), s(y)) | → | eq(x, y) |
| app(nil, l) | → | l | | app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) |
| app(app(l1, l2), l3) | → | app(l1, app(l2, l3)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | ifmem(eq(x, y), x, l) | | ifmem(true, x, l) | → | true |
| ifmem(false, x, l) | → | mem(x, l) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, ifmem, true, inter, 0, s, if, mem, false, ifinter, eq, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| app#(cons(x, l1), l2) | → | app#(l1, l2) | | app#(app(l1, l2), l3) | → | app#(l2, l3) |
| app#(app(l1, l2), l3) | → | app#(l1, app(l2, l3)) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| ifmem#(false, x, l) | → | mem#(x, l) | | mem#(x, cons(y, l)) | → | ifmem#(eq(x, y), x, l) |
Rewrite Rules
| if(true, x, y) | → | x | | if(false, x, y) | → | y |
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), 0) | → | false | | eq(s(x), s(y)) | → | eq(x, y) |
| app(nil, l) | → | l | | app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) |
| app(app(l1, l2), l3) | → | app(l1, app(l2, l3)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | ifmem(eq(x, y), x, l) | | ifmem(true, x, l) | → | true |
| ifmem(false, x, l) | → | mem(x, l) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, ifmem, true, inter, 0, s, if, mem, false, ifinter, eq, nil, cons
Strategy
Projection
The following projection was used:
- π (ifmem#): 3
- π (mem#): 2
Thus, the following dependency pairs are removed:
| mem#(x, cons(y, l)) | → | ifmem#(eq(x, y), x, l) |
Problem 6: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| ifmem#(false, x, l) | → | mem#(x, l) |
Rewrite Rules
| if(true, x, y) | → | x | | if(false, x, y) | → | y |
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), 0) | → | false | | eq(s(x), s(y)) | → | eq(x, y) |
| app(nil, l) | → | l | | app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) |
| app(app(l1, l2), l3) | → | app(l1, app(l2, l3)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | ifmem(eq(x, y), x, l) | | ifmem(true, x, l) | → | true |
| ifmem(false, x, l) | → | mem(x, l) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, ifmem, true, inter, 0, s, if, mem, false, ifinter, eq, nil, cons
Strategy
There are no SCCs!
Problem 5: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| inter#(l1, app(l2, l3)) | → | inter#(l1, l3) | | inter#(l1, app(l2, l3)) | → | inter#(l1, l2) |
| ifinter#(true, x, l1, l2) | → | inter#(l1, l2) | | inter#(l1, cons(x, l2)) | → | ifinter#(mem(x, l1), x, l2, l1) |
| inter#(app(l1, l2), l3) | → | inter#(l2, l3) | | ifinter#(false, x, l1, l2) | → | inter#(l1, l2) |
| inter#(cons(x, l1), l2) | → | ifinter#(mem(x, l2), x, l1, l2) | | inter#(app(l1, l2), l3) | → | inter#(l1, l3) |
Rewrite Rules
| if(true, x, y) | → | x | | if(false, x, y) | → | y |
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), 0) | → | false | | eq(s(x), s(y)) | → | eq(x, y) |
| app(nil, l) | → | l | | app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) |
| app(app(l1, l2), l3) | → | app(l1, app(l2, l3)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | ifmem(eq(x, y), x, l) | | ifmem(true, x, l) | → | true |
| ifmem(false, x, l) | → | mem(x, l) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, ifmem, true, inter, 0, s, if, mem, false, ifinter, eq, nil, cons
Strategy
Polynomial Interpretation
- 0: 3
- app(x,y): y + x
- cons(x,y): y + 2
- eq(x,y): 0
- false: 0
- if(x,y,z): 0
- ifinter(x1,x2,x3,x4): 0
- ifinter#(x1,x2,x3,x4): x4 + x3 + 1
- ifmem(x,y,z): 3y
- inter(x,y): 0
- inter#(x,y): y + x
- mem(x,y): 2x + 1
- nil: 1
- s(x): 2
- true: 0
Improved Usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| ifinter#(true, x, l1, l2) | → | inter#(l1, l2) | | inter#(l1, cons(x, l2)) | → | ifinter#(mem(x, l1), x, l2, l1) |
| ifinter#(false, x, l1, l2) | → | inter#(l1, l2) | | inter#(cons(x, l1), l2) | → | ifinter#(mem(x, l2), x, l1, l2) |
Problem 7: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| inter#(l1, app(l2, l3)) | → | inter#(l1, l3) | | inter#(l1, app(l2, l3)) | → | inter#(l1, l2) |
| inter#(app(l1, l2), l3) | → | inter#(l2, l3) | | inter#(app(l1, l2), l3) | → | inter#(l1, l3) |
Rewrite Rules
| if(true, x, y) | → | x | | if(false, x, y) | → | y |
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), 0) | → | false | | eq(s(x), s(y)) | → | eq(x, y) |
| app(nil, l) | → | l | | app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) |
| app(app(l1, l2), l3) | → | app(l1, app(l2, l3)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | ifmem(eq(x, y), x, l) | | ifmem(true, x, l) | → | true |
| ifmem(false, x, l) | → | mem(x, l) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, ifmem, true, inter, 0, s, if, mem, false, ifinter, eq, nil, cons
Strategy
Polynomial Interpretation
- 0: 0
- app(x,y): y + 2x + 1
- cons(x,y): 0
- eq(x,y): 0
- false: 0
- if(x,y,z): 0
- ifinter(x1,x2,x3,x4): 0
- ifmem(x,y,z): 0
- inter(x,y): 0
- inter#(x,y): x
- mem(x,y): 0
- nil: 0
- s(x): 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:
| inter#(app(l1, l2), l3) | → | inter#(l2, l3) | | inter#(app(l1, l2), l3) | → | inter#(l1, l3) |
Problem 8: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| inter#(l1, app(l2, l3)) | → | inter#(l1, l3) | | inter#(l1, app(l2, l3)) | → | inter#(l1, l2) |
Rewrite Rules
| if(true, x, y) | → | x | | if(false, x, y) | → | y |
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), 0) | → | false | | eq(s(x), s(y)) | → | eq(x, y) |
| app(nil, l) | → | l | | app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) |
| app(app(l1, l2), l3) | → | app(l1, app(l2, l3)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | ifmem(eq(x, y), x, l) | | ifmem(true, x, l) | → | true |
| ifmem(false, x, l) | → | mem(x, l) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, ifmem, true, inter, 0, s, if, mem, false, ifinter, eq, nil, cons
Strategy
Polynomial Interpretation
- 0: 0
- app(x,y): y + 2x + 1
- cons(x,y): 0
- eq(x,y): 0
- false: 0
- if(x,y,z): 0
- ifinter(x1,x2,x3,x4): 0
- ifmem(x,y,z): 0
- inter(x,y): 0
- inter#(x,y): 2y
- mem(x,y): 0
- nil: 0
- s(x): 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:
| inter#(l1, app(l2, l3)) | → | inter#(l1, l3) | | inter#(l1, app(l2, l3)) | → | inter#(l1, l2) |