YES(O(1), O(n^2)) 11.05/3.21 YES(O(1), O(n^2)) 11.05/3.26 11.05/3.26 11.05/3.26 11.05/3.26 11.05/3.26 11.05/3.26 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 11.05/3.26 11.05/3.26 11.05/3.26
11.05/3.26
11.05/3.26
11.05/3.26
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(O(1), O(n^2)).

0 CpxRelTRS
11.05/3.26 
↳1 CpxRelTrsToCDT (UPPER BOUND (ID))
11.05/3.26 
↳2 CdtProblem
11.05/3.26 
↳3 CdtLeafRemovalProof (ComplexityIfPolyImplication)
11.05/3.26 
↳4 CdtProblem
11.05/3.26 
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
11.05/3.26 
↳6 CdtProblem
11.05/3.26 
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
11.05/3.26 
↳8 CdtProblem
11.05/3.26 
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
11.05/3.26 
↳10 CdtProblem
11.05/3.26 
↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
11.05/3.26 
↳12 CdtProblem
11.05/3.26 
↳13 SIsEmptyProof (BOTH BOUNDS(ID, ID))
11.05/3.26 
↳14 BOUNDS(O(1), O(1))
11.05/3.26
11.05/3.26 11.05/3.26
11.05/3.26
11.05/3.26

(0) Obligation:

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

mergesort(Cons(x', Cons(x, xs))) → splitmerge(Cons(x', Cons(x, xs)), Nil, Nil) 11.05/3.26
mergesort(Cons(x, Nil)) → Cons(x, Nil) 11.05/3.26
merge(Cons(x', xs'), Cons(x, xs)) → merge[Ite][True][Ite][True][Ite](<=(x', x), Cons(x', xs'), Cons(x, xs)) 11.05/3.26
merge(Cons(x, xs), Nil) → Cons(x, xs) 11.05/3.26
splitmerge(Cons(x, xs), xs1, xs2) → splitmerge(xs, Cons(x, xs2), xs1) 11.05/3.26
splitmerge(Nil, xs1, xs2) → merge(mergesort(xs1), mergesort(xs2)) 11.05/3.26
mergesort(Nil) → Nil 11.05/3.26
merge(Nil, xs2) → xs2 11.05/3.26
notEmpty(Cons(x, xs)) → True 11.05/3.26
notEmpty(Nil) → False 11.05/3.26
goal(xs) → mergesort(xs)

The (relative) TRS S consists of the following rules:

<=(S(x), S(y)) → <=(x, y) 11.05/3.26
<=(0, y) → True 11.05/3.26
<=(S(x), 0) → False

Rewrite Strategy: INNERMOST
11.05/3.26
11.05/3.26

(1) CpxRelTrsToCDT (UPPER BOUND (ID) transformation)

Relative innermost TRS to CDT Problem.
11.05/3.26
11.05/3.26

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

<=(S(z0), S(z1)) → <=(z0, z1) 11.05/3.26
<=(0, z0) → True 11.05/3.26
<=(S(z0), 0) → False 11.05/3.26
mergesort(Cons(z0, Cons(z1, z2))) → splitmerge(Cons(z0, Cons(z1, z2)), Nil, Nil) 11.05/3.26
mergesort(Cons(z0, Nil)) → Cons(z0, Nil) 11.05/3.26
mergesort(Nil) → Nil 11.05/3.26
merge(Cons(z0, z1), Cons(z2, z3)) → merge[Ite][True][Ite][True][Ite](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)) 11.05/3.26
merge(Cons(z0, z1), Nil) → Cons(z0, z1) 11.05/3.26
merge(Nil, z0) → z0 11.05/3.26
splitmerge(Cons(z0, z1), z2, z3) → splitmerge(z1, Cons(z0, z3), z2) 11.05/3.26
splitmerge(Nil, z0, z1) → merge(mergesort(z0), mergesort(z1)) 11.05/3.26
notEmpty(Cons(z0, z1)) → True 11.05/3.26
notEmpty(Nil) → False 11.05/3.26
goal(z0) → mergesort(z0)
Tuples:

<='(S(z0), S(z1)) → c(<='(z0, z1)) 11.05/3.26
MERGESORT(Cons(z0, Cons(z1, z2))) → c3(SPLITMERGE(Cons(z0, Cons(z1, z2)), Nil, Nil)) 11.05/3.26
MERGE(Cons(z0, z1), Cons(z2, z3)) → c6(<='(z0, z2)) 11.05/3.26
SPLITMERGE(Cons(z0, z1), z2, z3) → c9(SPLITMERGE(z1, Cons(z0, z3), z2)) 11.05/3.26
SPLITMERGE(Nil, z0, z1) → c10(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0), MERGESORT(z1)) 11.05/3.26
GOAL(z0) → c13(MERGESORT(z0))
S tuples:

MERGESORT(Cons(z0, Cons(z1, z2))) → c3(SPLITMERGE(Cons(z0, Cons(z1, z2)), Nil, Nil)) 11.05/3.26
MERGE(Cons(z0, z1), Cons(z2, z3)) → c6(<='(z0, z2)) 11.05/3.26
SPLITMERGE(Cons(z0, z1), z2, z3) → c9(SPLITMERGE(z1, Cons(z0, z3), z2)) 11.05/3.26
SPLITMERGE(Nil, z0, z1) → c10(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0), MERGESORT(z1)) 11.05/3.26
GOAL(z0) → c13(MERGESORT(z0))
K tuples:none
Defined Rule Symbols:

mergesort, merge, splitmerge, notEmpty, goal, <=

Defined Pair Symbols:

<=', MERGESORT, MERGE, SPLITMERGE, GOAL

Compound Symbols:

c, c3, c6, c9, c10, c13

11.05/3.26
11.05/3.26

(3) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

GOAL(z0) → c13(MERGESORT(z0))
11.05/3.26
11.05/3.26

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

<=(S(z0), S(z1)) → <=(z0, z1) 11.05/3.26
<=(0, z0) → True 11.05/3.26
<=(S(z0), 0) → False 11.05/3.26
mergesort(Cons(z0, Cons(z1, z2))) → splitmerge(Cons(z0, Cons(z1, z2)), Nil, Nil) 11.05/3.26
mergesort(Cons(z0, Nil)) → Cons(z0, Nil) 11.05/3.26
mergesort(Nil) → Nil 11.05/3.26
merge(Cons(z0, z1), Cons(z2, z3)) → merge[Ite][True][Ite][True][Ite](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)) 11.05/3.26
merge(Cons(z0, z1), Nil) → Cons(z0, z1) 11.05/3.26
merge(Nil, z0) → z0 11.05/3.26
splitmerge(Cons(z0, z1), z2, z3) → splitmerge(z1, Cons(z0, z3), z2) 11.05/3.26
splitmerge(Nil, z0, z1) → merge(mergesort(z0), mergesort(z1)) 11.05/3.26
notEmpty(Cons(z0, z1)) → True 11.05/3.26
notEmpty(Nil) → False 11.05/3.26
goal(z0) → mergesort(z0)
Tuples:

<='(S(z0), S(z1)) → c(<='(z0, z1)) 11.05/3.26
MERGESORT(Cons(z0, Cons(z1, z2))) → c3(SPLITMERGE(Cons(z0, Cons(z1, z2)), Nil, Nil)) 11.05/3.26
MERGE(Cons(z0, z1), Cons(z2, z3)) → c6(<='(z0, z2)) 11.05/3.26
SPLITMERGE(Cons(z0, z1), z2, z3) → c9(SPLITMERGE(z1, Cons(z0, z3), z2)) 11.05/3.26
SPLITMERGE(Nil, z0, z1) → c10(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0), MERGESORT(z1))
S tuples:

MERGESORT(Cons(z0, Cons(z1, z2))) → c3(SPLITMERGE(Cons(z0, Cons(z1, z2)), Nil, Nil)) 11.05/3.26
MERGE(Cons(z0, z1), Cons(z2, z3)) → c6(<='(z0, z2)) 11.05/3.26
SPLITMERGE(Cons(z0, z1), z2, z3) → c9(SPLITMERGE(z1, Cons(z0, z3), z2)) 11.05/3.26
SPLITMERGE(Nil, z0, z1) → c10(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0), MERGESORT(z1))
K tuples:none
Defined Rule Symbols:

mergesort, merge, splitmerge, notEmpty, goal, <=

Defined Pair Symbols:

<=', MERGESORT, MERGE, SPLITMERGE

Compound Symbols:

c, c3, c6, c9, c10

11.05/3.27
11.05/3.27

(5) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

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

MERGE(Cons(z0, z1), Cons(z2, z3)) → c6(<='(z0, z2))
We considered the (Usable) Rules:

mergesort(Cons(z0, Cons(z1, z2))) → splitmerge(Cons(z0, Cons(z1, z2)), Nil, Nil) 11.05/3.27
mergesort(Cons(z0, Nil)) → Cons(z0, Nil) 11.05/3.27
mergesort(Nil) → Nil 11.05/3.27
splitmerge(Cons(z0, z1), z2, z3) → splitmerge(z1, Cons(z0, z3), z2) 11.05/3.27
splitmerge(Nil, z0, z1) → merge(mergesort(z0), mergesort(z1)) 11.05/3.27
merge(Cons(z0, z1), Cons(z2, z3)) → merge[Ite][True][Ite][True][Ite](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)) 11.05/3.27
merge(Cons(z0, z1), Nil) → Cons(z0, z1) 11.05/3.27
merge(Nil, z0) → z0 11.05/3.27
<=(S(z0), S(z1)) → <=(z0, z1) 11.05/3.27
<=(0, z0) → True 11.05/3.27
<=(S(z0), 0) → False
And the Tuples:

<='(S(z0), S(z1)) → c(<='(z0, z1)) 11.05/3.27
MERGESORT(Cons(z0, Cons(z1, z2))) → c3(SPLITMERGE(Cons(z0, Cons(z1, z2)), Nil, Nil)) 11.05/3.27
MERGE(Cons(z0, z1), Cons(z2, z3)) → c6(<='(z0, z2)) 11.05/3.27
SPLITMERGE(Cons(z0, z1), z2, z3) → c9(SPLITMERGE(z1, Cons(z0, z3), z2)) 11.05/3.27
SPLITMERGE(Nil, z0, z1) → c10(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0), MERGESORT(z1))
The order we found is given by the following interpretation:
Polynomial interpretation : 11.05/3.27

POL(0) = [3]    11.05/3.27
POL(<=(x1, x2)) = [3] + [3]x1 + [3]x2 + [3]x22 + [3]x1·x2 + [3]x12    11.05/3.27
POL(<='(x1, x2)) = [1]    11.05/3.27
POL(Cons(x1, x2)) = [2] + x2    11.05/3.27
POL(False) = [3]    11.05/3.27
POL(MERGE(x1, x2)) = x2    11.05/3.27
POL(MERGESORT(x1)) = [2]x12    11.05/3.27
POL(Nil) = 0    11.05/3.27
POL(S(x1)) = 0    11.05/3.27
POL(SPLITMERGE(x1, x2, x3)) = [2]x3 + [2]x32 + [3]x1·x3 + [2]x12 + [3]x1·x2 + [2]x22    11.05/3.27
POL(True) = [3]    11.05/3.27
POL(c(x1)) = x1    11.05/3.27
POL(c10(x1, x2, x3)) = x1 + x2 + x3    11.05/3.27
POL(c3(x1)) = x1    11.05/3.27
POL(c6(x1)) = x1    11.05/3.27
POL(c9(x1)) = x1    11.05/3.27
POL(merge(x1, x2)) = x1 + x2    11.05/3.27
POL(merge[Ite][True][Ite][True][Ite](x1, x2, x3)) = [2] + x3    11.05/3.27
POL(mergesort(x1)) = [2]x1    11.05/3.27
POL(splitmerge(x1, x2, x3)) = [2]x1 + [2]x2 + [2]x3   
11.05/3.27
11.05/3.27

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

<=(S(z0), S(z1)) → <=(z0, z1) 11.05/3.27
<=(0, z0) → True 11.05/3.27
<=(S(z0), 0) → False 11.05/3.27
mergesort(Cons(z0, Cons(z1, z2))) → splitmerge(Cons(z0, Cons(z1, z2)), Nil, Nil) 11.05/3.27
mergesort(Cons(z0, Nil)) → Cons(z0, Nil) 11.05/3.27
mergesort(Nil) → Nil 11.05/3.27
merge(Cons(z0, z1), Cons(z2, z3)) → merge[Ite][True][Ite][True][Ite](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)) 11.05/3.27
merge(Cons(z0, z1), Nil) → Cons(z0, z1) 11.05/3.27
merge(Nil, z0) → z0 11.05/3.27
splitmerge(Cons(z0, z1), z2, z3) → splitmerge(z1, Cons(z0, z3), z2) 11.05/3.27
splitmerge(Nil, z0, z1) → merge(mergesort(z0), mergesort(z1)) 11.05/3.27
notEmpty(Cons(z0, z1)) → True 11.05/3.27
notEmpty(Nil) → False 11.05/3.27
goal(z0) → mergesort(z0)
Tuples:

<='(S(z0), S(z1)) → c(<='(z0, z1)) 11.05/3.27
MERGESORT(Cons(z0, Cons(z1, z2))) → c3(SPLITMERGE(Cons(z0, Cons(z1, z2)), Nil, Nil)) 11.05/3.27
MERGE(Cons(z0, z1), Cons(z2, z3)) → c6(<='(z0, z2)) 11.05/3.27
SPLITMERGE(Cons(z0, z1), z2, z3) → c9(SPLITMERGE(z1, Cons(z0, z3), z2)) 11.05/3.27
SPLITMERGE(Nil, z0, z1) → c10(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0), MERGESORT(z1))
S tuples:

MERGESORT(Cons(z0, Cons(z1, z2))) → c3(SPLITMERGE(Cons(z0, Cons(z1, z2)), Nil, Nil)) 11.05/3.27
SPLITMERGE(Cons(z0, z1), z2, z3) → c9(SPLITMERGE(z1, Cons(z0, z3), z2)) 11.05/3.27
SPLITMERGE(Nil, z0, z1) → c10(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0), MERGESORT(z1))
K tuples:

MERGE(Cons(z0, z1), Cons(z2, z3)) → c6(<='(z0, z2))
Defined Rule Symbols:

mergesort, merge, splitmerge, notEmpty, goal, <=

Defined Pair Symbols:

<=', MERGESORT, MERGE, SPLITMERGE

Compound Symbols:

c, c3, c6, c9, c10

11.05/3.27
11.05/3.27

(7) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

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

MERGESORT(Cons(z0, Cons(z1, z2))) → c3(SPLITMERGE(Cons(z0, Cons(z1, z2)), Nil, Nil))
We considered the (Usable) Rules:

mergesort(Cons(z0, Cons(z1, z2))) → splitmerge(Cons(z0, Cons(z1, z2)), Nil, Nil) 11.05/3.27
mergesort(Cons(z0, Nil)) → Cons(z0, Nil) 11.05/3.27
mergesort(Nil) → Nil 11.05/3.27
splitmerge(Cons(z0, z1), z2, z3) → splitmerge(z1, Cons(z0, z3), z2) 11.05/3.27
splitmerge(Nil, z0, z1) → merge(mergesort(z0), mergesort(z1)) 11.05/3.27
merge(Cons(z0, z1), Cons(z2, z3)) → merge[Ite][True][Ite][True][Ite](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)) 11.05/3.27
merge(Cons(z0, z1), Nil) → Cons(z0, z1) 11.05/3.27
merge(Nil, z0) → z0 11.05/3.27
<=(S(z0), S(z1)) → <=(z0, z1) 11.05/3.27
<=(0, z0) → True 11.05/3.27
<=(S(z0), 0) → False
And the Tuples:

<='(S(z0), S(z1)) → c(<='(z0, z1)) 11.05/3.27
MERGESORT(Cons(z0, Cons(z1, z2))) → c3(SPLITMERGE(Cons(z0, Cons(z1, z2)), Nil, Nil)) 11.05/3.27
MERGE(Cons(z0, z1), Cons(z2, z3)) → c6(<='(z0, z2)) 11.05/3.27
SPLITMERGE(Cons(z0, z1), z2, z3) → c9(SPLITMERGE(z1, Cons(z0, z3), z2)) 11.05/3.27
SPLITMERGE(Nil, z0, z1) → c10(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0), MERGESORT(z1))
The order we found is given by the following interpretation:
Polynomial interpretation : 11.05/3.27

POL(0) = [3]    11.05/3.27
POL(<=(x1, x2)) = [3] + [3]x1 + [3]x2 + [3]x22 + [3]x1·x2 + [3]x12    11.05/3.27
POL(<='(x1, x2)) = 0    11.05/3.27
POL(Cons(x1, x2)) = [1] + x2    11.05/3.27
POL(False) = [3]    11.05/3.27
POL(MERGE(x1, x2)) = 0    11.05/3.27
POL(MERGESORT(x1)) = [1] + [2]x12    11.05/3.27
POL(Nil) = 0    11.05/3.27
POL(S(x1)) = 0    11.05/3.27
POL(SPLITMERGE(x1, x2, x3)) = [2] + x1 + [2]x3 + [2]x32 + [2]x1·x3 + x12 + [2]x1·x2 + [2]x22    11.05/3.27
POL(True) = [3]    11.05/3.27
POL(c(x1)) = x1    11.05/3.27
POL(c10(x1, x2, x3)) = x1 + x2 + x3    11.05/3.27
POL(c3(x1)) = x1    11.05/3.27
POL(c6(x1)) = x1    11.05/3.27
POL(c9(x1)) = x1    11.05/3.27
POL(merge(x1, x2)) = [3]    11.05/3.27
POL(merge[Ite][True][Ite][True][Ite](x1, x2, x3)) = [3]    11.05/3.27
POL(mergesort(x1)) = 0    11.05/3.27
POL(splitmerge(x1, x2, x3)) = [3] + [3]x1 + [3]x2 + [3]x3 + [3]x32 + [3]x2·x3 + [3]x1·x3 + [3]x12 + [3]x1·x2 + [3]x22   
11.05/3.27
11.05/3.27

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

<=(S(z0), S(z1)) → <=(z0, z1) 11.05/3.27
<=(0, z0) → True 11.05/3.27
<=(S(z0), 0) → False 11.05/3.27
mergesort(Cons(z0, Cons(z1, z2))) → splitmerge(Cons(z0, Cons(z1, z2)), Nil, Nil) 11.05/3.27
mergesort(Cons(z0, Nil)) → Cons(z0, Nil) 11.05/3.27
mergesort(Nil) → Nil 11.05/3.27
merge(Cons(z0, z1), Cons(z2, z3)) → merge[Ite][True][Ite][True][Ite](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)) 11.05/3.27
merge(Cons(z0, z1), Nil) → Cons(z0, z1) 11.05/3.27
merge(Nil, z0) → z0 11.05/3.27
splitmerge(Cons(z0, z1), z2, z3) → splitmerge(z1, Cons(z0, z3), z2) 11.05/3.27
splitmerge(Nil, z0, z1) → merge(mergesort(z0), mergesort(z1)) 11.05/3.27
notEmpty(Cons(z0, z1)) → True 11.05/3.27
notEmpty(Nil) → False 11.05/3.27
goal(z0) → mergesort(z0)
Tuples:

<='(S(z0), S(z1)) → c(<='(z0, z1)) 11.05/3.27
MERGESORT(Cons(z0, Cons(z1, z2))) → c3(SPLITMERGE(Cons(z0, Cons(z1, z2)), Nil, Nil)) 11.05/3.27
MERGE(Cons(z0, z1), Cons(z2, z3)) → c6(<='(z0, z2)) 11.05/3.27
SPLITMERGE(Cons(z0, z1), z2, z3) → c9(SPLITMERGE(z1, Cons(z0, z3), z2)) 11.05/3.27
SPLITMERGE(Nil, z0, z1) → c10(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0), MERGESORT(z1))
S tuples:

SPLITMERGE(Cons(z0, z1), z2, z3) → c9(SPLITMERGE(z1, Cons(z0, z3), z2)) 11.05/3.27
SPLITMERGE(Nil, z0, z1) → c10(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0), MERGESORT(z1))
K tuples:

MERGE(Cons(z0, z1), Cons(z2, z3)) → c6(<='(z0, z2)) 11.05/3.27
MERGESORT(Cons(z0, Cons(z1, z2))) → c3(SPLITMERGE(Cons(z0, Cons(z1, z2)), Nil, Nil))
Defined Rule Symbols:

mergesort, merge, splitmerge, notEmpty, goal, <=

Defined Pair Symbols:

<=', MERGESORT, MERGE, SPLITMERGE

Compound Symbols:

c, c3, c6, c9, c10

11.05/3.27
11.05/3.27

(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

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

SPLITMERGE(Nil, z0, z1) → c10(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0), MERGESORT(z1))
We considered the (Usable) Rules:

mergesort(Cons(z0, Cons(z1, z2))) → splitmerge(Cons(z0, Cons(z1, z2)), Nil, Nil) 11.05/3.27
mergesort(Cons(z0, Nil)) → Cons(z0, Nil) 11.05/3.27
mergesort(Nil) → Nil 11.05/3.27
splitmerge(Cons(z0, z1), z2, z3) → splitmerge(z1, Cons(z0, z3), z2) 11.05/3.27
splitmerge(Nil, z0, z1) → merge(mergesort(z0), mergesort(z1)) 11.05/3.27
merge(Cons(z0, z1), Cons(z2, z3)) → merge[Ite][True][Ite][True][Ite](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)) 11.05/3.27
merge(Cons(z0, z1), Nil) → Cons(z0, z1) 11.05/3.27
merge(Nil, z0) → z0 11.05/3.27
<=(S(z0), S(z1)) → <=(z0, z1) 11.05/3.27
<=(0, z0) → True 11.05/3.27
<=(S(z0), 0) → False
And the Tuples:

<='(S(z0), S(z1)) → c(<='(z0, z1)) 11.05/3.27
MERGESORT(Cons(z0, Cons(z1, z2))) → c3(SPLITMERGE(Cons(z0, Cons(z1, z2)), Nil, Nil)) 11.05/3.27
MERGE(Cons(z0, z1), Cons(z2, z3)) → c6(<='(z0, z2)) 11.05/3.27
SPLITMERGE(Cons(z0, z1), z2, z3) → c9(SPLITMERGE(z1, Cons(z0, z3), z2)) 11.05/3.27
SPLITMERGE(Nil, z0, z1) → c10(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0), MERGESORT(z1))
The order we found is given by the following interpretation:
Polynomial interpretation : 11.05/3.27

POL(0) = [3]    11.05/3.27
POL(<=(x1, x2)) = [3] + [3]x1 + [3]x2 + [3]x22 + [3]x1·x2 + [3]x12    11.05/3.27
POL(<='(x1, x2)) = 0    11.05/3.27
POL(Cons(x1, x2)) = [1] + x2    11.05/3.27
POL(False) = [3]    11.05/3.27
POL(MERGE(x1, x2)) = 0    11.05/3.27
POL(MERGESORT(x1)) = [2]x12    11.05/3.27
POL(Nil) = 0    11.05/3.27
POL(S(x1)) = 0    11.05/3.27
POL(SPLITMERGE(x1, x2, x3)) = [1] + x1 + [2]x3 + [2]x32 + [2]x1·x3 + x12 + [2]x1·x2 + [2]x22    11.05/3.27
POL(True) = [3]    11.05/3.27
POL(c(x1)) = x1    11.05/3.27
POL(c10(x1, x2, x3)) = x1 + x2 + x3    11.05/3.27
POL(c3(x1)) = x1    11.05/3.27
POL(c6(x1)) = x1    11.05/3.27
POL(c9(x1)) = x1    11.05/3.27
POL(merge(x1, x2)) = [3]    11.05/3.27
POL(merge[Ite][True][Ite][True][Ite](x1, x2, x3)) = [3]    11.05/3.27
POL(mergesort(x1)) = 0    11.05/3.27
POL(splitmerge(x1, x2, x3)) = [3] + [3]x1 + [3]x2 + [3]x3 + [3]x32 + [3]x2·x3 + [3]x1·x3 + [3]x12 + [3]x1·x2 + [3]x22   
11.05/3.27
11.05/3.27

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

<=(S(z0), S(z1)) → <=(z0, z1) 11.05/3.27
<=(0, z0) → True 11.05/3.27
<=(S(z0), 0) → False 11.05/3.27
mergesort(Cons(z0, Cons(z1, z2))) → splitmerge(Cons(z0, Cons(z1, z2)), Nil, Nil) 11.05/3.27
mergesort(Cons(z0, Nil)) → Cons(z0, Nil) 11.05/3.27
mergesort(Nil) → Nil 11.05/3.27
merge(Cons(z0, z1), Cons(z2, z3)) → merge[Ite][True][Ite][True][Ite](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)) 11.05/3.27
merge(Cons(z0, z1), Nil) → Cons(z0, z1) 11.05/3.27
merge(Nil, z0) → z0 11.05/3.27
splitmerge(Cons(z0, z1), z2, z3) → splitmerge(z1, Cons(z0, z3), z2) 11.05/3.27
splitmerge(Nil, z0, z1) → merge(mergesort(z0), mergesort(z1)) 11.05/3.27
notEmpty(Cons(z0, z1)) → True 11.05/3.27
notEmpty(Nil) → False 11.05/3.27
goal(z0) → mergesort(z0)
Tuples:

<='(S(z0), S(z1)) → c(<='(z0, z1)) 11.05/3.27
MERGESORT(Cons(z0, Cons(z1, z2))) → c3(SPLITMERGE(Cons(z0, Cons(z1, z2)), Nil, Nil)) 11.05/3.27
MERGE(Cons(z0, z1), Cons(z2, z3)) → c6(<='(z0, z2)) 11.05/3.27
SPLITMERGE(Cons(z0, z1), z2, z3) → c9(SPLITMERGE(z1, Cons(z0, z3), z2)) 11.05/3.27
SPLITMERGE(Nil, z0, z1) → c10(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0), MERGESORT(z1))
S tuples:

SPLITMERGE(Cons(z0, z1), z2, z3) → c9(SPLITMERGE(z1, Cons(z0, z3), z2))
K tuples:

MERGE(Cons(z0, z1), Cons(z2, z3)) → c6(<='(z0, z2)) 11.05/3.27
MERGESORT(Cons(z0, Cons(z1, z2))) → c3(SPLITMERGE(Cons(z0, Cons(z1, z2)), Nil, Nil)) 11.05/3.27
SPLITMERGE(Nil, z0, z1) → c10(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0), MERGESORT(z1))
Defined Rule Symbols:

mergesort, merge, splitmerge, notEmpty, goal, <=

Defined Pair Symbols:

<=', MERGESORT, MERGE, SPLITMERGE

Compound Symbols:

c, c3, c6, c9, c10

11.05/3.27
11.05/3.27

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

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

SPLITMERGE(Cons(z0, z1), z2, z3) → c9(SPLITMERGE(z1, Cons(z0, z3), z2))
We considered the (Usable) Rules:

mergesort(Cons(z0, Cons(z1, z2))) → splitmerge(Cons(z0, Cons(z1, z2)), Nil, Nil) 11.05/3.27
mergesort(Cons(z0, Nil)) → Cons(z0, Nil) 11.05/3.27
mergesort(Nil) → Nil 11.05/3.27
splitmerge(Cons(z0, z1), z2, z3) → splitmerge(z1, Cons(z0, z3), z2) 11.05/3.27
splitmerge(Nil, z0, z1) → merge(mergesort(z0), mergesort(z1)) 11.05/3.27
merge(Cons(z0, z1), Cons(z2, z3)) → merge[Ite][True][Ite][True][Ite](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)) 11.05/3.27
merge(Cons(z0, z1), Nil) → Cons(z0, z1) 11.05/3.27
merge(Nil, z0) → z0 11.05/3.27
<=(S(z0), S(z1)) → <=(z0, z1) 11.05/3.27
<=(0, z0) → True 11.05/3.27
<=(S(z0), 0) → False
And the Tuples:

<='(S(z0), S(z1)) → c(<='(z0, z1)) 11.05/3.27
MERGESORT(Cons(z0, Cons(z1, z2))) → c3(SPLITMERGE(Cons(z0, Cons(z1, z2)), Nil, Nil)) 11.05/3.27
MERGE(Cons(z0, z1), Cons(z2, z3)) → c6(<='(z0, z2)) 11.05/3.27
SPLITMERGE(Cons(z0, z1), z2, z3) → c9(SPLITMERGE(z1, Cons(z0, z3), z2)) 11.05/3.27
SPLITMERGE(Nil, z0, z1) → c10(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0), MERGESORT(z1))
The order we found is given by the following interpretation:
Polynomial interpretation : 11.05/3.27

POL(0) = [3]    11.05/3.27
POL(<=(x1, x2)) = [3] + [3]x1 + [3]x2 + [3]x22 + [3]x1·x2 + [3]x12    11.05/3.27
POL(<='(x1, x2)) = 0    11.05/3.27
POL(Cons(x1, x2)) = [1] + x2    11.05/3.27
POL(False) = [3]    11.05/3.27
POL(MERGE(x1, x2)) = 0    11.05/3.27
POL(MERGESORT(x1)) = [3]x12    11.05/3.27
POL(Nil) = 0    11.05/3.27
POL(S(x1)) = 0    11.05/3.27
POL(SPLITMERGE(x1, x2, x3)) = [2]x1 + [3]x3 + [3]x32 + [3]x1·x3 + [2]x12 + [3]x1·x2 + [3]x22    11.05/3.27
POL(True) = [3]    11.05/3.27
POL(c(x1)) = x1    11.05/3.27
POL(c10(x1, x2, x3)) = x1 + x2 + x3    11.05/3.27
POL(c3(x1)) = x1    11.05/3.27
POL(c6(x1)) = x1    11.05/3.27
POL(c9(x1)) = x1    11.05/3.27
POL(merge(x1, x2)) = [3]    11.05/3.27
POL(merge[Ite][True][Ite][True][Ite](x1, x2, x3)) = [3]    11.05/3.27
POL(mergesort(x1)) = 0    11.05/3.27
POL(splitmerge(x1, x2, x3)) = [3] + [3]x1 + [3]x2 + [3]x3 + [3]x32 + [3]x2·x3 + [3]x1·x3 + [3]x12 + [3]x1·x2 + [3]x22   
11.05/3.27
11.05/3.27

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

<=(S(z0), S(z1)) → <=(z0, z1) 11.05/3.27
<=(0, z0) → True 11.05/3.27
<=(S(z0), 0) → False 11.05/3.27
mergesort(Cons(z0, Cons(z1, z2))) → splitmerge(Cons(z0, Cons(z1, z2)), Nil, Nil) 11.05/3.27
mergesort(Cons(z0, Nil)) → Cons(z0, Nil) 11.05/3.27
mergesort(Nil) → Nil 11.05/3.27
merge(Cons(z0, z1), Cons(z2, z3)) → merge[Ite][True][Ite][True][Ite](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)) 11.05/3.27
merge(Cons(z0, z1), Nil) → Cons(z0, z1) 11.05/3.27
merge(Nil, z0) → z0 11.05/3.27
splitmerge(Cons(z0, z1), z2, z3) → splitmerge(z1, Cons(z0, z3), z2) 11.05/3.27
splitmerge(Nil, z0, z1) → merge(mergesort(z0), mergesort(z1)) 11.05/3.27
notEmpty(Cons(z0, z1)) → True 11.05/3.27
notEmpty(Nil) → False 11.05/3.27
goal(z0) → mergesort(z0)
Tuples:

<='(S(z0), S(z1)) → c(<='(z0, z1)) 11.05/3.27
MERGESORT(Cons(z0, Cons(z1, z2))) → c3(SPLITMERGE(Cons(z0, Cons(z1, z2)), Nil, Nil)) 11.05/3.27
MERGE(Cons(z0, z1), Cons(z2, z3)) → c6(<='(z0, z2)) 11.05/3.27
SPLITMERGE(Cons(z0, z1), z2, z3) → c9(SPLITMERGE(z1, Cons(z0, z3), z2)) 11.05/3.27
SPLITMERGE(Nil, z0, z1) → c10(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0), MERGESORT(z1))
S tuples:none
K tuples:

MERGE(Cons(z0, z1), Cons(z2, z3)) → c6(<='(z0, z2)) 11.05/3.27
MERGESORT(Cons(z0, Cons(z1, z2))) → c3(SPLITMERGE(Cons(z0, Cons(z1, z2)), Nil, Nil)) 11.05/3.27
SPLITMERGE(Nil, z0, z1) → c10(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0), MERGESORT(z1)) 11.05/3.27
SPLITMERGE(Cons(z0, z1), z2, z3) → c9(SPLITMERGE(z1, Cons(z0, z3), z2))
Defined Rule Symbols:

mergesort, merge, splitmerge, notEmpty, goal, <=

Defined Pair Symbols:

<=', MERGESORT, MERGE, SPLITMERGE

Compound Symbols:

c, c3, c6, c9, c10

11.05/3.27
11.05/3.27

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

The set S is empty
11.05/3.27
11.05/3.27

(14) BOUNDS(O(1), O(1))

11.05/3.27
11.05/3.27
11.34/3.33 EOF