TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60002 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (50ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor SubtermCriterion (1ms).
| – Problem 4 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (3ms), PolynomialLinearRange4iUR (330ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (2676ms), DependencyGraph (5ms), ReductionPairSAT (timeout)].
The following open problems remain:
Open Dependency Pair Problem 4
Dependency Pairs
| if#(true, x, l, accu, orig) | → | rev#(s(x), tail(l), cons(head(l), accu), orig) | | rev#(x, l, accu, orig) | → | if#(lt(x, length(orig)), x, l, accu, orig) |
Rewrite Rules
| length(nil) | → | 0 | | length(cons(x, l)) | → | s(length(l)) |
| lt(x, 0) | → | false | | lt(0, s(y)) | → | true |
| lt(s(x), s(y)) | → | lt(x, y) | | head(cons(x, l)) | → | x |
| head(nil) | → | undefined | | tail(nil) | → | nil |
| tail(cons(x, l)) | → | l | | reverse(l) | → | rev(0, l, nil, l) |
| rev(x, l, accu, orig) | → | if(lt(x, length(orig)), x, l, accu, orig) | | if(true, x, l, accu, orig) | → | rev(s(x), tail(l), cons(head(l), accu), orig) |
| if(false, x, l, accu, orig) | → | accu |
Original Signature
Termination of terms over the following signature is verified: rev, reverse, true, lt, tail, 0, s, if, undefined, length, false, head, nil, cons
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| if#(true, x, l, accu, orig) | → | head#(l) | | reverse#(l) | → | rev#(0, l, nil, l) |
| if#(true, x, l, accu, orig) | → | rev#(s(x), tail(l), cons(head(l), accu), orig) | | rev#(x, l, accu, orig) | → | if#(lt(x, length(orig)), x, l, accu, orig) |
| rev#(x, l, accu, orig) | → | lt#(x, length(orig)) | | rev#(x, l, accu, orig) | → | length#(orig) |
| lt#(s(x), s(y)) | → | lt#(x, y) | | length#(cons(x, l)) | → | length#(l) |
| if#(true, x, l, accu, orig) | → | tail#(l) |
Rewrite Rules
| length(nil) | → | 0 | | length(cons(x, l)) | → | s(length(l)) |
| lt(x, 0) | → | false | | lt(0, s(y)) | → | true |
| lt(s(x), s(y)) | → | lt(x, y) | | head(cons(x, l)) | → | x |
| head(nil) | → | undefined | | tail(nil) | → | nil |
| tail(cons(x, l)) | → | l | | reverse(l) | → | rev(0, l, nil, l) |
| rev(x, l, accu, orig) | → | if(lt(x, length(orig)), x, l, accu, orig) | | if(true, x, l, accu, orig) | → | rev(s(x), tail(l), cons(head(l), accu), orig) |
| if(false, x, l, accu, orig) | → | accu |
Original Signature
Termination of terms over the following signature is verified: rev, reverse, true, lt, tail, 0, s, if, undefined, length, false, head, cons, nil
Strategy
The following SCCs where found
| lt#(s(x), s(y)) → lt#(x, y) |
| length#(cons(x, l)) → length#(l) |
| if#(true, x, l, accu, orig) → rev#(s(x), tail(l), cons(head(l), accu), orig) | rev#(x, l, accu, orig) → if#(lt(x, length(orig)), x, l, accu, orig) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| lt#(s(x), s(y)) | → | lt#(x, y) |
Rewrite Rules
| length(nil) | → | 0 | | length(cons(x, l)) | → | s(length(l)) |
| lt(x, 0) | → | false | | lt(0, s(y)) | → | true |
| lt(s(x), s(y)) | → | lt(x, y) | | head(cons(x, l)) | → | x |
| head(nil) | → | undefined | | tail(nil) | → | nil |
| tail(cons(x, l)) | → | l | | reverse(l) | → | rev(0, l, nil, l) |
| rev(x, l, accu, orig) | → | if(lt(x, length(orig)), x, l, accu, orig) | | if(true, x, l, accu, orig) | → | rev(s(x), tail(l), cons(head(l), accu), orig) |
| if(false, x, l, accu, orig) | → | accu |
Original Signature
Termination of terms over the following signature is verified: rev, reverse, true, lt, tail, 0, s, if, undefined, length, false, head, cons, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| lt#(s(x), s(y)) | → | lt#(x, y) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| length#(cons(x, l)) | → | length#(l) |
Rewrite Rules
| length(nil) | → | 0 | | length(cons(x, l)) | → | s(length(l)) |
| lt(x, 0) | → | false | | lt(0, s(y)) | → | true |
| lt(s(x), s(y)) | → | lt(x, y) | | head(cons(x, l)) | → | x |
| head(nil) | → | undefined | | tail(nil) | → | nil |
| tail(cons(x, l)) | → | l | | reverse(l) | → | rev(0, l, nil, l) |
| rev(x, l, accu, orig) | → | if(lt(x, length(orig)), x, l, accu, orig) | | if(true, x, l, accu, orig) | → | rev(s(x), tail(l), cons(head(l), accu), orig) |
| if(false, x, l, accu, orig) | → | accu |
Original Signature
Termination of terms over the following signature is verified: rev, reverse, true, lt, tail, 0, s, if, undefined, length, false, head, cons, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| length#(cons(x, l)) | → | length#(l) |