*(

*(+(

*(

*(1,

R

↳Dependency Pair Analysis

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

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

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

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

Furthermore,

R

↳DPs

→DP Problem 1

↳Remaining Obligation(s)

The following remains to be proven:

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

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

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

*(x, 1) ->x

*(1,y) ->y

Duration:

0:00 minutes