Termination Proof using AProVE

Term Rewriting System R:
[a, x, k, d]
f(a, empty) -> g(a, empty)
f(a, cons(x, k)) -> f(cons(x, a), k)
g(empty, d) -> d
g(cons(x, k), d) -> g(k, cons(x, d))

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

F(a, empty) -> G(a, empty)
F(a, cons(x, k)) -> F(cons(x, a), k)
G(cons(x, k), d) -> G(k, cons(x, d))

Furthermore, R contains two SCCs.

     ↳DPs

       →DP Problem 1

         ↳Instantiation Transformation

       →DP Problem 2

         ↳Inst

Dependency Pair:

G(cons(x, k), d) -> G(k, cons(x, d))

Rules:

f(a, empty) -> g(a, empty)
f(a, cons(x, k)) -> f(cons(x, a), k)
g(empty, d) -> d
g(cons(x, k), d) -> g(k, cons(x, d))

Strategy:

innermost

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

G(cons(x, k), d) -> G(k, cons(x, d))

one new Dependency Pair is created:

G(cons(x0, k''), cons(x'', d'')) -> G(k'', cons(x0, cons(x'', d'')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

           →DP Problem 3

             ↳Instantiation Transformation

       →DP Problem 2

         ↳Inst

Dependency Pair:

G(cons(x0, k''), cons(x'', d'')) -> G(k'', cons(x0, cons(x'', d'')))

Rules:

f(a, empty) -> g(a, empty)
f(a, cons(x, k)) -> f(cons(x, a), k)
g(empty, d) -> d
g(cons(x, k), d) -> g(k, cons(x, d))

Strategy:

innermost

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

G(cons(x0, k''), cons(x'', d'')) -> G(k'', cons(x0, cons(x'', d'')))

one new Dependency Pair is created:

G(cons(x0'', k''''), cons(x'''', cons(x''''', d''''))) -> G(k'''', cons(x0'', cons(x'''', cons(x''''', d''''))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

           →DP Problem 3

             ↳Inst

...

               →DP Problem 4

                 ↳Argument Filtering and Ordering

       →DP Problem 2

         ↳Inst

Dependency Pair:

G(cons(x0'', k''''), cons(x'''', cons(x''''', d''''))) -> G(k'''', cons(x0'', cons(x'''', cons(x''''', d''''))))

Rules:

f(a, empty) -> g(a, empty)
f(a, cons(x, k)) -> f(cons(x, a), k)
g(empty, d) -> d
g(cons(x, k), d) -> g(k, cons(x, d))

Strategy:

innermost

The following dependency pair can be strictly oriented:

G(cons(x0'', k''''), cons(x'''', cons(x''''', d''''))) -> G(k'''', cons(x0'', cons(x'''', cons(x''''', d''''))))

There are no usable rules for innermost w.r.t. to the AFS that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(cons(x₁, x₂)) = 1 + x₁ + x₂

resulting in one new DP problem.
Used Argument Filtering System:

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

     ↳DPs

       →DP Problem 1

         ↳Inst

           →DP Problem 3

             ↳Inst

...

               →DP Problem 5

                 ↳Dependency Graph

       →DP Problem 2

         ↳Inst

Dependency Pair:

Rules:

f(a, empty) -> g(a, empty)
f(a, cons(x, k)) -> f(cons(x, a), k)
g(empty, d) -> d
g(cons(x, k), d) -> g(k, cons(x, d))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Instantiation Transformation

Dependency Pair:

F(a, cons(x, k)) -> F(cons(x, a), k)

Rules:

f(a, empty) -> g(a, empty)
f(a, cons(x, k)) -> f(cons(x, a), k)
g(empty, d) -> d
g(cons(x, k), d) -> g(k, cons(x, d))

Strategy:

innermost

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

F(a, cons(x, k)) -> F(cons(x, a), k)

one new Dependency Pair is created:

F(cons(x'', a''), cons(x0, k'')) -> F(cons(x0, cons(x'', a'')), k'')

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Inst

           →DP Problem 6

             ↳Instantiation Transformation

Dependency Pair:

F(cons(x'', a''), cons(x0, k'')) -> F(cons(x0, cons(x'', a'')), k'')

Rules:

f(a, empty) -> g(a, empty)
f(a, cons(x, k)) -> f(cons(x, a), k)
g(empty, d) -> d
g(cons(x, k), d) -> g(k, cons(x, d))

Strategy:

innermost

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

F(cons(x'', a''), cons(x0, k'')) -> F(cons(x0, cons(x'', a'')), k'')

one new Dependency Pair is created:

F(cons(x'''', cons(x''''', a'''')), cons(x0'', k'''')) -> F(cons(x0'', cons(x'''', cons(x''''', a''''))), k'''')

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Inst

           →DP Problem 6

             ↳Inst

...

               →DP Problem 7

                 ↳Argument Filtering and Ordering

Dependency Pair:

F(cons(x'''', cons(x''''', a'''')), cons(x0'', k'''')) -> F(cons(x0'', cons(x'''', cons(x''''', a''''))), k'''')

Rules:

f(a, empty) -> g(a, empty)
f(a, cons(x, k)) -> f(cons(x, a), k)
g(empty, d) -> d
g(cons(x, k), d) -> g(k, cons(x, d))

Strategy:

innermost

The following dependency pair can be strictly oriented:

F(cons(x'''', cons(x''''', a'''')), cons(x0'', k'''')) -> F(cons(x0'', cons(x'''', cons(x''''', a''''))), k'''')

There are no usable rules for innermost w.r.t. to the AFS that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(cons(x₁, x₂)) = 1 + x₁ + x₂

resulting in one new DP problem.
Used Argument Filtering System:

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

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Inst

           →DP Problem 6

             ↳Inst

...

               →DP Problem 8

                 ↳Dependency Graph

Dependency Pair:

Rules:

f(a, empty) -> g(a, empty)
f(a, cons(x, k)) -> f(cons(x, a), k)
g(empty, d) -> d
g(cons(x, k), d) -> g(k, cons(x, d))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

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