+(0,

+(s(

-(0,

-(

-(s(

R

↳Dependency Pair Analysis

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

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

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

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

-(0,*y*) -> 0

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

-(s(*x*), s(*y*)) -> -(*x*,*y*)**Dependency Pair:****-'(s(***x*), s(*y*)) -> -'(*x*,*y*)**Rules:**

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

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

-(0,*y*) -> 0

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

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

R

↳DPs

→DP Problem 1

↳Remaining Obligation(s)

→DP Problem 2

↳Remaining Obligation(s)

The following remains to be proven:

**Dependency Pair:****+'(s(***x*),*y*) -> +'(*x*,*y*)**Rules:**

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

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

-(0,*y*) -> 0

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

-(s(*x*), s(*y*)) -> -(*x*,*y*)**Dependency Pair:****-'(s(***x*), s(*y*)) -> -'(*x*,*y*)**Rules:**

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

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

-(0,*y*) -> 0

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

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

Duration:

0:00 minutes