Term Rewriting System R:
[X, Y]
g(X) -> u(h(X), h(X), X)
u(d, c(Y), X) -> k(Y)
h(d) -> c(a)
h(d) -> c(b)
f(k(a), k(b), X) -> f(X, X, X)

Innermost Termination of R to be shown.

Dependency Pair Analysis

R contains the following Dependency Pairs:

G(X) -> U(h(X), h(X), X)
G(X) -> H(X)
F(k(a), k(b), X) -> F(X, X, X)

R contains no SCCs.

Innermost Termination of R successfully shown.
0:00 minutes