+(

+(+(

*(

R

↳Dependency Pair Analysis

+'(x, +(y,z)) -> +'(+(x,y),z)

+'(x, +(y,z)) -> +'(x,y)

+'(+(x, *(y,z)), *(y,u)) -> +'(x, *(y, +(z,u)))

+'(+(x, *(y,z)), *(y,u)) -> *'(y, +(z,u))

+'(+(x, *(y,z)), *(y,u)) -> +'(z,u)

*'(x, +(y,z)) -> +'(*(x,y), *(x,z))

*'(x, +(y,z)) -> *'(x,y)

*'(x, +(y,z)) -> *'(x,z)

Furthermore,

R

↳DPs

→DP Problem 1

↳Remaining Obligation(s)

The following remains to be proven:

***'( x, +(y, z)) -> *'(x, y)**

+(x, +(y,z)) -> +(+(x,y),z)

+(+(x, *(y,z)), *(y,u)) -> +(x, *(y, +(z,u)))

*(x, +(y,z)) -> +(*(x,y), *(x,z))

innermost

Duration:

0:00 minutes