TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60359 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (56ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (439ms).
| | – Problem 4 was processed with processor DependencyGraph (0ms).
| – Problem 3 was processed with processor BackwardInstantiation (2ms).
| | – Problem 5 remains open; application of the following processors failed [ForwardInstantiation (1ms), Propagation (1ms), ForwardNarrowing (2ms), BackwardInstantiation (1ms), ForwardInstantiation (3ms), Propagation (0ms)].
The following open problems remain:
Open Dependency Pair Problem 3
Dependency Pairs
| if#(false, x, l) | → | last#(head(l), tail(l)) | | last#(x, l) | → | if#(empty(l), x, l) |
Rewrite Rules
| empty(nil) | → | true | | empty(cons(x, l)) | → | false |
| head(cons(x, l)) | → | x | | tail(nil) | → | nil |
| tail(cons(x, l)) | → | l | | rev(nil) | → | nil |
| rev(cons(x, l)) | → | cons(rev1(x, l), rev2(x, l)) | | last(x, l) | → | if(empty(l), x, l) |
| if(true, x, l) | → | x | | if(false, x, l) | → | last(head(l), tail(l)) |
| rev2(x, nil) | → | nil | | rev2(x, cons(y, l)) | → | rev(cons(x, rev2(y, l))) |
Original Signature
Termination of terms over the following signature is verified: rev1, rev, rev2, last, if, empty, false, true, head, tail, cons, nil
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| rev2#(x, cons(y, l)) | → | rev2#(y, l) | | if#(false, x, l) | → | last#(head(l), tail(l)) |
| if#(false, x, l) | → | head#(l) | | rev#(cons(x, l)) | → | rev2#(x, l) |
| if#(false, x, l) | → | tail#(l) | | rev2#(x, cons(y, l)) | → | rev#(cons(x, rev2(y, l))) |
| last#(x, l) | → | empty#(l) | | last#(x, l) | → | if#(empty(l), x, l) |
Rewrite Rules
| empty(nil) | → | true | | empty(cons(x, l)) | → | false |
| head(cons(x, l)) | → | x | | tail(nil) | → | nil |
| tail(cons(x, l)) | → | l | | rev(nil) | → | nil |
| rev(cons(x, l)) | → | cons(rev1(x, l), rev2(x, l)) | | last(x, l) | → | if(empty(l), x, l) |
| if(true, x, l) | → | x | | if(false, x, l) | → | last(head(l), tail(l)) |
| rev2(x, nil) | → | nil | | rev2(x, cons(y, l)) | → | rev(cons(x, rev2(y, l))) |
Original Signature
Termination of terms over the following signature is verified: rev, rev1, rev2, last, if, empty, true, false, head, tail, nil, cons
Strategy
The following SCCs where found
| if#(false, x, l) → last#(head(l), tail(l)) | last#(x, l) → if#(empty(l), x, l) |
| rev2#(x, cons(y, l)) → rev2#(y, l) | rev#(cons(x, l)) → rev2#(x, l) |
| rev2#(x, cons(y, l)) → rev#(cons(x, rev2(y, l))) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| rev2#(x, cons(y, l)) | → | rev2#(y, l) | | rev#(cons(x, l)) | → | rev2#(x, l) |
| rev2#(x, cons(y, l)) | → | rev#(cons(x, rev2(y, l))) |
Rewrite Rules
| empty(nil) | → | true | | empty(cons(x, l)) | → | false |
| head(cons(x, l)) | → | x | | tail(nil) | → | nil |
| tail(cons(x, l)) | → | l | | rev(nil) | → | nil |
| rev(cons(x, l)) | → | cons(rev1(x, l), rev2(x, l)) | | last(x, l) | → | if(empty(l), x, l) |
| if(true, x, l) | → | x | | if(false, x, l) | → | last(head(l), tail(l)) |
| rev2(x, nil) | → | nil | | rev2(x, cons(y, l)) | → | rev(cons(x, rev2(y, l))) |
Original Signature
Termination of terms over the following signature is verified: rev, rev1, rev2, last, if, empty, true, false, head, tail, nil, cons
Strategy
Polynomial Interpretation
- cons(x,y): 2y + 1
- empty(x): 0
- false: 0
- head(x): 0
- if(x,y,z): 0
- last(x,y): 0
- nil: 3
- rev(x): x
- rev#(x): 2x
- rev1(x,y): 1
- rev2(x,y): y
- rev2#(x,y): 2y
- tail(x): 0
- true: 0
Improved Usable rules
| rev2(x, nil) | → | nil | | rev(nil) | → | nil |
| rev(cons(x, l)) | → | cons(rev1(x, l), rev2(x, l)) | | rev2(x, cons(y, l)) | → | rev(cons(x, rev2(y, l))) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| rev2#(x, cons(y, l)) | → | rev2#(y, l) | | rev#(cons(x, l)) | → | rev2#(x, l) |
Problem 4: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| rev2#(x, cons(y, l)) | → | rev#(cons(x, rev2(y, l))) |
Rewrite Rules
| empty(nil) | → | true | | empty(cons(x, l)) | → | false |
| head(cons(x, l)) | → | x | | tail(nil) | → | nil |
| tail(cons(x, l)) | → | l | | rev(nil) | → | nil |
| rev(cons(x, l)) | → | cons(rev1(x, l), rev2(x, l)) | | last(x, l) | → | if(empty(l), x, l) |
| if(true, x, l) | → | x | | if(false, x, l) | → | last(head(l), tail(l)) |
| rev2(x, nil) | → | nil | | rev2(x, cons(y, l)) | → | rev(cons(x, rev2(y, l))) |
Original Signature
Termination of terms over the following signature is verified: rev1, rev, rev2, last, if, empty, false, true, head, tail, cons, nil
Strategy
There are no SCCs!
Problem 3: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| if#(false, x, l) | → | last#(head(l), tail(l)) | | last#(x, l) | → | if#(empty(l), x, l) |
Rewrite Rules
| empty(nil) | → | true | | empty(cons(x, l)) | → | false |
| head(cons(x, l)) | → | x | | tail(nil) | → | nil |
| tail(cons(x, l)) | → | l | | rev(nil) | → | nil |
| rev(cons(x, l)) | → | cons(rev1(x, l), rev2(x, l)) | | last(x, l) | → | if(empty(l), x, l) |
| if(true, x, l) | → | x | | if(false, x, l) | → | last(head(l), tail(l)) |
| rev2(x, nil) | → | nil | | rev2(x, cons(y, l)) | → | rev(cons(x, rev2(y, l))) |
Original Signature
Termination of terms over the following signature is verified: rev, rev1, rev2, last, if, empty, true, false, head, tail, nil, cons
Strategy
Instantiation
For all potential predecessors l → r of the rule last
#(
x,
l) → if
#(empty(
l),
x,
l) on dependency pair chains it holds that:
- last#(x, l) matches r,
- all variables of last#(x, l) are embedded in constructor contexts, i.e., each subterm of last#(x, l), containing a variable is rooted by a constructor symbol.
Thus, last
#(
x,
l) → if
#(empty(
l),
x,
l) is replaced by instances determined through the above matching. These instances are:
| last#(head(_l), tail(_l)) → if#(empty(tail(_l)), head(_l), tail(_l)) |