Term Rewriting System R:
f(a, x) -> g(a, x)
f(a, x) -> f(b, x)
g(a, x) -> f(b, x)

Termination of R to be shown.

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.

Termination of R successfully shown.
0:00 minutes