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

↳Usable Rules (Innermost)

**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))

innermost

As we are in the innermost case, we can delete all 3 non-usable-rules.

R

↳DPs

→DP Problem 1

↳UsableRules

→DP Problem 2

↳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

↳UsableRules

→DP Problem 2

↳SRS

...

→DP Problem 3

↳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

↳UsableRules

→DP Problem 2

↳SRS

...

→DP Problem 4

↳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 8.

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

30, 31, 32, 33, 34, 35, 36, 37, 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, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100

Node 30 is start node and node 31 is final node.

Those nodes are connect through the following edges:

- 31 to 31 labelled #(0)
- 30 to 31 labelled A(0)
- 30 to 32 labelled A(0)
- 32 to 31 labelled a(0)
- 30 to 33 labelled A(0)
- 33 to 34 labelled a(0)
- 34 to 31 labelled a(0)
- 34 to 35 labelled b(1)
- 35 to 36 labelled b(1)
- 36 to 37 labelled b(1)
- 37 to 38 labelled a(1)
- 38 to 39 labelled a(1)
- 39 to 31 labelled a(1)
- 32 to 35 labelled b(1)
- 30 to 38 labelled A(1)
- 30 to 39 labelled A(1)
- 30 to 31 labelled A(1)
- 33 to 35 labelled b(1)
- 39 to 35 labelled b(1)
- 38 to 35 labelled b(1)
- 30 to 36 labelled A(1)
- 39 to 36 labelled a(1)
- 37 to 40 labelled b(2)
- 40 to 41 labelled b(2)
- 41 to 42 labelled b(2)
- 42 to 43 labelled a(2)
- 43 to 44 labelled a(2)
- 44 to 36 labelled a(2)
- 30 to 36 labelled A(2)
- 30 to 43 labelled A(2)
- 30 to 44 labelled A(2)
- 38 to 45 labelled b(2)
- 45 to 46 labelled b(2)
- 46 to 47 labelled b(2)
- 47 to 48 labelled a(2)
- 48 to 49 labelled a(2)
- 49 to 40 labelled a(2)
- 30 to 40 labelled A(2)
- 30 to 48 labelled A(2)
- 30 to 49 labelled A(2)
- 43 to 45 labelled b(2)
- 48 to 50 labelled b(3)
- 50 to 51 labelled b(3)
- 51 to 52 labelled b(3)
- 52 to 53 labelled a(3)
- 53 to 54 labelled a(3)
- 54 to 42 labelled a(3)
- 30 to 42 labelled A(3)
- 30 to 53 labelled A(3)
- 30 to 54 labelled A(3)
- 30 to 46 labelled A(3)
- 54 to 46 labelled a(3)
- 54 to 50 labelled b(3)
- 30 to 51 labelled A(4)
- 30 to 55 labelled A(4)
- 55 to 56 labelled a(4)
- 56 to 51 labelled a(4)
- 30 to 56 labelled A(4)
- 52 to 57 labelled b(4)
- 57 to 58 labelled b(4)
- 58 to 59 labelled b(4)
- 59 to 60 labelled a(4)
- 60 to 61 labelled a(4)
- 61 to 51 labelled a(4)
- 30 to 57 labelled A(4)
- 56 to 57 labelled a(4)
- 55 to 62 labelled b(4)
- 62 to 63 labelled b(4)
- 63 to 64 labelled b(4)
- 64 to 65 labelled a(4)
- 65 to 66 labelled a(4)
- 66 to 57 labelled a(4)
- 60 to 62 labelled b(4)
- 65 to 67 labelled b(5)
- 67 to 68 labelled b(5)
- 68 to 69 labelled b(5)
- 69 to 70 labelled a(5)
- 70 to 71 labelled a(5)
- 71 to 59 labelled a(5)
- 30 to 59 labelled A(5)
- 30 to 70 labelled A(5)
- 30 to 71 labelled A(5)
- 55 to 67 labelled b(5)
- 30 to 63 labelled A(5)
- 71 to 63 labelled a(5)
- 71 to 67 labelled b(5)
- 30 to 68 labelled A(6)
- 30 to 72 labelled A(6)
- 72 to 73 labelled a(6)
- 73 to 68 labelled a(6)
- 30 to 73 labelled A(6)
- 69 to 74 labelled b(6)
- 74 to 75 labelled b(6)
- 75 to 76 labelled b(6)
- 76 to 77 labelled a(6)
- 77 to 78 labelled a(6)
- 78 to 68 labelled a(6)
- 77 to 79 labelled b(6)
- 79 to 80 labelled b(6)
- 80 to 81 labelled b(6)
- 81 to 82 labelled a(6)
- 82 to 83 labelled a(6)
- 83 to 74 labelled a(6)
- 72 to 79 labelled b(6)
- 30 to 74 labelled A(6)
- 30 to 82 labelled A(6)
- 30 to 83 labelled A(6)
- 30 to 76 labelled A(7)
- 30 to 84 labelled A(7)
- 84 to 85 labelled a(7)
- 85 to 76 labelled a(7)
- 30 to 85 labelled A(7)
- 82 to 86 labelled b(7)
- 86 to 87 labelled b(7)
- 87 to 88 labelled b(7)
- 88 to 89 labelled a(7)
- 89 to 90 labelled a(7)
- 90 to 76 labelled a(7)
- 85 to 91 labelled b(7)
- 91 to 92 labelled b(7)
- 92 to 93 labelled b(7)
- 93 to 94 labelled a(7)
- 94 to 95 labelled a(7)
- 95 to 80 labelled a(7)
- 90 to 91 labelled b(7)
- 30 to 80 labelled A(7)
- 30 to 94 labelled A(7)
- 30 to 95 labelled A(7)
- 88 to 96 labelled b(8)
- 96 to 97 labelled b(8)
- 97 to 98 labelled b(8)
- 98 to 99 labelled a(8)
- 99 to 100 labelled a(8)
- 100 to 92 labelled a(8)
- 30 to 92 labelled A(8)
- 30 to 99 labelled A(8)
- 30 to 100 labelled A(8)

Duration:

0:00 minutes