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

h#g#g#h#

Rewrite Rules

ghcd
hg

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

The dependency pairs h# → g# and g# → h# are consolidated into the rule h# → h# .

This is possible as

The dependency pairs g# → h# and h# → g# are consolidated into the rule g# → g# .

This is possible as

The dependency pairs g# → h# and h# → g# are consolidated into the rule g# → g# .

This is possible as


Summary

Removed Dependency PairsAdded Dependency Pairs
h# → g#g# → g#
g# → h#h# → h#