YES
The TRS could be proven terminating. The proof took 1151 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (68ms).
| – Problem 2 was processed with processor PolynomialLinearRange4 (386ms).
| | – Problem 3 was processed with processor PolynomialLinearRange4 (99ms).
| | | – Problem 4 was processed with processor DependencyGraph (56ms).
| | | | – Problem 5 was processed with processor PolynomialLinearRange4 (26ms).
| | | | | – Problem 6 was processed with processor PolynomialLinearRange4 (14ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| T(first(x_1, x_2)) | → | T(x_2) | | if#(false, X, Y) | → | T(Y) |
| T(first(X, Z)) | → | first#(X, Z) | | T(from(s(X))) | → | from#(s(X)) |
| T(s(x_1)) | → | T(x_1) | | and#(true, X) | → | T(X) |
| add#(0, X) | → | T(X) | | T(add(x_1, x_2)) | → | T(x_1) |
| T(add(X, Y)) | → | add#(X, Y) | | T(first(x_1, x_2)) | → | T(x_1) |
| if#(true, X, Y) | → | T(X) | | T(add(x_1, x_2)) | → | T(x_2) |
Rewrite Rules
| and(true, X) | → | X | | and(false, Y) | → | false |
| if(true, X, Y) | → | X | | if(false, X, Y) | → | Y |
| add(0, X) | → | X | | add(s(X), Y) | → | s(add(X, Y)) |
| first(0, X) | → | nil | | first(s(X), cons(Y, Z)) | → | cons(Y, first(X, Z)) |
| from(X) | → | cons(X, from(s(X))) |
Original Signature
Termination of terms over the following signature is verified: 0, s, if, true, false, from, add, first, and, nil, cons
Strategy
Context-sensitive strategy:
μ(from#) = μ(true) = μ(from) = μ(T) = μ(0) = μ(s) = μ(false) = μ(nil) = μ(cons) = ∅
μ(and#) = μ(add) = μ(and) = μ(if) = μ(if#) = μ(add#) = {1}
μ(first#) = μ(first) = {1, 2}
The following SCCs where found
| T(first(x_1, x_2)) → T(x_2) | T(s(x_1)) → T(x_1) |
| add#(0, X) → T(X) | T(add(x_1, x_2)) → T(x_1) |
| T(add(X, Y)) → add#(X, Y) | T(first(x_1, x_2)) → T(x_1) |
| T(add(x_1, x_2)) → T(x_2) |
Problem 2: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| T(first(x_1, x_2)) | → | T(x_2) | | T(s(x_1)) | → | T(x_1) |
| add#(0, X) | → | T(X) | | T(add(x_1, x_2)) | → | T(x_1) |
| T(add(X, Y)) | → | add#(X, Y) | | T(first(x_1, x_2)) | → | T(x_1) |
| T(add(x_1, x_2)) | → | T(x_2) |
Rewrite Rules
| and(true, X) | → | X | | and(false, Y) | → | false |
| if(true, X, Y) | → | X | | if(false, X, Y) | → | Y |
| add(0, X) | → | X | | add(s(X), Y) | → | s(add(X, Y)) |
| first(0, X) | → | nil | | first(s(X), cons(Y, Z)) | → | cons(Y, first(X, Z)) |
| from(X) | → | cons(X, from(s(X))) |
Original Signature
Termination of terms over the following signature is verified: 0, s, if, true, false, from, add, first, and, nil, cons
Strategy
Context-sensitive strategy:
μ(from#) = μ(true) = μ(from) = μ(T) = μ(0) = μ(s) = μ(false) = μ(cons) = μ(nil) = ∅
μ(and#) = μ(add) = μ(and) = μ(if) = μ(if#) = μ(add#) = {1}
μ(first#) = μ(first) = {1, 2}
Polynomial Interpretation
- 0: 0
- T(x): x
- add(x,y): 2y + x
- add#(x,y): y + x
- and(x,y): 0
- cons(x,y): 0
- false: 0
- first(x,y): y + x
- from(x): 2
- if(x,y,z): 0
- nil: 0
- s(x): x + 1
- true: 0
Standard Usable rules
| from(X) | → | cons(X, from(s(X))) | | add(s(X), Y) | → | s(add(X, Y)) |
| add(0, X) | → | X | | first(s(X), cons(Y, Z)) | → | cons(Y, first(X, Z)) |
| first(0, X) | → | nil |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
Problem 3: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| T(first(x_1, x_2)) | → | T(x_2) | | T(add(x_1, x_2)) | → | T(x_1) |
| add#(0, X) | → | T(X) | | T(add(X, Y)) | → | add#(X, Y) |
| T(first(x_1, x_2)) | → | T(x_1) | | T(add(x_1, x_2)) | → | T(x_2) |
Rewrite Rules
| and(true, X) | → | X | | and(false, Y) | → | false |
| if(true, X, Y) | → | X | | if(false, X, Y) | → | Y |
| add(0, X) | → | X | | add(s(X), Y) | → | s(add(X, Y)) |
| first(0, X) | → | nil | | first(s(X), cons(Y, Z)) | → | cons(Y, first(X, Z)) |
| from(X) | → | cons(X, from(s(X))) |
Original Signature
Termination of terms over the following signature is verified: 0, s, if, false, true, from, add, first, cons, nil, and
Strategy
Context-sensitive strategy:
μ(from#) = μ(true) = μ(from) = μ(T) = μ(0) = μ(s) = μ(false) = μ(nil) = μ(cons) = ∅
μ(and#) = μ(add) = μ(and) = μ(if) = μ(if#) = μ(add#) = {1}
μ(first#) = μ(first) = {1, 2}
Polynomial Interpretation
- 0: 1
- T(x): 2x + 1
- add(x,y): y + 2x
- add#(x,y): 2y + x
- and(x,y): 0
- cons(x,y): y
- false: 0
- first(x,y): y + 2x
- from(x): 0
- if(x,y,z): 0
- nil: 1
- s(x): x
- true: 0
Standard Usable rules
| from(X) | → | cons(X, from(s(X))) | | add(s(X), Y) | → | s(add(X, Y)) |
| add(0, X) | → | X | | first(s(X), cons(Y, Z)) | → | cons(Y, first(X, Z)) |
| first(0, X) | → | nil |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| T(add(X, Y)) | → | add#(X, Y) |
Problem 4: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| T(first(x_1, x_2)) | → | T(x_2) | | add#(0, X) | → | T(X) |
| T(add(x_1, x_2)) | → | T(x_1) | | T(first(x_1, x_2)) | → | T(x_1) |
| T(add(x_1, x_2)) | → | T(x_2) |
Rewrite Rules
| and(true, X) | → | X | | and(false, Y) | → | false |
| if(true, X, Y) | → | X | | if(false, X, Y) | → | Y |
| add(0, X) | → | X | | add(s(X), Y) | → | s(add(X, Y)) |
| first(0, X) | → | nil | | first(s(X), cons(Y, Z)) | → | cons(Y, first(X, Z)) |
| from(X) | → | cons(X, from(s(X))) |
Original Signature
Termination of terms over the following signature is verified: 0, s, if, true, false, from, add, first, and, nil, cons
Strategy
Context-sensitive strategy:
μ(from#) = μ(true) = μ(from) = μ(T) = μ(0) = μ(s) = μ(false) = μ(cons) = μ(nil) = ∅
μ(and#) = μ(add) = μ(and) = μ(if) = μ(if#) = μ(add#) = {1}
μ(first#) = μ(first) = {1, 2}
The following SCCs where found
| T(first(x_1, x_2)) → T(x_2) | T(add(x_1, x_2)) → T(x_1) |
| T(first(x_1, x_2)) → T(x_1) | T(add(x_1, x_2)) → T(x_2) |
Problem 5: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| T(first(x_1, x_2)) | → | T(x_2) | | T(add(x_1, x_2)) | → | T(x_1) |
| T(first(x_1, x_2)) | → | T(x_1) | | T(add(x_1, x_2)) | → | T(x_2) |
Rewrite Rules
| and(true, X) | → | X | | and(false, Y) | → | false |
| if(true, X, Y) | → | X | | if(false, X, Y) | → | Y |
| add(0, X) | → | X | | add(s(X), Y) | → | s(add(X, Y)) |
| first(0, X) | → | nil | | first(s(X), cons(Y, Z)) | → | cons(Y, first(X, Z)) |
| from(X) | → | cons(X, from(s(X))) |
Original Signature
Termination of terms over the following signature is verified: 0, s, if, true, false, from, add, first, and, nil, cons
Strategy
Context-sensitive strategy:
μ(from#) = μ(true) = μ(from) = μ(T) = μ(0) = μ(s) = μ(false) = μ(nil) = μ(cons) = ∅
μ(and#) = μ(add) = μ(and) = μ(if) = μ(if#) = μ(add#) = {1}
μ(first#) = μ(first) = {1, 2}
Polynomial Interpretation
- 0: 0
- T(x): 2x
- add(x,y): y + 2x
- and(x,y): 0
- cons(x,y): 0
- false: 0
- first(x,y): y + 2x + 1
- from(x): 0
- if(x,y,z): 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:
| T(first(x_1, x_2)) | → | T(x_2) | | T(first(x_1, x_2)) | → | T(x_1) |
Problem 6: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| T(add(x_1, x_2)) | → | T(x_1) | | T(add(x_1, x_2)) | → | T(x_2) |
Rewrite Rules
| and(true, X) | → | X | | and(false, Y) | → | false |
| if(true, X, Y) | → | X | | if(false, X, Y) | → | Y |
| add(0, X) | → | X | | add(s(X), Y) | → | s(add(X, Y)) |
| first(0, X) | → | nil | | first(s(X), cons(Y, Z)) | → | cons(Y, first(X, Z)) |
| from(X) | → | cons(X, from(s(X))) |
Original Signature
Termination of terms over the following signature is verified: 0, s, if, false, true, from, add, first, cons, nil, and
Strategy
Context-sensitive strategy:
μ(from#) = μ(true) = μ(from) = μ(T) = μ(0) = μ(s) = μ(false) = μ(cons) = μ(nil) = ∅
μ(and#) = μ(add) = μ(and) = μ(if) = μ(if#) = μ(add#) = {1}
μ(first#) = μ(first) = {1, 2}
Polynomial Interpretation
- 0: 0
- T(x): x
- add(x,y): 2y + x + 1
- and(x,y): 0
- cons(x,y): 0
- false: 0
- first(x,y): 0
- from(x): 0
- if(x,y,z): 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:
| T(add(x_1, x_2)) | → | T(x_1) | | T(add(x_1, x_2)) | → | T(x_2) |