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)
Termination of R to be shown.
R
↳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)
Furthermore, R contains one SCC.
R
↳DPs
→DP Problem 1
↳Non Termination
Dependency Pair:
F(k(a), k(b), X) -> F(X, X, X)
Rules:
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)
Found an infinite P-chain over R:
P =
F(k(a), k(b), X) -> F(X, X, X)
R =
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)
s = F(u(d, h(d), X'''), u(d, h(d), X'''), u(d, h(d), X'''))
evaluates to t =F(u(d, h(d), X'''), u(d, h(d), X'''), u(d, h(d), X'''))
Thus, s starts an infinite chain.
Non-Termination of R could be shown.
Duration:
0:00 minutes