**Term Rewriting System** *R*:

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

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

g(a) -> h(a, b, a)

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

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

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

R

↳**Dependency Pair Analysis**

*R* contains the following *Dependency Pairs:
*

G(a) -> H(a, b, a)

I(*x*) -> F(*x*, *x*)

H(*x*, *x*, *y*) -> G(*x*)

*R* contains **no** SCCs.

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

Duration:

0:00 minutes