TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60019 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (95ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor SubtermCriterion (0ms).
| – Problem 4 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (2ms), PolynomialLinearRange4iUR (249ms), DependencyGraph (2ms), PolynomialLinearRange8NegiUR (3640ms), DependencyGraph (2ms), ReductionPairSAT (timeout)].
| – Problem 5 was processed with processor SubtermCriterion (1ms).
The following open problems remain:
Open Dependency Pair Problem 4
Dependency Pairs
| if#(true, c, s(s(x)), a, b) | → | if#(lt(s(c), s(s(x))), s(c), s(s(x)), b, c) |
Rewrite Rules
| lt(0, s(x)) | → | true | | lt(x, 0) | → | false |
| lt(s(x), s(y)) | → | lt(x, y) | | fibo(0) | → | fib(0) |
| fibo(s(0)) | → | fib(s(0)) | | fibo(s(s(x))) | → | sum(fibo(s(x)), fibo(x)) |
| fib(0) | → | s(0) | | fib(s(0)) | → | s(0) |
| fib(s(s(x))) | → | if(true, 0, s(s(x)), 0, 0) | | if(true, c, s(s(x)), a, b) | → | if(lt(s(c), s(s(x))), s(c), s(s(x)), b, c) |
| if(false, c, s(s(x)), a, b) | → | sum(fibo(a), fibo(b)) | | sum(x, 0) | → | x |
| sum(x, s(y)) | → | s(sum(x, y)) |
Original Signature
Termination of terms over the following signature is verified: 0, s, if, sum, false, true, fibo, lt, fib
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| if#(true, c, s(s(x)), a, b) | → | lt#(s(c), s(s(x))) | | if#(false, c, s(s(x)), a, b) | → | fibo#(b) |
| sum#(x, s(y)) | → | sum#(x, y) | | fib#(s(s(x))) | → | if#(true, 0, s(s(x)), 0, 0) |
| fibo#(s(s(x))) | → | fibo#(x) | | lt#(s(x), s(y)) | → | lt#(x, y) |
| if#(true, c, s(s(x)), a, b) | → | if#(lt(s(c), s(s(x))), s(c), s(s(x)), b, c) | | fibo#(s(s(x))) | → | sum#(fibo(s(x)), fibo(x)) |
| if#(false, c, s(s(x)), a, b) | → | fibo#(a) | | fibo#(s(0)) | → | fib#(s(0)) |
| fibo#(0) | → | fib#(0) | | if#(false, c, s(s(x)), a, b) | → | sum#(fibo(a), fibo(b)) |
| fibo#(s(s(x))) | → | fibo#(s(x)) |
Rewrite Rules
| lt(0, s(x)) | → | true | | lt(x, 0) | → | false |
| lt(s(x), s(y)) | → | lt(x, y) | | fibo(0) | → | fib(0) |
| fibo(s(0)) | → | fib(s(0)) | | fibo(s(s(x))) | → | sum(fibo(s(x)), fibo(x)) |
| fib(0) | → | s(0) | | fib(s(0)) | → | s(0) |
| fib(s(s(x))) | → | if(true, 0, s(s(x)), 0, 0) | | if(true, c, s(s(x)), a, b) | → | if(lt(s(c), s(s(x))), s(c), s(s(x)), b, c) |
| if(false, c, s(s(x)), a, b) | → | sum(fibo(a), fibo(b)) | | sum(x, 0) | → | x |
| sum(x, s(y)) | → | s(sum(x, y)) |
Original Signature
Termination of terms over the following signature is verified: 0, s, if, true, false, sum, fibo, lt, fib
Strategy
The following SCCs where found
| sum#(x, s(y)) → sum#(x, y) |
| fibo#(s(s(x))) → fibo#(x) | fibo#(s(s(x))) → fibo#(s(x)) |
| lt#(s(x), s(y)) → lt#(x, y) |
| if#(true, c, s(s(x)), a, b) → if#(lt(s(c), s(s(x))), s(c), s(s(x)), b, c) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| lt#(s(x), s(y)) | → | lt#(x, y) |
Rewrite Rules
| lt(0, s(x)) | → | true | | lt(x, 0) | → | false |
| lt(s(x), s(y)) | → | lt(x, y) | | fibo(0) | → | fib(0) |
| fibo(s(0)) | → | fib(s(0)) | | fibo(s(s(x))) | → | sum(fibo(s(x)), fibo(x)) |
| fib(0) | → | s(0) | | fib(s(0)) | → | s(0) |
| fib(s(s(x))) | → | if(true, 0, s(s(x)), 0, 0) | | if(true, c, s(s(x)), a, b) | → | if(lt(s(c), s(s(x))), s(c), s(s(x)), b, c) |
| if(false, c, s(s(x)), a, b) | → | sum(fibo(a), fibo(b)) | | sum(x, 0) | → | x |
| sum(x, s(y)) | → | s(sum(x, y)) |
Original Signature
Termination of terms over the following signature is verified: 0, s, if, true, false, sum, fibo, lt, fib
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
| sum#(x, s(y)) | → | sum#(x, y) |
Rewrite Rules
| lt(0, s(x)) | → | true | | lt(x, 0) | → | false |
| lt(s(x), s(y)) | → | lt(x, y) | | fibo(0) | → | fib(0) |
| fibo(s(0)) | → | fib(s(0)) | | fibo(s(s(x))) | → | sum(fibo(s(x)), fibo(x)) |
| fib(0) | → | s(0) | | fib(s(0)) | → | s(0) |
| fib(s(s(x))) | → | if(true, 0, s(s(x)), 0, 0) | | if(true, c, s(s(x)), a, b) | → | if(lt(s(c), s(s(x))), s(c), s(s(x)), b, c) |
| if(false, c, s(s(x)), a, b) | → | sum(fibo(a), fibo(b)) | | sum(x, 0) | → | x |
| sum(x, s(y)) | → | s(sum(x, y)) |
Original Signature
Termination of terms over the following signature is verified: 0, s, if, true, false, sum, fibo, lt, fib
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| sum#(x, s(y)) | → | sum#(x, y) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| fibo#(s(s(x))) | → | fibo#(x) | | fibo#(s(s(x))) | → | fibo#(s(x)) |
Rewrite Rules
| lt(0, s(x)) | → | true | | lt(x, 0) | → | false |
| lt(s(x), s(y)) | → | lt(x, y) | | fibo(0) | → | fib(0) |
| fibo(s(0)) | → | fib(s(0)) | | fibo(s(s(x))) | → | sum(fibo(s(x)), fibo(x)) |
| fib(0) | → | s(0) | | fib(s(0)) | → | s(0) |
| fib(s(s(x))) | → | if(true, 0, s(s(x)), 0, 0) | | if(true, c, s(s(x)), a, b) | → | if(lt(s(c), s(s(x))), s(c), s(s(x)), b, c) |
| if(false, c, s(s(x)), a, b) | → | sum(fibo(a), fibo(b)) | | sum(x, 0) | → | x |
| sum(x, s(y)) | → | s(sum(x, y)) |
Original Signature
Termination of terms over the following signature is verified: 0, s, if, true, false, sum, fibo, lt, fib
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| fibo#(s(s(x))) | → | fibo#(x) | | fibo#(s(s(x))) | → | fibo#(s(x)) |