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