Termination Proof using AProVE

Term Rewriting System R:
[x, y, z]
rev(nil) -> nil
rev(rev(x)) -> x
rev(++(x, y)) -> ++(rev(y), rev(x))
++(nil, y) -> y
++(x, nil) -> x
++(.(x, y), z) -> .(x, ++(y, z))
++(x, ++(y, z)) -> ++(++(x, y), z)
make(x) -> .(x, nil)

Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

REV(++(x, y)) -> ++'(rev(y), rev(x))
REV(++(x, y)) -> REV(y)
REV(++(x, y)) -> REV(x)
++'(.(x, y), z) -> ++'(y, z)
++'(x, ++(y, z)) -> ++'(++(x, y), z)
++'(x, ++(y, z)) -> ++'(x, y)

Furthermore, R contains two SCCs.

     ↳DPs

       →DP Problem 1

         ↳Argument Filtering and Ordering

       →DP Problem 2

         ↳AFS

Dependency Pairs:

++'(x, ++(y, z)) -> ++'(x, y)
++'(x, ++(y, z)) -> ++'(++(x, y), z)
++'(.(x, y), z) -> ++'(y, z)

Rules:

rev(nil) -> nil
rev(rev(x)) -> x
rev(++(x, y)) -> ++(rev(y), rev(x))
++(nil, y) -> y
++(x, nil) -> x
++(.(x, y), z) -> .(x, ++(y, z))
++(x, ++(y, z)) -> ++(++(x, y), z)
make(x) -> .(x, nil)

The following dependency pair can be strictly oriented:

++'(.(x, y), z) -> ++'(y, z)

The following rules can be oriented:

++(nil, y) -> y
++(x, nil) -> x
++(.(x, y), z) -> .(x, ++(y, z))
++(x, ++(y, z)) -> ++(++(x, y), z)
rev(nil) -> nil
rev(rev(x)) -> x
rev(++(x, y)) -> ++(rev(y), rev(x))
make(x) -> .(x, nil)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(make(x₁)) = 1 + x₁

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

POL(rev(x₁)) = x₁

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

POL(nil) = 0

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

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

++'(x₁, x₂) -> ++'(x₁, x₂)
.(x₁, x₂) -> .(x₁, x₂)
++(x₁, x₂) -> ++(x₁, x₂)
rev(x₁) -> rev(x₁)
make(x₁) -> make(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

           →DP Problem 3

             ↳Argument Filtering and Ordering

       →DP Problem 2

         ↳AFS

Dependency Pairs:

++'(x, ++(y, z)) -> ++'(x, y)
++'(x, ++(y, z)) -> ++'(++(x, y), z)

Rules:

rev(nil) -> nil
rev(rev(x)) -> x
rev(++(x, y)) -> ++(rev(y), rev(x))
++(nil, y) -> y
++(x, nil) -> x
++(.(x, y), z) -> .(x, ++(y, z))
++(x, ++(y, z)) -> ++(++(x, y), z)
make(x) -> .(x, nil)

The following dependency pair can be strictly oriented:

++'(x, ++(y, z)) -> ++'(x, y)

The following rules can be oriented:

++(nil, y) -> y
++(x, nil) -> x
++(.(x, y), z) -> .(x, ++(y, z))
++(x, ++(y, z)) -> ++(++(x, y), z)
rev(nil) -> nil
rev(rev(x)) -> x
rev(++(x, y)) -> ++(rev(y), rev(x))
make(x) -> .(x, nil)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(make(x₁)) = x₁

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

POL(rev(x₁)) = x₁

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

POL(nil) = 0

POL(.(x₁, x₂)) = x₁ + x₂

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

++'(x₁, x₂) -> ++'(x₁, x₂)
++(x₁, x₂) -> ++(x₁, x₂)
.(x₁, x₂) -> .(x₁, x₂)
rev(x₁) -> rev(x₁)
make(x₁) -> make(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

           →DP Problem 3

             ↳AFS

...

               →DP Problem 4

                 ↳Argument Filtering and Ordering

       →DP Problem 2

         ↳AFS

Dependency Pair:

++'(x, ++(y, z)) -> ++'(++(x, y), z)

Rules:

rev(nil) -> nil
rev(rev(x)) -> x
rev(++(x, y)) -> ++(rev(y), rev(x))
++(nil, y) -> y
++(x, nil) -> x
++(.(x, y), z) -> .(x, ++(y, z))
++(x, ++(y, z)) -> ++(++(x, y), z)
make(x) -> .(x, nil)

The following dependency pair can be strictly oriented:

++'(x, ++(y, z)) -> ++'(++(x, y), z)

The following rules can be oriented:

++(nil, y) -> y
++(x, nil) -> x
++(.(x, y), z) -> .(x, ++(y, z))
++(x, ++(y, z)) -> ++(++(x, y), z)
rev(nil) -> nil
rev(rev(x)) -> x
rev(++(x, y)) -> ++(rev(y), rev(x))
make(x) -> .(x, nil)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(make(x₁)) = x₁

POL(rev(x₁)) = x₁

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

POL(nil) = 0

POL(.(x₁, x₂)) = x₁ + x₂

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

++'(x₁, x₂) -> x₂
++(x₁, x₂) -> ++(x₁, x₂)
.(x₁, x₂) -> .(x₁, x₂)
rev(x₁) -> rev(x₁)
make(x₁) -> make(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

           →DP Problem 3

             ↳AFS

...

               →DP Problem 5

                 ↳Dependency Graph

       →DP Problem 2

         ↳AFS

Dependency Pair:

Rules:

rev(nil) -> nil
rev(rev(x)) -> x
rev(++(x, y)) -> ++(rev(y), rev(x))
++(nil, y) -> y
++(x, nil) -> x
++(.(x, y), z) -> .(x, ++(y, z))
++(x, ++(y, z)) -> ++(++(x, y), z)
make(x) -> .(x, nil)

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳Argument Filtering and Ordering

Dependency Pairs:

REV(++(x, y)) -> REV(x)
REV(++(x, y)) -> REV(y)

Rules:

rev(nil) -> nil
rev(rev(x)) -> x
rev(++(x, y)) -> ++(rev(y), rev(x))
++(nil, y) -> y
++(x, nil) -> x
++(.(x, y), z) -> .(x, ++(y, z))
++(x, ++(y, z)) -> ++(++(x, y), z)
make(x) -> .(x, nil)

The following dependency pairs can be strictly oriented:

REV(++(x, y)) -> REV(x)
REV(++(x, y)) -> REV(y)

The following rules can be oriented:

rev(nil) -> nil
rev(rev(x)) -> x
rev(++(x, y)) -> ++(rev(y), rev(x))
++(nil, y) -> y
++(x, nil) -> x
++(.(x, y), z) -> .(x, ++(y, z))
++(x, ++(y, z)) -> ++(++(x, y), z)
make(x) -> .(x, nil)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(make(x₁)) = x₁

POL(rev(x₁)) = x₁

POL(REV(x₁)) = 1 + x₁

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

POL(nil) = 0

POL(.(x₁, x₂)) = x₁ + x₂

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

REV(x₁) -> REV(x₁)
++(x₁, x₂) -> ++(x₁, x₂)
rev(x₁) -> rev(x₁)
.(x₁, x₂) -> .(x₁, x₂)
make(x₁) -> make(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

           →DP Problem 6

             ↳Dependency Graph

Dependency Pair:

Rules:

rev(nil) -> nil
rev(rev(x)) -> x
rev(++(x, y)) -> ++(rev(y), rev(x))
++(nil, y) -> y
++(x, nil) -> x
++(.(x, y), z) -> .(x, ++(y, z))
++(x, ++(y, z)) -> ++(++(x, y), z)
make(x) -> .(x, nil)

Using the Dependency Graph resulted in no new DP problems.

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

POL(make(x₁))	= 1 + x₁
POL(++'(x₁, x₂))	= 1 + x₁ + x₂
POL(rev(x₁))	= x₁
POL(++(x₁, x₂))	= x₁ + x₂
POL(nil)	= 0
POL(.(x₁, x₂))	= 1 + x₁ + x₂