Term Rewriting System R:
[x]
f(g(a)) -> a
f(f(x)) -> b
g(x) -> f(g(x))

Termination of R to be shown. 



   TRS
     ↳Removing Redundant Rules



Removing the following rules from R which fullfill a polynomial ordering:

f(g(a)) -> a

where the Polynomial interpretation:
  POL(g(x1))=  1 + x1  
  POL(b)=  0  
  POL(a)=  0  
  POL(f(x1))=  x1  
was used.

Not all Rules of R can be deleted, so we still have to regard a part of R. 


   TRS
     ↳RRRPolo
       →TRS2
         ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

G(x) -> F(g(x))
G(x) -> G(x)

Furthermore, R contains one SCC. 


   TRS
     ↳RRRPolo
       →TRS2
         ↳DPs
           →DP Problem 1
             ↳Non Termination


Dependency Pair:

G(x) -> G(x)


Rules:


g(x) -> f(g(x))
f(f(x)) -> b





Found an infinite P-chain over R:
P =

G(x) -> G(x)

R =

g(x) -> f(g(x))
f(f(x)) -> b

s = G(x')
evaluates to t =G(x')

Thus, s starts an infinite chain.

Non-Termination of R could be shown.
Duration:
0:01 minutes