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

Termination of R to be shown. 



   TRS
     ↳Reversing
     ↳StSym
     ↳Rev
     ↳DPs




Rule(s) before reversing:

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


Rule(s) after reversing:

b'(a'(b'(a'(x)))) -> b'(a'(a'(b'(a'(b'(x))))))




Trying another alternative: 
   TRS
     ↳Rev
     ↳Stripping Symbols
     ↳Rev
     ↳DPs



The last symbol could be stripped
The system before stripping:

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

Continuing working on this following system:

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




Trying another alternative: 
   TRS
     ↳Rev
     ↳StSym
     ↳Reversing
     ↳DPs




Rule(s) before reversing:

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


Rule(s) after reversing:

b'(a'(b'(a'(x)))) -> b'(a'(a'(b'(a'(b'(x))))))



   TRS
     ↳Rev
     ↳StSym
     ↳Rev
       →TRS4
         ↳Stripping Symbols
     ↳DPs



The first symbol could be stripped
The system before stripping:

b'(a'(b'(a'(x)))) -> b'(a'(a'(b'(a'(b'(x))))))

Continuing working on this following system:

a'(b'(a'(x))) -> a'(a'(b'(a'(b'(x)))))




Trying another alternative: 
   TRS
     ↳Rev
     ↳StSym
     ↳Rev
     ↳Dependency Pair Analysis



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. 


   TRS
     ↳Rev
     ↳StSym
     ↳Rev
     ↳DPs
       →DP Problem 1
         ↳Non Termination


Dependency Pairs:

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


Rule:


a(b(a(b(x)))) -> b(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(a(b(a(b(x'')))))))
evaluates to t =A(b(a(a(b(a(b(a(a(b(x''))))))))))

Thus, s starts an infinite chain as s matches t.

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