Term Rewriting System R:
[x]
f(g(a)) -> f(s(g(b)))
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)) -> f(s(g(b)))


   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:01 minutes