f(s(

f(0) -> 0

p(s(

TRS

↳Dependency Pair Analysis

F(s(x)) -> F(f(p(s(x))))

F(s(x)) -> F(p(s(x)))

F(s(x)) -> P(s(x))

Furthermore,

TRS

↳DPs

→DP Problem 1

↳Non-Overlappingness Check

**F(s( x)) -> F(p(s(x)))**

f(s(x)) -> s(f(f(p(s(x)))))

f(0) -> 0

p(s(x)) ->x

R does not overlap into P. Moreover, R is locally confluent (all critical pairs are trivially joinable).Hence we can switch to innermost.

The transformation is resulting in one subcycle:

TRS

↳DPs

→DP Problem 1

↳NOC

→DP Problem 2

↳Rewriting Transformation

**F(s( x)) -> F(p(s(x)))**

f(s(x)) -> s(f(f(p(s(x)))))

f(0) -> 0

p(s(x)) ->x

innermost

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

As a result of transforming the rule

one new Dependency Pair is created:

F(s(x)) -> F(f(p(s(x))))

F(s(x)) -> F(f(x))

The transformation is resulting in one new DP problem:

TRS

↳DPs

→DP Problem 1

↳NOC

→DP Problem 2

↳Rw

...

→DP Problem 3

↳Rewriting Transformation

**F(s( x)) -> F(f(x))**

f(s(x)) -> s(f(f(p(s(x)))))

f(0) -> 0

p(s(x)) ->x

innermost

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

As a result of transforming the rule

one new Dependency Pair is created:

F(s(x)) -> F(p(s(x)))

F(s(x)) -> F(x)

The transformation is resulting in one new DP problem:

TRS

↳DPs

→DP Problem 1

↳NOC

→DP Problem 2

↳Rw

...

→DP Problem 4

↳Negative Polynomial Order

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

f(s(x)) -> s(f(f(p(s(x)))))

f(0) -> 0

p(s(x)) ->x

innermost

The following Dependency Pairs can be strictly oriented using the given order.

F(s(x)) -> F(x)

F(s(x)) -> F(f(x))

Moreover, the following usable rules (regarding the implicit AFS) are oriented.

f(0) -> 0

p(s(x)) ->x

f(s(x)) -> s(f(f(p(s(x)))))

Used ordering:

Polynomial Order with Interpretation:

**POL( **F(x_{1})** )** = x_{1}

**POL( **s(x_{1})** )** = x_{1} + 1

**POL( **f(x_{1})** )** = x_{1}

**POL( **0** )** = 0

**POL( **p(x_{1})** )** = max{0, x_{1} - 1}

This results in one new DP problem.

TRS

↳DPs

→DP Problem 1

↳NOC

→DP Problem 2

↳Rw

...

→DP Problem 5

↳Dependency Graph

f(s(x)) -> s(f(f(p(s(x)))))

f(0) -> 0

p(s(x)) ->x

innermost

Using the Dependency Graph resulted in no new DP problems.

Duration:

0:00 minutes