Term Rewriting System R:
[x]
f(g(a)) -> a
f(f(x)) -> b
g(x) -> f(g(x))
Innermost Termination of R to be shown.
R
↳Removing Redundant Rules for Innermost Termination
Removing the following rules from R which left hand sides contain non normal subterms
f(g(a)) -> a
R
↳RRRI
→TRS2
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
G(x) -> F(g(x))
G(x) -> G(x)
Furthermore, R contains one SCC.
R
↳RRRI
→TRS2
↳DPs
→DP Problem 1
↳Non Termination
Dependency Pair:
G(x) -> G(x)
Rules:
f(f(x)) -> b
g(x) -> f(g(x))
Found an infinite P-chain over R:
P =
G(x) -> G(x)
R =
f(f(x)) -> b
g(x) -> f(g(x))
s = G(x')
evaluates to t =G(x')
Thus, s starts an infinite chain.
Innermost Non-Termination of R could be shown.
Duration:
0:03 minutes