Term Rewriting System R:
[x]
a(a(x)) -> b(b(x))
b(b(a(x))) -> a(b(b(x)))

Innermost Termination of R to be shown. 



   TRS
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

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

Furthermore, R contains one SCC. 


   TRS
     ↳DPs
       →DP Problem 1
         ↳Modular Removal of Rules


Dependency Pairs:

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


Rules:


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


Strategy:

innermost




We have the following set of usable rules:

b(b(a(x))) -> a(b(b(x)))
a(a(x)) -> b(b(x))
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(b(x1))=  x1  
  POL(a(x1))=  1 + x1  
  POL(A(x1))=  x1  

We have the following set D of usable symbols: {B, b, a, A}
The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:

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


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