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