*(*(

*(+(

*(

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

↳Instantiation Transformation

→DP Problem 2

↳Remaining

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

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

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

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

On this DP problem, an Instantiation SCC transformation can be performed.

As a result of transforming the rule

one new Dependency Pair is created:

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

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

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Inst

→DP Problem 2

↳Remaining Obligation(s)

The following remains to be proven:

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

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

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

*(*x*, +(*y*, f(*z*))) -> *(g(*x*,*z*), +(*y*,*y*))**Dependency Pairs:*****'(+(***x*,*y*),*z*) -> *'(*y*,*z*)***'(+(***x*,*y*),*z*) -> *'(*x*,*z*)***'(*(***x*,*y*),*z*) -> *'(*y*,*z*)***'(*(***x*,*y*),*z*) -> *'(*x*, *(*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*))

R

↳DPs

→DP Problem 1

↳Inst

→DP Problem 2

↳Remaining Obligation(s)

The following remains to be proven:

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

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

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

*(*x*, +(*y*, f(*z*))) -> *(g(*x*,*z*), +(*y*,*y*))**Dependency Pairs:*****'(+(***x*,*y*),*z*) -> *'(*y*,*z*)***'(+(***x*,*y*),*z*) -> *'(*x*,*z*)***'(*(***x*,*y*),*z*) -> *'(*y*,*z*)***'(*(***x*,*y*),*z*) -> *'(*x*, *(*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*))

Duration:

0:00 minutes