NO
The TRS could be proven non-terminating. The proof took 683 ms.
The following reduction sequence is a witness for non-termination:
U12#(tt, zeros) →* U12#(tt, zeros)
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (7ms).
| – Problem 2 was processed with processor BackwardInstantiation (1ms).
| | – Problem 3 was processed with processor BackwardInstantiation (1ms).
| | | – Problem 5 was processed with processor Propagation (2ms).
| | | | – Problem 6 was processed with processor BackwardInstantiation (4ms).
| | | | | – Problem 8 was processed with processor Propagation (7ms).
| | | | | | – Problem 9 remains open; application of the following processors failed [BackwardsNarrowing (0ms), BackwardInstantiation (0ms), ForwardInstantiation (1ms), Propagation (1ms)].
| | | | | | – Problem 10 remains open; application of the following processors failed [ForwardNarrowing (0ms), BackwardInstantiation (25ms), ForwardInstantiation (0ms), Propagation (0ms)].
| | – Problem 4 was processed with processor Propagation (42ms).
| | | – Problem 7 was processed with processor BackwardInstantiation (1ms).
| | | | – Problem 8 remains open; application of the following processors failed [].
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U12#(tt, L) | → | T(L) | | length#(cons(N, L)) | → | U11#(tt, L) |
| T(zeros) | → | zeros# | | U12#(tt, L) | → | length#(L) |
| U11#(tt, L) | → | U12#(tt, L) |
Rewrite Rules
| zeros | → | cons(0, zeros) | | U11(tt, L) | → | U12(tt, L) |
| U12(tt, L) | → | s(length(L)) | | length(nil) | → | 0 |
| length(cons(N, L)) | → | U11(tt, L) |
Original Signature
Termination of terms over the following signature is verified: 0, s, zeros, tt, length, U11, U12, cons, nil
Strategy
Context-sensitive strategy:
μ(zeros#) = μ(T) = μ(0) = μ(zeros) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U12#) = μ(length#) = μ(s) = μ(length) = μ(U11) = μ(U12) = μ(cons) = {1}
The following SCCs where found
| length#(cons(N, L)) → U11#(tt, L) | U12#(tt, L) → length#(L) |
| U11#(tt, L) → U12#(tt, L) |
Problem 2: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| length#(cons(N, L)) | → | U11#(tt, L) | | U12#(tt, L) | → | length#(L) |
| U11#(tt, L) | → | U12#(tt, L) |
Rewrite Rules
| zeros | → | cons(0, zeros) | | U11(tt, L) | → | U12(tt, L) |
| U12(tt, L) | → | s(length(L)) | | length(nil) | → | 0 |
| length(cons(N, L)) | → | U11(tt, L) |
Original Signature
Termination of terms over the following signature is verified: 0, s, zeros, tt, length, U11, U12, cons, nil
Strategy
Context-sensitive strategy:
μ(zeros#) = μ(T) = μ(0) = μ(zeros) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U12#) = μ(length#) = μ(s) = μ(length) = μ(U11) = μ(U12) = μ(cons) = {1}
Instantiation
For all potential predecessors l → r of the rule
U12#(tt,
L) → length
#(
L) on dependency pair chains it holds that:
- U12#(tt, L) matches r,
- all variables of U12#(tt, L) are embedded in constructor contexts, i.e., each subterm of U12#(tt, L), containing a variable is rooted by a constructor symbol.
Thus,
U12#(tt,
L) → length
#(
L) is replaced by instances determined through the above matching. These instances are:
| U12#(tt, _L) → length#(_L) |
Instantiation
For all potential predecessors l → r of the rule
U11#(tt,
L) →
U12#(tt,
L) on dependency pair chains it holds that:
- U11#(tt, L) matches r,
- all variables of U11#(tt, L) are embedded in constructor contexts, i.e., each subterm of U11#(tt, L), containing a variable is rooted by a constructor symbol.
Thus,
U11#(tt,
L) →
U12#(tt,
L) is replaced by instances determined through the above matching. These instances are:
| U11#(tt, _L) → U12#(tt, _L) |
Problem 3: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| U12#(tt, L) | → | length#(L) | | U11#(tt, L) | → | U12#(tt, L) |
| length#(zeros) | → | U11#(tt, zeros) |
Rewrite Rules
| zeros | → | cons(0, zeros) | | U11(tt, L) | → | U12(tt, L) |
| U12(tt, L) | → | s(length(L)) | | length(nil) | → | 0 |
| length(cons(N, L)) | → | U11(tt, L) |
Original Signature
Termination of terms over the following signature is verified: 0, s, tt, zeros, length, U11, U12, nil, cons
Strategy
Context-sensitive strategy:
μ(zeros#) = μ(T) = μ(0) = μ(zeros) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U12#) = μ(length#) = μ(s) = μ(length) = μ(U11) = μ(U12) = μ(cons) = {1}
Instantiation
For all potential predecessors l → r of the rule
U12#(tt,
L) → length
#(
L) on dependency pair chains it holds that:
- U12#(tt, L) matches r,
- all variables of U12#(tt, L) are embedded in constructor contexts, i.e., each subterm of U12#(tt, L), containing a variable is rooted by a constructor symbol.
Thus,
U12#(tt,
L) → length
#(
L) is replaced by instances determined through the above matching. These instances are:
| U12#(tt, _L) → length#(_L) |
Instantiation
For all potential predecessors l → r of the rule
U11#(tt,
L) →
U12#(tt,
L) on dependency pair chains it holds that:
- U11#(tt, L) matches r,
- all variables of U11#(tt, L) are embedded in constructor contexts, i.e., each subterm of U11#(tt, L), containing a variable is rooted by a constructor symbol.
Thus,
U11#(tt,
L) →
U12#(tt,
L) is replaced by instances determined through the above matching. These instances are:
| U11#(tt, zeros) → U12#(tt, zeros) |
Problem 5: Propagation
Dependency Pair Problem
Dependency Pairs
| length#(zeros) | → | U11#(tt, zeros) | | U11#(tt, zeros) | → | U12#(tt, zeros) |
| U12#(tt, _L) | → | length#(_L) |
Rewrite Rules
| zeros | → | cons(0, zeros) | | U11(tt, L) | → | U12(tt, L) |
| U12(tt, L) | → | s(length(L)) | | length(nil) | → | 0 |
| length(cons(N, L)) | → | U11(tt, L) |
Original Signature
Termination of terms over the following signature is verified: 0, s, zeros, tt, length, U11, U12, cons, nil
Strategy
Context-sensitive strategy:
μ(zeros#) = μ(T) = μ(0) = μ(zeros) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U12#) = μ(length#) = μ(s) = μ(length) = μ(U11) = μ(U12) = μ(cons) = {1}
The dependency pairs length
#(zeros) →
U11#(tt, zeros) and
U11#(tt, zeros) →
U12#(tt, zeros) are consolidated into the rule length
#(zeros) →
U12#(tt, zeros) .
This is possible as
- all subterms of U11#(tt, zeros) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U11#(tt, zeros), but non-replacing in both length#(zeros) and U12#(tt, zeros)
The dependency pairs length
#(zeros) →
U11#(tt, zeros) and
U11#(tt, zeros) →
U12#(tt, zeros) are consolidated into the rule length
#(zeros) →
U12#(tt, zeros) .
This is possible as
- all subterms of U11#(tt, zeros) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U11#(tt, zeros), but non-replacing in both length#(zeros) and U12#(tt, zeros)
The dependency pairs length
#(zeros) →
U11#(tt, zeros) and
U11#(tt, zeros) →
U12#(tt, zeros) are consolidated into the rule length
#(zeros) →
U12#(tt, zeros) .
This is possible as
- all subterms of U11#(tt, zeros) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U11#(tt, zeros), but non-replacing in both length#(zeros) and U12#(tt, zeros)
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| length#(zeros) → U11#(tt, zeros) | length#(zeros) → U12#(tt, zeros) |
| U11#(tt, zeros) → U12#(tt, zeros) | |
Problem 6: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| length#(zeros) | → | U12#(tt, zeros) | | U12#(tt, _L) | → | length#(_L) |
Rewrite Rules
| zeros | → | cons(0, zeros) | | U11(tt, L) | → | U12(tt, L) |
| U12(tt, L) | → | s(length(L)) | | length(nil) | → | 0 |
| length(cons(N, L)) | → | U11(tt, L) |
Original Signature
Termination of terms over the following signature is verified: 0, s, tt, zeros, length, U11, U12, nil, cons
Strategy
Context-sensitive strategy:
μ(zeros#) = μ(T) = μ(0) = μ(zeros) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U12#) = μ(length#) = μ(s) = μ(length) = μ(U11) = μ(U12) = μ(cons) = {1}
Instantiation
For all potential predecessors l → r of the rule
U12#(tt,
_L) → length
#(
_L) on dependency pair chains it holds that:
- U12#(tt, _L) matches r,
- all variables of U12#(tt, _L) are embedded in constructor contexts, i.e., each subterm of U12#(tt, _L), containing a variable is rooted by a constructor symbol.
Thus,
U12#(tt,
_L) → length
#(
_L) is replaced by instances determined through the above matching. These instances are:
| U12#(tt, zeros) → length#(zeros) |
Problem 8: Propagation
Dependency Pair Problem
Dependency Pairs
| U11#(tt, L) | → | length#(L) | | length#(cons(N, L)) | → | U11#(tt, L) |
Rewrite Rules
| zeros | → | cons(0, zeros) | | U11(tt, L) | → | U12(tt, L) |
| U12(tt, L) | → | s(length(L)) | | length(nil) | → | 0 |
| length(cons(N, L)) | → | U11(tt, L) |
Original Signature
Termination of terms over the following signature is verified: 0, s, tt, zeros, length, U11, U12, nil, cons
Strategy
Context-sensitive strategy:
μ(zeros#) = μ(T) = μ(0) = μ(zeros) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U12#) = μ(length#) = μ(s) = μ(length) = μ(U11) = μ(U12) = μ(cons) = {1}
The dependency pairs length
#(cons(
N,
L)) →
U11#(tt,
L) and
U11#(tt,
L) → length
#(
L) are consolidated into the rule length
#(cons(
N,
L)) → length
#(
L) .
This is possible as
- all subterms of U11#(tt, L) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U11#(tt, L), but non-replacing in both length#(cons(N, L)) and length#(L)
The dependency pairs length
#(cons(
N,
L)) →
U11#(tt,
L) and
U11#(tt,
L) → length
#(
L) are consolidated into the rule length
#(cons(
N,
L)) → length
#(
L) .
This is possible as
- all subterms of U11#(tt, L) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U11#(tt, L), but non-replacing in both length#(cons(N, L)) and length#(L)
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| U11#(tt, L) → length#(L) | length#(cons(N, L)) → length#(L) |
| length#(cons(N, L)) → U11#(tt, L) | |
Problem 4: Propagation
Dependency Pair Problem
Dependency Pairs
| length#(cons(N, L)) | → | U11#(tt, L) | | U12#(tt, _L) | → | length#(_L) |
| U11#(tt, _L) | → | U12#(tt, _L) |
Rewrite Rules
| zeros | → | cons(0, zeros) | | U11(tt, L) | → | U12(tt, L) |
| U12(tt, L) | → | s(length(L)) | | length(nil) | → | 0 |
| length(cons(N, L)) | → | U11(tt, L) |
Original Signature
Termination of terms over the following signature is verified: 0, s, tt, zeros, length, U11, U12, nil, cons
Strategy
Context-sensitive strategy:
μ(zeros#) = μ(T) = μ(0) = μ(zeros) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U12#) = μ(length#) = μ(s) = μ(length) = μ(U11) = μ(U12) = μ(cons) = {1}
The dependency pairs
U11#(tt,
_L) →
U12#(tt,
_L) and
U12#(tt,
_L) → length
#(
_L) are consolidated into the rule
U11#(tt,
_L) → length
#(
_L) .
This is possible as
- all subterms of U12#(tt, _L) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U12#(tt, _L), but non-replacing in both U11#(tt, _L) and length#(_L)
The dependency pairs
U11#(tt,
_L) →
U12#(tt,
_L) and
U12#(tt,
_L) → length
#(
_L) are consolidated into the rule
U11#(tt,
_L) → length
#(
_L) .
This is possible as
- all subterms of U12#(tt, _L) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U12#(tt, _L), but non-replacing in both U11#(tt, _L) and length#(_L)
The dependency pairs
U11#(tt,
_L) →
U12#(tt,
_L) and
U12#(tt,
_L) → length
#(
_L) are consolidated into the rule
U11#(tt,
_L) → length
#(
_L) .
This is possible as
- all subterms of U12#(tt, _L) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U12#(tt, _L), but non-replacing in both U11#(tt, _L) and length#(_L)
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| U12#(tt, _L) → length#(_L) | U11#(tt, _L) → length#(_L) |
| U11#(tt, _L) → U12#(tt, _L) | |
Problem 7: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| length#(cons(N, L)) | → | U11#(tt, L) | | U11#(tt, _L) | → | length#(_L) |
Rewrite Rules
| zeros | → | cons(0, zeros) | | U11(tt, L) | → | U12(tt, L) |
| U12(tt, L) | → | s(length(L)) | | length(nil) | → | 0 |
| length(cons(N, L)) | → | U11(tt, L) |
Original Signature
Termination of terms over the following signature is verified: 0, s, zeros, tt, length, U11, U12, cons, nil
Strategy
Context-sensitive strategy:
μ(zeros#) = μ(T) = μ(0) = μ(zeros) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U12#) = μ(length#) = μ(s) = μ(length) = μ(U11) = μ(U12) = μ(cons) = {1}
Instantiation
For all potential predecessors l → r of the rule
U11#(tt,
_L) → length
#(
_L) on dependency pair chains it holds that:
- U11#(tt, _L) matches r,
- all variables of U11#(tt, _L) are embedded in constructor contexts, i.e., each subterm of U11#(tt, _L), containing a variable is rooted by a constructor symbol.
Thus,
U11#(tt,
_L) → length
#(
_L) is replaced by instances determined through the above matching. These instances are: