Termination Proof using AProVE

Term Rewriting System R:
[x, y, n, m]
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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:

MINUS(s(x), s(y)) -> MINUS(x, y)
QUOT(s(x), s(y)) -> QUOT(minus(x, y), s(y))
QUOT(s(x), s(y)) -> MINUS(x, y)
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 seven SCCs.

     ↳DPs

       →DP Problem 1

         ↳Forward Instantiation Transformation

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pair:

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

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

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

one new Dependency Pair is created:

MINUS(s(s(x'')), s(s(y''))) -> MINUS(s(x''), s(y''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 8

             ↳Forward Instantiation Transformation

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pair:

MINUS(s(s(x'')), s(s(y''))) -> MINUS(s(x''), s(y''))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

MINUS(s(s(x'')), s(s(y''))) -> MINUS(s(x''), s(y''))

one new Dependency Pair is created:

MINUS(s(s(s(x''''))), s(s(s(y'''')))) -> MINUS(s(s(x'''')), s(s(y'''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 8

             ↳FwdInst

...

               →DP Problem 9

                 ↳Polynomial Ordering

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pair:

MINUS(s(s(s(x''''))), s(s(s(y'''')))) -> MINUS(s(s(x'''')), s(s(y'''')))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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:

MINUS(s(s(s(x''''))), s(s(s(y'''')))) -> MINUS(s(s(x'''')), s(s(y'''')))

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

Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 8

             ↳FwdInst

...

               →DP Problem 10

                 ↳Dependency Graph

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pair:

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

         ↳FwdInst

       →DP Problem 2

         ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pair:

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

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

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

one new Dependency Pair is created:

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

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 11

             ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pair:

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

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

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

one new Dependency Pair is created:

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

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 11

             ↳FwdInst

...

               →DP Problem 12

                 ↳Polynomial Ordering

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pair:

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

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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(s(s(x''''))), s(s(s(y'''')))) -> LE(s(s(x'''')), s(s(y'''')))

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

Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 11

             ↳FwdInst

...

               →DP Problem 13

                 ↳Dependency Graph

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pair:

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳Forward Instantiation Transformation

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pair:

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

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

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

one new Dependency Pair is created:

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

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

           →DP Problem 14

             ↳Forward Instantiation Transformation

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pair:

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

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

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

one new Dependency Pair is created:

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

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

           →DP Problem 14

             ↳FwdInst

...

               →DP Problem 15

                 ↳Polynomial Ordering

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pair:

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

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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, add(n'''', add(n''''', x''''))), y'''') -> APP(add(n'''', add(n''''', x'''')), y'''')

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

Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

           →DP Problem 14

             ↳FwdInst

...

               →DP Problem 16

                 ↳Dependency Graph

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pair:

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Narrowing Transformation

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pair:

QUOT(s(x), s(y)) -> QUOT(minus(x, y), s(y))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

QUOT(s(x), s(y)) -> QUOT(minus(x, y), s(y))

two new Dependency Pairs are created:

QUOT(s(x''), s(0)) -> QUOT(x'', s(0))
QUOT(s(s(x'')), s(s(y''))) -> QUOT(minus(x'', y''), s(s(y'')))

The transformation is resulting in two new DP problems:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

           →DP Problem 17

             ↳Forward Instantiation Transformation

           →DP Problem 18

             ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pair:

QUOT(s(x''), s(0)) -> QUOT(x'', s(0))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

QUOT(s(x''), s(0)) -> QUOT(x'', s(0))

one new Dependency Pair is created:

QUOT(s(s(x'''')), s(0)) -> QUOT(s(x''''), s(0))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

           →DP Problem 17

             ↳FwdInst

...

               →DP Problem 19

                 ↳Polynomial Ordering

           →DP Problem 18

             ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pair:

QUOT(s(s(x'''')), s(0)) -> QUOT(s(x''''), s(0))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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:

QUOT(s(s(x'''')), s(0)) -> QUOT(s(x''''), s(0))

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

Used ordering: Polynomial ordering with Polynomial interpretation:

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

POL(0) = 0

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

           →DP Problem 17

             ↳FwdInst

...

               →DP Problem 22

                 ↳Dependency Graph

           →DP Problem 18

             ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pair:

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

           →DP Problem 17

             ↳FwdInst

           →DP Problem 18

             ↳Narrowing Transformation

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pair:

QUOT(s(s(x'')), s(s(y''))) -> QUOT(minus(x'', y''), s(s(y'')))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

QUOT(s(s(x'')), s(s(y''))) -> QUOT(minus(x'', y''), s(s(y'')))

two new Dependency Pairs are created:

QUOT(s(s(x''')), s(s(0))) -> QUOT(x''', s(s(0)))
QUOT(s(s(s(x'))), s(s(s(y')))) -> QUOT(minus(x', y'), s(s(s(y'))))

The transformation is resulting in two new DP problems:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

           →DP Problem 17

             ↳FwdInst

           →DP Problem 18

             ↳Nar

...

               →DP Problem 20

                 ↳Polynomial Ordering

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pair:

QUOT(s(s(x''')), s(s(0))) -> QUOT(x''', s(s(0)))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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:

QUOT(s(s(x''')), s(s(0))) -> QUOT(x''', s(s(0)))

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

Used ordering: Polynomial ordering with Polynomial interpretation:

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

POL(0) = 0

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

           →DP Problem 17

             ↳FwdInst

           →DP Problem 18

             ↳Nar

...

               →DP Problem 21

                 ↳Polynomial Ordering

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pair:

QUOT(s(s(s(x'))), s(s(s(y')))) -> QUOT(minus(x', y'), s(s(s(y'))))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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:

QUOT(s(s(s(x'))), s(s(s(y')))) -> QUOT(minus(x', y'), s(s(s(y'))))

Additionally, the following usable rules for innermost w.r.t. to the implicit AFS can be oriented:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)

Used ordering: Polynomial ordering with Polynomial interpretation:

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

POL(0) = 1

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

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Narrowing Transformation

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

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:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

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

three new Dependency Pairs are created:

LOW(n', add(0, x)) -> IF_LOW(true, n', add(0, x))
LOW(0, add(s(x''), x)) -> IF_LOW(false, 0, add(s(x''), x))
LOW(s(y'), add(s(x''), x)) -> IF_LOW(le(x'', y'), s(y'), add(s(x''), x))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

           →DP Problem 25

             ↳Narrowing Transformation

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pairs:

LOW(s(y'), add(s(x''), x)) -> IF_LOW(le(x'', y'), s(y'), add(s(x''), x))
LOW(0, add(s(x''), x)) -> IF_LOW(false, 0, add(s(x''), x))
IF_LOW(true, n, add(m, x)) -> LOW(n, x)
LOW(n', add(0, x)) -> IF_LOW(true, n', add(0, x))
IF_LOW(false, n, add(m, x)) -> LOW(n, x)

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

LOW(s(y'), add(s(x''), x)) -> IF_LOW(le(x'', y'), s(y'), add(s(x''), x))

three new Dependency Pairs are created:

LOW(s(y''), add(s(0), x)) -> IF_LOW(true, s(y''), add(s(0), x))
LOW(s(0), add(s(s(x''')), x)) -> IF_LOW(false, s(0), add(s(s(x''')), x))
LOW(s(s(y'')), add(s(s(x''')), x)) -> IF_LOW(le(x''', y''), s(s(y'')), add(s(s(x''')), x))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

           →DP Problem 25

             ↳Nar

...

               →DP Problem 26

                 ↳Instantiation Transformation

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pairs:

LOW(s(s(y'')), add(s(s(x''')), x)) -> IF_LOW(le(x''', y''), s(s(y'')), add(s(s(x''')), x))
LOW(s(0), add(s(s(x''')), x)) -> IF_LOW(false, s(0), add(s(s(x''')), x))
LOW(s(y''), add(s(0), x)) -> IF_LOW(true, s(y''), add(s(0), x))
IF_LOW(true, n, add(m, x)) -> LOW(n, x)
LOW(n', add(0, x)) -> IF_LOW(true, n', add(0, x))
IF_LOW(false, n, add(m, x)) -> LOW(n, x)
LOW(0, add(s(x''), x)) -> IF_LOW(false, 0, add(s(x''), x))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

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

three new Dependency Pairs are created:

IF_LOW(true, n', add(0, x'')) -> LOW(n', x'')
IF_LOW(true, s(y''''), add(s(0), x'')) -> LOW(s(y''''), x'')
IF_LOW(true, s(s(y'''')), add(s(s(x''''')), x')) -> LOW(s(s(y'''')), x')

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

           →DP Problem 25

             ↳Nar

...

               →DP Problem 27

                 ↳Instantiation Transformation

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pairs:

IF_LOW(true, s(s(y'''')), add(s(s(x''''')), x')) -> LOW(s(s(y'''')), x')
LOW(s(0), add(s(s(x''')), x)) -> IF_LOW(false, s(0), add(s(s(x''')), x))
IF_LOW(true, s(y''''), add(s(0), x'')) -> LOW(s(y''''), x'')
LOW(s(y''), add(s(0), x)) -> IF_LOW(true, s(y''), add(s(0), x))
LOW(0, add(s(x''), x)) -> IF_LOW(false, 0, add(s(x''), x))
IF_LOW(true, n', add(0, x'')) -> LOW(n', x'')
LOW(n', add(0, x)) -> IF_LOW(true, n', add(0, x))
IF_LOW(false, n, add(m, x)) -> LOW(n, x)
LOW(s(s(y'')), add(s(s(x''')), x)) -> IF_LOW(le(x''', y''), s(s(y'')), add(s(s(x''')), x))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

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

three new Dependency Pairs are created:

IF_LOW(false, 0, add(s(x''''), x'')) -> LOW(0, x'')
IF_LOW(false, s(0), add(s(s(x''''')), x'')) -> LOW(s(0), x'')
IF_LOW(false, s(s(y'''')), add(s(s(x''''')), x')) -> LOW(s(s(y'''')), x')

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

           →DP Problem 25

             ↳Nar

...

               →DP Problem 28

                 ↳Forward Instantiation Transformation

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pairs:

IF_LOW(false, s(s(y'''')), add(s(s(x''''')), x')) -> LOW(s(s(y'''')), x')
LOW(s(s(y'')), add(s(s(x''')), x)) -> IF_LOW(le(x''', y''), s(s(y'')), add(s(s(x''')), x))
IF_LOW(false, s(0), add(s(s(x''''')), x'')) -> LOW(s(0), x'')
LOW(s(0), add(s(s(x''')), x)) -> IF_LOW(false, s(0), add(s(s(x''')), x))
IF_LOW(true, s(y''''), add(s(0), x'')) -> LOW(s(y''''), x'')
LOW(s(y''), add(s(0), x)) -> IF_LOW(true, s(y''), add(s(0), x))
IF_LOW(false, 0, add(s(x''''), x'')) -> LOW(0, x'')
LOW(0, add(s(x''), x)) -> IF_LOW(false, 0, add(s(x''), x))
IF_LOW(true, n', add(0, x'')) -> LOW(n', x'')
LOW(n', add(0, x)) -> IF_LOW(true, n', add(0, x))
IF_LOW(true, s(s(y'''')), add(s(s(x''''')), x')) -> LOW(s(s(y'''')), x')

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

IF_LOW(true, n', add(0, x'')) -> LOW(n', x'')

five new Dependency Pairs are created:

IF_LOW(true, n''', add(0, add(0, x'''))) -> LOW(n''', add(0, x'''))
IF_LOW(true, 0, add(0, add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
IF_LOW(true, s(y''''), add(0, add(s(0), x'''))) -> LOW(s(y''''), add(s(0), x'''))
IF_LOW(true, s(0), add(0, add(s(s(x''''')), x'''))) -> LOW(s(0), add(s(s(x''''')), x'''))
IF_LOW(true, s(s(y'''')), add(0, add(s(s(x''''')), x'''))) -> LOW(s(s(y'''')), add(s(s(x''''')), x'''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

           →DP Problem 25

             ↳Nar

...

               →DP Problem 29

                 ↳Forward Instantiation Transformation

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pairs:

IF_LOW(true, s(s(y'''')), add(0, add(s(s(x''''')), x'''))) -> LOW(s(s(y'''')), add(s(s(x''''')), x'''))
IF_LOW(true, s(0), add(0, add(s(s(x''''')), x'''))) -> LOW(s(0), add(s(s(x''''')), x'''))
IF_LOW(true, s(s(y'''')), add(s(s(x''''')), x')) -> LOW(s(s(y'''')), x')
LOW(s(s(y'')), add(s(s(x''')), x)) -> IF_LOW(le(x''', y''), s(s(y'')), add(s(s(x''')), x))
IF_LOW(false, s(0), add(s(s(x''''')), x'')) -> LOW(s(0), x'')
LOW(s(0), add(s(s(x''')), x)) -> IF_LOW(false, s(0), add(s(s(x''')), x))
IF_LOW(true, s(y''''), add(s(0), x'')) -> LOW(s(y''''), x'')
LOW(s(y''), add(s(0), x)) -> IF_LOW(true, s(y''), add(s(0), x))
IF_LOW(true, s(y''''), add(0, add(s(0), x'''))) -> LOW(s(y''''), add(s(0), x'''))
IF_LOW(false, 0, add(s(x''''), x'')) -> LOW(0, x'')
LOW(0, add(s(x''), x)) -> IF_LOW(false, 0, add(s(x''), x))
IF_LOW(true, 0, add(0, add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
IF_LOW(true, n''', add(0, add(0, x'''))) -> LOW(n''', add(0, x'''))
LOW(n', add(0, x)) -> IF_LOW(true, n', add(0, x))
IF_LOW(false, s(s(y'''')), add(s(s(x''''')), x')) -> LOW(s(s(y'''')), x')

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

LOW(n', add(0, x)) -> IF_LOW(true, n', add(0, x))

five new Dependency Pairs are created:

LOW(n'', add(0, add(0, x'''''))) -> IF_LOW(true, n'', add(0, add(0, x''''')))
LOW(0, add(0, add(s(x''''''), x'0''))) -> IF_LOW(true, 0, add(0, add(s(x''''''), x'0'')))
LOW(s(y''''''), add(0, add(s(0), x'''''))) -> IF_LOW(true, s(y''''''), add(0, add(s(0), x''''')))
LOW(s(0), add(0, add(s(s(x''''''')), x'''''))) -> IF_LOW(true, s(0), add(0, add(s(s(x''''''')), x''''')))
LOW(s(s(y'''''')), add(0, add(s(s(x''''''')), x'''''))) -> IF_LOW(true, s(s(y'''''')), add(0, add(s(s(x''''''')), x''''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

           →DP Problem 25

             ↳Nar

...

               →DP Problem 30

                 ↳Forward Instantiation Transformation

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pairs:

IF_LOW(false, s(s(y'''')), add(s(s(x''''')), x')) -> LOW(s(s(y'''')), x')
LOW(s(s(y'''''')), add(0, add(s(s(x''''''')), x'''''))) -> IF_LOW(true, s(s(y'''''')), add(0, add(s(s(x''''''')), x''''')))
IF_LOW(true, s(0), add(0, add(s(s(x''''')), x'''))) -> LOW(s(0), add(s(s(x''''')), x'''))
LOW(s(0), add(0, add(s(s(x''''''')), x'''''))) -> IF_LOW(true, s(0), add(0, add(s(s(x''''''')), x''''')))
IF_LOW(true, s(y''''), add(0, add(s(0), x'''))) -> LOW(s(y''''), add(s(0), x'''))
LOW(s(y''''''), add(0, add(s(0), x'''''))) -> IF_LOW(true, s(y''''''), add(0, add(s(0), x''''')))
IF_LOW(false, 0, add(s(x''''), x'')) -> LOW(0, x'')
LOW(0, add(s(x''), x)) -> IF_LOW(false, 0, add(s(x''), x))
IF_LOW(true, 0, add(0, add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
LOW(0, add(0, add(s(x''''''), x'0''))) -> IF_LOW(true, 0, add(0, add(s(x''''''), x'0'')))
IF_LOW(true, n''', add(0, add(0, x'''))) -> LOW(n''', add(0, x'''))
LOW(n'', add(0, add(0, x'''''))) -> IF_LOW(true, n'', add(0, add(0, x''''')))
IF_LOW(false, s(0), add(s(s(x''''')), x'')) -> LOW(s(0), x'')
LOW(s(0), add(s(s(x''')), x)) -> IF_LOW(false, s(0), add(s(s(x''')), x))
IF_LOW(true, s(y''''), add(s(0), x'')) -> LOW(s(y''''), x'')
LOW(s(y''), add(s(0), x)) -> IF_LOW(true, s(y''), add(s(0), x))
IF_LOW(true, s(s(y'''')), add(s(s(x''''')), x')) -> LOW(s(s(y'''')), x')
LOW(s(s(y'')), add(s(s(x''')), x)) -> IF_LOW(le(x''', y''), s(s(y'')), add(s(s(x''')), x))
IF_LOW(true, s(s(y'''')), add(0, add(s(s(x''''')), x'''))) -> LOW(s(s(y'''')), add(s(s(x''''')), x'''))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

IF_LOW(true, s(y''''), add(s(0), x'')) -> LOW(s(y''''), x'')

seven new Dependency Pairs are created:

IF_LOW(true, s(y'''''), add(s(0), add(s(0), x'''))) -> LOW(s(y'''''), add(s(0), x'''))
IF_LOW(true, s(0), add(s(0), add(s(s(x''''')), x'''))) -> LOW(s(0), add(s(s(x''''')), x'''))
IF_LOW(true, s(s(y''''')), add(s(0), add(s(s(x''''')), x'''))) -> LOW(s(s(y''''')), add(s(s(x''''')), x'''))
IF_LOW(true, s(y'''''), add(s(0), add(0, add(0, x''''''')))) -> LOW(s(y'''''), add(0, add(0, x''''''')))
IF_LOW(true, s(y'''''), add(s(0), add(0, add(s(0), x''''''')))) -> LOW(s(y'''''), add(0, add(s(0), x''''''')))
IF_LOW(true, s(0), add(s(0), add(0, add(s(s(x''''''''')), x''''''')))) -> LOW(s(0), add(0, add(s(s(x''''''''')), x''''''')))
IF_LOW(true, s(s(y'''''''')), add(s(0), add(0, add(s(s(x''''''''')), x''''''')))) -> LOW(s(s(y'''''''')), add(0, add(s(s(x''''''''')), x''''''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

           →DP Problem 25

             ↳Nar

...

               →DP Problem 31

                 ↳Forward Instantiation Transformation

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pairs:

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

IF_LOW(true, s(s(y'''')), add(s(s(x''''')), x')) -> LOW(s(s(y'''')), x')

five new Dependency Pairs are created:

IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(s(0), x'''))) -> LOW(s(s(y''''')), add(s(0), x'''))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> LOW(s(s(y''''')), add(s(s(x''''')), x'''))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(0, add(0, x''''''')))) -> LOW(s(s(y''''')), add(0, add(0, x''''''')))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(0, add(s(0), x''''''')))) -> LOW(s(s(y''''')), add(0, add(s(0), x''''''')))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(0, add(s(s(x''''''''')), x''''''')))) -> LOW(s(s(y''''')), add(0, add(s(s(x''''''''')), x''''''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

           →DP Problem 25

             ↳Nar

...

               →DP Problem 32

                 ↳Forward Instantiation Transformation

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pairs:

IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(0, add(s(s(x''''''''')), x''''''')))) -> LOW(s(s(y''''')), add(0, add(s(s(x''''''''')), x''''''')))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(0, add(s(0), x''''''')))) -> LOW(s(s(y''''')), add(0, add(s(0), x''''''')))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(0, add(0, x''''''')))) -> LOW(s(s(y''''')), add(0, add(0, x''''''')))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> LOW(s(s(y''''')), add(s(s(x''''')), x'''))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(s(0), x'''))) -> LOW(s(s(y''''')), add(s(0), x'''))
IF_LOW(true, s(0), add(s(0), add(0, add(s(s(x''''''''')), x''''''')))) -> LOW(s(0), add(0, add(s(s(x''''''''')), x''''''')))
IF_LOW(true, s(y'''''), add(s(0), add(0, add(s(0), x''''''')))) -> LOW(s(y'''''), add(0, add(s(0), x''''''')))
IF_LOW(true, s(y'''''), add(s(0), add(0, add(0, x''''''')))) -> LOW(s(y'''''), add(0, add(0, x''''''')))
IF_LOW(true, s(s(y''''')), add(s(0), add(s(s(x''''')), x'''))) -> LOW(s(s(y''''')), add(s(s(x''''')), x'''))
IF_LOW(true, s(0), add(0, add(s(s(x''''')), x'''))) -> LOW(s(0), add(s(s(x''''')), x'''))
LOW(s(0), add(0, add(s(s(x''''''')), x'''''))) -> IF_LOW(true, s(0), add(0, add(s(s(x''''''')), x''''')))
IF_LOW(true, s(y''''), add(0, add(s(0), x'''))) -> LOW(s(y''''), add(s(0), x'''))
LOW(s(y''''''), add(0, add(s(0), x'''''))) -> IF_LOW(true, s(y''''''), add(0, add(s(0), x''''')))
IF_LOW(false, 0, add(s(x''''), x'')) -> LOW(0, x'')
LOW(0, add(s(x''), x)) -> IF_LOW(false, 0, add(s(x''), x))
IF_LOW(true, 0, add(0, add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
LOW(0, add(0, add(s(x''''''), x'0''))) -> IF_LOW(true, 0, add(0, add(s(x''''''), x'0'')))
IF_LOW(true, n''', add(0, add(0, x'''))) -> LOW(n''', add(0, x'''))
LOW(n'', add(0, add(0, x'''''))) -> IF_LOW(true, n'', add(0, add(0, x''''')))
IF_LOW(false, s(0), add(s(s(x''''')), x'')) -> LOW(s(0), x'')
LOW(s(0), add(s(s(x''')), x)) -> IF_LOW(false, s(0), add(s(s(x''')), x))
IF_LOW(true, s(0), add(s(0), add(s(s(x''''')), x'''))) -> LOW(s(0), add(s(s(x''''')), x'''))
IF_LOW(true, s(y'''''), add(s(0), add(s(0), x'''))) -> LOW(s(y'''''), add(s(0), x'''))
LOW(s(y''), add(s(0), x)) -> IF_LOW(true, s(y''), add(s(0), x))
IF_LOW(false, s(s(y'''')), add(s(s(x''''')), x')) -> LOW(s(s(y'''')), x')
LOW(s(s(y'')), add(s(s(x''')), x)) -> IF_LOW(le(x''', y''), s(s(y'')), add(s(s(x''')), x))
IF_LOW(true, s(s(y'''')), add(0, add(s(s(x''''')), x'''))) -> LOW(s(s(y'''')), add(s(s(x''''')), x'''))
LOW(s(s(y'''''')), add(0, add(s(s(x''''''')), x'''''))) -> IF_LOW(true, s(s(y'''''')), add(0, add(s(s(x''''''')), x''''')))
IF_LOW(true, s(s(y'''''''')), add(s(0), add(0, add(s(s(x''''''''')), x''''''')))) -> LOW(s(s(y'''''''')), add(0, add(s(s(x''''''''')), x''''''')))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

IF_LOW(false, 0, add(s(x''''), x'')) -> LOW(0, x'')

three new Dependency Pairs are created:

IF_LOW(false, 0, add(s(x''''), add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
IF_LOW(false, 0, add(s(x''''), add(0, add(0, x''''''')))) -> LOW(0, add(0, add(0, x''''''')))
IF_LOW(false, 0, add(s(x''''), add(0, add(s(x''''''''), x'0'''')))) -> LOW(0, add(0, add(s(x''''''''), x'0'''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

           →DP Problem 25

             ↳Nar

...

               →DP Problem 33

                 ↳Forward Instantiation Transformation

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pairs:

IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(0, add(s(0), x''''''')))) -> LOW(s(s(y''''')), add(0, add(s(0), x''''''')))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(0, add(0, x''''''')))) -> LOW(s(s(y''''')), add(0, add(0, x''''''')))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> LOW(s(s(y''''')), add(s(s(x''''')), x'''))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(s(0), x'''))) -> LOW(s(s(y''''')), add(s(0), x'''))
IF_LOW(true, s(s(y'''''''')), add(s(0), add(0, add(s(s(x''''''''')), x''''''')))) -> LOW(s(s(y'''''''')), add(0, add(s(s(x''''''''')), x''''''')))
IF_LOW(true, s(0), add(s(0), add(0, add(s(s(x''''''''')), x''''''')))) -> LOW(s(0), add(0, add(s(s(x''''''''')), x''''''')))
IF_LOW(true, s(y'''''), add(s(0), add(0, add(s(0), x''''''')))) -> LOW(s(y'''''), add(0, add(s(0), x''''''')))
IF_LOW(true, s(y'''''), add(s(0), add(0, add(0, x''''''')))) -> LOW(s(y'''''), add(0, add(0, x''''''')))
IF_LOW(true, s(s(y''''')), add(s(0), add(s(s(x''''')), x'''))) -> LOW(s(s(y''''')), add(s(s(x''''')), x'''))
IF_LOW(true, s(0), add(0, add(s(s(x''''')), x'''))) -> LOW(s(0), add(s(s(x''''')), x'''))
LOW(s(0), add(0, add(s(s(x''''''')), x'''''))) -> IF_LOW(true, s(0), add(0, add(s(s(x''''''')), x''''')))
IF_LOW(true, s(y''''), add(0, add(s(0), x'''))) -> LOW(s(y''''), add(s(0), x'''))
LOW(s(y''''''), add(0, add(s(0), x'''''))) -> IF_LOW(true, s(y''''''), add(0, add(s(0), x''''')))
IF_LOW(false, 0, add(s(x''''), add(0, add(s(x''''''''), x'0'''')))) -> LOW(0, add(0, add(s(x''''''''), x'0'''')))
IF_LOW(false, 0, add(s(x''''), add(0, add(0, x''''''')))) -> LOW(0, add(0, add(0, x''''''')))
IF_LOW(false, 0, add(s(x''''), add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
LOW(0, add(s(x''), x)) -> IF_LOW(false, 0, add(s(x''), x))
IF_LOW(true, 0, add(0, add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
LOW(0, add(0, add(s(x''''''), x'0''))) -> IF_LOW(true, 0, add(0, add(s(x''''''), x'0'')))
IF_LOW(true, n''', add(0, add(0, x'''))) -> LOW(n''', add(0, x'''))
LOW(n'', add(0, add(0, x'''''))) -> IF_LOW(true, n'', add(0, add(0, x''''')))
IF_LOW(false, s(0), add(s(s(x''''')), x'')) -> LOW(s(0), x'')
LOW(s(0), add(s(s(x''')), x)) -> IF_LOW(false, s(0), add(s(s(x''')), x))
IF_LOW(true, s(0), add(s(0), add(s(s(x''''')), x'''))) -> LOW(s(0), add(s(s(x''''')), x'''))
IF_LOW(true, s(y'''''), add(s(0), add(s(0), x'''))) -> LOW(s(y'''''), add(s(0), x'''))
LOW(s(y''), add(s(0), x)) -> IF_LOW(true, s(y''), add(s(0), x))
IF_LOW(false, s(s(y'''')), add(s(s(x''''')), x')) -> LOW(s(s(y'''')), x')
LOW(s(s(y'')), add(s(s(x''')), x)) -> IF_LOW(le(x''', y''), s(s(y'')), add(s(s(x''')), x))
IF_LOW(true, s(s(y'''')), add(0, add(s(s(x''''')), x'''))) -> LOW(s(s(y'''')), add(s(s(x''''')), x'''))
LOW(s(s(y'''''')), add(0, add(s(s(x''''''')), x'''''))) -> IF_LOW(true, s(s(y'''''')), add(0, add(s(s(x''''''')), x''''')))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(0, add(s(s(x''''''''')), x''''''')))) -> LOW(s(s(y''''')), add(0, add(s(s(x''''''''')), x''''''')))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

LOW(0, add(s(x''), x)) -> IF_LOW(false, 0, add(s(x''), x))

three new Dependency Pairs are created:

LOW(0, add(s(x'''), add(s(x'''''''), x'0''))) -> IF_LOW(false, 0, add(s(x'''), add(s(x'''''''), x'0'')))
LOW(0, add(s(x'''), add(0, add(0, x''''''''')))) -> IF_LOW(false, 0, add(s(x'''), add(0, add(0, x'''''''''))))
LOW(0, add(s(x'''), add(0, add(s(x''''''''''), x'0'''''')))) -> IF_LOW(false, 0, add(s(x'''), add(0, add(s(x''''''''''), x'0''''''))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

           →DP Problem 25

             ↳Nar

...

               →DP Problem 34

                 ↳Forward Instantiation Transformation

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pairs:

IF_LOW(true, s(s(y'''''''')), add(s(0), add(0, add(s(s(x''''''''')), x''''''')))) -> LOW(s(s(y'''''''')), add(0, add(s(s(x''''''''')), x''''''')))
IF_LOW(true, s(0), add(s(0), add(0, add(s(s(x''''''''')), x''''''')))) -> LOW(s(0), add(0, add(s(s(x''''''''')), x''''''')))
IF_LOW(true, s(y'''''), add(s(0), add(0, add(s(0), x''''''')))) -> LOW(s(y'''''), add(0, add(s(0), x''''''')))
IF_LOW(true, s(y'''''), add(s(0), add(0, add(0, x''''''')))) -> LOW(s(y'''''), add(0, add(0, x''''''')))
IF_LOW(true, s(s(y''''')), add(s(0), add(s(s(x''''')), x'''))) -> LOW(s(s(y''''')), add(s(s(x''''')), x'''))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(0, add(s(s(x''''''''')), x''''''')))) -> LOW(s(s(y''''')), add(0, add(s(s(x''''''''')), x''''''')))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(0, add(0, x''''''')))) -> LOW(s(s(y''''')), add(0, add(0, x''''''')))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> LOW(s(s(y''''')), add(s(s(x''''')), x'''))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(s(0), x'''))) -> LOW(s(s(y''''')), add(s(0), x'''))
IF_LOW(false, s(s(y'''')), add(s(s(x''''')), x')) -> LOW(s(s(y'''')), x')
LOW(s(s(y'')), add(s(s(x''')), x)) -> IF_LOW(le(x''', y''), s(s(y'')), add(s(s(x''')), x))
IF_LOW(true, s(s(y'''')), add(0, add(s(s(x''''')), x'''))) -> LOW(s(s(y'''')), add(s(s(x''''')), x'''))
LOW(s(s(y'''''')), add(0, add(s(s(x''''''')), x'''''))) -> IF_LOW(true, s(s(y'''''')), add(0, add(s(s(x''''''')), x''''')))
IF_LOW(true, s(0), add(0, add(s(s(x''''')), x'''))) -> LOW(s(0), add(s(s(x''''')), x'''))
LOW(s(0), add(0, add(s(s(x''''''')), x'''''))) -> IF_LOW(true, s(0), add(0, add(s(s(x''''''')), x''''')))
IF_LOW(false, 0, add(s(x''''), add(0, add(s(x''''''''), x'0'''')))) -> LOW(0, add(0, add(s(x''''''''), x'0'''')))
LOW(0, add(s(x'''), add(0, add(s(x''''''''''), x'0'''''')))) -> IF_LOW(false, 0, add(s(x'''), add(0, add(s(x''''''''''), x'0''''''))))
IF_LOW(false, 0, add(s(x''''), add(0, add(0, x''''''')))) -> LOW(0, add(0, add(0, x''''''')))
LOW(0, add(s(x'''), add(0, add(0, x''''''''')))) -> IF_LOW(false, 0, add(s(x'''), add(0, add(0, x'''''''''))))
IF_LOW(false, 0, add(s(x''''), add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
LOW(0, add(s(x'''), add(s(x'''''''), x'0''))) -> IF_LOW(false, 0, add(s(x'''), add(s(x'''''''), x'0'')))
IF_LOW(true, 0, add(0, add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
LOW(0, add(0, add(s(x''''''), x'0''))) -> IF_LOW(true, 0, add(0, add(s(x''''''), x'0'')))
IF_LOW(true, n''', add(0, add(0, x'''))) -> LOW(n''', add(0, x'''))
LOW(n'', add(0, add(0, x'''''))) -> IF_LOW(true, n'', add(0, add(0, x''''')))
IF_LOW(false, s(0), add(s(s(x''''')), x'')) -> LOW(s(0), x'')
LOW(s(0), add(s(s(x''')), x)) -> IF_LOW(false, s(0), add(s(s(x''')), x))
IF_LOW(true, s(0), add(s(0), add(s(s(x''''')), x'''))) -> LOW(s(0), add(s(s(x''''')), x'''))
IF_LOW(true, s(y'''''), add(s(0), add(s(0), x'''))) -> LOW(s(y'''''), add(s(0), x'''))
LOW(s(y''), add(s(0), x)) -> IF_LOW(true, s(y''), add(s(0), x))
IF_LOW(true, s(y''''), add(0, add(s(0), x'''))) -> LOW(s(y''''), add(s(0), x'''))
LOW(s(y''''''), add(0, add(s(0), x'''''))) -> IF_LOW(true, s(y''''''), add(0, add(s(0), x''''')))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(0, add(s(0), x''''''')))) -> LOW(s(s(y''''')), add(0, add(s(0), x''''''')))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

IF_LOW(false, s(0), add(s(s(x''''')), x'')) -> LOW(s(0), x'')

five new Dependency Pairs are created:

IF_LOW(false, s(0), add(s(s(x''''')), add(s(0), x'''))) -> LOW(s(0), add(s(0), x'''))
IF_LOW(false, s(0), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> LOW(s(0), add(s(s(x''''')), x'''))
IF_LOW(false, s(0), add(s(s(x''''')), add(0, add(0, x''''''')))) -> LOW(s(0), add(0, add(0, x''''''')))
IF_LOW(false, s(0), add(s(s(x''''')), add(0, add(s(0), x''''''')))) -> LOW(s(0), add(0, add(s(0), x''''''')))
IF_LOW(false, s(0), add(s(s(x''''')), add(0, add(s(s(x''''''''')), x''''''')))) -> LOW(s(0), add(0, add(s(s(x''''''''')), x''''''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

           →DP Problem 25

             ↳Nar

...

               →DP Problem 35

                 ↳Forward Instantiation Transformation

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pairs:

IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(0, add(s(s(x''''''''')), x''''''')))) -> LOW(s(s(y''''')), add(0, add(s(s(x''''''''')), x''''''')))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(0, add(s(0), x''''''')))) -> LOW(s(s(y''''')), add(0, add(s(0), x''''''')))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(0, add(0, x''''''')))) -> LOW(s(s(y''''')), add(0, add(0, x''''''')))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> LOW(s(s(y''''')), add(s(s(x''''')), x'''))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(s(0), x'''))) -> LOW(s(s(y''''')), add(s(0), x'''))
IF_LOW(true, s(0), add(s(0), add(0, add(s(s(x''''''''')), x''''''')))) -> LOW(s(0), add(0, add(s(s(x''''''''')), x''''''')))
IF_LOW(true, s(y'''''), add(s(0), add(0, add(s(0), x''''''')))) -> LOW(s(y'''''), add(0, add(s(0), x''''''')))
IF_LOW(true, s(y'''''), add(s(0), add(0, add(0, x''''''')))) -> LOW(s(y'''''), add(0, add(0, x''''''')))
IF_LOW(true, s(s(y''''')), add(s(0), add(s(s(x''''')), x'''))) -> LOW(s(s(y''''')), add(s(s(x''''')), x'''))
IF_LOW(false, s(0), add(s(s(x''''')), add(0, add(s(s(x''''''''')), x''''''')))) -> LOW(s(0), add(0, add(s(s(x''''''''')), x''''''')))
IF_LOW(false, s(0), add(s(s(x''''')), add(0, add(s(0), x''''''')))) -> LOW(s(0), add(0, add(s(0), x''''''')))
IF_LOW(true, s(0), add(0, add(s(s(x''''')), x'''))) -> LOW(s(0), add(s(s(x''''')), x'''))
LOW(s(0), add(0, add(s(s(x''''''')), x'''''))) -> IF_LOW(true, s(0), add(0, add(s(s(x''''''')), x''''')))
IF_LOW(true, s(y''''), add(0, add(s(0), x'''))) -> LOW(s(y''''), add(s(0), x'''))
LOW(s(y''''''), add(0, add(s(0), x'''''))) -> IF_LOW(true, s(y''''''), add(0, add(s(0), x''''')))
IF_LOW(false, 0, add(s(x''''), add(0, add(s(x''''''''), x'0'''')))) -> LOW(0, add(0, add(s(x''''''''), x'0'''')))
LOW(0, add(s(x'''), add(0, add(s(x''''''''''), x'0'''''')))) -> IF_LOW(false, 0, add(s(x'''), add(0, add(s(x''''''''''), x'0''''''))))
IF_LOW(false, 0, add(s(x''''), add(0, add(0, x''''''')))) -> LOW(0, add(0, add(0, x''''''')))
LOW(0, add(s(x'''), add(0, add(0, x''''''''')))) -> IF_LOW(false, 0, add(s(x'''), add(0, add(0, x'''''''''))))
IF_LOW(false, 0, add(s(x''''), add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
LOW(0, add(s(x'''), add(s(x'''''''), x'0''))) -> IF_LOW(false, 0, add(s(x'''), add(s(x'''''''), x'0'')))
IF_LOW(true, 0, add(0, add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
LOW(0, add(0, add(s(x''''''), x'0''))) -> IF_LOW(true, 0, add(0, add(s(x''''''), x'0'')))
IF_LOW(true, n''', add(0, add(0, x'''))) -> LOW(n''', add(0, x'''))
LOW(n'', add(0, add(0, x'''''))) -> IF_LOW(true, n'', add(0, add(0, x''''')))
IF_LOW(false, s(0), add(s(s(x''''')), add(0, add(0, x''''''')))) -> LOW(s(0), add(0, add(0, x''''''')))
IF_LOW(false, s(0), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> LOW(s(0), add(s(s(x''''')), x'''))
IF_LOW(false, s(0), add(s(s(x''''')), add(s(0), x'''))) -> LOW(s(0), add(s(0), x'''))
LOW(s(0), add(s(s(x''')), x)) -> IF_LOW(false, s(0), add(s(s(x''')), x))
IF_LOW(true, s(0), add(s(0), add(s(s(x''''')), x'''))) -> LOW(s(0), add(s(s(x''''')), x'''))
IF_LOW(true, s(y'''''), add(s(0), add(s(0), x'''))) -> LOW(s(y'''''), add(s(0), x'''))
LOW(s(y''), add(s(0), x)) -> IF_LOW(true, s(y''), add(s(0), x))
IF_LOW(false, s(s(y'''')), add(s(s(x''''')), x')) -> LOW(s(s(y'''')), x')
LOW(s(s(y'')), add(s(s(x''')), x)) -> IF_LOW(le(x''', y''), s(s(y'')), add(s(s(x''')), x))
IF_LOW(true, s(s(y'''')), add(0, add(s(s(x''''')), x'''))) -> LOW(s(s(y'''')), add(s(s(x''''')), x'''))
LOW(s(s(y'''''')), add(0, add(s(s(x''''''')), x'''''))) -> IF_LOW(true, s(s(y'''''')), add(0, add(s(s(x''''''')), x''''')))
IF_LOW(true, s(s(y'''''''')), add(s(0), add(0, add(s(s(x''''''''')), x''''''')))) -> LOW(s(s(y'''''''')), add(0, add(s(s(x''''''''')), x''''''')))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

IF_LOW(false, s(s(y'''')), add(s(s(x''''')), x')) -> LOW(s(s(y'''')), x')

five new Dependency Pairs are created:

IF_LOW(false, s(s(y''''')), add(s(s(x''''')), add(s(0), x'''))) -> LOW(s(s(y''''')), add(s(0), x'''))
IF_LOW(false, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> LOW(s(s(y''''')), add(s(s(x''''')), x'''))
IF_LOW(false, s(s(y''''')), add(s(s(x''''')), add(0, add(0, x''''''')))) -> LOW(s(s(y''''')), add(0, add(0, x''''''')))
IF_LOW(false, s(s(y''''')), add(s(s(x''''')), add(0, add(s(0), x''''''')))) -> LOW(s(s(y''''')), add(0, add(s(0), x''''''')))
IF_LOW(false, s(s(y''''')), add(s(s(x''''')), add(0, add(s(s(x''''''''')), x''''''')))) -> LOW(s(s(y''''')), add(0, add(s(s(x''''''''')), x''''''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

           →DP Problem 25

             ↳Nar

...

               →DP Problem 36

                 ↳Polynomial Ordering

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pairs:

IF_LOW(false, s(s(y''''')), add(s(s(x''''')), add(0, add(s(s(x''''''''')), x''''''')))) -> LOW(s(s(y''''')), add(0, add(s(s(x''''''''')), x''''''')))
IF_LOW(false, s(s(y''''')), add(s(s(x''''')), add(0, add(s(0), x''''''')))) -> LOW(s(s(y''''')), add(0, add(s(0), x''''''')))
IF_LOW(false, s(s(y''''')), add(s(s(x''''')), add(0, add(0, x''''''')))) -> LOW(s(s(y''''')), add(0, add(0, x''''''')))
IF_LOW(false, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> LOW(s(s(y''''')), add(s(s(x''''')), x'''))
IF_LOW(false, s(s(y''''')), add(s(s(x''''')), add(s(0), x'''))) -> LOW(s(s(y''''')), add(s(0), x'''))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(0, add(s(0), x''''''')))) -> LOW(s(s(y''''')), add(0, add(s(0), x''''''')))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(0, add(0, x''''''')))) -> LOW(s(s(y''''')), add(0, add(0, x''''''')))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> LOW(s(s(y''''')), add(s(s(x''''')), x'''))
IF_LOW(true, s(s(y'''''''')), add(s(0), add(0, add(s(s(x''''''''')), x''''''')))) -> LOW(s(s(y'''''''')), add(0, add(s(s(x''''''''')), x''''''')))
IF_LOW(true, s(0), add(s(0), add(0, add(s(s(x''''''''')), x''''''')))) -> LOW(s(0), add(0, add(s(s(x''''''''')), x''''''')))
IF_LOW(true, s(y'''''), add(s(0), add(0, add(s(0), x''''''')))) -> LOW(s(y'''''), add(0, add(s(0), x''''''')))
IF_LOW(true, s(y'''''), add(s(0), add(0, add(0, x''''''')))) -> LOW(s(y'''''), add(0, add(0, x''''''')))
IF_LOW(true, s(s(y''''')), add(s(0), add(s(s(x''''')), x'''))) -> LOW(s(s(y''''')), add(s(s(x''''')), x'''))
IF_LOW(false, s(0), add(s(s(x''''')), add(0, add(s(s(x''''''''')), x''''''')))) -> LOW(s(0), add(0, add(s(s(x''''''''')), x''''''')))
IF_LOW(false, s(0), add(s(s(x''''')), add(0, add(s(0), x''''''')))) -> LOW(s(0), add(0, add(s(0), x''''''')))
IF_LOW(true, s(0), add(0, add(s(s(x''''')), x'''))) -> LOW(s(0), add(s(s(x''''')), x'''))
LOW(s(0), add(0, add(s(s(x''''''')), x'''''))) -> IF_LOW(true, s(0), add(0, add(s(s(x''''''')), x''''')))
IF_LOW(true, s(y''''), add(0, add(s(0), x'''))) -> LOW(s(y''''), add(s(0), x'''))
LOW(s(y''''''), add(0, add(s(0), x'''''))) -> IF_LOW(true, s(y''''''), add(0, add(s(0), x''''')))
IF_LOW(false, 0, add(s(x''''), add(0, add(s(x''''''''), x'0'''')))) -> LOW(0, add(0, add(s(x''''''''), x'0'''')))
LOW(0, add(s(x'''), add(0, add(s(x''''''''''), x'0'''''')))) -> IF_LOW(false, 0, add(s(x'''), add(0, add(s(x''''''''''), x'0''''''))))
IF_LOW(false, 0, add(s(x''''), add(0, add(0, x''''''')))) -> LOW(0, add(0, add(0, x''''''')))
LOW(0, add(s(x'''), add(0, add(0, x''''''''')))) -> IF_LOW(false, 0, add(s(x'''), add(0, add(0, x'''''''''))))
IF_LOW(false, 0, add(s(x''''), add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
LOW(0, add(s(x'''), add(s(x'''''''), x'0''))) -> IF_LOW(false, 0, add(s(x'''), add(s(x'''''''), x'0'')))
IF_LOW(true, 0, add(0, add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
LOW(0, add(0, add(s(x''''''), x'0''))) -> IF_LOW(true, 0, add(0, add(s(x''''''), x'0'')))
IF_LOW(true, n''', add(0, add(0, x'''))) -> LOW(n''', add(0, x'''))
LOW(n'', add(0, add(0, x'''''))) -> IF_LOW(true, n'', add(0, add(0, x''''')))
IF_LOW(false, s(0), add(s(s(x''''')), add(0, add(0, x''''''')))) -> LOW(s(0), add(0, add(0, x''''''')))
IF_LOW(false, s(0), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> LOW(s(0), add(s(s(x''''')), x'''))
IF_LOW(false, s(0), add(s(s(x''''')), add(s(0), x'''))) -> LOW(s(0), add(s(0), x'''))
LOW(s(0), add(s(s(x''')), x)) -> IF_LOW(false, s(0), add(s(s(x''')), x))
IF_LOW(true, s(0), add(s(0), add(s(s(x''''')), x'''))) -> LOW(s(0), add(s(s(x''''')), x'''))
IF_LOW(true, s(y'''''), add(s(0), add(s(0), x'''))) -> LOW(s(y'''''), add(s(0), x'''))
LOW(s(y''), add(s(0), x)) -> IF_LOW(true, s(y''), add(s(0), x))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(s(0), x'''))) -> LOW(s(s(y''''')), add(s(0), x'''))
LOW(s(s(y'')), add(s(s(x''')), x)) -> IF_LOW(le(x''', y''), s(s(y'')), add(s(s(x''')), x))
IF_LOW(true, s(s(y'''')), add(0, add(s(s(x''''')), x'''))) -> LOW(s(s(y'''')), add(s(s(x''''')), x'''))
LOW(s(s(y'''''')), add(0, add(s(s(x''''''')), x'''''))) -> IF_LOW(true, s(s(y'''''')), add(0, add(s(s(x''''''')), x''''')))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(0, add(s(s(x''''''''')), x''''''')))) -> LOW(s(s(y''''')), add(0, add(s(s(x''''''''')), x''''''')))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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_LOW(true, s(0), add(0, add(s(s(x''''')), x'''))) -> LOW(s(0), add(s(s(x''''')), x'''))
IF_LOW(true, s(y''''), add(0, add(s(0), x'''))) -> LOW(s(y''''), add(s(0), x'''))
IF_LOW(true, 0, add(0, add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
IF_LOW(true, n''', add(0, add(0, x'''))) -> LOW(n''', add(0, x'''))
IF_LOW(true, s(s(y'''')), add(0, add(s(s(x''''')), x'''))) -> LOW(s(s(y'''')), add(s(s(x''''')), x'''))

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

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(0) = 1

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

POL(false) = 0

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

POL(true) = 0

POL(s(x₁)) = 0

POL(le(x₁, x₂)) = 0

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

           →DP Problem 25

             ↳Nar

...

               →DP Problem 37

                 ↳Dependency Graph

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pairs:

IF_LOW(false, s(s(y''''')), add(s(s(x''''')), add(0, add(s(s(x''''''''')), x''''''')))) -> LOW(s(s(y''''')), add(0, add(s(s(x''''''''')), x''''''')))
IF_LOW(false, s(s(y''''')), add(s(s(x''''')), add(0, add(s(0), x''''''')))) -> LOW(s(s(y''''')), add(0, add(s(0), x''''''')))
IF_LOW(false, s(s(y''''')), add(s(s(x''''')), add(0, add(0, x''''''')))) -> LOW(s(s(y''''')), add(0, add(0, x''''''')))
IF_LOW(false, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> LOW(s(s(y''''')), add(s(s(x''''')), x'''))
IF_LOW(false, s(s(y''''')), add(s(s(x''''')), add(s(0), x'''))) -> LOW(s(s(y''''')), add(s(0), x'''))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(0, add(s(0), x''''''')))) -> LOW(s(s(y''''')), add(0, add(s(0), x''''''')))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(0, add(0, x''''''')))) -> LOW(s(s(y''''')), add(0, add(0, x''''''')))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> LOW(s(s(y''''')), add(s(s(x''''')), x'''))
IF_LOW(true, s(s(y'''''''')), add(s(0), add(0, add(s(s(x''''''''')), x''''''')))) -> LOW(s(s(y'''''''')), add(0, add(s(s(x''''''''')), x''''''')))
IF_LOW(true, s(0), add(s(0), add(0, add(s(s(x''''''''')), x''''''')))) -> LOW(s(0), add(0, add(s(s(x''''''''')), x''''''')))
IF_LOW(true, s(y'''''), add(s(0), add(0, add(s(0), x''''''')))) -> LOW(s(y'''''), add(0, add(s(0), x''''''')))
IF_LOW(true, s(y'''''), add(s(0), add(0, add(0, x''''''')))) -> LOW(s(y'''''), add(0, add(0, x''''''')))
IF_LOW(true, s(s(y''''')), add(s(0), add(s(s(x''''')), x'''))) -> LOW(s(s(y''''')), add(s(s(x''''')), x'''))
IF_LOW(false, s(0), add(s(s(x''''')), add(0, add(s(s(x''''''''')), x''''''')))) -> LOW(s(0), add(0, add(s(s(x''''''''')), x''''''')))
IF_LOW(false, s(0), add(s(s(x''''')), add(0, add(s(0), x''''''')))) -> LOW(s(0), add(0, add(s(0), x''''''')))
LOW(s(0), add(0, add(s(s(x''''''')), x'''''))) -> IF_LOW(true, s(0), add(0, add(s(s(x''''''')), x''''')))
LOW(s(y''''''), add(0, add(s(0), x'''''))) -> IF_LOW(true, s(y''''''), add(0, add(s(0), x''''')))
IF_LOW(false, 0, add(s(x''''), add(0, add(s(x''''''''), x'0'''')))) -> LOW(0, add(0, add(s(x''''''''), x'0'''')))
LOW(0, add(s(x'''), add(0, add(s(x''''''''''), x'0'''''')))) -> IF_LOW(false, 0, add(s(x'''), add(0, add(s(x''''''''''), x'0''''''))))
IF_LOW(false, 0, add(s(x''''), add(0, add(0, x''''''')))) -> LOW(0, add(0, add(0, x''''''')))
LOW(0, add(s(x'''), add(0, add(0, x''''''''')))) -> IF_LOW(false, 0, add(s(x'''), add(0, add(0, x'''''''''))))
IF_LOW(false, 0, add(s(x''''), add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
LOW(0, add(s(x'''), add(s(x'''''''), x'0''))) -> IF_LOW(false, 0, add(s(x'''), add(s(x'''''''), x'0'')))
LOW(0, add(0, add(s(x''''''), x'0''))) -> IF_LOW(true, 0, add(0, add(s(x''''''), x'0'')))
LOW(n'', add(0, add(0, x'''''))) -> IF_LOW(true, n'', add(0, add(0, x''''')))
IF_LOW(false, s(0), add(s(s(x''''')), add(0, add(0, x''''''')))) -> LOW(s(0), add(0, add(0, x''''''')))
IF_LOW(false, s(0), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> LOW(s(0), add(s(s(x''''')), x'''))
IF_LOW(false, s(0), add(s(s(x''''')), add(s(0), x'''))) -> LOW(s(0), add(s(0), x'''))
LOW(s(0), add(s(s(x''')), x)) -> IF_LOW(false, s(0), add(s(s(x''')), x))
IF_LOW(true, s(0), add(s(0), add(s(s(x''''')), x'''))) -> LOW(s(0), add(s(s(x''''')), x'''))
IF_LOW(true, s(y'''''), add(s(0), add(s(0), x'''))) -> LOW(s(y'''''), add(s(0), x'''))
LOW(s(y''), add(s(0), x)) -> IF_LOW(true, s(y''), add(s(0), x))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(s(0), x'''))) -> LOW(s(s(y''''')), add(s(0), x'''))
LOW(s(s(y'')), add(s(s(x''')), x)) -> IF_LOW(le(x''', y''), s(s(y'')), add(s(s(x''')), x))
LOW(s(s(y'''''')), add(0, add(s(s(x''''''')), x'''''))) -> IF_LOW(true, s(s(y'''''')), add(0, add(s(s(x''''''')), x''''')))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(0, add(s(s(x''''''''')), x''''''')))) -> LOW(s(s(y''''')), add(0, add(s(s(x''''''''')), x''''''')))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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 the DP problem was split into 2 DP problems.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

           →DP Problem 25

             ↳Nar

...

               →DP Problem 38

                 ↳Polynomial Ordering

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pairs:

IF_LOW(false, s(s(y''''')), add(s(s(x''''')), add(s(0), x'''))) -> LOW(s(s(y''''')), add(s(0), x'''))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> LOW(s(s(y''''')), add(s(s(x''''')), x'''))
IF_LOW(true, s(s(y''''')), add(s(0), add(s(s(x''''')), x'''))) -> LOW(s(s(y''''')), add(s(s(x''''')), x'''))
IF_LOW(false, s(0), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> LOW(s(0), add(s(s(x''''')), x'''))
IF_LOW(false, s(0), add(s(s(x''''')), add(s(0), x'''))) -> LOW(s(0), add(s(0), x'''))
LOW(s(0), add(s(s(x''')), x)) -> IF_LOW(false, s(0), add(s(s(x''')), x))
IF_LOW(true, s(0), add(s(0), add(s(s(x''''')), x'''))) -> LOW(s(0), add(s(s(x''''')), x'''))
IF_LOW(true, s(y'''''), add(s(0), add(s(0), x'''))) -> LOW(s(y'''''), add(s(0), x'''))
LOW(s(y''), add(s(0), x)) -> IF_LOW(true, s(y''), add(s(0), x))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(s(0), x'''))) -> LOW(s(s(y''''')), add(s(0), x'''))
LOW(s(s(y'')), add(s(s(x''')), x)) -> IF_LOW(le(x''', y''), s(s(y'')), add(s(s(x''')), x))
IF_LOW(false, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> LOW(s(s(y''''')), add(s(s(x''''')), x'''))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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_LOW(true, s(s(y''''')), add(s(0), add(s(s(x''''')), x'''))) -> LOW(s(s(y''''')), add(s(s(x''''')), x'''))
IF_LOW(true, s(0), add(s(0), add(s(s(x''''')), x'''))) -> LOW(s(0), add(s(s(x''''')), x'''))
IF_LOW(true, s(y'''''), add(s(0), add(s(0), x'''))) -> LOW(s(y'''''), add(s(0), x'''))

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

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(0) = 1

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

POL(false) = 0

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

POL(true) = 0

POL(s(x₁)) = x₁

POL(le(x₁, x₂)) = 0

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

           →DP Problem 25

             ↳Nar

...

               →DP Problem 40

                 ↳Dependency Graph

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pairs:

IF_LOW(false, s(s(y''''')), add(s(s(x''''')), add(s(0), x'''))) -> LOW(s(s(y''''')), add(s(0), x'''))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> LOW(s(s(y''''')), add(s(s(x''''')), x'''))
IF_LOW(false, s(0), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> LOW(s(0), add(s(s(x''''')), x'''))
IF_LOW(false, s(0), add(s(s(x''''')), add(s(0), x'''))) -> LOW(s(0), add(s(0), x'''))
LOW(s(0), add(s(s(x''')), x)) -> IF_LOW(false, s(0), add(s(s(x''')), x))
LOW(s(y''), add(s(0), x)) -> IF_LOW(true, s(y''), add(s(0), x))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(s(0), x'''))) -> LOW(s(s(y''''')), add(s(0), x'''))
LOW(s(s(y'')), add(s(s(x''')), x)) -> IF_LOW(le(x''', y''), s(s(y'')), add(s(s(x''')), x))
IF_LOW(false, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> LOW(s(s(y''''')), add(s(s(x''''')), x'''))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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 the DP problem was split into 2 DP problems.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

           →DP Problem 25

             ↳Nar

...

               →DP Problem 42

                 ↳Polynomial Ordering

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pairs:

IF_LOW(false, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> LOW(s(s(y''''')), add(s(s(x''''')), x'''))
LOW(s(s(y'')), add(s(s(x''')), x)) -> IF_LOW(le(x''', y''), s(s(y'')), add(s(s(x''')), x))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> LOW(s(s(y''''')), add(s(s(x''''')), x'''))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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_LOW(false, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> LOW(s(s(y''''')), add(s(s(x''''')), x'''))
IF_LOW(true, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> LOW(s(s(y''''')), add(s(s(x''''')), x'''))

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

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(0) = 0

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

POL(false) = 0

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

POL(true) = 0

POL(s(x₁)) = 0

POL(le(x₁, x₂)) = 0

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

           →DP Problem 25

             ↳Nar

...

               →DP Problem 44

                 ↳Dependency Graph

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pair:

LOW(s(s(y'')), add(s(s(x''')), x)) -> IF_LOW(le(x''', y''), s(s(y'')), add(s(s(x''')), x))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

           →DP Problem 25

             ↳Nar

...

               →DP Problem 43

                 ↳Polynomial Ordering

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pairs:

LOW(s(0), add(s(s(x''')), x)) -> IF_LOW(false, s(0), add(s(s(x''')), x))
IF_LOW(false, s(0), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> LOW(s(0), add(s(s(x''''')), x'''))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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:

IF_LOW(false, s(0), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> LOW(s(0), add(s(s(x''''')), x'''))

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

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(0) = 0

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

POL(false) = 0

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

POL(s(x₁)) = 1

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

           →DP Problem 25

             ↳Nar

...

               →DP Problem 45

                 ↳Dependency Graph

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pair:

LOW(s(0), add(s(s(x''')), x)) -> IF_LOW(false, s(0), add(s(s(x''')), x))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

           →DP Problem 25

             ↳Nar

...

               →DP Problem 39

                 ↳Polynomial Ordering

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pairs:

LOW(0, add(s(x'''), add(s(x'''''''), x'0''))) -> IF_LOW(false, 0, add(s(x'''), add(s(x'''''''), x'0'')))
IF_LOW(false, 0, add(s(x''''), add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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:

IF_LOW(false, 0, add(s(x''''), add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))

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

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(0) = 0

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

POL(false) = 0

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

POL(s(x₁)) = 1

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

           →DP Problem 25

             ↳Nar

...

               →DP Problem 41

                 ↳Dependency Graph

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

Dependency Pair:

LOW(0, add(s(x'''), add(s(x'''''''), x'0''))) -> IF_LOW(false, 0, add(s(x'''), add(s(x'''''''), x'0'')))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Narrowing Transformation

       →DP Problem 7

         ↳Nar

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:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

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

three new Dependency Pairs are created:

HIGH(n', add(0, x)) -> IF_HIGH(true, n', add(0, x))
HIGH(0, add(s(x''), x)) -> IF_HIGH(false, 0, add(s(x''), x))
HIGH(s(y'), add(s(x''), x)) -> IF_HIGH(le(x'', y'), s(y'), add(s(x''), x))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

           →DP Problem 46

             ↳Narrowing Transformation

       →DP Problem 7

         ↳Nar

Dependency Pairs:

HIGH(s(y'), add(s(x''), x)) -> IF_HIGH(le(x'', y'), s(y'), add(s(x''), x))
HIGH(0, add(s(x''), x)) -> IF_HIGH(false, 0, add(s(x''), x))
IF_HIGH(true, n, add(m, x)) -> HIGH(n, x)
HIGH(n', add(0, x)) -> IF_HIGH(true, n', add(0, x))
IF_HIGH(false, n, add(m, x)) -> HIGH(n, x)

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

HIGH(s(y'), add(s(x''), x)) -> IF_HIGH(le(x'', y'), s(y'), add(s(x''), x))

three new Dependency Pairs are created:

HIGH(s(y''), add(s(0), x)) -> IF_HIGH(true, s(y''), add(s(0), x))
HIGH(s(0), add(s(s(x''')), x)) -> IF_HIGH(false, s(0), add(s(s(x''')), x))
HIGH(s(s(y'')), add(s(s(x''')), x)) -> IF_HIGH(le(x''', y''), s(s(y'')), add(s(s(x''')), x))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

           →DP Problem 46

             ↳Nar

...

               →DP Problem 47

                 ↳Instantiation Transformation

       →DP Problem 7

         ↳Nar

Dependency Pairs:

HIGH(s(s(y'')), add(s(s(x''')), x)) -> IF_HIGH(le(x''', y''), s(s(y'')), add(s(s(x''')), x))
HIGH(s(0), add(s(s(x''')), x)) -> IF_HIGH(false, s(0), add(s(s(x''')), x))
HIGH(s(y''), add(s(0), x)) -> IF_HIGH(true, s(y''), add(s(0), x))
IF_HIGH(true, n, add(m, x)) -> HIGH(n, x)
HIGH(n', add(0, x)) -> IF_HIGH(true, n', add(0, x))
IF_HIGH(false, n, add(m, x)) -> HIGH(n, x)
HIGH(0, add(s(x''), x)) -> IF_HIGH(false, 0, add(s(x''), x))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

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

three new Dependency Pairs are created:

IF_HIGH(true, n', add(0, x'')) -> HIGH(n', x'')
IF_HIGH(true, s(y''''), add(s(0), x'')) -> HIGH(s(y''''), x'')
IF_HIGH(true, s(s(y'''')), add(s(s(x''''')), x')) -> HIGH(s(s(y'''')), x')

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

           →DP Problem 46

             ↳Nar

...

               →DP Problem 48

                 ↳Instantiation Transformation

       →DP Problem 7

         ↳Nar

Dependency Pairs:

IF_HIGH(true, s(s(y'''')), add(s(s(x''''')), x')) -> HIGH(s(s(y'''')), x')
HIGH(s(0), add(s(s(x''')), x)) -> IF_HIGH(false, s(0), add(s(s(x''')), x))
IF_HIGH(true, s(y''''), add(s(0), x'')) -> HIGH(s(y''''), x'')
HIGH(s(y''), add(s(0), x)) -> IF_HIGH(true, s(y''), add(s(0), x))
HIGH(0, add(s(x''), x)) -> IF_HIGH(false, 0, add(s(x''), x))
IF_HIGH(true, n', add(0, x'')) -> HIGH(n', x'')
HIGH(n', add(0, x)) -> IF_HIGH(true, n', add(0, x))
IF_HIGH(false, n, add(m, x)) -> HIGH(n, x)
HIGH(s(s(y'')), add(s(s(x''')), x)) -> IF_HIGH(le(x''', y''), s(s(y'')), add(s(s(x''')), x))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

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

three new Dependency Pairs are created:

IF_HIGH(false, 0, add(s(x''''), x'')) -> HIGH(0, x'')
IF_HIGH(false, s(0), add(s(s(x''''')), x'')) -> HIGH(s(0), x'')
IF_HIGH(false, s(s(y'''')), add(s(s(x''''')), x')) -> HIGH(s(s(y'''')), x')

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

           →DP Problem 46

             ↳Nar

...

               →DP Problem 49

                 ↳Forward Instantiation Transformation

       →DP Problem 7

         ↳Nar

Dependency Pairs:

IF_HIGH(false, s(s(y'''')), add(s(s(x''''')), x')) -> HIGH(s(s(y'''')), x')
HIGH(s(s(y'')), add(s(s(x''')), x)) -> IF_HIGH(le(x''', y''), s(s(y'')), add(s(s(x''')), x))
IF_HIGH(false, s(0), add(s(s(x''''')), x'')) -> HIGH(s(0), x'')
HIGH(s(0), add(s(s(x''')), x)) -> IF_HIGH(false, s(0), add(s(s(x''')), x))
IF_HIGH(true, s(y''''), add(s(0), x'')) -> HIGH(s(y''''), x'')
HIGH(s(y''), add(s(0), x)) -> IF_HIGH(true, s(y''), add(s(0), x))
IF_HIGH(false, 0, add(s(x''''), x'')) -> HIGH(0, x'')
HIGH(0, add(s(x''), x)) -> IF_HIGH(false, 0, add(s(x''), x))
IF_HIGH(true, n', add(0, x'')) -> HIGH(n', x'')
HIGH(n', add(0, x)) -> IF_HIGH(true, n', add(0, x))
IF_HIGH(true, s(s(y'''')), add(s(s(x''''')), x')) -> HIGH(s(s(y'''')), x')

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

IF_HIGH(true, n', add(0, x'')) -> HIGH(n', x'')

five new Dependency Pairs are created:

IF_HIGH(true, n''', add(0, add(0, x'''))) -> HIGH(n''', add(0, x'''))
IF_HIGH(true, 0, add(0, add(s(x''''), x'0))) -> HIGH(0, add(s(x''''), x'0))
IF_HIGH(true, s(y''''), add(0, add(s(0), x'''))) -> HIGH(s(y''''), add(s(0), x'''))
IF_HIGH(true, s(0), add(0, add(s(s(x''''')), x'''))) -> HIGH(s(0), add(s(s(x''''')), x'''))
IF_HIGH(true, s(s(y'''')), add(0, add(s(s(x''''')), x'''))) -> HIGH(s(s(y'''')), add(s(s(x''''')), x'''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

           →DP Problem 46

             ↳Nar

...

               →DP Problem 50

                 ↳Forward Instantiation Transformation

       →DP Problem 7

         ↳Nar

Dependency Pairs:

IF_HIGH(true, s(s(y'''')), add(0, add(s(s(x''''')), x'''))) -> HIGH(s(s(y'''')), add(s(s(x''''')), x'''))
IF_HIGH(true, s(0), add(0, add(s(s(x''''')), x'''))) -> HIGH(s(0), add(s(s(x''''')), x'''))
IF_HIGH(true, s(s(y'''')), add(s(s(x''''')), x')) -> HIGH(s(s(y'''')), x')
HIGH(s(s(y'')), add(s(s(x''')), x)) -> IF_HIGH(le(x''', y''), s(s(y'')), add(s(s(x''')), x))
IF_HIGH(false, s(0), add(s(s(x''''')), x'')) -> HIGH(s(0), x'')
HIGH(s(0), add(s(s(x''')), x)) -> IF_HIGH(false, s(0), add(s(s(x''')), x))
IF_HIGH(true, s(y''''), add(s(0), x'')) -> HIGH(s(y''''), x'')
HIGH(s(y''), add(s(0), x)) -> IF_HIGH(true, s(y''), add(s(0), x))
IF_HIGH(true, s(y''''), add(0, add(s(0), x'''))) -> HIGH(s(y''''), add(s(0), x'''))
IF_HIGH(false, 0, add(s(x''''), x'')) -> HIGH(0, x'')
HIGH(0, add(s(x''), x)) -> IF_HIGH(false, 0, add(s(x''), x))
IF_HIGH(true, 0, add(0, add(s(x''''), x'0))) -> HIGH(0, add(s(x''''), x'0))
IF_HIGH(true, n''', add(0, add(0, x'''))) -> HIGH(n''', add(0, x'''))
HIGH(n', add(0, x)) -> IF_HIGH(true, n', add(0, x))
IF_HIGH(false, s(s(y'''')), add(s(s(x''''')), x')) -> HIGH(s(s(y'''')), x')

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

HIGH(n', add(0, x)) -> IF_HIGH(true, n', add(0, x))

five new Dependency Pairs are created:

HIGH(n'', add(0, add(0, x'''''))) -> IF_HIGH(true, n'', add(0, add(0, x''''')))
HIGH(0, add(0, add(s(x''''''), x'0''))) -> IF_HIGH(true, 0, add(0, add(s(x''''''), x'0'')))
HIGH(s(y''''''), add(0, add(s(0), x'''''))) -> IF_HIGH(true, s(y''''''), add(0, add(s(0), x''''')))
HIGH(s(0), add(0, add(s(s(x''''''')), x'''''))) -> IF_HIGH(true, s(0), add(0, add(s(s(x''''''')), x''''')))
HIGH(s(s(y'''''')), add(0, add(s(s(x''''''')), x'''''))) -> IF_HIGH(true, s(s(y'''''')), add(0, add(s(s(x''''''')), x''''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

           →DP Problem 46

             ↳Nar

...

               →DP Problem 51

                 ↳Forward Instantiation Transformation

       →DP Problem 7

         ↳Nar

Dependency Pairs:

IF_HIGH(false, s(s(y'''')), add(s(s(x''''')), x')) -> HIGH(s(s(y'''')), x')
HIGH(s(s(y'''''')), add(0, add(s(s(x''''''')), x'''''))) -> IF_HIGH(true, s(s(y'''''')), add(0, add(s(s(x''''''')), x''''')))
IF_HIGH(true, s(0), add(0, add(s(s(x''''')), x'''))) -> HIGH(s(0), add(s(s(x''''')), x'''))
HIGH(s(0), add(0, add(s(s(x''''''')), x'''''))) -> IF_HIGH(true, s(0), add(0, add(s(s(x''''''')), x''''')))
IF_HIGH(true, s(y''''), add(0, add(s(0), x'''))) -> HIGH(s(y''''), add(s(0), x'''))
HIGH(s(y''''''), add(0, add(s(0), x'''''))) -> IF_HIGH(true, s(y''''''), add(0, add(s(0), x''''')))
IF_HIGH(false, 0, add(s(x''''), x'')) -> HIGH(0, x'')
HIGH(0, add(s(x''), x)) -> IF_HIGH(false, 0, add(s(x''), x))
IF_HIGH(true, 0, add(0, add(s(x''''), x'0))) -> HIGH(0, add(s(x''''), x'0))
HIGH(0, add(0, add(s(x''''''), x'0''))) -> IF_HIGH(true, 0, add(0, add(s(x''''''), x'0'')))
IF_HIGH(true, n''', add(0, add(0, x'''))) -> HIGH(n''', add(0, x'''))
HIGH(n'', add(0, add(0, x'''''))) -> IF_HIGH(true, n'', add(0, add(0, x''''')))
IF_HIGH(false, s(0), add(s(s(x''''')), x'')) -> HIGH(s(0), x'')
HIGH(s(0), add(s(s(x''')), x)) -> IF_HIGH(false, s(0), add(s(s(x''')), x))
IF_HIGH(true, s(y''''), add(s(0), x'')) -> HIGH(s(y''''), x'')
HIGH(s(y''), add(s(0), x)) -> IF_HIGH(true, s(y''), add(s(0), x))
IF_HIGH(true, s(s(y'''')), add(s(s(x''''')), x')) -> HIGH(s(s(y'''')), x')
HIGH(s(s(y'')), add(s(s(x''')), x)) -> IF_HIGH(le(x''', y''), s(s(y'')), add(s(s(x''')), x))
IF_HIGH(true, s(s(y'''')), add(0, add(s(s(x''''')), x'''))) -> HIGH(s(s(y'''')), add(s(s(x''''')), x'''))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

IF_HIGH(true, s(y''''), add(s(0), x'')) -> HIGH(s(y''''), x'')

seven new Dependency Pairs are created:

IF_HIGH(true, s(y'''''), add(s(0), add(s(0), x'''))) -> HIGH(s(y'''''), add(s(0), x'''))
IF_HIGH(true, s(0), add(s(0), add(s(s(x''''')), x'''))) -> HIGH(s(0), add(s(s(x''''')), x'''))
IF_HIGH(true, s(s(y''''')), add(s(0), add(s(s(x''''')), x'''))) -> HIGH(s(s(y''''')), add(s(s(x''''')), x'''))
IF_HIGH(true, s(y'''''), add(s(0), add(0, add(0, x''''''')))) -> HIGH(s(y'''''), add(0, add(0, x''''''')))
IF_HIGH(true, s(y'''''), add(s(0), add(0, add(s(0), x''''''')))) -> HIGH(s(y'''''), add(0, add(s(0), x''''''')))
IF_HIGH(true, s(0), add(s(0), add(0, add(s(s(x''''''''')), x''''''')))) -> HIGH(s(0), add(0, add(s(s(x''''''''')), x''''''')))
IF_HIGH(true, s(s(y'''''''')), add(s(0), add(0, add(s(s(x''''''''')), x''''''')))) -> HIGH(s(s(y'''''''')), add(0, add(s(s(x''''''''')), x''''''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

           →DP Problem 46

             ↳Nar

...

               →DP Problem 52

                 ↳Forward Instantiation Transformation

       →DP Problem 7

         ↳Nar

Dependency Pairs:

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

IF_HIGH(true, s(s(y'''')), add(s(s(x''''')), x')) -> HIGH(s(s(y'''')), x')

five new Dependency Pairs are created:

IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(s(0), x'''))) -> HIGH(s(s(y''''')), add(s(0), x'''))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> HIGH(s(s(y''''')), add(s(s(x''''')), x'''))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(0, add(0, x''''''')))) -> HIGH(s(s(y''''')), add(0, add(0, x''''''')))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(0, add(s(0), x''''''')))) -> HIGH(s(s(y''''')), add(0, add(s(0), x''''''')))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(0, add(s(s(x''''''''')), x''''''')))) -> HIGH(s(s(y''''')), add(0, add(s(s(x''''''''')), x''''''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

           →DP Problem 46

             ↳Nar

...

               →DP Problem 53

                 ↳Forward Instantiation Transformation

       →DP Problem 7

         ↳Nar

Dependency Pairs:

IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(0, add(s(s(x''''''''')), x''''''')))) -> HIGH(s(s(y''''')), add(0, add(s(s(x''''''''')), x''''''')))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(0, add(s(0), x''''''')))) -> HIGH(s(s(y''''')), add(0, add(s(0), x''''''')))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(0, add(0, x''''''')))) -> HIGH(s(s(y''''')), add(0, add(0, x''''''')))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> HIGH(s(s(y''''')), add(s(s(x''''')), x'''))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(s(0), x'''))) -> HIGH(s(s(y''''')), add(s(0), x'''))
IF_HIGH(true, s(0), add(s(0), add(0, add(s(s(x''''''''')), x''''''')))) -> HIGH(s(0), add(0, add(s(s(x''''''''')), x''''''')))
IF_HIGH(true, s(y'''''), add(s(0), add(0, add(s(0), x''''''')))) -> HIGH(s(y'''''), add(0, add(s(0), x''''''')))
IF_HIGH(true, s(y'''''), add(s(0), add(0, add(0, x''''''')))) -> HIGH(s(y'''''), add(0, add(0, x''''''')))
IF_HIGH(true, s(s(y''''')), add(s(0), add(s(s(x''''')), x'''))) -> HIGH(s(s(y''''')), add(s(s(x''''')), x'''))
IF_HIGH(true, s(0), add(0, add(s(s(x''''')), x'''))) -> HIGH(s(0), add(s(s(x''''')), x'''))
HIGH(s(0), add(0, add(s(s(x''''''')), x'''''))) -> IF_HIGH(true, s(0), add(0, add(s(s(x''''''')), x''''')))
IF_HIGH(true, s(y''''), add(0, add(s(0), x'''))) -> HIGH(s(y''''), add(s(0), x'''))
HIGH(s(y''''''), add(0, add(s(0), x'''''))) -> IF_HIGH(true, s(y''''''), add(0, add(s(0), x''''')))
IF_HIGH(false, 0, add(s(x''''), x'')) -> HIGH(0, x'')
HIGH(0, add(s(x''), x)) -> IF_HIGH(false, 0, add(s(x''), x))
IF_HIGH(true, 0, add(0, add(s(x''''), x'0))) -> HIGH(0, add(s(x''''), x'0))
HIGH(0, add(0, add(s(x''''''), x'0''))) -> IF_HIGH(true, 0, add(0, add(s(x''''''), x'0'')))
IF_HIGH(true, n''', add(0, add(0, x'''))) -> HIGH(n''', add(0, x'''))
HIGH(n'', add(0, add(0, x'''''))) -> IF_HIGH(true, n'', add(0, add(0, x''''')))
IF_HIGH(false, s(0), add(s(s(x''''')), x'')) -> HIGH(s(0), x'')
HIGH(s(0), add(s(s(x''')), x)) -> IF_HIGH(false, s(0), add(s(s(x''')), x))
IF_HIGH(true, s(0), add(s(0), add(s(s(x''''')), x'''))) -> HIGH(s(0), add(s(s(x''''')), x'''))
IF_HIGH(true, s(y'''''), add(s(0), add(s(0), x'''))) -> HIGH(s(y'''''), add(s(0), x'''))
HIGH(s(y''), add(s(0), x)) -> IF_HIGH(true, s(y''), add(s(0), x))
IF_HIGH(false, s(s(y'''')), add(s(s(x''''')), x')) -> HIGH(s(s(y'''')), x')
HIGH(s(s(y'')), add(s(s(x''')), x)) -> IF_HIGH(le(x''', y''), s(s(y'')), add(s(s(x''')), x))
IF_HIGH(true, s(s(y'''')), add(0, add(s(s(x''''')), x'''))) -> HIGH(s(s(y'''')), add(s(s(x''''')), x'''))
HIGH(s(s(y'''''')), add(0, add(s(s(x''''''')), x'''''))) -> IF_HIGH(true, s(s(y'''''')), add(0, add(s(s(x''''''')), x''''')))
IF_HIGH(true, s(s(y'''''''')), add(s(0), add(0, add(s(s(x''''''''')), x''''''')))) -> HIGH(s(s(y'''''''')), add(0, add(s(s(x''''''''')), x''''''')))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

IF_HIGH(false, 0, add(s(x''''), x'')) -> HIGH(0, x'')

three new Dependency Pairs are created:

IF_HIGH(false, 0, add(s(x''''), add(s(x''''), x'0))) -> HIGH(0, add(s(x''''), x'0))
IF_HIGH(false, 0, add(s(x''''), add(0, add(0, x''''''')))) -> HIGH(0, add(0, add(0, x''''''')))
IF_HIGH(false, 0, add(s(x''''), add(0, add(s(x''''''''), x'0'''')))) -> HIGH(0, add(0, add(s(x''''''''), x'0'''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

           →DP Problem 46

             ↳Nar

...

               →DP Problem 54

                 ↳Forward Instantiation Transformation

       →DP Problem 7

         ↳Nar

Dependency Pairs:

IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(0, add(s(0), x''''''')))) -> HIGH(s(s(y''''')), add(0, add(s(0), x''''''')))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(0, add(0, x''''''')))) -> HIGH(s(s(y''''')), add(0, add(0, x''''''')))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> HIGH(s(s(y''''')), add(s(s(x''''')), x'''))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(s(0), x'''))) -> HIGH(s(s(y''''')), add(s(0), x'''))
IF_HIGH(true, s(s(y'''''''')), add(s(0), add(0, add(s(s(x''''''''')), x''''''')))) -> HIGH(s(s(y'''''''')), add(0, add(s(s(x''''''''')), x''''''')))
IF_HIGH(true, s(0), add(s(0), add(0, add(s(s(x''''''''')), x''''''')))) -> HIGH(s(0), add(0, add(s(s(x''''''''')), x''''''')))
IF_HIGH(true, s(y'''''), add(s(0), add(0, add(s(0), x''''''')))) -> HIGH(s(y'''''), add(0, add(s(0), x''''''')))
IF_HIGH(true, s(y'''''), add(s(0), add(0, add(0, x''''''')))) -> HIGH(s(y'''''), add(0, add(0, x''''''')))
IF_HIGH(true, s(s(y''''')), add(s(0), add(s(s(x''''')), x'''))) -> HIGH(s(s(y''''')), add(s(s(x''''')), x'''))
IF_HIGH(true, s(0), add(0, add(s(s(x''''')), x'''))) -> HIGH(s(0), add(s(s(x''''')), x'''))
HIGH(s(0), add(0, add(s(s(x''''''')), x'''''))) -> IF_HIGH(true, s(0), add(0, add(s(s(x''''''')), x''''')))
IF_HIGH(true, s(y''''), add(0, add(s(0), x'''))) -> HIGH(s(y''''), add(s(0), x'''))
HIGH(s(y''''''), add(0, add(s(0), x'''''))) -> IF_HIGH(true, s(y''''''), add(0, add(s(0), x''''')))
IF_HIGH(false, 0, add(s(x''''), add(0, add(s(x''''''''), x'0'''')))) -> HIGH(0, add(0, add(s(x''''''''), x'0'''')))
IF_HIGH(false, 0, add(s(x''''), add(0, add(0, x''''''')))) -> HIGH(0, add(0, add(0, x''''''')))
IF_HIGH(false, 0, add(s(x''''), add(s(x''''), x'0))) -> HIGH(0, add(s(x''''), x'0))
HIGH(0, add(s(x''), x)) -> IF_HIGH(false, 0, add(s(x''), x))
IF_HIGH(true, 0, add(0, add(s(x''''), x'0))) -> HIGH(0, add(s(x''''), x'0))
HIGH(0, add(0, add(s(x''''''), x'0''))) -> IF_HIGH(true, 0, add(0, add(s(x''''''), x'0'')))
IF_HIGH(true, n''', add(0, add(0, x'''))) -> HIGH(n''', add(0, x'''))
HIGH(n'', add(0, add(0, x'''''))) -> IF_HIGH(true, n'', add(0, add(0, x''''')))
IF_HIGH(false, s(0), add(s(s(x''''')), x'')) -> HIGH(s(0), x'')
HIGH(s(0), add(s(s(x''')), x)) -> IF_HIGH(false, s(0), add(s(s(x''')), x))
IF_HIGH(true, s(0), add(s(0), add(s(s(x''''')), x'''))) -> HIGH(s(0), add(s(s(x''''')), x'''))
IF_HIGH(true, s(y'''''), add(s(0), add(s(0), x'''))) -> HIGH(s(y'''''), add(s(0), x'''))
HIGH(s(y''), add(s(0), x)) -> IF_HIGH(true, s(y''), add(s(0), x))
IF_HIGH(false, s(s(y'''')), add(s(s(x''''')), x')) -> HIGH(s(s(y'''')), x')
HIGH(s(s(y'')), add(s(s(x''')), x)) -> IF_HIGH(le(x''', y''), s(s(y'')), add(s(s(x''')), x))
IF_HIGH(true, s(s(y'''')), add(0, add(s(s(x''''')), x'''))) -> HIGH(s(s(y'''')), add(s(s(x''''')), x'''))
HIGH(s(s(y'''''')), add(0, add(s(s(x''''''')), x'''''))) -> IF_HIGH(true, s(s(y'''''')), add(0, add(s(s(x''''''')), x''''')))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(0, add(s(s(x''''''''')), x''''''')))) -> HIGH(s(s(y''''')), add(0, add(s(s(x''''''''')), x''''''')))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

HIGH(0, add(s(x''), x)) -> IF_HIGH(false, 0, add(s(x''), x))

three new Dependency Pairs are created:

HIGH(0, add(s(x'''), add(s(x'''''''), x'0''))) -> IF_HIGH(false, 0, add(s(x'''), add(s(x'''''''), x'0'')))
HIGH(0, add(s(x'''), add(0, add(0, x''''''''')))) -> IF_HIGH(false, 0, add(s(x'''), add(0, add(0, x'''''''''))))
HIGH(0, add(s(x'''), add(0, add(s(x''''''''''), x'0'''''')))) -> IF_HIGH(false, 0, add(s(x'''), add(0, add(s(x''''''''''), x'0''''''))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

           →DP Problem 46

             ↳Nar

...

               →DP Problem 55

                 ↳Forward Instantiation Transformation

       →DP Problem 7

         ↳Nar

Dependency Pairs:

IF_HIGH(true, s(s(y'''''''')), add(s(0), add(0, add(s(s(x''''''''')), x''''''')))) -> HIGH(s(s(y'''''''')), add(0, add(s(s(x''''''''')), x''''''')))
IF_HIGH(true, s(0), add(s(0), add(0, add(s(s(x''''''''')), x''''''')))) -> HIGH(s(0), add(0, add(s(s(x''''''''')), x''''''')))
IF_HIGH(true, s(y'''''), add(s(0), add(0, add(s(0), x''''''')))) -> HIGH(s(y'''''), add(0, add(s(0), x''''''')))
IF_HIGH(true, s(y'''''), add(s(0), add(0, add(0, x''''''')))) -> HIGH(s(y'''''), add(0, add(0, x''''''')))
IF_HIGH(true, s(s(y''''')), add(s(0), add(s(s(x''''')), x'''))) -> HIGH(s(s(y''''')), add(s(s(x''''')), x'''))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(0, add(s(s(x''''''''')), x''''''')))) -> HIGH(s(s(y''''')), add(0, add(s(s(x''''''''')), x''''''')))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(0, add(0, x''''''')))) -> HIGH(s(s(y''''')), add(0, add(0, x''''''')))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> HIGH(s(s(y''''')), add(s(s(x''''')), x'''))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(s(0), x'''))) -> HIGH(s(s(y''''')), add(s(0), x'''))
IF_HIGH(false, s(s(y'''')), add(s(s(x''''')), x')) -> HIGH(s(s(y'''')), x')
HIGH(s(s(y'')), add(s(s(x''')), x)) -> IF_HIGH(le(x''', y''), s(s(y'')), add(s(s(x''')), x))
IF_HIGH(true, s(s(y'''')), add(0, add(s(s(x''''')), x'''))) -> HIGH(s(s(y'''')), add(s(s(x''''')), x'''))
HIGH(s(s(y'''''')), add(0, add(s(s(x''''''')), x'''''))) -> IF_HIGH(true, s(s(y'''''')), add(0, add(s(s(x''''''')), x''''')))
IF_HIGH(true, s(0), add(0, add(s(s(x''''')), x'''))) -> HIGH(s(0), add(s(s(x''''')), x'''))
HIGH(s(0), add(0, add(s(s(x''''''')), x'''''))) -> IF_HIGH(true, s(0), add(0, add(s(s(x''''''')), x''''')))
IF_HIGH(false, 0, add(s(x''''), add(0, add(s(x''''''''), x'0'''')))) -> HIGH(0, add(0, add(s(x''''''''), x'0'''')))
HIGH(0, add(s(x'''), add(0, add(s(x''''''''''), x'0'''''')))) -> IF_HIGH(false, 0, add(s(x'''), add(0, add(s(x''''''''''), x'0''''''))))
IF_HIGH(false, 0, add(s(x''''), add(0, add(0, x''''''')))) -> HIGH(0, add(0, add(0, x''''''')))
HIGH(0, add(s(x'''), add(0, add(0, x''''''''')))) -> IF_HIGH(false, 0, add(s(x'''), add(0, add(0, x'''''''''))))
IF_HIGH(false, 0, add(s(x''''), add(s(x''''), x'0))) -> HIGH(0, add(s(x''''), x'0))
HIGH(0, add(s(x'''), add(s(x'''''''), x'0''))) -> IF_HIGH(false, 0, add(s(x'''), add(s(x'''''''), x'0'')))
IF_HIGH(true, 0, add(0, add(s(x''''), x'0))) -> HIGH(0, add(s(x''''), x'0))
HIGH(0, add(0, add(s(x''''''), x'0''))) -> IF_HIGH(true, 0, add(0, add(s(x''''''), x'0'')))
IF_HIGH(true, n''', add(0, add(0, x'''))) -> HIGH(n''', add(0, x'''))
HIGH(n'', add(0, add(0, x'''''))) -> IF_HIGH(true, n'', add(0, add(0, x''''')))
IF_HIGH(false, s(0), add(s(s(x''''')), x'')) -> HIGH(s(0), x'')
HIGH(s(0), add(s(s(x''')), x)) -> IF_HIGH(false, s(0), add(s(s(x''')), x))
IF_HIGH(true, s(0), add(s(0), add(s(s(x''''')), x'''))) -> HIGH(s(0), add(s(s(x''''')), x'''))
IF_HIGH(true, s(y'''''), add(s(0), add(s(0), x'''))) -> HIGH(s(y'''''), add(s(0), x'''))
HIGH(s(y''), add(s(0), x)) -> IF_HIGH(true, s(y''), add(s(0), x))
IF_HIGH(true, s(y''''), add(0, add(s(0), x'''))) -> HIGH(s(y''''), add(s(0), x'''))
HIGH(s(y''''''), add(0, add(s(0), x'''''))) -> IF_HIGH(true, s(y''''''), add(0, add(s(0), x''''')))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(0, add(s(0), x''''''')))) -> HIGH(s(s(y''''')), add(0, add(s(0), x''''''')))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

IF_HIGH(false, s(0), add(s(s(x''''')), x'')) -> HIGH(s(0), x'')

five new Dependency Pairs are created:

IF_HIGH(false, s(0), add(s(s(x''''')), add(s(0), x'''))) -> HIGH(s(0), add(s(0), x'''))
IF_HIGH(false, s(0), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> HIGH(s(0), add(s(s(x''''')), x'''))
IF_HIGH(false, s(0), add(s(s(x''''')), add(0, add(0, x''''''')))) -> HIGH(s(0), add(0, add(0, x''''''')))
IF_HIGH(false, s(0), add(s(s(x''''')), add(0, add(s(0), x''''''')))) -> HIGH(s(0), add(0, add(s(0), x''''''')))
IF_HIGH(false, s(0), add(s(s(x''''')), add(0, add(s(s(x''''''''')), x''''''')))) -> HIGH(s(0), add(0, add(s(s(x''''''''')), x''''''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

           →DP Problem 46

             ↳Nar

...

               →DP Problem 56

                 ↳Forward Instantiation Transformation

       →DP Problem 7

         ↳Nar

Dependency Pairs:

IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(0, add(s(s(x''''''''')), x''''''')))) -> HIGH(s(s(y''''')), add(0, add(s(s(x''''''''')), x''''''')))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(0, add(s(0), x''''''')))) -> HIGH(s(s(y''''')), add(0, add(s(0), x''''''')))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(0, add(0, x''''''')))) -> HIGH(s(s(y''''')), add(0, add(0, x''''''')))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> HIGH(s(s(y''''')), add(s(s(x''''')), x'''))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(s(0), x'''))) -> HIGH(s(s(y''''')), add(s(0), x'''))
IF_HIGH(true, s(0), add(s(0), add(0, add(s(s(x''''''''')), x''''''')))) -> HIGH(s(0), add(0, add(s(s(x''''''''')), x''''''')))
IF_HIGH(true, s(y'''''), add(s(0), add(0, add(s(0), x''''''')))) -> HIGH(s(y'''''), add(0, add(s(0), x''''''')))
IF_HIGH(true, s(y'''''), add(s(0), add(0, add(0, x''''''')))) -> HIGH(s(y'''''), add(0, add(0, x''''''')))
IF_HIGH(true, s(s(y''''')), add(s(0), add(s(s(x''''')), x'''))) -> HIGH(s(s(y''''')), add(s(s(x''''')), x'''))
IF_HIGH(false, s(0), add(s(s(x''''')), add(0, add(s(s(x''''''''')), x''''''')))) -> HIGH(s(0), add(0, add(s(s(x''''''''')), x''''''')))
IF_HIGH(false, s(0), add(s(s(x''''')), add(0, add(s(0), x''''''')))) -> HIGH(s(0), add(0, add(s(0), x''''''')))
IF_HIGH(true, s(0), add(0, add(s(s(x''''')), x'''))) -> HIGH(s(0), add(s(s(x''''')), x'''))
HIGH(s(0), add(0, add(s(s(x''''''')), x'''''))) -> IF_HIGH(true, s(0), add(0, add(s(s(x''''''')), x''''')))
IF_HIGH(true, s(y''''), add(0, add(s(0), x'''))) -> HIGH(s(y''''), add(s(0), x'''))
HIGH(s(y''''''), add(0, add(s(0), x'''''))) -> IF_HIGH(true, s(y''''''), add(0, add(s(0), x''''')))
IF_HIGH(false, 0, add(s(x''''), add(0, add(s(x''''''''), x'0'''')))) -> HIGH(0, add(0, add(s(x''''''''), x'0'''')))
HIGH(0, add(s(x'''), add(0, add(s(x''''''''''), x'0'''''')))) -> IF_HIGH(false, 0, add(s(x'''), add(0, add(s(x''''''''''), x'0''''''))))
IF_HIGH(false, 0, add(s(x''''), add(0, add(0, x''''''')))) -> HIGH(0, add(0, add(0, x''''''')))
HIGH(0, add(s(x'''), add(0, add(0, x''''''''')))) -> IF_HIGH(false, 0, add(s(x'''), add(0, add(0, x'''''''''))))
IF_HIGH(false, 0, add(s(x''''), add(s(x''''), x'0))) -> HIGH(0, add(s(x''''), x'0))
HIGH(0, add(s(x'''), add(s(x'''''''), x'0''))) -> IF_HIGH(false, 0, add(s(x'''), add(s(x'''''''), x'0'')))
IF_HIGH(true, 0, add(0, add(s(x''''), x'0))) -> HIGH(0, add(s(x''''), x'0))
HIGH(0, add(0, add(s(x''''''), x'0''))) -> IF_HIGH(true, 0, add(0, add(s(x''''''), x'0'')))
IF_HIGH(true, n''', add(0, add(0, x'''))) -> HIGH(n''', add(0, x'''))
HIGH(n'', add(0, add(0, x'''''))) -> IF_HIGH(true, n'', add(0, add(0, x''''')))
IF_HIGH(false, s(0), add(s(s(x''''')), add(0, add(0, x''''''')))) -> HIGH(s(0), add(0, add(0, x''''''')))
IF_HIGH(false, s(0), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> HIGH(s(0), add(s(s(x''''')), x'''))
IF_HIGH(false, s(0), add(s(s(x''''')), add(s(0), x'''))) -> HIGH(s(0), add(s(0), x'''))
HIGH(s(0), add(s(s(x''')), x)) -> IF_HIGH(false, s(0), add(s(s(x''')), x))
IF_HIGH(true, s(0), add(s(0), add(s(s(x''''')), x'''))) -> HIGH(s(0), add(s(s(x''''')), x'''))
IF_HIGH(true, s(y'''''), add(s(0), add(s(0), x'''))) -> HIGH(s(y'''''), add(s(0), x'''))
HIGH(s(y''), add(s(0), x)) -> IF_HIGH(true, s(y''), add(s(0), x))
IF_HIGH(false, s(s(y'''')), add(s(s(x''''')), x')) -> HIGH(s(s(y'''')), x')
HIGH(s(s(y'')), add(s(s(x''')), x)) -> IF_HIGH(le(x''', y''), s(s(y'')), add(s(s(x''')), x))
IF_HIGH(true, s(s(y'''')), add(0, add(s(s(x''''')), x'''))) -> HIGH(s(s(y'''')), add(s(s(x''''')), x'''))
HIGH(s(s(y'''''')), add(0, add(s(s(x''''''')), x'''''))) -> IF_HIGH(true, s(s(y'''''')), add(0, add(s(s(x''''''')), x''''')))
IF_HIGH(true, s(s(y'''''''')), add(s(0), add(0, add(s(s(x''''''''')), x''''''')))) -> HIGH(s(s(y'''''''')), add(0, add(s(s(x''''''''')), x''''''')))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

IF_HIGH(false, s(s(y'''')), add(s(s(x''''')), x')) -> HIGH(s(s(y'''')), x')

five new Dependency Pairs are created:

IF_HIGH(false, s(s(y''''')), add(s(s(x''''')), add(s(0), x'''))) -> HIGH(s(s(y''''')), add(s(0), x'''))
IF_HIGH(false, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> HIGH(s(s(y''''')), add(s(s(x''''')), x'''))
IF_HIGH(false, s(s(y''''')), add(s(s(x''''')), add(0, add(0, x''''''')))) -> HIGH(s(s(y''''')), add(0, add(0, x''''''')))
IF_HIGH(false, s(s(y''''')), add(s(s(x''''')), add(0, add(s(0), x''''''')))) -> HIGH(s(s(y''''')), add(0, add(s(0), x''''''')))
IF_HIGH(false, s(s(y''''')), add(s(s(x''''')), add(0, add(s(s(x''''''''')), x''''''')))) -> HIGH(s(s(y''''')), add(0, add(s(s(x''''''''')), x''''''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

           →DP Problem 46

             ↳Nar

...

               →DP Problem 57

                 ↳Polynomial Ordering

       →DP Problem 7

         ↳Nar

Dependency Pairs:

IF_HIGH(false, s(s(y''''')), add(s(s(x''''')), add(0, add(s(s(x''''''''')), x''''''')))) -> HIGH(s(s(y''''')), add(0, add(s(s(x''''''''')), x''''''')))
IF_HIGH(false, s(s(y''''')), add(s(s(x''''')), add(0, add(s(0), x''''''')))) -> HIGH(s(s(y''''')), add(0, add(s(0), x''''''')))
IF_HIGH(false, s(s(y''''')), add(s(s(x''''')), add(0, add(0, x''''''')))) -> HIGH(s(s(y''''')), add(0, add(0, x''''''')))
IF_HIGH(false, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> HIGH(s(s(y''''')), add(s(s(x''''')), x'''))
IF_HIGH(false, s(s(y''''')), add(s(s(x''''')), add(s(0), x'''))) -> HIGH(s(s(y''''')), add(s(0), x'''))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(0, add(s(0), x''''''')))) -> HIGH(s(s(y''''')), add(0, add(s(0), x''''''')))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(0, add(0, x''''''')))) -> HIGH(s(s(y''''')), add(0, add(0, x''''''')))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> HIGH(s(s(y''''')), add(s(s(x''''')), x'''))
IF_HIGH(true, s(s(y'''''''')), add(s(0), add(0, add(s(s(x''''''''')), x''''''')))) -> HIGH(s(s(y'''''''')), add(0, add(s(s(x''''''''')), x''''''')))
IF_HIGH(true, s(0), add(s(0), add(0, add(s(s(x''''''''')), x''''''')))) -> HIGH(s(0), add(0, add(s(s(x''''''''')), x''''''')))
IF_HIGH(true, s(y'''''), add(s(0), add(0, add(s(0), x''''''')))) -> HIGH(s(y'''''), add(0, add(s(0), x''''''')))
IF_HIGH(true, s(y'''''), add(s(0), add(0, add(0, x''''''')))) -> HIGH(s(y'''''), add(0, add(0, x''''''')))
IF_HIGH(true, s(s(y''''')), add(s(0), add(s(s(x''''')), x'''))) -> HIGH(s(s(y''''')), add(s(s(x''''')), x'''))
IF_HIGH(false, s(0), add(s(s(x''''')), add(0, add(s(s(x''''''''')), x''''''')))) -> HIGH(s(0), add(0, add(s(s(x''''''''')), x''''''')))
IF_HIGH(false, s(0), add(s(s(x''''')), add(0, add(s(0), x''''''')))) -> HIGH(s(0), add(0, add(s(0), x''''''')))
IF_HIGH(true, s(0), add(0, add(s(s(x''''')), x'''))) -> HIGH(s(0), add(s(s(x''''')), x'''))
HIGH(s(0), add(0, add(s(s(x''''''')), x'''''))) -> IF_HIGH(true, s(0), add(0, add(s(s(x''''''')), x''''')))
IF_HIGH(true, s(y''''), add(0, add(s(0), x'''))) -> HIGH(s(y''''), add(s(0), x'''))
HIGH(s(y''''''), add(0, add(s(0), x'''''))) -> IF_HIGH(true, s(y''''''), add(0, add(s(0), x''''')))
IF_HIGH(false, 0, add(s(x''''), add(0, add(s(x''''''''), x'0'''')))) -> HIGH(0, add(0, add(s(x''''''''), x'0'''')))
HIGH(0, add(s(x'''), add(0, add(s(x''''''''''), x'0'''''')))) -> IF_HIGH(false, 0, add(s(x'''), add(0, add(s(x''''''''''), x'0''''''))))
IF_HIGH(false, 0, add(s(x''''), add(0, add(0, x''''''')))) -> HIGH(0, add(0, add(0, x''''''')))
HIGH(0, add(s(x'''), add(0, add(0, x''''''''')))) -> IF_HIGH(false, 0, add(s(x'''), add(0, add(0, x'''''''''))))
IF_HIGH(false, 0, add(s(x''''), add(s(x''''), x'0))) -> HIGH(0, add(s(x''''), x'0))
HIGH(0, add(s(x'''), add(s(x'''''''), x'0''))) -> IF_HIGH(false, 0, add(s(x'''), add(s(x'''''''), x'0'')))
IF_HIGH(true, 0, add(0, add(s(x''''), x'0))) -> HIGH(0, add(s(x''''), x'0))
HIGH(0, add(0, add(s(x''''''), x'0''))) -> IF_HIGH(true, 0, add(0, add(s(x''''''), x'0'')))
IF_HIGH(true, n''', add(0, add(0, x'''))) -> HIGH(n''', add(0, x'''))
HIGH(n'', add(0, add(0, x'''''))) -> IF_HIGH(true, n'', add(0, add(0, x''''')))
IF_HIGH(false, s(0), add(s(s(x''''')), add(0, add(0, x''''''')))) -> HIGH(s(0), add(0, add(0, x''''''')))
IF_HIGH(false, s(0), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> HIGH(s(0), add(s(s(x''''')), x'''))
IF_HIGH(false, s(0), add(s(s(x''''')), add(s(0), x'''))) -> HIGH(s(0), add(s(0), x'''))
HIGH(s(0), add(s(s(x''')), x)) -> IF_HIGH(false, s(0), add(s(s(x''')), x))
IF_HIGH(true, s(0), add(s(0), add(s(s(x''''')), x'''))) -> HIGH(s(0), add(s(s(x''''')), x'''))
IF_HIGH(true, s(y'''''), add(s(0), add(s(0), x'''))) -> HIGH(s(y'''''), add(s(0), x'''))
HIGH(s(y''), add(s(0), x)) -> IF_HIGH(true, s(y''), add(s(0), x))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(s(0), x'''))) -> HIGH(s(s(y''''')), add(s(0), x'''))
HIGH(s(s(y'')), add(s(s(x''')), x)) -> IF_HIGH(le(x''', y''), s(s(y'')), add(s(s(x''')), x))
IF_HIGH(true, s(s(y'''')), add(0, add(s(s(x''''')), x'''))) -> HIGH(s(s(y'''')), add(s(s(x''''')), x'''))
HIGH(s(s(y'''''')), add(0, add(s(s(x''''''')), x'''''))) -> IF_HIGH(true, s(s(y'''''')), add(0, add(s(s(x''''''')), x''''')))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(0, add(s(s(x''''''''')), x''''''')))) -> HIGH(s(s(y''''')), add(0, add(s(s(x''''''''')), x''''''')))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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(true, s(0), add(0, add(s(s(x''''')), x'''))) -> HIGH(s(0), add(s(s(x''''')), x'''))
IF_HIGH(true, s(y''''), add(0, add(s(0), x'''))) -> HIGH(s(y''''), add(s(0), x'''))
IF_HIGH(true, 0, add(0, add(s(x''''), x'0))) -> HIGH(0, add(s(x''''), x'0))
IF_HIGH(true, n''', add(0, add(0, x'''))) -> HIGH(n''', add(0, x'''))
IF_HIGH(true, s(s(y'''')), add(0, add(s(s(x''''')), x'''))) -> HIGH(s(s(y'''')), add(s(s(x''''')), x'''))

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

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(0) = 1

POL(false) = 0

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

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

POL(true) = 0

POL(s(x₁)) = 0

POL(le(x₁, x₂)) = 0

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

           →DP Problem 46

             ↳Nar

...

               →DP Problem 58

                 ↳Dependency Graph

       →DP Problem 7

         ↳Nar

Dependency Pairs:

IF_HIGH(false, s(s(y''''')), add(s(s(x''''')), add(0, add(s(s(x''''''''')), x''''''')))) -> HIGH(s(s(y''''')), add(0, add(s(s(x''''''''')), x''''''')))
IF_HIGH(false, s(s(y''''')), add(s(s(x''''')), add(0, add(s(0), x''''''')))) -> HIGH(s(s(y''''')), add(0, add(s(0), x''''''')))
IF_HIGH(false, s(s(y''''')), add(s(s(x''''')), add(0, add(0, x''''''')))) -> HIGH(s(s(y''''')), add(0, add(0, x''''''')))
IF_HIGH(false, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> HIGH(s(s(y''''')), add(s(s(x''''')), x'''))
IF_HIGH(false, s(s(y''''')), add(s(s(x''''')), add(s(0), x'''))) -> HIGH(s(s(y''''')), add(s(0), x'''))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(0, add(s(0), x''''''')))) -> HIGH(s(s(y''''')), add(0, add(s(0), x''''''')))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(0, add(0, x''''''')))) -> HIGH(s(s(y''''')), add(0, add(0, x''''''')))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> HIGH(s(s(y''''')), add(s(s(x''''')), x'''))
IF_HIGH(true, s(s(y'''''''')), add(s(0), add(0, add(s(s(x''''''''')), x''''''')))) -> HIGH(s(s(y'''''''')), add(0, add(s(s(x''''''''')), x''''''')))
IF_HIGH(true, s(0), add(s(0), add(0, add(s(s(x''''''''')), x''''''')))) -> HIGH(s(0), add(0, add(s(s(x''''''''')), x''''''')))
IF_HIGH(true, s(y'''''), add(s(0), add(0, add(s(0), x''''''')))) -> HIGH(s(y'''''), add(0, add(s(0), x''''''')))
IF_HIGH(true, s(y'''''), add(s(0), add(0, add(0, x''''''')))) -> HIGH(s(y'''''), add(0, add(0, x''''''')))
IF_HIGH(true, s(s(y''''')), add(s(0), add(s(s(x''''')), x'''))) -> HIGH(s(s(y''''')), add(s(s(x''''')), x'''))
IF_HIGH(false, s(0), add(s(s(x''''')), add(0, add(s(s(x''''''''')), x''''''')))) -> HIGH(s(0), add(0, add(s(s(x''''''''')), x''''''')))
IF_HIGH(false, s(0), add(s(s(x''''')), add(0, add(s(0), x''''''')))) -> HIGH(s(0), add(0, add(s(0), x''''''')))
HIGH(s(0), add(0, add(s(s(x''''''')), x'''''))) -> IF_HIGH(true, s(0), add(0, add(s(s(x''''''')), x''''')))
HIGH(s(y''''''), add(0, add(s(0), x'''''))) -> IF_HIGH(true, s(y''''''), add(0, add(s(0), x''''')))
IF_HIGH(false, 0, add(s(x''''), add(0, add(s(x''''''''), x'0'''')))) -> HIGH(0, add(0, add(s(x''''''''), x'0'''')))
HIGH(0, add(s(x'''), add(0, add(s(x''''''''''), x'0'''''')))) -> IF_HIGH(false, 0, add(s(x'''), add(0, add(s(x''''''''''), x'0''''''))))
IF_HIGH(false, 0, add(s(x''''), add(0, add(0, x''''''')))) -> HIGH(0, add(0, add(0, x''''''')))
HIGH(0, add(s(x'''), add(0, add(0, x''''''''')))) -> IF_HIGH(false, 0, add(s(x'''), add(0, add(0, x'''''''''))))
IF_HIGH(false, 0, add(s(x''''), add(s(x''''), x'0))) -> HIGH(0, add(s(x''''), x'0))
HIGH(0, add(s(x'''), add(s(x'''''''), x'0''))) -> IF_HIGH(false, 0, add(s(x'''), add(s(x'''''''), x'0'')))
HIGH(0, add(0, add(s(x''''''), x'0''))) -> IF_HIGH(true, 0, add(0, add(s(x''''''), x'0'')))
HIGH(n'', add(0, add(0, x'''''))) -> IF_HIGH(true, n'', add(0, add(0, x''''')))
IF_HIGH(false, s(0), add(s(s(x''''')), add(0, add(0, x''''''')))) -> HIGH(s(0), add(0, add(0, x''''''')))
IF_HIGH(false, s(0), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> HIGH(s(0), add(s(s(x''''')), x'''))
IF_HIGH(false, s(0), add(s(s(x''''')), add(s(0), x'''))) -> HIGH(s(0), add(s(0), x'''))
HIGH(s(0), add(s(s(x''')), x)) -> IF_HIGH(false, s(0), add(s(s(x''')), x))
IF_HIGH(true, s(0), add(s(0), add(s(s(x''''')), x'''))) -> HIGH(s(0), add(s(s(x''''')), x'''))
IF_HIGH(true, s(y'''''), add(s(0), add(s(0), x'''))) -> HIGH(s(y'''''), add(s(0), x'''))
HIGH(s(y''), add(s(0), x)) -> IF_HIGH(true, s(y''), add(s(0), x))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(s(0), x'''))) -> HIGH(s(s(y''''')), add(s(0), x'''))
HIGH(s(s(y'')), add(s(s(x''')), x)) -> IF_HIGH(le(x''', y''), s(s(y'')), add(s(s(x''')), x))
HIGH(s(s(y'''''')), add(0, add(s(s(x''''''')), x'''''))) -> IF_HIGH(true, s(s(y'''''')), add(0, add(s(s(x''''''')), x''''')))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(0, add(s(s(x''''''''')), x''''''')))) -> HIGH(s(s(y''''')), add(0, add(s(s(x''''''''')), x''''''')))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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 the DP problem was split into 2 DP problems.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

           →DP Problem 46

             ↳Nar

...

               →DP Problem 59

                 ↳Polynomial Ordering

       →DP Problem 7

         ↳Nar

Dependency Pairs:

IF_HIGH(false, s(s(y''''')), add(s(s(x''''')), add(s(0), x'''))) -> HIGH(s(s(y''''')), add(s(0), x'''))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> HIGH(s(s(y''''')), add(s(s(x''''')), x'''))
IF_HIGH(true, s(s(y''''')), add(s(0), add(s(s(x''''')), x'''))) -> HIGH(s(s(y''''')), add(s(s(x''''')), x'''))
IF_HIGH(false, s(0), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> HIGH(s(0), add(s(s(x''''')), x'''))
IF_HIGH(false, s(0), add(s(s(x''''')), add(s(0), x'''))) -> HIGH(s(0), add(s(0), x'''))
HIGH(s(0), add(s(s(x''')), x)) -> IF_HIGH(false, s(0), add(s(s(x''')), x))
IF_HIGH(true, s(0), add(s(0), add(s(s(x''''')), x'''))) -> HIGH(s(0), add(s(s(x''''')), x'''))
IF_HIGH(true, s(y'''''), add(s(0), add(s(0), x'''))) -> HIGH(s(y'''''), add(s(0), x'''))
HIGH(s(y''), add(s(0), x)) -> IF_HIGH(true, s(y''), add(s(0), x))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(s(0), x'''))) -> HIGH(s(s(y''''')), add(s(0), x'''))
HIGH(s(s(y'')), add(s(s(x''')), x)) -> IF_HIGH(le(x''', y''), s(s(y'')), add(s(s(x''')), x))
IF_HIGH(false, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> HIGH(s(s(y''''')), add(s(s(x''''')), x'''))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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(true, s(s(y''''')), add(s(0), add(s(s(x''''')), x'''))) -> HIGH(s(s(y''''')), add(s(s(x''''')), x'''))
IF_HIGH(true, s(0), add(s(0), add(s(s(x''''')), x'''))) -> HIGH(s(0), add(s(s(x''''')), x'''))
IF_HIGH(true, s(y'''''), add(s(0), add(s(0), x'''))) -> HIGH(s(y'''''), add(s(0), x'''))

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

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(0) = 1

POL(false) = 0

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

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

POL(true) = 0

POL(s(x₁)) = x₁

POL(le(x₁, x₂)) = 0

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

           →DP Problem 46

             ↳Nar

...

               →DP Problem 61

                 ↳Dependency Graph

       →DP Problem 7

         ↳Nar

Dependency Pairs:

IF_HIGH(false, s(s(y''''')), add(s(s(x''''')), add(s(0), x'''))) -> HIGH(s(s(y''''')), add(s(0), x'''))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> HIGH(s(s(y''''')), add(s(s(x''''')), x'''))
IF_HIGH(false, s(0), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> HIGH(s(0), add(s(s(x''''')), x'''))
IF_HIGH(false, s(0), add(s(s(x''''')), add(s(0), x'''))) -> HIGH(s(0), add(s(0), x'''))
HIGH(s(0), add(s(s(x''')), x)) -> IF_HIGH(false, s(0), add(s(s(x''')), x))
HIGH(s(y''), add(s(0), x)) -> IF_HIGH(true, s(y''), add(s(0), x))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(s(0), x'''))) -> HIGH(s(s(y''''')), add(s(0), x'''))
HIGH(s(s(y'')), add(s(s(x''')), x)) -> IF_HIGH(le(x''', y''), s(s(y'')), add(s(s(x''')), x))
IF_HIGH(false, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> HIGH(s(s(y''''')), add(s(s(x''''')), x'''))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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 the DP problem was split into 2 DP problems.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

           →DP Problem 46

             ↳Nar

...

               →DP Problem 63

                 ↳Polynomial Ordering

       →DP Problem 7

         ↳Nar

Dependency Pairs:

IF_HIGH(false, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> HIGH(s(s(y''''')), add(s(s(x''''')), x'''))
HIGH(s(s(y'')), add(s(s(x''')), x)) -> IF_HIGH(le(x''', y''), s(s(y'')), add(s(s(x''')), x))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> HIGH(s(s(y''''')), add(s(s(x''''')), x'''))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> HIGH(s(s(y''''')), add(s(s(x''''')), x'''))
IF_HIGH(true, s(s(y''''')), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> HIGH(s(s(y''''')), add(s(s(x''''')), x'''))

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

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(0) = 0

POL(false) = 0

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

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

POL(true) = 0

POL(s(x₁)) = 0

POL(le(x₁, x₂)) = 0

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

           →DP Problem 46

             ↳Nar

...

               →DP Problem 65

                 ↳Dependency Graph

       →DP Problem 7

         ↳Nar

Dependency Pair:

HIGH(s(s(y'')), add(s(s(x''')), x)) -> IF_HIGH(le(x''', y''), s(s(y'')), add(s(s(x''')), x))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

           →DP Problem 46

             ↳Nar

...

               →DP Problem 64

                 ↳Polynomial Ordering

       →DP Problem 7

         ↳Nar

Dependency Pairs:

HIGH(s(0), add(s(s(x''')), x)) -> IF_HIGH(false, s(0), add(s(s(x''')), x))
IF_HIGH(false, s(0), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> HIGH(s(0), add(s(s(x''''')), x'''))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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:

IF_HIGH(false, s(0), add(s(s(x''''')), add(s(s(x''''')), x'''))) -> HIGH(s(0), add(s(s(x''''')), x'''))

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

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(0) = 0

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

POL(false) = 0

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

POL(s(x₁)) = 1

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

           →DP Problem 46

             ↳Nar

...

               →DP Problem 66

                 ↳Dependency Graph

       →DP Problem 7

         ↳Nar

Dependency Pair:

HIGH(s(0), add(s(s(x''')), x)) -> IF_HIGH(false, s(0), add(s(s(x''')), x))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

           →DP Problem 46

             ↳Nar

...

               →DP Problem 60

                 ↳Polynomial Ordering

       →DP Problem 7

         ↳Nar

Dependency Pairs:

HIGH(0, add(s(x'''), add(s(x'''''''), x'0''))) -> IF_HIGH(false, 0, add(s(x'''), add(s(x'''''''), x'0'')))
IF_HIGH(false, 0, add(s(x''''), add(s(x''''), x'0))) -> HIGH(0, add(s(x''''), x'0))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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:

IF_HIGH(false, 0, add(s(x''''), add(s(x''''), x'0))) -> HIGH(0, add(s(x''''), x'0))

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

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(0) = 0

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

POL(false) = 0

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

POL(s(x₁)) = 1

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

           →DP Problem 46

             ↳Nar

...

               →DP Problem 62

                 ↳Dependency Graph

       →DP Problem 7

         ↳Nar

Dependency Pair:

HIGH(0, add(s(x'''), add(s(x'''''''), x'0''))) -> IF_HIGH(false, 0, add(s(x'''), add(s(x'''''''), x'0'')))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Narrowing Transformation

Dependency Pairs:

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

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

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

two new Dependency Pairs are created:

QUICKSORT(add(n'', nil)) -> QUICKSORT(nil)
QUICKSORT(add(n'', add(m', x''))) -> QUICKSORT(if_low(le(m', n''), n'', add(m', x'')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

           →DP Problem 67

             ↳Narrowing Transformation

Dependency Pairs:

QUICKSORT(add(n'', add(m', x''))) -> QUICKSORT(if_low(le(m', n''), n'', add(m', x'')))
QUICKSORT(add(n, x)) -> QUICKSORT(high(n, x))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

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

two new Dependency Pairs are created:

QUICKSORT(add(n'', nil)) -> QUICKSORT(nil)
QUICKSORT(add(n'', add(m', x''))) -> QUICKSORT(if_high(le(m', n''), n'', add(m', x'')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

           →DP Problem 67

             ↳Nar

...

               →DP Problem 68

                 ↳Narrowing Transformation

Dependency Pairs:

QUICKSORT(add(n'', add(m', x''))) -> QUICKSORT(if_high(le(m', n''), n'', add(m', x'')))
QUICKSORT(add(n'', add(m', x''))) -> QUICKSORT(if_low(le(m', n''), n'', add(m', x'')))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

QUICKSORT(add(n'', add(m', x''))) -> QUICKSORT(if_low(le(m', n''), n'', add(m', x'')))

three new Dependency Pairs are created:

QUICKSORT(add(n''', add(0, x''))) -> QUICKSORT(if_low(true, n''', add(0, x'')))
QUICKSORT(add(0, add(s(x'), x''))) -> QUICKSORT(if_low(false, 0, add(s(x'), x'')))
QUICKSORT(add(s(y'), add(s(x'), x''))) -> QUICKSORT(if_low(le(x', y'), s(y'), add(s(x'), x'')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

           →DP Problem 67

             ↳Nar

...

               →DP Problem 69

                 ↳Rewriting Transformation

Dependency Pairs:

QUICKSORT(add(s(y'), add(s(x'), x''))) -> QUICKSORT(if_low(le(x', y'), s(y'), add(s(x'), x'')))
QUICKSORT(add(0, add(s(x'), x''))) -> QUICKSORT(if_low(false, 0, add(s(x'), x'')))
QUICKSORT(add(n''', add(0, x''))) -> QUICKSORT(if_low(true, n''', add(0, x'')))
QUICKSORT(add(n'', add(m', x''))) -> QUICKSORT(if_high(le(m', n''), n'', add(m', x'')))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

QUICKSORT(add(n''', add(0, x''))) -> QUICKSORT(if_low(true, n''', add(0, x'')))

one new Dependency Pair is created:

QUICKSORT(add(n''', add(0, x''))) -> QUICKSORT(add(0, low(n''', x'')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

           →DP Problem 67

             ↳Nar

...

               →DP Problem 70

                 ↳Rewriting Transformation

Dependency Pairs:

QUICKSORT(add(n''', add(0, x''))) -> QUICKSORT(add(0, low(n''', x'')))
QUICKSORT(add(0, add(s(x'), x''))) -> QUICKSORT(if_low(false, 0, add(s(x'), x'')))
QUICKSORT(add(n'', add(m', x''))) -> QUICKSORT(if_high(le(m', n''), n'', add(m', x'')))
QUICKSORT(add(s(y'), add(s(x'), x''))) -> QUICKSORT(if_low(le(x', y'), s(y'), add(s(x'), x'')))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

QUICKSORT(add(0, add(s(x'), x''))) -> QUICKSORT(if_low(false, 0, add(s(x'), x'')))

one new Dependency Pair is created:

QUICKSORT(add(0, add(s(x'), x''))) -> QUICKSORT(low(0, x''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

           →DP Problem 67

             ↳Nar

...

               →DP Problem 71

                 ↳Narrowing Transformation

Dependency Pairs:

QUICKSORT(add(0, add(s(x'), x''))) -> QUICKSORT(low(0, x''))
QUICKSORT(add(s(y'), add(s(x'), x''))) -> QUICKSORT(if_low(le(x', y'), s(y'), add(s(x'), x'')))
QUICKSORT(add(n'', add(m', x''))) -> QUICKSORT(if_high(le(m', n''), n'', add(m', x'')))
QUICKSORT(add(n''', add(0, x''))) -> QUICKSORT(add(0, low(n''', x'')))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

QUICKSORT(add(n'', add(m', x''))) -> QUICKSORT(if_high(le(m', n''), n'', add(m', x'')))

three new Dependency Pairs are created:

QUICKSORT(add(n''', add(0, x''))) -> QUICKSORT(if_high(true, n''', add(0, x'')))
QUICKSORT(add(0, add(s(x'), x''))) -> QUICKSORT(if_high(false, 0, add(s(x'), x'')))
QUICKSORT(add(s(y'), add(s(x'), x''))) -> QUICKSORT(if_high(le(x', y'), s(y'), add(s(x'), x'')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

           →DP Problem 67

             ↳Nar

...

               →DP Problem 72

                 ↳Rewriting Transformation

Dependency Pairs:

QUICKSORT(add(s(y'), add(s(x'), x''))) -> QUICKSORT(if_high(le(x', y'), s(y'), add(s(x'), x'')))
QUICKSORT(add(0, add(s(x'), x''))) -> QUICKSORT(if_high(false, 0, add(s(x'), x'')))
QUICKSORT(add(n''', add(0, x''))) -> QUICKSORT(if_high(true, n''', add(0, x'')))
QUICKSORT(add(n''', add(0, x''))) -> QUICKSORT(add(0, low(n''', x'')))
QUICKSORT(add(s(y'), add(s(x'), x''))) -> QUICKSORT(if_low(le(x', y'), s(y'), add(s(x'), x'')))
QUICKSORT(add(0, add(s(x'), x''))) -> QUICKSORT(low(0, x''))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

QUICKSORT(add(n''', add(0, x''))) -> QUICKSORT(if_high(true, n''', add(0, x'')))

one new Dependency Pair is created:

QUICKSORT(add(n''', add(0, x''))) -> QUICKSORT(high(n''', x''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

           →DP Problem 67

             ↳Nar

...

               →DP Problem 73

                 ↳Rewriting Transformation

Dependency Pairs:

QUICKSORT(add(n''', add(0, x''))) -> QUICKSORT(high(n''', x''))
QUICKSORT(add(0, add(s(x'), x''))) -> QUICKSORT(if_high(false, 0, add(s(x'), x'')))
QUICKSORT(add(0, add(s(x'), x''))) -> QUICKSORT(low(0, x''))
QUICKSORT(add(n''', add(0, x''))) -> QUICKSORT(add(0, low(n''', x'')))
QUICKSORT(add(s(y'), add(s(x'), x''))) -> QUICKSORT(if_low(le(x', y'), s(y'), add(s(x'), x'')))
QUICKSORT(add(s(y'), add(s(x'), x''))) -> QUICKSORT(if_high(le(x', y'), s(y'), add(s(x'), x'')))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

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

QUICKSORT(add(0, add(s(x'), x''))) -> QUICKSORT(if_high(false, 0, add(s(x'), x'')))

one new Dependency Pair is created:

QUICKSORT(add(0, add(s(x'), x''))) -> QUICKSORT(add(s(x'), high(0, x'')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

           →DP Problem 67

             ↳Nar

...

               →DP Problem 74

                 ↳Polynomial Ordering

Dependency Pairs:

QUICKSORT(add(0, add(s(x'), x''))) -> QUICKSORT(add(s(x'), high(0, x'')))
QUICKSORT(add(s(y'), add(s(x'), x''))) -> QUICKSORT(if_high(le(x', y'), s(y'), add(s(x'), x'')))
QUICKSORT(add(0, add(s(x'), x''))) -> QUICKSORT(low(0, x''))
QUICKSORT(add(n''', add(0, x''))) -> QUICKSORT(add(0, low(n''', x'')))
QUICKSORT(add(s(y'), add(s(x'), x''))) -> QUICKSORT(if_low(le(x', y'), s(y'), add(s(x'), x'')))
QUICKSORT(add(n''', add(0, x''))) -> QUICKSORT(high(n''', x''))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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(0, add(s(x'), x''))) -> QUICKSORT(add(s(x'), high(0, x'')))
QUICKSORT(add(0, add(s(x'), x''))) -> QUICKSORT(low(0, x''))
QUICKSORT(add(n''', add(0, x''))) -> QUICKSORT(high(n''', x''))

Additionally, the following usable rules for innermost w.r.t. to the implicit AFS can be oriented:

if_high(true, n, add(m, x)) -> high(n, x)
if_high(false, n, add(m, x)) -> add(m, high(n, x))
high(n, nil) -> nil
high(n, add(m, x)) -> if_high(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)
low(n, nil) -> nil
low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x))

Used ordering: Polynomial ordering with Polynomial interpretation:

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

POL(0) = 1

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

POL(false) = 0

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

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

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

POL(true) = 0

POL(nil) = 0

POL(s(x₁)) = 0

POL(le(x₁, x₂)) = 0

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

           →DP Problem 67

             ↳Nar

...

               →DP Problem 75

                 ↳Dependency Graph

Dependency Pairs:

QUICKSORT(add(s(y'), add(s(x'), x''))) -> QUICKSORT(if_high(le(x', y'), s(y'), add(s(x'), x'')))
QUICKSORT(add(n''', add(0, x''))) -> QUICKSORT(add(0, low(n''', x'')))
QUICKSORT(add(s(y'), add(s(x'), x''))) -> QUICKSORT(if_low(le(x', y'), s(y'), add(s(x'), x'')))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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 the DP problem was split into 2 DP problems.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

           →DP Problem 67

             ↳Nar

...

               →DP Problem 76

                 ↳Polynomial Ordering

Dependency Pair:

QUICKSORT(add(n''', add(0, x''))) -> QUICKSORT(add(0, low(n''', x'')))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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:

QUICKSORT(add(n''', add(0, x''))) -> QUICKSORT(add(0, low(n''', x'')))

Additionally, the following usable rules for innermost w.r.t. to the implicit AFS can be oriented:

if_low(true, n, add(m, x)) -> add(m, low(n, x))
if_low(false, n, add(m, x)) -> low(n, x)
low(n, nil) -> nil
low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x))

Used ordering: Polynomial ordering with Polynomial interpretation:

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

POL(0) = 0

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

POL(false) = 0

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

POL(true) = 0

POL(nil) = 0

POL(s(x₁)) = 0

POL(le(x₁, x₂)) = 0

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

           →DP Problem 67

             ↳Nar

...

               →DP Problem 78

                 ↳Dependency Graph

Dependency Pair:

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

       →DP Problem 5

         ↳Nar

       →DP Problem 6

         ↳Nar

       →DP Problem 7

         ↳Nar

           →DP Problem 67

             ↳Nar

...

               →DP Problem 77

                 ↳Polynomial Ordering

Dependency Pairs:

QUICKSORT(add(s(y'), add(s(x'), x''))) -> QUICKSORT(if_low(le(x', y'), s(y'), add(s(x'), x'')))
QUICKSORT(add(s(y'), add(s(x'), x''))) -> QUICKSORT(if_high(le(x', y'), s(y'), add(s(x'), x'')))

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
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(s(y'), add(s(x'), x''))) -> QUICKSORT(if_low(le(x', y'), s(y'), add(s(x'), x'')))
QUICKSORT(add(s(y'), add(s(x'), x''))) -> QUICKSORT(if_high(le(x', y'), s(y'), add(s(x'), x'')))

Additionally, the following usable rules for innermost w.r.t. to the implicit AFS can be oriented:

if_low(true, n, add(m, x)) -> add(m, low(n, x))
if_low(false, n, add(m, x)) -> low(n, x)
low(n, nil) -> nil
low(n, add(m, x)) -> if_low(le(m, n), n, add(m, 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))

Used ordering: Polynomial ordering with Polynomial interpretation:

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

POL(0) = 0

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

POL(false) = 0

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

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

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

POL(true) = 0

POL(nil) = 0

POL(s(x₁)) = 1

POL(le(x₁, x₂)) = 0

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

resulting in one new DP problem.

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

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

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

POL(QUOT(x₁, x₂))	= 1 + x₁
POL(0)	= 0
POL(s(x₁))	= 1 + x₁

POL(QUOT(x₁, x₂))	= 1 + x₁ + x₂
POL(0)	= 1
POL(minus(x₁, x₂))	= x₁
POL(s(x₁))	= 1 + x₁

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

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

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