**Term Rewriting System** *R*:

**[***x*, *y*, *z*]

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

g(*x*, *y*) -> *x*

g(*x*, *y*) -> *y*

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

R

↳**Dependency Pair Analysis**

*R* contains the following *Dependency Pairs:
*

F(g(*x*, *y*), *x*, *z*) -> F(*z*, *z*, *z*)

*R* contains **no** SCCs.

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

Duration:

0:00 minutes