f(+(

+(

R

↳Dependency Pair Analysis

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

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

+'(x, +(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 Pair:****F(+(***x*, 0)) -> F(*x*)**Rules:**

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

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

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

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

R

↳DPs

→DP Problem 1

↳Remaining Obligation(s)

→DP Problem 2

↳Remaining Obligation(s)

The following remains to be proven:

**Dependency Pair:****F(+(***x*, 0)) -> F(*x*)**Rules:**

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

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

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

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

Duration:

0:00 minutes