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 (97ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor SubtermCriterion (1ms).
| – Problem 4 was processed with processor BackwardInstantiation (2ms).
| | – Problem 7 was processed with processor BackwardInstantiation (1ms).
| | | – Problem 8 was processed with processor Propagation (3ms).
| | | | – Problem 9 remains open; application of the following processors failed [ForwardNarrowing (0ms), BackwardInstantiation (1ms), ForwardInstantiation (2ms), Propagation (1ms)].
| – Problem 5 was processed with processor SubtermCriterion (0ms).
| – Problem 6 was processed with processor SubtermCriterion (2ms).
The following open problems remain:
Open Dependency Pair Problem 4
Dependency Pairs
| if#(false, false, l, t, n) | → | lessE#(l, t, s(n)) | | lessE#(l, t, n) | → | if#(le(length(l), n), le(length(toList(t)), n), l, t, n) |
Rewrite Rules
| lessElements(l, t) | → | lessE(l, t, 0) | | lessE(l, t, n) | → | if(le(length(l), n), le(length(toList(t)), n), l, t, n) |
| if(true, b, l, t, n) | → | l | | if(false, true, l, t, n) | → | t |
| if(false, false, l, t, n) | → | lessE(l, t, s(n)) | | length(nil) | → | 0 |
| length(cons(n, l)) | → | s(length(l)) | | toList(leaf) | → | nil |
| toList(node(t1, n, t2)) | → | append(toList(t1), cons(n, toList(t2))) | | append(nil, l2) | → | l2 |
| append(cons(n, l1), l2) | → | cons(n, append(l1, l2)) | | le(s(n), 0) | → | false |
| le(0, m) | → | true | | le(s(n), s(m)) | → | le(n, m) |
| a | → | c | | a | → | d |
Original Signature
Termination of terms over the following signature is verified: append, d, c, a, true, lessE, leaf, node, 0, le, s, if, length, false, toList, lessElements, nil, cons
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| toList#(node(t1, n, t2)) | → | toList#(t2) | | le#(s(n), s(m)) | → | le#(n, m) |
| lessE#(l, t, n) | → | length#(l) | | append#(cons(n, l1), l2) | → | append#(l1, l2) |
| lessE#(l, t, n) | → | le#(length(l), n) | | lessE#(l, t, n) | → | toList#(t) |
| lessElements#(l, t) | → | lessE#(l, t, 0) | | toList#(node(t1, n, t2)) | → | append#(toList(t1), cons(n, toList(t2))) |
| if#(false, false, l, t, n) | → | lessE#(l, t, s(n)) | | lessE#(l, t, n) | → | length#(toList(t)) |
| length#(cons(n, l)) | → | length#(l) | | toList#(node(t1, n, t2)) | → | toList#(t1) |
| lessE#(l, t, n) | → | le#(length(toList(t)), n) | | lessE#(l, t, n) | → | if#(le(length(l), n), le(length(toList(t)), n), l, t, n) |
Rewrite Rules
| lessElements(l, t) | → | lessE(l, t, 0) | | lessE(l, t, n) | → | if(le(length(l), n), le(length(toList(t)), n), l, t, n) |
| if(true, b, l, t, n) | → | l | | if(false, true, l, t, n) | → | t |
| if(false, false, l, t, n) | → | lessE(l, t, s(n)) | | length(nil) | → | 0 |
| length(cons(n, l)) | → | s(length(l)) | | toList(leaf) | → | nil |
| toList(node(t1, n, t2)) | → | append(toList(t1), cons(n, toList(t2))) | | append(nil, l2) | → | l2 |
| append(cons(n, l1), l2) | → | cons(n, append(l1, l2)) | | le(s(n), 0) | → | false |
| le(0, m) | → | true | | le(s(n), s(m)) | → | le(n, m) |
| a | → | c | | a | → | d |
Original Signature
Termination of terms over the following signature is verified: append, d, c, a, true, lessE, leaf, node, 0, le, s, if, length, false, toList, lessElements, cons, nil
Strategy
The following SCCs where found
| length#(cons(n, l)) → length#(l) |
| le#(s(n), s(m)) → le#(n, m) |
| append#(cons(n, l1), l2) → append#(l1, l2) |
| if#(false, false, l, t, n) → lessE#(l, t, s(n)) | lessE#(l, t, n) → if#(le(length(l), n), le(length(toList(t)), n), l, t, n) |
| toList#(node(t1, n, t2)) → toList#(t2) | toList#(node(t1, n, t2)) → toList#(t1) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| toList#(node(t1, n, t2)) | → | toList#(t2) | | toList#(node(t1, n, t2)) | → | toList#(t1) |
Rewrite Rules
| lessElements(l, t) | → | lessE(l, t, 0) | | lessE(l, t, n) | → | if(le(length(l), n), le(length(toList(t)), n), l, t, n) |
| if(true, b, l, t, n) | → | l | | if(false, true, l, t, n) | → | t |
| if(false, false, l, t, n) | → | lessE(l, t, s(n)) | | length(nil) | → | 0 |
| length(cons(n, l)) | → | s(length(l)) | | toList(leaf) | → | nil |
| toList(node(t1, n, t2)) | → | append(toList(t1), cons(n, toList(t2))) | | append(nil, l2) | → | l2 |
| append(cons(n, l1), l2) | → | cons(n, append(l1, l2)) | | le(s(n), 0) | → | false |
| le(0, m) | → | true | | le(s(n), s(m)) | → | le(n, m) |
| a | → | c | | a | → | d |
Original Signature
Termination of terms over the following signature is verified: append, d, c, a, true, lessE, leaf, node, 0, le, s, if, length, false, toList, lessElements, cons, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| toList#(node(t1, n, t2)) | → | toList#(t2) | | toList#(node(t1, n, t2)) | → | toList#(t1) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| append#(cons(n, l1), l2) | → | append#(l1, l2) |
Rewrite Rules
| lessElements(l, t) | → | lessE(l, t, 0) | | lessE(l, t, n) | → | if(le(length(l), n), le(length(toList(t)), n), l, t, n) |
| if(true, b, l, t, n) | → | l | | if(false, true, l, t, n) | → | t |
| if(false, false, l, t, n) | → | lessE(l, t, s(n)) | | length(nil) | → | 0 |
| length(cons(n, l)) | → | s(length(l)) | | toList(leaf) | → | nil |
| toList(node(t1, n, t2)) | → | append(toList(t1), cons(n, toList(t2))) | | append(nil, l2) | → | l2 |
| append(cons(n, l1), l2) | → | cons(n, append(l1, l2)) | | le(s(n), 0) | → | false |
| le(0, m) | → | true | | le(s(n), s(m)) | → | le(n, m) |
| a | → | c | | a | → | d |
Original Signature
Termination of terms over the following signature is verified: append, d, c, a, true, lessE, leaf, node, 0, le, s, if, length, false, toList, lessElements, cons, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| append#(cons(n, l1), l2) | → | append#(l1, l2) |
Problem 4: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| if#(false, false, l, t, n) | → | lessE#(l, t, s(n)) | | lessE#(l, t, n) | → | if#(le(length(l), n), le(length(toList(t)), n), l, t, n) |
Rewrite Rules
| lessElements(l, t) | → | lessE(l, t, 0) | | lessE(l, t, n) | → | if(le(length(l), n), le(length(toList(t)), n), l, t, n) |
| if(true, b, l, t, n) | → | l | | if(false, true, l, t, n) | → | t |
| if(false, false, l, t, n) | → | lessE(l, t, s(n)) | | length(nil) | → | 0 |
| length(cons(n, l)) | → | s(length(l)) | | toList(leaf) | → | nil |
| toList(node(t1, n, t2)) | → | append(toList(t1), cons(n, toList(t2))) | | append(nil, l2) | → | l2 |
| append(cons(n, l1), l2) | → | cons(n, append(l1, l2)) | | le(s(n), 0) | → | false |
| le(0, m) | → | true | | le(s(n), s(m)) | → | le(n, m) |
| a | → | c | | a | → | d |
Original Signature
Termination of terms over the following signature is verified: append, d, c, a, true, lessE, leaf, node, 0, le, s, if, length, false, toList, lessElements, cons, nil
Strategy
Instantiation
For all potential predecessors l → r of the rule lessE
#(
l,
t,
n) → if
#(le(length(
l),
n), le(length(toList(
t)),
n),
l,
t,
n) on dependency pair chains it holds that:
- lessE#(l, t, n) matches r,
- all variables of lessE#(l, t, n) are embedded in constructor contexts, i.e., each subterm of lessE#(l, t, n), containing a variable is rooted by a constructor symbol.
Thus, lessE
#(
l,
t,
n) → if
#(le(length(
l),
n), le(length(toList(
t)),
n),
l,
t,
n) is replaced by instances determined through the above matching. These instances are:
| lessE#(_l, _t, s(_n)) → if#(le(length(_l), s(_n)), le(length(toList(_t)), s(_n)), _l, _t, s(_n)) |
Problem 7: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| if#(false, false, l, t, n) | → | lessE#(l, t, s(n)) | | lessE#(_l, _t, s(_n)) | → | if#(le(length(_l), s(_n)), le(length(toList(_t)), s(_n)), _l, _t, s(_n)) |
Rewrite Rules
| lessElements(l, t) | → | lessE(l, t, 0) | | lessE(l, t, n) | → | if(le(length(l), n), le(length(toList(t)), n), l, t, n) |
| if(true, b, l, t, n) | → | l | | if(false, true, l, t, n) | → | t |
| if(false, false, l, t, n) | → | lessE(l, t, s(n)) | | length(nil) | → | 0 |
| length(cons(n, l)) | → | s(length(l)) | | toList(leaf) | → | nil |
| toList(node(t1, n, t2)) | → | append(toList(t1), cons(n, toList(t2))) | | append(nil, l2) | → | l2 |
| append(cons(n, l1), l2) | → | cons(n, append(l1, l2)) | | le(s(n), 0) | → | false |
| le(0, m) | → | true | | le(s(n), s(m)) | → | le(n, m) |
| a | → | c | | a | → | d |
Original Signature
Termination of terms over the following signature is verified: append, d, c, a, true, lessE, leaf, node, 0, le, s, if, length, false, toList, lessElements, nil, cons
Strategy
Instantiation
For all potential predecessors l → r of the rule lessE
#(
_l,
_t, s(
_n)) → if
#(le(length(
_l), s(
_n)), le(length(toList(
_t)), s(
_n)),
_l,
_t, s(
_n)) on dependency pair chains it holds that:
- lessE#(_l, _t, s(_n)) matches r,
- all variables of lessE#(_l, _t, s(_n)) are embedded in constructor contexts, i.e., each subterm of lessE#(_l, _t, s(_n)), containing a variable is rooted by a constructor symbol.
Thus, lessE
#(
_l,
_t, s(
_n)) → if
#(le(length(
_l), s(
_n)), le(length(toList(
_t)), s(
_n)),
_l,
_t, s(
_n)) is replaced by instances determined through the above matching. These instances are:
| lessE#(l, t, s(n)) → if#(le(length(l), s(n)), le(length(toList(t)), s(n)), l, t, s(n)) |
Problem 8: Propagation
Dependency Pair Problem
Dependency Pairs
| lessE#(l, t, s(n)) | → | if#(le(length(l), s(n)), le(length(toList(t)), s(n)), l, t, s(n)) | | if#(false, false, l, t, n) | → | lessE#(l, t, s(n)) |
Rewrite Rules
| lessElements(l, t) | → | lessE(l, t, 0) | | lessE(l, t, n) | → | if(le(length(l), n), le(length(toList(t)), n), l, t, n) |
| if(true, b, l, t, n) | → | l | | if(false, true, l, t, n) | → | t |
| if(false, false, l, t, n) | → | lessE(l, t, s(n)) | | length(nil) | → | 0 |
| length(cons(n, l)) | → | s(length(l)) | | toList(leaf) | → | nil |
| toList(node(t1, n, t2)) | → | append(toList(t1), cons(n, toList(t2))) | | append(nil, l2) | → | l2 |
| append(cons(n, l1), l2) | → | cons(n, append(l1, l2)) | | le(s(n), 0) | → | false |
| le(0, m) | → | true | | le(s(n), s(m)) | → | le(n, m) |
| a | → | c | | a | → | d |
Original Signature
Termination of terms over the following signature is verified: append, d, c, a, true, lessE, leaf, node, 0, le, s, if, length, false, toList, lessElements, cons, nil
Strategy
The dependency pairs if
#(false, false,
l,
t,
n) → lessE
#(
l,
t, s(
n)) and lessE
#(
l,
t, s(
n)) → if
#(le(length(
l), s(
n)), le(length(toList(
t)), s(
n)),
l,
t, s(
n)) are consolidated into the rule if
#(false, false,
l,
t,
n) → if
#(le(length(
l), s(
n)), le(length(toList(
t)), s(
n)),
l,
t, s(
n)) .
This is possible as
- all subterms of lessE#(l, t, s(n)) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in lessE#(l, t, s(n)), but non-replacing in both if#(false, false, l, t, n) and if#(le(length(l), s(n)), le(length(toList(t)), s(n)), l, t, s(n))
The dependency pairs if
#(false, false,
l,
t,
n) → lessE
#(
l,
t, s(
n)) and lessE
#(
l,
t, s(
n)) → if
#(le(length(
l), s(
n)), le(length(toList(
t)), s(
n)),
l,
t, s(
n)) are consolidated into the rule if
#(false, false,
l,
t,
n) → if
#(le(length(
l), s(
n)), le(length(toList(
t)), s(
n)),
l,
t, s(
n)) .
This is possible as
- all subterms of lessE#(l, t, s(n)) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in lessE#(l, t, s(n)), but non-replacing in both if#(false, false, l, t, n) and if#(le(length(l), s(n)), le(length(toList(t)), s(n)), l, t, s(n))
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| lessE#(l, t, s(n)) → if#(le(length(l), s(n)), le(length(toList(t)), s(n)), l, t, s(n)) | if#(false, false, l, t, n) → if#(le(length(l), s(n)), le(length(toList(t)), s(n)), l, t, s(n)) |
| if#(false, false, l, t, n) → lessE#(l, t, s(n)) | |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| length#(cons(n, l)) | → | length#(l) |
Rewrite Rules
| lessElements(l, t) | → | lessE(l, t, 0) | | lessE(l, t, n) | → | if(le(length(l), n), le(length(toList(t)), n), l, t, n) |
| if(true, b, l, t, n) | → | l | | if(false, true, l, t, n) | → | t |
| if(false, false, l, t, n) | → | lessE(l, t, s(n)) | | length(nil) | → | 0 |
| length(cons(n, l)) | → | s(length(l)) | | toList(leaf) | → | nil |
| toList(node(t1, n, t2)) | → | append(toList(t1), cons(n, toList(t2))) | | append(nil, l2) | → | l2 |
| append(cons(n, l1), l2) | → | cons(n, append(l1, l2)) | | le(s(n), 0) | → | false |
| le(0, m) | → | true | | le(s(n), s(m)) | → | le(n, m) |
| a | → | c | | a | → | d |
Original Signature
Termination of terms over the following signature is verified: append, d, c, a, true, lessE, leaf, node, 0, le, s, if, length, false, toList, lessElements, cons, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| length#(cons(n, l)) | → | length#(l) |
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| le#(s(n), s(m)) | → | le#(n, m) |
Rewrite Rules
| lessElements(l, t) | → | lessE(l, t, 0) | | lessE(l, t, n) | → | if(le(length(l), n), le(length(toList(t)), n), l, t, n) |
| if(true, b, l, t, n) | → | l | | if(false, true, l, t, n) | → | t |
| if(false, false, l, t, n) | → | lessE(l, t, s(n)) | | length(nil) | → | 0 |
| length(cons(n, l)) | → | s(length(l)) | | toList(leaf) | → | nil |
| toList(node(t1, n, t2)) | → | append(toList(t1), cons(n, toList(t2))) | | append(nil, l2) | → | l2 |
| append(cons(n, l1), l2) | → | cons(n, append(l1, l2)) | | le(s(n), 0) | → | false |
| le(0, m) | → | true | | le(s(n), s(m)) | → | le(n, m) |
| a | → | c | | a | → | d |
Original Signature
Termination of terms over the following signature is verified: append, d, c, a, true, lessE, leaf, node, 0, le, s, if, length, false, toList, lessElements, cons, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| le#(s(n), s(m)) | → | le#(n, m) |