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:



↳ 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)

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
              ↳ 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)

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:



↳ 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)

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
              ↳ 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:



↳ 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)

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
              ↳ 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:



↳ 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)

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
              ↳ 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))

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
              ↳ 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))

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
              ↳ 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))

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
              ↳ 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(x1, x2)) = x_2   
POL(le(x1, x2)) = 0   
POL(true) = 0   
POL(QUICKSORT(x1)) = x_1   
POL(IF_QS(x1, x2, x3, x4)) = x_1 + x_2 + x_4   
POL(0) = 3   
POL(add(x1, x2)) = 1 + (4)x_2   
POL(if_high(x1, x2, x3)) = x_3   
POL(low(x1, x2)) = (2)x_2   
POL(false) = 0   
POL(s(x1)) = x_1   
POL(nil) = 4   
POL(if_low(x1, x2, x3)) = (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.