f(

f(a(

f(b(

R

↳Dependency Pair Analysis

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

R

↳DPs

→DP Problem 1

↳MRR

→DP Problem 2

↳NOC

...

→DP Problem 4

↳Non-Overlappingness Check

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

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

↳RFC Match Bounds

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

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

innermost

Using RFC Match Bounds, the DP problem could be solved. The Match Bound was 4.

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74

Node 38 is start node and node 39 is final node.

Those nodes are connect through the following edges:

- 39 to 39 labelled #(0)
- 38 to 39 labelled A(0)
- 38 to 40 labelled A(0)
- 40 to 39 labelled a(0)
- 38 to 41 labelled A(0)
- 41 to 42 labelled a(0)
- 42 to 39 labelled a(0)
- 42 to 43 labelled b(1)
- 43 to 44 labelled b(1)
- 44 to 45 labelled b(1)
- 45 to 46 labelled a(1)
- 46 to 47 labelled a(1)
- 47 to 39 labelled a(1)
- 38 to 46 labelled A(1)
- 38 to 47 labelled A(1)
- 38 to 39 labelled A(1)
- 40 to 43 labelled b(1)
- 41 to 43 labelled b(1)
- 47 to 43 labelled b(1)
- 46 to 43 labelled b(1)
- 38 to 44 labelled A(1)
- 47 to 44 labelled a(1)
- 38 to 44 labelled A(2)
- 38 to 48 labelled A(2)
- 48 to 49 labelled a(2)
- 49 to 44 labelled a(2)
- 38 to 49 labelled A(2)
- 45 to 50 labelled b(2)
- 50 to 51 labelled b(2)
- 51 to 52 labelled b(2)
- 52 to 53 labelled a(2)
- 53 to 54 labelled a(2)
- 54 to 44 labelled a(2)
- 38 to 50 labelled A(2)
- 49 to 50 labelled a(2)
- 46 to 55 labelled b(2)
- 55 to 56 labelled b(2)
- 56 to 57 labelled b(2)
- 57 to 58 labelled a(2)
- 58 to 59 labelled a(2)
- 59 to 50 labelled a(2)
- 48 to 55 labelled b(2)
- 53 to 55 labelled b(2)
- 58 to 60 labelled b(3)
- 60 to 61 labelled b(3)
- 61 to 62 labelled b(3)
- 62 to 63 labelled a(3)
- 63 to 64 labelled a(3)
- 64 to 52 labelled a(3)
- 48 to 60 labelled b(3)
- 38 to 52 labelled A(3)
- 38 to 63 labelled A(3)
- 38 to 64 labelled A(3)
- 64 to 65 labelled b(3)
- 65 to 66 labelled b(3)
- 66 to 67 labelled b(3)
- 67 to 68 labelled a(3)
- 68 to 69 labelled a(3)
- 69 to 56 labelled a(3)
- 38 to 56 labelled A(3)
- 38 to 68 labelled A(3)
- 38 to 69 labelled A(3)
- 62 to 70 labelled b(4)
- 70 to 71 labelled b(4)
- 71 to 72 labelled b(4)
- 72 to 73 labelled a(4)
- 73 to 74 labelled a(4)
- 74 to 66 labelled a(4)
- 38 to 66 labelled A(4)
- 38 to 73 labelled A(4)
- 38 to 74 labelled A(4)

Duration:

0:00 minutes