Term Rewriting System R:
[X]
g(X) -> h(X)
c -> d
h(d) -> g(c)
Termination of R to be shown.
TRS
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
G(X) -> H(X)
H(d) -> G(c)
H(d) -> C
Furthermore, R contains one SCC.
TRS
↳DPs
→DP Problem 1
↳Non Termination
Dependency Pairs:
H(d) -> G(c)
G(X) -> H(X)
Rules:
g(X) -> h(X)
c -> d
h(d) -> g(c)
Found an infinite P-chain over R:
P =
H(d) -> G(c)
G(X) -> H(X)
R =
g(X) -> h(X)
c -> d
h(d) -> g(c)
s = G(c)
evaluates to t =G(c)
Thus, s starts an infinite chain.
Non-Termination of R could be shown.
Duration:
0:00 minutes