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

Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

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

Furthermore, R contains one SCC. 


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


Dependency Pairs:

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


Rules:


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





We have the following set of usable rules:

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

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

F(f(b, a), x) -> F(b, x)
F(x, f(y, z)) -> F(x, y)
F(f(a, b), x) -> F(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
             ↳Semantic Labelling


Dependency Pairs:

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


Rules:


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





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

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


   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 2
             ↳SemLab
             ...
               →DP Problem 3
                 ↳Modular Removal of Rules


Dependency Pairs:

F11(x, f11(y, z)) -> F11(f11(x, y), z)
F11(f10(b, a), x) -> F11(b, f11(b, x))
F10(x, f01(y, z)) -> F11(f10(x, y), z)
F10(x, f00(y, z)) -> F10(f10(x, y), z)
F11(x, f10(y, z)) -> F10(f11(x, y), z)
F10(f10(b, a), x) -> F11(b, f10(b, x))


Rules:


f00(f01(a, b), x) -> f00(a, f00(a, x))
f00(x, f00(y, z)) -> f00(f00(x, y), z)
f00(x, f01(y, z)) -> f01(f00(x, y), z)
f01(f01(a, b), x) -> f00(a, f01(a, x))
f01(x, f10(y, z)) -> f00(f01(x, y), z)
f01(x, f11(y, z)) -> f01(f01(x, y), z)
f10(f10(b, a), x) -> f11(b, f10(b, x))
f10(x, f00(y, z)) -> f10(f10(x, y), z)
f10(x, f01(y, z)) -> f11(f10(x, y), z)
f11(f10(b, a), x) -> f11(b, f11(b, x))
f11(x, f10(y, z)) -> f10(f11(x, y), z)
f11(x, f11(y, z)) -> f11(f11(x, y), z)





We have the following set of usable rules:

f11(f10(b, a), x) -> f11(b, f11(b, x))
f11(x, f10(y, z)) -> f10(f11(x, y), z)
f11(x, f11(y, z)) -> f11(f11(x, y), z)
f10(f10(b, a), x) -> f11(b, f10(b, x))
f10(x, f00(y, z)) -> f10(f10(x, y), z)
f10(x, f01(y, z)) -> f11(f10(x, y), z)
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(f_11(x1, x2))=  x1 + x2  
  POL(f_00(x1, x2))=  x1 + x2  
  POL(b)=  0  
  POL(F_11(x1, x2))=  x1 + x2  
  POL(f_10(x1, x2))=  x1 + x2  
  POL(f_01(x1, x2))=  x1 + x2  
  POL(a)=  0  
  POL(F_10(x1, x2))=  x1 + x2  

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

F11(f10(b, a), x) -> F11(b, f11(b, x))
F10(x, f01(y, z)) -> F11(f10(x, y), z)
F10(x, f00(y, z)) -> F10(f10(x, y), z)
F10(f10(b, a), x) -> F11(b, f10(b, x))

The following rules can be deleted as they contain symbols in their lhs which do not occur in D:

f11(f10(b, a), x) -> f11(b, f11(b, x))
f10(f10(b, a), x) -> f11(b, f10(b, x))
f10(x, f00(y, z)) -> f10(f10(x, y), z)
f10(x, f01(y, z)) -> f11(f10(x, y), z)
6 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
             ↳SemLab
             ...
               →DP Problem 5
                 ↳Unlabel


Dependency Pair:

F11(x, f11(y, z)) -> F11(f11(x, y), z)


Rules:


f11(x, f10(y, z)) -> f10(f11(x, y), z)
f11(x, f11(y, z)) -> f11(f11(x, y), z)





Removed all semantic labels.

   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 2
             ↳SemLab
             ...
               →DP Problem 6
                 ↳Size-Change Principle


Dependency Pair:

F(x, f(y, z)) -> F(f(x, y), z)


Rule:


f(x, f(y, z)) -> f(f(x, y), z)





We number the DPs as follows:
  1. F(x, f(y, z)) -> F(f(x, y), z)
and get the following Size-Change Graph(s):
{1} , {1}
2>2

which lead(s) to this/these maximal multigraph(s):
{1} , {1}
2>2

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial


We obtain no new DP problems. 


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


Dependency Pairs:

F01(f01(a, b), x) -> F00(a, f01(a, x))
F01(x, f11(y, z)) -> F01(f01(x, y), z)
F00(f01(a, b), x) -> F00(a, f00(a, x))
F01(x, f10(y, z)) -> F00(f01(x, y), z)
F00(x, f01(y, z)) -> F01(f00(x, y), z)
F00(x, f00(y, z)) -> F00(f00(x, y), z)


Rules:


f00(f01(a, b), x) -> f00(a, f00(a, x))
f00(x, f00(y, z)) -> f00(f00(x, y), z)
f00(x, f01(y, z)) -> f01(f00(x, y), z)
f01(f01(a, b), x) -> f00(a, f01(a, x))
f01(x, f10(y, z)) -> f00(f01(x, y), z)
f01(x, f11(y, z)) -> f01(f01(x, y), z)
f10(f10(b, a), x) -> f11(b, f10(b, x))
f10(x, f00(y, z)) -> f10(f10(x, y), z)
f10(x, f01(y, z)) -> f11(f10(x, y), z)
f11(f10(b, a), x) -> f11(b, f11(b, x))
f11(x, f10(y, z)) -> f10(f11(x, y), z)
f11(x, f11(y, z)) -> f11(f11(x, y), z)





We have the following set of usable rules:

f01(x, f10(y, z)) -> f00(f01(x, y), z)
f01(x, f11(y, z)) -> f01(f01(x, y), z)
f01(f01(a, b), x) -> f00(a, f01(a, x))
f00(x, f00(y, z)) -> f00(f00(x, y), z)
f00(x, f01(y, z)) -> f01(f00(x, y), z)
f00(f01(a, b), x) -> f00(a, f00(a, x))
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(f_11(x1, x2))=  x1 + x2  
  POL(F_00(x1, x2))=  x1 + x2  
  POL(f_00(x1, x2))=  x1 + x2  
  POL(b)=  0  
  POL(f_10(x1, x2))=  x1 + x2  
  POL(F_01(x1, x2))=  x1 + x2  
  POL(f_01(x1, x2))=  x1 + x2  
  POL(a)=  0  

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

F01(f01(a, b), x) -> F00(a, f01(a, x))
F01(x, f11(y, z)) -> F01(f01(x, y), z)
F00(f01(a, b), x) -> F00(a, f00(a, x))
F01(x, f10(y, z)) -> F00(f01(x, y), z)

The following rules can be deleted as they contain symbols in their lhs which do not occur in D:

f01(x, f10(y, z)) -> f00(f01(x, y), z)
f01(x, f11(y, z)) -> f01(f01(x, y), z)
f01(f01(a, b), x) -> f00(a, f01(a, x))
f00(f01(a, b), x) -> f00(a, f00(a, x))
6 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
             ↳SemLab
             ...
               →DP Problem 7
                 ↳Unlabel


Dependency Pair:

F00(x, f00(y, z)) -> F00(f00(x, y), z)


Rules:


f00(x, f00(y, z)) -> f00(f00(x, y), z)
f00(x, f01(y, z)) -> f01(f00(x, y), z)





Removed all semantic labels.

   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 2
             ↳SemLab
             ...
               →DP Problem 8
                 ↳Reference


Dependency Pair:

F(x, f(y, z)) -> F(f(x, y), z)


Rule:


f(x, f(y, z)) -> f(f(x, y), z)





DP Problem 8 is equal to DP Problem 6 and thus proved successfully.
Termination of R successfully shown.
Duration:
0:07 minutes