*(

*(+(

*(*(

+(+(

R

↳Dependency Pair Analysis

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

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

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

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

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

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

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

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

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

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

Furthermore,

R

↳DPs

→DP Problem 1

↳Remaining Obligation(s)

→DP Problem 2

↳Remaining Obligation(s)

The following remains to be proven:

**Dependency Pairs:****+'(+(***x*,*y*),*z*) -> +'(*y*,*z*)**+'(+(***x*,*y*),*z*) -> +'(*x*, +(*y*,*z*))**Rules:**

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

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

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

+(+(*x*,*y*),*z*) -> +(*x*, +(*y*,*z*))**Dependency Pairs:*****'(*(***x*,*y*),*z*) -> *'(*y*,*z*)***'(*(***x*,*y*),*z*) -> *'(*x*, *(*y*,*z*))***'(+(***y*,*z*),*x*) -> *'(*x*,*z*)***'(+(***y*,*z*),*x*) -> *'(*x*,*y*)***'(***x*, +(*y*,*z*)) -> *'(*x*,*z*)***'(***x*, +(*y*,*z*)) -> *'(*x*,*y*)**Rules:**

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

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

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

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

R

↳DPs

→DP Problem 1

↳Remaining Obligation(s)

→DP Problem 2

↳Remaining Obligation(s)

The following remains to be proven:

**Dependency Pairs:****+'(+(***x*,*y*),*z*) -> +'(*y*,*z*)**+'(+(***x*,*y*),*z*) -> +'(*x*, +(*y*,*z*))**Rules:**

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

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

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

+(+(*x*,*y*),*z*) -> +(*x*, +(*y*,*z*))**Dependency Pairs:*****'(*(***x*,*y*),*z*) -> *'(*y*,*z*)***'(*(***x*,*y*),*z*) -> *'(*x*, *(*y*,*z*))***'(+(***y*,*z*),*x*) -> *'(*x*,*z*)***'(+(***y*,*z*),*x*) -> *'(*x*,*y*)***'(***x*, +(*y*,*z*)) -> *'(*x*,*z*)***'(***x*, +(*y*,*z*)) -> *'(*x*,*y*)**Rules:**

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

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

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

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

Duration:

0:00 minutes