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

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
         ↳Modular Removal of Rules


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





We have the following set of usable rules: none
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(b(x1))=  x1  
  POL(a(x1))=  x1  
  POL(F(x1, x2))=  1 + x1 + x2  

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


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





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


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
         ↳MRR
           →DP Problem 2
             ↳NOC
             ...
               →DP Problem 4
                 ↳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
         ↳MRR
           →DP Problem 2
             ↳NOC
             ...
               →DP Problem 5
                 ↳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 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:



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