Termination proof of AG_#3.55

Termination of the given RelTRS could be proven:

0 RelTRS

↳1 RelTRStoRelADPProof (⇔, 0 ms)

↳2 RelADPP

↳3 RelADPDepGraphProof (⇔, 0 ms)

↳4 AND

    ↳5 RelADPP

        ↳6 RelADPCleverAfsProof (⇒, 231 ms)

        ↳7 QDP

        ↳8 QDPOrderProof (⇔, 24 ms)

        ↳9 QDP

        ↳10 PisEmptyProof (⇔, 0 ms)

        ↳11 YES

    ↳12 RelADPP

        ↳13 RelADPCleverAfsProof (⇒, 237 ms)

        ↳14 QDP

        ↳15 MRRProof (⇔, 9 ms)

        ↳16 QDP

        ↳17 MRRProof (⇔, 11 ms)

        ↳18 QDP

        ↳19 MRRProof (⇔, 0 ms)

        ↳20 QDP

        ↳21 QDPOrderProof (⇔, 13 ms)

        ↳22 QDP

        ↳23 PisEmptyProof (⇔, 0 ms)

        ↳24 YES

    ↳25 RelADPP

        ↳26 RelADPCleverAfsProof (⇒, 237 ms)

        ↳27 QDP

        ↳28 MRRProof (⇔, 4 ms)

        ↳29 QDP

        ↳30 MRRProof (⇔, 0 ms)

        ↳31 QDP

        ↳32 MRRProof (⇔, 0 ms)

        ↳33 QDP

        ↳34 MRRProof (⇔, 5 ms)

        ↳35 QDP

        ↳36 QDPOrderProof (⇔, 0 ms)

        ↳37 QDP

        ↳38 PisEmptyProof (⇔, 0 ms)

        ↳39 YES

    ↳40 RelADPP

        ↳41 RelADPCleverAfsProof (⇒, 201 ms)

        ↳42 QDP

        ↳43 QDPOrderProof (⇔, 28 ms)

        ↳44 QDP

        ↳45 DependencyGraphProof (⇔, 0 ms)

        ↳46 TRUE

    ↳47 RelADPP

        ↳48 RelADPCleverAfsProof (⇒, 200 ms)

        ↳49 QDP

        ↳50 QDPOrderProof (⇔, 32 ms)

        ↳51 QDP

        ↳52 PisEmptyProof (⇔, 0 ms)

        ↳53 YES

    ↳54 RelADPP

        ↳55 RelADPCleverAfsProof (⇒, 243 ms)

        ↳56 QDP

        ↳57 QDPOrderProof (⇔, 31 ms)

        ↳58 QDP

        ↳59 PisEmptyProof (⇔, 0 ms)

        ↳60 YES

    ↳61 RelADPP

        ↳62 RelADPCleverAfsProof (⇒, 237 ms)

        ↳63 QDP

        ↳64 MRRProof (⇔, 7 ms)

        ↳65 QDP

        ↳66 MRRProof (⇔, 10 ms)

        ↳67 QDP

        ↳68 MRRProof (⇔, 0 ms)

        ↳69 QDP

        ↳70 MRRProof (⇔, 0 ms)

        ↳71 QDP

        ↳72 QDPOrderProof (⇔, 6 ms)

        ↳73 QDP

        ↳74 PisEmptyProof (⇔, 0 ms)

        ↳75 YES

(0) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

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

The relative TRS consists of the following S rules:

rand(x) → rand(s(x))
rand(x) → x

(1) RelTRStoRelADPProof (EQUIVALENT transformation)

We upgrade the RelTRS problem to an equivalent Relative ADP Problem [IJCAR24].

(2) Obligation:

Relative ADP Problem with
absolute ADPs:

minus(x, 0) → x
minus(s(x), s(y)) → MINUS(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(QUOT(minus(x, y), s(y)))
quot(s(x), s(y)) → s(quot(MINUS(x, y), s(y)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → LE(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, APP(x, y))
low(n, nil) → nil
low(n, add(m, x)) → IF_LOW(le(m, n), n, add(m, x))
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))
high(n, add(m, x)) → if_high(LE(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → HIGH(n, x)
if_high(false, n, add(m, x)) → add(m, HIGH(n, x))
quicksort(nil) → nil
quicksort(add(n, x)) → APP(quicksort(low(n, x)), add(n, quicksort(high(n, x))))
quicksort(add(n, x)) → app(QUICKSORT(low(n, x)), add(n, quicksort(high(n, x))))
quicksort(add(n, x)) → app(quicksort(LOW(n, x)), add(n, quicksort(high(n, x))))
quicksort(add(n, x)) → app(quicksort(low(n, x)), add(n, QUICKSORT(high(n, x))))
quicksort(add(n, x)) → app(quicksort(low(n, x)), add(n, quicksort(HIGH(n, x))))

and relative ADPs:

rand(x) → RAND(s(x))
rand(x) → x

(3) RelADPDepGraphProof (EQUIVALENT transformation)

We use the relative dependency graph processor [IJCAR24].
The approximation of the Relative Dependency Graph contains:
7 SCCs with nodes from P_abs,
0 Lassos,
Result: This relative DT problem is equivalent to 7 subproblems.

(4) Complex Obligation (AND)

(5) Obligation:

Relative ADP Problem with
absolute ADPs:

quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
app(add(n, x), y) → add(n, APP(x, y))
le(s(x), s(y)) → le(x, y)
if_low(true, n, add(m, x)) → add(m, low(n, x))
le(s(x), 0) → false
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_low(false, n, add(m, x)) → low(n, x)
if_high(true, n, add(m, x)) → high(n, x)
quot(0, s(y)) → 0
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
low(n, nil) → nil
if_high(false, n, add(m, x)) → add(m, high(n, x))
app(nil, y) → y
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
quicksort(add(n, x)) → app(quicksort(low(n, x)), add(n, quicksort(high(n, x))))
minus(x, 0) → x
quicksort(nil) → nil

and relative ADPs:

rand(x) → rand(s(x))
rand(x) → x

(6) RelADPCleverAfsProof (SOUND transformation)

We use the first derelatifying processor [IJCAR24].
There are no annotations in relative ADPs, so the relative ADP problem can be transformed into a non-relative DP problem.

Furthermore, We use an argument filter [LPAR04].
Filtering:low_2 = 0 true = app_2 = add_2 = quicksort_1 = if_high_3 = 0, 1 rand_1 = APP_2 = 1 quot_2 = 0, 1 false = nil = s_1 = if_low_3 = 0, 1 le_2 = 0, 1 0 = minus_2 = 1 high_2 = 0
Found this filtering by looking at the following order that orders at least one DP strictly:Combined order from the following AFS and order.
APP(x1, x2) = APP(x1)
add(x1, x2) = add(x1, x2)
quot(x1, x2) = quot
s(x1) = x1
minus(x1, x2) = x1
le(x1, x2) = le
if_low(x1, x2, x3) = x3
true = true
low(x1, x2) = x2
0 = 0
false = false
high(x1, x2) = x2
nil = nil
if_high(x1, x2, x3) = x3
app(x1, x2) = app(x1, x2)
quicksort(x1) = quicksort(x1)

Recursive path order with status [RPO].
Quasi-Precedence:

APP₁ > nil
[quot, 0] > [le, true] > false > nil
quicksort₁ > [add₂, app₂] > [le, true] > false > nil

Status:

APP₁: multiset
add₂: [1,2]
quot: []
le: multiset
true: multiset
0: multiset
false: multiset
nil: multiset
app₂: [1,2]
quicksort₁: multiset

(7) Obligation:

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

APP(add0(n, x)) → APP(x)

The TRS R consists of the following rules:

quot → s0(quot)
le → le
if_low(add0(m, x)) → add0(m, low(x))
le → false0
high(nil0) → nil0
high(add0(m, x)) → if_high(add0(m, x))
rand0(x) → rand0(s0(x))
if_low(add0(m, x)) → low(x)
if_high(add0(m, x)) → high(x)
quot → 00
low(add0(m, x)) → if_low(add0(m, x))
low(nil0) → nil0
if_high(add0(m, x)) → add0(m, high(x))
app0(add0(n, x), y) → add0(n, app0(x, y))
app0(nil0, y) → y
minus(s0(x)) → minus(x)
le → true0
quicksort0(add0(n, x)) → app0(quicksort0(low(x)), add0(n, quicksort0(high(x))))
minus(x) → x
quicksort0(nil0) → nil0
rand0(x) → x

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

(8) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

APP(add0(n, x)) → APP(x)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
APP(x1) = APP(x1)
add0(x1, x2) = add0(x1, x2)
quot = quot
s0(x1) = x1
le = le
if_low(x1) = if_low(x1)
low(x1) = low(x1)
false0 = false0
high(x1) = x1
nil0 = nil0
if_high(x1) = x1
rand0(x1) = x1
00 = 00
app0(x1, x2) = app0(x1, x2)
minus(x1) = minus(x1)
true0 = true0
quicksort0(x1) = quicksort0(x1)

Recursive path order with status [RPO].
Quasi-Precedence:

quot > 00 > [APP₁, add0₂, if_low₁, low₁]
[le, false0] > true0 > [APP₁, add0₂, if_low₁, low₁]
minus₁ > [APP₁, add0₂, if_low₁, low₁]
quicksort0₁ > nil0 > [APP₁, add0₂, if_low₁, low₁]
quicksort0₁ > app0₂ > [APP₁, add0₂, if_low₁, low₁]

Status:

APP₁: multiset
add0₂: multiset
quot: multiset
le: multiset
if_low₁: multiset
low₁: multiset
false0: multiset
nil0: multiset
00: multiset
app0₂: [1,2]
minus₁: [1]
true0: multiset
quicksort0₁: multiset

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

quot → s0(quot)
le → le
if_low(add0(m, x)) → add0(m, low(x))
le → false0
high(nil0) → nil0
high(add0(m, x)) → if_high(add0(m, x))
rand0(x) → rand0(s0(x))
if_low(add0(m, x)) → low(x)
if_high(add0(m, x)) → high(x)
quot → 00
low(add0(m, x)) → if_low(add0(m, x))
low(nil0) → nil0
if_high(add0(m, x)) → add0(m, high(x))
app0(add0(n, x), y) → add0(n, app0(x, y))
app0(nil0, y) → y
minus(s0(x)) → minus(x)
le → true0
quicksort0(add0(n, x)) → app0(quicksort0(low(x)), add0(n, quicksort0(high(x))))
minus(x) → x
quicksort0(nil0) → nil0
rand0(x) → x

(9) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

quot → s0(quot)
le → le
if_low(add0(m, x)) → add0(m, low(x))
le → false0
high(nil0) → nil0
high(add0(m, x)) → if_high(add0(m, x))
rand0(x) → rand0(s0(x))
if_low(add0(m, x)) → low(x)
if_high(add0(m, x)) → high(x)
quot → 00
low(add0(m, x)) → if_low(add0(m, x))
low(nil0) → nil0
if_high(add0(m, x)) → add0(m, high(x))
app0(add0(n, x), y) → add0(n, app0(x, y))
app0(nil0, y) → y
minus(s0(x)) → minus(x)
le → true0
quicksort0(add0(n, x)) → app0(quicksort0(low(x)), add0(n, quicksort0(high(x))))
minus(x) → x
quicksort0(nil0) → nil0
rand0(x) → x

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

(10) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(11) YES

(12) Obligation:

Relative ADP Problem with
absolute ADPs:

quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
le(s(x), s(y)) → le(x, y)
if_low(true, n, add(m, x)) → add(m, low(n, x))
le(s(x), 0) → false
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_low(false, n, add(m, x)) → low(n, x)
if_high(true, n, add(m, x)) → high(n, x)
quot(0, s(y)) → 0
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
low(n, nil) → nil
if_high(false, n, add(m, x)) → add(m, high(n, x))
app(add(n, x), y) → add(n, app(x, y))
app(nil, y) → y
le(0, y) → true
quicksort(add(n, x)) → app(quicksort(low(n, x)), add(n, quicksort(high(n, x))))
minus(x, 0) → x
minus(s(x), s(y)) → MINUS(x, y)
quicksort(nil) → nil

and relative ADPs:

rand(x) → rand(s(x))
rand(x) → x

(13) RelADPCleverAfsProof (SOUND transformation)

We use the first derelatifying processor [IJCAR24].
There are no annotations in relative ADPs, so the relative ADP problem can be transformed into a non-relative DP problem.

Furthermore, We use an argument filter [LPAR04].
Filtering:low_2 = 0, 1 MINUS_2 = true = add_2 = 0 app_2 = 0 quicksort_1 = if_high_3 = 0, 1, 2 rand_1 = quot_2 = 1 false = nil = s_1 = if_low_3 = 0, 1, 2 le_2 = 1 0 = minus_2 = 1 high_2 = 0, 1
Found this filtering by looking at the following order that orders at least one DP strictly:Combined order from the following AFS and order.
MINUS(x1, x2) = MINUS(x1, x2)
s(x1) = s(x1)
quot(x1, x2) = x1
minus(x1, x2) = x1
le(x1, x2) = x1
if_low(x1, x2, x3) = if_low
true = true
add(x1, x2) = x2
low(x1, x2) = low
0 = 0
false = false
high(x1, x2) = high
nil = nil
if_high(x1, x2, x3) = if_high
app(x1, x2) = x2
quicksort(x1) = quicksort(x1)

Recursive path order with status [RPO].
Quasi-Precedence:

MINUS₂ > [if_low, true, low, false, high, nil, if_high]
s₁ > [if_low, true, low, false, high, nil, if_high]
0 > [if_low, true, low, false, high, nil, if_high]
quicksort₁ > [if_low, true, low, false, high, nil, if_high]

Status:

MINUS₂: [2,1]
s₁: [1]
if_low: []
true: multiset
low: []
0: multiset
false: multiset
high: []
nil: multiset
if_high: []
quicksort₁: multiset

(14) Obligation:

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

MINUS0(s0(x), s0(y)) → MINUS0(x, y)

The TRS R consists of the following rules:

quot(s0(x)) → s0(quot(minus(x)))
le(s0(x)) → le(x)
if_low → add(low)
le(s0(x)) → false0
high → nil0
high → if_high
rand0(x) → rand0(s0(x))
if_low → low
if_high → high
quot(00) → 00
low → if_low
low → nil0
if_high → add(high)
app(y) → add(app(y))
app(y) → y
minus(s0(x)) → minus(x)
le(00) → true0
quicksort0(add(x)) → app(add(quicksort0(high)))
minus(x) → x
quicksort0(nil0) → nil0
rand0(x) → x

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

(15) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.

Strictly oriented rules of the TRS R:

low → nil0
rand0(x) → x

Used ordering: Polynomial interpretation [POLO]:

POL(00) = 0
POL(MINUS0(x₁, x₂)) = x₁ + x₂
POL(add(x₁)) = x₁
POL(app(x₁)) = 2·x₁
POL(false0) = 0
POL(high) = 0
POL(if_high) = 0
POL(if_low) = 2
POL(le(x₁)) = 2·x₁
POL(low) = 2
POL(minus(x₁)) = x₁
POL(nil0) = 0
POL(quicksort0(x₁)) = x₁
POL(quot(x₁)) = x₁
POL(rand0(x₁)) = 2 + x₁
POL(s0(x₁)) = x₁
POL(true0) = 0

(16) Obligation:

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

MINUS0(s0(x), s0(y)) → MINUS0(x, y)

The TRS R consists of the following rules:

quot(s0(x)) → s0(quot(minus(x)))
le(s0(x)) → le(x)
if_low → add(low)
le(s0(x)) → false0
high → nil0
high → if_high
rand0(x) → rand0(s0(x))
if_low → low
if_high → high
quot(00) → 00
low → if_low
if_high → add(high)
app(y) → add(app(y))
app(y) → y
minus(s0(x)) → minus(x)
le(00) → true0
quicksort0(add(x)) → app(add(quicksort0(high)))
minus(x) → x
quicksort0(nil0) → nil0

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

(17) MRRProof (EQUIVALENT transformation)

le(s0(x)) → false0
quot(00) → 00
le(00) → true0

Used ordering: Polynomial interpretation [POLO]:

POL(00) = 0
POL(MINUS0(x₁, x₂)) = x₁ + x₂
POL(add(x₁)) = x₁
POL(app(x₁)) = x₁
POL(false0) = 1
POL(high) = 0
POL(if_high) = 0
POL(if_low) = 0
POL(le(x₁)) = 2 + x₁
POL(low) = 0
POL(minus(x₁)) = x₁
POL(nil0) = 0
POL(quicksort0(x₁)) = 2·x₁
POL(quot(x₁)) = 1 + 2·x₁
POL(rand0(x₁)) = x₁
POL(s0(x₁)) = x₁
POL(true0) = 1

(18) Obligation:

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

MINUS0(s0(x), s0(y)) → MINUS0(x, y)

The TRS R consists of the following rules:

quot(s0(x)) → s0(quot(minus(x)))
le(s0(x)) → le(x)
if_low → add(low)
high → nil0
high → if_high
rand0(x) → rand0(s0(x))
if_low → low
if_high → high
low → if_low
if_high → add(high)
app(y) → add(app(y))
app(y) → y
minus(s0(x)) → minus(x)
quicksort0(add(x)) → app(add(quicksort0(high)))
minus(x) → x
quicksort0(nil0) → nil0

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

(19) MRRProof (EQUIVALENT transformation)

quicksort0(nil0) → nil0

Used ordering: Polynomial interpretation [POLO]:

POL(MINUS0(x₁, x₂)) = x₁ + x₂
POL(add(x₁)) = x₁
POL(app(x₁)) = x₁
POL(high) = 0
POL(if_high) = 0
POL(if_low) = 0
POL(le(x₁)) = x₁
POL(low) = 0
POL(minus(x₁)) = x₁
POL(nil0) = 0
POL(quicksort0(x₁)) = 2 + x₁
POL(quot(x₁)) = x₁
POL(rand0(x₁)) = x₁
POL(s0(x₁)) = x₁

(20) Obligation:

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

MINUS0(s0(x), s0(y)) → MINUS0(x, y)

The TRS R consists of the following rules:

quot(s0(x)) → s0(quot(minus(x)))
le(s0(x)) → le(x)
if_low → add(low)
high → nil0
high → if_high
rand0(x) → rand0(s0(x))
if_low → low
if_high → high
low → if_low
if_high → add(high)
app(y) → add(app(y))
app(y) → y
minus(s0(x)) → minus(x)
quicksort0(add(x)) → app(add(quicksort0(high)))
minus(x) → x

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

(21) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

MINUS0(s0(x), s0(y)) → MINUS0(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( quot(x₁) ) = max{0, 2x₁ - 1}

POL( s0(x₁) ) = x₁ + 2

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

POL( le(x₁) ) = 0

POL( if_low ) = 2

POL( add(x₁) ) = 2

POL( low ) = 2

POL( high ) = 2

POL( nil0 ) = 2

POL( if_high ) = 2

POL( rand0(x₁) ) = max{0, -2}

POL( app(x₁) ) = x₁ + 2

POL( quicksort0(x₁) ) = 2x₁

POL( MINUS0(x₁, x₂) ) = 2x₁ + 2x₂

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

quot(s0(x)) → s0(quot(minus(x)))
le(s0(x)) → le(x)
if_low → add(low)
high → nil0
high → if_high
rand0(x) → rand0(s0(x))
if_low → low
if_high → high
low → if_low
if_high → add(high)
app(y) → add(app(y))
app(y) → y
minus(s0(x)) → minus(x)
quicksort0(add(x)) → app(add(quicksort0(high)))
minus(x) → x

(22) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

quot(s0(x)) → s0(quot(minus(x)))
le(s0(x)) → le(x)
if_low → add(low)
high → nil0
high → if_high
rand0(x) → rand0(s0(x))
if_low → low
if_high → high
low → if_low
if_high → add(high)
app(y) → add(app(y))
app(y) → y
minus(s0(x)) → minus(x)
quicksort0(add(x)) → app(add(quicksort0(high)))
minus(x) → x

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

(23) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(24) YES

(25) Obligation:

Relative ADP Problem with
absolute ADPs:

quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
if_low(true, n, add(m, x)) → add(m, low(n, x))
le(s(x), 0) → false
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_low(false, n, add(m, x)) → low(n, x)
if_high(true, n, add(m, x)) → high(n, x)
le(s(x), s(y)) → LE(x, y)
quot(0, s(y)) → 0
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
low(n, nil) → nil
if_high(false, n, add(m, x)) → add(m, high(n, x))
app(add(n, x), y) → add(n, app(x, y))
app(nil, y) → y
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
quicksort(add(n, x)) → app(quicksort(low(n, x)), add(n, quicksort(high(n, x))))
minus(x, 0) → x
quicksort(nil) → nil

and relative ADPs:

rand(x) → rand(s(x))
rand(x) → x

(26) RelADPCleverAfsProof (SOUND transformation)

We use the first derelatifying processor [IJCAR24].
There are no annotations in relative ADPs, so the relative ADP problem can be transformed into a non-relative DP problem.

Furthermore, We use an argument filter [LPAR04].
Filtering:low_2 = 0, 1 true = add_2 = 0 app_2 = 0 quicksort_1 = if_high_3 = 0, 1 rand_1 = quot_2 = 1 false = nil = s_1 = if_low_3 = 0, 1, 2 LE_2 = le_2 = 0, 1 0 = minus_2 = 1 high_2 = 0
Found this filtering by looking at the following order that orders at least one DP strictly:Combined order from the following AFS and order.
LE(x1, x2) = LE(x1, x2)
s(x1) = s(x1)
quot(x1, x2) = x1
minus(x1, x2) = x1
le(x1, x2) = le
if_low(x1, x2, x3) = if_low
true = true
add(x1, x2) = x2
low(x1, x2) = low
0 = 0
false = false
high(x1, x2) = x2
nil = nil
if_high(x1, x2, x3) = x3
app(x1, x2) = x2
quicksort(x1) = x1

Recursive path order with status [RPO].
Quasi-Precedence:

[if_low, low] > [le, false] > true
[if_low, low] > nil
0 > [le, false] > true

Status:

LE₂: multiset
s₁: multiset
le: []
if_low: multiset
true: multiset
low: multiset
0: multiset
false: multiset
nil: multiset

(27) Obligation:

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

LE0(s0(x), s0(y)) → LE0(x, y)

The TRS R consists of the following rules:

quot(s0(x)) → s0(quot(minus(x)))
le → le
if_low → add(low)
le → false0
high(nil0) → nil0
high(add(x)) → if_high(add(x))
rand0(x) → rand0(s0(x))
if_low → low
if_high(add(x)) → high(x)
quot(00) → 00
low → if_low
low → nil0
if_high(add(x)) → add(high(x))
app(y) → add(app(y))
app(y) → y
minus(s0(x)) → minus(x)
le → true0
quicksort0(add(x)) → app(add(quicksort0(high(x))))
minus(x) → x
quicksort0(nil0) → nil0
rand0(x) → x

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

(28) MRRProof (EQUIVALENT transformation)

le → false0
rand0(x) → x

Used ordering: Polynomial interpretation [POLO]:

POL(00) = 0
POL(LE0(x₁, x₂)) = x₁ + x₂
POL(add(x₁)) = x₁
POL(app(x₁)) = x₁
POL(false0) = 0
POL(high(x₁)) = x₁
POL(if_high(x₁)) = x₁
POL(if_low) = 0
POL(le) = 2
POL(low) = 0
POL(minus(x₁)) = x₁
POL(nil0) = 0
POL(quicksort0(x₁)) = 2·x₁
POL(quot(x₁)) = x₁
POL(rand0(x₁)) = 2 + x₁
POL(s0(x₁)) = x₁
POL(true0) = 2

(29) Obligation:

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

LE0(s0(x), s0(y)) → LE0(x, y)

The TRS R consists of the following rules:

quot(s0(x)) → s0(quot(minus(x)))
le → le
if_low → add(low)
high(nil0) → nil0
high(add(x)) → if_high(add(x))
rand0(x) → rand0(s0(x))
if_low → low
if_high(add(x)) → high(x)
quot(00) → 00
low → if_low
low → nil0
if_high(add(x)) → add(high(x))
app(y) → add(app(y))
app(y) → y
minus(s0(x)) → minus(x)
le → true0
quicksort0(add(x)) → app(add(quicksort0(high(x))))
minus(x) → x
quicksort0(nil0) → nil0

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

(30) MRRProof (EQUIVALENT transformation)

le → true0

Used ordering: Polynomial interpretation [POLO]:

POL(00) = 0
POL(LE0(x₁, x₂)) = x₁ + x₂
POL(add(x₁)) = x₁
POL(app(x₁)) = x₁
POL(high(x₁)) = x₁
POL(if_high(x₁)) = x₁
POL(if_low) = 0
POL(le) = 2
POL(low) = 0
POL(minus(x₁)) = x₁
POL(nil0) = 0
POL(quicksort0(x₁)) = 2·x₁
POL(quot(x₁)) = x₁
POL(rand0(x₁)) = x₁
POL(s0(x₁)) = x₁
POL(true0) = 1

(31) Obligation:

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

LE0(s0(x), s0(y)) → LE0(x, y)

The TRS R consists of the following rules:

quot(s0(x)) → s0(quot(minus(x)))
le → le
if_low → add(low)
high(nil0) → nil0
high(add(x)) → if_high(add(x))
rand0(x) → rand0(s0(x))
if_low → low
if_high(add(x)) → high(x)
quot(00) → 00
low → if_low
low → nil0
if_high(add(x)) → add(high(x))
app(y) → add(app(y))
app(y) → y
minus(s0(x)) → minus(x)
quicksort0(add(x)) → app(add(quicksort0(high(x))))
minus(x) → x
quicksort0(nil0) → nil0

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

(32) MRRProof (EQUIVALENT transformation)

quot(00) → 00
quicksort0(nil0) → nil0

Used ordering: Polynomial interpretation [POLO]:

POL(00) = 1
POL(LE0(x₁, x₂)) = x₁ + x₂
POL(add(x₁)) = x₁
POL(app(x₁)) = x₁
POL(high(x₁)) = x₁
POL(if_high(x₁)) = x₁
POL(if_low) = 2
POL(le) = 0
POL(low) = 2
POL(minus(x₁)) = x₁
POL(nil0) = 2
POL(quicksort0(x₁)) = 2 + x₁
POL(quot(x₁)) = 2 + 2·x₁
POL(rand0(x₁)) = x₁
POL(s0(x₁)) = x₁

(33) Obligation:

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

LE0(s0(x), s0(y)) → LE0(x, y)

The TRS R consists of the following rules:

quot(s0(x)) → s0(quot(minus(x)))
le → le
if_low → add(low)
high(nil0) → nil0
high(add(x)) → if_high(add(x))
rand0(x) → rand0(s0(x))
if_low → low
if_high(add(x)) → high(x)
low → if_low
low → nil0
if_high(add(x)) → add(high(x))
app(y) → add(app(y))
app(y) → y
minus(s0(x)) → minus(x)
quicksort0(add(x)) → app(add(quicksort0(high(x))))
minus(x) → x

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

(34) MRRProof (EQUIVALENT transformation)

low → nil0

Used ordering: Polynomial interpretation [POLO]:

POL(LE0(x₁, x₂)) = x₁ + x₂
POL(add(x₁)) = x₁
POL(app(x₁)) = x₁
POL(high(x₁)) = x₁
POL(if_high(x₁)) = x₁
POL(if_low) = 2
POL(le) = 0
POL(low) = 2
POL(minus(x₁)) = x₁
POL(nil0) = 0
POL(quicksort0(x₁)) = x₁
POL(quot(x₁)) = 2 + x₁
POL(rand0(x₁)) = x₁
POL(s0(x₁)) = x₁

(35) Obligation:

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

LE0(s0(x), s0(y)) → LE0(x, y)

The TRS R consists of the following rules:

quot(s0(x)) → s0(quot(minus(x)))
le → le
if_low → add(low)
high(nil0) → nil0
high(add(x)) → if_high(add(x))
rand0(x) → rand0(s0(x))
if_low → low
if_high(add(x)) → high(x)
low → if_low
if_high(add(x)) → add(high(x))
app(y) → add(app(y))
app(y) → y
minus(s0(x)) → minus(x)
quicksort0(add(x)) → app(add(quicksort0(high(x))))
minus(x) → x

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

(36) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

LE0(s0(x), s0(y)) → LE0(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
LE0(x1, x2) = LE0(x1, x2)
s0(x1) = s0(x1)
quot(x1) = quot(x1)
minus(x1) = minus(x1)
le = le
if_low = if_low
add(x1) = x1
low = low
high(x1) = x1
nil0 = nil0
if_high(x1) = x1
rand0(x1) = rand0
app(x1) = x1
quicksort0(x1) = x1

Recursive path order with status [RPO].
Quasi-Precedence:

quot₁ > s0₁ > LE0₂
quot₁ > s0₁ > minus₁
[if_low, low]
rand0 > s0₁ > LE0₂
rand0 > s0₁ > minus₁

Status:

LE0₂: [2,1]
s0₁: multiset
quot₁: multiset
minus₁: multiset
le: multiset
if_low: multiset
low: multiset
nil0: multiset
rand0: []

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

quot(s0(x)) → s0(quot(minus(x)))
le → le
if_low → add(low)
high(nil0) → nil0
high(add(x)) → if_high(add(x))
rand0(x) → rand0(s0(x))
if_low → low
if_high(add(x)) → high(x)
low → if_low
if_high(add(x)) → add(high(x))
app(y) → add(app(y))
app(y) → y
minus(s0(x)) → minus(x)
quicksort0(add(x)) → app(add(quicksort0(high(x))))
minus(x) → x

(37) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

quot(s0(x)) → s0(quot(minus(x)))
le → le
if_low → add(low)
high(nil0) → nil0
high(add(x)) → if_high(add(x))
rand0(x) → rand0(s0(x))
if_low → low
if_high(add(x)) → high(x)
low → if_low
if_high(add(x)) → add(high(x))
app(y) → add(app(y))
app(y) → y
minus(s0(x)) → minus(x)
quicksort0(add(x)) → app(add(quicksort0(high(x))))
minus(x) → x

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

(38) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(39) YES

(40) Obligation:

Relative ADP Problem with
absolute ADPs:

quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
le(s(x), s(y)) → le(x, y)
le(s(x), 0) → false
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)
low(n, add(m, x)) → IF_LOW(le(m, n), n, add(m, x))
quot(0, s(y)) → 0
if_low(false, n, add(m, x)) → LOW(n, x)
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
low(n, nil) → nil
if_high(false, n, add(m, x)) → add(m, high(n, x))
app(add(n, x), y) → add(n, app(x, y))
app(nil, y) → y
if_low(true, n, add(m, x)) → add(m, LOW(n, x))
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
quicksort(add(n, x)) → app(quicksort(low(n, x)), add(n, quicksort(high(n, x))))
minus(x, 0) → x
quicksort(nil) → nil

and relative ADPs:

rand(x) → rand(s(x))
rand(x) → x

(41) RelADPCleverAfsProof (SOUND transformation)

We use the first derelatifying processor [IJCAR24].
There are no annotations in relative ADPs, so the relative ADP problem can be transformed into a non-relative DP problem.

Furthermore, We use an argument filter [LPAR04].
Filtering:low_2 = 0 true = add_2 = 0 app_2 = IF_LOW_3 = 0 quicksort_1 = if_high_3 = 0, 1 rand_1 = quot_2 = false = nil = s_1 = if_low_3 = 0, 1 le_2 = 0, 1 0 = minus_2 = 1 high_2 = 0 LOW_2 =
Found this filtering by looking at the following order that orders at least one DP strictly:Combined order from the following AFS and order.
IF_LOW(x1, x2, x3) = IF_LOW(x2, x3)
false = false
add(x1, x2) = add(x2)
LOW(x1, x2) = LOW(x1, x2)
true = true
le(x1, x2) = le
quot(x1, x2) = quot(x1, x2)
s(x1) = s(x1)
minus(x1, x2) = minus(x1)
if_low(x1, x2, x3) = x3
low(x1, x2) = x2
0 = 0
high(x1, x2) = x2
nil = nil
if_high(x1, x2, x3) = x3
app(x1, x2) = app(x1, x2)
quicksort(x1) = quicksort(x1)

Recursive path order with status [RPO].
Quasi-Precedence:

[true, le] > add₁ > [IF_LOW₂, LOW₂] > [false, 0]
quot₂ > s₁ > minus₁ > [false, 0]
quicksort₁ > nil > [false, 0]
quicksort₁ > app₂ > add₁ > [IF_LOW₂, LOW₂] > [false, 0]

Status:

IF_LOW₂: multiset
false: multiset
add₁: multiset
LOW₂: multiset
true: multiset
le: []
quot₂: [2,1]
s₁: multiset
minus₁: [1]
0: multiset
nil: multiset
app₂: multiset
quicksort₁: [1]

(42) Obligation:

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

IF_LOW(n, add(x)) → LOW0(n, x)
LOW0(n, add(x)) → IF_LOW(n, add(x))

The TRS R consists of the following rules:

quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
le → le
if_low(add(x)) → add(low(x))
le → false0
high(nil0) → nil0
high(add(x)) → if_high(add(x))
rand0(x) → rand0(s0(x))
if_low(add(x)) → low(x)
if_high(add(x)) → high(x)
quot0(00, s0(y)) → 00
low(add(x)) → if_low(add(x))
low(nil0) → nil0
if_high(add(x)) → add(high(x))
app0(add(x), y) → add(app0(x, y))
app0(nil0, y) → y
minus(s0(x)) → minus(x)
le → true0
quicksort0(add(x)) → app0(quicksort0(low(x)), add(quicksort0(high(x))))
minus(x) → x
quicksort0(nil0) → nil0
rand0(x) → x

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

(43) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

IF_LOW(n, add(x)) → LOW0(n, x)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
IF_LOW(x1, x2) = IF_LOW(x2)
add(x1) = add(x1)
LOW0(x1, x2) = LOW0(x2)
quot0(x1, x2) = quot0
s0(x1) = x1
minus(x1) = minus(x1)
le = le
if_low(x1) = x1
low(x1) = x1
false0 = false0
high(x1) = x1
nil0 = nil0
if_high(x1) = x1
rand0(x1) = x1
00 = 00
app0(x1, x2) = app0(x1, x2)
true0 = true0
quicksort0(x1) = quicksort0(x1)

Recursive path order with status [RPO].
Quasi-Precedence:

[quot0, 00] > minus₁ > [IF_LOW₁, LOW0₁]
le > false0 > [IF_LOW₁, LOW0₁]
le > true0 > [IF_LOW₁, LOW0₁]
quicksort0₁ > nil0 > [IF_LOW₁, LOW0₁]
quicksort0₁ > app0₂ > add₁ > [IF_LOW₁, LOW0₁]

Status:

IF_LOW₁: [1]
add₁: [1]
LOW0₁: [1]
quot0: []
minus₁: [1]
le: multiset
false0: multiset
nil0: multiset
00: multiset
app0₂: [2,1]
true0: multiset
quicksort0₁: multiset

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
le → le
if_low(add(x)) → add(low(x))
le → false0
high(nil0) → nil0
high(add(x)) → if_high(add(x))
rand0(x) → rand0(s0(x))
if_low(add(x)) → low(x)
if_high(add(x)) → high(x)
quot0(00, s0(y)) → 00
low(add(x)) → if_low(add(x))
low(nil0) → nil0
if_high(add(x)) → add(high(x))
app0(add(x), y) → add(app0(x, y))
app0(nil0, y) → y
minus(s0(x)) → minus(x)
le → true0
quicksort0(add(x)) → app0(quicksort0(low(x)), add(quicksort0(high(x))))
minus(x) → x
quicksort0(nil0) → nil0
rand0(x) → x

(44) Obligation:

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

LOW0(n, add(x)) → IF_LOW(n, add(x))

The TRS R consists of the following rules:

quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
le → le
if_low(add(x)) → add(low(x))
le → false0
high(nil0) → nil0
high(add(x)) → if_high(add(x))
rand0(x) → rand0(s0(x))
if_low(add(x)) → low(x)
if_high(add(x)) → high(x)
quot0(00, s0(y)) → 00
low(add(x)) → if_low(add(x))
low(nil0) → nil0
if_high(add(x)) → add(high(x))
app0(add(x), y) → add(app0(x, y))
app0(nil0, y) → y
minus(s0(x)) → minus(x)
le → true0
quicksort0(add(x)) → app0(quicksort0(low(x)), add(quicksort0(high(x))))
minus(x) → x
quicksort0(nil0) → nil0
rand0(x) → x

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

(45) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(46) TRUE

(47) Obligation:

Relative ADP Problem with
absolute ADPs:

quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
if_high(false, n, add(m, x)) → add(m, HIGH(n, x))
le(s(x), s(y)) → le(x, y)
if_low(true, n, add(m, x)) → add(m, low(n, x))
le(s(x), 0) → false
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_low(false, n, add(m, x)) → low(n, x)
quot(0, s(y)) → 0
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
low(n, nil) → nil
app(add(n, x), y) → add(n, app(x, y))
if_high(true, n, add(m, x)) → HIGH(n, x)
app(nil, y) → y
high(n, add(m, x)) → IF_HIGH(le(m, n), n, add(m, x))
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
quicksort(add(n, x)) → app(quicksort(low(n, x)), add(n, quicksort(high(n, x))))
minus(x, 0) → x
quicksort(nil) → nil

and relative ADPs:

rand(x) → rand(s(x))
rand(x) → x

(48) RelADPCleverAfsProof (SOUND transformation)

We use the first derelatifying processor [IJCAR24].
There are no annotations in relative ADPs, so the relative ADP problem can be transformed into a non-relative DP problem.

Furthermore, We use an argument filter [LPAR04].
Filtering:HIGH_2 = 0 low_2 = 0 true = IF_HIGH_3 = 1 add_2 = app_2 = quicksort_1 = if_high_3 = 0, 1 rand_1 = quot_2 = false = nil = s_1 = if_low_3 = 0, 1 le_2 = 1 0 = minus_2 = 1 high_2 = 0
Found this filtering by looking at the following order that orders at least one DP strictly:Combined order from the following AFS and order.
IF_HIGH(x1, x2, x3) = IF_HIGH(x1, x3)
true = true
add(x1, x2) = add(x1, x2)
HIGH(x1, x2) = HIGH(x2)
le(x1, x2) = le(x1)
false = false
quot(x1, x2) = quot(x1, x2)
s(x1) = x1
minus(x1, x2) = x1
if_low(x1, x2, x3) = x3
low(x1, x2) = x2
0 = 0
high(x1, x2) = x2
nil = nil
if_high(x1, x2, x3) = x3
app(x1, x2) = app(x1, x2)
quicksort(x1) = quicksort(x1)

Recursive path order with status [RPO].
Quasi-Precedence:

0 > true > [add₂, HIGH₁, le₁] > IF_HIGH₂
0 > true > [add₂, HIGH₁, le₁] > false
[nil, quicksort₁] > app₂ > [add₂, HIGH₁, le₁] > IF_HIGH₂
[nil, quicksort₁] > app₂ > [add₂, HIGH₁, le₁] > false

Status:

IF_HIGH₂: multiset
true: multiset
add₂: multiset
HIGH₁: multiset
le₁: multiset
false: multiset
quot₂: [1,2]
0: multiset
nil: multiset
app₂: multiset
quicksort₁: [1]

(49) Obligation:

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

IF_HIGH(true0, add0(m, x)) → HIGH(x)
HIGH(add0(m, x)) → IF_HIGH(le(m), add0(m, x))
IF_HIGH(false0, add0(m, x)) → HIGH(x)

The TRS R consists of the following rules:

quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
le(s0(x)) → le(x)
if_low(add0(m, x)) → add0(m, low(x))
le(s0(x)) → false0
high(nil0) → nil0
high(add0(m, x)) → if_high(add0(m, x))
rand0(x) → rand0(s0(x))
if_low(add0(m, x)) → low(x)
if_high(add0(m, x)) → high(x)
quot0(00, s0(y)) → 00
low(add0(m, x)) → if_low(add0(m, x))
low(nil0) → nil0
if_high(add0(m, x)) → add0(m, high(x))
app0(add0(n, x), y) → add0(n, app0(x, y))
app0(nil0, y) → y
minus(s0(x)) → minus(x)
le(00) → true0
quicksort0(add0(n, x)) → app0(quicksort0(low(x)), add0(n, quicksort0(high(x))))
minus(x) → x
quicksort0(nil0) → nil0
rand0(x) → x

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

(50) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

IF_HIGH(true0, add0(m, x)) → HIGH(x)
HIGH(add0(m, x)) → IF_HIGH(le(m), add0(m, x))
IF_HIGH(false0, add0(m, x)) → HIGH(x)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
IF_HIGH(x1, x2) = IF_HIGH(x1, x2)
true0 = true0
add0(x1, x2) = add0(x2)
HIGH(x1) = HIGH(x1)
le(x1) = le
false0 = false0
quot0(x1, x2) = x2
s0(x1) = x1
minus(x1) = x1
if_low(x1) = x1
low(x1) = x1
high(x1) = x1
nil0 = nil0
if_high(x1) = x1
rand0(x1) = x1
00 = 00
app0(x1, x2) = app0(x1, x2)
quicksort0(x1) = quicksort0(x1)

Recursive path order with status [RPO].
Quasi-Precedence:

nil0 > [IF_HIGH₂, 00]
quicksort0₁ > app0₂ > [true0, add0₁, HIGH₁, le] > false0 > [IF_HIGH₂, 00]

Status:

IF_HIGH₂: [1,2]
true0: multiset
add0₁: multiset
HIGH₁: multiset
le: multiset
false0: multiset
nil0: multiset
00: multiset
app0₂: multiset
quicksort0₁: multiset

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
le(s0(x)) → le(x)
if_low(add0(m, x)) → add0(m, low(x))
le(s0(x)) → false0
high(nil0) → nil0
high(add0(m, x)) → if_high(add0(m, x))
rand0(x) → rand0(s0(x))
if_low(add0(m, x)) → low(x)
if_high(add0(m, x)) → high(x)
quot0(00, s0(y)) → 00
low(add0(m, x)) → if_low(add0(m, x))
low(nil0) → nil0
if_high(add0(m, x)) → add0(m, high(x))
app0(add0(n, x), y) → add0(n, app0(x, y))
app0(nil0, y) → y
minus(s0(x)) → minus(x)
le(00) → true0
quicksort0(add0(n, x)) → app0(quicksort0(low(x)), add0(n, quicksort0(high(x))))
minus(x) → x
quicksort0(nil0) → nil0
rand0(x) → x

(51) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
le(s0(x)) → le(x)
if_low(add0(m, x)) → add0(m, low(x))
le(s0(x)) → false0
high(nil0) → nil0
high(add0(m, x)) → if_high(add0(m, x))
rand0(x) → rand0(s0(x))
if_low(add0(m, x)) → low(x)
if_high(add0(m, x)) → high(x)
quot0(00, s0(y)) → 00
low(add0(m, x)) → if_low(add0(m, x))
low(nil0) → nil0
if_high(add0(m, x)) → add0(m, high(x))
app0(add0(n, x), y) → add0(n, app0(x, y))
app0(nil0, y) → y
minus(s0(x)) → minus(x)
le(00) → true0
quicksort0(add0(n, x)) → app0(quicksort0(low(x)), add0(n, quicksort0(high(x))))
minus(x) → x
quicksort0(nil0) → nil0
rand0(x) → x

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

(52) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(53) YES

(54) Obligation:

Relative ADP Problem with
absolute ADPs:

quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
le(s(x), s(y)) → le(x, y)
if_low(true, n, add(m, x)) → add(m, low(n, x))
quicksort(add(n, x)) → app(quicksort(low(n, x)), add(n, QUICKSORT(high(n, x))))
le(s(x), 0) → false
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_low(false, n, add(m, x)) → low(n, x)
if_high(true, n, add(m, x)) → high(n, x)
quot(0, s(y)) → 0
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
quicksort(add(n, x)) → app(QUICKSORT(low(n, x)), add(n, quicksort(high(n, x))))
low(n, nil) → nil
if_high(false, n, add(m, x)) → add(m, high(n, x))
app(add(n, x), y) → add(n, app(x, y))
app(nil, y) → y
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
quicksort(add(n, x)) → app(quicksort(low(n, x)), add(n, quicksort(high(n, x))))
minus(x, 0) → x
quicksort(nil) → nil

and relative ADPs:

rand(x) → rand(s(x))
rand(x) → x

(55) RelADPCleverAfsProof (SOUND transformation)

We use the first derelatifying processor [IJCAR24].
There are no annotations in relative ADPs, so the relative ADP problem can be transformed into a non-relative DP problem.

Furthermore, We use an argument filter [LPAR04].
Filtering:low_2 = 0 true = add_2 = app_2 = quicksort_1 = QUICKSORT_1 = if_high_3 = 0, 1 rand_1 = quot_2 = false = nil = s_1 = if_low_3 = 0, 1 le_2 = 0, 1 0 = minus_2 = 1 high_2 = 0
Found this filtering by looking at the following order that orders at least one DP strictly:Combined order from the following AFS and order.
QUICKSORT(x1) = QUICKSORT(x1)
add(x1, x2) = add(x1, x2)
high(x1, x2) = x2
low(x1, x2) = x2
quot(x1, x2) = quot(x1, x2)
s(x1) = s(x1)
minus(x1, x2) = minus(x1)
le(x1, x2) = le
if_low(x1, x2, x3) = x3
true = true
0 = 0
false = false
nil = nil
if_high(x1, x2, x3) = x3
app(x1, x2) = app(x1, x2)
quicksort(x1) = quicksort(x1)

Recursive path order with status [RPO].
Quasi-Precedence:

quot₂ > s₁ > false > [minus₁, nil]
le > [QUICKSORT₁, add₂, true, app₂] > [minus₁, nil]
le > false > [minus₁, nil]
0 > false > [minus₁, nil]
quicksort₁ > [QUICKSORT₁, add₂, true, app₂] > [minus₁, nil]

Status:

QUICKSORT₁: [1]
add₂: [1,2]
quot₂: [1,2]
s₁: multiset
minus₁: multiset
le: []
true: multiset
0: multiset
false: multiset
nil: multiset
app₂: [1,2]
quicksort₁: [1]

(56) Obligation:

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

QUICKSORT0(add0(n, x)) → QUICKSORT0(high(x))
QUICKSORT0(add0(n, x)) → QUICKSORT0(low(x))

The TRS R consists of the following rules:

quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
le → le
if_low(add0(m, x)) → add0(m, low(x))
le → false0
high(nil0) → nil0
high(add0(m, x)) → if_high(add0(m, x))
rand0(x) → rand0(s0(x))
if_low(add0(m, x)) → low(x)
if_high(add0(m, x)) → high(x)
quot0(00, s0(y)) → 00
low(add0(m, x)) → if_low(add0(m, x))
low(nil0) → nil0
if_high(add0(m, x)) → add0(m, high(x))
app0(add0(n, x), y) → add0(n, app0(x, y))
app0(nil0, y) → y
minus(s0(x)) → minus(x)
le → true0
quicksort0(add0(n, x)) → app0(quicksort0(low(x)), add0(n, quicksort0(high(x))))
minus(x) → x
quicksort0(nil0) → nil0
rand0(x) → x

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

(57) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

QUICKSORT0(add0(n, x)) → QUICKSORT0(high(x))
QUICKSORT0(add0(n, x)) → QUICKSORT0(low(x))

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
QUICKSORT0(x1) = QUICKSORT0(x1)
add0(x1, x2) = add0(x1, x2)
high(x1) = high(x1)
low(x1) = x1
quot0(x1, x2) = quot0
s0(x1) = x1
minus(x1) = minus(x1)
le = le
if_low(x1) = x1
false0 = false0
nil0 = nil0
if_high(x1) = if_high(x1)
rand0(x1) = x1
00 = 00
app0(x1, x2) = app0(x1, x2)
true0 = true0
quicksort0(x1) = quicksort0(x1)

Recursive path order with status [RPO].
Quasi-Precedence:

[quot0, minus₁, 00]
[le, false0] > true0
quicksort0₁ > app0₂ > [QUICKSORT0₁, add0₂, high₁, if_high₁] > nil0

Status:

QUICKSORT0₁: [1]
add0₂: multiset
high₁: multiset
quot0: multiset
minus₁: multiset
le: multiset
false0: multiset
nil0: multiset
if_high₁: multiset
00: multiset
app0₂: multiset
true0: multiset
quicksort0₁: [1]

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
le → le
if_low(add0(m, x)) → add0(m, low(x))
le → false0
high(nil0) → nil0
high(add0(m, x)) → if_high(add0(m, x))
rand0(x) → rand0(s0(x))
if_low(add0(m, x)) → low(x)
if_high(add0(m, x)) → high(x)
quot0(00, s0(y)) → 00
low(add0(m, x)) → if_low(add0(m, x))
low(nil0) → nil0
if_high(add0(m, x)) → add0(m, high(x))
app0(add0(n, x), y) → add0(n, app0(x, y))
app0(nil0, y) → y
minus(s0(x)) → minus(x)
le → true0
quicksort0(add0(n, x)) → app0(quicksort0(low(x)), add0(n, quicksort0(high(x))))
minus(x) → x
quicksort0(nil0) → nil0
rand0(x) → x

(58) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
le → le
if_low(add0(m, x)) → add0(m, low(x))
le → false0
high(nil0) → nil0
high(add0(m, x)) → if_high(add0(m, x))
rand0(x) → rand0(s0(x))
if_low(add0(m, x)) → low(x)
if_high(add0(m, x)) → high(x)
quot0(00, s0(y)) → 00
low(add0(m, x)) → if_low(add0(m, x))
low(nil0) → nil0
if_high(add0(m, x)) → add0(m, high(x))
app0(add0(n, x), y) → add0(n, app0(x, y))
app0(nil0, y) → y
minus(s0(x)) → minus(x)
le → true0
quicksort0(add0(n, x)) → app0(quicksort0(low(x)), add0(n, quicksort0(high(x))))
minus(x) → x
quicksort0(nil0) → nil0
rand0(x) → x

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

(59) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(60) YES

(61) Obligation:

Relative ADP Problem with
absolute ADPs:

quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
le(s(x), s(y)) → le(x, y)
if_low(true, n, add(m, x)) → add(m, low(n, x))
le(s(x), 0) → false
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_low(false, n, add(m, x)) → low(n, x)
if_high(true, n, add(m, x)) → high(n, x)
quot(0, s(y)) → 0
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
quot(s(x), s(y)) → s(QUOT(minus(x, y), s(y)))
low(n, nil) → nil
if_high(false, n, add(m, x)) → add(m, high(n, x))
app(add(n, x), y) → add(n, app(x, y))
app(nil, y) → y
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
quicksort(add(n, x)) → app(quicksort(low(n, x)), add(n, quicksort(high(n, x))))
minus(x, 0) → x
quicksort(nil) → nil

and relative ADPs:

rand(x) → rand(s(x))
rand(x) → x

(62) RelADPCleverAfsProof (SOUND transformation)

We use the first derelatifying processor [IJCAR24].
There are no annotations in relative ADPs, so the relative ADP problem can be transformed into a non-relative DP problem.

Furthermore, We use an argument filter [LPAR04].
Filtering:low_2 = 0, 1 true = QUOT_2 = 1 add_2 = 0, 1 app_2 = 0 quicksort_1 = if_high_3 = 0, 1 rand_1 = quot_2 = 1 false = nil = s_1 = if_low_3 = 0, 1 le_2 = 0, 1 0 = minus_2 = 1 high_2 = 0, 1
Found this filtering by looking at the following order that orders at least one DP strictly:Combined order from the following AFS and order.
QUOT(x1, x2) = QUOT(x1)
s(x1) = s(x1)
minus(x1, x2) = x1
quot(x1, x2) = quot(x1)
le(x1, x2) = le
if_low(x1, x2, x3) = x3
true = true
add(x1, x2) = add
low(x1, x2) = low
0 = 0
false = false
high(x1, x2) = high
nil = nil
if_high(x1, x2, x3) = x3
app(x1, x2) = app(x2)
quicksort(x1) = quicksort(x1)

Recursive path order with status [RPO].
Quasi-Precedence:

quot₁ > [QUOT₁, s₁] > 0 > [false, nil]
le > [true, add, low, high] > [false, nil]
[app₁, quicksort₁] > [true, add, low, high] > [false, nil]

Status:

QUOT₁: [1]
s₁: multiset
quot₁: [1]
le: []
true: multiset
add: multiset
low: multiset
0: multiset
false: multiset
high: multiset
nil: multiset
app₁: [1]
quicksort₁: [1]

(63) Obligation:

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

QUOT(s0(x)) → QUOT(minus(x))

The TRS R consists of the following rules:

quot(s0(x)) → s0(quot(minus(x)))
le → le
if_low(add) → add
le → false0
high → nil0
high → if_high(add)
rand0(x) → rand0(s0(x))
if_low(add) → low
if_high(add) → high
quot(00) → 00
low → if_low(add)
low → nil0
if_high(add) → add
app(y) → add
app(y) → y
minus(s0(x)) → minus(x)
le → true0
quicksort0(add) → app(add)
minus(x) → x
quicksort0(nil0) → nil0
rand0(x) → x

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

(64) MRRProof (EQUIVALENT transformation)

le → false0
rand0(x) → x

Used ordering: Polynomial interpretation [POLO]:

POL(00) = 0
POL(QUOT(x₁)) = x₁
POL(add) = 0
POL(app(x₁)) = 2·x₁
POL(false0) = 0
POL(high) = 0
POL(if_high(x₁)) = x₁
POL(if_low(x₁)) = x₁
POL(le) = 2
POL(low) = 0
POL(minus(x₁)) = x₁
POL(nil0) = 0
POL(quicksort0(x₁)) = x₁
POL(quot(x₁)) = x₁
POL(rand0(x₁)) = 2 + x₁
POL(s0(x₁)) = x₁
POL(true0) = 2

(65) Obligation:

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

QUOT(s0(x)) → QUOT(minus(x))

The TRS R consists of the following rules:

quot(s0(x)) → s0(quot(minus(x)))
le → le
if_low(add) → add
high → nil0
high → if_high(add)
rand0(x) → rand0(s0(x))
if_low(add) → low
if_high(add) → high
quot(00) → 00
low → if_low(add)
low → nil0
if_high(add) → add
app(y) → add
app(y) → y
minus(s0(x)) → minus(x)
le → true0
quicksort0(add) → app(add)
minus(x) → x
quicksort0(nil0) → nil0

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

(66) MRRProof (EQUIVALENT transformation)

le → true0

Used ordering: Polynomial interpretation [POLO]:

POL(00) = 0
POL(QUOT(x₁)) = x₁
POL(add) = 0
POL(app(x₁)) = 2·x₁
POL(high) = 0
POL(if_high(x₁)) = x₁
POL(if_low(x₁)) = x₁
POL(le) = 2
POL(low) = 0
POL(minus(x₁)) = x₁
POL(nil0) = 0
POL(quicksort0(x₁)) = x₁
POL(quot(x₁)) = x₁
POL(rand0(x₁)) = x₁
POL(s0(x₁)) = x₁
POL(true0) = 1

(67) Obligation:

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

QUOT(s0(x)) → QUOT(minus(x))

The TRS R consists of the following rules:

quot(s0(x)) → s0(quot(minus(x)))
le → le
if_low(add) → add
high → nil0
high → if_high(add)
rand0(x) → rand0(s0(x))
if_low(add) → low
if_high(add) → high
quot(00) → 00
low → if_low(add)
low → nil0
if_high(add) → add
app(y) → add
app(y) → y
minus(s0(x)) → minus(x)
quicksort0(add) → app(add)
minus(x) → x
quicksort0(nil0) → nil0

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

(68) MRRProof (EQUIVALENT transformation)

if_low(add) → add
high → nil0
quot(00) → 00
low → nil0
if_high(add) → add
app(y) → y
quicksort0(add) → app(add)
quicksort0(nil0) → nil0

Used ordering: Polynomial interpretation [POLO]:

POL(00) = 2
POL(QUOT(x₁)) = x₁
POL(add) = 1
POL(app(x₁)) = 1 + x₁
POL(high) = 2
POL(if_high(x₁)) = 2·x₁
POL(if_low(x₁)) = 2·x₁
POL(le) = 0
POL(low) = 2
POL(minus(x₁)) = x₁
POL(nil0) = 1
POL(quicksort0(x₁)) = 2 + 2·x₁
POL(quot(x₁)) = 2·x₁
POL(rand0(x₁)) = x₁
POL(s0(x₁)) = x₁

(69) Obligation:

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

QUOT(s0(x)) → QUOT(minus(x))

The TRS R consists of the following rules:

quot(s0(x)) → s0(quot(minus(x)))
le → le
high → if_high(add)
rand0(x) → rand0(s0(x))
if_low(add) → low
if_high(add) → high
low → if_low(add)
app(y) → add
minus(s0(x)) → minus(x)
minus(x) → x

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

(70) MRRProof (EQUIVALENT transformation)

app(y) → add

Used ordering: Polynomial interpretation [POLO]:

POL(QUOT(x₁)) = x₁
POL(add) = 0
POL(app(x₁)) = 2 + x₁
POL(high) = 0
POL(if_high(x₁)) = 2·x₁
POL(if_low(x₁)) = 2·x₁
POL(le) = 0
POL(low) = 0
POL(minus(x₁)) = x₁
POL(quot(x₁)) = 2·x₁
POL(rand0(x₁)) = x₁
POL(s0(x₁)) = x₁

(71) Obligation:

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

QUOT(s0(x)) → QUOT(minus(x))

The TRS R consists of the following rules:

quot(s0(x)) → s0(quot(minus(x)))
le → le
high → if_high(add)
rand0(x) → rand0(s0(x))
if_low(add) → low
if_high(add) → high
low → if_low(add)
minus(s0(x)) → minus(x)
minus(x) → x

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

(72) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

QUOT(s0(x)) → QUOT(minus(x))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( quot(x₁) ) = max{0, 2x₁ - 2}

POL( s0(x₁) ) = 2x₁ + 2

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

POL( le ) = 0

POL( high ) = 0

POL( if_high(x₁) ) = max{0, x₁ - 1}

POL( add ) = 1

POL( rand0(x₁) ) = max{0, -2}

POL( if_low(x₁) ) = 0

POL( low ) = 0

POL( QUOT(x₁) ) = 2x₁

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

quot(s0(x)) → s0(quot(minus(x)))
le → le
high → if_high(add)
rand0(x) → rand0(s0(x))
if_low(add) → low
if_high(add) → high
low → if_low(add)
minus(s0(x)) → minus(x)
minus(x) → x

(73) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

quot(s0(x)) → s0(quot(minus(x)))
le → le
high → if_high(add)
rand0(x) → rand0(s0(x))
if_low(add) → low
if_high(add) → high
low → if_low(add)
minus(s0(x)) → minus(x)
minus(x) → x

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

(74) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(0) Obligation:

(1) RelTRStoRelADPProof (EQUIVALENT transformation)

(2) Obligation:

(3) RelADPDepGraphProof (EQUIVALENT transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) RelADPCleverAfsProof (SOUND transformation)

(7) Obligation:

(8) QDPOrderProof (EQUIVALENT transformation)

(9) Obligation:

(10) PisEmptyProof (EQUIVALENT transformation)

(11) YES

(12) Obligation:

(13) RelADPCleverAfsProof (SOUND transformation)

(14) Obligation:

(15) MRRProof (EQUIVALENT transformation)

(16) Obligation:

(17) MRRProof (EQUIVALENT transformation)

(18) Obligation:

(19) MRRProof (EQUIVALENT transformation)

(20) Obligation:

(21) QDPOrderProof (EQUIVALENT transformation)

(22) Obligation:

(23) PisEmptyProof (EQUIVALENT transformation)

(24) YES

(25) Obligation:

(26) RelADPCleverAfsProof (SOUND transformation)

(27) Obligation:

(28) MRRProof (EQUIVALENT transformation)

(29) Obligation:

(30) MRRProof (EQUIVALENT transformation)

(31) Obligation:

(32) MRRProof (EQUIVALENT transformation)

(33) Obligation:

(34) MRRProof (EQUIVALENT transformation)

(35) Obligation:

(36) QDPOrderProof (EQUIVALENT transformation)

(37) Obligation:

(38) PisEmptyProof (EQUIVALENT transformation)

(39) YES

(40) Obligation:

(41) RelADPCleverAfsProof (SOUND transformation)

(42) Obligation:

(43) QDPOrderProof (EQUIVALENT transformation)

(44) Obligation:

(45) DependencyGraphProof (EQUIVALENT transformation)

(46) TRUE

(47) Obligation:

(48) RelADPCleverAfsProof (SOUND transformation)

(49) Obligation:

(50) QDPOrderProof (EQUIVALENT transformation)

(51) Obligation:

(52) PisEmptyProof (EQUIVALENT transformation)

(53) YES

(54) Obligation:

(55) RelADPCleverAfsProof (SOUND transformation)

(56) Obligation:

(57) QDPOrderProof (EQUIVALENT transformation)

(58) Obligation:

(59) PisEmptyProof (EQUIVALENT transformation)

(60) YES

(61) Obligation:

(62) RelADPCleverAfsProof (SOUND transformation)

(63) Obligation:

(64) MRRProof (EQUIVALENT transformation)

(65) Obligation:

(66) MRRProof (EQUIVALENT transformation)

(67) Obligation:

(68) MRRProof (EQUIVALENT transformation)

(69) Obligation:

(70) MRRProof (EQUIVALENT transformation)

(71) Obligation:

(72) QDPOrderProof (EQUIVALENT transformation)

(73) Obligation:

(74) PisEmptyProof (EQUIVALENT transformation)

(75) YES