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 (25ms).
| – Problem 2 was processed with processor BackwardInstantiation (2ms).
| | – Problem 3 remains open; application of the following processors failed [ForwardInstantiation (4ms), Propagation (1ms), ForwardNarrowing (0ms), BackwardInstantiation (1ms), ForwardInstantiation (1ms), Propagation (0ms)].
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| ifappend#(l1, l2, false) | → | append#(tl(l1), l2) | | append#(l1, l2) | → | ifappend#(l1, l2, is_empty(l1)) |
Rewrite Rules
| is_empty(nil) | → | true | | is_empty(cons(x, l)) | → | false |
| hd(cons(x, l)) | → | x | | tl(cons(x, l)) | → | cons(x, l) |
| append(l1, l2) | → | ifappend(l1, l2, is_empty(l1)) | | ifappend(l1, l2, true) | → | l2 |
| ifappend(l1, l2, false) | → | cons(hd(l1), append(tl(l1), l2)) |
Original Signature
Termination of terms over the following signature is verified: append, ifappend, tl, false, true, hd, is_empty, cons, nil
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| ifappend#(l1, l2, false) | → | hd#(l1) | | ifappend#(l1, l2, false) | → | append#(tl(l1), l2) |
| ifappend#(l1, l2, false) | → | tl#(l1) | | append#(l1, l2) | → | ifappend#(l1, l2, is_empty(l1)) |
| append#(l1, l2) | → | is_empty#(l1) |
Rewrite Rules
| is_empty(nil) | → | true | | is_empty(cons(x, l)) | → | false |
| hd(cons(x, l)) | → | x | | tl(cons(x, l)) | → | cons(x, l) |
| append(l1, l2) | → | ifappend(l1, l2, is_empty(l1)) | | ifappend(l1, l2, true) | → | l2 |
| ifappend(l1, l2, false) | → | cons(hd(l1), append(tl(l1), l2)) |
Original Signature
Termination of terms over the following signature is verified: append, tl, ifappend, true, false, hd, is_empty, nil, cons
Strategy
The following SCCs where found
| ifappend#(l1, l2, false) → append#(tl(l1), l2) | append#(l1, l2) → ifappend#(l1, l2, is_empty(l1)) |
Problem 2: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| ifappend#(l1, l2, false) | → | append#(tl(l1), l2) | | append#(l1, l2) | → | ifappend#(l1, l2, is_empty(l1)) |
Rewrite Rules
| is_empty(nil) | → | true | | is_empty(cons(x, l)) | → | false |
| hd(cons(x, l)) | → | x | | tl(cons(x, l)) | → | cons(x, l) |
| append(l1, l2) | → | ifappend(l1, l2, is_empty(l1)) | | ifappend(l1, l2, true) | → | l2 |
| ifappend(l1, l2, false) | → | cons(hd(l1), append(tl(l1), l2)) |
Original Signature
Termination of terms over the following signature is verified: append, tl, ifappend, true, false, hd, is_empty, nil, cons
Strategy
Instantiation
For all potential predecessors l → r of the rule append
#(
l1,
l2) → ifappend
#(
l1,
l2, is_empty(
l1)) on dependency pair chains it holds that:
- append#(l1, l2) matches r,
- all variables of append#(l1, l2) are embedded in constructor contexts, i.e., each subterm of append#(l1, l2), containing a variable is rooted by a constructor symbol.
Thus, append
#(
l1,
l2) → ifappend
#(
l1,
l2, is_empty(
l1)) is replaced by instances determined through the above matching. These instances are:
| append#(tl(_l1), _l2) → ifappend#(tl(_l1), _l2, is_empty(tl(_l1))) |