Termination w.r.t. Q proof of /tmp/tmpWdOBbb/quicksort.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
low(n, nil) → nil
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))
if_low(false, n, add(m, x)) → low(n, x)
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
if_high(false, n, add(m, x)) → add(m, high(n, x))
head(add(n, x)) → n
tail(add(n, x)) → x
isempty(nil) → true
isempty(add(n, x)) → false
quicksort(x) → if_qs(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
if_qs(true, x, n, y) → nil
if_qs(false, x, n, y) → app(quicksort(x), add(n, quicksort(y)))

Q is empty.

↳ QTRS

  ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
low(n, nil) → nil
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))
if_low(false, n, add(m, x)) → low(n, x)
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
if_high(false, n, add(m, x)) → add(m, high(n, x))
head(add(n, x)) → n
tail(add(n, x)) → x
isempty(nil) → true
isempty(add(n, x)) → false
quicksort(x) → if_qs(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
if_qs(true, x, n, y) → nil
if_qs(false, x, n, y) → app(quicksort(x), add(n, quicksort(y)))

Q is empty.

The TRS is overlay and locally confluent. By [19] we can switch to innermost.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
low(n, nil) → nil
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))
if_low(false, n, add(m, x)) → low(n, x)
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
if_high(false, n, add(m, x)) → add(m, high(n, x))
head(add(n, x)) → n
tail(add(n, x)) → x
isempty(nil) → true
isempty(add(n, x)) → false
quicksort(x) → if_qs(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
if_qs(true, x, n, y) → nil
if_qs(false, x, n, y) → app(quicksort(x), add(n, quicksort(y)))

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
head(add(x0, x1))
tail(add(x0, x1))
isempty(nil)
isempty(add(x0, x1))
quicksort(x0)
if_qs(true, x0, x1, x2)
if_qs(false, x0, x1, x2)

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

QUICKSORT(x) → TAIL(x)
QUICKSORT(x) → HEAD(x)
LOW(n, add(m, x)) → IF_LOW(le(m, n), n, add(m, x))
IF_LOW(false, n, add(m, x)) → LOW(n, x)
IF_QS(false, x, n, y) → APP(quicksort(x), add(n, quicksort(y)))
QUICKSORT(x) → IF_QS(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
HIGH(n, add(m, x)) → LE(m, n)
LE(s(x), s(y)) → LE(x, y)
LOW(n, add(m, x)) → LE(m, n)
QUICKSORT(x) → HIGH(head(x), tail(x))
APP(add(n, x), y) → APP(x, y)
IF_HIGH(false, n, add(m, x)) → HIGH(n, x)
QUICKSORT(x) → LOW(head(x), tail(x))
HIGH(n, add(m, x)) → IF_HIGH(le(m, n), n, add(m, x))
IF_LOW(true, n, add(m, x)) → LOW(n, x)
IF_HIGH(true, n, add(m, x)) → HIGH(n, x)
IF_QS(false, x, n, y) → QUICKSORT(x)
IF_QS(false, x, n, y) → QUICKSORT(y)
QUICKSORT(x) → ISEMPTY(x)

The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
low(n, nil) → nil
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))
if_low(false, n, add(m, x)) → low(n, x)
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
if_high(false, n, add(m, x)) → add(m, high(n, x))
head(add(n, x)) → n
tail(add(n, x)) → x
isempty(nil) → true
isempty(add(n, x)) → false
quicksort(x) → if_qs(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
if_qs(true, x, n, y) → nil
if_qs(false, x, n, y) → app(quicksort(x), add(n, quicksort(y)))

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
head(add(x0, x1))
tail(add(x0, x1))
isempty(nil)
isempty(add(x0, x1))
quicksort(x0)
if_qs(true, x0, x1, x2)
if_qs(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

QUICKSORT(x) → TAIL(x)
QUICKSORT(x) → HEAD(x)
LOW(n, add(m, x)) → IF_LOW(le(m, n), n, add(m, x))
IF_LOW(false, n, add(m, x)) → LOW(n, x)
IF_QS(false, x, n, y) → APP(quicksort(x), add(n, quicksort(y)))
QUICKSORT(x) → IF_QS(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
HIGH(n, add(m, x)) → LE(m, n)
LE(s(x), s(y)) → LE(x, y)
LOW(n, add(m, x)) → LE(m, n)
QUICKSORT(x) → HIGH(head(x), tail(x))
APP(add(n, x), y) → APP(x, y)
IF_HIGH(false, n, add(m, x)) → HIGH(n, x)
QUICKSORT(x) → LOW(head(x), tail(x))
HIGH(n, add(m, x)) → IF_HIGH(le(m, n), n, add(m, x))
IF_LOW(true, n, add(m, x)) → LOW(n, x)
IF_HIGH(true, n, add(m, x)) → HIGH(n, x)
IF_QS(false, x, n, y) → QUICKSORT(x)
IF_QS(false, x, n, y) → QUICKSORT(y)
QUICKSORT(x) → ISEMPTY(x)

The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
low(n, nil) → nil
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))
if_low(false, n, add(m, x)) → low(n, x)
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
if_high(false, n, add(m, x)) → add(m, high(n, x))
head(add(n, x)) → n
tail(add(n, x)) → x
isempty(nil) → true
isempty(add(n, x)) → false
quicksort(x) → if_qs(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
if_qs(true, x, n, y) → nil
if_qs(false, x, n, y) → app(quicksort(x), add(n, quicksort(y)))

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
head(add(x0, x1))
tail(add(x0, x1))
isempty(nil)
isempty(add(x0, x1))
quicksort(x0)
if_qs(true, x0, x1, x2)
if_qs(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 5 SCCs with 8 less nodes.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP(add(n, x), y) → APP(x, y)

The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
low(n, nil) → nil
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))
if_low(false, n, add(m, x)) → low(n, x)
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
if_high(false, n, add(m, x)) → add(m, high(n, x))
head(add(n, x)) → n
tail(add(n, x)) → x
isempty(nil) → true
isempty(add(n, x)) → false
quicksort(x) → if_qs(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
if_qs(true, x, n, y) → nil
if_qs(false, x, n, y) → app(quicksort(x), add(n, quicksort(y)))

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
head(add(x0, x1))
tail(add(x0, x1))
isempty(nil)
isempty(add(x0, x1))
quicksort(x0)
if_qs(true, x0, x1, x2)
if_qs(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP(add(n, x), y) → APP(x, y)

R is empty.
The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
head(add(x0, x1))
tail(add(x0, x1))
isempty(nil)
isempty(add(x0, x1))
quicksort(x0)
if_qs(true, x0, x1, x2)
if_qs(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
head(add(x0, x1))
tail(add(x0, x1))
isempty(nil)
isempty(add(x0, x1))
quicksort(x0)
if_qs(true, x0, x1, x2)
if_qs(false, x0, x1, x2)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP(add(n, x), y) → APP(x, y)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

APP(add(n, x), y) → APP(x, y)
The graph contains the following edges 1 > 1, 2 >= 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LE(s(x), s(y)) → LE(x, y)

The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
low(n, nil) → nil
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))
if_low(false, n, add(m, x)) → low(n, x)
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
if_high(false, n, add(m, x)) → add(m, high(n, x))
head(add(n, x)) → n
tail(add(n, x)) → x
isempty(nil) → true
isempty(add(n, x)) → false
quicksort(x) → if_qs(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
if_qs(true, x, n, y) → nil
if_qs(false, x, n, y) → app(quicksort(x), add(n, quicksort(y)))

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
head(add(x0, x1))
tail(add(x0, x1))
isempty(nil)
isempty(add(x0, x1))
quicksort(x0)
if_qs(true, x0, x1, x2)
if_qs(false, x0, x1, x2)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LE(s(x), s(y)) → LE(x, y)

R is empty.
The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
head(add(x0, x1))
tail(add(x0, x1))
isempty(nil)
isempty(add(x0, x1))
quicksort(x0)
if_qs(true, x0, x1, x2)
if_qs(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
head(add(x0, x1))
tail(add(x0, x1))
isempty(nil)
isempty(add(x0, x1))
quicksort(x0)
if_qs(true, x0, x1, x2)
if_qs(false, x0, x1, x2)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LE(s(x), s(y)) → LE(x, y)

From the DPs we obtained the following set of size-change graphs:

LE(s(x), s(y)) → LE(x, y)
The graph contains the following edges 1 > 1, 2 > 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

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

The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
low(n, nil) → nil
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))
if_low(false, n, add(m, x)) → low(n, x)
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
if_high(false, n, add(m, x)) → add(m, high(n, x))
head(add(n, x)) → n
tail(add(n, x)) → x
isempty(nil) → true
isempty(add(n, x)) → false
quicksort(x) → if_qs(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
if_qs(true, x, n, y) → nil
if_qs(false, x, n, y) → app(quicksort(x), add(n, quicksort(y)))

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
head(add(x0, x1))
tail(add(x0, x1))
isempty(nil)
isempty(add(x0, x1))
quicksort(x0)
if_qs(true, x0, x1, x2)
if_qs(false, x0, x1, x2)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

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

The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
head(add(x0, x1))
tail(add(x0, x1))
isempty(nil)
isempty(add(x0, x1))
quicksort(x0)
if_qs(true, x0, x1, x2)
if_qs(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

app(nil, x0)
app(add(x0, x1), x2)
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
head(add(x0, x1))
tail(add(x0, x1))
isempty(nil)
isempty(add(x0, x1))
quicksort(x0)
if_qs(true, x0, x1, x2)
if_qs(false, x0, x1, x2)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

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

The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

HIGH(n, add(m, x)) → IF_HIGH(le(m, n), n, add(m, x))
The graph contains the following edges 1 >= 2, 2 >= 3
IF_HIGH(false, n, add(m, x)) → HIGH(n, x)
The graph contains the following edges 2 >= 1, 3 > 2
IF_HIGH(true, n, add(m, x)) → HIGH(n, x)
The graph contains the following edges 2 >= 1, 3 > 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

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

The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
low(n, nil) → nil
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))
if_low(false, n, add(m, x)) → low(n, x)
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
if_high(false, n, add(m, x)) → add(m, high(n, x))
head(add(n, x)) → n
tail(add(n, x)) → x
isempty(nil) → true
isempty(add(n, x)) → false
quicksort(x) → if_qs(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
if_qs(true, x, n, y) → nil
if_qs(false, x, n, y) → app(quicksort(x), add(n, quicksort(y)))

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
head(add(x0, x1))
tail(add(x0, x1))
isempty(nil)
isempty(add(x0, x1))
quicksort(x0)
if_qs(true, x0, x1, x2)
if_qs(false, x0, x1, x2)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

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

The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
head(add(x0, x1))
tail(add(x0, x1))
isempty(nil)
isempty(add(x0, x1))
quicksort(x0)
if_qs(true, x0, x1, x2)
if_qs(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

app(nil, x0)
app(add(x0, x1), x2)
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
head(add(x0, x1))
tail(add(x0, x1))
isempty(nil)
isempty(add(x0, x1))
quicksort(x0)
if_qs(true, x0, x1, x2)
if_qs(false, x0, x1, x2)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

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

The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

LOW(n, add(m, x)) → IF_LOW(le(m, n), n, add(m, x))
The graph contains the following edges 1 >= 2, 2 >= 3
IF_LOW(false, n, add(m, x)) → LOW(n, x)
The graph contains the following edges 2 >= 1, 3 > 2
IF_LOW(true, n, add(m, x)) → LOW(n, x)
The graph contains the following edges 2 >= 1, 3 > 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

IF_QS(false, x, n, y) → QUICKSORT(x)
QUICKSORT(x) → IF_QS(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
IF_QS(false, x, n, y) → QUICKSORT(y)

The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
low(n, nil) → nil
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))
if_low(false, n, add(m, x)) → low(n, x)
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
if_high(false, n, add(m, x)) → add(m, high(n, x))
head(add(n, x)) → n
tail(add(n, x)) → x
isempty(nil) → true
isempty(add(n, x)) → false
quicksort(x) → if_qs(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
if_qs(true, x, n, y) → nil
if_qs(false, x, n, y) → app(quicksort(x), add(n, quicksort(y)))

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
head(add(x0, x1))
tail(add(x0, x1))
isempty(nil)
isempty(add(x0, x1))
quicksort(x0)
if_qs(true, x0, x1, x2)
if_qs(false, x0, x1, x2)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

IF_QS(false, x, n, y) → QUICKSORT(x)
QUICKSORT(x) → IF_QS(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
IF_QS(false, x, n, y) → QUICKSORT(y)

The TRS R consists of the following rules:

isempty(nil) → true
isempty(add(n, x)) → false
head(add(n, x)) → n
tail(add(n, x)) → x
low(n, nil) → nil
if_low(false, n, add(m, x)) → low(n, x)
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
high(n, nil) → nil
if_high(true, n, add(m, x)) → high(n, x)
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
if_high(false, n, add(m, x)) → add(m, high(n, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
head(add(x0, x1))
tail(add(x0, x1))
isempty(nil)
isempty(add(x0, x1))
quicksort(x0)
if_qs(true, x0, x1, x2)
if_qs(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

app(nil, x0)
app(add(x0, x1), x2)
quicksort(x0)
if_qs(true, x0, x1, x2)
if_qs(false, x0, x1, x2)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

QUICKSORT(x) → IF_QS(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
IF_QS(false, x, n, y) → QUICKSORT(x)
IF_QS(false, x, n, y) → QUICKSORT(y)

The TRS R consists of the following rules:

isempty(nil) → true
isempty(add(n, x)) → false
head(add(n, x)) → n
tail(add(n, x)) → x
low(n, nil) → nil
if_low(false, n, add(m, x)) → low(n, x)
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
high(n, nil) → nil
if_high(true, n, add(m, x)) → high(n, x)
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
if_high(false, n, add(m, x)) → add(m, high(n, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
head(add(x0, x1))
tail(add(x0, x1))
isempty(nil)
isempty(add(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule QUICKSORT(x) → IF_QS(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x))) at position [0] we obtained the following new rules:

QUICKSORT(add(x0, x1)) → IF_QS(false, low(head(add(x0, x1)), tail(add(x0, x1))), head(add(x0, x1)), high(head(add(x0, x1)), tail(add(x0, x1))))
QUICKSORT(nil) → IF_QS(true, low(head(nil), tail(nil)), head(nil), high(head(nil), tail(nil)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

QUICKSORT(nil) → IF_QS(true, low(head(nil), tail(nil)), head(nil), high(head(nil), tail(nil)))
QUICKSORT(add(x0, x1)) → IF_QS(false, low(head(add(x0, x1)), tail(add(x0, x1))), head(add(x0, x1)), high(head(add(x0, x1)), tail(add(x0, x1))))
IF_QS(false, x, n, y) → QUICKSORT(x)
IF_QS(false, x, n, y) → QUICKSORT(y)

The TRS R consists of the following rules:

isempty(nil) → true
isempty(add(n, x)) → false
head(add(n, x)) → n
tail(add(n, x)) → x
low(n, nil) → nil
if_low(false, n, add(m, x)) → low(n, x)
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
high(n, nil) → nil
if_high(true, n, add(m, x)) → high(n, x)
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
if_high(false, n, add(m, x)) → add(m, high(n, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
head(add(x0, x1))
tail(add(x0, x1))
isempty(nil)
isempty(add(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

QUICKSORT(add(x0, x1)) → IF_QS(false, low(head(add(x0, x1)), tail(add(x0, x1))), head(add(x0, x1)), high(head(add(x0, x1)), tail(add(x0, x1))))
IF_QS(false, x, n, y) → QUICKSORT(x)
IF_QS(false, x, n, y) → QUICKSORT(y)

The TRS R consists of the following rules:

isempty(nil) → true
isempty(add(n, x)) → false
head(add(n, x)) → n
tail(add(n, x)) → x
low(n, nil) → nil
if_low(false, n, add(m, x)) → low(n, x)
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
high(n, nil) → nil
if_high(true, n, add(m, x)) → high(n, x)
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
if_high(false, n, add(m, x)) → add(m, high(n, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
head(add(x0, x1))
tail(add(x0, x1))
isempty(nil)
isempty(add(x0, x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

QUICKSORT(add(x0, x1)) → IF_QS(false, low(head(add(x0, x1)), tail(add(x0, x1))), head(add(x0, x1)), high(head(add(x0, x1)), tail(add(x0, x1))))
IF_QS(false, x, n, y) → QUICKSORT(x)
IF_QS(false, x, n, y) → QUICKSORT(y)

The TRS R consists of the following rules:

head(add(n, x)) → n
tail(add(n, x)) → x
low(n, nil) → nil
if_low(false, n, add(m, x)) → low(n, x)
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
high(n, nil) → nil
if_high(true, n, add(m, x)) → high(n, x)
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
if_high(false, n, add(m, x)) → add(m, high(n, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
head(add(x0, x1))
tail(add(x0, x1))
isempty(nil)
isempty(add(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

isempty(nil)
isempty(add(x0, x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

QUICKSORT(add(x0, x1)) → IF_QS(false, low(head(add(x0, x1)), tail(add(x0, x1))), head(add(x0, x1)), high(head(add(x0, x1)), tail(add(x0, x1))))
IF_QS(false, x, n, y) → QUICKSORT(x)
IF_QS(false, x, n, y) → QUICKSORT(y)

The TRS R consists of the following rules:

head(add(n, x)) → n
tail(add(n, x)) → x
low(n, nil) → nil
if_low(false, n, add(m, x)) → low(n, x)
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
high(n, nil) → nil
if_high(true, n, add(m, x)) → high(n, x)
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
if_high(false, n, add(m, x)) → add(m, high(n, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
head(add(x0, x1))
tail(add(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule QUICKSORT(add(x0, x1)) → IF_QS(false, low(head(add(x0, x1)), tail(add(x0, x1))), head(add(x0, x1)), high(head(add(x0, x1)), tail(add(x0, x1)))) at position [1,0] we obtained the following new rules:

QUICKSORT(add(x0, x1)) → IF_QS(false, low(x0, tail(add(x0, x1))), head(add(x0, x1)), high(head(add(x0, x1)), tail(add(x0, x1))))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

QUICKSORT(add(x0, x1)) → IF_QS(false, low(x0, tail(add(x0, x1))), head(add(x0, x1)), high(head(add(x0, x1)), tail(add(x0, x1))))
IF_QS(false, x, n, y) → QUICKSORT(x)
IF_QS(false, x, n, y) → QUICKSORT(y)

The TRS R consists of the following rules:

head(add(n, x)) → n
tail(add(n, x)) → x
low(n, nil) → nil
if_low(false, n, add(m, x)) → low(n, x)
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
high(n, nil) → nil
if_high(true, n, add(m, x)) → high(n, x)
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
if_high(false, n, add(m, x)) → add(m, high(n, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
head(add(x0, x1))
tail(add(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule QUICKSORT(add(x0, x1)) → IF_QS(false, low(x0, tail(add(x0, x1))), head(add(x0, x1)), high(head(add(x0, x1)), tail(add(x0, x1)))) at position [1,1] we obtained the following new rules:

QUICKSORT(add(x0, x1)) → IF_QS(false, low(x0, x1), head(add(x0, x1)), high(head(add(x0, x1)), tail(add(x0, x1))))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

IF_QS(false, x, n, y) → QUICKSORT(x)
QUICKSORT(add(x0, x1)) → IF_QS(false, low(x0, x1), head(add(x0, x1)), high(head(add(x0, x1)), tail(add(x0, x1))))
IF_QS(false, x, n, y) → QUICKSORT(y)

The TRS R consists of the following rules:

head(add(n, x)) → n
tail(add(n, x)) → x
low(n, nil) → nil
if_low(false, n, add(m, x)) → low(n, x)
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
high(n, nil) → nil
if_high(true, n, add(m, x)) → high(n, x)
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
if_high(false, n, add(m, x)) → add(m, high(n, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
head(add(x0, x1))
tail(add(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule QUICKSORT(add(x0, x1)) → IF_QS(false, low(x0, x1), head(add(x0, x1)), high(head(add(x0, x1)), tail(add(x0, x1)))) at position [2] we obtained the following new rules:

QUICKSORT(add(x0, x1)) → IF_QS(false, low(x0, x1), x0, high(head(add(x0, x1)), tail(add(x0, x1))))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

QUICKSORT(add(x0, x1)) → IF_QS(false, low(x0, x1), x0, high(head(add(x0, x1)), tail(add(x0, x1))))
IF_QS(false, x, n, y) → QUICKSORT(x)
IF_QS(false, x, n, y) → QUICKSORT(y)

The TRS R consists of the following rules:

head(add(n, x)) → n
tail(add(n, x)) → x
low(n, nil) → nil
if_low(false, n, add(m, x)) → low(n, x)
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
high(n, nil) → nil
if_high(true, n, add(m, x)) → high(n, x)
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
if_high(false, n, add(m, x)) → add(m, high(n, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
head(add(x0, x1))
tail(add(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule QUICKSORT(add(x0, x1)) → IF_QS(false, low(x0, x1), x0, high(head(add(x0, x1)), tail(add(x0, x1)))) at position [3,0] we obtained the following new rules:

QUICKSORT(add(x0, x1)) → IF_QS(false, low(x0, x1), x0, high(x0, tail(add(x0, x1))))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

QUICKSORT(add(x0, x1)) → IF_QS(false, low(x0, x1), x0, high(x0, tail(add(x0, x1))))
IF_QS(false, x, n, y) → QUICKSORT(x)
IF_QS(false, x, n, y) → QUICKSORT(y)

The TRS R consists of the following rules:

head(add(n, x)) → n
tail(add(n, x)) → x
low(n, nil) → nil
if_low(false, n, add(m, x)) → low(n, x)
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
high(n, nil) → nil
if_high(true, n, add(m, x)) → high(n, x)
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
if_high(false, n, add(m, x)) → add(m, high(n, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
head(add(x0, x1))
tail(add(x0, x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

QUICKSORT(add(x0, x1)) → IF_QS(false, low(x0, x1), x0, high(x0, tail(add(x0, x1))))
IF_QS(false, x, n, y) → QUICKSORT(x)
IF_QS(false, x, n, y) → QUICKSORT(y)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
head(add(x0, x1))
tail(add(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

head(add(x0, x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

QUICKSORT(add(x0, x1)) → IF_QS(false, low(x0, x1), x0, high(x0, tail(add(x0, x1))))
IF_QS(false, x, n, y) → QUICKSORT(x)
IF_QS(false, x, n, y) → QUICKSORT(y)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
tail(add(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule QUICKSORT(add(x0, x1)) → IF_QS(false, low(x0, x1), x0, high(x0, tail(add(x0, x1)))) at position [3,1] we obtained the following new rules:

QUICKSORT(add(x0, x1)) → IF_QS(false, low(x0, x1), x0, high(x0, x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ Rewriting

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

IF_QS(false, x, n, y) → QUICKSORT(x)
QUICKSORT(add(x0, x1)) → IF_QS(false, low(x0, x1), x0, high(x0, x1))
IF_QS(false, x, n, y) → QUICKSORT(y)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
tail(add(x0, x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ Rewriting

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

IF_QS(false, x, n, y) → QUICKSORT(x)
QUICKSORT(add(x0, x1)) → IF_QS(false, low(x0, x1), x0, high(x0, x1))
IF_QS(false, x, n, y) → QUICKSORT(y)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
tail(add(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

tail(add(x0, x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ Rewriting

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

IF_QS(false, x, n, y) → QUICKSORT(x)
QUICKSORT(add(x0, x1)) → IF_QS(false, low(x0, x1), x0, high(x0, x1))
IF_QS(false, x, n, y) → QUICKSORT(y)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

QUICKSORT(add(x0, x1)) → IF_QS(false, low(x0, x1), x0, high(x0, x1))

The remaining pairs can at least be oriented weakly.

IF_QS(false, x, n, y) → QUICKSORT(x)
IF_QS(false, x, n, y) → QUICKSORT(y)

Used ordering: Polynomial interpretation [25,35]:

POL(high(x₁, x₂)) = x_2
POL(le(x₁, x₂)) = 0
POL(true) = 0
POL(QUICKSORT(x₁)) = x_1
POL(IF_QS(x₁, x₂, x₃, x₄)) = x_1 + x_2 + x_4
POL(0) = 3
POL(add(x₁, x₂)) = 1 + (4)x_2
POL(if_high(x₁, x₂, x₃)) = x_3
POL(low(x₁, x₂)) = (2)x_2
POL(false) = 0
POL(s(x₁)) = x_1
POL(nil) = 4
POL(if_low(x₁, x₂, x₃)) = (2)x_3

The value of delta used in the strict ordering is 1.
The following usable rules [17] were oriented:

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

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ UsableRulesProof

                                                          ↳ QDP

                                                            ↳ QReductionProof

                                                              ↳ QDP

                                                                ↳ Rewriting

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ QDPOrderProof

                                                                              ↳ QDP

                                                                                ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

IF_QS(false, x, n, y) → QUICKSORT(x)
IF_QS(false, x, n, y) → QUICKSORT(y)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 2 less nodes.