f(

f(a(

f(b(

f(c(

R

↳Dependency Pair Analysis

F(x, a(b(c(y)))) -> F(b(c(a(b(x)))),y)

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

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

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

Furthermore,

R

↳DPs

→DP Problem 1

↳Modular Removal of Rules

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

f(x, a(b(c(y)))) -> f(b(c(a(b(x)))),y)

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

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

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

We have the following set of usable rules: none

To remove rules and DPs from this DP problem we used the following monotonic and C

Polynomial interpretation:

_{ }^{ }POL(c(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(b(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(a(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(F(x)_{1}, x_{2})= 1 + x _{1}+ x_{2}_{ }^{ }

We have the following set D of usable symbols: {c, b, a, F}

No Dependency Pairs can be deleted.

4 non usable rules have been deleted.

The result of this processor delivers one new DP problem.

R

↳DPs

→DP Problem 1

↳MRR

→DP Problem 2

↳Non-Overlappingness Check

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

none

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:

R

↳DPs

→DP Problem 1

↳MRR

→DP Problem 2

↳NOC

...

→DP Problem 3

↳Scc To SRS

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

none

innermost

It has been determined that showing finiteness of this DP problem is equivalent to showing termination of a string rewrite system.

(Re)applying the dependency pair method (incl. the dependency graph) for the following SRS:

The graph does not contain any SCC and, thus, we obtain no new DP problems.

a(b(c(x))) -> b(a(c(b(x))))

Duration:

0:00 minutes