The TRS could be proven non-terminating. The proof took 174 ms.
The following reduction sequence is a witness for non-termination:
g# →* g#
The following DP Processors were used
Problem 1 was processed with processor Propagation (2ms).
| – Problem 2 remains open; application of the following processors failed [ForwardNarrowing (0ms), BackwardInstantiation (1ms), ForwardInstantiation (1ms), Propagation (2ms)].
Problem 1: Propagation
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
Original Signature
Termination of terms over the following signature is verified: g, d, c, h
Strategy
The dependency pairs h
# → g
# and g
# → h
# are consolidated into the rule h
# → h
# .
This is possible as
- all subterms of g# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in g#, but non-replacing in both h# and h#
The dependency pairs h
# → g
# and g
# → h
# are consolidated into the rule h
# → h
# .
This is possible as
- all subterms of g# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in g#, but non-replacing in both h# and h#
The dependency pairs g
# → h
# and h
# → g
# are consolidated into the rule g
# → g
# .
This is possible as
- all subterms of h# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in h#, but non-replacing in both g# and g#
The dependency pairs g
# → h
# and h
# → g
# are consolidated into the rule g
# → g
# .
This is possible as
- all subterms of h# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in h#, but non-replacing in both g# and g#
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| h# → g# | g# → g# |
| g# → h# | h# → h# |