Term Rewriting System R:

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

Termination of R to be shown.


R contains the following Dependency Pairs: 


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

Furthermore, R contains one SCC.


SCC1:

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

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


Non-Termination of R could be shown.

Duration: 1.65 seconds.