(0) Obligation:

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

a(x, y) → b(x, b(0, c(y)))
c(b(y, c(x))) → c(c(b(a(0, 0), y)))
b(y, 0) → y

Q is empty.