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