Runtime Complexity (innermost) proof of /tmp/tmpd38nJ8/flatten.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), 10 ms)

↳8 CpxTypedWeightedCompleteTrs

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

↳10 CpxRNTS

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

↳12 CpxRNTS

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

↳14 CpxRNTS

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

↳16 CpxRNTS

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

↳18 CpxRNTS

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

↳20 CpxRNTS

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

↳22 CpxRNTS

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

↳24 CpxRNTS

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

↳26 CpxRNTS

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

↳28 CpxRNTS

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

↳30 CpxRNTS

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

↳32 CpxRNTS

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

↳34 CpxRNTS

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

↳36 CpxRNTS

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

↳38 CpxRNTS

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

↳40 CpxRNTS

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

↳42 CpxRNTS

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

↳44 CpxRNTS

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

↳46 CpxRNTS

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

↳48 CpxRNTS

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

↳50 CpxRNTS

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

↳52 CpxRNTS

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

↳54 CpxRNTS

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

↳56 CpxRNTS

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

↳58 CpxRNTS

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

↳60 CpxRNTS

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

↳62 CpxRNTS

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

↳64 CpxRNTS

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

↳66 CpxRNTS

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

↳68 CpxRNTS

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

↳70 CpxRNTS

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

↳72 CpxRNTS

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

↳74 CpxRNTS

↳75 FinalProof (⇔, 0 ms)

↳76 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:

#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
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
flatten :: leaf:node → :::nil
flatten#1 :: leaf:node → :::nil
leaf :: leaf:node
node :: :::nil → leaf:node → leaf:node → leaf:node
flattensort :: leaf:node → :::nil
insertionsort :: :::nil → :::nil
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insert#2 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
insertionsort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#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

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:

#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
append :: :::nil → :::nil → :::nil
append#1 :: :::nil → :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
nil :: :::nil
flatten :: leaf:node → :::nil
flatten#1 :: leaf:node → :::nil
leaf :: leaf:node
node :: :::nil → leaf:node → leaf:node → leaf:node
flattensort :: leaf:node → :::nil
insertionsort :: :::nil → :::nil
insert :: #0:#neg:#pos:#s → :::nil → :::nil
insert#1 :: :::nil → #0:#neg:#pos:#s → :::nil
insert#2 :: #false:#true:null_#cklt → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true:null_#cklt
#true :: #false:#true:null_#cklt
insertionsort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT:null_#compare
#GT :: #EQ:#GT:#LT:null_#compare
#LT :: #EQ:#GT:#LT:null_#compare
#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
null_#cklt :: #false:#true:null_#cklt
null_#compare :: #EQ:#GT:#LT:null_#compare

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:

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 }
{ append#1, append }
{ #cklt }
{ #less }
{ insert#2, insert, insert#1 }
{ flatten#1 }
{ insertionsort#1 }
{ flatten }
{ insertionsort }
{ flattensort }

(16) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {#compare}, {append#1,append}, {#cklt}, {#less}, {insert#2,insert,insert#1}, {flatten#1}, {insertionsort#1}, {flatten}, {insertionsort}, {flattensort}

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

Function symbols to be analyzed: {#compare}, {append#1,append}, {#cklt}, {#less}, {insert#2,insert,insert#1}, {flatten#1}, {insertionsort#1}, {flatten}, {insertionsort}, {flattensort}
Previous analysis results are:

#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: {append#1,append}, {#cklt}, {#less}, {insert#2,insert,insert#1}, {flatten#1}, {insertionsort#1}, {flatten}, {insertionsort}, {flattensort}
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: 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'

(24) Obligation:

Complexity RNTS consisting of the following rules:

#compare: runtime: O(1) [0], size: O(1) [3]
append#1: runtime: ?, size: O(n¹) [z + z']
append: runtime: ?, size: O(n¹) [z + z']

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

(26) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {#cklt}, {#less}, {insert#2,insert,insert#1}, {flatten#1}, {insertionsort#1}, {flatten}, {insertionsort}, {flattensort}
Previous analysis results are:

#compare: runtime: O(1) [0], size: O(1) [3]
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']

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

Function symbols to be analyzed: {#cklt}, {#less}, {insert#2,insert,insert#1}, {flatten#1}, {insertionsort#1}, {flatten}, {insertionsort}, {flattensort}
Previous analysis results are:

#compare: runtime: O(1) [0], size: O(1) [3]
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']

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

(30) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {#cklt}, {#less}, {insert#2,insert,insert#1}, {flatten#1}, {insertionsort#1}, {flatten}, {insertionsort}, {flattensort}
Previous analysis results are:

#compare: runtime: O(1) [0], size: O(1) [3]
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']
#cklt: runtime: ?, size: O(1) [2]

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

(32) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {#less}, {insert#2,insert,insert#1}, {flatten#1}, {insertionsort#1}, {flatten}, {insertionsort}, {flattensort}
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:

Function symbols to be analyzed: {#less}, {insert#2,insert,insert#1}, {flatten#1}, {insertionsort#1}, {flatten}, {insertionsort}, {flattensort}
Previous analysis results are:

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

Function symbols to be analyzed: {#less}, {insert#2,insert,insert#1}, {flatten#1}, {insertionsort#1}, {flatten}, {insertionsort}, {flattensort}
Previous analysis results are:

(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: {insert#2,insert,insert#1}, {flatten#1}, {insertionsort#1}, {flatten}, {insertionsort}, {flattensort}
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:

Function symbols to be analyzed: {insert#2,insert,insert#1}, {flatten#1}, {insertionsort#1}, {flatten}, {insertionsort}, {flattensort}
Previous analysis results are:

(41) 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'

(42) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {insert#2,insert,insert#1}, {flatten#1}, {insertionsort#1}, {flatten}, {insertionsort}, {flattensort}
Previous analysis results are:

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

(44) Obligation:

Complexity RNTS consisting of the following rules:

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

Function symbols to be analyzed: {flatten#1}, {insertionsort#1}, {flatten}, {insertionsort}, {flattensort}
Previous analysis results are:

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

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

(48) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {flatten#1}, {insertionsort#1}, {flatten}, {insertionsort}, {flattensort}
Previous analysis results are:

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

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

(50) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {insertionsort#1}, {flatten}, {insertionsort}, {flattensort}
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: {insertionsort#1}, {flatten}, {insertionsort}, {flattensort}
Previous analysis results are:

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

(54) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {insertionsort#1}, {flatten}, {insertionsort}, {flattensort}
Previous analysis results are:

#compare: runtime: O(1) [0], size: O(1) [3]
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']
#cklt: runtime: O(1) [0], size: O(1) [2]
#less: runtime: O(1) [1], size: O(1) [2]
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']
flatten#1: runtime: O(n²) [1 + 8·z + 2·z²], size: O(n¹) [1 + z]
insertionsort#1: runtime: ?, size: O(n¹) [z]

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

(56) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {flatten}, {insertionsort}, {flattensort}
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: {flatten}, {insertionsort}, {flattensort}
Previous analysis results are:

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

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

(60) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {flatten}, {insertionsort}, {flattensort}
Previous analysis results are:

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

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

(62) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {insertionsort}, {flattensort}
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}, {flattensort}
Previous analysis results are:

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

(66) Obligation:

Complexity RNTS consisting of the following rules:

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

(67) 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²

(68) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed: {flattensort}
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: {flattensort}
Previous analysis results are:

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

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

(72) Obligation:

Complexity RNTS consisting of the following rules:

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

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

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

(74) Obligation:

Complexity RNTS consisting of the following rules:

Function symbols to be analyzed:
Previous analysis results are:

(75) FinalProof (EQUIVALENT transformation)

Computed overall runtime complexity

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

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

(10) Obligation:

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

(12) Obligation:

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

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

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

(26) Obligation:

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

(28) Obligation:

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

(30) Obligation:

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

(32) Obligation:

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

(34) Obligation:

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

(36) Obligation:

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

(38) Obligation:

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

(40) Obligation:

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

(42) Obligation:

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

(44) Obligation:

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

(46) Obligation:

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

(48) Obligation:

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

(50) Obligation:

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

(52) Obligation:

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

(54) Obligation:

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

(56) Obligation:

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

(58) Obligation:

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

(60) Obligation:

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

(62) Obligation:

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

(64) Obligation:

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

(66) Obligation:

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

(68) Obligation:

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

(70) Obligation:

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

(72) Obligation:

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

(74) Obligation:

(75) FinalProof (EQUIVALENT transformation)

(76) BOUNDS(1, n^2)