f(s(

f(

R

↳Dependency Pair Analysis

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

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

Furthermore,

R

↳DPs

→DP Problem 1

↳Forward Instantiation Transformation

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

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

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

innermost

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

As a result of transforming the rule

two new Dependency Pairs are created:

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

F(s(y''), s(y0)) -> F(y0, s(y''))

F(x0, s(s(x''))) -> F(s(x''),x0)

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳FwdInst

→DP Problem 2

↳Forward Instantiation Transformation

**F( x0, s(s(x''))) -> F(s(x''), x0)**

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

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

innermost

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

As a result of transforming the rule

three new Dependency Pairs are created:

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

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

F(s(s(y'''')),y) -> F(s(y''''), s(s(y'''')))

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

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳FwdInst

→DP Problem 2

↳FwdInst

...

→DP Problem 3

↳Remaining Obligation(s)

The following remains to be proven:

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

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

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

innermost

Duration:

0:00 minutes