Runtime Complexity (innermost) proof of /tmp/tmpYjl9T9/insertionsort.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), 35 ms)

↳8 CpxTypedWeightedCompleteTrs

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

↳10 CpxRNTS

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

↳12 CpxRNTS

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

↳14 CpxRNTS

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

↳16 CpxRNTS

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

↳18 CpxRNTS

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

↳20 CpxRNTS

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

↳22 CpxRNTS

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

↳24 CpxRNTS

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

↳26 CpxRNTS

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

↳28 CpxRNTS

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

↳30 CpxRNTS

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

↳32 CpxRNTS

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

↳34 CpxRNTS

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

↳36 CpxRNTS

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

↳38 CpxRNTS

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

↳40 CpxRNTS

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

↳42 CpxRNTS

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

↳44 CpxRNTS

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

↳46 CpxRNTS

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

↳48 CpxRNTS

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

↳50 CpxRNTS

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

↳52 CpxRNTS

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

↳54 CpxRNTS

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

↳56 CpxRNTS

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

↳58 CpxRNTS

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

↳60 CpxRNTS

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

↳62 CpxRNTS

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

↳64 CpxRNTS

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

↳66 CpxRNTS

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

↳68 CpxRNTS

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

↳70 CpxRNTS

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

↳72 CpxRNTS

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

↳74 CpxRNTS

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

↳76 CpxRNTS

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

↳78 CpxRNTS

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

↳80 CpxRNTS

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

↳82 CpxRNTS

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

↳84 CpxRNTS

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

↳86 CpxRNTS

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

↳88 CpxRNTS

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

↳90 CpxRNTS

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

↳92 CpxRNTS

↳93 FinalProof (⇔, 0 ms)

↳94 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
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
#false :: #false:#true
#true :: #false:#true
insertD :: #0:#neg:#pos:#s → :::nil → :::nil
insertD#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insertD#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
insertionsort :: :::nil → :::nil
insertionsort#1 :: :::nil → :::nil
insertionsortD :: :::nil → :::nil
insertionsortD#1 :: :::nil → :::nil
testInsertionsort :: a → :::nil
testList :: #unit → :::nil
#unit :: #unit
testInsertionsortD :: 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
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true:null_#cklt
#cklt :: #EQ:#GT:#LT:null_#compare → #false:#true:null_#cklt
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT:null_#compare
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
insert#2 :: #false:#true:null_#cklt → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
#false :: #false:#true:null_#cklt
#true :: #false:#true:null_#cklt
insertD :: #0:#neg:#pos:#s → :::nil → :::nil
insertD#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insertD#2 :: #false:#true:null_#cklt → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
insertionsort :: :::nil → :::nil
insertionsort#1 :: :::nil → :::nil
insertionsortD :: :::nil → :::nil
insertionsortD#1 :: :::nil → :::nil
testInsertionsort :: a → :::nil
testList :: #unit → :::nil
#unit :: #unit
testInsertionsortD :: b → :::nil
#EQ :: #EQ:#GT:#LT:null_#compare
#GT :: #EQ:#GT:#LT:null_#compare
#LT :: #EQ:#GT:#LT:null_#compare
null_#cklt :: #false:#true:null_#cklt
null_#compare :: #EQ:#GT:#LT:null_#compare
const :: a
const1 :: 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
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true:null_#cklt
#cklt :: #EQ:#GT:#LT:null_#compare → #false:#true:null_#cklt
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT:null_#compare
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
insert#2 :: #false:#true:null_#cklt → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
#false :: #false:#true:null_#cklt
#true :: #false:#true:null_#cklt
insertD :: #0:#neg:#pos:#s → :::nil → :::nil
insertD#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insertD#2 :: #false:#true:null_#cklt → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
insertionsort :: :::nil → :::nil
insertionsort#1 :: :::nil → :::nil
insertionsortD :: :::nil → :::nil
insertionsortD#1 :: :::nil → :::nil
testInsertionsort :: a → :::nil
testList :: #unit → :::nil
#unit :: #unit
testInsertionsortD :: b → :::nil
#EQ :: #EQ:#GT:#LT:null_#compare
#GT :: #EQ:#GT:#LT:null_#compare
#LT :: #EQ:#GT:#LT:null_#compare
null_#cklt :: #false:#true:null_#cklt
null_#compare :: #EQ:#GT:#LT:null_#compare
const :: a
const1 :: 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:

{ #compare }
{ #cklt }
{ #abs }
{ #less }
{ insertD#2, insertD#1, insertD }
{ insert#2, insert, insert#1 }
{ testList }
{ insertionsortD#1 }
{ insertionsort#1 }
{ insertionsortD }
{ insertionsort }
{ testInsertionsortD }
{ testInsertionsort }

(16) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {#compare}, {#cklt}, {#abs}, {#less}, {insertD#2,insertD#1,insertD}, {insert#2,insert,insert#1}, {testList}, {insertionsortD#1}, {insertionsort#1}, {insertionsortD}, {insertionsort}, {testInsertionsortD}, {testInsertionsort}

(17) 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

(18) Obligation:

Complexity RNTS consisting of the following rules:

#compare: runtime: ?, size: O(1) [3]

(19) 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

(20) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {#cklt}, {#abs}, {#less}, {insertD#2,insertD#1,insertD}, {insert#2,insert,insert#1}, {testList}, {insertionsortD#1}, {insertionsort#1}, {insertionsortD}, {insertionsort}, {testInsertionsortD}, {testInsertionsort}
Previous analysis results are:

#compare: runtime: O(1) [0], size: O(1) [3]

(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:

#compare: runtime: O(1) [0], size: O(1) [3]

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

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

(24) Obligation:

Complexity RNTS consisting of the following rules:

#compare: runtime: O(1) [0], size: O(1) [3]
#cklt: runtime: ?, size: O(1) [2]

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

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

(26) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {#abs}, {#less}, {insertD#2,insertD#1,insertD}, {insert#2,insert,insert#1}, {testList}, {insertionsortD#1}, {insertionsort#1}, {insertionsortD}, {insertionsort}, {testInsertionsortD}, {testInsertionsort}
Previous analysis results are:

#compare: runtime: O(1) [0], size: O(1) [3]
#cklt: runtime: O(1) [0], size: O(1) [2]

(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:

#compare: runtime: O(1) [0], size: O(1) [3]
#cklt: runtime: O(1) [0], size: O(1) [2]

(29) 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

(30) Obligation:

Complexity RNTS consisting of the following rules:

#compare: runtime: O(1) [0], size: O(1) [3]
#cklt: runtime: O(1) [0], size: O(1) [2]
#abs: runtime: ?, size: O(n¹) [1 + z]

(31) 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

(32) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {#less}, {insertD#2,insertD#1,insertD}, {insert#2,insert,insert#1}, {testList}, {insertionsortD#1}, {insertionsort#1}, {insertionsortD}, {insertionsort}, {testInsertionsortD}, {testInsertionsort}
Previous analysis results are:

#compare: runtime: O(1) [0], size: O(1) [3]
#cklt: runtime: O(1) [0], size: O(1) [2]
#abs: runtime: O(1) [1], size: O(n¹) [1 + z]

(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:

#compare: runtime: O(1) [0], size: O(1) [3]
#cklt: runtime: O(1) [0], size: O(1) [2]
#abs: runtime: O(1) [1], size: O(n¹) [1 + z]

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

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

(36) Obligation:

Complexity RNTS consisting of the following rules:

#compare: runtime: O(1) [0], size: O(1) [3]
#cklt: runtime: O(1) [0], size: O(1) [2]
#abs: runtime: O(1) [1], size: O(n¹) [1 + z]
#less: runtime: ?, size: O(1) [2]

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

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

(38) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {insertD#2,insertD#1,insertD}, {insert#2,insert,insert#1}, {testList}, {insertionsortD#1}, {insertionsort#1}, {insertionsortD}, {insertionsort}, {testInsertionsortD}, {testInsertionsort}
Previous analysis results are:

#compare: runtime: O(1) [0], size: O(1) [3]
#cklt: runtime: O(1) [0], size: O(1) [2]
#abs: runtime: O(1) [1], size: O(n¹) [1 + z]
#less: runtime: O(1) [1], size: O(1) [2]

(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:

#compare: runtime: O(1) [0], size: O(1) [3]
#cklt: runtime: O(1) [0], size: O(1) [2]
#abs: runtime: O(1) [1], size: O(n¹) [1 + z]
#less: runtime: O(1) [1], size: O(1) [2]

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

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

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

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

(42) Obligation:

Complexity RNTS consisting of the following rules:

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

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

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

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

(44) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {insert#2,insert,insert#1}, {testList}, {insertionsortD#1}, {insertionsort#1}, {insertionsortD}, {insertionsort}, {testInsertionsortD}, {testInsertionsort}
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: insert#2
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 2 + z' + z'' + z1

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

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

(48) Obligation:

Complexity RNTS consisting of the following rules:

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

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

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

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

(50) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {testList}, {insertionsortD#1}, {insertionsort#1}, {insertionsortD}, {insertionsort}, {testInsertionsortD}, {testInsertionsort}
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:

Function symbols to be analyzed: {testList}, {insertionsortD#1}, {insertionsort#1}, {insertionsortD}, {insertionsort}, {testInsertionsortD}, {testInsertionsort}
Previous analysis results are:

(53) 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

(54) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {testList}, {insertionsortD#1}, {insertionsort#1}, {insertionsortD}, {insertionsort}, {testInsertionsortD}, {testInsertionsort}
Previous analysis results are:

(55) 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

(56) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {insertionsortD#1}, {insertionsort#1}, {insertionsortD}, {insertionsort}, {testInsertionsortD}, {testInsertionsort}
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:

Function symbols to be analyzed: {insertionsortD#1}, {insertionsort#1}, {insertionsortD}, {insertionsort}, {testInsertionsortD}, {testInsertionsort}
Previous analysis results are:

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

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

(60) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {insertionsortD#1}, {insertionsort#1}, {insertionsortD}, {insertionsort}, {testInsertionsortD}, {testInsertionsort}
Previous analysis results are:

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

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

(62) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {insertionsort#1}, {insertionsortD}, {insertionsort}, {testInsertionsortD}, {testInsertionsort}
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:

Function symbols to be analyzed: {insertionsort#1}, {insertionsortD}, {insertionsort}, {testInsertionsortD}, {testInsertionsort}
Previous analysis results are:

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

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

(66) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {insertionsort#1}, {insertionsortD}, {insertionsort}, {testInsertionsortD}, {testInsertionsort}
Previous analysis results are:

#compare: runtime: O(1) [0], size: O(1) [3]
#cklt: runtime: O(1) [0], size: O(1) [2]
#abs: runtime: O(1) [1], size: O(n¹) [1 + z]
#less: runtime: O(1) [1], size: O(1) [2]
insertD#2: runtime: O(n¹) [3 + 4·z1], size: O(n¹) [2 + z' + z'' + z1]
insertD#1: runtime: O(n¹) [1 + 4·z], size: O(n¹) [1 + z + z']
insertD: runtime: O(n¹) [2 + 4·z'], size: O(n¹) [1 + z + z']
insert#2: runtime: O(n¹) [3 + 4·z1], size: O(n¹) [2 + z' + z'' + z1]
insert: runtime: O(n¹) [2 + 4·z'], size: O(n¹) [1 + z + z']
insert#1: runtime: O(n¹) [1 + 4·z], size: O(n¹) [1 + z + z']
testList: runtime: O(1) [11], size: O(1) [74]
insertionsortD#1: runtime: O(n²) [1 + 4·z²], size: O(n¹) [z]
insertionsort#1: runtime: ?, size: O(n¹) [z]

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

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

(68) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {insertionsortD}, {insertionsort}, {testInsertionsortD}, {testInsertionsort}
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:

Function symbols to be analyzed: {insertionsortD}, {insertionsort}, {testInsertionsortD}, {testInsertionsort}
Previous analysis results are:

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

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

(72) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {insertionsortD}, {insertionsort}, {testInsertionsortD}, {testInsertionsort}
Previous analysis results are:

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

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

(74) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {insertionsort}, {testInsertionsortD}, {testInsertionsort}
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:

Function symbols to be analyzed: {insertionsort}, {testInsertionsortD}, {testInsertionsort}
Previous analysis results are:

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

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

(78) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {insertionsort}, {testInsertionsortD}, {testInsertionsort}
Previous analysis results are:

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

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

(80) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {testInsertionsortD}, {testInsertionsort}
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:

Function symbols to be analyzed: {testInsertionsortD}, {testInsertionsort}
Previous analysis results are:

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

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

(84) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {testInsertionsortD}, {testInsertionsort}
Previous analysis results are:

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

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

(86) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {testInsertionsort}
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:

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

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

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

(90) Obligation:

Complexity RNTS consisting of the following rules:

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

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

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

(92) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed:
Previous analysis results are:

(93) FinalProof (EQUIVALENT transformation)

Computed overall runtime complexity