+(

+(

+(+(

*(

*(+(

R

↳Dependency Pair Analysis

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

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

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

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

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

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

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

+(*x*, i(*x*)) -> 0

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

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

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

+(*x*, 0) ->*x*

+(*x*, i(*x*)) -> 0

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

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

*(+(*x*,*y*),*z*) -> +(*(*x*,*z*), *(*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*, 0) ->*x*

+(*x*, i(*x*)) -> 0

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

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

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

+(*x*, 0) ->*x*

+(*x*, i(*x*)) -> 0

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

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

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

Duration:

0:00 minutes