*(*(

*(+(

*(

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))

innermost

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

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

**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

↳Inst

→DP Problem 2

↳Remaining Obligation(s)

The following remains to be proven:

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

**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