g(c(

f(c(s(

f(f(

f(

R

↳Dependency Pair Analysis

G(c(x, s(y))) -> G(c(s(x),y))

F(c(s(x),y)) -> F(c(x, s(y)))

F(f(x)) -> F(d(f(x)))

Furthermore,

R

↳DPs

→DP Problem 1

↳Instantiation Transformation

→DP Problem 2

↳Remaining

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

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

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

f(f(x)) -> f(d(f(x)))

f(x) ->x

On this DP problem, an Instantiation SCC transformation can be performed.

As a result of transforming the rule

one new Dependency Pair is created:

G(c(x, s(y))) -> G(c(s(x),y))

G(c(s(x''), s(y''))) -> G(c(s(s(x'')),y''))

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Inst

→DP Problem 2

↳Remaining Obligation(s)

The following remains to be proven:

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

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

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

f(f(*x*)) -> f(d(f(*x*)))

f(*x*) ->*x***Dependency Pair:****F(c(s(***x*),*y*)) -> F(c(*x*, s(*y*)))**Rules:**

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

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

f(f(*x*)) -> f(d(f(*x*)))

f(*x*) ->*x*

R

↳DPs

→DP Problem 1

↳Inst

→DP Problem 2

↳Remaining Obligation(s)

The following remains to be proven:

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

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

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

f(f(*x*)) -> f(d(f(*x*)))

f(*x*) ->*x***Dependency Pair:****F(c(s(***x*),*y*)) -> F(c(*x*, s(*y*)))**Rules:**

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

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

f(f(*x*)) -> f(d(f(*x*)))

f(*x*) ->*x*

Duration:

0:00 minutes