Term Rewriting System R:
[x, 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 Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

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 contains one SCC. 


   R
     ↳DPs
       →DP Problem 1
         ↳Usable Rules (Innermost)


Dependency Pairs:

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


Rules:


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


Strategy:

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


Dependency Pairs:

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


Rule:

none


Strategy:

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:

a(a(b(b(x)))) -> b(b(b(a(a(a(x))))))
There is only one SCC in the graph and, thus, we obtain one new DP problem.


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
           →DP Problem 2
             ↳SRS
             ...
               →DP Problem 3
                 ↳Non-Overlappingness Check


Dependency Pairs:

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


Rule:


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


Dependency Pairs:

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


Rule:


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


Strategy:

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:



Innermost Termination of R successfully shown.
Duration:
0:00 minutes