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