Termination Proof using AProVE

Term Rewriting System R:
[x, y]
h(x, y) -> f(x, y, x)
f(0, 1, x) -> h(x, x)
g(x, y) -> x
g(x, y) -> y

Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

H(x, y) -> F(x, y, x)
F(0, 1, x) -> H(x, x)

Furthermore, R contains one SCC.

     ↳DPs

       →DP Problem 1

         ↳Non Termination

Dependency Pairs:

F(0, 1, x) -> H(x, x)
H(x, y) -> F(x, y, x)

Rules:

h(x, y) -> f(x, y, x)
f(0, 1, x) -> h(x, x)
g(x, y) -> x
g(x, y) -> y

Found an infinite P-chain over R:
P =

F(0, 1, x) -> H(x, x)
H(x, y) -> F(x, y, x)

R =

h(x, y) -> f(x, y, x)
f(0, 1, x) -> h(x, x)
g(x, y) -> x
g(x, y) -> y

s = H(g(1, 0), g(1, 0))
evaluates to t =H(g(1, 0), g(1, 0))

Thus, s starts an infinite chain.

Non-Termination of R could be shown.
Duration:
0:00 minutes