(0) Obligation:

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

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

Q is empty.