TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60282 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (36ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor BackwardInstantiation (2ms).
| | – Problem 5 was processed with processor BackwardInstantiation (1ms).
| | | – Problem 6 was processed with processor Propagation (4ms).
| | | | – Problem 7 remains open; application of the following processors failed [ForwardNarrowing (1ms), BackwardInstantiation (0ms), ForwardInstantiation (1ms), Propagation (0ms)].
| – Problem 4 was processed with processor SubtermCriterion (1ms).
The following open problems remain:
Open Dependency Pair Problem 3
Dependency Pairs
| cond#(false, n, l) | → | nthtail#(s(n), l) | | nthtail#(n, l) | → | cond#(ge(n, length(l)), n, l) |
Rewrite Rules
| nthtail(n, l) | → | cond(ge(n, length(l)), n, l) | | cond(true, n, l) | → | l |
| cond(false, n, l) | → | tail(nthtail(s(n), l)) | | tail(nil) | → | nil |
| tail(cons(x, l)) | → | l | | length(nil) | → | 0 |
| length(cons(x, l)) | → | s(length(l)) | | ge(u, 0) | → | true |
| ge(0, s(v)) | → | false | | ge(s(u), s(v)) | → | ge(u, v) |
Original Signature
Termination of terms over the following signature is verified: 0, s, length, false, true, ge, tail, nthtail, cond, cons, nil
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| cond#(false, n, l) | → | nthtail#(s(n), l) | | nthtail#(n, l) | → | cond#(ge(n, length(l)), n, l) |
| cond#(false, n, l) | → | tail#(nthtail(s(n), l)) | | nthtail#(n, l) | → | length#(l) |
| nthtail#(n, l) | → | ge#(n, length(l)) | | ge#(s(u), s(v)) | → | ge#(u, v) |
| length#(cons(x, l)) | → | length#(l) |
Rewrite Rules
| nthtail(n, l) | → | cond(ge(n, length(l)), n, l) | | cond(true, n, l) | → | l |
| cond(false, n, l) | → | tail(nthtail(s(n), l)) | | tail(nil) | → | nil |
| tail(cons(x, l)) | → | l | | length(nil) | → | 0 |
| length(cons(x, l)) | → | s(length(l)) | | ge(u, 0) | → | true |
| ge(0, s(v)) | → | false | | ge(s(u), s(v)) | → | ge(u, v) |
Original Signature
Termination of terms over the following signature is verified: 0, s, length, true, false, ge, cond, nthtail, tail, nil, cons
Strategy
The following SCCs where found
| cond#(false, n, l) → nthtail#(s(n), l) | nthtail#(n, l) → cond#(ge(n, length(l)), n, l) |
| ge#(s(u), s(v)) → ge#(u, v) |
| length#(cons(x, l)) → length#(l) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| length#(cons(x, l)) | → | length#(l) |
Rewrite Rules
| nthtail(n, l) | → | cond(ge(n, length(l)), n, l) | | cond(true, n, l) | → | l |
| cond(false, n, l) | → | tail(nthtail(s(n), l)) | | tail(nil) | → | nil |
| tail(cons(x, l)) | → | l | | length(nil) | → | 0 |
| length(cons(x, l)) | → | s(length(l)) | | ge(u, 0) | → | true |
| ge(0, s(v)) | → | false | | ge(s(u), s(v)) | → | ge(u, v) |
Original Signature
Termination of terms over the following signature is verified: 0, s, length, true, false, ge, cond, nthtail, tail, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| length#(cons(x, l)) | → | length#(l) |
Problem 3: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| cond#(false, n, l) | → | nthtail#(s(n), l) | | nthtail#(n, l) | → | cond#(ge(n, length(l)), n, l) |
Rewrite Rules
| nthtail(n, l) | → | cond(ge(n, length(l)), n, l) | | cond(true, n, l) | → | l |
| cond(false, n, l) | → | tail(nthtail(s(n), l)) | | tail(nil) | → | nil |
| tail(cons(x, l)) | → | l | | length(nil) | → | 0 |
| length(cons(x, l)) | → | s(length(l)) | | ge(u, 0) | → | true |
| ge(0, s(v)) | → | false | | ge(s(u), s(v)) | → | ge(u, v) |
Original Signature
Termination of terms over the following signature is verified: 0, s, length, true, false, ge, cond, nthtail, tail, nil, cons
Strategy
Instantiation
For all potential predecessors l → r of the rule nthtail
#(
n,
l) → cond
#(ge(
n, length(
l)),
n,
l) on dependency pair chains it holds that:
- nthtail#(n, l) matches r,
- all variables of nthtail#(n, l) are embedded in constructor contexts, i.e., each subterm of nthtail#(n, l), containing a variable is rooted by a constructor symbol.
Thus, nthtail
#(
n,
l) → cond
#(ge(
n, length(
l)),
n,
l) is replaced by instances determined through the above matching. These instances are:
| nthtail#(s(_n), _l) → cond#(ge(s(_n), length(_l)), s(_n), _l) |
Problem 5: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| cond#(false, n, l) | → | nthtail#(s(n), l) | | nthtail#(s(_n), _l) | → | cond#(ge(s(_n), length(_l)), s(_n), _l) |
Rewrite Rules
| nthtail(n, l) | → | cond(ge(n, length(l)), n, l) | | cond(true, n, l) | → | l |
| cond(false, n, l) | → | tail(nthtail(s(n), l)) | | tail(nil) | → | nil |
| tail(cons(x, l)) | → | l | | length(nil) | → | 0 |
| length(cons(x, l)) | → | s(length(l)) | | ge(u, 0) | → | true |
| ge(0, s(v)) | → | false | | ge(s(u), s(v)) | → | ge(u, v) |
Original Signature
Termination of terms over the following signature is verified: 0, s, length, false, true, ge, tail, nthtail, cond, cons, nil
Strategy
Instantiation
For all potential predecessors l → r of the rule nthtail
#(s(
_n),
_l) → cond
#(ge(s(
_n), length(
_l)), s(
_n),
_l) on dependency pair chains it holds that:
- nthtail#(s(_n), _l) matches r,
- all variables of nthtail#(s(_n), _l) are embedded in constructor contexts, i.e., each subterm of nthtail#(s(_n), _l), containing a variable is rooted by a constructor symbol.
Thus, nthtail
#(s(
_n),
_l) → cond
#(ge(s(
_n), length(
_l)), s(
_n),
_l) is replaced by instances determined through the above matching. These instances are:
| nthtail#(s(n), l) → cond#(ge(s(n), length(l)), s(n), l) |
Problem 6: Propagation
Dependency Pair Problem
Dependency Pairs
| cond#(false, n, l) | → | nthtail#(s(n), l) | | nthtail#(s(n), l) | → | cond#(ge(s(n), length(l)), s(n), l) |
Rewrite Rules
| nthtail(n, l) | → | cond(ge(n, length(l)), n, l) | | cond(true, n, l) | → | l |
| cond(false, n, l) | → | tail(nthtail(s(n), l)) | | tail(nil) | → | nil |
| tail(cons(x, l)) | → | l | | length(nil) | → | 0 |
| length(cons(x, l)) | → | s(length(l)) | | ge(u, 0) | → | true |
| ge(0, s(v)) | → | false | | ge(s(u), s(v)) | → | ge(u, v) |
Original Signature
Termination of terms over the following signature is verified: 0, s, length, true, false, ge, cond, nthtail, tail, nil, cons
Strategy
The dependency pairs cond
#(false,
n,
l) → nthtail
#(s(
n),
l) and nthtail
#(s(
n),
l) → cond
#(ge(s(
n), length(
l)), s(
n),
l) are consolidated into the rule cond
#(false,
n,
l) → cond
#(ge(s(
n), length(
l)), s(
n),
l) .
This is possible as
- all subterms of nthtail#(s(n), l) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in nthtail#(s(n), l), but non-replacing in both cond#(false, n, l) and cond#(ge(s(n), length(l)), s(n), l)
The dependency pairs cond
#(false,
n,
l) → nthtail
#(s(
n),
l) and nthtail
#(s(
n),
l) → cond
#(ge(s(
n), length(
l)), s(
n),
l) are consolidated into the rule cond
#(false,
n,
l) → cond
#(ge(s(
n), length(
l)), s(
n),
l) .
This is possible as
- all subterms of nthtail#(s(n), l) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in nthtail#(s(n), l), but non-replacing in both cond#(false, n, l) and cond#(ge(s(n), length(l)), s(n), l)
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| cond#(false, n, l) → nthtail#(s(n), l) | cond#(false, n, l) → cond#(ge(s(n), length(l)), s(n), l) |
| nthtail#(s(n), l) → cond#(ge(s(n), length(l)), s(n), l) | |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| ge#(s(u), s(v)) | → | ge#(u, v) |
Rewrite Rules
| nthtail(n, l) | → | cond(ge(n, length(l)), n, l) | | cond(true, n, l) | → | l |
| cond(false, n, l) | → | tail(nthtail(s(n), l)) | | tail(nil) | → | nil |
| tail(cons(x, l)) | → | l | | length(nil) | → | 0 |
| length(cons(x, l)) | → | s(length(l)) | | ge(u, 0) | → | true |
| ge(0, s(v)) | → | false | | ge(s(u), s(v)) | → | ge(u, v) |
Original Signature
Termination of terms over the following signature is verified: 0, s, length, true, false, ge, cond, nthtail, tail, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| ge#(s(u), s(v)) | → | ge#(u, v) |