+(

+(

f(0, s(0),

g(

g(

R

↳Dependency Pair Analysis

+'(X, s(Y)) -> +'(X,Y)

F(0, s(0),X) -> F(X, +(X,X),X)

F(0, s(0),X) -> +'(X,X)

Furthermore,

R

↳DPs

→DP Problem 1

↳Remaining Obligation(s)

→DP Problem 2

↳Remaining Obligation(s)

The following remains to be proven:

**Dependency Pair:****+'(***X*, s(*Y*)) -> +'(*X*,*Y*)**Rules:**

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

+(*X*, s(*Y*)) -> s(+(*X*,*Y*))

f(0, s(0),*X*) -> f(*X*, +(*X*,*X*),*X*)

g(*X*,*Y*) ->*X*

g(*X*,*Y*) ->*Y***Dependency Pair:****F(0, s(0),***X*) -> F(*X*, +(*X*,*X*),*X*)**Rules:**

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

+(*X*, s(*Y*)) -> s(+(*X*,*Y*))

f(0, s(0),*X*) -> f(*X*, +(*X*,*X*),*X*)

g(*X*,*Y*) ->*X*

g(*X*,*Y*) ->*Y*

R

↳DPs

→DP Problem 1

↳Remaining Obligation(s)

→DP Problem 2

↳Remaining Obligation(s)

The following remains to be proven:

**Dependency Pair:****+'(***X*, s(*Y*)) -> +'(*X*,*Y*)**Rules:**

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

+(*X*, s(*Y*)) -> s(+(*X*,*Y*))

f(0, s(0),*X*) -> f(*X*, +(*X*,*X*),*X*)

g(*X*,*Y*) ->*X*

g(*X*,*Y*) ->*Y***Dependency Pair:****F(0, s(0),***X*) -> F(*X*, +(*X*,*X*),*X*)**Rules:**

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

+(*X*, s(*Y*)) -> s(+(*X*,*Y*))

f(0, s(0),*X*) -> f(*X*, +(*X*,*X*),*X*)

g(*X*,*Y*) ->*X*

g(*X*,*Y*) ->*Y*

Duration:

0:00 minutes