**Term Rewriting System** *R*:

**[***x*]

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

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

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

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

R

↳**Dependency Pair Analysis**

*R* contains the following *Dependency Pairs:
*

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

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

G(a, *x*) -> F(b, *x*)

*R* contains **no** SCCs.

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

Duration:

0:00 minutes