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

Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

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

Furthermore, R contains one SCC. 


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


Dependency Pairs:

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


Rules:


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





We have the following set of usable rules:

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

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

A(a(f(x, y))) -> A(y)
A(a(f(x, y))) -> A(x)

No Rules can be deleted.

The result of this processor delivers one new DP problem.



   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 2
             ↳Narrowing Transformation


Dependency Pairs:

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


Rules:


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





On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

F(a(x), a(y)) -> A(f(x, y))
two new Dependency Pairs are created:

F(a(a(x'')), a(a(y''))) -> A(a(f(x'', y'')))
F(a(b(x'')), a(b(y''))) -> A(b(f(x'', y'')))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 3
                 ↳Semantic Labelling


Dependency Pairs:

A(a(f(x, y))) -> F(a(b(a(b(a(x))))), a(b(a(b(a(y))))))
F(a(a(x'')), a(a(y''))) -> A(a(f(x'', y'')))
F(a(x), a(y)) -> F(x, y)
F(b(x), b(y)) -> F(x, y)


Rules:


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





Using Semantic Labelling, the DP problem could be transformed. The following model was found:
a(x0)=  0
f(x0, x1)=  x1
b(x0)=  1 + x0
F(x0, x1)=  0
A(x0)=  x0

From the dependency graph we obtain 2 (labeled) SCCs which each result in correspondingDP problem.


   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 4
                 ↳Modular Removal of Rules


Dependency Pairs:

F00(b1(x), b1(y)) -> F11(x, y)
F00(a0(x), a0(y)) -> F00(x, y)
F00(a0(a1(x'')), a0(a1(y''))) -> A0(a1(f11(x'', y'')))
F00(a0(a1(x'')), a0(a0(y''))) -> A0(a0(f10(x'', y'')))
F00(a0(a0(x'')), a0(a1(y''))) -> A0(a1(f01(x'', y'')))
A0(a1(f11(x, y))) -> F00(a1(b0(a1(b0(a1(x))))), a1(b0(a1(b0(a1(y))))))
A0(a0(f10(x, y))) -> F00(a1(b0(a1(b0(a1(x))))), a1(b0(a1(b0(a0(y))))))
A0(a1(f01(x, y))) -> F00(a1(b0(a1(b0(a0(x))))), a1(b0(a1(b0(a1(y))))))
F00(a0(a0(x'')), a0(a0(y''))) -> A0(a0(f00(x'', y'')))
F11(b0(x), b0(y)) -> F00(x, y)
F00(a1(x), a1(y)) -> F11(x, y)
A0(a0(f00(x, y))) -> F00(a1(b0(a1(b0(a0(x))))), a1(b0(a1(b0(a0(y))))))


Rules:


a0(a0(f00(x, y))) -> f00(a1(b0(a1(b0(a0(x))))), a1(b0(a1(b0(a0(y))))))
a0(a1(f01(x, y))) -> f00(a1(b0(a1(b0(a0(x))))), a1(b0(a1(b0(a1(y))))))
a0(a0(f10(x, y))) -> f00(a1(b0(a1(b0(a1(x))))), a1(b0(a1(b0(a0(y))))))
a0(a1(f11(x, y))) -> f00(a1(b0(a1(b0(a1(x))))), a1(b0(a1(b0(a1(y))))))
f00(a0(x), a0(y)) -> a0(f00(x, y))
f00(a0(x), a1(y)) -> a1(f01(x, y))
f00(a1(x), a0(y)) -> a0(f10(x, y))
f00(a1(x), a1(y)) -> a1(f11(x, y))
f00(b1(x), b1(y)) -> b1(f11(x, y))
f01(b1(x), b0(y)) -> b0(f10(x, y))
f10(b0(x), b1(y)) -> b1(f01(x, y))
f11(b0(x), b0(y)) -> b0(f00(x, y))





We have the following set of usable rules:

a0(a0(f00(x, y))) -> f00(a1(b0(a1(b0(a0(x))))), a1(b0(a1(b0(a0(y))))))
a0(a1(f01(x, y))) -> f00(a1(b0(a1(b0(a0(x))))), a1(b0(a1(b0(a1(y))))))
a0(a0(f10(x, y))) -> f00(a1(b0(a1(b0(a1(x))))), a1(b0(a1(b0(a0(y))))))
a0(a1(f11(x, y))) -> f00(a1(b0(a1(b0(a1(x))))), a1(b0(a1(b0(a1(y))))))
f11(b0(x), b0(y)) -> b0(f00(x, y))
f10(b0(x), b1(y)) -> b1(f01(x, y))
f00(a1(x), a1(y)) -> a1(f11(x, y))
f01(b1(x), b0(y)) -> b0(f10(x, y))
f00(a0(x), a0(y)) -> a0(f00(x, y))
f00(a0(x), a1(y)) -> a1(f01(x, y))
f00(a1(x), a0(y)) -> a0(f10(x, y))
f00(b1(x), b1(y)) -> b1(f11(x, y))
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(A_0(x1))=  x1  
  POL(f_11(x1, x2))=  x1 + x2  
  POL(F_00(x1, x2))=  x1 + x2  
  POL(a_1(x1))=  x1  
  POL(f_00(x1, x2))=  x1 + x2  
  POL(b_0(x1))=  x1  
  POL(a_0(x1))=  x1  
  POL(F_11(x1, x2))=  x1 + x2  
  POL(f_10(x1, x2))=  x1 + x2  
  POL(f_01(x1, x2))=  x1 + x2  
  POL(b_1(x1))=  1 + x1  

We have the following set D of usable symbols: {A0, f11, F00, a1, f00, b0, a0, F11, f10, f01, b1}
The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:

F00(b1(x), b1(y)) -> F11(x, y)

The following rules can be deleted as the lhs is strictly greater than the corresponding rhs:

f01(b1(x), b0(y)) -> b0(f10(x, y))
f00(b1(x), b1(y)) -> b1(f11(x, y))


The result of this processor delivers one new DP problem.



   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 6
                 ↳Modular Removal of Rules


Dependency Pairs:

F00(a0(a1(x'')), a0(a1(y''))) -> A0(a1(f11(x'', y'')))
A0(a1(f11(x, y))) -> F00(a1(b0(a1(b0(a1(x))))), a1(b0(a1(b0(a1(y))))))
A0(a0(f10(x, y))) -> F00(a1(b0(a1(b0(a1(x))))), a1(b0(a1(b0(a0(y))))))
F00(a0(a1(x'')), a0(a0(y''))) -> A0(a0(f10(x'', y'')))
A0(a1(f01(x, y))) -> F00(a1(b0(a1(b0(a0(x))))), a1(b0(a1(b0(a1(y))))))
F00(a0(a0(x'')), a0(a1(y''))) -> A0(a1(f01(x'', y'')))
F11(b0(x), b0(y)) -> F00(x, y)
F00(a1(x), a1(y)) -> F11(x, y)
A0(a0(f00(x, y))) -> F00(a1(b0(a1(b0(a0(x))))), a1(b0(a1(b0(a0(y))))))
F00(a0(a0(x'')), a0(a0(y''))) -> A0(a0(f00(x'', y'')))
F00(a0(x), a0(y)) -> F00(x, y)


Rules:


a0(a0(f00(x, y))) -> f00(a1(b0(a1(b0(a0(x))))), a1(b0(a1(b0(a0(y))))))
a0(a1(f01(x, y))) -> f00(a1(b0(a1(b0(a0(x))))), a1(b0(a1(b0(a1(y))))))
a0(a0(f10(x, y))) -> f00(a1(b0(a1(b0(a1(x))))), a1(b0(a1(b0(a0(y))))))
a0(a1(f11(x, y))) -> f00(a1(b0(a1(b0(a1(x))))), a1(b0(a1(b0(a1(y))))))
f00(a1(x), a1(y)) -> a1(f11(x, y))
f00(a0(x), a0(y)) -> a0(f00(x, y))
f00(a0(x), a1(y)) -> a1(f01(x, y))
f00(a1(x), a0(y)) -> a0(f10(x, y))
f10(b0(x), b1(y)) -> b1(f01(x, y))
f11(b0(x), b0(y)) -> b0(f00(x, y))





We have the following set of usable rules:

a0(a0(f00(x, y))) -> f00(a1(b0(a1(b0(a0(x))))), a1(b0(a1(b0(a0(y))))))
a0(a1(f01(x, y))) -> f00(a1(b0(a1(b0(a0(x))))), a1(b0(a1(b0(a1(y))))))
a0(a0(f10(x, y))) -> f00(a1(b0(a1(b0(a1(x))))), a1(b0(a1(b0(a0(y))))))
a0(a1(f11(x, y))) -> f00(a1(b0(a1(b0(a1(x))))), a1(b0(a1(b0(a1(y))))))
f11(b0(x), b0(y)) -> b0(f00(x, y))
f10(b0(x), b1(y)) -> b1(f01(x, y))
f00(a1(x), a1(y)) -> a1(f11(x, y))
f00(a0(x), a0(y)) -> a0(f00(x, y))
f00(a0(x), a1(y)) -> a1(f01(x, y))
f00(a1(x), a0(y)) -> a0(f10(x, y))
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(A_0(x1))=  1 + x1  
  POL(f_11(x1, x2))=  x1 + x2  
  POL(F_00(x1, x2))=  x1 + x2  
  POL(a_1(x1))=  x1  
  POL(f_00(x1, x2))=  x1 + x2  
  POL(b_0(x1))=  x1  
  POL(a_0(x1))=  1 + x1  
  POL(f_10(x1, x2))=  x1 + x2  
  POL(F_11(x1, x2))=  x1 + x2  
  POL(f_01(x1, x2))=  x1 + x2  
  POL(b_1(x1))=  x1  

We have the following set D of usable symbols: {A0, f11, F00, a1, f00, b0, a0, F11, f10, f01, b1}
The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:

F00(a0(a1(x'')), a0(a1(y''))) -> A0(a1(f11(x'', y'')))
A0(a1(f11(x, y))) -> F00(a1(b0(a1(b0(a1(x))))), a1(b0(a1(b0(a1(y))))))
A0(a0(f10(x, y))) -> F00(a1(b0(a1(b0(a1(x))))), a1(b0(a1(b0(a0(y))))))
F00(a0(a1(x'')), a0(a0(y''))) -> A0(a0(f10(x'', y'')))
F00(a0(a0(x'')), a0(a1(y''))) -> A0(a1(f01(x'', y'')))
F00(a0(a0(x'')), a0(a0(y''))) -> A0(a0(f00(x'', y'')))
F00(a0(x), a0(y)) -> F00(x, y)

The following rules can be deleted as the lhs is strictly greater than the corresponding rhs:

a0(a0(f10(x, y))) -> f00(a1(b0(a1(b0(a1(x))))), a1(b0(a1(b0(a0(y))))))
a0(a1(f11(x, y))) -> f00(a1(b0(a1(b0(a1(x))))), a1(b0(a1(b0(a1(y))))))
f00(a0(x), a0(y)) -> a0(f00(x, y))
f00(a0(x), a1(y)) -> a1(f01(x, y))


The result of this processor delivers one new DP problem.



   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 7
                 ↳Modular Removal of Rules


Dependency Pairs:

F11(b0(x), b0(y)) -> F00(x, y)
F00(a1(x), a1(y)) -> F11(x, y)


Rules:


a0(a0(f00(x, y))) -> f00(a1(b0(a1(b0(a0(x))))), a1(b0(a1(b0(a0(y))))))
a0(a1(f01(x, y))) -> f00(a1(b0(a1(b0(a0(x))))), a1(b0(a1(b0(a1(y))))))
f00(a1(x), a1(y)) -> a1(f11(x, y))
f00(a1(x), a0(y)) -> a0(f10(x, y))
f11(b0(x), b0(y)) -> b0(f00(x, y))
f10(b0(x), b1(y)) -> b1(f01(x, 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(F_00(x1, x2))=  x1 + x2  
  POL(a_1(x1))=  x1  
  POL(b_0(x1))=  x1  
  POL(F_11(x1, x2))=  x1 + x2  

We have the following set D of usable symbols: {F00, F11}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:

F11(b0(x), b0(y)) -> F00(x, y)
F00(a1(x), a1(y)) -> F11(x, y)

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. 



   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 5
                 ↳Modular Removal of Rules


Dependency Pairs:

F10(b0(x), b1(y)) -> F01(x, y)
F01(b1(x), b0(y)) -> F10(x, y)


Rules:


a0(a0(f00(x, y))) -> f00(a1(b0(a1(b0(a0(x))))), a1(b0(a1(b0(a0(y))))))
a0(a1(f01(x, y))) -> f00(a1(b0(a1(b0(a0(x))))), a1(b0(a1(b0(a1(y))))))
a0(a0(f10(x, y))) -> f00(a1(b0(a1(b0(a1(x))))), a1(b0(a1(b0(a0(y))))))
a0(a1(f11(x, y))) -> f00(a1(b0(a1(b0(a1(x))))), a1(b0(a1(b0(a1(y))))))
f00(a0(x), a0(y)) -> a0(f00(x, y))
f00(a0(x), a1(y)) -> a1(f01(x, y))
f00(a1(x), a0(y)) -> a0(f10(x, y))
f00(a1(x), a1(y)) -> a1(f11(x, y))
f00(b1(x), b1(y)) -> b1(f11(x, y))
f01(b1(x), b0(y)) -> b0(f10(x, y))
f10(b0(x), b1(y)) -> b1(f01(x, y))
f11(b0(x), b0(y)) -> b0(f00(x, 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_0(x1))=  x1  
  POL(F_01(x1, x2))=  x1 + x2  
  POL(F_10(x1, x2))=  x1 + x2  
  POL(b_1(x1))=  x1  

We have the following set D of usable symbols: {F01, F10}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:

F10(b0(x), b1(y)) -> F01(x, y)
F01(b1(x), b0(y)) -> F10(x, y)

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.


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