TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60001 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (47ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor BackwardInstantiation (4ms).
| | – Problem 6 was processed with processor BackwardInstantiation (1ms).
| | | – Problem 7 was processed with processor Propagation (2ms).
| | | | – Problem 8 remains open; application of the following processors failed [ForwardNarrowing (0ms), BackwardInstantiation (1ms), ForwardInstantiation (1ms), Propagation (1ms)].
| – Problem 4 was processed with processor PolynomialLinearRange4iUR (73ms).
| | – Problem 5 was processed with processor PolynomialLinearRange4iUR (23ms).
The following open problems remain:
Open Dependency Pair Problem 3
Dependency Pairs
| if#(false, x, y, z) | → | gen#(x, y, s(z)) | | gen#(x, y, z) | → | if#(ge(z, x), x, y, z) |
Rewrite Rules
| times(x, y) | → | sum(generate(x, y)) | | generate(x, y) | → | gen(x, y, 0) |
| gen(x, y, z) | → | if(ge(z, x), x, y, z) | | if(true, x, y, z) | → | nil |
| if(false, x, y, z) | → | cons(y, gen(x, y, s(z))) | | sum(nil) | → | 0 |
| sum(cons(0, xs)) | → | sum(xs) | | sum(cons(s(x), xs)) | → | s(sum(cons(x, xs))) |
| ge(x, 0) | → | true | | ge(0, s(y)) | → | false |
| ge(s(x), s(y)) | → | ge(x, y) |
Original Signature
Termination of terms over the following signature is verified: gen, 0, s, generate, times, if, false, true, sum, ge, cons, nil
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| if#(false, x, y, z) | → | gen#(x, y, s(z)) | | gen#(x, y, z) | → | if#(ge(z, x), x, y, z) |
| sum#(cons(0, xs)) | → | sum#(xs) | | gen#(x, y, z) | → | ge#(z, x) |
| generate#(x, y) | → | gen#(x, y, 0) | | sum#(cons(s(x), xs)) | → | sum#(cons(x, xs)) |
| ge#(s(x), s(y)) | → | ge#(x, y) | | times#(x, y) | → | generate#(x, y) |
| times#(x, y) | → | sum#(generate(x, y)) |
Rewrite Rules
| times(x, y) | → | sum(generate(x, y)) | | generate(x, y) | → | gen(x, y, 0) |
| gen(x, y, z) | → | if(ge(z, x), x, y, z) | | if(true, x, y, z) | → | nil |
| if(false, x, y, z) | → | cons(y, gen(x, y, s(z))) | | sum(nil) | → | 0 |
| sum(cons(0, xs)) | → | sum(xs) | | sum(cons(s(x), xs)) | → | s(sum(cons(x, xs))) |
| ge(x, 0) | → | true | | ge(0, s(y)) | → | false |
| ge(s(x), s(y)) | → | ge(x, y) |
Original Signature
Termination of terms over the following signature is verified: gen, 0, generate, s, times, if, sum, true, false, ge, nil, cons
Strategy
The following SCCs where found
| sum#(cons(0, xs)) → sum#(xs) | sum#(cons(s(x), xs)) → sum#(cons(x, xs)) |
| if#(false, x, y, z) → gen#(x, y, s(z)) | gen#(x, y, z) → if#(ge(z, x), x, y, z) |
| ge#(s(x), s(y)) → ge#(x, y) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| ge#(s(x), s(y)) | → | ge#(x, y) |
Rewrite Rules
| times(x, y) | → | sum(generate(x, y)) | | generate(x, y) | → | gen(x, y, 0) |
| gen(x, y, z) | → | if(ge(z, x), x, y, z) | | if(true, x, y, z) | → | nil |
| if(false, x, y, z) | → | cons(y, gen(x, y, s(z))) | | sum(nil) | → | 0 |
| sum(cons(0, xs)) | → | sum(xs) | | sum(cons(s(x), xs)) | → | s(sum(cons(x, xs))) |
| ge(x, 0) | → | true | | ge(0, s(y)) | → | false |
| ge(s(x), s(y)) | → | ge(x, y) |
Original Signature
Termination of terms over the following signature is verified: gen, 0, generate, s, times, if, sum, true, false, ge, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| ge#(s(x), s(y)) | → | ge#(x, y) |
Problem 3: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| if#(false, x, y, z) | → | gen#(x, y, s(z)) | | gen#(x, y, z) | → | if#(ge(z, x), x, y, z) |
Rewrite Rules
| times(x, y) | → | sum(generate(x, y)) | | generate(x, y) | → | gen(x, y, 0) |
| gen(x, y, z) | → | if(ge(z, x), x, y, z) | | if(true, x, y, z) | → | nil |
| if(false, x, y, z) | → | cons(y, gen(x, y, s(z))) | | sum(nil) | → | 0 |
| sum(cons(0, xs)) | → | sum(xs) | | sum(cons(s(x), xs)) | → | s(sum(cons(x, xs))) |
| ge(x, 0) | → | true | | ge(0, s(y)) | → | false |
| ge(s(x), s(y)) | → | ge(x, y) |
Original Signature
Termination of terms over the following signature is verified: gen, 0, generate, s, times, if, sum, true, false, ge, nil, cons
Strategy
Instantiation
For all potential predecessors l → r of the rule gen
#(
x,
y,
z) → if
#(ge(
z,
x),
x,
y,
z) on dependency pair chains it holds that:
- gen#(x, y, z) matches r,
- all variables of gen#(x, y, z) are embedded in constructor contexts, i.e., each subterm of gen#(x, y, z), containing a variable is rooted by a constructor symbol.
Thus, gen
#(
x,
y,
z) → if
#(ge(
z,
x),
x,
y,
z) is replaced by instances determined through the above matching. These instances are:
| gen#(_x, _y, s(_z)) → if#(ge(s(_z), _x), _x, _y, s(_z)) |
Problem 6: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| if#(false, x, y, z) | → | gen#(x, y, s(z)) | | gen#(_x, _y, s(_z)) | → | if#(ge(s(_z), _x), _x, _y, s(_z)) |
Rewrite Rules
| times(x, y) | → | sum(generate(x, y)) | | generate(x, y) | → | gen(x, y, 0) |
| gen(x, y, z) | → | if(ge(z, x), x, y, z) | | if(true, x, y, z) | → | nil |
| if(false, x, y, z) | → | cons(y, gen(x, y, s(z))) | | sum(nil) | → | 0 |
| sum(cons(0, xs)) | → | sum(xs) | | sum(cons(s(x), xs)) | → | s(sum(cons(x, xs))) |
| ge(x, 0) | → | true | | ge(0, s(y)) | → | false |
| ge(s(x), s(y)) | → | ge(x, y) |
Original Signature
Termination of terms over the following signature is verified: gen, 0, s, generate, times, if, false, true, sum, ge, cons, nil
Strategy
Instantiation
For all potential predecessors l → r of the rule gen
#(
_x,
_y, s(
_z)) → if
#(ge(s(
_z),
_x),
_x,
_y, s(
_z)) on dependency pair chains it holds that:
- gen#(_x, _y, s(_z)) matches r,
- all variables of gen#(_x, _y, s(_z)) are embedded in constructor contexts, i.e., each subterm of gen#(_x, _y, s(_z)), containing a variable is rooted by a constructor symbol.
Thus, gen
#(
_x,
_y, s(
_z)) → if
#(ge(s(
_z),
_x),
_x,
_y, s(
_z)) is replaced by instances determined through the above matching. These instances are:
| gen#(x, y, s(z)) → if#(ge(s(z), x), x, y, s(z)) |
Problem 7: Propagation
Dependency Pair Problem
Dependency Pairs
| if#(false, x, y, z) | → | gen#(x, y, s(z)) | | gen#(x, y, s(z)) | → | if#(ge(s(z), x), x, y, s(z)) |
Rewrite Rules
| times(x, y) | → | sum(generate(x, y)) | | generate(x, y) | → | gen(x, y, 0) |
| gen(x, y, z) | → | if(ge(z, x), x, y, z) | | if(true, x, y, z) | → | nil |
| if(false, x, y, z) | → | cons(y, gen(x, y, s(z))) | | sum(nil) | → | 0 |
| sum(cons(0, xs)) | → | sum(xs) | | sum(cons(s(x), xs)) | → | s(sum(cons(x, xs))) |
| ge(x, 0) | → | true | | ge(0, s(y)) | → | false |
| ge(s(x), s(y)) | → | ge(x, y) |
Original Signature
Termination of terms over the following signature is verified: gen, 0, generate, s, times, if, sum, true, false, ge, nil, cons
Strategy
The dependency pairs if
#(false,
x,
y,
z) → gen
#(
x,
y, s(
z)) and gen
#(
x,
y, s(
z)) → if
#(ge(s(
z),
x),
x,
y, s(
z)) are consolidated into the rule if
#(false,
x,
y,
z) → if
#(ge(s(
z),
x),
x,
y, s(
z)) .
This is possible as
- all subterms of gen#(x, y, s(z)) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in gen#(x, y, s(z)), but non-replacing in both if#(false, x, y, z) and if#(ge(s(z), x), x, y, s(z))
The dependency pairs if
#(false,
x,
y,
z) → gen
#(
x,
y, s(
z)) and gen
#(
x,
y, s(
z)) → if
#(ge(s(
z),
x),
x,
y, s(
z)) are consolidated into the rule if
#(false,
x,
y,
z) → if
#(ge(s(
z),
x),
x,
y, s(
z)) .
This is possible as
- all subterms of gen#(x, y, s(z)) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in gen#(x, y, s(z)), but non-replacing in both if#(false, x, y, z) and if#(ge(s(z), x), x, y, s(z))
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| if#(false, x, y, z) → gen#(x, y, s(z)) | if#(false, x, y, z) → if#(ge(s(z), x), x, y, s(z)) |
| gen#(x, y, s(z)) → if#(ge(s(z), x), x, y, s(z)) | |
Problem 4: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| sum#(cons(0, xs)) | → | sum#(xs) | | sum#(cons(s(x), xs)) | → | sum#(cons(x, xs)) |
Rewrite Rules
| times(x, y) | → | sum(generate(x, y)) | | generate(x, y) | → | gen(x, y, 0) |
| gen(x, y, z) | → | if(ge(z, x), x, y, z) | | if(true, x, y, z) | → | nil |
| if(false, x, y, z) | → | cons(y, gen(x, y, s(z))) | | sum(nil) | → | 0 |
| sum(cons(0, xs)) | → | sum(xs) | | sum(cons(s(x), xs)) | → | s(sum(cons(x, xs))) |
| ge(x, 0) | → | true | | ge(0, s(y)) | → | false |
| ge(s(x), s(y)) | → | ge(x, y) |
Original Signature
Termination of terms over the following signature is verified: gen, 0, generate, s, times, if, sum, true, false, ge, nil, cons
Strategy
Polynomial Interpretation
- 0: 0
- cons(x,y): 3y + x
- false: 0
- ge(x,y): 0
- gen(x,y,z): 0
- generate(x,y): 0
- if(x1,x2,x3,x4): 0
- nil: 0
- s(x): 3x + 1
- sum(x): 0
- sum#(x): 3x
- times(x,y): 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:
| sum#(cons(s(x), xs)) | → | sum#(cons(x, xs)) |
Problem 5: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| sum#(cons(0, xs)) | → | sum#(xs) |
Rewrite Rules
| times(x, y) | → | sum(generate(x, y)) | | generate(x, y) | → | gen(x, y, 0) |
| gen(x, y, z) | → | if(ge(z, x), x, y, z) | | if(true, x, y, z) | → | nil |
| if(false, x, y, z) | → | cons(y, gen(x, y, s(z))) | | sum(nil) | → | 0 |
| sum(cons(0, xs)) | → | sum(xs) | | sum(cons(s(x), xs)) | → | s(sum(cons(x, xs))) |
| ge(x, 0) | → | true | | ge(0, s(y)) | → | false |
| ge(s(x), s(y)) | → | ge(x, y) |
Original Signature
Termination of terms over the following signature is verified: gen, 0, s, generate, times, if, false, true, sum, ge, cons, nil
Strategy
Polynomial Interpretation
- 0: 2
- cons(x,y): 2y + 1
- false: 0
- ge(x,y): 0
- gen(x,y,z): 0
- generate(x,y): 0
- if(x1,x2,x3,x4): 0
- nil: 0
- s(x): 0
- sum(x): 0
- sum#(x): 2x
- times(x,y): 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:
| sum#(cons(0, xs)) | → | sum#(xs) |