*(*(

*(+(

*(

R

↳Dependency Pair Analysis

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

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

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

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

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

Furthermore,

R

↳DPs

→DP Problem 1

↳Remaining Obligation(s)

→DP Problem 2

↳Remaining Obligation(s)

The following remains to be proven:

**Dependency Pair:*****'(***x*, +(*y*, f(*z*))) -> *'(g(*x*,*z*), +(*y*,*y*))**Rules:**

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

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

*(*x*, +(*y*, f(*z*))) -> *(g(*x*,*z*), +(*y*,*y*))**Strategy:**innermost

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

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

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

*(*x*, +(*y*, f(*z*))) -> *(g(*x*,*z*), +(*y*,*y*))**Strategy:**innermost

R

↳DPs

→DP Problem 1

↳Remaining Obligation(s)

→DP Problem 2

↳Remaining Obligation(s)

The following remains to be proven:

**Dependency Pair:*****'(***x*, +(*y*, f(*z*))) -> *'(g(*x*,*z*), +(*y*,*y*))**Rules:**

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

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

*(*x*, +(*y*, f(*z*))) -> *(g(*x*,*z*), +(*y*,*y*))**Strategy:**innermost

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

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

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

*(*x*, +(*y*, f(*z*))) -> *(g(*x*,*z*), +(*y*,*y*))**Strategy:**innermost

Duration:

0:00 minutes