NO
The TRS could be proven non-terminating. The proof took 12150 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 (102ms).
| – Problem 2 was processed with processor BackwardInstantiation (1ms).
| | – Problem 6 was processed with processor BackwardInstantiation (1ms).
| | | – Problem 7 was processed with processor Propagation (1ms).
| | | | – Problem 10 was processed with processor BackwardInstantiation (2ms).
| | | | | – Problem 12 was processed with processor Propagation (1ms).
| | | | | | – Problem 14 was processed with processor BackwardsNarrowing (41ms).
| | | | | | | – Problem 15 was processed with processor BackwardsNarrowing (10ms).
| | | | | | | | – Problem 16 was processed with processor BackwardsNarrowing (1ms).
| | | | | | | | | – Problem 17 remains open; application of the following processors failed [BackwardsNarrowing (0ms), BackwardInstantiation (1ms), ForwardInstantiation (0ms), Propagation (0ms)].
| | – Problem 8 was processed with processor Propagation (1ms).
| | | – Problem 9 was processed with processor BackwardInstantiation (1ms).
| | | | – Problem 11 was processed with processor Propagation (9ms).
| | | | | – Problem 13 remains open; application of the following processors failed [ForwardNarrowing (2ms), BackwardInstantiation (39ms), ForwardInstantiation (1ms), Propagation (9ms)].
| – Problem 3 was processed with processor PolynomialLinearRange4 (198ms).
| | – Problem 4 was processed with processor DependencyGraph (28ms).
| | | – Problem 5 was processed with processor PolynomialLinearRange4 (38ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| take#(s(M), cons(N, IL)) | → | U21#(tt, IL, M, N) | | U21#(tt, IL, M, N) | → | U22#(tt, IL, M, N) |
| U12#(tt, L) | → | T(L) | | T(take(x_1, x_2)) | → | T(x_2) |
| length#(cons(N, L)) | → | U11#(tt, L) | | T(zeros) | → | zeros# |
| U12#(tt, L) | → | length#(L) | | T(take(x_1, x_2)) | → | T(x_1) |
| U11#(tt, L) | → | U12#(tt, L) | | U23#(tt, IL, M, N) | → | T(N) |
| U22#(tt, IL, M, N) | → | U23#(tt, IL, M, N) | | T(take(M, IL)) | → | take#(M, IL) |
Rewrite Rules
| zeros | → | cons(0, zeros) | | U11(tt, L) | → | U12(tt, L) |
| U12(tt, L) | → | s(length(L)) | | U21(tt, IL, M, N) | → | U22(tt, IL, M, N) |
| U22(tt, IL, M, N) | → | U23(tt, IL, M, N) | | U23(tt, IL, M, N) | → | cons(N, take(M, IL)) |
| length(nil) | → | 0 | | length(cons(N, L)) | → | U11(tt, L) |
| take(0, IL) | → | nil | | take(s(M), cons(N, IL)) | → | U21(tt, IL, M, N) |
Original Signature
Termination of terms over the following signature is verified: 0, s, zeros, tt, take, length, U11, U12, U23, U21, cons, U22, nil
Strategy
Context-sensitive strategy:
μ(zeros#) = μ(T) = μ(0) = μ(zeros) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(length#) = μ(U21#) = μ(U23#) = μ(s) = μ(length) = μ(U11) = μ(U12) = μ(U23) = μ(U21) = μ(U22) = μ(cons) = {1}
μ(take#) = μ(take) = {1, 2}
The following SCCs where found
| length#(cons(N, L)) → U11#(tt, L) | U12#(tt, L) → length#(L) |
| U11#(tt, L) → U12#(tt, L) |
| take#(s(M), cons(N, IL)) → U21#(tt, IL, M, N) | U21#(tt, IL, M, N) → U22#(tt, IL, M, N) |
| T(take(x_1, x_2)) → T(x_2) | T(take(x_1, x_2)) → T(x_1) |
| U23#(tt, IL, M, N) → T(N) | U22#(tt, IL, M, N) → U23#(tt, IL, M, N) |
| T(take(M, IL)) → take#(M, IL) |
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)) | | U21(tt, IL, M, N) | → | U22(tt, IL, M, N) |
| U22(tt, IL, M, N) | → | U23(tt, IL, M, N) | | U23(tt, IL, M, N) | → | cons(N, take(M, IL)) |
| length(nil) | → | 0 | | length(cons(N, L)) | → | U11(tt, L) |
| take(0, IL) | → | nil | | take(s(M), cons(N, IL)) | → | U21(tt, IL, M, N) |
Original Signature
Termination of terms over the following signature is verified: 0, s, zeros, tt, take, length, U11, U12, U23, U21, cons, U22, nil
Strategy
Context-sensitive strategy:
μ(zeros#) = μ(T) = μ(0) = μ(zeros) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(length#) = μ(U21#) = μ(U23#) = μ(s) = μ(length) = μ(U11) = μ(U12) = μ(U23) = μ(U21) = μ(cons) = μ(U22) = {1}
μ(take#) = μ(take) = {1, 2}
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 6: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| U12#(tt, L) | → | length#(L) | | U11#(tt, L) | → | U12#(tt, L) |
| length#(zeros) | → | U11#(tt, zeros) | | length#(U23(tt, _x21, _x22, _x23)) | → | U11#(tt, take(_x22, _x21)) |
Rewrite Rules
| zeros | → | cons(0, zeros) | | U11(tt, L) | → | U12(tt, L) |
| U12(tt, L) | → | s(length(L)) | | U21(tt, IL, M, N) | → | U22(tt, IL, M, N) |
| U22(tt, IL, M, N) | → | U23(tt, IL, M, N) | | U23(tt, IL, M, N) | → | cons(N, take(M, IL)) |
| length(nil) | → | 0 | | length(cons(N, L)) | → | U11(tt, L) |
| take(0, IL) | → | nil | | take(s(M), cons(N, IL)) | → | U21(tt, IL, M, N) |
Original Signature
Termination of terms over the following signature is verified: 0, s, zeros, tt, take, length, U11, U12, U23, U21, cons, U22, nil
Strategy
Context-sensitive strategy:
μ(zeros#) = μ(T) = μ(0) = μ(zeros) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(length#) = μ(U21#) = μ(U23#) = μ(s) = μ(length) = μ(U11) = μ(U12) = μ(U23) = μ(U21) = μ(U22) = μ(cons) = {1}
μ(take#) = μ(take) = {1, 2}
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) | U11#(tt, take(_x22, _x21)) → U12#(tt, take(_x22, _x21)) |
Problem 7: Propagation
Dependency Pair Problem
Dependency Pairs
| length#(U23(tt, _x21, _x22, _x23)) | → | U11#(tt, take(_x22, _x21)) | | length#(zeros) | → | U11#(tt, zeros) |
| U11#(tt, zeros) | → | U12#(tt, zeros) | | U12#(tt, _L) | → | length#(_L) |
| U11#(tt, take(_x22, _x21)) | → | U12#(tt, take(_x22, _x21)) |
Rewrite Rules
| zeros | → | cons(0, zeros) | | U11(tt, L) | → | U12(tt, L) |
| U12(tt, L) | → | s(length(L)) | | U21(tt, IL, M, N) | → | U22(tt, IL, M, N) |
| U22(tt, IL, M, N) | → | U23(tt, IL, M, N) | | U23(tt, IL, M, N) | → | cons(N, take(M, IL)) |
| length(nil) | → | 0 | | length(cons(N, L)) | → | U11(tt, L) |
| take(0, IL) | → | nil | | take(s(M), cons(N, IL)) | → | U21(tt, IL, M, N) |
Original Signature
Termination of terms over the following signature is verified: 0, s, zeros, tt, take, length, U11, U12, U23, U21, cons, U22, nil
Strategy
Context-sensitive strategy:
μ(zeros#) = μ(T) = μ(0) = μ(zeros) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(length#) = μ(U21#) = μ(U23#) = μ(s) = μ(length) = μ(U11) = μ(U12) = μ(U23) = μ(U21) = μ(cons) = μ(U22) = {1}
μ(take#) = μ(take) = {1, 2}
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)
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 10: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| length#(U23(tt, _x21, _x22, _x23)) | → | U11#(tt, take(_x22, _x21)) | | length#(zeros) | → | U12#(tt, zeros) |
| U12#(tt, _L) | → | length#(_L) | | U11#(tt, take(_x22, _x21)) | → | U12#(tt, take(_x22, _x21)) |
Rewrite Rules
| zeros | → | cons(0, zeros) | | U11(tt, L) | → | U12(tt, L) |
| U12(tt, L) | → | s(length(L)) | | U21(tt, IL, M, N) | → | U22(tt, IL, M, N) |
| U22(tt, IL, M, N) | → | U23(tt, IL, M, N) | | U23(tt, IL, M, N) | → | cons(N, take(M, IL)) |
| length(nil) | → | 0 | | length(cons(N, L)) | → | U11(tt, L) |
| take(0, IL) | → | nil | | take(s(M), cons(N, IL)) | → | U21(tt, IL, M, N) |
Original Signature
Termination of terms over the following signature is verified: 0, s, zeros, tt, take, length, U11, U12, U23, U21, cons, U22, nil
Strategy
Context-sensitive strategy:
μ(zeros#) = μ(T) = μ(0) = μ(zeros) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(length#) = μ(U21#) = μ(U23#) = μ(s) = μ(length) = μ(U11) = μ(U12) = μ(U23) = μ(U21) = μ(U22) = μ(cons) = {1}
μ(take#) = μ(take) = {1, 2}
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, take(_x22, _x21)) → length#(take(_x22, _x21)) | U12#(tt, zeros) → length#(zeros) |
Problem 12: Propagation
Dependency Pair Problem
Dependency Pairs
| U12#(tt, take(_x22, _x21)) | → | length#(take(_x22, _x21)) | | U12#(tt, zeros) | → | length#(zeros) |
| length#(U23(tt, _x21, _x22, _x23)) | → | U11#(tt, take(_x22, _x21)) | | length#(zeros) | → | U12#(tt, zeros) |
| U11#(tt, take(_x22, _x21)) | → | U12#(tt, take(_x22, _x21)) |
Rewrite Rules
| zeros | → | cons(0, zeros) | | U11(tt, L) | → | U12(tt, L) |
| U12(tt, L) | → | s(length(L)) | | U21(tt, IL, M, N) | → | U22(tt, IL, M, N) |
| U22(tt, IL, M, N) | → | U23(tt, IL, M, N) | | U23(tt, IL, M, N) | → | cons(N, take(M, IL)) |
| length(nil) | → | 0 | | length(cons(N, L)) | → | U11(tt, L) |
| take(0, IL) | → | nil | | take(s(M), cons(N, IL)) | → | U21(tt, IL, M, N) |
Original Signature
Termination of terms over the following signature is verified: 0, s, zeros, tt, take, length, U11, U12, U23, U21, cons, U22, nil
Strategy
Context-sensitive strategy:
μ(zeros#) = μ(T) = μ(0) = μ(zeros) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(length#) = μ(U21#) = μ(U23#) = μ(s) = μ(length) = μ(U11) = μ(U12) = μ(U23) = μ(U21) = μ(cons) = μ(U22) = {1}
μ(take#) = μ(take) = {1, 2}
The dependency pairs
U12#(tt, zeros) → length
#(zeros) and length
#(zeros) →
U12#(tt, zeros) are consolidated into the rule
U12#(tt, zeros) →
U12#(tt, zeros) .
This is possible as
- all subterms of length#(zeros) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in length#(zeros), but non-replacing in both U12#(tt, zeros) and U12#(tt, zeros)
The dependency pairs length
#(zeros) →
U12#(tt, zeros) and
U12#(tt, zeros) → length
#(zeros) are consolidated into the rule length
#(zeros) → length
#(zeros) .
This is possible as
- all subterms of U12#(tt, zeros) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U12#(tt, zeros), but non-replacing in both length#(zeros) and length#(zeros)
The dependency pairs length
#(zeros) →
U12#(tt, zeros) and
U12#(tt, zeros) → length
#(zeros) are consolidated into the rule length
#(zeros) → length
#(zeros) .
This is possible as
- all subterms of U12#(tt, zeros) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U12#(tt, zeros), but non-replacing in both length#(zeros) and length#(zeros)
The dependency pairs length
#(zeros) →
U12#(tt, zeros) and
U12#(tt, zeros) → length
#(zeros) are consolidated into the rule length
#(zeros) → length
#(zeros) .
This is possible as
- all subterms of U12#(tt, zeros) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U12#(tt, zeros), but non-replacing in both length#(zeros) and length#(zeros)
The dependency pairs length
#(zeros) →
U12#(tt, zeros) and
U12#(tt, zeros) → length
#(zeros) are consolidated into the rule length
#(zeros) → length
#(zeros) .
This is possible as
- all subterms of U12#(tt, zeros) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U12#(tt, zeros), but non-replacing in both length#(zeros) and length#(zeros)
The dependency pairs length
#(zeros) →
U12#(tt, zeros) and
U12#(tt, zeros) → length
#(zeros) are consolidated into the rule length
#(zeros) → length
#(zeros) .
This is possible as
- all subterms of U12#(tt, zeros) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U12#(tt, zeros), but non-replacing in both length#(zeros) and length#(zeros)
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| U12#(tt, zeros) → length#(zeros) | U12#(tt, zeros) → U12#(tt, zeros) |
| length#(zeros) → U12#(tt, zeros) | length#(zeros) → length#(zeros) |
Problem 14: BackwardsNarrowing
Dependency Pair Problem
Dependency Pairs
| U12#(tt, zeros) | → | U12#(tt, zeros) | | U12#(tt, take(_x22, _x21)) | → | length#(take(_x22, _x21)) |
| length#(zeros) | → | length#(zeros) | | length#(U23(tt, _x21, _x22, _x23)) | → | U11#(tt, take(_x22, _x21)) |
| U11#(tt, take(_x22, _x21)) | → | U12#(tt, take(_x22, _x21)) |
Rewrite Rules
| zeros | → | cons(0, zeros) | | U11(tt, L) | → | U12(tt, L) |
| U12(tt, L) | → | s(length(L)) | | U21(tt, IL, M, N) | → | U22(tt, IL, M, N) |
| U22(tt, IL, M, N) | → | U23(tt, IL, M, N) | | U23(tt, IL, M, N) | → | cons(N, take(M, IL)) |
| length(nil) | → | 0 | | length(cons(N, L)) | → | U11(tt, L) |
| take(0, IL) | → | nil | | take(s(M), cons(N, IL)) | → | U21(tt, IL, M, N) |
Original Signature
Termination of terms over the following signature is verified: 0, s, zeros, tt, take, length, U11, U12, U23, U21, cons, U22, nil
Strategy
Context-sensitive strategy:
μ(zeros#) = μ(T) = μ(0) = μ(zeros) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(length#) = μ(U21#) = μ(U23#) = μ(s) = μ(length) = μ(U11) = μ(U12) = μ(U23) = μ(U21) = μ(U22) = μ(cons) = {1}
μ(take#) = μ(take) = {1, 2}
The left-hand side of the rule length
#(
U23(tt,
_x21,
_x22,
_x23)) →
U11#(tt, take(
_x22,
_x21)) is backward narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
| length#(U22(tt, _x31, _x32, _x33)) | |
Thus, the rule length
#(
U23(tt,
_x21,
_x22,
_x23)) →
U11#(tt, take(
_x22,
_x21)) is replaced by the following rules:
| length#(U22(tt, _x31, _x32, _x33)) → U11#(tt, take(_x32, _x31)) |
Problem 15: BackwardsNarrowing
Dependency Pair Problem
Dependency Pairs
| U12#(tt, zeros) | → | U12#(tt, zeros) | | length#(zeros) | → | length#(zeros) |
| U12#(tt, take(_x22, _x21)) | → | length#(take(_x22, _x21)) | | U11#(tt, take(_x22, _x21)) | → | U12#(tt, take(_x22, _x21)) |
| length#(U22(tt, _x31, _x32, _x33)) | → | U11#(tt, take(_x32, _x31)) |
Rewrite Rules
| zeros | → | cons(0, zeros) | | U11(tt, L) | → | U12(tt, L) |
| U12(tt, L) | → | s(length(L)) | | U21(tt, IL, M, N) | → | U22(tt, IL, M, N) |
| U22(tt, IL, M, N) | → | U23(tt, IL, M, N) | | U23(tt, IL, M, N) | → | cons(N, take(M, IL)) |
| length(nil) | → | 0 | | length(cons(N, L)) | → | U11(tt, L) |
| take(0, IL) | → | nil | | take(s(M), cons(N, IL)) | → | U21(tt, IL, M, N) |
Original Signature
Termination of terms over the following signature is verified: 0, s, zeros, tt, take, length, U11, U12, U23, U21, cons, U22, nil
Strategy
Context-sensitive strategy:
μ(zeros#) = μ(T) = μ(0) = μ(zeros) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(length#) = μ(U21#) = μ(U23#) = μ(s) = μ(length) = μ(U11) = μ(U12) = μ(U23) = μ(U21) = μ(cons) = μ(U22) = {1}
μ(take#) = μ(take) = {1, 2}
The left-hand side of the rule length
#(
U22(tt,
_x31,
_x32,
_x33)) →
U11#(tt, take(
_x32,
_x31)) is backward narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
| length#(U21(tt, _x21, _x22, _x23)) | |
Thus, the rule length
#(
U22(tt,
_x31,
_x32,
_x33)) →
U11#(tt, take(
_x32,
_x31)) is replaced by the following rules:
| length#(U21(tt, _x21, _x22, _x23)) → U11#(tt, take(_x22, _x21)) |
Problem 16: BackwardsNarrowing
Dependency Pair Problem
Dependency Pairs
| U12#(tt, zeros) | → | U12#(tt, zeros) | | length#(U21(tt, _x21, _x22, _x23)) | → | U11#(tt, take(_x22, _x21)) |
| U12#(tt, take(_x22, _x21)) | → | length#(take(_x22, _x21)) | | length#(zeros) | → | length#(zeros) |
| U11#(tt, take(_x22, _x21)) | → | U12#(tt, take(_x22, _x21)) |
Rewrite Rules
| zeros | → | cons(0, zeros) | | U11(tt, L) | → | U12(tt, L) |
| U12(tt, L) | → | s(length(L)) | | U21(tt, IL, M, N) | → | U22(tt, IL, M, N) |
| U22(tt, IL, M, N) | → | U23(tt, IL, M, N) | | U23(tt, IL, M, N) | → | cons(N, take(M, IL)) |
| length(nil) | → | 0 | | length(cons(N, L)) | → | U11(tt, L) |
| take(0, IL) | → | nil | | take(s(M), cons(N, IL)) | → | U21(tt, IL, M, N) |
Original Signature
Termination of terms over the following signature is verified: 0, s, zeros, tt, take, length, U11, U12, U23, U21, cons, U22, nil
Strategy
Context-sensitive strategy:
μ(zeros#) = μ(T) = μ(0) = μ(zeros) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(length#) = μ(U21#) = μ(U23#) = μ(s) = μ(length) = μ(U11) = μ(U12) = μ(U23) = μ(U21) = μ(U22) = μ(cons) = {1}
μ(take#) = μ(take) = {1, 2}
The left-hand side of the rule length
#(
U21(tt,
_x21,
_x22,
_x23)) →
U11#(tt, take(
_x22,
_x21)) is backward narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
| length#(take(s(_x32), cons(_x33, _x31))) | |
Thus, the rule length
#(
U21(tt,
_x21,
_x22,
_x23)) →
U11#(tt, take(
_x22,
_x21)) is replaced by the following rules:
| length#(take(s(_x32), cons(_x33, _x31))) → U11#(tt, take(_x32, _x31)) |
Problem 8: 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)) | | U21(tt, IL, M, N) | → | U22(tt, IL, M, N) |
| U22(tt, IL, M, N) | → | U23(tt, IL, M, N) | | U23(tt, IL, M, N) | → | cons(N, take(M, IL)) |
| length(nil) | → | 0 | | length(cons(N, L)) | → | U11(tt, L) |
| take(0, IL) | → | nil | | take(s(M), cons(N, IL)) | → | U21(tt, IL, M, N) |
Original Signature
Termination of terms over the following signature is verified: 0, s, zeros, tt, take, length, U11, U12, U23, U21, cons, U22, nil
Strategy
Context-sensitive strategy:
μ(zeros#) = μ(T) = μ(0) = μ(zeros) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(length#) = μ(U21#) = μ(U23#) = μ(s) = μ(length) = μ(U11) = μ(U12) = μ(U23) = μ(U21) = μ(U22) = μ(cons) = {1}
μ(take#) = μ(take) = {1, 2}
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 9: 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)) | | U21(tt, IL, M, N) | → | U22(tt, IL, M, N) |
| U22(tt, IL, M, N) | → | U23(tt, IL, M, N) | | U23(tt, IL, M, N) | → | cons(N, take(M, IL)) |
| length(nil) | → | 0 | | length(cons(N, L)) | → | U11(tt, L) |
| take(0, IL) | → | nil | | take(s(M), cons(N, IL)) | → | U21(tt, IL, M, N) |
Original Signature
Termination of terms over the following signature is verified: 0, s, zeros, tt, take, length, U11, U12, U23, U21, cons, U22, nil
Strategy
Context-sensitive strategy:
μ(zeros#) = μ(T) = μ(0) = μ(zeros) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(length#) = μ(U21#) = μ(U23#) = μ(s) = μ(length) = μ(U11) = μ(U12) = μ(U23) = μ(U21) = μ(cons) = μ(U22) = {1}
μ(take#) = μ(take) = {1, 2}
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:
Problem 11: 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)) | | U21(tt, IL, M, N) | → | U22(tt, IL, M, N) |
| U22(tt, IL, M, N) | → | U23(tt, IL, M, N) | | U23(tt, IL, M, N) | → | cons(N, take(M, IL)) |
| length(nil) | → | 0 | | length(cons(N, L)) | → | U11(tt, L) |
| take(0, IL) | → | nil | | take(s(M), cons(N, IL)) | → | U21(tt, IL, M, N) |
Original Signature
Termination of terms over the following signature is verified: 0, s, zeros, tt, take, length, U11, U12, U23, U21, cons, U22, nil
Strategy
Context-sensitive strategy:
μ(zeros#) = μ(T) = μ(0) = μ(zeros) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(length#) = μ(U21#) = μ(U23#) = μ(s) = μ(length) = μ(U11) = μ(U12) = μ(U23) = μ(U21) = μ(U22) = μ(cons) = {1}
μ(take#) = μ(take) = {1, 2}
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 3: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| take#(s(M), cons(N, IL)) | → | U21#(tt, IL, M, N) | | U21#(tt, IL, M, N) | → | U22#(tt, IL, M, N) |
| T(take(x_1, x_2)) | → | T(x_2) | | T(take(x_1, x_2)) | → | T(x_1) |
| U23#(tt, IL, M, N) | → | T(N) | | U22#(tt, IL, M, N) | → | U23#(tt, IL, M, N) |
| T(take(M, IL)) | → | take#(M, IL) |
Rewrite Rules
| zeros | → | cons(0, zeros) | | U11(tt, L) | → | U12(tt, L) |
| U12(tt, L) | → | s(length(L)) | | U21(tt, IL, M, N) | → | U22(tt, IL, M, N) |
| U22(tt, IL, M, N) | → | U23(tt, IL, M, N) | | U23(tt, IL, M, N) | → | cons(N, take(M, IL)) |
| length(nil) | → | 0 | | length(cons(N, L)) | → | U11(tt, L) |
| take(0, IL) | → | nil | | take(s(M), cons(N, IL)) | → | U21(tt, IL, M, N) |
Original Signature
Termination of terms over the following signature is verified: 0, s, zeros, tt, take, length, U11, U12, U23, U21, cons, U22, nil
Strategy
Context-sensitive strategy:
μ(zeros#) = μ(T) = μ(0) = μ(zeros) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(length#) = μ(U21#) = μ(U23#) = μ(s) = μ(length) = μ(U11) = μ(U12) = μ(U23) = μ(U21) = μ(cons) = μ(U22) = {1}
μ(take#) = μ(take) = {1, 2}
Polynomial Interpretation
- 0: 0
- T(x): 3x
- U11(x,y): x
- U12(x,y): x
- U21(x1,x2,x3,x4): 3x4 + 1
- U21#(x1,x2,x3,x4): 3x4 + x1
- U22(x1,x2,x3,x4): 3x4 + 1
- U22#(x1,x2,x3,x4): 3x4 + 2
- U23(x1,x2,x3,x4): 3x4 + 1
- U23#(x1,x2,x3,x4): 3x4
- cons(x,y): 2x + 1
- length(x): x + 1
- nil: 0
- s(x): 0
- take(x,y): 3y + 2x
- take#(x,y): 2y + 2x
- tt: 2
- zeros: 1
Standard Usable rules
| take(0, IL) | → | nil | | U12(tt, L) | → | s(length(L)) |
| take(s(M), cons(N, IL)) | → | U21(tt, IL, M, N) | | U11(tt, L) | → | U12(tt, L) |
| zeros | → | cons(0, zeros) | | length(cons(N, L)) | → | U11(tt, L) |
| U23(tt, IL, M, N) | → | cons(N, take(M, IL)) | | U22(tt, IL, M, N) | → | U23(tt, IL, M, N) |
| length(nil) | → | 0 | | U21(tt, IL, M, N) | → | U22(tt, IL, M, N) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| U22#(tt, IL, M, N) | → | U23#(tt, IL, M, N) |
Problem 4: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| take#(s(M), cons(N, IL)) | → | U21#(tt, IL, M, N) | | U21#(tt, IL, M, N) | → | U22#(tt, IL, M, N) |
| T(take(x_1, x_2)) | → | T(x_2) | | T(take(x_1, x_2)) | → | T(x_1) |
| U23#(tt, IL, M, N) | → | T(N) | | T(take(M, IL)) | → | take#(M, IL) |
Rewrite Rules
| zeros | → | cons(0, zeros) | | U11(tt, L) | → | U12(tt, L) |
| U12(tt, L) | → | s(length(L)) | | U21(tt, IL, M, N) | → | U22(tt, IL, M, N) |
| U22(tt, IL, M, N) | → | U23(tt, IL, M, N) | | U23(tt, IL, M, N) | → | cons(N, take(M, IL)) |
| length(nil) | → | 0 | | length(cons(N, L)) | → | U11(tt, L) |
| take(0, IL) | → | nil | | take(s(M), cons(N, IL)) | → | U21(tt, IL, M, N) |
Original Signature
Termination of terms over the following signature is verified: 0, s, zeros, tt, take, length, U11, U12, U23, U21, cons, U22, nil
Strategy
Context-sensitive strategy:
μ(zeros#) = μ(T) = μ(0) = μ(zeros) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(length#) = μ(U21#) = μ(U23#) = μ(s) = μ(length) = μ(U11) = μ(U12) = μ(U23) = μ(U21) = μ(U22) = μ(cons) = {1}
μ(take#) = μ(take) = {1, 2}
The following SCCs where found
| T(take(x_1, x_2)) → T(x_2) | T(take(x_1, x_2)) → T(x_1) |
Problem 5: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| T(take(x_1, x_2)) | → | T(x_2) | | T(take(x_1, x_2)) | → | T(x_1) |
Rewrite Rules
| zeros | → | cons(0, zeros) | | U11(tt, L) | → | U12(tt, L) |
| U12(tt, L) | → | s(length(L)) | | U21(tt, IL, M, N) | → | U22(tt, IL, M, N) |
| U22(tt, IL, M, N) | → | U23(tt, IL, M, N) | | U23(tt, IL, M, N) | → | cons(N, take(M, IL)) |
| length(nil) | → | 0 | | length(cons(N, L)) | → | U11(tt, L) |
| take(0, IL) | → | nil | | take(s(M), cons(N, IL)) | → | U21(tt, IL, M, N) |
Original Signature
Termination of terms over the following signature is verified: 0, s, zeros, tt, take, length, U11, U12, U23, U21, cons, U22, nil
Strategy
Context-sensitive strategy:
μ(zeros#) = μ(T) = μ(0) = μ(zeros) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(length#) = μ(U21#) = μ(U23#) = μ(s) = μ(length) = μ(U11) = μ(U12) = μ(U23) = μ(U21) = μ(cons) = μ(U22) = {1}
μ(take#) = μ(take) = {1, 2}
Polynomial Interpretation
- 0: 0
- T(x): x
- U11(x,y): 0
- U12(x,y): 0
- U21(x1,x2,x3,x4): 0
- U22(x1,x2,x3,x4): 0
- U23(x1,x2,x3,x4): 0
- cons(x,y): 0
- length(x): 0
- nil: 0
- s(x): 0
- take(x,y): y + 2x + 2
- tt: 0
- zeros: 0
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| T(take(x_1, x_2)) | → | T(x_2) | | T(take(x_1, x_2)) | → | T(x_1) |