exp(

exp(

*(0,

*(s(

-(0,

-(

-(s(

R

↳Dependency Pair Analysis

EXP(x, s(y)) -> *'(x, exp(x,y))

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

*'(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)

→DP Problem 3

↳Remaining Obligation(s)

The following remains to be proven:

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

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

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

*(0,*y*) -> 0

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

-(0,*y*) -> 0

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

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

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

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

*(0,*y*) -> 0

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

-(0,*y*) -> 0

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

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

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

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

*(0,*y*) -> 0

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

→DP Problem 3

↳Remaining Obligation(s)

The following remains to be proven:

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

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

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

*(0,*y*) -> 0

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

-(0,*y*) -> 0

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

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

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

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

*(0,*y*) -> 0

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

-(0,*y*) -> 0

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

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

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

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

*(0,*y*) -> 0

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

→DP Problem 3

↳Remaining Obligation(s)

The following remains to be proven:

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

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

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

*(0,*y*) -> 0

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

-(0,*y*) -> 0

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

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

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

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

*(0,*y*) -> 0

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

-(0,*y*) -> 0

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

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

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

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

*(0,*y*) -> 0

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

-(0,*y*) -> 0

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

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

Duration:

0:00 minutes