(0) Obligation:

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

+(x, +(y, z)) → +(+(x, y), z)
*(x, +(y, z)) → +(*(x, y), *(x, z))
+(+(x, *(y, z)), *(y, u)) → +(x, *(y, +(z, u)))

Q is empty.