(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

a(a(x)) → a(b(a(x)))

Q is empty.