s(a) -> a

s(s(

s(f(

s(g(

f(

f(a,

f(g(

g(a, a) -> a

R

↳Dependency Pair Analysis

S(f(x,y)) -> F(s(y), s(x))

S(f(x,y)) -> S(y)

S(f(x,y)) -> S(x)

S(g(x,y)) -> G(s(x), s(y))

S(g(x,y)) -> S(x)

S(g(x,y)) -> S(y)

F(g(x,y), g(u,v)) -> G(f(x,u), f(y,v))

F(g(x,y), g(u,v)) -> F(x,u)

F(g(x,y), g(u,v)) -> F(y,v)

Furthermore,

R

↳DPs

→DP Problem 1

↳Remaining Obligation(s)

→DP Problem 2

↳Remaining Obligation(s)

The following remains to be proven:

**Dependency Pairs:****F(g(***x*,*y*), g(*u*,*v*)) -> F(*y*,*v*)**F(g(***x*,*y*), g(*u*,*v*)) -> F(*x*,*u*)**Rules:**

s(a) -> a

s(s(*x*)) ->*x*

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

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

f(*x*, a) ->*x*

f(a,*y*) ->*y*

f(g(*x*,*y*), g(*u*,*v*)) -> g(f(*x*,*u*), f(*y*,*v*))

g(a, a) -> a**Dependency Pairs:****S(g(***x*,*y*)) -> S(*y*)**S(g(***x*,*y*)) -> S(*x*)**S(f(***x*,*y*)) -> S(*x*)**S(f(***x*,*y*)) -> S(*y*)**Rules:**

s(a) -> a

s(s(*x*)) ->*x*

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

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

f(*x*, a) ->*x*

f(a,*y*) ->*y*

f(g(*x*,*y*), g(*u*,*v*)) -> g(f(*x*,*u*), f(*y*,*v*))

g(a, a) -> a

R

↳DPs

→DP Problem 1

↳Remaining Obligation(s)

→DP Problem 2

↳Remaining Obligation(s)

The following remains to be proven:

**Dependency Pairs:****F(g(***x*,*y*), g(*u*,*v*)) -> F(*y*,*v*)**F(g(***x*,*y*), g(*u*,*v*)) -> F(*x*,*u*)**Rules:**

s(a) -> a

s(s(*x*)) ->*x*

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

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

f(*x*, a) ->*x*

f(a,*y*) ->*y*

f(g(*x*,*y*), g(*u*,*v*)) -> g(f(*x*,*u*), f(*y*,*v*))

g(a, a) -> a**Dependency Pairs:****S(g(***x*,*y*)) -> S(*y*)**S(g(***x*,*y*)) -> S(*x*)**S(f(***x*,*y*)) -> S(*x*)**S(f(***x*,*y*)) -> S(*y*)**Rules:**

s(a) -> a

s(s(*x*)) ->*x*

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

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

f(*x*, a) ->*x*

f(a,*y*) ->*y*

f(g(*x*,*y*), g(*u*,*v*)) -> g(f(*x*,*u*), f(*y*,*v*))

g(a, a) -> a

Duration:

0:00 minutes