Termination Proof using AProVE

Term Rewriting System R:
[X, Y]
f(s(X)) -> f(X)
g(cons(0, Y)) -> g(Y)
g(cons(s(X), Y)) -> s(X)
h(cons(X, Y)) -> h(g(cons(X, Y)))

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

F(s(X)) -> F(X)
G(cons(0, Y)) -> G(Y)
H(cons(X, Y)) -> H(g(cons(X, Y)))
H(cons(X, Y)) -> G(cons(X, Y))

Furthermore, R contains three SCCs.

     ↳DPs

       →DP Problem 1

         ↳Argument Filtering and Ordering

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Nar

Dependency Pair:

F(s(X)) -> F(X)

Rules:

f(s(X)) -> f(X)
g(cons(0, Y)) -> g(Y)
g(cons(s(X), Y)) -> s(X)
h(cons(X, Y)) -> h(g(cons(X, Y)))

Strategy:

innermost

The following dependency pair can be strictly oriented:

F(s(X)) -> F(X)

There are no usable rules for innermost that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:

F(x₁) -> F(x₁)
s(x₁) -> s(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

           →DP Problem 4

             ↳Dependency Graph

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Nar

Dependency Pair:

Rules:

f(s(X)) -> f(X)
g(cons(0, Y)) -> g(Y)
g(cons(s(X), Y)) -> s(X)
h(cons(X, Y)) -> h(g(cons(X, Y)))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳Argument Filtering and Ordering

       →DP Problem 3

         ↳Nar

Dependency Pair:

G(cons(0, Y)) -> G(Y)

Rules:

f(s(X)) -> f(X)
g(cons(0, Y)) -> g(Y)
g(cons(s(X), Y)) -> s(X)
h(cons(X, Y)) -> h(g(cons(X, Y)))

Strategy:

innermost

The following dependency pair can be strictly oriented:

G(cons(0, Y)) -> G(Y)

There are no usable rules for innermost that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:

G(x₁) -> G(x₁)
cons(x₁, x₂) -> cons(x₁, x₂)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

           →DP Problem 5

             ↳Dependency Graph

       →DP Problem 3

         ↳Nar

Dependency Pair:

Rules:

f(s(X)) -> f(X)
g(cons(0, Y)) -> g(Y)
g(cons(s(X), Y)) -> s(X)
h(cons(X, Y)) -> h(g(cons(X, Y)))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Narrowing Transformation

Dependency Pair:

H(cons(X, Y)) -> H(g(cons(X, Y)))

Rules:

f(s(X)) -> f(X)
g(cons(0, Y)) -> g(Y)
g(cons(s(X), Y)) -> s(X)
h(cons(X, Y)) -> h(g(cons(X, Y)))

Strategy:

innermost

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

H(cons(X, Y)) -> H(g(cons(X, Y)))

two new Dependency Pairs are created:

H(cons(0, Y'')) -> H(g(Y''))
H(cons(s(X''), Y'')) -> H(s(X''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Nar

           →DP Problem 6

             ↳Argument Filtering and Ordering

Dependency Pair:

H(cons(0, Y'')) -> H(g(Y''))

Rules:

f(s(X)) -> f(X)
g(cons(0, Y)) -> g(Y)
g(cons(s(X), Y)) -> s(X)
h(cons(X, Y)) -> h(g(cons(X, Y)))

Strategy:

innermost

The following dependency pair can be strictly oriented:

H(cons(0, Y'')) -> H(g(Y''))

The following usable rules for innermost can be oriented:

g(cons(0, Y)) -> g(Y)
g(cons(s(X), Y)) -> s(X)

Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:

H(x₁) -> H(x₁)
cons(x₁, x₂) -> cons(x₁, x₂)
g(x₁) -> x₁
s(x₁) -> s(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Nar

           →DP Problem 6

             ↳AFS

...

               →DP Problem 7

                 ↳Dependency Graph

Dependency Pair:

Rules:

f(s(X)) -> f(X)
g(cons(0, Y)) -> g(Y)
g(cons(s(X), Y)) -> s(X)
h(cons(X, Y)) -> h(g(cons(X, Y)))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

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