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 (72ms).
| – Problem 2 was processed with processor BackwardInstantiation (3ms).
| | – Problem 4 was processed with processor BackwardInstantiation (5ms).
| | | – Problem 5 was processed with processor ForwardInstantiation (3ms).
| | | | – Problem 6 was processed with processor Propagation (11ms).
| | | | | – Problem 7 was processed with processor BackwardInstantiation (5ms).
| | | | | | – Problem 8 remains open; application of the following processors failed [ForwardInstantiation (5ms), Propagation (5ms)].
| – Problem 3 was processed with processor SubtermCriterion (1ms).
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| count#(n, x) | → | if#(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x)) | | if#(false, false, n, m, x, y) | → | count#(m, x) |
| if#(false, true, n, m, x, y) | → | count#(n, y) |
Rewrite Rules
| isEmpty(empty) | → | true | | isEmpty(node(l, r)) | → | false |
| left(empty) | → | empty | | left(node(l, r)) | → | l |
| right(empty) | → | empty | | right(node(l, r)) | → | r |
| inc(0) | → | s(0) | | inc(s(x)) | → | s(inc(x)) |
| count(n, x) | → | if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x)) | | if(true, b, n, m, x, y) | → | x |
| if(false, false, n, m, x, y) | → | count(m, x) | | if(false, true, n, m, x, y) | → | count(n, y) |
| nrOfNodes(n) | → | count(n, 0) |
Original Signature
Termination of terms over the following signature is verified: nrOfNodes, count, true, isEmpty, node, 0, s, inc, if, empty, false, left, right
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| count#(n, x) | → | if#(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x)) | | if#(false, false, n, m, x, y) | → | count#(m, x) |
| nrOfNodes#(n) | → | count#(n, 0) | | count#(n, x) | → | isEmpty#(left(n)) |
| if#(false, true, n, m, x, y) | → | count#(n, y) | | count#(n, x) | → | isEmpty#(n) |
| count#(n, x) | → | right#(n) | | count#(n, x) | → | left#(n) |
| inc#(s(x)) | → | inc#(x) | | count#(n, x) | → | inc#(x) |
| count#(n, x) | → | left#(left(n)) | | count#(n, x) | → | right#(left(n)) |
Rewrite Rules
| isEmpty(empty) | → | true | | isEmpty(node(l, r)) | → | false |
| left(empty) | → | empty | | left(node(l, r)) | → | l |
| right(empty) | → | empty | | right(node(l, r)) | → | r |
| inc(0) | → | s(0) | | inc(s(x)) | → | s(inc(x)) |
| count(n, x) | → | if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x)) | | if(true, b, n, m, x, y) | → | x |
| if(false, false, n, m, x, y) | → | count(m, x) | | if(false, true, n, m, x, y) | → | count(n, y) |
| nrOfNodes(n) | → | count(n, 0) |
Original Signature
Termination of terms over the following signature is verified: nrOfNodes, count, true, isEmpty, node, 0, s, inc, if, empty, false, left, right
Strategy
The following SCCs where found
| if#(false, false, n, m, x, y) → count#(m, x) | count#(n, x) → if#(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x)) |
| if#(false, true, n, m, x, y) → count#(n, y) |
Problem 2: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| if#(false, false, n, m, x, y) | → | count#(m, x) | | count#(n, x) | → | if#(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x)) |
| if#(false, true, n, m, x, y) | → | count#(n, y) |
Rewrite Rules
| isEmpty(empty) | → | true | | isEmpty(node(l, r)) | → | false |
| left(empty) | → | empty | | left(node(l, r)) | → | l |
| right(empty) | → | empty | | right(node(l, r)) | → | r |
| inc(0) | → | s(0) | | inc(s(x)) | → | s(inc(x)) |
| count(n, x) | → | if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x)) | | if(true, b, n, m, x, y) | → | x |
| if(false, false, n, m, x, y) | → | count(m, x) | | if(false, true, n, m, x, y) | → | count(n, y) |
| nrOfNodes(n) | → | count(n, 0) |
Original Signature
Termination of terms over the following signature is verified: nrOfNodes, count, true, isEmpty, node, 0, s, inc, if, empty, false, left, right
Strategy
Instantiation
For all potential predecessors l → r of the rule count
#(
n,
x) → if
#(isEmpty(
n), isEmpty(left(
n)), right(
n), node(left(left(
n)), node(right(left(
n)), right(
n))),
x, inc(
x)) on dependency pair chains it holds that:
- count#(n, x) matches r,
- all variables of count#(n, x) are embedded in constructor contexts, i.e., each subterm of count#(n, x), containing a variable is rooted by a constructor symbol.
Thus, count
#(
n,
x) → if
#(isEmpty(
n), isEmpty(left(
n)), right(
n), node(left(left(
n)), node(right(left(
n)), right(
n))),
x, inc(
x)) is replaced by instances determined through the above matching. These instances are:
| count#(_n, _y) → if#(isEmpty(_n), isEmpty(left(_n)), right(_n), node(left(left(_n)), node(right(left(_n)), right(_n))), _y, inc(_y)) | count#(_m, _x) → if#(isEmpty(_m), isEmpty(left(_m)), right(_m), node(left(left(_m)), node(right(left(_m)), right(_m))), _x, inc(_x)) |
Problem 4: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| if#(false, false, n, m, x, y) | → | count#(m, x) | | if#(false, true, n, m, x, y) | → | count#(n, y) |
| count#(_n, _y) | → | if#(isEmpty(_n), isEmpty(left(_n)), right(_n), node(left(left(_n)), node(right(left(_n)), right(_n))), _y, inc(_y)) | | count#(_m, _x) | → | if#(isEmpty(_m), isEmpty(left(_m)), right(_m), node(left(left(_m)), node(right(left(_m)), right(_m))), _x, inc(_x)) |
Rewrite Rules
| isEmpty(empty) | → | true | | isEmpty(node(l, r)) | → | false |
| left(empty) | → | empty | | left(node(l, r)) | → | l |
| right(empty) | → | empty | | right(node(l, r)) | → | r |
| inc(0) | → | s(0) | | inc(s(x)) | → | s(inc(x)) |
| count(n, x) | → | if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x)) | | if(true, b, n, m, x, y) | → | x |
| if(false, false, n, m, x, y) | → | count(m, x) | | if(false, true, n, m, x, y) | → | count(n, y) |
| nrOfNodes(n) | → | count(n, 0) |
Original Signature
Termination of terms over the following signature is verified: nrOfNodes, count, true, isEmpty, node, 0, s, inc, if, empty, false, left, right
Strategy
Instantiation
For all potential predecessors l → r of the rule count
#(
_n,
_y) → if
#(isEmpty(
_n), isEmpty(left(
_n)), right(
_n), node(left(left(
_n)), node(right(left(
_n)), right(
_n))),
_y, inc(
_y)) on dependency pair chains it holds that:
- count#(_n, _y) matches r,
- all variables of count#(_n, _y) are embedded in constructor contexts, i.e., each subterm of count#(_n, _y), containing a variable is rooted by a constructor symbol.
Thus, count
#(
_n,
_y) → if
#(isEmpty(
_n), isEmpty(left(
_n)), right(
_n), node(left(left(
_n)), node(right(left(
_n)), right(
_n))),
_y, inc(
_y)) is replaced by instances determined through the above matching. These instances are:
| count#(m, x) → if#(isEmpty(m), isEmpty(left(m)), right(m), node(left(left(m)), node(right(left(m)), right(m))), x, inc(x)) | count#(n, y) → if#(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), y, inc(y)) |
Instantiation
For all potential predecessors l → r of the rule count
#(
_m,
_x) → if
#(isEmpty(
_m), isEmpty(left(
_m)), right(
_m), node(left(left(
_m)), node(right(left(
_m)), right(
_m))),
_x, inc(
_x)) on dependency pair chains it holds that:
- count#(_m, _x) matches r,
- all variables of count#(_m, _x) are embedded in constructor contexts, i.e., each subterm of count#(_m, _x), containing a variable is rooted by a constructor symbol.
Thus, count
#(
_m,
_x) → if
#(isEmpty(
_m), isEmpty(left(
_m)), right(
_m), node(left(left(
_m)), node(right(left(
_m)), right(
_m))),
_x, inc(
_x)) is replaced by instances determined through the above matching. These instances are:
| count#(m, x) → if#(isEmpty(m), isEmpty(left(m)), right(m), node(left(left(m)), node(right(left(m)), right(m))), x, inc(x)) | count#(n, y) → if#(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), y, inc(y)) |
Problem 5: ForwardInstantiation
Dependency Pair Problem
Dependency Pairs
| if#(false, false, n, m, x, y) | → | count#(m, x) | | if#(false, true, n, m, x, y) | → | count#(n, y) |
| count#(m, x) | → | if#(isEmpty(m), isEmpty(left(m)), right(m), node(left(left(m)), node(right(left(m)), right(m))), x, inc(x)) | | count#(n, y) | → | if#(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), y, inc(y)) |
Rewrite Rules
| isEmpty(empty) | → | true | | isEmpty(node(l, r)) | → | false |
| left(empty) | → | empty | | left(node(l, r)) | → | l |
| right(empty) | → | empty | | right(node(l, r)) | → | r |
| inc(0) | → | s(0) | | inc(s(x)) | → | s(inc(x)) |
| count(n, x) | → | if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x)) | | if(true, b, n, m, x, y) | → | x |
| if(false, false, n, m, x, y) | → | count(m, x) | | if(false, true, n, m, x, y) | → | count(n, y) |
| nrOfNodes(n) | → | count(n, 0) |
Original Signature
Termination of terms over the following signature is verified: nrOfNodes, count, true, isEmpty, node, 0, s, inc, if, empty, false, left, right
Strategy
Instantiation
For all potential successors l → r of the rule if
#(false, false,
n,
m,
x,
y) → count
#(
m,
x) on dependency pair chains it holds that:
- count#(m, x) matches l,
- all variables of count#(m, x) are embedded in constructor contexts, i.e., each subterm of count#(m, x) containing a variable is rooted by a constructor symbol.
Thus, if
#(false, false,
n,
m,
x,
y) → count
#(
m,
x) is replaced by instances determined through the above matching. These instances are:
| if#(false, false, n, m, x, y) → count#(m, x) | if#(false, false, m, m, x, x) → count#(m, x) |
Instantiation
For all potential successors l → r of the rule if
#(false, true,
n,
m,
x,
y) → count
#(
n,
y) on dependency pair chains it holds that:
- count#(n, y) matches l,
- all variables of count#(n, y) are embedded in constructor contexts, i.e., each subterm of count#(n, y) containing a variable is rooted by a constructor symbol.
Thus, if
#(false, true,
n,
m,
x,
y) → count
#(
n,
y) is replaced by instances determined through the above matching. These instances are:
| if#(false, true, n, m, x, y) → count#(n, y) | if#(false, true, n, n, y, y) → count#(n, y) |
Problem 6: Propagation
Dependency Pair Problem
Dependency Pairs
| if#(false, false, n, m, x, y) | → | count#(m, x) | | if#(false, true, n, m, x, y) | → | count#(n, y) |
| if#(false, false, m, m, x, x) | → | count#(m, x) | | count#(m, x) | → | if#(isEmpty(m), isEmpty(left(m)), right(m), node(left(left(m)), node(right(left(m)), right(m))), x, inc(x)) |
| count#(n, y) | → | if#(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), y, inc(y)) | | if#(false, true, n, n, y, y) | → | count#(n, y) |
Rewrite Rules
| isEmpty(empty) | → | true | | isEmpty(node(l, r)) | → | false |
| left(empty) | → | empty | | left(node(l, r)) | → | l |
| right(empty) | → | empty | | right(node(l, r)) | → | r |
| inc(0) | → | s(0) | | inc(s(x)) | → | s(inc(x)) |
| count(n, x) | → | if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x)) | | if(true, b, n, m, x, y) | → | x |
| if(false, false, n, m, x, y) | → | count(m, x) | | if(false, true, n, m, x, y) | → | count(n, y) |
| nrOfNodes(n) | → | count(n, 0) |
Original Signature
Termination of terms over the following signature is verified: nrOfNodes, count, true, isEmpty, node, 0, s, inc, if, empty, false, left, right
Strategy
The dependency pairs if
#(false, false,
n,
m,
x,
y) → count
#(
m,
x) and count
#(
m,
x) → if
#(isEmpty(
m), isEmpty(left(
m)), right(
m), node(left(left(
m)), node(right(left(
m)), right(
m))),
x, inc(
x)) are consolidated into the rule if
#(false, false,
n,
m,
x,
y) → if
#(isEmpty(
m), isEmpty(left(
m)), right(
m), node(left(left(
m)), node(right(left(
m)), right(
m))),
x, inc(
x)) .
This is possible as
- all subterms of count#(m, x) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in count#(m, x), but non-replacing in both if#(false, false, n, m, x, y) and if#(isEmpty(m), isEmpty(left(m)), right(m), node(left(left(m)), node(right(left(m)), right(m))), x, inc(x))
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| if#(false, false, n, m, x, y) → count#(m, x) | if#(false, false, n, m, x, y) → if#(isEmpty(m), isEmpty(left(m)), right(m), node(left(left(m)), node(right(left(m)), right(m))), x, inc(x)) |
| count#(m, x) → if#(isEmpty(m), isEmpty(left(m)), right(m), node(left(left(m)), node(right(left(m)), right(m))), x, inc(x)) | |
Problem 7: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| if#(false, true, n, m, x, y) | → | count#(n, y) | | if#(false, false, m, m, x, x) | → | count#(m, x) |
| count#(n, y) | → | if#(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), y, inc(y)) | | if#(false, false, n, m, x, y) | → | if#(isEmpty(m), isEmpty(left(m)), right(m), node(left(left(m)), node(right(left(m)), right(m))), x, inc(x)) |
| if#(false, true, n, n, y, y) | → | count#(n, y) |
Rewrite Rules
| isEmpty(empty) | → | true | | isEmpty(node(l, r)) | → | false |
| left(empty) | → | empty | | left(node(l, r)) | → | l |
| right(empty) | → | empty | | right(node(l, r)) | → | r |
| inc(0) | → | s(0) | | inc(s(x)) | → | s(inc(x)) |
| count(n, x) | → | if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x)) | | if(true, b, n, m, x, y) | → | x |
| if(false, false, n, m, x, y) | → | count(m, x) | | if(false, true, n, m, x, y) | → | count(n, y) |
| nrOfNodes(n) | → | count(n, 0) |
Original Signature
Termination of terms over the following signature is verified: nrOfNodes, count, true, isEmpty, node, 0, s, inc, if, empty, false, left, right
Strategy
Instantiation
For all potential predecessors l → r of the rule count
#(
n,
y) → if
#(isEmpty(
n), isEmpty(left(
n)), right(
n), node(left(left(
n)), node(right(left(
n)), right(
n))),
y, inc(
y)) on dependency pair chains it holds that:
- count#(n, y) matches r,
- all variables of count#(n, y) are embedded in constructor contexts, i.e., each subterm of count#(n, y), containing a variable is rooted by a constructor symbol.
Thus, count
#(
n,
y) → if
#(isEmpty(
n), isEmpty(left(
n)), right(
n), node(left(left(
n)), node(right(left(
n)), right(
n))),
y, inc(
y)) is replaced by instances determined through the above matching. These instances are:
| count#(m, x) → if#(isEmpty(m), isEmpty(left(m)), right(m), node(left(left(m)), node(right(left(m)), right(m))), x, inc(x)) | count#(_n, _y) → if#(isEmpty(_n), isEmpty(left(_n)), right(_n), node(left(left(_n)), node(right(left(_n)), right(_n))), _y, inc(_y)) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| isEmpty(empty) | → | true | | isEmpty(node(l, r)) | → | false |
| left(empty) | → | empty | | left(node(l, r)) | → | l |
| right(empty) | → | empty | | right(node(l, r)) | → | r |
| inc(0) | → | s(0) | | inc(s(x)) | → | s(inc(x)) |
| count(n, x) | → | if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x)) | | if(true, b, n, m, x, y) | → | x |
| if(false, false, n, m, x, y) | → | count(m, x) | | if(false, true, n, m, x, y) | → | count(n, y) |
| nrOfNodes(n) | → | count(n, 0) |
Original Signature
Termination of terms over the following signature is verified: nrOfNodes, count, true, isEmpty, node, 0, s, inc, if, empty, false, left, right
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed: