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