**Term Rewriting System** *R*:

**[***X*, *Y*, *Z*]

f(f(*X*, *Y*), *Z*) -> f(*X*, f(*Y*, *Z*))

f(*X*, f(*Y*, *Z*)) -> f(*Y*, *Y*)

**Innermost Termination** of *R* to be shown.

R

↳**Dependency Pair Analysis**

*R* contains the following *Dependency Pairs:
*

F(f(*X*, *Y*), *Z*) -> F(*X*, f(*Y*, *Z*))

F(f(*X*, *Y*), *Z*) -> F(*Y*, *Z*)

F(*X*, f(*Y*, *Z*)) -> F(*Y*, *Y*)

*R* contains **no** SCCs.

**Innermost Termination** of *R* successfully shown.

Duration:

0:00 minutes