MAYBE 18.35/7.31 MAYBE 18.35/7.34 18.35/7.34 18.35/7.34 18.35/7.34 18.35/7.34 18.35/7.34 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 18.35/7.34 18.35/7.34 18.35/7.34
18.35/7.34
18.35/7.34
18.35/7.34
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), INFINITE).

0 CpxTRS
18.35/7.34 
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
18.35/7.34 
↳2 CdtProblem
18.35/7.34 
↳3 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
18.35/7.34 
↳4 CdtProblem
18.35/7.34 
↳5 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
18.35/7.34 
↳6 CdtProblem
18.35/7.34 
↳7 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
18.35/7.34 
↳8 CdtProblem
18.35/7.34 
↳9 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
18.35/7.34 
↳10 CdtProblem
18.35/7.34 
↳11 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
18.35/7.34 
↳12 CdtProblem
18.35/7.34 
↳13 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
18.35/7.34 
↳14 CdtProblem
18.35/7.34 
↳15 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
18.35/7.34 
↳16 CdtProblem
18.35/7.34 
↳17 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
18.35/7.34 
↳18 CdtProblem
18.35/7.34 
↳19 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID))
18.35/7.34 
↳20 CdtProblem
18.35/7.34 
↳21 CdtLeafRemovalProof (ComplexityIfPolyImplication)
18.35/7.34 
↳22 CdtProblem
18.35/7.34 
↳23 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
18.35/7.34 
↳24 CdtProblem
18.35/7.34 
↳25 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
18.35/7.34 
↳26 CdtProblem
18.35/7.34 
↳27 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
18.35/7.34 
↳28 CdtProblem
18.35/7.34 
↳29 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
18.35/7.34 
↳30 CdtProblem
18.35/7.34
18.35/7.34 18.35/7.34
18.35/7.34
18.35/7.34

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

qsort(nil) → nil 18.35/7.34
qsort(.(x, y)) → ++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y)))) 18.35/7.34
lowers(x, nil) → nil 18.35/7.34
lowers(x, .(y, z)) → if(<=(y, x), .(y, lowers(x, z)), lowers(x, z)) 18.35/7.34
greaters(x, nil) → nil 18.35/7.34
greaters(x, .(y, z)) → if(<=(y, x), greaters(x, z), .(y, greaters(x, z)))

Rewrite Strategy: INNERMOST
18.35/7.34
18.35/7.34

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT
18.35/7.34
18.35/7.34

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

qsort(nil) → nil 18.35/7.34
qsort(.(z0, z1)) → ++(qsort(lowers(z0, z1)), .(z0, qsort(greaters(z0, z1)))) 18.35/7.34
lowers(z0, nil) → nil 18.35/7.34
lowers(z0, .(z1, z2)) → if(<=(z1, z0), .(z1, lowers(z0, z2)), lowers(z0, z2)) 18.35/7.34
greaters(z0, nil) → nil 18.35/7.34
greaters(z0, .(z1, z2)) → if(<=(z1, z0), greaters(z0, z2), .(z1, greaters(z0, z2)))
Tuples:

QSORT(.(z0, z1)) → c1(QSORT(lowers(z0, z1)), LOWERS(z0, z1), QSORT(greaters(z0, z1)), GREATERS(z0, z1)) 18.35/7.34
LOWERS(z0, .(z1, z2)) → c3(LOWERS(z0, z2), LOWERS(z0, z2)) 18.35/7.34
GREATERS(z0, .(z1, z2)) → c5(GREATERS(z0, z2), GREATERS(z0, z2))
S tuples:

QSORT(.(z0, z1)) → c1(QSORT(lowers(z0, z1)), LOWERS(z0, z1), QSORT(greaters(z0, z1)), GREATERS(z0, z1)) 18.35/7.34
LOWERS(z0, .(z1, z2)) → c3(LOWERS(z0, z2), LOWERS(z0, z2)) 18.35/7.34
GREATERS(z0, .(z1, z2)) → c5(GREATERS(z0, z2), GREATERS(z0, z2))
K tuples:none
Defined Rule Symbols:

qsort, lowers, greaters

Defined Pair Symbols:

QSORT, LOWERS, GREATERS

Compound Symbols:

c1, c3, c5

18.35/7.34
18.35/7.34

(3) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

QSORT(.(z0, z1)) → c1(QSORT(lowers(z0, z1)), LOWERS(z0, z1), QSORT(greaters(z0, z1)), GREATERS(z0, z1))
We considered the (Usable) Rules:

lowers(z0, nil) → nil 18.35/7.34
lowers(z0, .(z1, z2)) → if(<=(z1, z0), .(z1, lowers(z0, z2)), lowers(z0, z2)) 18.35/7.34
greaters(z0, nil) → nil 18.35/7.34
greaters(z0, .(z1, z2)) → if(<=(z1, z0), greaters(z0, z2), .(z1, greaters(z0, z2)))
And the Tuples:

QSORT(.(z0, z1)) → c1(QSORT(lowers(z0, z1)), LOWERS(z0, z1), QSORT(greaters(z0, z1)), GREATERS(z0, z1)) 18.35/7.34
LOWERS(z0, .(z1, z2)) → c3(LOWERS(z0, z2), LOWERS(z0, z2)) 18.35/7.34
GREATERS(z0, .(z1, z2)) → c5(GREATERS(z0, z2), GREATERS(z0, z2))
The order we found is given by the following interpretation:
Polynomial interpretation : 18.35/7.34

POL(.(x1, x2)) = [4]    18.35/7.34
POL(<=(x1, x2)) = [5] + x1 + x2    18.35/7.34
POL(GREATERS(x1, x2)) = 0    18.35/7.34
POL(LOWERS(x1, x2)) = 0    18.35/7.34
POL(QSORT(x1)) = [4]x1    18.35/7.34
POL(c1(x1, x2, x3, x4)) = x1 + x2 + x3 + x4    18.35/7.34
POL(c3(x1, x2)) = x1 + x2    18.35/7.34
POL(c5(x1, x2)) = x1 + x2    18.35/7.34
POL(greaters(x1, x2)) = [2]    18.35/7.34
POL(if(x1, x2, x3)) = 0    18.35/7.34
POL(lowers(x1, x2)) = 0    18.35/7.34
POL(nil) = 0   
18.35/7.34
18.35/7.34

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

qsort(nil) → nil 18.35/7.34
qsort(.(z0, z1)) → ++(qsort(lowers(z0, z1)), .(z0, qsort(greaters(z0, z1)))) 18.35/7.34
lowers(z0, nil) → nil 18.35/7.34
lowers(z0, .(z1, z2)) → if(<=(z1, z0), .(z1, lowers(z0, z2)), lowers(z0, z2)) 18.35/7.34
greaters(z0, nil) → nil 18.35/7.34
greaters(z0, .(z1, z2)) → if(<=(z1, z0), greaters(z0, z2), .(z1, greaters(z0, z2)))
Tuples:

QSORT(.(z0, z1)) → c1(QSORT(lowers(z0, z1)), LOWERS(z0, z1), QSORT(greaters(z0, z1)), GREATERS(z0, z1)) 18.35/7.34
LOWERS(z0, .(z1, z2)) → c3(LOWERS(z0, z2), LOWERS(z0, z2)) 18.35/7.34
GREATERS(z0, .(z1, z2)) → c5(GREATERS(z0, z2), GREATERS(z0, z2))
S tuples:

LOWERS(z0, .(z1, z2)) → c3(LOWERS(z0, z2), LOWERS(z0, z2)) 18.35/7.34
GREATERS(z0, .(z1, z2)) → c5(GREATERS(z0, z2), GREATERS(z0, z2))
K tuples:

QSORT(.(z0, z1)) → c1(QSORT(lowers(z0, z1)), LOWERS(z0, z1), QSORT(greaters(z0, z1)), GREATERS(z0, z1))
Defined Rule Symbols:

qsort, lowers, greaters

Defined Pair Symbols:

QSORT, LOWERS, GREATERS

Compound Symbols:

c1, c3, c5

18.35/7.34
18.35/7.34

(5) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace QSORT(.(z0, z1)) → c1(QSORT(lowers(z0, z1)), LOWERS(z0, z1), QSORT(greaters(z0, z1)), GREATERS(z0, z1)) by

QSORT(.(z0, nil)) → c1(QSORT(nil), LOWERS(z0, nil), QSORT(greaters(z0, nil)), GREATERS(z0, nil)) 18.35/7.34
QSORT(.(z0, .(z1, z2))) → c1(QSORT(if(<=(z1, z0), .(z1, lowers(z0, z2)), lowers(z0, z2))), LOWERS(z0, .(z1, z2)), QSORT(greaters(z0, .(z1, z2))), GREATERS(z0, .(z1, z2)))
18.35/7.34
18.35/7.34

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

qsort(nil) → nil 18.35/7.34
qsort(.(z0, z1)) → ++(qsort(lowers(z0, z1)), .(z0, qsort(greaters(z0, z1)))) 18.35/7.34
lowers(z0, nil) → nil 18.35/7.34
lowers(z0, .(z1, z2)) → if(<=(z1, z0), .(z1, lowers(z0, z2)), lowers(z0, z2)) 18.35/7.34
greaters(z0, nil) → nil 18.35/7.34
greaters(z0, .(z1, z2)) → if(<=(z1, z0), greaters(z0, z2), .(z1, greaters(z0, z2)))
Tuples:

LOWERS(z0, .(z1, z2)) → c3(LOWERS(z0, z2), LOWERS(z0, z2)) 18.35/7.34
GREATERS(z0, .(z1, z2)) → c5(GREATERS(z0, z2), GREATERS(z0, z2)) 18.35/7.34
QSORT(.(z0, nil)) → c1(QSORT(nil), LOWERS(z0, nil), QSORT(greaters(z0, nil)), GREATERS(z0, nil)) 18.35/7.34
QSORT(.(z0, .(z1, z2))) → c1(QSORT(if(<=(z1, z0), .(z1, lowers(z0, z2)), lowers(z0, z2))), LOWERS(z0, .(z1, z2)), QSORT(greaters(z0, .(z1, z2))), GREATERS(z0, .(z1, z2)))
S tuples:

LOWERS(z0, .(z1, z2)) → c3(LOWERS(z0, z2), LOWERS(z0, z2)) 18.35/7.34
GREATERS(z0, .(z1, z2)) → c5(GREATERS(z0, z2), GREATERS(z0, z2))
K tuples:

QSORT(.(z0, z1)) → c1(QSORT(lowers(z0, z1)), LOWERS(z0, z1), QSORT(greaters(z0, z1)), GREATERS(z0, z1))
Defined Rule Symbols:

qsort, lowers, greaters

Defined Pair Symbols:

LOWERS, GREATERS, QSORT

Compound Symbols:

c3, c5, c1

18.35/7.34
18.35/7.34

(7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 4 trailing tuple parts
18.35/7.34
18.35/7.34

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

qsort(nil) → nil 18.35/7.34
qsort(.(z0, z1)) → ++(qsort(lowers(z0, z1)), .(z0, qsort(greaters(z0, z1)))) 18.35/7.34
lowers(z0, nil) → nil 18.35/7.34
lowers(z0, .(z1, z2)) → if(<=(z1, z0), .(z1, lowers(z0, z2)), lowers(z0, z2)) 18.35/7.34
greaters(z0, nil) → nil 18.35/7.34
greaters(z0, .(z1, z2)) → if(<=(z1, z0), greaters(z0, z2), .(z1, greaters(z0, z2)))
Tuples:

LOWERS(z0, .(z1, z2)) → c3(LOWERS(z0, z2), LOWERS(z0, z2)) 18.35/7.34
GREATERS(z0, .(z1, z2)) → c5(GREATERS(z0, z2), GREATERS(z0, z2)) 18.35/7.34
QSORT(.(z0, nil)) → c1(QSORT(greaters(z0, nil))) 18.35/7.34
QSORT(.(z0, .(z1, z2))) → c1(LOWERS(z0, .(z1, z2)), QSORT(greaters(z0, .(z1, z2))), GREATERS(z0, .(z1, z2)))
S tuples:

LOWERS(z0, .(z1, z2)) → c3(LOWERS(z0, z2), LOWERS(z0, z2)) 18.35/7.34
GREATERS(z0, .(z1, z2)) → c5(GREATERS(z0, z2), GREATERS(z0, z2))
K tuples:

QSORT(.(z0, z1)) → c1(QSORT(lowers(z0, z1)), LOWERS(z0, z1), QSORT(greaters(z0, z1)), GREATERS(z0, z1))
Defined Rule Symbols:

qsort, lowers, greaters

Defined Pair Symbols:

LOWERS, GREATERS, QSORT

Compound Symbols:

c3, c5, c1, c1

18.35/7.34
18.35/7.34

(9) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace QSORT(.(z0, nil)) → c1(QSORT(greaters(z0, nil))) by

QSORT(.(z0, nil)) → c1(QSORT(nil))
18.35/7.34
18.35/7.34

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

qsort(nil) → nil 18.35/7.34
qsort(.(z0, z1)) → ++(qsort(lowers(z0, z1)), .(z0, qsort(greaters(z0, z1)))) 18.35/7.34
lowers(z0, nil) → nil 18.35/7.34
lowers(z0, .(z1, z2)) → if(<=(z1, z0), .(z1, lowers(z0, z2)), lowers(z0, z2)) 18.35/7.34
greaters(z0, nil) → nil 18.35/7.34
greaters(z0, .(z1, z2)) → if(<=(z1, z0), greaters(z0, z2), .(z1, greaters(z0, z2)))
Tuples:

LOWERS(z0, .(z1, z2)) → c3(LOWERS(z0, z2), LOWERS(z0, z2)) 18.35/7.34
GREATERS(z0, .(z1, z2)) → c5(GREATERS(z0, z2), GREATERS(z0, z2)) 18.35/7.34
QSORT(.(z0, .(z1, z2))) → c1(LOWERS(z0, .(z1, z2)), QSORT(greaters(z0, .(z1, z2))), GREATERS(z0, .(z1, z2))) 18.35/7.34
QSORT(.(z0, nil)) → c1(QSORT(nil))
S tuples:

LOWERS(z0, .(z1, z2)) → c3(LOWERS(z0, z2), LOWERS(z0, z2)) 18.35/7.34
GREATERS(z0, .(z1, z2)) → c5(GREATERS(z0, z2), GREATERS(z0, z2))
K tuples:

QSORT(.(z0, z1)) → c1(QSORT(lowers(z0, z1)), LOWERS(z0, z1), QSORT(greaters(z0, z1)), GREATERS(z0, z1))
Defined Rule Symbols:

qsort, lowers, greaters

Defined Pair Symbols:

LOWERS, GREATERS, QSORT

Compound Symbols:

c3, c5, c1, c1

18.35/7.34
18.35/7.34

(11) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts
18.35/7.34
18.35/7.34

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

qsort(nil) → nil 18.35/7.34
qsort(.(z0, z1)) → ++(qsort(lowers(z0, z1)), .(z0, qsort(greaters(z0, z1)))) 18.35/7.34
lowers(z0, nil) → nil 18.35/7.34
lowers(z0, .(z1, z2)) → if(<=(z1, z0), .(z1, lowers(z0, z2)), lowers(z0, z2)) 18.35/7.34
greaters(z0, nil) → nil 18.35/7.34
greaters(z0, .(z1, z2)) → if(<=(z1, z0), greaters(z0, z2), .(z1, greaters(z0, z2)))
Tuples:

LOWERS(z0, .(z1, z2)) → c3(LOWERS(z0, z2), LOWERS(z0, z2)) 18.35/7.34
GREATERS(z0, .(z1, z2)) → c5(GREATERS(z0, z2), GREATERS(z0, z2)) 18.35/7.34
QSORT(.(z0, .(z1, z2))) → c1(LOWERS(z0, .(z1, z2)), QSORT(greaters(z0, .(z1, z2))), GREATERS(z0, .(z1, z2))) 18.35/7.34
QSORT(.(z0, nil)) → c1
S tuples:

LOWERS(z0, .(z1, z2)) → c3(LOWERS(z0, z2), LOWERS(z0, z2)) 18.35/7.34
GREATERS(z0, .(z1, z2)) → c5(GREATERS(z0, z2), GREATERS(z0, z2))
K tuples:

QSORT(.(z0, z1)) → c1(QSORT(lowers(z0, z1)), LOWERS(z0, z1), QSORT(greaters(z0, z1)), GREATERS(z0, z1))
Defined Rule Symbols:

qsort, lowers, greaters

Defined Pair Symbols:

LOWERS, GREATERS, QSORT

Compound Symbols:

c3, c5, c1, c1

18.35/7.34
18.35/7.34

(13) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

QSORT(.(z0, nil)) → c1
18.35/7.34
18.35/7.34

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

qsort(nil) → nil 18.35/7.34
qsort(.(z0, z1)) → ++(qsort(lowers(z0, z1)), .(z0, qsort(greaters(z0, z1)))) 18.35/7.34
lowers(z0, nil) → nil 18.35/7.34
lowers(z0, .(z1, z2)) → if(<=(z1, z0), .(z1, lowers(z0, z2)), lowers(z0, z2)) 18.35/7.34
greaters(z0, nil) → nil 18.35/7.34
greaters(z0, .(z1, z2)) → if(<=(z1, z0), greaters(z0, z2), .(z1, greaters(z0, z2)))
Tuples:

LOWERS(z0, .(z1, z2)) → c3(LOWERS(z0, z2), LOWERS(z0, z2)) 18.35/7.34
GREATERS(z0, .(z1, z2)) → c5(GREATERS(z0, z2), GREATERS(z0, z2)) 18.35/7.34
QSORT(.(z0, .(z1, z2))) → c1(LOWERS(z0, .(z1, z2)), QSORT(greaters(z0, .(z1, z2))), GREATERS(z0, .(z1, z2))) 18.35/7.34
QSORT(.(z0, nil)) → c1
S tuples:

LOWERS(z0, .(z1, z2)) → c3(LOWERS(z0, z2), LOWERS(z0, z2)) 18.35/7.34
GREATERS(z0, .(z1, z2)) → c5(GREATERS(z0, z2), GREATERS(z0, z2))
K tuples:none
Defined Rule Symbols:

qsort, lowers, greaters

Defined Pair Symbols:

LOWERS, GREATERS, QSORT

Compound Symbols:

c3, c5, c1, c1

18.35/7.34
18.35/7.34

(15) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace QSORT(.(z0, .(z1, z2))) → c1(LOWERS(z0, .(z1, z2)), QSORT(greaters(z0, .(z1, z2))), GREATERS(z0, .(z1, z2))) by

QSORT(.(z0, .(z1, z2))) → c1(LOWERS(z0, .(z1, z2)), QSORT(if(<=(z1, z0), greaters(z0, z2), .(z1, greaters(z0, z2)))), GREATERS(z0, .(z1, z2)))
18.35/7.34
18.35/7.34

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

qsort(nil) → nil 18.35/7.34
qsort(.(z0, z1)) → ++(qsort(lowers(z0, z1)), .(z0, qsort(greaters(z0, z1)))) 18.35/7.34
lowers(z0, nil) → nil 18.35/7.34
lowers(z0, .(z1, z2)) → if(<=(z1, z0), .(z1, lowers(z0, z2)), lowers(z0, z2)) 18.35/7.34
greaters(z0, nil) → nil 18.35/7.34
greaters(z0, .(z1, z2)) → if(<=(z1, z0), greaters(z0, z2), .(z1, greaters(z0, z2)))
Tuples:

LOWERS(z0, .(z1, z2)) → c3(LOWERS(z0, z2), LOWERS(z0, z2)) 18.35/7.34
GREATERS(z0, .(z1, z2)) → c5(GREATERS(z0, z2), GREATERS(z0, z2)) 18.35/7.34
QSORT(.(z0, nil)) → c1 18.35/7.34
QSORT(.(z0, .(z1, z2))) → c1(LOWERS(z0, .(z1, z2)), QSORT(if(<=(z1, z0), greaters(z0, z2), .(z1, greaters(z0, z2)))), GREATERS(z0, .(z1, z2)))
S tuples:

LOWERS(z0, .(z1, z2)) → c3(LOWERS(z0, z2), LOWERS(z0, z2)) 18.35/7.34
GREATERS(z0, .(z1, z2)) → c5(GREATERS(z0, z2), GREATERS(z0, z2))
K tuples:none
Defined Rule Symbols:

qsort, lowers, greaters

Defined Pair Symbols:

LOWERS, GREATERS, QSORT

Compound Symbols:

c3, c5, c1, c1

18.35/7.34
18.35/7.34

(17) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts
18.35/7.34
18.35/7.34

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

qsort(nil) → nil 18.35/7.34
qsort(.(z0, z1)) → ++(qsort(lowers(z0, z1)), .(z0, qsort(greaters(z0, z1)))) 18.35/7.34
lowers(z0, nil) → nil 18.35/7.34
lowers(z0, .(z1, z2)) → if(<=(z1, z0), .(z1, lowers(z0, z2)), lowers(z0, z2)) 18.35/7.34
greaters(z0, nil) → nil 18.35/7.34
greaters(z0, .(z1, z2)) → if(<=(z1, z0), greaters(z0, z2), .(z1, greaters(z0, z2)))
Tuples:

LOWERS(z0, .(z1, z2)) → c3(LOWERS(z0, z2), LOWERS(z0, z2)) 18.35/7.34
GREATERS(z0, .(z1, z2)) → c5(GREATERS(z0, z2), GREATERS(z0, z2)) 18.35/7.34
QSORT(.(z0, nil)) → c1 18.35/7.34
QSORT(.(z0, .(z1, z2))) → c1(LOWERS(z0, .(z1, z2)), GREATERS(z0, .(z1, z2)))
S tuples:

LOWERS(z0, .(z1, z2)) → c3(LOWERS(z0, z2), LOWERS(z0, z2)) 18.35/7.34
GREATERS(z0, .(z1, z2)) → c5(GREATERS(z0, z2), GREATERS(z0, z2))
K tuples:none
Defined Rule Symbols:

qsort, lowers, greaters

Defined Pair Symbols:

LOWERS, GREATERS, QSORT

Compound Symbols:

c3, c5, c1, c1

18.35/7.34
18.35/7.34

(19) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC
18.35/7.34
18.35/7.34

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

qsort(nil) → nil 18.35/7.34
qsort(.(z0, z1)) → ++(qsort(lowers(z0, z1)), .(z0, qsort(greaters(z0, z1)))) 18.35/7.34
lowers(z0, nil) → nil 18.35/7.34
lowers(z0, .(z1, z2)) → if(<=(z1, z0), .(z1, lowers(z0, z2)), lowers(z0, z2)) 18.35/7.34
greaters(z0, nil) → nil 18.35/7.34
greaters(z0, .(z1, z2)) → if(<=(z1, z0), greaters(z0, z2), .(z1, greaters(z0, z2)))
Tuples:

LOWERS(z0, .(z1, z2)) → c3(LOWERS(z0, z2), LOWERS(z0, z2)) 18.35/7.34
GREATERS(z0, .(z1, z2)) → c5(GREATERS(z0, z2), GREATERS(z0, z2)) 18.35/7.34
QSORT(.(z0, nil)) → c1 18.35/7.34
QSORT(.(z0, .(z1, z2))) → c(LOWERS(z0, .(z1, z2))) 18.35/7.34
QSORT(.(z0, .(z1, z2))) → c(GREATERS(z0, .(z1, z2)))
S tuples:

LOWERS(z0, .(z1, z2)) → c3(LOWERS(z0, z2), LOWERS(z0, z2)) 18.35/7.34
GREATERS(z0, .(z1, z2)) → c5(GREATERS(z0, z2), GREATERS(z0, z2))
K tuples:none
Defined Rule Symbols:

qsort, lowers, greaters

Defined Pair Symbols:

LOWERS, GREATERS, QSORT

Compound Symbols:

c3, c5, c1, c

18.35/7.34
18.35/7.34

(21) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 2 leading nodes:

QSORT(.(z0, .(z1, z2))) → c(LOWERS(z0, .(z1, z2))) 18.35/7.34
QSORT(.(z0, .(z1, z2))) → c(GREATERS(z0, .(z1, z2)))
Removed 1 trailing nodes:

QSORT(.(z0, nil)) → c1
18.35/7.34
18.35/7.34

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

qsort(nil) → nil 18.35/7.34
qsort(.(z0, z1)) → ++(qsort(lowers(z0, z1)), .(z0, qsort(greaters(z0, z1)))) 18.35/7.34
lowers(z0, nil) → nil 18.35/7.34
lowers(z0, .(z1, z2)) → if(<=(z1, z0), .(z1, lowers(z0, z2)), lowers(z0, z2)) 18.35/7.34
greaters(z0, nil) → nil 18.35/7.34
greaters(z0, .(z1, z2)) → if(<=(z1, z0), greaters(z0, z2), .(z1, greaters(z0, z2)))
Tuples:

LOWERS(z0, .(z1, z2)) → c3(LOWERS(z0, z2), LOWERS(z0, z2)) 18.35/7.34
GREATERS(z0, .(z1, z2)) → c5(GREATERS(z0, z2), GREATERS(z0, z2))
S tuples:

LOWERS(z0, .(z1, z2)) → c3(LOWERS(z0, z2), LOWERS(z0, z2)) 18.35/7.34
GREATERS(z0, .(z1, z2)) → c5(GREATERS(z0, z2), GREATERS(z0, z2))
K tuples:none
Defined Rule Symbols:

qsort, lowers, greaters

Defined Pair Symbols:

LOWERS, GREATERS

Compound Symbols:

c3, c5

18.35/7.34
18.35/7.34

(23) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace LOWERS(z0, .(z1, z2)) → c3(LOWERS(z0, z2), LOWERS(z0, z2)) by

LOWERS(z0, .(z1, .(y1, y2))) → c3(LOWERS(z0, .(y1, y2)), LOWERS(z0, .(y1, y2)))
18.35/7.34
18.35/7.34

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

qsort(nil) → nil 18.35/7.34
qsort(.(z0, z1)) → ++(qsort(lowers(z0, z1)), .(z0, qsort(greaters(z0, z1)))) 18.35/7.34
lowers(z0, nil) → nil 18.35/7.34
lowers(z0, .(z1, z2)) → if(<=(z1, z0), .(z1, lowers(z0, z2)), lowers(z0, z2)) 18.35/7.34
greaters(z0, nil) → nil 18.35/7.34
greaters(z0, .(z1, z2)) → if(<=(z1, z0), greaters(z0, z2), .(z1, greaters(z0, z2)))
Tuples:

GREATERS(z0, .(z1, z2)) → c5(GREATERS(z0, z2), GREATERS(z0, z2)) 18.35/7.34
LOWERS(z0, .(z1, .(y1, y2))) → c3(LOWERS(z0, .(y1, y2)), LOWERS(z0, .(y1, y2)))
S tuples:

GREATERS(z0, .(z1, z2)) → c5(GREATERS(z0, z2), GREATERS(z0, z2)) 18.35/7.34
LOWERS(z0, .(z1, .(y1, y2))) → c3(LOWERS(z0, .(y1, y2)), LOWERS(z0, .(y1, y2)))
K tuples:none
Defined Rule Symbols:

qsort, lowers, greaters

Defined Pair Symbols:

GREATERS, LOWERS

Compound Symbols:

c5, c3

18.35/7.34
18.35/7.34

(25) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace GREATERS(z0, .(z1, z2)) → c5(GREATERS(z0, z2), GREATERS(z0, z2)) by

GREATERS(z0, .(z1, .(y1, y2))) → c5(GREATERS(z0, .(y1, y2)), GREATERS(z0, .(y1, y2)))
18.35/7.34
18.35/7.34

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

qsort(nil) → nil 18.35/7.34
qsort(.(z0, z1)) → ++(qsort(lowers(z0, z1)), .(z0, qsort(greaters(z0, z1)))) 18.35/7.34
lowers(z0, nil) → nil 18.35/7.34
lowers(z0, .(z1, z2)) → if(<=(z1, z0), .(z1, lowers(z0, z2)), lowers(z0, z2)) 18.35/7.34
greaters(z0, nil) → nil 18.35/7.34
greaters(z0, .(z1, z2)) → if(<=(z1, z0), greaters(z0, z2), .(z1, greaters(z0, z2)))
Tuples:

LOWERS(z0, .(z1, .(y1, y2))) → c3(LOWERS(z0, .(y1, y2)), LOWERS(z0, .(y1, y2))) 18.35/7.34
GREATERS(z0, .(z1, .(y1, y2))) → c5(GREATERS(z0, .(y1, y2)), GREATERS(z0, .(y1, y2)))
S tuples:

LOWERS(z0, .(z1, .(y1, y2))) → c3(LOWERS(z0, .(y1, y2)), LOWERS(z0, .(y1, y2))) 18.35/7.34
GREATERS(z0, .(z1, .(y1, y2))) → c5(GREATERS(z0, .(y1, y2)), GREATERS(z0, .(y1, y2)))
K tuples:none
Defined Rule Symbols:

qsort, lowers, greaters

Defined Pair Symbols:

LOWERS, GREATERS

Compound Symbols:

c3, c5

18.35/7.34
18.35/7.34

(27) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace LOWERS(z0, .(z1, .(y1, y2))) → c3(LOWERS(z0, .(y1, y2)), LOWERS(z0, .(y1, y2))) by

LOWERS(z0, .(z1, .(z2, .(y2, y3)))) → c3(LOWERS(z0, .(z2, .(y2, y3))), LOWERS(z0, .(z2, .(y2, y3))))
18.35/7.34
18.35/7.34

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

qsort(nil) → nil 18.35/7.34
qsort(.(z0, z1)) → ++(qsort(lowers(z0, z1)), .(z0, qsort(greaters(z0, z1)))) 18.35/7.34
lowers(z0, nil) → nil 18.35/7.34
lowers(z0, .(z1, z2)) → if(<=(z1, z0), .(z1, lowers(z0, z2)), lowers(z0, z2)) 18.35/7.34
greaters(z0, nil) → nil 18.35/7.34
greaters(z0, .(z1, z2)) → if(<=(z1, z0), greaters(z0, z2), .(z1, greaters(z0, z2)))
Tuples:

GREATERS(z0, .(z1, .(y1, y2))) → c5(GREATERS(z0, .(y1, y2)), GREATERS(z0, .(y1, y2))) 18.35/7.34
LOWERS(z0, .(z1, .(z2, .(y2, y3)))) → c3(LOWERS(z0, .(z2, .(y2, y3))), LOWERS(z0, .(z2, .(y2, y3))))
S tuples:

GREATERS(z0, .(z1, .(y1, y2))) → c5(GREATERS(z0, .(y1, y2)), GREATERS(z0, .(y1, y2))) 18.35/7.34
LOWERS(z0, .(z1, .(z2, .(y2, y3)))) → c3(LOWERS(z0, .(z2, .(y2, y3))), LOWERS(z0, .(z2, .(y2, y3))))
K tuples:none
Defined Rule Symbols:

qsort, lowers, greaters

Defined Pair Symbols:

GREATERS, LOWERS

Compound Symbols:

c5, c3

18.35/7.34
18.35/7.34

(29) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace GREATERS(z0, .(z1, .(y1, y2))) → c5(GREATERS(z0, .(y1, y2)), GREATERS(z0, .(y1, y2))) by

GREATERS(z0, .(z1, .(z2, .(y2, y3)))) → c5(GREATERS(z0, .(z2, .(y2, y3))), GREATERS(z0, .(z2, .(y2, y3))))
18.35/7.34
18.35/7.34

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

qsort(nil) → nil 18.35/7.34
qsort(.(z0, z1)) → ++(qsort(lowers(z0, z1)), .(z0, qsort(greaters(z0, z1)))) 18.35/7.34
lowers(z0, nil) → nil 18.35/7.34
lowers(z0, .(z1, z2)) → if(<=(z1, z0), .(z1, lowers(z0, z2)), lowers(z0, z2)) 18.35/7.34
greaters(z0, nil) → nil 18.35/7.34
greaters(z0, .(z1, z2)) → if(<=(z1, z0), greaters(z0, z2), .(z1, greaters(z0, z2)))
Tuples:

LOWERS(z0, .(z1, .(z2, .(y2, y3)))) → c3(LOWERS(z0, .(z2, .(y2, y3))), LOWERS(z0, .(z2, .(y2, y3)))) 18.35/7.34
GREATERS(z0, .(z1, .(z2, .(y2, y3)))) → c5(GREATERS(z0, .(z2, .(y2, y3))), GREATERS(z0, .(z2, .(y2, y3))))
S tuples:

LOWERS(z0, .(z1, .(z2, .(y2, y3)))) → c3(LOWERS(z0, .(z2, .(y2, y3))), LOWERS(z0, .(z2, .(y2, y3)))) 18.35/7.34
GREATERS(z0, .(z1, .(z2, .(y2, y3)))) → c5(GREATERS(z0, .(z2, .(y2, y3))), GREATERS(z0, .(z2, .(y2, y3))))
K tuples:none
Defined Rule Symbols:

qsort, lowers, greaters

Defined Pair Symbols:

LOWERS, GREATERS

Compound Symbols:

c3, c5

18.35/7.34
18.35/7.34
18.35/7.39 EOF