Term Rewriting System R:

   [x]
   a(b(x)) -> b(b(a(a(x))))

Termination of R to be shown.


This program has no overlaps, so it is sufficient to show innermost termination. 


R contains the following Dependency Pairs: 


   A(b(x)) -> A(a(x))
   A(b(x)) -> A(x)

Furthermore, R contains one SCC.


SCC1:

A(b(x)) -> A(x)
A(b(x)) -> A(a(x))

Found an infinite P-chain over R:
P = A(b(x)) -> A(x)
A(b(x)) -> A(a(x))
R = [a(b(x)) -> b(b(a(a(x))))]
s = A(b(b(x''))) evaluates to t = A(b(b(a(a(x'')))))
Thus, s starts an infinite reduction as s matches t.


Non-Termination of R could be shown.

Duration: 0.702 seconds.