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

Innermost Termination of R to be shown.



   TRS
Reversing
Rev
DPs




Rule(s) before reversing:

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


Rule(s) after reversing:

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





Trying another alternative:
   TRS
Rev
Reversing
DPs




Rule(s) before reversing:

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


Rule(s) after reversing:

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





Trying another alternative:
   TRS
Rev
Rev
Dependency Pair Analysis



R contains the following Dependency Pairs:

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

Furthermore, R contains one SCC.


   TRS
Rev
Rev
DPs
       →DP Problem 1
Non Termination


Dependency Pairs:

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


Rule:


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


Strategy:

innermost




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

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

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