app(f, app(g,

app(f, app(h,

R

↳Dependency Pair Analysis

APP(f, app(g,x)) -> APP(g, app(f, app(f,x)))

APP(f, app(g,x)) -> APP(f, app(f,x))

APP(f, app(g,x)) -> APP(f,x)

APP(f, app(h,x)) -> APP(h, app(g,x))

APP(f, app(h,x)) -> APP(g,x)

Furthermore,

R

↳DPs

→DP Problem 1

↳A-Transformation

**APP(f, app(g, x)) -> APP(f, x)**

app(f, app(g,x)) -> app(g, app(f, app(f,x)))

app(f, app(h,x)) -> app(h, app(g,x))

innermost

We have an applicative DP problem with proper arity. Thus we can use the A-Transformation to obtain one new DP problem which consists of the A-transformed TRSs.

R

↳DPs

→DP Problem 1

↳ATrans

→DP Problem 2

↳Negative Polynomial Order

**F(g( x)) -> F(x)**

f(g(x)) -> g(f(f(x)))

f(h(x)) -> h(g(x))

innermost

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

F(g(x)) -> F(x)

F(g(x)) -> F(f(x))

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

f(h(x)) -> h(g(x))

f(g(x)) -> g(f(f(x)))

Used ordering:

Polynomial Order with Interpretation:

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

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

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

**POL( **h(x_{1})** )** = 0

This results in one new DP problem.

R

↳DPs

→DP Problem 1

↳ATrans

→DP Problem 2

↳Neg POLO

...

→DP Problem 3

↳Dependency Graph

f(g(x)) -> g(f(f(x)))

f(h(x)) -> h(g(x))

innermost

Using the Dependency Graph resulted in no new DP problems.

Duration:

0:00 minutes