Termination Proof using AProVE

Term Rewriting System R:
[x, y, z]
qsort(nil) -> nil
qsort(.(x, y)) -> ++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y))))
lowers(x, nil) -> nil
lowers(x, .(y, z)) -> if(<=(y, x), .(y, lowers(x, z)), lowers(x, z))
greaters(x, nil) -> nil
greaters(x, .(y, z)) -> if(<=(y, x), greaters(x, z), .(y, greaters(x, z)))

Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

QSORT(.(x, y)) -> QSORT(lowers(x, y))
QSORT(.(x, y)) -> LOWERS(x, y)
QSORT(.(x, y)) -> QSORT(greaters(x, y))
QSORT(.(x, y)) -> GREATERS(x, y)
LOWERS(x, .(y, z)) -> LOWERS(x, z)
GREATERS(x, .(y, z)) -> GREATERS(x, z)

Furthermore, R contains three SCCs.

     ↳DPs

       →DP Problem 1

         ↳Forward Instantiation Transformation

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳Nar

Dependency Pair:

LOWERS(x, .(y, z)) -> LOWERS(x, z)

Rules:

qsort(nil) -> nil
qsort(.(x, y)) -> ++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y))))
lowers(x, nil) -> nil
lowers(x, .(y, z)) -> if(<=(y, x), .(y, lowers(x, z)), lowers(x, z))
greaters(x, nil) -> nil
greaters(x, .(y, z)) -> if(<=(y, x), greaters(x, z), .(y, greaters(x, z)))

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

LOWERS(x, .(y, z)) -> LOWERS(x, z)

one new Dependency Pair is created:

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

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 4

             ↳Forward Instantiation Transformation

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳Nar

Dependency Pair:

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

Rules:

qsort(nil) -> nil
qsort(.(x, y)) -> ++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y))))
lowers(x, nil) -> nil
lowers(x, .(y, z)) -> if(<=(y, x), .(y, lowers(x, z)), lowers(x, z))
greaters(x, nil) -> nil
greaters(x, .(y, z)) -> if(<=(y, x), greaters(x, z), .(y, greaters(x, z)))

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

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

one new Dependency Pair is created:

LOWERS(x'''', .(y, .(y''0, .(y'''', z'''')))) -> LOWERS(x'''', .(y''0, .(y'''', z'''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 4

             ↳FwdInst

...

               →DP Problem 5

                 ↳Polynomial Ordering

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳Nar

Dependency Pair:

LOWERS(x'''', .(y, .(y''0, .(y'''', z'''')))) -> LOWERS(x'''', .(y''0, .(y'''', z'''')))

Rules:

qsort(nil) -> nil
qsort(.(x, y)) -> ++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y))))
lowers(x, nil) -> nil
lowers(x, .(y, z)) -> if(<=(y, x), .(y, lowers(x, z)), lowers(x, z))
greaters(x, nil) -> nil
greaters(x, .(y, z)) -> if(<=(y, x), greaters(x, z), .(y, greaters(x, z)))

The following dependency pair can be strictly oriented:

LOWERS(x'''', .(y, .(y''0, .(y'''', z'''')))) -> LOWERS(x'''', .(y''0, .(y'''', z'''')))

There are no usable rules w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 4

             ↳FwdInst

...

               →DP Problem 6

                 ↳Dependency Graph

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳Nar

Dependency Pair:

Rules:

qsort(nil) -> nil
qsort(.(x, y)) -> ++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y))))
lowers(x, nil) -> nil
lowers(x, .(y, z)) -> if(<=(y, x), .(y, lowers(x, z)), lowers(x, z))
greaters(x, nil) -> nil
greaters(x, .(y, z)) -> if(<=(y, x), greaters(x, z), .(y, greaters(x, z)))

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳Nar

Dependency Pair:

GREATERS(x, .(y, z)) -> GREATERS(x, z)

Rules:

qsort(nil) -> nil
qsort(.(x, y)) -> ++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y))))
lowers(x, nil) -> nil
lowers(x, .(y, z)) -> if(<=(y, x), .(y, lowers(x, z)), lowers(x, z))
greaters(x, nil) -> nil
greaters(x, .(y, z)) -> if(<=(y, x), greaters(x, z), .(y, greaters(x, z)))

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

GREATERS(x, .(y, z)) -> GREATERS(x, z)

one new Dependency Pair is created:

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

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 7

             ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳Nar

Dependency Pair:

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

Rules:

qsort(nil) -> nil
qsort(.(x, y)) -> ++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y))))
lowers(x, nil) -> nil
lowers(x, .(y, z)) -> if(<=(y, x), .(y, lowers(x, z)), lowers(x, z))
greaters(x, nil) -> nil
greaters(x, .(y, z)) -> if(<=(y, x), greaters(x, z), .(y, greaters(x, z)))

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

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

one new Dependency Pair is created:

GREATERS(x'''', .(y, .(y''0, .(y'''', z'''')))) -> GREATERS(x'''', .(y''0, .(y'''', z'''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 7

             ↳FwdInst

...

               →DP Problem 8

                 ↳Polynomial Ordering

       →DP Problem 3

         ↳Nar

Dependency Pair:

GREATERS(x'''', .(y, .(y''0, .(y'''', z'''')))) -> GREATERS(x'''', .(y''0, .(y'''', z'''')))

Rules:

qsort(nil) -> nil
qsort(.(x, y)) -> ++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y))))
lowers(x, nil) -> nil
lowers(x, .(y, z)) -> if(<=(y, x), .(y, lowers(x, z)), lowers(x, z))
greaters(x, nil) -> nil
greaters(x, .(y, z)) -> if(<=(y, x), greaters(x, z), .(y, greaters(x, z)))

The following dependency pair can be strictly oriented:

GREATERS(x'''', .(y, .(y''0, .(y'''', z'''')))) -> GREATERS(x'''', .(y''0, .(y'''', z'''')))

There are no usable rules w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 7

             ↳FwdInst

...

               →DP Problem 9

                 ↳Dependency Graph

       →DP Problem 3

         ↳Nar

Dependency Pair:

Rules:

qsort(nil) -> nil
qsort(.(x, y)) -> ++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y))))
lowers(x, nil) -> nil
lowers(x, .(y, z)) -> if(<=(y, x), .(y, lowers(x, z)), lowers(x, z))
greaters(x, nil) -> nil
greaters(x, .(y, z)) -> if(<=(y, x), greaters(x, z), .(y, greaters(x, z)))

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳Narrowing Transformation

Dependency Pairs:

QSORT(.(x, y)) -> QSORT(greaters(x, y))
QSORT(.(x, y)) -> QSORT(lowers(x, y))

Rules:

qsort(nil) -> nil
qsort(.(x, y)) -> ++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y))))
lowers(x, nil) -> nil
lowers(x, .(y, z)) -> if(<=(y, x), .(y, lowers(x, z)), lowers(x, z))
greaters(x, nil) -> nil
greaters(x, .(y, z)) -> if(<=(y, x), greaters(x, z), .(y, greaters(x, z)))

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

QSORT(.(x, y)) -> QSORT(lowers(x, y))

two new Dependency Pairs are created:

QSORT(.(x'', nil)) -> QSORT(nil)
QSORT(.(x'', .(y'', z'))) -> QSORT(if(<=(y'', x''), .(y'', lowers(x'', z')), lowers(x'', z')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳Nar

           →DP Problem 10

             ↳Narrowing Transformation

Dependency Pair:

QSORT(.(x, y)) -> QSORT(greaters(x, y))

Rules:

qsort(nil) -> nil
qsort(.(x, y)) -> ++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y))))
lowers(x, nil) -> nil
lowers(x, .(y, z)) -> if(<=(y, x), .(y, lowers(x, z)), lowers(x, z))
greaters(x, nil) -> nil
greaters(x, .(y, z)) -> if(<=(y, x), greaters(x, z), .(y, greaters(x, z)))

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

QSORT(.(x, y)) -> QSORT(greaters(x, y))

two new Dependency Pairs are created:

QSORT(.(x'', nil)) -> QSORT(nil)
QSORT(.(x'', .(y'', z'))) -> QSORT(if(<=(y'', x''), greaters(x'', z'), .(y'', greaters(x'', z'))))

The transformation is resulting in no new DP problems.

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

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

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