f(a, f(b,

f(b, f(c,

f(c, f(a,

R

↳Dependency Pair Analysis

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

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

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

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

F(c, f(a,x)) -> F(a, f(c,x))

F(c, f(a,x)) -> F(c,x)

Furthermore,

R

↳DPs

→DP Problem 1

↳A-Transformation

**F(b, f(c, x)) -> F(b, x)**

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

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

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

↳Modular Removal of Rules

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

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

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

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

innermost

We have the following set of usable rules:

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

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

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

a(b(x)) -> b(a(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

↳ATrans

→DP Problem 2

↳MRR

...

→DP Problem 3

↳Modular Removal of Rules

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

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

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

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

innermost

We have the following set of usable rules:

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

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

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

a(b(x)) -> b(a(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

↳ATrans

→DP Problem 2

↳MRR

...

→DP Problem 4

↳Modular Removal of Rules

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

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

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

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

innermost

We have the following set of usable rules:

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

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

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

a(b(x)) -> b(a(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

↳ATrans

→DP Problem 2

↳MRR

...

→DP Problem 5

↳Negative Polynomial Order

**C(a( x)) -> A(c(x))**

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

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

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

innermost

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

C(a(x)) -> A(c(x))

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

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

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

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

Used ordering:

Polynomial Order with Interpretation:

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

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

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

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

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

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

This results in one new DP problem.

R

↳DPs

→DP Problem 1

↳ATrans

→DP Problem 2

↳MRR

...

→DP Problem 6

↳Dependency Graph

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

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

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

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

innermost

Using the Dependency Graph resulted in no new DP problems.

Duration:

0:00 minutes