The TRS could be proven non-terminating. The proof took 315 ms.
The following reduction sequence is a witness for non-termination:
h#(c) →* h#(c)
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (0ms).
| – Problem 2 was processed with processor BackwardInstantiation (2ms).
| | – Problem 3 was processed with processor Propagation (2ms).
| | | – Problem 4 was processed with processor BackwardsNarrowing (1ms).
| | | | – Problem 5 remains open; application of the following processors failed [BackwardsNarrowing (0ms), BackwardInstantiation (1ms), ForwardInstantiation (0ms), Propagation (1ms), BackwardsNarrowing (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
Parameters
- Use inverse cap function: true
- Use strongly defined symbols: false
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:
Caught Exception: class java.lang.ThreadDeath
null
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: BackwardsNarrowing
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
Parameters
- Use original terms restriction: true
- Narrowing normal form lookahead: 2
The left-hand side of the rule h
#(d) → h
#(c) 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 |
|---|
| h#(c) | |
Thus, the rule h
#(d) → h
#(c) is replaced by the following rules: