NO
The TRS could be proven non-terminating. The proof took 757 ms.
The following reduction sequence is a witness for non-termination:
g#(n__c) →* g#(n__c)
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (24ms).
| – Problem 2 was processed with processor ForwardNarrowing (1ms).
| | – Problem 3 was processed with processor ForwardNarrowing (1ms).
| | | – Problem 4 was processed with processor ForwardNarrowing (1ms).
| | | | – Problem 5 was processed with processor ForwardNarrowing (1ms).
| | | | | – Problem 6 was processed with processor ForwardNarrowing (1ms).
| | | | | | – Problem 7 was processed with processor BackwardInstantiation (2ms).
| | | | | | | – Problem 8 was processed with processor Propagation (2ms).
| | | | | | | | – Problem 9 was processed with processor ForwardNarrowing (1ms).
| | | | | | | | | – Problem 10 remains open; application of the following processors failed [ForwardNarrowing (1ms), BackwardInstantiation (2ms), ForwardInstantiation (3ms), Propagation (2ms), ForwardNarrowing (1ms), BackwardInstantiation (2ms), ForwardInstantiation (2ms), Propagation (3ms)].
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| g#(X) | → | activate#(X) | | g#(X) | → | h#(activate(X)) |
| c# | → | d# | | activate#(n__c) | → | c# |
| activate#(n__d) | → | d# | | h#(n__d) | → | g#(n__c) |
Rewrite Rules
| g(X) | → | h(activate(X)) | | c | → | d |
| h(n__d) | → | g(n__c) | | d | → | n__d |
| c | → | n__c | | activate(n__d) | → | d |
| activate(n__c) | → | c | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, n__d, g, d, n__c, c, h
Strategy
The following SCCs where found
| g#(X) → h#(activate(X)) | h#(n__d) → g#(n__c) |
Problem 2: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| g#(X) | → | h#(activate(X)) | | h#(n__d) | → | g#(n__c) |
Rewrite Rules
| g(X) | → | h(activate(X)) | | c | → | d |
| h(n__d) | → | g(n__c) | | d | → | n__d |
| c | → | n__c | | activate(n__d) | → | d |
| activate(n__c) | → | c | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, n__d, g, d, n__c, c, h
Strategy
The right-hand side of the rule g
#(
X) → h
#(activate(
X)) is 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 |
|---|
| h#(d) | |
| h#(c) | |
| h#(_x21) | |
Thus, the rule g
#(
X) → h
#(activate(
X)) is replaced by the following rules:
| g#(_x21) → h#(_x21) | g#(n__d) → h#(d) |
| g#(n__c) → h#(c) |
Problem 3: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| g#(_x21) | → | h#(_x21) | | g#(n__d) | → | h#(d) |
| g#(n__c) | → | h#(c) | | h#(n__d) | → | g#(n__c) |
Rewrite Rules
| g(X) | → | h(activate(X)) | | c | → | d |
| h(n__d) | → | g(n__c) | | d | → | n__d |
| c | → | n__c | | activate(n__d) | → | d |
| activate(n__c) | → | c | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: n__d, activate, g, d, n__c, c, h
Strategy
The right-hand side of the rule g
#(n__c) → h
#(c) is 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 |
|---|
| h#(d) | |
| h#(n__c) | |
Thus, the rule g
#(n__c) → h
#(c) is replaced by the following rules:
| g#(n__c) → h#(n__c) | g#(n__c) → h#(d) |
Problem 4: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| g#(_x21) | → | h#(_x21) | | g#(n__d) | → | h#(d) |
| g#(n__c) | → | h#(n__c) | | g#(n__c) | → | h#(d) |
| h#(n__d) | → | g#(n__c) |
Rewrite Rules
| g(X) | → | h(activate(X)) | | c | → | d |
| h(n__d) | → | g(n__c) | | d | → | n__d |
| c | → | n__c | | activate(n__d) | → | d |
| activate(n__c) | → | c | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, n__d, g, d, n__c, c, h
Strategy
The right-hand side of the rule g
#(n__d) → h
#(d) is 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 |
|---|
| h#(n__d) | |
Thus, the rule g
#(n__d) → h
#(d) is replaced by the following rules:
Problem 5: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| g#(_x21) | → | h#(_x21) | | g#(n__d) | → | h#(n__d) |
| g#(n__c) | → | h#(n__c) | | g#(n__c) | → | h#(d) |
| h#(n__d) | → | g#(n__c) |
Rewrite Rules
| g(X) | → | h(activate(X)) | | c | → | d |
| h(n__d) | → | g(n__c) | | d | → | n__d |
| c | → | n__c | | activate(n__d) | → | d |
| activate(n__c) | → | c | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: n__d, activate, g, d, n__c, c, h
Strategy
The right-hand side of the rule g
#(n__c) → h
#(n__c) is 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 |
|---|
Thus, the rule g
#(n__c) → h
#(n__c) is deleted.
Problem 6: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| g#(_x21) | → | h#(_x21) | | g#(n__d) | → | h#(n__d) |
| g#(n__c) | → | h#(d) | | h#(n__d) | → | g#(n__c) |
Rewrite Rules
| g(X) | → | h(activate(X)) | | c | → | d |
| h(n__d) | → | g(n__c) | | d | → | n__d |
| c | → | n__c | | activate(n__d) | → | d |
| activate(n__c) | → | c | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, n__d, g, d, n__c, c, h
Strategy
The right-hand side of the rule g
#(n__c) → h
#(d) is 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 |
|---|
| h#(n__d) | |
Thus, the rule g
#(n__c) → h
#(d) is replaced by the following rules:
Problem 7: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| g#(n__c) | → | h#(n__d) | | g#(_x21) | → | h#(_x21) |
| g#(n__d) | → | h#(n__d) | | h#(n__d) | → | g#(n__c) |
Rewrite Rules
| g(X) | → | h(activate(X)) | | c | → | d |
| h(n__d) | → | g(n__c) | | d | → | n__d |
| c | → | n__c | | activate(n__d) | → | d |
| activate(n__c) | → | c | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: n__d, activate, g, d, n__c, c, h
Strategy
Instantiation
For all potential predecessors l → r of the rule g
#(
_x21) → h
#(
_x21) on dependency pair chains it holds that:
- g#(_x21) matches r,
- all variables of g#(_x21) are embedded in constructor contexts, i.e., each subterm of g#(_x21), containing a variable is rooted by a constructor symbol.
Thus, g
#(
_x21) → h
#(
_x21) is replaced by instances determined through the above matching. These instances are:
Problem 8: Propagation
Dependency Pair Problem
Dependency Pairs
| g#(n__c) | → | h#(n__d) | | g#(n__d) | → | h#(n__d) |
| g#(n__c) | → | h#(n__c) | | h#(n__d) | → | g#(n__c) |
Rewrite Rules
| g(X) | → | h(activate(X)) | | c | → | d |
| h(n__d) | → | g(n__c) | | d | → | n__d |
| c | → | n__c | | activate(n__d) | → | d |
| activate(n__c) | → | c | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, n__d, g, d, n__c, c, h
Strategy
The dependency pairs g
#(n__c) → h
#(n__d) and h
#(n__d) → g
#(n__c) are consolidated into the rule g
#(n__c) → g
#(n__c) .
This is possible as
- all subterms of h#(n__d) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in h#(n__d), but non-replacing in both g#(n__c) and g#(n__c)
The dependency pairs h
#(n__d) → g
#(n__c) and g
#(n__c) → h
#(n__d) are consolidated into the rule h
#(n__d) → h
#(n__d) .
This is possible as
- all subterms of g#(n__c) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in g#(n__c), but non-replacing in both h#(n__d) and h#(n__d)
The dependency pairs h
#(n__d) → g
#(n__c) and g
#(n__c) → h
#(n__d) are consolidated into the rule h
#(n__d) → h
#(n__d) .
This is possible as
- all subterms of g#(n__c) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in g#(n__c), but non-replacing in both h#(n__d) and h#(n__d)
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| g#(n__c) → h#(n__d) | g#(n__c) → g#(n__c) |
| h#(n__d) → g#(n__c) | h#(n__d) → h#(n__d) |
Problem 9: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| g#(n__c) | → | g#(n__c) | | g#(n__d) | → | h#(n__d) |
| h#(n__d) | → | h#(n__d) | | g#(n__c) | → | h#(n__c) |
Rewrite Rules
| g(X) | → | h(activate(X)) | | c | → | d |
| h(n__d) | → | g(n__c) | | d | → | n__d |
| c | → | n__c | | activate(n__d) | → | d |
| activate(n__c) | → | c | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: n__d, activate, g, d, n__c, c, h
Strategy
The right-hand side of the rule g
#(n__c) → h
#(n__c) is 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 |
|---|
Thus, the rule g
#(n__c) → h
#(n__c) is deleted.