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

Innermost 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

         ↳Instantiation Transformation

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

Strategy:

innermost

On this DP problem, an Instantiation SCC transformation can be performed.
As a result of transforming the rule

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

one new Dependency Pair is created:

H(y', y') -> F(y', y', y')

The transformation is resulting in no new DP problems.

Innermost Termination of R successfully shown.
Duration:
0:00 minutes