Runtime Complexity (innermost) proof of /tmp/tmpAY2CrK/quicksort.raml.xml

The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^2).

0 CpxRelTRS

↳1 RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)

↳2 CpxWeightedTrs

↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)

↳4 CpxTypedWeightedTrs

↳5 CompletionProof (UPPER BOUND(ID), 0 ms)

↳6 CpxTypedWeightedCompleteTrs

↳7 NarrowingProof (BOTH BOUNDS(ID, ID), 13 ms)

↳8 CpxTypedWeightedCompleteTrs

↳9 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 4 ms)

↳10 CpxRNTS

↳11 InliningProof (UPPER BOUND(ID), 741 ms)

↳12 CpxRNTS

↳13 SimplificationProof (BOTH BOUNDS(ID, ID), 10 ms)

↳14 CpxRNTS

↳15 CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID), 0 ms)

↳16 CpxRNTS

↳17 IntTrsBoundProof (UPPER BOUND(ID), 814 ms)

↳18 CpxRNTS

↳19 IntTrsBoundProof (UPPER BOUND(ID), 221 ms)

↳20 CpxRNTS

↳21 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳22 CpxRNTS

↳23 IntTrsBoundProof (UPPER BOUND(ID), 512 ms)

↳24 CpxRNTS

↳25 IntTrsBoundProof (UPPER BOUND(ID), 47 ms)

↳26 CpxRNTS

↳27 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳28 CpxRNTS

↳29 IntTrsBoundProof (UPPER BOUND(ID), 452 ms)

↳30 CpxRNTS

↳31 IntTrsBoundProof (UPPER BOUND(ID), 100 ms)

↳32 CpxRNTS

↳33 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳34 CpxRNTS

↳35 IntTrsBoundProof (UPPER BOUND(ID), 1385 ms)

↳36 CpxRNTS

↳37 IntTrsBoundProof (UPPER BOUND(ID), 239 ms)

↳38 CpxRNTS

↳39 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳40 CpxRNTS

↳41 IntTrsBoundProof (UPPER BOUND(ID), 221 ms)

↳42 CpxRNTS

↳43 IntTrsBoundProof (UPPER BOUND(ID), 63 ms)

↳44 CpxRNTS

↳45 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳46 CpxRNTS

↳47 IntTrsBoundProof (UPPER BOUND(ID), 673 ms)

↳48 CpxRNTS

↳49 IntTrsBoundProof (UPPER BOUND(ID), 122 ms)

↳50 CpxRNTS

↳51 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳52 CpxRNTS

↳53 IntTrsBoundProof (UPPER BOUND(ID), 114 ms)

↳54 CpxRNTS

↳55 IntTrsBoundProof (UPPER BOUND(ID), 52 ms)

↳56 CpxRNTS

↳57 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳58 CpxRNTS

↳59 IntTrsBoundProof (UPPER BOUND(ID), 265 ms)

↳60 CpxRNTS

↳61 IntTrsBoundProof (UPPER BOUND(ID), 36 ms)

↳62 CpxRNTS

↳63 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳64 CpxRNTS

↳65 IntTrsBoundProof (UPPER BOUND(ID), 175 ms)

↳66 CpxRNTS

↳67 IntTrsBoundProof (UPPER BOUND(ID), 5 ms)

↳68 CpxRNTS

↳69 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳70 CpxRNTS

↳71 IntTrsBoundProof (UPPER BOUND(ID), 600 ms)

↳72 CpxRNTS

↳73 IntTrsBoundProof (UPPER BOUND(ID), 113 ms)

↳74 CpxRNTS

↳75 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳76 CpxRNTS

↳77 IntTrsBoundProof (UPPER BOUND(ID), 570 ms)

↳78 CpxRNTS

↳79 IntTrsBoundProof (UPPER BOUND(ID), 56 ms)

↳80 CpxRNTS

↳81 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳82 CpxRNTS

↳83 IntTrsBoundProof (UPPER BOUND(ID), 283 ms)

↳84 CpxRNTS

↳85 IntTrsBoundProof (UPPER BOUND(ID), 74 ms)

↳86 CpxRNTS

↳87 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳88 CpxRNTS

↳89 IntTrsBoundProof (UPPER BOUND(ID), 423 ms)

↳90 CpxRNTS

↳91 IntTrsBoundProof (UPPER BOUND(ID), 37 ms)

↳92 CpxRNTS

↳93 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳94 CpxRNTS

↳95 IntTrsBoundProof (UPPER BOUND(ID), 171 ms)

↳96 CpxRNTS

↳97 IntTrsBoundProof (UPPER BOUND(ID), 46 ms)

↳98 CpxRNTS

↳99 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳100 CpxRNTS

↳101 IntTrsBoundProof (UPPER BOUND(ID), 514 ms)

↳102 CpxRNTS

↳103 IntTrsBoundProof (UPPER BOUND(ID), 266 ms)

↳104 CpxRNTS

↳105 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳106 CpxRNTS

↳107 IntTrsBoundProof (UPPER BOUND(ID), 1577 ms)

↳108 CpxRNTS

↳109 IntTrsBoundProof (UPPER BOUND(ID), 855 ms)

↳110 CpxRNTS

↳111 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳112 CpxRNTS

↳113 IntTrsBoundProof (UPPER BOUND(ID), 192 ms)

↳114 CpxRNTS

↳115 IntTrsBoundProof (UPPER BOUND(ID), 62 ms)

↳116 CpxRNTS

↳117 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳118 CpxRNTS

↳119 IntTrsBoundProof (UPPER BOUND(ID), 70 ms)

↳120 CpxRNTS

↳121 IntTrsBoundProof (UPPER BOUND(ID), 4 ms)

↳122 CpxRNTS

↳123 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳124 CpxRNTS

↳125 IntTrsBoundProof (UPPER BOUND(ID), 121 ms)

↳126 CpxRNTS

↳127 IntTrsBoundProof (UPPER BOUND(ID), 3 ms)

↳128 CpxRNTS

↳129 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳130 CpxRNTS

↳131 IntTrsBoundProof (UPPER BOUND(ID), 323 ms)

↳132 CpxRNTS

↳133 IntTrsBoundProof (UPPER BOUND(ID), 10 ms)

↳134 CpxRNTS

↳135 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳136 CpxRNTS

↳137 IntTrsBoundProof (UPPER BOUND(ID), 276 ms)

↳138 CpxRNTS

↳139 IntTrsBoundProof (UPPER BOUND(ID), 20 ms)

↳140 CpxRNTS

↳141 FinalProof (⇔, 0 ms)

↳142 BOUNDS(1, n^2)

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^2).

The TRS R consists of the following rules:

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

Rewrite Strategy: INNERMOST

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

Transformed relative TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^2).

The TRS R consists of the following rules:

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

The TRS has the following type information:

#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#greater :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#ckgt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
appendD :: :::nil → :::nil → :::nil
appendD#1 :: :::nil → :::nil → :::nil
quicksort :: :::nil → :::nil
quicksort#1 :: :::nil → :::nil
quicksort#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
split :: #0:#neg:#pos:#s → :::nil → tuple#2
tuple#2 :: :::nil → :::nil → tuple#2
quicksortD :: :::nil → :::nil
quicksortD#1 :: :::nil → :::nil
quicksortD#2 :: tuple#2 → #0:#neg:#pos:#s → :::nil
splitD :: #0:#neg:#pos:#s → :::nil → tuple#2
split#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
split#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
split#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
#false :: #false:#true
#true :: #false:#true
splitD#1 :: :::nil → #0:#neg:#pos:#s → tuple#2
splitD#2 :: tuple#2 → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2
splitD#3 :: #false:#true → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2
testList :: #unit → :::nil
testQuicksort :: a → :::nil
#unit :: #unit
testQuicksort2 :: b → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT

Rewrite Strategy: INNERMOST

(5) CompletionProof (UPPER BOUND(ID) transformation)

The transformation into a RNTS is sound, since:

(a) The obligation is a constructor system where every type has a constant constructor,

(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:

Due to the following rules being added:

And the following fresh constants:

(6) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

The TRS has the following type information:

#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#greater :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true:null_#ckgt
#ckgt :: #EQ:#GT:#LT:null_#compare → #false:#true:null_#ckgt
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT:null_#compare
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
appendD :: :::nil → :::nil → :::nil
appendD#1 :: :::nil → :::nil → :::nil
quicksort :: :::nil → :::nil
quicksort#1 :: :::nil → :::nil
quicksort#2 :: tuple#2:const → #0:#neg:#pos:#s → :::nil
split :: #0:#neg:#pos:#s → :::nil → tuple#2:const
tuple#2 :: :::nil → :::nil → tuple#2:const
quicksortD :: :::nil → :::nil
quicksortD#1 :: :::nil → :::nil
quicksortD#2 :: tuple#2:const → #0:#neg:#pos:#s → :::nil
splitD :: #0:#neg:#pos:#s → :::nil → tuple#2:const
split#1 :: :::nil → #0:#neg:#pos:#s → tuple#2:const
split#2 :: tuple#2:const → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2:const
split#3 :: #false:#true:null_#ckgt → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2:const
#false :: #false:#true:null_#ckgt
#true :: #false:#true:null_#ckgt
splitD#1 :: :::nil → #0:#neg:#pos:#s → tuple#2:const
splitD#2 :: tuple#2:const → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2:const
splitD#3 :: #false:#true:null_#ckgt → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2:const
testList :: #unit → :::nil
testQuicksort :: a → :::nil
#unit :: #unit
testQuicksort2 :: b → :::nil
#EQ :: #EQ:#GT:#LT:null_#compare
#GT :: #EQ:#GT:#LT:null_#compare
#LT :: #EQ:#GT:#LT:null_#compare
null_#ckgt :: #false:#true:null_#ckgt
null_#compare :: #EQ:#GT:#LT:null_#compare
const :: tuple#2:const
const1 :: a
const2 :: b

Rewrite Strategy: INNERMOST

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

Narrowed the inner basic terms of all right-hand sides by a single narrowing step.

(8) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

The TRS has the following type information:

#abs :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#greater :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true:null_#ckgt
#ckgt :: #EQ:#GT:#LT:null_#compare → #false:#true:null_#ckgt
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT:null_#compare
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
appendD :: :::nil → :::nil → :::nil
appendD#1 :: :::nil → :::nil → :::nil
quicksort :: :::nil → :::nil
quicksort#1 :: :::nil → :::nil
quicksort#2 :: tuple#2:const → #0:#neg:#pos:#s → :::nil
split :: #0:#neg:#pos:#s → :::nil → tuple#2:const
tuple#2 :: :::nil → :::nil → tuple#2:const
quicksortD :: :::nil → :::nil
quicksortD#1 :: :::nil → :::nil
quicksortD#2 :: tuple#2:const → #0:#neg:#pos:#s → :::nil
splitD :: #0:#neg:#pos:#s → :::nil → tuple#2:const
split#1 :: :::nil → #0:#neg:#pos:#s → tuple#2:const
split#2 :: tuple#2:const → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2:const
split#3 :: #false:#true:null_#ckgt → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2:const
#false :: #false:#true:null_#ckgt
#true :: #false:#true:null_#ckgt
splitD#1 :: :::nil → #0:#neg:#pos:#s → tuple#2:const
splitD#2 :: tuple#2:const → #0:#neg:#pos:#s → #0:#neg:#pos:#s → tuple#2:const
splitD#3 :: #false:#true:null_#ckgt → :::nil → :::nil → #0:#neg:#pos:#s → tuple#2:const
testList :: #unit → :::nil
testQuicksort :: a → :::nil
#unit :: #unit
testQuicksort2 :: b → :::nil
#EQ :: #EQ:#GT:#LT:null_#compare
#GT :: #EQ:#GT:#LT:null_#compare
#LT :: #EQ:#GT:#LT:null_#compare
null_#ckgt :: #false:#true:null_#ckgt
null_#compare :: #EQ:#GT:#LT:null_#compare
const :: tuple#2:const
const1 :: a
const2 :: b

Rewrite Strategy: INNERMOST

(9) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

(10) Obligation:

Complexity RNTS consisting of the following rules:

(11) InliningProof (UPPER BOUND(ID) transformation)

Inlined the following terminating rules on right-hand sides where appropriate:

(12) Obligation:

Complexity RNTS consisting of the following rules:

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

Simplified the RNTS by moving equalities from the constraints into the right-hand sides.

(14) Obligation:

Complexity RNTS consisting of the following rules:

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

Found the following analysis order by SCC decomposition:

{ appendD, appendD#1 }
{ split#3 }
{ splitD#3 }
{ #compare }
{ #ckgt }
{ append#1, append }
{ #abs }
{ split#2 }
{ splitD#2 }
{ #greater }
{ testList }
{ split#1 }
{ splitD#1 }
{ split }
{ quicksort#1, quicksort#2 }
{ quicksortD#2, quicksortD#1 }
{ splitD }
{ quicksort }
{ quicksortD }
{ testQuicksort2 }
{ testQuicksort }

(16) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {appendD,appendD#1}, {split#3}, {splitD#3}, {#compare}, {#ckgt}, {append#1,append}, {#abs}, {split#2}, {splitD#2}, {#greater}, {testList}, {split#1}, {splitD#1}, {split}, {quicksort#1,quicksort#2}, {quicksortD#2,quicksortD#1}, {splitD}, {quicksort}, {quicksortD}, {testQuicksort2}, {testQuicksort}

(17) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: appendD
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z + z'

Computed SIZE bound using CoFloCo for: appendD#1
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z + z'

(18) Obligation:

Complexity RNTS consisting of the following rules:

appendD: runtime: ?, size: O(n¹) [z + z']
appendD#1: runtime: ?, size: O(n¹) [z + z']

(19) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: appendD
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 2 + 2·z

Computed RUNTIME bound using CoFloCo for: appendD#1
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + 2·z

(20) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {split#3}, {splitD#3}, {#compare}, {#ckgt}, {append#1,append}, {#abs}, {split#2}, {splitD#2}, {#greater}, {testList}, {split#1}, {splitD#1}, {split}, {quicksort#1,quicksort#2}, {quicksortD#2,quicksortD#1}, {splitD}, {quicksort}, {quicksortD}, {testQuicksort2}, {testQuicksort}
Previous analysis results are:

appendD: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
appendD#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']

(21) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(22) Obligation:

Complexity RNTS consisting of the following rules:

appendD: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
appendD#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']

(23) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: split#3
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 2 + z' + z'' + z1

(24) Obligation:

Complexity RNTS consisting of the following rules:

appendD: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
appendD#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
split#3: runtime: ?, size: O(n¹) [2 + z' + z'' + z1]

(25) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: split#3
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(26) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {splitD#3}, {#compare}, {#ckgt}, {append#1,append}, {#abs}, {split#2}, {splitD#2}, {#greater}, {testList}, {split#1}, {splitD#1}, {split}, {quicksort#1,quicksort#2}, {quicksortD#2,quicksortD#1}, {splitD}, {quicksort}, {quicksortD}, {testQuicksort2}, {testQuicksort}
Previous analysis results are:

appendD: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
appendD#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
split#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]

(27) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(28) Obligation:

Complexity RNTS consisting of the following rules:

appendD: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
appendD#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
split#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]

(29) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: splitD#3
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 2 + z' + z'' + z1

(30) Obligation:

Complexity RNTS consisting of the following rules:

(31) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: splitD#3
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(32) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {#compare}, {#ckgt}, {append#1,append}, {#abs}, {split#2}, {splitD#2}, {#greater}, {testList}, {split#1}, {splitD#1}, {split}, {quicksort#1,quicksort#2}, {quicksortD#2,quicksortD#1}, {splitD}, {quicksort}, {quicksortD}, {testQuicksort2}, {testQuicksort}
Previous analysis results are:

(33) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(34) Obligation:

Complexity RNTS consisting of the following rules:

(35) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: #compare
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 3

(36) Obligation:

Complexity RNTS consisting of the following rules:

(37) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: #compare
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

(38) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {#ckgt}, {append#1,append}, {#abs}, {split#2}, {splitD#2}, {#greater}, {testList}, {split#1}, {splitD#1}, {split}, {quicksort#1,quicksort#2}, {quicksortD#2,quicksortD#1}, {splitD}, {quicksort}, {quicksortD}, {testQuicksort2}, {testQuicksort}
Previous analysis results are:

(39) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(40) Obligation:

Complexity RNTS consisting of the following rules:

(41) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: #ckgt
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 2

(42) Obligation:

Complexity RNTS consisting of the following rules:

(43) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: #ckgt
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

(44) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {append#1,append}, {#abs}, {split#2}, {splitD#2}, {#greater}, {testList}, {split#1}, {splitD#1}, {split}, {quicksort#1,quicksort#2}, {quicksortD#2,quicksortD#1}, {splitD}, {quicksort}, {quicksortD}, {testQuicksort2}, {testQuicksort}
Previous analysis results are:

(45) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(46) Obligation:

Complexity RNTS consisting of the following rules:

(47) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: append#1
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z + z'

Computed SIZE bound using CoFloCo for: append
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z + z'

(48) Obligation:

Complexity RNTS consisting of the following rules:

(49) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using PUBS for: append#1
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + 2·z

Computed RUNTIME bound using CoFloCo for: append
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 2 + 2·z

(50) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {#abs}, {split#2}, {splitD#2}, {#greater}, {testList}, {split#1}, {splitD#1}, {split}, {quicksort#1,quicksort#2}, {quicksortD#2,quicksortD#1}, {splitD}, {quicksort}, {quicksortD}, {testQuicksort2}, {testQuicksort}
Previous analysis results are:

(51) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(52) Obligation:

Complexity RNTS consisting of the following rules:

(53) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: #abs
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(54) Obligation:

Complexity RNTS consisting of the following rules:

(55) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: #abs
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(56) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {split#2}, {splitD#2}, {#greater}, {testList}, {split#1}, {splitD#1}, {split}, {quicksort#1,quicksort#2}, {quicksortD#2,quicksortD#1}, {splitD}, {quicksort}, {quicksortD}, {testQuicksort2}, {testQuicksort}
Previous analysis results are:

(57) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(58) Obligation:

Complexity RNTS consisting of the following rules:

(59) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: split#2
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z + z''

(60) Obligation:

Complexity RNTS consisting of the following rules:

(61) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: split#2
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 3

(62) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {splitD#2}, {#greater}, {testList}, {split#1}, {splitD#1}, {split}, {quicksort#1,quicksort#2}, {quicksortD#2,quicksortD#1}, {splitD}, {quicksort}, {quicksortD}, {testQuicksort2}, {testQuicksort}
Previous analysis results are:

(63) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(64) Obligation:

Complexity RNTS consisting of the following rules:

(65) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: splitD#2
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z + z''

(66) Obligation:

Complexity RNTS consisting of the following rules:

(67) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: splitD#2
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 3

(68) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {#greater}, {testList}, {split#1}, {splitD#1}, {split}, {quicksort#1,quicksort#2}, {quicksortD#2,quicksortD#1}, {splitD}, {quicksort}, {quicksortD}, {testQuicksort2}, {testQuicksort}
Previous analysis results are:

(69) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(70) Obligation:

Complexity RNTS consisting of the following rules:

(71) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: #greater
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 2

(72) Obligation:

Complexity RNTS consisting of the following rules:

(73) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: #greater
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(74) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {testList}, {split#1}, {splitD#1}, {split}, {quicksort#1,quicksort#2}, {quicksortD#2,quicksortD#1}, {splitD}, {quicksort}, {quicksortD}, {testQuicksort2}, {testQuicksort}
Previous analysis results are:

(75) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(76) Obligation:

Complexity RNTS consisting of the following rules:

(77) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: testList
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 74

(78) Obligation:

Complexity RNTS consisting of the following rules:

(79) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: testList
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 11

(80) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {split#1}, {splitD#1}, {split}, {quicksort#1,quicksort#2}, {quicksortD#2,quicksortD#1}, {splitD}, {quicksort}, {quicksortD}, {testQuicksort2}, {testQuicksort}
Previous analysis results are:

(81) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(82) Obligation:

Complexity RNTS consisting of the following rules:

(83) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: split#1
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(84) Obligation:

Complexity RNTS consisting of the following rules:

(85) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: split#1
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + 5·z

(86) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {splitD#1}, {split}, {quicksort#1,quicksort#2}, {quicksortD#2,quicksortD#1}, {splitD}, {quicksort}, {quicksortD}, {testQuicksort2}, {testQuicksort}
Previous analysis results are:

(87) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(88) Obligation:

Complexity RNTS consisting of the following rules:

(89) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: splitD#1
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(90) Obligation:

Complexity RNTS consisting of the following rules:

(91) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: splitD#1
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + 5·z

(92) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {split}, {quicksort#1,quicksort#2}, {quicksortD#2,quicksortD#1}, {splitD}, {quicksort}, {quicksortD}, {testQuicksort2}, {testQuicksort}
Previous analysis results are:

(93) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(94) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {split}, {quicksort#1,quicksort#2}, {quicksortD#2,quicksortD#1}, {splitD}, {quicksort}, {quicksortD}, {testQuicksort2}, {testQuicksort}
Previous analysis results are:

(95) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: split
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z'

(96) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {split}, {quicksort#1,quicksort#2}, {quicksortD#2,quicksortD#1}, {splitD}, {quicksort}, {quicksortD}, {testQuicksort2}, {testQuicksort}
Previous analysis results are:

(97) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: split
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 2 + 5·z'

(98) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {quicksort#1,quicksort#2}, {quicksortD#2,quicksortD#1}, {splitD}, {quicksort}, {quicksortD}, {testQuicksort2}, {testQuicksort}
Previous analysis results are:

(99) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(100) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {quicksort#1,quicksort#2}, {quicksortD#2,quicksortD#1}, {splitD}, {quicksort}, {quicksortD}, {testQuicksort2}, {testQuicksort}
Previous analysis results are:

(101) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: quicksort#1
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z

Computed SIZE bound using CoFloCo for: quicksort#2
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z + z'

(102) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {quicksort#1,quicksort#2}, {quicksortD#2,quicksortD#1}, {splitD}, {quicksort}, {quicksortD}, {testQuicksort2}, {testQuicksort}
Previous analysis results are:

(103) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: quicksort#1
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 5 + 38·z + 35·z²

Computed RUNTIME bound using KoAT for: quicksort#2
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 15 + 78·z + 70·z²

(104) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {quicksortD#2,quicksortD#1}, {splitD}, {quicksort}, {quicksortD}, {testQuicksort2}, {testQuicksort}
Previous analysis results are:

(105) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(106) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {quicksortD#2,quicksortD#1}, {splitD}, {quicksort}, {quicksortD}, {testQuicksort2}, {testQuicksort}
Previous analysis results are:

(107) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: quicksortD#2
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + 3·z + 3·z'

Computed SIZE bound using CoFloCo for: quicksortD#1
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + 3·z

(108) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {quicksortD#2,quicksortD#1}, {splitD}, {quicksort}, {quicksortD}, {testQuicksort2}, {testQuicksort}
Previous analysis results are:

appendD: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
appendD#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
split#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
splitD#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
#compare: runtime: O(1) [0], size: O(1) [3]
#ckgt: runtime: O(1) [0], size: O(1) [2]
append#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
append: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
#abs: runtime: O(1) [1], size: O(n¹) [1 + z]
split#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
splitD#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
#greater: runtime: O(1) [1], size: O(1) [2]
testList: runtime: O(1) [11], size: O(1) [74]
split#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
splitD#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
split: runtime: O(n¹) [2 + 5·z'], size: O(n¹) [1 + z']
quicksort#1: runtime: O(n²) [5 + 38·z + 35·z²], size: O(n¹) [z]
quicksort#2: runtime: O(n²) [15 + 78·z + 70·z²], size: O(n¹) [z + z']
quicksortD#2: runtime: ?, size: O(n¹) [1 + 3·z + 3·z']
quicksortD#1: runtime: ?, size: O(n¹) [1 + 3·z]

(109) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: quicksortD#2
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 11 + 55·z + 44·z²

Computed RUNTIME bound using KoAT for: quicksortD#1
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 114 + 148·z + 44·z²

(110) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {splitD}, {quicksort}, {quicksortD}, {testQuicksort2}, {testQuicksort}
Previous analysis results are:

appendD: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
appendD#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
split#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
splitD#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
#compare: runtime: O(1) [0], size: O(1) [3]
#ckgt: runtime: O(1) [0], size: O(1) [2]
append#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
append: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
#abs: runtime: O(1) [1], size: O(n¹) [1 + z]
split#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
splitD#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
#greater: runtime: O(1) [1], size: O(1) [2]
testList: runtime: O(1) [11], size: O(1) [74]
split#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
splitD#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
split: runtime: O(n¹) [2 + 5·z'], size: O(n¹) [1 + z']
quicksort#1: runtime: O(n²) [5 + 38·z + 35·z²], size: O(n¹) [z]
quicksort#2: runtime: O(n²) [15 + 78·z + 70·z²], size: O(n¹) [z + z']
quicksortD#2: runtime: O(n²) [11 + 55·z + 44·z²], size: O(n¹) [1 + 3·z + 3·z']
quicksortD#1: runtime: O(n²) [114 + 148·z + 44·z²], size: O(n¹) [1 + 3·z]

(111) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(112) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {splitD}, {quicksort}, {quicksortD}, {testQuicksort2}, {testQuicksort}
Previous analysis results are:

appendD: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
appendD#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
split#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
splitD#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
#compare: runtime: O(1) [0], size: O(1) [3]
#ckgt: runtime: O(1) [0], size: O(1) [2]
append#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
append: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
#abs: runtime: O(1) [1], size: O(n¹) [1 + z]
split#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
splitD#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
#greater: runtime: O(1) [1], size: O(1) [2]
testList: runtime: O(1) [11], size: O(1) [74]
split#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
splitD#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
split: runtime: O(n¹) [2 + 5·z'], size: O(n¹) [1 + z']
quicksort#1: runtime: O(n²) [5 + 38·z + 35·z²], size: O(n¹) [z]
quicksort#2: runtime: O(n²) [15 + 78·z + 70·z²], size: O(n¹) [z + z']
quicksortD#2: runtime: O(n²) [11 + 55·z + 44·z²], size: O(n¹) [1 + 3·z + 3·z']
quicksortD#1: runtime: O(n²) [114 + 148·z + 44·z²], size: O(n¹) [1 + 3·z]

(113) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: splitD
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z'

(114) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {splitD}, {quicksort}, {quicksortD}, {testQuicksort2}, {testQuicksort}
Previous analysis results are:

appendD: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
appendD#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
split#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
splitD#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
#compare: runtime: O(1) [0], size: O(1) [3]
#ckgt: runtime: O(1) [0], size: O(1) [2]
append#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
append: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
#abs: runtime: O(1) [1], size: O(n¹) [1 + z]
split#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
splitD#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
#greater: runtime: O(1) [1], size: O(1) [2]
testList: runtime: O(1) [11], size: O(1) [74]
split#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
splitD#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
split: runtime: O(n¹) [2 + 5·z'], size: O(n¹) [1 + z']
quicksort#1: runtime: O(n²) [5 + 38·z + 35·z²], size: O(n¹) [z]
quicksort#2: runtime: O(n²) [15 + 78·z + 70·z²], size: O(n¹) [z + z']
quicksortD#2: runtime: O(n²) [11 + 55·z + 44·z²], size: O(n¹) [1 + 3·z + 3·z']
quicksortD#1: runtime: O(n²) [114 + 148·z + 44·z²], size: O(n¹) [1 + 3·z]
splitD: runtime: ?, size: O(n¹) [1 + z']

(115) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: splitD
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 2 + 5·z'

(116) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {quicksort}, {quicksortD}, {testQuicksort2}, {testQuicksort}
Previous analysis results are:

appendD: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
appendD#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
split#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
splitD#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
#compare: runtime: O(1) [0], size: O(1) [3]
#ckgt: runtime: O(1) [0], size: O(1) [2]
append#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
append: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
#abs: runtime: O(1) [1], size: O(n¹) [1 + z]
split#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
splitD#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
#greater: runtime: O(1) [1], size: O(1) [2]
testList: runtime: O(1) [11], size: O(1) [74]
split#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
splitD#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
split: runtime: O(n¹) [2 + 5·z'], size: O(n¹) [1 + z']
quicksort#1: runtime: O(n²) [5 + 38·z + 35·z²], size: O(n¹) [z]
quicksort#2: runtime: O(n²) [15 + 78·z + 70·z²], size: O(n¹) [z + z']
quicksortD#2: runtime: O(n²) [11 + 55·z + 44·z²], size: O(n¹) [1 + 3·z + 3·z']
quicksortD#1: runtime: O(n²) [114 + 148·z + 44·z²], size: O(n¹) [1 + 3·z]
splitD: runtime: O(n¹) [2 + 5·z'], size: O(n¹) [1 + z']

(117) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(118) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {quicksort}, {quicksortD}, {testQuicksort2}, {testQuicksort}
Previous analysis results are:

appendD: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
appendD#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
split#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
splitD#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
#compare: runtime: O(1) [0], size: O(1) [3]
#ckgt: runtime: O(1) [0], size: O(1) [2]
append#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
append: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
#abs: runtime: O(1) [1], size: O(n¹) [1 + z]
split#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
splitD#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
#greater: runtime: O(1) [1], size: O(1) [2]
testList: runtime: O(1) [11], size: O(1) [74]
split#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
splitD#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
split: runtime: O(n¹) [2 + 5·z'], size: O(n¹) [1 + z']
quicksort#1: runtime: O(n²) [5 + 38·z + 35·z²], size: O(n¹) [z]
quicksort#2: runtime: O(n²) [15 + 78·z + 70·z²], size: O(n¹) [z + z']
quicksortD#2: runtime: O(n²) [11 + 55·z + 44·z²], size: O(n¹) [1 + 3·z + 3·z']
quicksortD#1: runtime: O(n²) [114 + 148·z + 44·z²], size: O(n¹) [1 + 3·z]
splitD: runtime: O(n¹) [2 + 5·z'], size: O(n¹) [1 + z']

(119) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: quicksort
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z

(120) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {quicksort}, {quicksortD}, {testQuicksort2}, {testQuicksort}
Previous analysis results are:

appendD: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
appendD#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
split#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
splitD#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
#compare: runtime: O(1) [0], size: O(1) [3]
#ckgt: runtime: O(1) [0], size: O(1) [2]
append#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
append: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
#abs: runtime: O(1) [1], size: O(n¹) [1 + z]
split#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
splitD#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
#greater: runtime: O(1) [1], size: O(1) [2]
testList: runtime: O(1) [11], size: O(1) [74]
split#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
splitD#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
split: runtime: O(n¹) [2 + 5·z'], size: O(n¹) [1 + z']
quicksort#1: runtime: O(n²) [5 + 38·z + 35·z²], size: O(n¹) [z]
quicksort#2: runtime: O(n²) [15 + 78·z + 70·z²], size: O(n¹) [z + z']
quicksortD#2: runtime: O(n²) [11 + 55·z + 44·z²], size: O(n¹) [1 + 3·z + 3·z']
quicksortD#1: runtime: O(n²) [114 + 148·z + 44·z²], size: O(n¹) [1 + 3·z]
splitD: runtime: O(n¹) [2 + 5·z'], size: O(n¹) [1 + z']
quicksort: runtime: ?, size: O(n¹) [z]

(121) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: quicksort
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 6 + 38·z + 35·z²

(122) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {quicksortD}, {testQuicksort2}, {testQuicksort}
Previous analysis results are:

appendD: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
appendD#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
split#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
splitD#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
#compare: runtime: O(1) [0], size: O(1) [3]
#ckgt: runtime: O(1) [0], size: O(1) [2]
append#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
append: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
#abs: runtime: O(1) [1], size: O(n¹) [1 + z]
split#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
splitD#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
#greater: runtime: O(1) [1], size: O(1) [2]
testList: runtime: O(1) [11], size: O(1) [74]
split#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
splitD#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
split: runtime: O(n¹) [2 + 5·z'], size: O(n¹) [1 + z']
quicksort#1: runtime: O(n²) [5 + 38·z + 35·z²], size: O(n¹) [z]
quicksort#2: runtime: O(n²) [15 + 78·z + 70·z²], size: O(n¹) [z + z']
quicksortD#2: runtime: O(n²) [11 + 55·z + 44·z²], size: O(n¹) [1 + 3·z + 3·z']
quicksortD#1: runtime: O(n²) [114 + 148·z + 44·z²], size: O(n¹) [1 + 3·z]
splitD: runtime: O(n¹) [2 + 5·z'], size: O(n¹) [1 + z']
quicksort: runtime: O(n²) [6 + 38·z + 35·z²], size: O(n¹) [z]

(123) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(124) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {quicksortD}, {testQuicksort2}, {testQuicksort}
Previous analysis results are:

appendD: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
appendD#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
split#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
splitD#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
#compare: runtime: O(1) [0], size: O(1) [3]
#ckgt: runtime: O(1) [0], size: O(1) [2]
append#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
append: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
#abs: runtime: O(1) [1], size: O(n¹) [1 + z]
split#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
splitD#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
#greater: runtime: O(1) [1], size: O(1) [2]
testList: runtime: O(1) [11], size: O(1) [74]
split#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
splitD#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
split: runtime: O(n¹) [2 + 5·z'], size: O(n¹) [1 + z']
quicksort#1: runtime: O(n²) [5 + 38·z + 35·z²], size: O(n¹) [z]
quicksort#2: runtime: O(n²) [15 + 78·z + 70·z²], size: O(n¹) [z + z']
quicksortD#2: runtime: O(n²) [11 + 55·z + 44·z²], size: O(n¹) [1 + 3·z + 3·z']
quicksortD#1: runtime: O(n²) [114 + 148·z + 44·z²], size: O(n¹) [1 + 3·z]
splitD: runtime: O(n¹) [2 + 5·z'], size: O(n¹) [1 + z']
quicksort: runtime: O(n²) [6 + 38·z + 35·z²], size: O(n¹) [z]

(125) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: quicksortD
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + 3·z

(126) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {quicksortD}, {testQuicksort2}, {testQuicksort}
Previous analysis results are:

appendD: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
appendD#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
split#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
splitD#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
#compare: runtime: O(1) [0], size: O(1) [3]
#ckgt: runtime: O(1) [0], size: O(1) [2]
append#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
append: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
#abs: runtime: O(1) [1], size: O(n¹) [1 + z]
split#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
splitD#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
#greater: runtime: O(1) [1], size: O(1) [2]
testList: runtime: O(1) [11], size: O(1) [74]
split#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
splitD#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
split: runtime: O(n¹) [2 + 5·z'], size: O(n¹) [1 + z']
quicksort#1: runtime: O(n²) [5 + 38·z + 35·z²], size: O(n¹) [z]
quicksort#2: runtime: O(n²) [15 + 78·z + 70·z²], size: O(n¹) [z + z']
quicksortD#2: runtime: O(n²) [11 + 55·z + 44·z²], size: O(n¹) [1 + 3·z + 3·z']
quicksortD#1: runtime: O(n²) [114 + 148·z + 44·z²], size: O(n¹) [1 + 3·z]
splitD: runtime: O(n¹) [2 + 5·z'], size: O(n¹) [1 + z']
quicksort: runtime: O(n²) [6 + 38·z + 35·z²], size: O(n¹) [z]
quicksortD: runtime: ?, size: O(n¹) [1 + 3·z]

(127) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: quicksortD
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 115 + 148·z + 44·z²

(128) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {testQuicksort2}, {testQuicksort}
Previous analysis results are:

appendD: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
appendD#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
split#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
splitD#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
#compare: runtime: O(1) [0], size: O(1) [3]
#ckgt: runtime: O(1) [0], size: O(1) [2]
append#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
append: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
#abs: runtime: O(1) [1], size: O(n¹) [1 + z]
split#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
splitD#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
#greater: runtime: O(1) [1], size: O(1) [2]
testList: runtime: O(1) [11], size: O(1) [74]
split#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
splitD#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
split: runtime: O(n¹) [2 + 5·z'], size: O(n¹) [1 + z']
quicksort#1: runtime: O(n²) [5 + 38·z + 35·z²], size: O(n¹) [z]
quicksort#2: runtime: O(n²) [15 + 78·z + 70·z²], size: O(n¹) [z + z']
quicksortD#2: runtime: O(n²) [11 + 55·z + 44·z²], size: O(n¹) [1 + 3·z + 3·z']
quicksortD#1: runtime: O(n²) [114 + 148·z + 44·z²], size: O(n¹) [1 + 3·z]
splitD: runtime: O(n¹) [2 + 5·z'], size: O(n¹) [1 + z']
quicksort: runtime: O(n²) [6 + 38·z + 35·z²], size: O(n¹) [z]
quicksortD: runtime: O(n²) [115 + 148·z + 44·z²], size: O(n¹) [1 + 3·z]

(129) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(130) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {testQuicksort2}, {testQuicksort}
Previous analysis results are:

appendD: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
appendD#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
split#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
splitD#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
#compare: runtime: O(1) [0], size: O(1) [3]
#ckgt: runtime: O(1) [0], size: O(1) [2]
append#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
append: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
#abs: runtime: O(1) [1], size: O(n¹) [1 + z]
split#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
splitD#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
#greater: runtime: O(1) [1], size: O(1) [2]
testList: runtime: O(1) [11], size: O(1) [74]
split#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
splitD#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
split: runtime: O(n¹) [2 + 5·z'], size: O(n¹) [1 + z']
quicksort#1: runtime: O(n²) [5 + 38·z + 35·z²], size: O(n¹) [z]
quicksort#2: runtime: O(n²) [15 + 78·z + 70·z²], size: O(n¹) [z + z']
quicksortD#2: runtime: O(n²) [11 + 55·z + 44·z²], size: O(n¹) [1 + 3·z + 3·z']
quicksortD#1: runtime: O(n²) [114 + 148·z + 44·z²], size: O(n¹) [1 + 3·z]
splitD: runtime: O(n¹) [2 + 5·z'], size: O(n¹) [1 + z']
quicksort: runtime: O(n²) [6 + 38·z + 35·z²], size: O(n¹) [z]
quicksortD: runtime: O(n²) [115 + 148·z + 44·z²], size: O(n¹) [1 + 3·z]

(131) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: testQuicksort2
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 74

(132) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {testQuicksort2}, {testQuicksort}
Previous analysis results are:

appendD: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
appendD#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
split#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
splitD#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
#compare: runtime: O(1) [0], size: O(1) [3]
#ckgt: runtime: O(1) [0], size: O(1) [2]
append#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
append: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
#abs: runtime: O(1) [1], size: O(n¹) [1 + z]
split#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
splitD#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
#greater: runtime: O(1) [1], size: O(1) [2]
testList: runtime: O(1) [11], size: O(1) [74]
split#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
splitD#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
split: runtime: O(n¹) [2 + 5·z'], size: O(n¹) [1 + z']
quicksort#1: runtime: O(n²) [5 + 38·z + 35·z²], size: O(n¹) [z]
quicksort#2: runtime: O(n²) [15 + 78·z + 70·z²], size: O(n¹) [z + z']
quicksortD#2: runtime: O(n²) [11 + 55·z + 44·z²], size: O(n¹) [1 + 3·z + 3·z']
quicksortD#1: runtime: O(n²) [114 + 148·z + 44·z²], size: O(n¹) [1 + 3·z]
splitD: runtime: O(n¹) [2 + 5·z'], size: O(n¹) [1 + z']
quicksort: runtime: O(n²) [6 + 38·z + 35·z²], size: O(n¹) [z]
quicksortD: runtime: O(n²) [115 + 148·z + 44·z²], size: O(n¹) [1 + 3·z]
testQuicksort2: runtime: ?, size: O(1) [74]

(133) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: testQuicksort2
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 194490

(134) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {testQuicksort}
Previous analysis results are:

appendD: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
appendD#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
split#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
splitD#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
#compare: runtime: O(1) [0], size: O(1) [3]
#ckgt: runtime: O(1) [0], size: O(1) [2]
append#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
append: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
#abs: runtime: O(1) [1], size: O(n¹) [1 + z]
split#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
splitD#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
#greater: runtime: O(1) [1], size: O(1) [2]
testList: runtime: O(1) [11], size: O(1) [74]
split#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
splitD#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
split: runtime: O(n¹) [2 + 5·z'], size: O(n¹) [1 + z']
quicksort#1: runtime: O(n²) [5 + 38·z + 35·z²], size: O(n¹) [z]
quicksort#2: runtime: O(n²) [15 + 78·z + 70·z²], size: O(n¹) [z + z']
quicksortD#2: runtime: O(n²) [11 + 55·z + 44·z²], size: O(n¹) [1 + 3·z + 3·z']
quicksortD#1: runtime: O(n²) [114 + 148·z + 44·z²], size: O(n¹) [1 + 3·z]
splitD: runtime: O(n¹) [2 + 5·z'], size: O(n¹) [1 + z']
quicksort: runtime: O(n²) [6 + 38·z + 35·z²], size: O(n¹) [z]
quicksortD: runtime: O(n²) [115 + 148·z + 44·z²], size: O(n¹) [1 + 3·z]
testQuicksort2: runtime: O(1) [194490], size: O(1) [74]

(135) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(136) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {testQuicksort}
Previous analysis results are:

appendD: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
appendD#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
split#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
splitD#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
#compare: runtime: O(1) [0], size: O(1) [3]
#ckgt: runtime: O(1) [0], size: O(1) [2]
append#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
append: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
#abs: runtime: O(1) [1], size: O(n¹) [1 + z]
split#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
splitD#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
#greater: runtime: O(1) [1], size: O(1) [2]
testList: runtime: O(1) [11], size: O(1) [74]
split#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
splitD#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
split: runtime: O(n¹) [2 + 5·z'], size: O(n¹) [1 + z']
quicksort#1: runtime: O(n²) [5 + 38·z + 35·z²], size: O(n¹) [z]
quicksort#2: runtime: O(n²) [15 + 78·z + 70·z²], size: O(n¹) [z + z']
quicksortD#2: runtime: O(n²) [11 + 55·z + 44·z²], size: O(n¹) [1 + 3·z + 3·z']
quicksortD#1: runtime: O(n²) [114 + 148·z + 44·z²], size: O(n¹) [1 + 3·z]
splitD: runtime: O(n¹) [2 + 5·z'], size: O(n¹) [1 + z']
quicksort: runtime: O(n²) [6 + 38·z + 35·z²], size: O(n¹) [z]
quicksortD: runtime: O(n²) [115 + 148·z + 44·z²], size: O(n¹) [1 + 3·z]
testQuicksort2: runtime: O(1) [194490], size: O(1) [74]

(137) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: testQuicksort
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 74

(138) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {testQuicksort}
Previous analysis results are:

appendD: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
appendD#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
split#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
splitD#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
#compare: runtime: O(1) [0], size: O(1) [3]
#ckgt: runtime: O(1) [0], size: O(1) [2]
append#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
append: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
#abs: runtime: O(1) [1], size: O(n¹) [1 + z]
split#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
splitD#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
#greater: runtime: O(1) [1], size: O(1) [2]
testList: runtime: O(1) [11], size: O(1) [74]
split#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
splitD#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
split: runtime: O(n¹) [2 + 5·z'], size: O(n¹) [1 + z']
quicksort#1: runtime: O(n²) [5 + 38·z + 35·z²], size: O(n¹) [z]
quicksort#2: runtime: O(n²) [15 + 78·z + 70·z²], size: O(n¹) [z + z']
quicksortD#2: runtime: O(n²) [11 + 55·z + 44·z²], size: O(n¹) [1 + 3·z + 3·z']
quicksortD#1: runtime: O(n²) [114 + 148·z + 44·z²], size: O(n¹) [1 + 3·z]
splitD: runtime: O(n¹) [2 + 5·z'], size: O(n¹) [1 + z']
quicksort: runtime: O(n²) [6 + 38·z + 35·z²], size: O(n¹) [z]
quicksortD: runtime: O(n²) [115 + 148·z + 44·z²], size: O(n¹) [1 + 3·z]
testQuicksort2: runtime: O(1) [194490], size: O(1) [74]
testQuicksort: runtime: ?, size: O(1) [74]

(139) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: testQuicksort
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 194490

(140) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed:
Previous analysis results are:

appendD: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
appendD#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
split#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
splitD#3: runtime: O(1) [1], size: O(n¹) [2 + z' + z'' + z1]
#compare: runtime: O(1) [0], size: O(1) [3]
#ckgt: runtime: O(1) [0], size: O(1) [2]
append#1: runtime: O(n¹) [1 + 2·z], size: O(n¹) [z + z']
append: runtime: O(n¹) [2 + 2·z], size: O(n¹) [z + z']
#abs: runtime: O(1) [1], size: O(n¹) [1 + z]
split#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
splitD#2: runtime: O(1) [3], size: O(n¹) [1 + z + z'']
#greater: runtime: O(1) [1], size: O(1) [2]
testList: runtime: O(1) [11], size: O(1) [74]
split#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
splitD#1: runtime: O(n¹) [1 + 5·z], size: O(n¹) [1 + z]
split: runtime: O(n¹) [2 + 5·z'], size: O(n¹) [1 + z']
quicksort#1: runtime: O(n²) [5 + 38·z + 35·z²], size: O(n¹) [z]
quicksort#2: runtime: O(n²) [15 + 78·z + 70·z²], size: O(n¹) [z + z']
quicksortD#2: runtime: O(n²) [11 + 55·z + 44·z²], size: O(n¹) [1 + 3·z + 3·z']
quicksortD#1: runtime: O(n²) [114 + 148·z + 44·z²], size: O(n¹) [1 + 3·z]
splitD: runtime: O(n¹) [2 + 5·z'], size: O(n¹) [1 + z']
quicksort: runtime: O(n²) [6 + 38·z + 35·z²], size: O(n¹) [z]
quicksortD: runtime: O(n²) [115 + 148·z + 44·z²], size: O(n¹) [1 + 3·z]
testQuicksort2: runtime: O(1) [194490], size: O(1) [74]
testQuicksort: runtime: O(1) [194490], size: O(1) [74]

(141) FinalProof (EQUIVALENT transformation)

Computed overall runtime complexity