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

Innermost Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

F(a, f(a, x)) -> F(c, f(b, x))
F(a, f(a, x)) -> F(b, x)
F(b, f(b, x)) -> F(a, f(c, x))
F(b, f(b, x)) -> F(c, x)
F(c, f(c, x)) -> F(b, f(a, x))
F(c, f(c, x)) -> F(a, x)

Furthermore, R contains one SCC. 


   R
     ↳DPs
       →DP Problem 1
         ↳A-Transformation


Dependency Pairs:

F(c, f(c, x)) -> F(a, x)
F(b, f(b, x)) -> F(c, x)
F(a, f(a, x)) -> F(b, x)
F(b, f(b, x)) -> F(a, f(c, x))
F(c, f(c, x)) -> F(b, f(a, x))
F(a, f(a, x)) -> F(c, f(b, x))


Rules:


f(a, f(a, x)) -> f(c, f(b, x))
f(b, f(b, x)) -> f(a, f(c, x))
f(c, f(c, x)) -> f(b, f(a, x))


Strategy:

innermost




We have an applicative DP problem with proper arity. Thus we can use the A-Transformation to obtain one new DP problem which consists of the A-transformed TRSs.


   R
     ↳DPs
       →DP Problem 1
         ↳ATrans
           →DP Problem 2
             ↳Modular Removal of Rules


Dependency Pairs:

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


Rules:


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


Strategy:

innermost




We have the following set of usable rules:

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

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

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

No Rules can be deleted.

The result of this processor delivers one new DP problem.



   R
     ↳DPs
       →DP Problem 1
         ↳ATrans
           →DP Problem 2
             ↳MRR
             ...
               →DP Problem 3
                 ↳RFC Match Bounds


Dependency Pairs:

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


Rules:


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


Strategy:

innermost




Using RFC Match Bounds, the DP problem could be solved. The Match Bound was 1.
The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

33, 34, 35, 36, 37, 38, 39, 40

Node 33 is start node and node 34 is final node.

Those nodes are connect through the following edges:



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