+(

+(

+(0,

+(s(

+(

f(g(f(

f(g(h(

f(h(

R

↳Dependency Pair Analysis

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

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

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

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

F(g(f(x))) -> F(h(s(0),x))

F(g(h(x,y))) -> F(h(s(x),y))

F(h(x, h(y,z))) -> F(h(+(x,y),z))

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

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

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

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

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

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

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

f(g(f(*x*))) -> f(h(s(0),*x*))

f(g(h(*x*,*y*))) -> f(h(s(*x*),*y*))

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

**Dependency Pair:****F(h(***x*, h(*y*,*z*))) -> F(h(+(*x*,*y*),*z*))**Rules:**

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

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

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

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

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

f(g(f(*x*))) -> f(h(s(0),*x*))

f(g(h(*x*,*y*))) -> f(h(s(*x*),*y*))

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

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

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

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

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

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

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

f(g(f(*x*))) -> f(h(s(0),*x*))

f(g(h(*x*,*y*))) -> f(h(s(*x*),*y*))

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

**Dependency Pair:****F(h(***x*, h(*y*,*z*))) -> F(h(+(*x*,*y*),*z*))**Rules:**

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

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

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

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

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

f(g(f(*x*))) -> f(h(s(0),*x*))

f(g(h(*x*,*y*))) -> f(h(s(*x*),*y*))

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

Duration:

0:00 minutes