**Term Rewriting System** *R*:

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

f(g(h(*x*, *y*)), f(a, a)) -> f(h(*x*, *x*), g(f(*y*, a)))

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

R

↳**Dependency Pair Analysis**

*R* contains the following *Dependency Pairs:
*

F(g(h(*x*, *y*)), f(a, a)) -> F(h(*x*, *x*), g(f(*y*, a)))

F(g(h(*x*, *y*)), f(a, a)) -> F(*y*, a)

*R* contains **no** SCCs.

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

Duration:

0:00 minutes