YES

The TRS could be proven terminating. The proof took 496 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (14ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (331ms).
 | – Problem 3 was processed with processor SubtermCriterion (1ms).
 | – Problem 4 was processed with processor SubtermCriterion (1ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

lowers#(x, .(y, z))lowers#(x, z)greaters#(x, .(y, z))greaters#(x, z)
qsort#(.(x, y))qsort#(greaters(x, y))qsort#(.(x, y))qsort#(lowers(x, y))
qsort#(.(x, y))greaters#(x, y)qsort#(.(x, y))lowers#(x, y)

Rewrite Rules

qsort(nil)nilqsort(.(x, y))++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y))))
lowers(x, nil)nillowers(x, .(y, z))if(<=(y, x), .(y, lowers(x, z)), lowers(x, z))
greaters(x, nil)nilgreaters(x, .(y, z))if(<=(y, x), greaters(x, z), .(y, greaters(x, z)))

Original Signature

Termination of terms over the following signature is verified: if, <=, qsort, ++, ., nil, lowers, greaters

Strategy


The following SCCs where found

lowers#(x, .(y, z)) → lowers#(x, z)

qsort#(.(x, y)) → qsort#(greaters(x, y))qsort#(.(x, y)) → qsort#(lowers(x, y))

greaters#(x, .(y, z)) → greaters#(x, z)

Problem 2: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

qsort#(.(x, y))qsort#(greaters(x, y))qsort#(.(x, y))qsort#(lowers(x, y))

Rewrite Rules

qsort(nil)nilqsort(.(x, y))++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y))))
lowers(x, nil)nillowers(x, .(y, z))if(<=(y, x), .(y, lowers(x, z)), lowers(x, z))
greaters(x, nil)nilgreaters(x, .(y, z))if(<=(y, x), greaters(x, z), .(y, greaters(x, z)))

Original Signature

Termination of terms over the following signature is verified: if, <=, qsort, ++, ., nil, lowers, greaters

Strategy


Polynomial Interpretation

Improved Usable rules

greaters(x, .(y, z))if(<=(y, x), greaters(x, z), .(y, greaters(x, z)))greaters(x, nil)nil
lowers(x, nil)nillowers(x, .(y, z))if(<=(y, x), .(y, lowers(x, z)), lowers(x, z))

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

qsort#(.(x, y))qsort#(greaters(x, y))qsort#(.(x, y))qsort#(lowers(x, y))

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

greaters#(x, .(y, z))greaters#(x, z)

Rewrite Rules

qsort(nil)nilqsort(.(x, y))++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y))))
lowers(x, nil)nillowers(x, .(y, z))if(<=(y, x), .(y, lowers(x, z)), lowers(x, z))
greaters(x, nil)nilgreaters(x, .(y, z))if(<=(y, x), greaters(x, z), .(y, greaters(x, z)))

Original Signature

Termination of terms over the following signature is verified: if, <=, qsort, ++, ., nil, lowers, greaters

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

greaters#(x, .(y, z))greaters#(x, z)

Problem 4: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

lowers#(x, .(y, z))lowers#(x, z)

Rewrite Rules

qsort(nil)nilqsort(.(x, y))++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y))))
lowers(x, nil)nillowers(x, .(y, z))if(<=(y, x), .(y, lowers(x, z)), lowers(x, z))
greaters(x, nil)nilgreaters(x, .(y, z))if(<=(y, x), greaters(x, z), .(y, greaters(x, z)))

Original Signature

Termination of terms over the following signature is verified: if, <=, qsort, ++, ., nil, lowers, greaters

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

lowers#(x, .(y, z))lowers#(x, z)