Termination Proof using AProVE

Term Rewriting System R:
[y, x, n, m]
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
app(nil, y) -> y
app(add(n, x), y) -> add(n, app(x, y))
low(n, nil) -> nil
low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) -> add(m, low(n, x))
if_low(false, n, add(m, x)) -> low(n, x)
high(n, nil) -> nil
high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) -> high(n, x)
if_high(false, n, add(m, x)) -> add(m, high(n, x))
quicksort(nil) -> nil
quicksort(add(n, x)) -> app(quicksort(low(n, x)), add(n, quicksort(high(n, x))))

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

LE(s(x), s(y)) -> LE(x, y)
APP(add(n, x), y) -> APP(x, y)
LOW(n, add(m, x)) -> IF_LOW(le(m, n), n, add(m, x))
LOW(n, add(m, x)) -> LE(m, n)
IF_LOW(true, n, add(m, x)) -> LOW(n, x)
IF_LOW(false, n, add(m, x)) -> LOW(n, x)
HIGH(n, add(m, x)) -> IF_HIGH(le(m, n), n, add(m, x))
HIGH(n, add(m, x)) -> LE(m, n)
IF_HIGH(true, n, add(m, x)) -> HIGH(n, x)
IF_HIGH(false, n, add(m, x)) -> HIGH(n, x)
QUICKSORT(add(n, x)) -> APP(quicksort(low(n, x)), add(n, quicksort(high(n, x))))
QUICKSORT(add(n, x)) -> QUICKSORT(low(n, x))
QUICKSORT(add(n, x)) -> LOW(n, x)
QUICKSORT(add(n, x)) -> QUICKSORT(high(n, x))
QUICKSORT(add(n, x)) -> HIGH(n, x)

Furthermore, R contains five SCCs.

     ↳DPs

       →DP Problem 1

         ↳Argument Filtering and Ordering

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

Dependency Pair:

LE(s(x), s(y)) -> LE(x, y)

Rules:

le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
app(nil, y) -> y
app(add(n, x), y) -> add(n, app(x, y))
low(n, nil) -> nil
low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) -> add(m, low(n, x))
if_low(false, n, add(m, x)) -> low(n, x)
high(n, nil) -> nil
high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) -> high(n, x)
if_high(false, n, add(m, x)) -> add(m, high(n, x))
quicksort(nil) -> nil
quicksort(add(n, x)) -> app(quicksort(low(n, x)), add(n, quicksort(high(n, x))))

Strategy:

innermost

The following dependency pair can be strictly oriented:

LE(s(x), s(y)) -> LE(x, y)

There are no usable rules for innermost that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

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

LE(x₁, x₂) -> LE(x₁, x₂)
s(x₁) -> s(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

           →DP Problem 6

             ↳Dependency Graph

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

Dependency Pair:

Rules:

le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
app(nil, y) -> y
app(add(n, x), y) -> add(n, app(x, y))
low(n, nil) -> nil
low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) -> add(m, low(n, x))
if_low(false, n, add(m, x)) -> low(n, x)
high(n, nil) -> nil
high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) -> high(n, x)
if_high(false, n, add(m, x)) -> add(m, high(n, x))
quicksort(nil) -> nil
quicksort(add(n, x)) -> app(quicksort(low(n, x)), add(n, quicksort(high(n, x))))

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

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

Dependency Pair:

APP(add(n, x), y) -> APP(x, y)

Rules:

le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
app(nil, y) -> y
app(add(n, x), y) -> add(n, app(x, y))
low(n, nil) -> nil
low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) -> add(m, low(n, x))
if_low(false, n, add(m, x)) -> low(n, x)
high(n, nil) -> nil
high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) -> high(n, x)
if_high(false, n, add(m, x)) -> add(m, high(n, x))
quicksort(nil) -> nil
quicksort(add(n, x)) -> app(quicksort(low(n, x)), add(n, quicksort(high(n, x))))

Strategy:

innermost

The following dependency pair can be strictly oriented:

APP(add(n, x), y) -> APP(x, y)

There are no usable rules for innermost that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

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

APP(x₁, x₂) -> APP(x₁, x₂)
add(x₁, x₂) -> add(x₁, x₂)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

           →DP Problem 7

             ↳Dependency Graph

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

Dependency Pair:

Rules:

le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
app(nil, y) -> y
app(add(n, x), y) -> add(n, app(x, y))
low(n, nil) -> nil
low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) -> add(m, low(n, x))
if_low(false, n, add(m, x)) -> low(n, x)
high(n, nil) -> nil
high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) -> high(n, x)
if_high(false, n, add(m, x)) -> add(m, high(n, x))
quicksort(nil) -> nil
quicksort(add(n, x)) -> app(quicksort(low(n, x)), add(n, quicksort(high(n, x))))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Argument Filtering and Ordering

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

Dependency Pairs:

IF_LOW(false, n, add(m, x)) -> LOW(n, x)
IF_LOW(true, n, add(m, x)) -> LOW(n, x)
LOW(n, add(m, x)) -> IF_LOW(le(m, n), n, add(m, x))

Rules:

le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
app(nil, y) -> y
app(add(n, x), y) -> add(n, app(x, y))
low(n, nil) -> nil
low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) -> add(m, low(n, x))
if_low(false, n, add(m, x)) -> low(n, x)
high(n, nil) -> nil
high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) -> high(n, x)
if_high(false, n, add(m, x)) -> add(m, high(n, x))
quicksort(nil) -> nil
quicksort(add(n, x)) -> app(quicksort(low(n, x)), add(n, quicksort(high(n, x))))

Strategy:

innermost

The following dependency pair can be strictly oriented:

LOW(n, add(m, x)) -> IF_LOW(le(m, n), n, add(m, x))

The following usable rules for innermost can be oriented:

le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)

Used ordering: Polynomial ordering with Polynomial interpretation:

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

POL(false) = 0

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

POL(true) = 0

POL(le) = 0

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

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

LOW(x₁, x₂) -> LOW(x₁, x₂)
IF_LOW(x₁, x₂, x₃) -> IF_LOW(x₁, x₂, x₃)
add(x₁, x₂) -> add(x₁, x₂)
le(x₁, x₂) -> le

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

           →DP Problem 8

             ↳Dependency Graph

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

Dependency Pairs:

IF_LOW(false, n, add(m, x)) -> LOW(n, x)
IF_LOW(true, n, add(m, x)) -> LOW(n, x)

Rules:

le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
app(nil, y) -> y
app(add(n, x), y) -> add(n, app(x, y))
low(n, nil) -> nil
low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) -> add(m, low(n, x))
if_low(false, n, add(m, x)) -> low(n, x)
high(n, nil) -> nil
high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) -> high(n, x)
if_high(false, n, add(m, x)) -> add(m, high(n, x))
quicksort(nil) -> nil
quicksort(add(n, x)) -> app(quicksort(low(n, x)), add(n, quicksort(high(n, x))))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳Argument Filtering and Ordering

       →DP Problem 5

         ↳AFS

Dependency Pairs:

IF_HIGH(false, n, add(m, x)) -> HIGH(n, x)
IF_HIGH(true, n, add(m, x)) -> HIGH(n, x)
HIGH(n, add(m, x)) -> IF_HIGH(le(m, n), n, add(m, x))

Rules:

le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
app(nil, y) -> y
app(add(n, x), y) -> add(n, app(x, y))
low(n, nil) -> nil
low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) -> add(m, low(n, x))
if_low(false, n, add(m, x)) -> low(n, x)
high(n, nil) -> nil
high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) -> high(n, x)
if_high(false, n, add(m, x)) -> add(m, high(n, x))
quicksort(nil) -> nil
quicksort(add(n, x)) -> app(quicksort(low(n, x)), add(n, quicksort(high(n, x))))

Strategy:

innermost

The following dependency pairs can be strictly oriented:

IF_HIGH(false, n, add(m, x)) -> HIGH(n, x)
IF_HIGH(true, n, add(m, x)) -> HIGH(n, x)

The following usable rules for innermost can be oriented:

le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)

Used ordering: Polynomial ordering with Polynomial interpretation:

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

POL(false) = 0

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

POL(true) = 0

POL(le) = 0

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

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

IF_HIGH(x₁, x₂, x₃) -> IF_HIGH(x₁, x₂, x₃)
HIGH(x₁, x₂) -> HIGH(x₁, x₂)
add(x₁, x₂) -> add(x₁, x₂)
le(x₁, x₂) -> le

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

           →DP Problem 9

             ↳Dependency Graph

       →DP Problem 5

         ↳AFS

Dependency Pair:

HIGH(n, add(m, x)) -> IF_HIGH(le(m, n), n, add(m, x))

Rules:

le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
app(nil, y) -> y
app(add(n, x), y) -> add(n, app(x, y))
low(n, nil) -> nil
low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) -> add(m, low(n, x))
if_low(false, n, add(m, x)) -> low(n, x)
high(n, nil) -> nil
high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) -> high(n, x)
if_high(false, n, add(m, x)) -> add(m, high(n, x))
quicksort(nil) -> nil
quicksort(add(n, x)) -> app(quicksort(low(n, x)), add(n, quicksort(high(n, x))))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳Argument Filtering and Ordering

Dependency Pairs:

QUICKSORT(add(n, x)) -> QUICKSORT(high(n, x))
QUICKSORT(add(n, x)) -> QUICKSORT(low(n, x))

Rules:

le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
app(nil, y) -> y
app(add(n, x), y) -> add(n, app(x, y))
low(n, nil) -> nil
low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) -> add(m, low(n, x))
if_low(false, n, add(m, x)) -> low(n, x)
high(n, nil) -> nil
high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) -> high(n, x)
if_high(false, n, add(m, x)) -> add(m, high(n, x))
quicksort(nil) -> nil
quicksort(add(n, x)) -> app(quicksort(low(n, x)), add(n, quicksort(high(n, x))))

Strategy:

innermost

The following dependency pairs can be strictly oriented:

QUICKSORT(add(n, x)) -> QUICKSORT(high(n, x))
QUICKSORT(add(n, x)) -> QUICKSORT(low(n, x))

The following usable rules for innermost can be oriented:

high(n, nil) -> nil
high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) -> high(n, x)
if_high(false, n, add(m, x)) -> add(m, high(n, x))
low(n, nil) -> nil
low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) -> add(m, low(n, x))
if_low(false, n, add(m, x)) -> low(n, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)

Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

POL(false) = 0

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

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

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

POL(nil) = 0

POL(true) = 0

POL(le) = 0

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

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

QUICKSORT(x₁) -> QUICKSORT(x₁)
add(x₁, x₂) -> add(x₁, x₂)
high(x₁, x₂) -> high(x₁, x₂)
low(x₁, x₂) -> low(x₁, x₂)
if_high(x₁, x₂, x₃) -> if_high(x₁, x₂, x₃)
le(x₁, x₂) -> le
if_low(x₁, x₂, x₃) -> if_low(x₁, x₂, x₃)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

           →DP Problem 10

             ↳Dependency Graph

Dependency Pair:

Rules:

le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
app(nil, y) -> y
app(add(n, x), y) -> add(n, app(x, y))
low(n, nil) -> nil
low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) -> add(m, low(n, x))
if_low(false, n, add(m, x)) -> low(n, x)
high(n, nil) -> nil
high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) -> high(n, x)
if_high(false, n, add(m, x)) -> add(m, high(n, x))
quicksort(nil) -> nil
quicksort(add(n, x)) -> app(quicksort(low(n, x)), add(n, quicksort(high(n, x))))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

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

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

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

POL(LOW(x₁, x₂))	= 1 + x₁ + x₂
POL(false)	= 0
POL(IF_LOW(x₁, x₂, x₃))	= x₁ + x₂ + x₃
POL(true)	= 0
POL(le)	= 0
POL(add(x₁, x₂))	= 1 + x₁ + x₂

POL(IF_HIGH(x₁, x₂, x₃))	= x₁ + x₂ + x₃
POL(false)	= 0
POL(HIGH(x₁, x₂))	= x₁ + x₂
POL(true)	= 0
POL(le)	= 0
POL(add(x₁, x₂))	= 1 + x₁ + x₂

POL(QUICKSORT(x₁))	= 1 + x₁
POL(if_low(x₁, x₂, x₃))	= x₁ + x₂ + x₃
POL(false)	= 0
POL(high(x₁, x₂))	= x₁ + x₂
POL(if_high(x₁, x₂, x₃))	= x₁ + x₂ + x₃
POL(low(x₁, x₂))	= x₁ + x₂
POL(nil)	= 0
POL(true)	= 0
POL(le)	= 0
POL(add(x₁, x₂))	= 1 + x₁ + x₂