f(

f(

f(

f(a(

f(b(

f(c(

R

↳Dependency Pair Analysis

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

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

F(x, c(a(y))) -> F(c(a(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(b( x), y) -> F(x, b(y))**

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

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

f(x, c(a(y))) -> f(c(a(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.

6 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(b( x), y) -> F(x, b(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(b( x), y) -> F(x, b(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:

There is only one SCC in the graph and, thus, we obtain one new DP problem.

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

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

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

R

↳DPs

→DP Problem 1

↳MRR

→DP Problem 2

↳NOC

...

→DP Problem 4

↳Modular Removal of Rules

**A(b( x)) -> A(x)**

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

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

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

We have the following set of usable rules:

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

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

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

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

Polynomial interpretation:

_{ }^{ }POL(c(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(C(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(B(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(b(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(a(x)_{1})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(A(x)_{1})= 1 + x _{1}_{ }^{ }

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

The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:

C(a(x)) -> C(x)

No Rules can be deleted.

The result of this processor delivers one new DP problem.

R

↳DPs

→DP Problem 1

↳MRR

→DP Problem 2

↳NOC

...

→DP Problem 5

↳Modular Removal of Rules

**A(b( x)) -> A(x)**

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

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

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

We have the following set of usable rules:

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

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

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

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

Polynomial interpretation:

_{ }^{ }POL(c(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(C(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(B(x)_{1})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(b(x)_{1})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(a(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(A(x)_{1})= x _{1}_{ }^{ }

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

The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:

A(b(x)) -> A(x)

No Rules can be deleted.

The result of this processor delivers one new DP problem.

R

↳DPs

→DP Problem 1

↳MRR

→DP Problem 2

↳NOC

...

→DP Problem 6

↳Modular Removal of Rules

**B(c( x)) -> B(x)**

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

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

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

We have the following set of usable rules:

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

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

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

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

Polynomial interpretation:

_{ }^{ }POL(c(x)_{1})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(C(x)_{1})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(B(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(b(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(a(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(A(x)_{1})= x _{1}_{ }^{ }

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

The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:

B(c(x)) -> B(x)

No Rules can be deleted.

The result of this processor delivers one new DP problem.

R

↳DPs

→DP Problem 1

↳MRR

→DP Problem 2

↳NOC

...

→DP Problem 7

↳Negative Polynomial Order

**B(c( x)) -> C(b(x))**

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

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

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

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

B(c(x)) -> C(b(x))

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

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

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

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

Used ordering:

Polynomial Order with Interpretation:

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

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

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

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

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

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

This results in one new DP problem.

R

↳DPs

→DP Problem 1

↳MRR

→DP Problem 2

↳NOC

...

→DP Problem 8

↳Dependency Graph

**A(b( x)) -> B(a(x))**

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

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

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

Using the Dependency Graph resulted in no new DP problems.

Duration:

0:00 minutes