f(

f(a(

f(b(

R

↳Dependency Pair Analysis

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

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

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

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

f(b(x),y) -> f(x, b(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(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: {b, a, F}

No Dependency Pairs can be deleted.

3 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.

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

R

↳DPs

→DP Problem 1

↳MRR

→DP Problem 2

↳NOC

...

→DP Problem 4

↳Non-Overlappingness Check

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

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

R

↳DPs

→DP Problem 1

↳MRR

→DP Problem 2

↳NOC

...

→DP Problem 5

↳Modular Removal of Rules

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

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

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

Polynomial interpretation:

_{ }^{ }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: {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)

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

No Rules can be deleted.

After the removal, there are no SCCs in the dependency graph which results in no DP problems which have to be solved.

**Termination** of *R* successfully shown.

Duration:

0:00 minutes