**Term Rewriting System** *R*:

**[***x*]

f(a, f(a, *x*)) -> f(a, f(f(a, a), f(a, *x*)))

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

R

↳**Dependency Pair Analysis**

*R* contains the following *Dependency Pairs:
*

F(a, f(a, *x*)) -> F(a, f(f(a, a), f(a, *x*)))

F(a, f(a, *x*)) -> F(f(a, a), f(a, *x*))

F(a, f(a, *x*)) -> F(a, a)

*R* contains **no** SCCs.

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

Duration:

0:00 minutes