YES
The TRS could be proven terminating. The proof took 367 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (68ms).
| – Problem 2 was processed with processor PolynomialLinearRange4 (62ms).
| – Problem 3 was processed with processor PolynomialLinearRange4 (110ms).
| | – Problem 4 was processed with processor DependencyGraph (0ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U12#(y', y, x, x') | → | plus#(x', y') | | plus#(x, y) | → | U01#(x, y, x) |
| U11#(s(x'), y, x) | → | T(y) | | plus#(x, y) | → | U11#(x, y, x) |
| fib#(s(x)) | → | U31#(fib(x), x) | | fib#(s(x)) | → | fib#(x) |
| U11#(s(x'), y, x) | → | U12#(y, y, x, x') | | U01#(0, y, x) | → | U02#(y, y, x) |
| U12#(y', y, x, x') | → | T(x') | | U01#(0, y, x) | → | T(y) |
| U31#(pair(y, z), x) | → | plus#(y, z) |
Rewrite Rules
| plus(x, y) | → | U01(x, y, x) | | U01(0, y, x) | → | U02(y, y, x) |
| U02(y', y, x) | → | y' | | plus(x, y) | → | U11(x, y, x) |
| U11(s(x'), y, x) | → | U12(y, y, x, x') | | U12(y', y, x, x') | → | s(plus(x', y')) |
| fib(0) | → | pair(0, s(0)) | | fib(s(x)) | → | U31(fib(x), x) |
| U31(pair(y, z), x) | → | pair(z, plus(y, z)) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, pair, fib
Strategy
Context-sensitive strategy:
μ(T) = μ(0) = ∅
μ(U11#) = μ(U12#) = μ(U31#) = μ(fib) = μ(s) = μ(U01) = μ(U02) = μ(U11) = μ(U12) = μ(fib#) = μ(U31) = μ(U02#) = μ(U01#) = {1}
μ(plus) = μ(pair) = μ(plus#) = {1, 2}
The following SCCs where found
| U12#(y', y, x, x') → plus#(x', y') | plus#(x, y) → U11#(x, y, x) |
| U11#(s(x'), y, x) → U12#(y, y, x, x') |
Problem 2: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| plus(x, y) | → | U01(x, y, x) | | U01(0, y, x) | → | U02(y, y, x) |
| U02(y', y, x) | → | y' | | plus(x, y) | → | U11(x, y, x) |
| U11(s(x'), y, x) | → | U12(y, y, x, x') | | U12(y', y, x, x') | → | s(plus(x', y')) |
| fib(0) | → | pair(0, s(0)) | | fib(s(x)) | → | U31(fib(x), x) |
| U31(pair(y, z), x) | → | pair(z, plus(y, z)) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, pair, fib
Strategy
Context-sensitive strategy:
μ(T) = μ(0) = ∅
μ(U11#) = μ(U12#) = μ(U31#) = μ(fib) = μ(s) = μ(U01) = μ(U02) = μ(U11) = μ(U12) = μ(U31) = μ(fib#) = μ(U02#) = μ(U01#) = {1}
μ(plus) = μ(pair) = μ(plus#) = {1, 2}
Polynomial Interpretation
- 0: 0
- U01(x,y,z): 0
- U02(x,y,z): 0
- U11(x,y,z): 0
- U12(x1,x2,x3,x4): 0
- U31(x,y): 0
- fib(x): 0
- fib#(x): 2x + 1
- pair(x,y): 0
- plus(x,y): 0
- s(x): x + 1
There are no usable rules
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
| U12#(y', y, x, x') | → | plus#(x', y') | | plus#(x, y) | → | U11#(x, y, x) |
| U11#(s(x'), y, x) | → | U12#(y, y, x, x') |
Rewrite Rules
| plus(x, y) | → | U01(x, y, x) | | U01(0, y, x) | → | U02(y, y, x) |
| U02(y', y, x) | → | y' | | plus(x, y) | → | U11(x, y, x) |
| U11(s(x'), y, x) | → | U12(y, y, x, x') | | U12(y', y, x, x') | → | s(plus(x', y')) |
| fib(0) | → | pair(0, s(0)) | | fib(s(x)) | → | U31(fib(x), x) |
| U31(pair(y, z), x) | → | pair(z, plus(y, z)) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, pair, fib
Strategy
Context-sensitive strategy:
μ(T) = μ(0) = ∅
μ(U11#) = μ(U12#) = μ(U31#) = μ(fib) = μ(s) = μ(U01) = μ(U02) = μ(U11) = μ(U12) = μ(U31) = μ(fib#) = μ(U02#) = μ(U01#) = {1}
μ(plus) = μ(pair) = μ(plus#) = {1, 2}
Polynomial Interpretation
- 0: 2
- U01(x,y,z): z + y
- U02(x,y,z): x
- U11(x,y,z): y + x
- U11#(x,y,z): 2x
- U12(x1,x2,x3,x4): x4 + x1 + 1
- U12#(x1,x2,x3,x4): 2x4 + 1
- U31(x,y): 3
- fib(x): 3
- pair(x,y): 3
- plus(x,y): y + x
- plus#(x,y): 2x
- s(x): x + 1
Standard Usable rules
| fib(s(x)) | → | U31(fib(x), x) | | U12(y', y, x, x') | → | s(plus(x', y')) |
| plus(x, y) | → | U01(x, y, x) | | U01(0, y, x) | → | U02(y, y, x) |
| U02(y', y, x) | → | y' | | U31(pair(y, z), x) | → | pair(z, plus(y, z)) |
| fib(0) | → | pair(0, s(0)) | | U11(s(x'), y, x) | → | U12(y, y, x, x') |
| plus(x, y) | → | U11(x, y, x) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| U12#(y', y, x, x') | → | plus#(x', y') | | U11#(s(x'), y, x) | → | U12#(y, y, x, x') |
Problem 4: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| plus#(x, y) | → | U11#(x, y, x) |
Rewrite Rules
| plus(x, y) | → | U01(x, y, x) | | U01(0, y, x) | → | U02(y, y, x) |
| U02(y', y, x) | → | y' | | plus(x, y) | → | U11(x, y, x) |
| U11(s(x'), y, x) | → | U12(y, y, x, x') | | U12(y', y, x, x') | → | s(plus(x', y')) |
| fib(0) | → | pair(0, s(0)) | | fib(s(x)) | → | U31(fib(x), x) |
| U31(pair(y, z), x) | → | pair(z, plus(y, z)) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, pair, fib
Strategy
Context-sensitive strategy:
μ(T) = μ(0) = ∅
μ(U11#) = μ(U12#) = μ(U31#) = μ(fib) = μ(s) = μ(U01) = μ(U02) = μ(U11) = μ(U12) = μ(fib#) = μ(U31) = μ(U02#) = μ(U01#) = {1}
μ(plus) = μ(pair) = μ(plus#) = {1, 2}
There are no SCCs!