YES
The TRS could be proven terminating. The proof took 538 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (34ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| | – Problem 5 was processed with processor DependencyGraph (0ms).
| – Problem 3 was processed with processor SubtermCriterion (1ms).
| – Problem 4 was processed with processor PolynomialLinearRange4iUR (355ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| ifrm#(true, N, add(M, X)) | → | rm#(N, X) | | rm#(N, add(M, X)) | → | eq#(N, M) |
| eq#(s(X), s(Y)) | → | eq#(X, Y) | | ifrm#(false, N, add(M, X)) | → | rm#(N, X) |
| purge#(add(N, X)) | → | purge#(rm(N, X)) | | rm#(N, add(M, X)) | → | ifrm#(eq(N, M), N, add(M, X)) |
| purge#(add(N, X)) | → | rm#(N, X) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(X)) | → | false |
| eq(s(X), 0) | → | false | | eq(s(X), s(Y)) | → | eq(X, Y) |
| rm(N, nil) | → | nil | | rm(N, add(M, X)) | → | ifrm(eq(N, M), N, add(M, X)) |
| ifrm(true, N, add(M, X)) | → | rm(N, X) | | ifrm(false, N, add(M, X)) | → | add(M, rm(N, X)) |
| purge(nil) | → | nil | | purge(add(N, X)) | → | add(N, purge(rm(N, X))) |
Original Signature
Termination of terms over the following signature is verified: 0, s, rm, true, false, ifrm, add, purge, eq, nil
Strategy
The following SCCs where found
| eq#(s(X), s(Y)) → eq#(X, Y) |
| purge#(add(N, X)) → purge#(rm(N, X)) |
| ifrm#(true, N, add(M, X)) → rm#(N, X) | ifrm#(false, N, add(M, X)) → rm#(N, X) |
| rm#(N, add(M, X)) → ifrm#(eq(N, M), N, add(M, X)) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| ifrm#(true, N, add(M, X)) | → | rm#(N, X) | | ifrm#(false, N, add(M, X)) | → | rm#(N, X) |
| rm#(N, add(M, X)) | → | ifrm#(eq(N, M), N, add(M, X)) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(X)) | → | false |
| eq(s(X), 0) | → | false | | eq(s(X), s(Y)) | → | eq(X, Y) |
| rm(N, nil) | → | nil | | rm(N, add(M, X)) | → | ifrm(eq(N, M), N, add(M, X)) |
| ifrm(true, N, add(M, X)) | → | rm(N, X) | | ifrm(false, N, add(M, X)) | → | add(M, rm(N, X)) |
| purge(nil) | → | nil | | purge(add(N, X)) | → | add(N, purge(rm(N, X))) |
Original Signature
Termination of terms over the following signature is verified: 0, s, rm, true, false, ifrm, add, purge, eq, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| ifrm#(true, N, add(M, X)) | → | rm#(N, X) | | ifrm#(false, N, add(M, X)) | → | rm#(N, X) |
Problem 5: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| rm#(N, add(M, X)) | → | ifrm#(eq(N, M), N, add(M, X)) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(X)) | → | false |
| eq(s(X), 0) | → | false | | eq(s(X), s(Y)) | → | eq(X, Y) |
| rm(N, nil) | → | nil | | rm(N, add(M, X)) | → | ifrm(eq(N, M), N, add(M, X)) |
| ifrm(true, N, add(M, X)) | → | rm(N, X) | | ifrm(false, N, add(M, X)) | → | add(M, rm(N, X)) |
| purge(nil) | → | nil | | purge(add(N, X)) | → | add(N, purge(rm(N, X))) |
Original Signature
Termination of terms over the following signature is verified: 0, rm, s, ifrm, false, true, add, purge, nil, eq
Strategy
There are no SCCs!
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| eq#(s(X), s(Y)) | → | eq#(X, Y) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(X)) | → | false |
| eq(s(X), 0) | → | false | | eq(s(X), s(Y)) | → | eq(X, Y) |
| rm(N, nil) | → | nil | | rm(N, add(M, X)) | → | ifrm(eq(N, M), N, add(M, X)) |
| ifrm(true, N, add(M, X)) | → | rm(N, X) | | ifrm(false, N, add(M, X)) | → | add(M, rm(N, X)) |
| purge(nil) | → | nil | | purge(add(N, X)) | → | add(N, purge(rm(N, X))) |
Original Signature
Termination of terms over the following signature is verified: 0, s, rm, true, false, ifrm, add, purge, eq, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| eq#(s(X), s(Y)) | → | eq#(X, Y) |
Problem 4: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| purge#(add(N, X)) | → | purge#(rm(N, X)) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(X)) | → | false |
| eq(s(X), 0) | → | false | | eq(s(X), s(Y)) | → | eq(X, Y) |
| rm(N, nil) | → | nil | | rm(N, add(M, X)) | → | ifrm(eq(N, M), N, add(M, X)) |
| ifrm(true, N, add(M, X)) | → | rm(N, X) | | ifrm(false, N, add(M, X)) | → | add(M, rm(N, X)) |
| purge(nil) | → | nil | | purge(add(N, X)) | → | add(N, purge(rm(N, X))) |
Original Signature
Termination of terms over the following signature is verified: 0, s, rm, true, false, ifrm, add, purge, eq, nil
Strategy
Polynomial Interpretation
- 0: 0
- add(x,y): y + x + 1
- eq(x,y): 0
- false: 0
- ifrm(x,y,z): z
- nil: 0
- purge(x): 0
- purge#(x): x + 1
- rm(x,y): y
- s(x): 3x + 1
- true: 2
Improved Usable rules
| ifrm(false, N, add(M, X)) | → | add(M, rm(N, X)) | | rm(N, add(M, X)) | → | ifrm(eq(N, M), N, add(M, X)) |
| rm(N, nil) | → | nil | | ifrm(true, N, add(M, X)) | → | rm(N, X) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| purge#(add(N, X)) | → | purge#(rm(N, X)) |