WORST_CASE(Omega(n^2),O(n^2)) proof of /export/starexec/sandbox2/benchmark/theBenchmark.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^2, n^2). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 225 ms] (2) CpxRelTRS (3) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (4) CpxWeightedTrs (5) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CpxTypedWeightedTrs (7) CompletionProof [UPPER BOUND(ID), 0 ms] (8) CpxTypedWeightedCompleteTrs (9) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (10) CpxRNTS (11) CompleteCoflocoProof [FINISHED, 42.9 s] (12) BOUNDS(1, n^2) (13) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (14) CpxRelTRS (15) SlicingProof [LOWER BOUND(ID), 7 ms] (16) CpxRelTRS (17) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (18) typed CpxTrs (19) OrderProof [LOWER BOUND(ID), 0 ms] (20) typed CpxTrs (21) RewriteLemmaProof [LOWER BOUND(ID), 1856 ms] (22) typed CpxTrs (23) RewriteLemmaProof [LOWER BOUND(ID), 231 ms] (24) BEST (25) proven lower bound (26) LowerBoundPropagationProof [FINISHED, 0 ms] (27) BOUNDS(n^1, INF) (28) typed CpxTrs (29) RewriteLemmaProof [LOWER BOUND(ID), 176 ms] (30) typed CpxTrs (31) RewriteLemmaProof [LOWER BOUND(ID), 77 ms] (32) typed CpxTrs (33) RewriteLemmaProof [LOWER BOUND(ID), 83 ms] (34) BEST (35) proven lower bound (36) LowerBoundPropagationProof [FINISHED, 0 ms] (37) BOUNDS(n^2, INF) (38) typed CpxTrs (39) RewriteLemmaProof [LOWER BOUND(ID), 53 ms] (40) typed CpxTrs (41) RewriteLemmaProof [LOWER BOUND(ID), 98 ms] (42) typed CpxTrs ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^2, n^2). The TRS R consists of the following rules: #abs(#0) -> #0 #abs(#neg(@x)) -> #pos(@x) #abs(#pos(@x)) -> #pos(@x) #abs(#s(@x)) -> #pos(#s(@x)) #greater(@x, @y) -> #ckgt(#compare(@x, @y)) append(@l, @ys) -> append#1(@l, @ys) append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) append#1(nil, @ys) -> @ys appendD(@l, @ys) -> appendD#1(@l, @ys) appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) appendD#1(nil, @ys) -> @ys quicksort(@l) -> quicksort#1(@l) quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) quicksort#1(nil) -> nil quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) quicksortD(@l) -> quicksortD#1(@l) quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) quicksortD#1(nil) -> nil quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) split(@pivot, @l) -> split#1(@l, @pivot) split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) split#1(nil, @pivot) -> tuple#2(nil, nil) split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) split#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) split#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) splitD(@pivot, @l) -> splitD#1(@l, @pivot) splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) splitD#1(nil, @pivot) -> tuple#2(nil, nil) splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) splitD#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) splitD#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) testList(@x) -> ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)))))))))) testQuicksort(@x) -> quicksort(testList(#unit)) testQuicksort2(@x) -> quicksort(testList(#unit)) The (relative) TRS S consists of the following rules: #ckgt(#EQ) -> #false #ckgt(#GT) -> #true #ckgt(#LT) -> #false #compare(#0, #0) -> #EQ #compare(#0, #neg(@y)) -> #GT #compare(#0, #pos(@y)) -> #LT #compare(#0, #s(@y)) -> #LT #compare(#neg(@x), #0) -> #LT #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) #compare(#neg(@x), #pos(@y)) -> #LT #compare(#pos(@x), #0) -> #GT #compare(#pos(@x), #neg(@y)) -> #GT #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) #compare(#s(@x), #0) -> #GT #compare(#s(@x), #s(@y)) -> #compare(@x, @y) Rewrite Strategy: INNERMOST ---------------------------------------- (1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID)) proved innermost termination of relative rules ---------------------------------------- (2) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^2, n^2). The TRS R consists of the following rules: #abs(#0) -> #0 #abs(#neg(@x)) -> #pos(@x) #abs(#pos(@x)) -> #pos(@x) #abs(#s(@x)) -> #pos(#s(@x)) #greater(@x, @y) -> #ckgt(#compare(@x, @y)) append(@l, @ys) -> append#1(@l, @ys) append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) append#1(nil, @ys) -> @ys appendD(@l, @ys) -> appendD#1(@l, @ys) appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) appendD#1(nil, @ys) -> @ys quicksort(@l) -> quicksort#1(@l) quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) quicksort#1(nil) -> nil quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) quicksortD(@l) -> quicksortD#1(@l) quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) quicksortD#1(nil) -> nil quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) split(@pivot, @l) -> split#1(@l, @pivot) split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) split#1(nil, @pivot) -> tuple#2(nil, nil) split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) split#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) split#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) splitD(@pivot, @l) -> splitD#1(@l, @pivot) splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) splitD#1(nil, @pivot) -> tuple#2(nil, nil) splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) splitD#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) splitD#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) testList(@x) -> ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)))))))))) testQuicksort(@x) -> quicksort(testList(#unit)) testQuicksort2(@x) -> quicksort(testList(#unit)) The (relative) TRS S consists of the following rules: #ckgt(#EQ) -> #false #ckgt(#GT) -> #true #ckgt(#LT) -> #false #compare(#0, #0) -> #EQ #compare(#0, #neg(@y)) -> #GT #compare(#0, #pos(@y)) -> #LT #compare(#0, #s(@y)) -> #LT #compare(#neg(@x), #0) -> #LT #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) #compare(#neg(@x), #pos(@y)) -> #LT #compare(#pos(@x), #0) -> #GT #compare(#pos(@x), #neg(@y)) -> #GT #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) #compare(#s(@x), #0) -> #GT #compare(#s(@x), #s(@y)) -> #compare(@x, @y) Rewrite Strategy: INNERMOST ---------------------------------------- (3) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID)) Transformed relative TRS to weighted TRS ---------------------------------------- (4) 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: #abs(#0) -> #0 [1] #abs(#neg(@x)) -> #pos(@x) [1] #abs(#pos(@x)) -> #pos(@x) [1] #abs(#s(@x)) -> #pos(#s(@x)) [1] #greater(@x, @y) -> #ckgt(#compare(@x, @y)) [1] append(@l, @ys) -> append#1(@l, @ys) [1] append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) [1] append#1(nil, @ys) -> @ys [1] appendD(@l, @ys) -> appendD#1(@l, @ys) [1] appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) [1] appendD#1(nil, @ys) -> @ys [1] quicksort(@l) -> quicksort#1(@l) [1] quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) [1] quicksort#1(nil) -> nil [1] quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) [1] quicksortD(@l) -> quicksortD#1(@l) [1] quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) [1] quicksortD#1(nil) -> nil [1] quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) [1] split(@pivot, @l) -> split#1(@l, @pivot) [1] split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) [1] split#1(nil, @pivot) -> tuple#2(nil, nil) [1] split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) [1] split#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) [1] split#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) [1] splitD(@pivot, @l) -> splitD#1(@l, @pivot) [1] splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) [1] splitD#1(nil, @pivot) -> tuple#2(nil, nil) [1] splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) [1] splitD#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) [1] splitD#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) [1] testList(@x) -> ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)))))))))) [1] testQuicksort(@x) -> quicksort(testList(#unit)) [1] testQuicksort2(@x) -> quicksort(testList(#unit)) [1] #ckgt(#EQ) -> #false [0] #ckgt(#GT) -> #true [0] #ckgt(#LT) -> #false [0] #compare(#0, #0) -> #EQ [0] #compare(#0, #neg(@y)) -> #GT [0] #compare(#0, #pos(@y)) -> #LT [0] #compare(#0, #s(@y)) -> #LT [0] #compare(#neg(@x), #0) -> #LT [0] #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) [0] #compare(#neg(@x), #pos(@y)) -> #LT [0] #compare(#pos(@x), #0) -> #GT [0] #compare(#pos(@x), #neg(@y)) -> #GT [0] #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) [0] #compare(#s(@x), #0) -> #GT [0] #compare(#s(@x), #s(@y)) -> #compare(@x, @y) [0] Rewrite Strategy: INNERMOST ---------------------------------------- (5) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (6) Obligation: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: #abs(#0) -> #0 [1] #abs(#neg(@x)) -> #pos(@x) [1] #abs(#pos(@x)) -> #pos(@x) [1] #abs(#s(@x)) -> #pos(#s(@x)) [1] #greater(@x, @y) -> #ckgt(#compare(@x, @y)) [1] append(@l, @ys) -> append#1(@l, @ys) [1] append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) [1] append#1(nil, @ys) -> @ys [1] appendD(@l, @ys) -> appendD#1(@l, @ys) [1] appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) [1] appendD#1(nil, @ys) -> @ys [1] quicksort(@l) -> quicksort#1(@l) [1] quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) [1] quicksort#1(nil) -> nil [1] quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) [1] quicksortD(@l) -> quicksortD#1(@l) [1] quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) [1] quicksortD#1(nil) -> nil [1] quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) [1] split(@pivot, @l) -> split#1(@l, @pivot) [1] split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) [1] split#1(nil, @pivot) -> tuple#2(nil, nil) [1] split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) [1] split#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) [1] split#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) [1] splitD(@pivot, @l) -> splitD#1(@l, @pivot) [1] splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) [1] splitD#1(nil, @pivot) -> tuple#2(nil, nil) [1] splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) [1] splitD#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) [1] splitD#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) [1] testList(@x) -> ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)))))))))) [1] testQuicksort(@x) -> quicksort(testList(#unit)) [1] testQuicksort2(@x) -> quicksort(testList(#unit)) [1] #ckgt(#EQ) -> #false [0] #ckgt(#GT) -> #true [0] #ckgt(#LT) -> #false [0] #compare(#0, #0) -> #EQ [0] #compare(#0, #neg(@y)) -> #GT [0] #compare(#0, #pos(@y)) -> #LT [0] #compare(#0, #s(@y)) -> #LT [0] #compare(#neg(@x), #0) -> #LT [0] #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) [0] #compare(#neg(@x), #pos(@y)) -> #LT [0] #compare(#pos(@x), #0) -> #GT [0] #compare(#pos(@x), #neg(@y)) -> #GT [0] #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) [0] #compare(#s(@x), #0) -> #GT [0] #compare(#s(@x), #s(@y)) -> #compare(@x, @y) [0] 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 ---------------------------------------- (7) CompletionProof (UPPER BOUND(ID)) The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added: #ckgt(v0) -> null_#ckgt [0] #compare(v0, v1) -> null_#compare [0] quicksort#2(v0, v1) -> null_quicksort#2 [0] quicksortD#2(v0, v1) -> null_quicksortD#2 [0] split#2(v0, v1, v2) -> null_split#2 [0] split#3(v0, v1, v2, v3) -> null_split#3 [0] splitD#2(v0, v1, v2) -> null_splitD#2 [0] splitD#3(v0, v1, v2, v3) -> null_splitD#3 [0] append#1(v0, v1) -> null_append#1 [0] appendD#1(v0, v1) -> null_appendD#1 [0] quicksort#1(v0) -> null_quicksort#1 [0] quicksortD#1(v0) -> null_quicksortD#1 [0] split#1(v0, v1) -> null_split#1 [0] splitD#1(v0, v1) -> null_splitD#1 [0] And the following fresh constants: null_#ckgt, null_#compare, null_quicksort#2, null_quicksortD#2, null_split#2, null_split#3, null_splitD#2, null_splitD#3, null_append#1, null_appendD#1, null_quicksort#1, null_quicksortD#1, null_split#1, null_splitD#1, const, const1 ---------------------------------------- (8) Obligation: Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: #abs(#0) -> #0 [1] #abs(#neg(@x)) -> #pos(@x) [1] #abs(#pos(@x)) -> #pos(@x) [1] #abs(#s(@x)) -> #pos(#s(@x)) [1] #greater(@x, @y) -> #ckgt(#compare(@x, @y)) [1] append(@l, @ys) -> append#1(@l, @ys) [1] append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) [1] append#1(nil, @ys) -> @ys [1] appendD(@l, @ys) -> appendD#1(@l, @ys) [1] appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) [1] appendD#1(nil, @ys) -> @ys [1] quicksort(@l) -> quicksort#1(@l) [1] quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) [1] quicksort#1(nil) -> nil [1] quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) [1] quicksortD(@l) -> quicksortD#1(@l) [1] quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) [1] quicksortD#1(nil) -> nil [1] quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) [1] split(@pivot, @l) -> split#1(@l, @pivot) [1] split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) [1] split#1(nil, @pivot) -> tuple#2(nil, nil) [1] split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) [1] split#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) [1] split#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) [1] splitD(@pivot, @l) -> splitD#1(@l, @pivot) [1] splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) [1] splitD#1(nil, @pivot) -> tuple#2(nil, nil) [1] splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) [1] splitD#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) [1] splitD#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) [1] testList(@x) -> ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)))))))))) [1] testQuicksort(@x) -> quicksort(testList(#unit)) [1] testQuicksort2(@x) -> quicksort(testList(#unit)) [1] #ckgt(#EQ) -> #false [0] #ckgt(#GT) -> #true [0] #ckgt(#LT) -> #false [0] #compare(#0, #0) -> #EQ [0] #compare(#0, #neg(@y)) -> #GT [0] #compare(#0, #pos(@y)) -> #LT [0] #compare(#0, #s(@y)) -> #LT [0] #compare(#neg(@x), #0) -> #LT [0] #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) [0] #compare(#neg(@x), #pos(@y)) -> #LT [0] #compare(#pos(@x), #0) -> #GT [0] #compare(#pos(@x), #neg(@y)) -> #GT [0] #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) [0] #compare(#s(@x), #0) -> #GT [0] #compare(#s(@x), #s(@y)) -> #compare(@x, @y) [0] #ckgt(v0) -> null_#ckgt [0] #compare(v0, v1) -> null_#compare [0] quicksort#2(v0, v1) -> null_quicksort#2 [0] quicksortD#2(v0, v1) -> null_quicksortD#2 [0] split#2(v0, v1, v2) -> null_split#2 [0] split#3(v0, v1, v2, v3) -> null_split#3 [0] splitD#2(v0, v1, v2) -> null_splitD#2 [0] splitD#3(v0, v1, v2, v3) -> null_splitD#3 [0] append#1(v0, v1) -> null_append#1 [0] appendD#1(v0, v1) -> null_appendD#1 [0] quicksort#1(v0) -> null_quicksort#1 [0] quicksortD#1(v0) -> null_quicksortD#1 [0] split#1(v0, v1) -> null_split#1 [0] splitD#1(v0, v1) -> null_splitD#1 [0] 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:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 -> :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 -> :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 append#1 :: :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 -> :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 -> :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 :: :: #0:#neg:#pos:#s -> :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 -> :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 nil :: :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 appendD :: :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 -> :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 -> :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 appendD#1 :: :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 -> :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 -> :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 quicksort :: :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 -> :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 quicksort#1 :: :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 -> :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 quicksort#2 :: tuple#2:null_split#2:null_split#3:null_splitD#2:null_splitD#3:null_split#1:null_splitD#1 -> #0:#neg:#pos:#s -> :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 split :: #0:#neg:#pos:#s -> :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 -> tuple#2:null_split#2:null_split#3:null_splitD#2:null_splitD#3:null_split#1:null_splitD#1 tuple#2 :: :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 -> :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 -> tuple#2:null_split#2:null_split#3:null_splitD#2:null_splitD#3:null_split#1:null_splitD#1 quicksortD :: :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 -> :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 quicksortD#1 :: :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 -> :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 quicksortD#2 :: tuple#2:null_split#2:null_split#3:null_splitD#2:null_splitD#3:null_split#1:null_splitD#1 -> #0:#neg:#pos:#s -> :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 splitD :: #0:#neg:#pos:#s -> :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 -> tuple#2:null_split#2:null_split#3:null_splitD#2:null_splitD#3:null_split#1:null_splitD#1 split#1 :: :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 -> #0:#neg:#pos:#s -> tuple#2:null_split#2:null_split#3:null_splitD#2:null_splitD#3:null_split#1:null_splitD#1 split#2 :: tuple#2:null_split#2:null_split#3:null_splitD#2:null_splitD#3:null_split#1:null_splitD#1 -> #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> tuple#2:null_split#2:null_split#3:null_splitD#2:null_splitD#3:null_split#1:null_splitD#1 split#3 :: #false:#true:null_#ckgt -> :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 -> :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 -> #0:#neg:#pos:#s -> tuple#2:null_split#2:null_split#3:null_splitD#2:null_splitD#3:null_split#1:null_splitD#1 #false :: #false:#true:null_#ckgt #true :: #false:#true:null_#ckgt splitD#1 :: :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 -> #0:#neg:#pos:#s -> tuple#2:null_split#2:null_split#3:null_splitD#2:null_splitD#3:null_split#1:null_splitD#1 splitD#2 :: tuple#2:null_split#2:null_split#3:null_splitD#2:null_splitD#3:null_split#1:null_splitD#1 -> #0:#neg:#pos:#s -> #0:#neg:#pos:#s -> tuple#2:null_split#2:null_split#3:null_splitD#2:null_splitD#3:null_split#1:null_splitD#1 splitD#3 :: #false:#true:null_#ckgt -> :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 -> :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 -> #0:#neg:#pos:#s -> tuple#2:null_split#2:null_split#3:null_splitD#2:null_splitD#3:null_split#1:null_splitD#1 testList :: #unit -> :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 testQuicksort :: a -> :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 #unit :: #unit testQuicksort2 :: b -> :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 #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 null_quicksort#2 :: :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 null_quicksortD#2 :: :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 null_split#2 :: tuple#2:null_split#2:null_split#3:null_splitD#2:null_splitD#3:null_split#1:null_splitD#1 null_split#3 :: tuple#2:null_split#2:null_split#3:null_splitD#2:null_splitD#3:null_split#1:null_splitD#1 null_splitD#2 :: tuple#2:null_split#2:null_split#3:null_splitD#2:null_splitD#3:null_split#1:null_splitD#1 null_splitD#3 :: tuple#2:null_split#2:null_split#3:null_splitD#2:null_splitD#3:null_split#1:null_splitD#1 null_append#1 :: :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 null_appendD#1 :: :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 null_quicksort#1 :: :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 null_quicksortD#1 :: :::nil:null_quicksort#2:null_quicksortD#2:null_append#1:null_appendD#1:null_quicksort#1:null_quicksortD#1 null_split#1 :: tuple#2:null_split#2:null_split#3:null_splitD#2:null_splitD#3:null_split#1:null_splitD#1 null_splitD#1 :: tuple#2:null_split#2:null_split#3:null_splitD#2:null_splitD#3:null_split#1:null_splitD#1 const :: a const1 :: b Rewrite Strategy: INNERMOST ---------------------------------------- (9) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: #0 => 0 nil => 0 #false => 1 #true => 2 #unit => 0 #EQ => 1 #GT => 2 #LT => 3 null_#ckgt => 0 null_#compare => 0 null_quicksort#2 => 0 null_quicksortD#2 => 0 null_split#2 => 0 null_split#3 => 0 null_splitD#2 => 0 null_splitD#3 => 0 null_append#1 => 0 null_appendD#1 => 0 null_quicksort#1 => 0 null_quicksortD#1 => 0 null_split#1 => 0 null_splitD#1 => 0 const => 0 const1 => 0 ---------------------------------------- (10) Obligation: Complexity RNTS consisting of the following rules: #abs(z) -{ 1 }-> 0 :|: z = 0 #abs(z) -{ 1 }-> 1 + @x :|: @x >= 0, z = 1 + @x #abs(z) -{ 1 }-> 1 + (1 + @x) :|: @x >= 0, z = 1 + @x #ckgt(z) -{ 0 }-> 2 :|: z = 2 #ckgt(z) -{ 0 }-> 1 :|: z = 1 #ckgt(z) -{ 0 }-> 1 :|: z = 3 #ckgt(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 #compare(z, z') -{ 0 }-> 3 :|: z = 0, z' = 1 + @y, @y >= 0 #compare(z, z') -{ 0 }-> 3 :|: @x >= 0, z = 1 + @x, z' = 0 #compare(z, z') -{ 0 }-> 3 :|: @x >= 0, z = 1 + @x, z' = 1 + @y, @y >= 0 #compare(z, z') -{ 0 }-> 2 :|: z = 0, z' = 1 + @y, @y >= 0 #compare(z, z') -{ 0 }-> 2 :|: @x >= 0, z = 1 + @x, z' = 0 #compare(z, z') -{ 0 }-> 2 :|: @x >= 0, z = 1 + @x, z' = 1 + @y, @y >= 0 #compare(z, z') -{ 0 }-> 1 :|: z = 0, z' = 0 #compare(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 #compare(z, z') -{ 0 }-> #compare(@x, @y) :|: @x >= 0, z = 1 + @x, z' = 1 + @y, @y >= 0 #compare(z, z') -{ 0 }-> #compare(@y, @x) :|: @x >= 0, z = 1 + @x, z' = 1 + @y, @y >= 0 #greater(z, z') -{ 1 }-> #ckgt(#compare(@x, @y)) :|: z = @x, @x >= 0, z' = @y, @y >= 0 append(z, z') -{ 1 }-> append#1(@l, @ys) :|: z = @l, @l >= 0, z' = @ys, @ys >= 0 append#1(z, z') -{ 1 }-> @ys :|: z' = @ys, z = 0, @ys >= 0 append#1(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 append#1(z, z') -{ 1 }-> 1 + @x + append(@xs, @ys) :|: z' = @ys, @x >= 0, z = 1 + @x + @xs, @xs >= 0, @ys >= 0 appendD(z, z') -{ 1 }-> appendD#1(@l, @ys) :|: z = @l, @l >= 0, z' = @ys, @ys >= 0 appendD#1(z, z') -{ 1 }-> @ys :|: z' = @ys, z = 0, @ys >= 0 appendD#1(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 appendD#1(z, z') -{ 1 }-> 1 + @x + appendD(@xs, @ys) :|: z' = @ys, @x >= 0, z = 1 + @x + @xs, @xs >= 0, @ys >= 0 quicksort(z) -{ 1 }-> quicksort#1(@l) :|: z = @l, @l >= 0 quicksort#1(z) -{ 1 }-> quicksort#2(split(@z, @zs), @z) :|: z = 1 + @z + @zs, @zs >= 0, @z >= 0 quicksort#1(z) -{ 1 }-> 0 :|: z = 0 quicksort#1(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 quicksort#2(z, z') -{ 1 }-> append(quicksort(@xs), 1 + @z + quicksort(@ys)) :|: z' = @z, z = 1 + @xs + @ys, @xs >= 0, @ys >= 0, @z >= 0 quicksort#2(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 quicksortD(z) -{ 1 }-> quicksortD#1(@l) :|: z = @l, @l >= 0 quicksortD#1(z) -{ 1 }-> quicksortD#2(splitD(@z, @zs), @z) :|: z = 1 + @z + @zs, @zs >= 0, @z >= 0 quicksortD#1(z) -{ 1 }-> 0 :|: z = 0 quicksortD#1(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 quicksortD#2(z, z') -{ 1 }-> appendD(quicksortD(@xs), 1 + @z + quicksortD(@ys)) :|: z' = @z, z = 1 + @xs + @ys, @xs >= 0, @ys >= 0, @z >= 0 quicksortD#2(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 split(z, z') -{ 1 }-> split#1(@l, @pivot) :|: @l >= 0, z = @pivot, z' = @l, @pivot >= 0 split#1(z, z') -{ 1 }-> split#2(split(@pivot, @xs), @pivot, @x) :|: @x >= 0, z = 1 + @x + @xs, z' = @pivot, @xs >= 0, @pivot >= 0 split#1(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 split#1(z, z') -{ 1 }-> 1 + 0 + 0 :|: z' = @pivot, @pivot >= 0, z = 0 split#2(z, z', z'') -{ 1 }-> split#3(#greater(@x, @pivot), @ls, @rs, @x) :|: @ls >= 0, z = 1 + @ls + @rs, @x >= 0, z' = @pivot, @pivot >= 0, z'' = @x, @rs >= 0 split#2(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0 split#3(z, z', z'', z1) -{ 0 }-> 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0 split#3(z, z', z'', z1) -{ 1 }-> 1 + @ls + (1 + @x + @rs) :|: z = 2, z1 = @x, @ls >= 0, @x >= 0, z' = @ls, @rs >= 0, z'' = @rs split#3(z, z', z'', z1) -{ 1 }-> 1 + (1 + @x + @ls) + @rs :|: z1 = @x, @ls >= 0, @x >= 0, z = 1, z' = @ls, @rs >= 0, z'' = @rs splitD(z, z') -{ 1 }-> splitD#1(@l, @pivot) :|: @l >= 0, z = @pivot, z' = @l, @pivot >= 0 splitD#1(z, z') -{ 1 }-> splitD#2(splitD(@pivot, @xs), @pivot, @x) :|: @x >= 0, z = 1 + @x + @xs, z' = @pivot, @xs >= 0, @pivot >= 0 splitD#1(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 splitD#1(z, z') -{ 1 }-> 1 + 0 + 0 :|: z' = @pivot, @pivot >= 0, z = 0 splitD#2(z, z', z'') -{ 1 }-> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) :|: @ls >= 0, z = 1 + @ls + @rs, @x >= 0, z' = @pivot, @pivot >= 0, z'' = @x, @rs >= 0 splitD#2(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0 splitD#3(z, z', z'', z1) -{ 0 }-> 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0 splitD#3(z, z', z'', z1) -{ 1 }-> 1 + @ls + (1 + @x + @rs) :|: z = 2, z1 = @x, @ls >= 0, @x >= 0, z' = @ls, @rs >= 0, z'' = @rs splitD#3(z, z', z'', z1) -{ 1 }-> 1 + (1 + @x + @ls) + @rs :|: z1 = @x, @ls >= 0, @x >= 0, z = 1, z' = @ls, @rs >= 0, z'' = @rs testList(z) -{ 1 }-> 1 + #abs(0) + (1 + #abs(1 + (1 + (1 + (1 + (1 + 0))))) + (1 + #abs(1 + (1 + (1 + (1 + (1 + (1 + 0)))))) + (1 + #abs(1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + 0)))))))))) + (1 + #abs(1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + 0)))))))) + (1 + #abs(1 + (1 + 0)) + (1 + #abs(1 + (1 + (1 + 0))) + (1 + #abs(1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + 0))))))))) + (1 + #abs(1 + (1 + (1 + (1 + (1 + (1 + (1 + 0))))))) + (1 + #abs(1 + (1 + (1 + (1 + 0)))) + 0))))))))) :|: z = @x, @x >= 0 testQuicksort(z) -{ 1 }-> quicksort(testList(0)) :|: z = @x, @x >= 0 testQuicksort2(z) -{ 1 }-> quicksort(testList(0)) :|: z = @x, @x >= 0 Only complete derivations are relevant for the runtime complexity. ---------------------------------------- (11) CompleteCoflocoProof (FINISHED) Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo: eq(start(V, V3, V37, V44),0,[fun(V, Out)],[V >= 0]). eq(start(V, V3, V37, V44),0,[fun1(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V37, V44),0,[append(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V37, V44),0,[fun4(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V37, V44),0,[appendD(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V37, V44),0,[fun5(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V37, V44),0,[quicksort(V, Out)],[V >= 0]). eq(start(V, V3, V37, V44),0,[fun6(V, Out)],[V >= 0]). eq(start(V, V3, V37, V44),0,[fun7(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V37, V44),0,[quicksortD(V, Out)],[V >= 0]). eq(start(V, V3, V37, V44),0,[fun8(V, Out)],[V >= 0]). eq(start(V, V3, V37, V44),0,[fun9(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V37, V44),0,[split(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V37, V44),0,[fun10(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V37, V44),0,[fun11(V, V3, V37, Out)],[V >= 0,V3 >= 0,V37 >= 0]). eq(start(V, V3, V37, V44),0,[fun12(V, V3, V37, V44, Out)],[V >= 0,V3 >= 0,V37 >= 0,V44 >= 0]). eq(start(V, V3, V37, V44),0,[splitD(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V37, V44),0,[fun13(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V37, V44),0,[fun14(V, V3, V37, Out)],[V >= 0,V3 >= 0,V37 >= 0]). eq(start(V, V3, V37, V44),0,[fun15(V, V3, V37, V44, Out)],[V >= 0,V3 >= 0,V37 >= 0,V44 >= 0]). eq(start(V, V3, V37, V44),0,[testList(V, Out)],[V >= 0]). eq(start(V, V3, V37, V44),0,[testQuicksort(V, Out)],[V >= 0]). eq(start(V, V3, V37, V44),0,[testQuicksort2(V, Out)],[V >= 0]). eq(start(V, V3, V37, V44),0,[fun2(V, Out)],[V >= 0]). eq(start(V, V3, V37, V44),0,[fun3(V, V3, Out)],[V >= 0,V3 >= 0]). eq(fun(V, Out),1,[],[Out = 0,V = 0]). eq(fun(V, Out),1,[],[Out = 1 + V1,V1 >= 0,V = 1 + V1]). eq(fun(V, Out),1,[],[Out = 2 + V2,V2 >= 0,V = 1 + V2]). eq(fun1(V, V3, Out),1,[fun3(V4, V5, Ret0),fun2(Ret0, Ret)],[Out = Ret,V = V4,V4 >= 0,V3 = V5,V5 >= 0]). eq(append(V, V3, Out),1,[fun4(V6, V7, Ret1)],[Out = Ret1,V = V6,V6 >= 0,V3 = V7,V7 >= 0]). eq(fun4(V, V3, Out),1,[append(V9, V10, Ret11)],[Out = 1 + Ret11 + V8,V3 = V10,V8 >= 0,V = 1 + V8 + V9,V9 >= 0,V10 >= 0]). eq(fun4(V, V3, Out),1,[],[Out = V11,V3 = V11,V = 0,V11 >= 0]). eq(appendD(V, V3, Out),1,[fun5(V13, V12, Ret2)],[Out = Ret2,V = V13,V13 >= 0,V3 = V12,V12 >= 0]). eq(fun5(V, V3, Out),1,[appendD(V16, V15, Ret12)],[Out = 1 + Ret12 + V14,V3 = V15,V14 >= 0,V = 1 + V14 + V16,V16 >= 0,V15 >= 0]). eq(fun5(V, V3, Out),1,[],[Out = V17,V3 = V17,V = 0,V17 >= 0]). eq(quicksort(V, Out),1,[fun6(V18, Ret3)],[Out = Ret3,V = V18,V18 >= 0]). eq(fun6(V, Out),1,[split(V19, V20, Ret01),fun7(Ret01, V19, Ret4)],[Out = Ret4,V = 1 + V19 + V20,V20 >= 0,V19 >= 0]). eq(fun6(V, Out),1,[],[Out = 0,V = 0]). eq(fun7(V, V3, Out),1,[quicksort(V23, Ret02),quicksort(V21, Ret111),append(Ret02, 1 + V22 + Ret111, Ret5)],[Out = Ret5,V3 = V22,V = 1 + V21 + V23,V23 >= 0,V21 >= 0,V22 >= 0]). eq(quicksortD(V, Out),1,[fun8(V24, Ret6)],[Out = Ret6,V = V24,V24 >= 0]). eq(fun8(V, Out),1,[splitD(V25, V26, Ret03),fun9(Ret03, V25, Ret7)],[Out = Ret7,V = 1 + V25 + V26,V26 >= 0,V25 >= 0]). eq(fun8(V, Out),1,[],[Out = 0,V = 0]). eq(fun9(V, V3, Out),1,[quicksortD(V29, Ret04),quicksortD(V28, Ret112),appendD(Ret04, 1 + V27 + Ret112, Ret8)],[Out = Ret8,V3 = V27,V = 1 + V28 + V29,V29 >= 0,V28 >= 0,V27 >= 0]). eq(split(V, V3, Out),1,[fun10(V31, V30, Ret9)],[Out = Ret9,V31 >= 0,V = V30,V3 = V31,V30 >= 0]). eq(fun10(V, V3, Out),1,[split(V34, V32, Ret05),fun11(Ret05, V34, V33, Ret10)],[Out = Ret10,V33 >= 0,V = 1 + V32 + V33,V3 = V34,V32 >= 0,V34 >= 0]). eq(fun10(V, V3, Out),1,[],[Out = 1,V3 = V35,V35 >= 0,V = 0]). eq(fun11(V, V3, V37, Out),1,[fun1(V38, V39, Ret06),fun12(Ret06, V36, V40, V38, Ret13)],[Out = Ret13,V36 >= 0,V = 1 + V36 + V40,V38 >= 0,V3 = V39,V39 >= 0,V37 = V38,V40 >= 0]). eq(fun12(V, V3, V37, V44, Out),1,[],[Out = 2 + V41 + V42 + V43,V44 = V42,V41 >= 0,V42 >= 0,V = 1,V3 = V41,V43 >= 0,V37 = V43]). eq(fun12(V, V3, V37, V44, Out),1,[],[Out = 2 + V45 + V46 + V47,V = 2,V44 = V46,V45 >= 0,V46 >= 0,V3 = V45,V47 >= 0,V37 = V47]). eq(splitD(V, V3, Out),1,[fun13(V48, V49, Ret14)],[Out = Ret14,V48 >= 0,V = V49,V3 = V48,V49 >= 0]). eq(fun13(V, V3, Out),1,[splitD(V51, V50, Ret07),fun14(Ret07, V51, V52, Ret15)],[Out = Ret15,V52 >= 0,V = 1 + V50 + V52,V3 = V51,V50 >= 0,V51 >= 0]). eq(fun13(V, V3, Out),1,[],[Out = 1,V3 = V53,V53 >= 0,V = 0]). eq(fun14(V, V3, V37, Out),1,[fun1(V57, V54, Ret08),fun15(Ret08, V55, V56, V57, Ret16)],[Out = Ret16,V55 >= 0,V = 1 + V55 + V56,V57 >= 0,V3 = V54,V54 >= 0,V37 = V57,V56 >= 0]). eq(fun15(V, V3, V37, V44, Out),1,[],[Out = 2 + V58 + V59 + V60,V44 = V60,V58 >= 0,V60 >= 0,V = 1,V3 = V58,V59 >= 0,V37 = V59]). eq(fun15(V, V3, V37, V44, Out),1,[],[Out = 2 + V61 + V62 + V63,V = 2,V44 = V61,V62 >= 0,V61 >= 0,V3 = V62,V63 >= 0,V37 = V63]). eq(testList(V, Out),1,[fun(0, Ret011),fun(1 + (1 + (1 + (1 + (1 + 0)))), Ret101),fun(1 + (1 + (1 + (1 + (1 + (1 + 0))))), Ret1101),fun(1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + 0))))))))), Ret11101),fun(1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + 0))))))), Ret111101),fun(1 + (1 + 0), Ret1111101),fun(1 + (1 + (1 + 0)), Ret11111101),fun(1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + (1 + 0)))))))), Ret111111101),fun(1 + (1 + (1 + (1 + (1 + (1 + (1 + 0)))))), Ret1111111101),fun(1 + (1 + (1 + (1 + 0))), Ret11111111101)],[Out = 10 + Ret011 + Ret101 + Ret1101 + Ret11101 + Ret111101 + Ret1111101 + Ret11111101 + Ret111111101 + Ret1111111101 + Ret11111111101,V = V64,V64 >= 0]). eq(testQuicksort(V, Out),1,[testList(0, Ret09),quicksort(Ret09, Ret17)],[Out = Ret17,V = V65,V65 >= 0]). eq(testQuicksort2(V, Out),1,[testList(0, Ret010),quicksort(Ret010, Ret18)],[Out = Ret18,V = V66,V66 >= 0]). eq(fun2(V, Out),0,[],[Out = 1,V = 1]). eq(fun2(V, Out),0,[],[Out = 2,V = 2]). eq(fun2(V, Out),0,[],[Out = 1,V = 3]). eq(fun3(V, V3, Out),0,[],[Out = 1,V = 0,V3 = 0]). eq(fun3(V, V3, Out),0,[],[Out = 2,V = 0,V3 = 1 + V67,V67 >= 0]). eq(fun3(V, V3, Out),0,[],[Out = 3,V = 0,V3 = 1 + V68,V68 >= 0]). eq(fun3(V, V3, Out),0,[],[Out = 3,V69 >= 0,V = 1 + V69,V3 = 0]). eq(fun3(V, V3, Out),0,[fun3(V70, V71, Ret19)],[Out = Ret19,V71 >= 0,V = 1 + V71,V3 = 1 + V70,V70 >= 0]). eq(fun3(V, V3, Out),0,[],[Out = 3,V73 >= 0,V = 1 + V73,V3 = 1 + V72,V72 >= 0]). eq(fun3(V, V3, Out),0,[],[Out = 2,V74 >= 0,V = 1 + V74,V3 = 0]). eq(fun3(V, V3, Out),0,[],[Out = 2,V76 >= 0,V = 1 + V76,V3 = 1 + V75,V75 >= 0]). eq(fun3(V, V3, Out),0,[fun3(V78, V77, Ret20)],[Out = Ret20,V78 >= 0,V = 1 + V78,V3 = 1 + V77,V77 >= 0]). eq(fun2(V, Out),0,[],[Out = 0,V79 >= 0,V = V79]). eq(fun3(V, V3, Out),0,[],[Out = 0,V81 >= 0,V80 >= 0,V = V81,V3 = V80]). eq(fun7(V, V3, Out),0,[],[Out = 0,V83 >= 0,V82 >= 0,V = V83,V3 = V82]). eq(fun9(V, V3, Out),0,[],[Out = 0,V84 >= 0,V85 >= 0,V = V84,V3 = V85]). eq(fun11(V, V3, V37, Out),0,[],[Out = 0,V86 >= 0,V37 = V88,V87 >= 0,V = V86,V3 = V87,V88 >= 0]). eq(fun12(V, V3, V37, V44, Out),0,[],[Out = 0,V44 = V92,V90 >= 0,V37 = V91,V89 >= 0,V = V90,V3 = V89,V91 >= 0,V92 >= 0]). eq(fun14(V, V3, V37, Out),0,[],[Out = 0,V94 >= 0,V37 = V95,V93 >= 0,V = V94,V3 = V93,V95 >= 0]). eq(fun15(V, V3, V37, V44, Out),0,[],[Out = 0,V44 = V99,V96 >= 0,V37 = V98,V97 >= 0,V = V96,V3 = V97,V98 >= 0,V99 >= 0]). eq(fun4(V, V3, Out),0,[],[Out = 0,V100 >= 0,V101 >= 0,V = V100,V3 = V101]). eq(fun5(V, V3, Out),0,[],[Out = 0,V103 >= 0,V102 >= 0,V = V103,V3 = V102]). eq(fun6(V, Out),0,[],[Out = 0,V104 >= 0,V = V104]). eq(fun8(V, Out),0,[],[Out = 0,V105 >= 0,V = V105]). eq(fun10(V, V3, Out),0,[],[Out = 0,V107 >= 0,V106 >= 0,V = V107,V3 = V106]). eq(fun13(V, V3, Out),0,[],[Out = 0,V109 >= 0,V108 >= 0,V = V109,V3 = V108]). input_output_vars(fun(V,Out),[V],[Out]). input_output_vars(fun1(V,V3,Out),[V,V3],[Out]). input_output_vars(append(V,V3,Out),[V,V3],[Out]). input_output_vars(fun4(V,V3,Out),[V,V3],[Out]). input_output_vars(appendD(V,V3,Out),[V,V3],[Out]). input_output_vars(fun5(V,V3,Out),[V,V3],[Out]). input_output_vars(quicksort(V,Out),[V],[Out]). input_output_vars(fun6(V,Out),[V],[Out]). input_output_vars(fun7(V,V3,Out),[V,V3],[Out]). input_output_vars(quicksortD(V,Out),[V],[Out]). input_output_vars(fun8(V,Out),[V],[Out]). input_output_vars(fun9(V,V3,Out),[V,V3],[Out]). input_output_vars(split(V,V3,Out),[V,V3],[Out]). input_output_vars(fun10(V,V3,Out),[V,V3],[Out]). input_output_vars(fun11(V,V3,V37,Out),[V,V3,V37],[Out]). input_output_vars(fun12(V,V3,V37,V44,Out),[V,V3,V37,V44],[Out]). input_output_vars(splitD(V,V3,Out),[V,V3],[Out]). input_output_vars(fun13(V,V3,Out),[V,V3],[Out]). input_output_vars(fun14(V,V3,V37,Out),[V,V3,V37],[Out]). input_output_vars(fun15(V,V3,V37,V44,Out),[V,V3,V37,V44],[Out]). input_output_vars(testList(V,Out),[V],[Out]). input_output_vars(testQuicksort(V,Out),[V],[Out]). input_output_vars(testQuicksort2(V,Out),[V],[Out]). input_output_vars(fun2(V,Out),[V],[Out]). input_output_vars(fun3(V,V3,Out),[V,V3],[Out]). CoFloCo proof output: Preprocessing Cost Relations ===================================== #### Computed strongly connected components 0. recursive : [append/3,fun4/3] 1. recursive : [appendD/3,fun5/3] 2. non_recursive : [fun/2] 3. non_recursive : [fun2/2] 4. recursive : [fun3/3] 5. non_recursive : [fun1/3] 6. non_recursive : [fun12/5] 7. non_recursive : [fun11/4] 8. recursive [non_tail] : [fun10/3,split/3] 9. non_recursive : [fun15/5] 10. non_recursive : [fun14/4] 11. recursive [non_tail] : [fun13/3,splitD/3] 12. recursive [non_tail,multiple] : [fun6/2,fun7/3,quicksort/2] 13. recursive [non_tail,multiple] : [fun8/2,fun9/3,quicksortD/2] 14. non_recursive : [testList/2] 15. non_recursive : [testQuicksort/2] 16. non_recursive : [testQuicksort2/2] 17. non_recursive : [start/4] #### Obtained direct recursion through partial evaluation 0. SCC is partially evaluated into append/3 1. SCC is partially evaluated into appendD/3 2. SCC is partially evaluated into fun/2 3. SCC is partially evaluated into fun2/2 4. SCC is partially evaluated into fun3/3 5. SCC is partially evaluated into fun1/3 6. SCC is partially evaluated into fun12/5 7. SCC is partially evaluated into fun11/4 8. SCC is partially evaluated into split/3 9. SCC is partially evaluated into fun15/5 10. SCC is partially evaluated into fun14/4 11. SCC is partially evaluated into splitD/3 12. SCC is partially evaluated into quicksort/2 13. SCC is partially evaluated into quicksortD/2 14. SCC is partially evaluated into testList/2 15. SCC is partially evaluated into testQuicksort/2 16. SCC is partially evaluated into testQuicksort2/2 17. SCC is partially evaluated into start/4 Control-Flow Refinement of Cost Relations ===================================== ### Specialization of cost equations append/3 * CE 49 is refined into CE [81] * CE 47 is refined into CE [82] * CE 48 is refined into CE [83] ### Cost equations --> "Loop" of append/3 * CEs [82] --> Loop 49 * CEs [83] --> Loop 50 * CEs [81] --> Loop 51 ### Ranking functions of CR append(V,V3,Out) * RF of phase [51]: [V] #### Partial ranking functions of CR append(V,V3,Out) * Partial RF of phase [51]: - RF of loop [51:1]: V ### Specialization of cost equations appendD/3 * CE 39 is refined into CE [84] * CE 37 is refined into CE [85] * CE 38 is refined into CE [86] ### Cost equations --> "Loop" of appendD/3 * CEs [85] --> Loop 52 * CEs [86] --> Loop 53 * CEs [84] --> Loop 54 ### Ranking functions of CR appendD(V,V3,Out) * RF of phase [54]: [V] #### Partial ranking functions of CR appendD(V,V3,Out) * Partial RF of phase [54]: - RF of loop [54:1]: V ### Specialization of cost equations fun/2 * CE 55 is refined into CE [87] * CE 56 is refined into CE [88] * CE 54 is refined into CE [89] ### Cost equations --> "Loop" of fun/2 * CEs [87] --> Loop 55 * CEs [88] --> Loop 56 * CEs [89] --> Loop 57 ### Ranking functions of CR fun(V,Out) #### Partial ranking functions of CR fun(V,Out) ### Specialization of cost equations fun2/2 * CE 70 is refined into CE [90] * CE 69 is refined into CE [91] * CE 68 is refined into CE [92] * CE 67 is refined into CE [93] ### Cost equations --> "Loop" of fun2/2 * CEs [90] --> Loop 58 * CEs [91] --> Loop 59 * CEs [92] --> Loop 60 * CEs [93] --> Loop 61 ### Ranking functions of CR fun2(V,Out) #### Partial ranking functions of CR fun2(V,Out) ### Specialization of cost equations fun3/3 * CE 76 is refined into CE [94] * CE 78 is refined into CE [95] * CE 80 is refined into CE [96] * CE 74 is refined into CE [97] * CE 77 is refined into CE [98] * CE 73 is refined into CE [99] * CE 72 is refined into CE [100] * CE 71 is refined into CE [101] * CE 75 is refined into CE [102] * CE 79 is refined into CE [103] ### Cost equations --> "Loop" of fun3/3 * CEs [102] --> Loop 62 * CEs [103] --> Loop 63 * CEs [94] --> Loop 64 * CEs [95] --> Loop 65 * CEs [96] --> Loop 66 * CEs [97] --> Loop 67 * CEs [98] --> Loop 68 * CEs [99] --> Loop 69 * CEs [100] --> Loop 70 * CEs [101] --> Loop 71 ### Ranking functions of CR fun3(V,V3,Out) * RF of phase [62,63]: [V/2+V3/2-1/2] #### Partial ranking functions of CR fun3(V,V3,Out) * Partial RF of phase [62,63]: - RF of loop [62:1]: V/2+V3/2-1/2 - RF of loop [63:1]: V depends on loops [62:1] V3 depends on loops [62:1] ### Specialization of cost equations fun1/3 * CE 57 is refined into CE [104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120] ### Cost equations --> "Loop" of fun1/3 * CEs [117] --> Loop 72 * CEs [115,119] --> Loop 73 * CEs [116] --> Loop 74 * CEs [110] --> Loop 75 * CEs [112] --> Loop 76 * CEs [111,113] --> Loop 77 * CEs [106] --> Loop 78 * CEs [108] --> Loop 79 * CEs [107,109] --> Loop 80 * CEs [104] --> Loop 81 * CEs [105,114,118,120] --> Loop 82 ### Ranking functions of CR fun1(V,V3,Out) #### Partial ranking functions of CR fun1(V,V3,Out) ### Specialization of cost equations fun12/5 * CE 60 is refined into CE [121] * CE 59 is refined into CE [122] * CE 58 is refined into CE [123] ### Cost equations --> "Loop" of fun12/5 * CEs [121] --> Loop 83 * CEs [122] --> Loop 84 * CEs [123] --> Loop 85 ### Ranking functions of CR fun12(V,V3,V37,V44,Out) #### Partial ranking functions of CR fun12(V,V3,V37,V44,Out) ### Specialization of cost equations fun11/4 * CE 52 is refined into CE [124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140] * CE 53 is refined into CE [141] ### Cost equations --> "Loop" of fun11/4 * CEs [137,139] --> Loop 86 * CEs [136] --> Loop 87 * CEs [127,129] --> Loop 88 * CEs [128,130] --> Loop 89 * CEs [132,134] --> Loop 90 * CEs [131,133,135] --> Loop 91 * CEs [124] --> Loop 92 * CEs [125,126,138,140,141] --> Loop 93 ### Ranking functions of CR fun11(V,V3,V37,Out) #### Partial ranking functions of CR fun11(V,V3,V37,Out) ### Specialization of cost equations split/3 * CE 42 is refined into CE [142,143,144,145,146,147,148] * CE 40 is refined into CE [149] * CE 41 is refined into CE [150] ### Cost equations --> "Loop" of split/3 * CEs [149] --> Loop 94 * CEs [150] --> Loop 95 * CEs [148] --> Loop 96 * CEs [146] --> Loop 97 * CEs [147] --> Loop 98 * CEs [143,145] --> Loop 99 * CEs [144] --> Loop 100 * CEs [142] --> Loop 101 ### Ranking functions of CR split(V,V3,Out) * RF of phase [96,97]: [V3] * RF of phase [99]: [V3] * RF of phase [100,101]: [V3] #### Partial ranking functions of CR split(V,V3,Out) * Partial RF of phase [96,97]: - RF of loop [96:1]: V3/2-1/2 - RF of loop [97:1]: V3 * Partial RF of phase [99]: - RF of loop [99:1]: V3 * Partial RF of phase [100,101]: - RF of loop [100:1]: V3-1 - RF of loop [101:1]: V3 ### Specialization of cost equations fun15/5 * CE 63 is refined into CE [151] * CE 62 is refined into CE [152] * CE 61 is refined into CE [153] ### Cost equations --> "Loop" of fun15/5 * CEs [151] --> Loop 102 * CEs [152] --> Loop 103 * CEs [153] --> Loop 104 ### Ranking functions of CR fun15(V,V3,V37,V44,Out) #### Partial ranking functions of CR fun15(V,V3,V37,V44,Out) ### Specialization of cost equations fun14/4 * CE 50 is refined into CE [154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170] * CE 51 is refined into CE [171] ### Cost equations --> "Loop" of fun14/4 * CEs [167,169] --> Loop 105 * CEs [166] --> Loop 106 * CEs [157,159] --> Loop 107 * CEs [158,160] --> Loop 108 * CEs [162,164] --> Loop 109 * CEs [161,163,165] --> Loop 110 * CEs [154] --> Loop 111 * CEs [155,156,168,170,171] --> Loop 112 ### Ranking functions of CR fun14(V,V3,V37,Out) #### Partial ranking functions of CR fun14(V,V3,V37,Out) ### Specialization of cost equations splitD/3 * CE 32 is refined into CE [172,173,174,175,176,177,178] * CE 30 is refined into CE [179] * CE 31 is refined into CE [180] ### Cost equations --> "Loop" of splitD/3 * CEs [179] --> Loop 113 * CEs [180] --> Loop 114 * CEs [178] --> Loop 115 * CEs [176] --> Loop 116 * CEs [177] --> Loop 117 * CEs [173,175] --> Loop 118 * CEs [174] --> Loop 119 * CEs [172] --> Loop 120 ### Ranking functions of CR splitD(V,V3,Out) * RF of phase [115,116]: [V3] * RF of phase [118]: [V3] * RF of phase [119,120]: [V3] #### Partial ranking functions of CR splitD(V,V3,Out) * Partial RF of phase [115,116]: - RF of loop [115:1]: V3/2-1/2 - RF of loop [116:1]: V3 * Partial RF of phase [118]: - RF of loop [118:1]: V3 * Partial RF of phase [119,120]: - RF of loop [119:1]: V3-1 - RF of loop [120:1]: V3 ### Specialization of cost equations quicksort/2 * CE 43 is refined into CE [181] * CE 44 is refined into CE [182] * CE 46 is refined into CE [183,184,185,186,187] * CE 45 is refined into CE [188,189,190,191,192,193,194,195,196,197,198,199] ### Cost equations --> "Loop" of quicksort/2 * CEs [199] --> Loop 121 * CEs [198] --> Loop 122 * CEs [191] --> Loop 123 * CEs [190] --> Loop 124 * CEs [196] --> Loop 125 * CEs [188] --> Loop 126 * CEs [195] --> Loop 127 * CEs [194] --> Loop 128 * CEs [192] --> Loop 129 * CEs [197] --> Loop 130 * CEs [189] --> Loop 131 * CEs [193] --> Loop 132 * CEs [181,182,183,184,185,186,187] --> Loop 133 ### Ranking functions of CR quicksort(V,Out) * RF of phase [121,122,123,124,125,126,130,131]: [V-1] #### Partial ranking functions of CR quicksort(V,Out) * Partial RF of phase [121,122,123,124,125,126,130,131]: - RF of loop [121:1,121:2,122:1,122:2,125:1,125:2,130:1,130:2]: V/2-1 - RF of loop [123:1,123:2,124:1,124:2,126:1,126:2,131:1,131:2]: V-1 ### Specialization of cost equations quicksortD/2 * CE 33 is refined into CE [200] * CE 34 is refined into CE [201] * CE 36 is refined into CE [202,203,204,205,206] * CE 35 is refined into CE [207,208,209,210,211,212,213,214,215,216,217,218] ### Cost equations --> "Loop" of quicksortD/2 * CEs [218] --> Loop 134 * CEs [217] --> Loop 135 * CEs [210] --> Loop 136 * CEs [209] --> Loop 137 * CEs [215] --> Loop 138 * CEs [207] --> Loop 139 * CEs [214] --> Loop 140 * CEs [213] --> Loop 141 * CEs [211] --> Loop 142 * CEs [216] --> Loop 143 * CEs [208] --> Loop 144 * CEs [212] --> Loop 145 * CEs [200,201,202,203,204,205,206] --> Loop 146 ### Ranking functions of CR quicksortD(V,Out) * RF of phase [134,135,136,137,138,139,143,144]: [V-1] #### Partial ranking functions of CR quicksortD(V,Out) * Partial RF of phase [134,135,136,137,138,139,143,144]: - RF of loop [134:1,134:2,135:1,135:2,138:1,138:2,143:1,143:2]: V/2-1 - RF of loop [136:1,136:2,137:1,137:2,139:1,139:2,144:1,144:2]: V-1 ### Specialization of cost equations testList/2 * CE 64 is refined into CE [219,220,221,222,223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238,239,240,241,242,243,244,245,246,247,248,249,250,251,252,253,254,255,256,257,258,259,260,261,262,263,264,265,266,267,268,269,270,271,272,273,274,275,276,277,278,279,280,281,282,283,284,285,286,287,288,289,290,291,292,293,294,295,296,297,298,299,300,301,302,303,304,305,306,307,308,309,310,311,312,313,314,315,316,317,318,319,320,321,322,323,324,325,326,327,328,329,330,331,332,333,334,335,336,337,338,339,340,341,342,343,344,345,346,347,348,349,350,351,352,353,354,355,356,357,358,359,360,361,362,363,364,365,366,367,368,369,370,371,372,373,374,375,376,377,378,379,380,381,382,383,384,385,386,387,388,389,390,391,392,393,394,395,396,397,398,399,400,401,402,403,404,405,406,407,408,409,410,411,412,413,414,415,416,417,418,419,420,421,422,423,424,425,426,427,428,429,430,431,432,433,434,435,436,437,438,439,440,441,442,443,444,445,446,447,448,449,450,451,452,453,454,455,456,457,458,459,460,461,462,463,464,465,466,467,468,469,470,471,472,473,474,475,476,477,478,479,480,481,482,483,484,485,486,487,488,489,490,491,492,493,494,495,496,497,498,499,500,501,502,503,504,505,506,507,508,509,510,511,512,513,514,515,516,517,518,519,520,521,522,523,524,525,526,527,528,529,530,531,532,533,534,535,536,537,538,539,540,541,542,543,544,545,546,547,548,549,550,551,552,553,554,555,556,557,558,559,560,561,562,563,564,565,566,567,568,569,570,571,572,573,574,575,576,577,578,579,580,581,582,583,584,585,586,587,588,589,590,591,592,593,594,595,596,597,598,599,600,601,602,603,604,605,606,607,608,609,610,611,612,613,614,615,616,617,618,619,620,621,622,623,624,625,626,627,628,629,630,631,632,633,634,635,636,637,638,639,640,641,642,643,644,645,646,647,648,649,650,651,652,653,654,655,656,657,658,659,660,661,662,663,664,665,666,667,668,669,670,671,672,673,674,675,676,677,678,679,680,681,682,683,684,685,686,687,688,689,690,691,692,693,694,695,696,697,698,699,700,701,702,703,704,705,706,707,708,709,710,711,712,713,714,715,716,717,718,719,720,721,722,723,724,725,726,727,728,729,730] ### Cost equations --> "Loop" of testList/2 * CEs [219] --> Loop 147 * CEs [220,221,223,227,235,251,283,347,475] --> Loop 148 * CEs [222,224,225,228,229,231,236,237,239,243,252,253,255,259,267,284,285,287,291,299,315,348,349,351,355,363,379,411,476,477,479,483,491,507,539,603] --> Loop 149 * CEs [226,230,232,233,238,240,241,244,245,247,254,256,257,260,261,263,268,269,271,275,286,288,289,292,293,295,300,301,303,307,316,317,319,323,331,350,352,353,356,357,359,364,365,367,371,380,381,383,387,395,412,413,415,419,427,443,478,480,481,484,485,487,492,493,495,499,508,509,511,515,523,540,541,543,547,555,571,604,605,607,611,619,635,667] --> Loop 150 * CEs [234,242,246,248,249,258,262,264,265,270,272,273,276,277,279,290,294,296,297,302,304,305,308,309,311,318,320,321,324,325,327,332,333,335,339,354,358,360,361,366,368,369,372,373,375,382,384,385,388,389,391,396,397,399,403,414,416,417,420,421,423,428,429,431,435,444,445,447,451,459,482,486,488,489,494,496,497,500,501,503,510,512,513,516,517,519,524,525,527,531,542,544,545,548,549,551,556,557,559,563,572,573,575,579,587,606,608,609,612,613,615,620,621,623,627,636,637,639,643,651,668,669,671,675,683,699] --> Loop 151 * CEs [250,266,274,278,280,281,298,306,310,312,313,322,326,328,329,334,336,337,340,341,343,362,370,374,376,377,386,390,392,393,398,400,401,404,405,407,418,422,424,425,430,432,433,436,437,439,446,448,449,452,453,455,460,461,463,467,490,498,502,504,505,514,518,520,521,526,528,529,532,533,535,546,550,552,553,558,560,561,564,565,567,574,576,577,580,581,583,588,589,591,595,610,614,616,617,622,624,625,628,629,631,638,640,641,644,645,647,652,653,655,659,670,672,673,676,677,679,684,685,687,691,700,701,703,707,715] --> Loop 152 * CEs [282,314,330,338,342,344,345,378,394,402,406,408,409,426,434,438,440,441,450,454,456,457,462,464,465,468,469,471,506,522,530,534,536,537,554,562,566,568,569,578,582,584,585,590,592,593,596,597,599,618,626,630,632,633,642,646,648,649,654,656,657,660,661,663,674,678,680,681,686,688,689,692,693,695,702,704,705,708,709,711,716,717,719,723] --> Loop 153 * CEs [346,410,442,458,466,470,472,473,538,570,586,594,598,600,601,634,650,658,662,664,665,682,690,694,696,697,706,710,712,713,718,720,721,724,725,727] --> Loop 154 * CEs [474,602,666,698,714,722,726,728,729] --> Loop 155 * CEs [730] --> Loop 156 ### Ranking functions of CR testList(V,Out) #### Partial ranking functions of CR testList(V,Out) ### Specialization of cost equations testQuicksort/2 * CE 65 is refined into CE [731,732,733,734,735,736,737,738,739,740,741,742,743,744,745,746,747,748,749,750,751,752,753,754,755,756,757,758,759,760] ### Cost equations --> "Loop" of testQuicksort/2 * CEs [759] --> Loop 157 * CEs [756] --> Loop 158 * CEs [753] --> Loop 159 * CEs [750] --> Loop 160 * CEs [747] --> Loop 161 * CEs [744] --> Loop 162 * CEs [741] --> Loop 163 * CEs [738] --> Loop 164 * CEs [735] --> Loop 165 * CEs [732] --> Loop 166 * CEs [731,733,734,736,737,739,740,742,743,745,746,748,749,751,752,754,755,757,758,760] --> Loop 167 ### Ranking functions of CR testQuicksort(V,Out) #### Partial ranking functions of CR testQuicksort(V,Out) ### Specialization of cost equations testQuicksort2/2 * CE 66 is refined into CE [761,762,763,764,765,766,767,768,769,770,771,772,773,774,775,776,777,778,779,780,781,782,783,784,785,786,787,788,789,790] ### Cost equations --> "Loop" of testQuicksort2/2 * CEs [789] --> Loop 168 * CEs [786] --> Loop 169 * CEs [783] --> Loop 170 * CEs [780] --> Loop 171 * CEs [777] --> Loop 172 * CEs [774] --> Loop 173 * CEs [771] --> Loop 174 * CEs [768] --> Loop 175 * CEs [765] --> Loop 176 * CEs [762] --> Loop 177 * CEs [761,763,764,766,767,769,770,772,773,775,776,778,779,781,782,784,785,787,788,790] --> Loop 178 ### Ranking functions of CR testQuicksort2(V,Out) #### Partial ranking functions of CR testQuicksort2(V,Out) ### Specialization of cost equations start/4 * CE 1 is refined into CE [791] * CE 2 is refined into CE [792] * CE 3 is refined into CE [793,794,795,796,797,798,799,800,801,802,803,804,805,806,807,808,809,810,811,812,813,814,815,816,817,818,819,820,821,822,823,824,825,826,827,828,829,830,831,832,833,834,835,836,837,838,839,840,841,842,843,844,845,846,847,848] * CE 4 is refined into CE [849,850,851,852,853] * CE 5 is refined into CE [854,855,856,857,858,859,860,861,862,863,864,865,866,867,868,869,870,871,872,873,874,875,876,877,878,879,880] * CE 6 is refined into CE [881,882,883,884,885,886,887,888,889,890,891,892,893,894,895,896,897,898,899,900,901,902,903,904,905,906,907,908,909,910,911,912,913,914,915,916,917,918,919,920,921,922,923,924,925,926,927,928,929,930,931,932,933,934,935,936] * CE 7 is refined into CE [937,938,939,940,941] * CE 8 is refined into CE [942,943,944,945,946,947,948,949,950,951,952,953,954,955,956,957,958,959,960,961,962,963,964,965,966,967,968] * CE 9 is refined into CE [969,970,971,972,973,974,975,976,977,978,979,980,981,982,983,984,985] * CE 10 is refined into CE [986,987,988,989,990,991,992,993,994,995,996,997,998,999,1000,1001,1002] * CE 11 is refined into CE [1003,1004,1005,1006] * CE 12 is refined into CE [1007,1008,1009,1010] * CE 13 is refined into CE [1011,1012,1013] * CE 14 is refined into CE [1014,1015,1016,1017,1018,1019,1020,1021,1022,1023] * CE 15 is refined into CE [1024,1025,1026,1027] * CE 16 is refined into CE [1028,1029,1030,1031] * CE 17 is refined into CE [1032,1033,1034] * CE 18 is refined into CE [1035,1036,1037] * CE 19 is refined into CE [1038,1039,1040,1041,1042] * CE 20 is refined into CE [1043,1044,1045,1046,1047,1048,1049] * CE 21 is refined into CE [1050,1051,1052] * CE 22 is refined into CE [1053,1054,1055,1056,1057] * CE 23 is refined into CE [1058,1059,1060,1061,1062,1063,1064] * CE 24 is refined into CE [1065,1066,1067] * CE 25 is refined into CE [1068,1069,1070,1071,1072,1073,1074,1075,1076,1077] * CE 26 is refined into CE [1078,1079,1080,1081,1082,1083,1084,1085,1086,1087] * CE 27 is refined into CE [1088,1089,1090,1091,1092,1093,1094,1095,1096,1097] * CE 28 is refined into CE [1098,1099,1100,1101] * CE 29 is refined into CE [1102,1103,1104,1105,1106,1107,1108,1109,1110] ### Cost equations --> "Loop" of start/4 * CEs [1048,1063] --> Loop 179 * CEs [1021,1108] --> Loop 180 * CEs [1041,1056] --> Loop 181 * CEs [978,995] --> Loop 182 * CEs [1046,1047,1061,1062] --> Loop 183 * CEs [970,971,972,975,987,988,989,992,1018,1019,1020,1040,1043,1045,1055,1058,1060,1105,1106] --> Loop 184 * CEs [1100] --> Loop 185 * CEs [1051,1066,1099] --> Loop 186 * CEs [973,976,977,990,993,994,1050,1065,1098] --> Loop 187 * CEs [791,792,793,794,795,796,797,798,799,800,801,802,803,804,805,806,807,808,809,810,811,812,813,814,815,816,817,818,819,820,821,822,823,824,825,826,827,828,829,830,831,832,833,834,835,836,837,838,839,840,841,842,843,844,845,846,847,848,849,850,851,852,853,854,855,856,857,858,859,860,861,862,863,864,865,866,867,868,869,870,871,872,873,874,875,876,877,878,879,880,881,882,883,884,885,886,887,888,889,890,891,892,893,894,895,896,897,898,899,900,901,902,903,904,905,906,907,908,909,910,911,912,913,914,915,916,917,918,919,920,921,922,923,924,925,926,927,928,929,930,931,932,933,934,935,936,937,938,939,940,941,942,943,944,945,946,947,948,949,950,951,952,953,954,955,956,957,958,959,960,961,962,963,964,965,966,967,968,969,974,979,980,981,982,983,984,985,986,991,996,997,998,999,1000,1001,1002,1003,1004,1005,1006,1007,1008,1009,1010,1011,1012,1013,1014,1015,1016,1017,1022,1023,1024,1025,1026,1027,1028,1029,1030,1031,1032,1033,1034,1035,1036,1037,1038,1039,1042,1044,1049,1052,1053,1054,1057,1059,1064,1067,1068,1069,1070,1071,1072,1073,1074,1075,1076,1077,1078,1079,1080,1081,1082,1083,1084,1085,1086,1087,1088,1089,1090,1091,1092,1093,1094,1095,1096,1097,1101,1102,1103,1104,1107,1109,1110] --> Loop 188 ### Ranking functions of CR start(V,V3,V37,V44) #### Partial ranking functions of CR start(V,V3,V37,V44) Computing Bounds ===================================== #### Cost of chains of append(V,V3,Out): * Chain [[51],50]: 2*it(51)+2 Such that:it(51) =< -V3+Out with precondition: [V+V3=Out,V>=1,V3>=0] * Chain [[51],49]: 2*it(51)+1 Such that:it(51) =< Out with precondition: [V3>=0,Out>=1,V>=Out] * Chain [50]: 2 with precondition: [V=0,V3=Out,V3>=0] * Chain [49]: 1 with precondition: [Out=0,V>=0,V3>=0] #### Cost of chains of appendD(V,V3,Out): * Chain [[54],53]: 2*it(54)+2 Such that:it(54) =< -V3+Out with precondition: [V+V3=Out,V>=1,V3>=0] * Chain [[54],52]: 2*it(54)+1 Such that:it(54) =< Out with precondition: [V3>=0,Out>=1,V>=Out] * Chain [53]: 2 with precondition: [V=0,V3=Out,V3>=0] * Chain [52]: 1 with precondition: [Out=0,V>=0,V3>=0] #### Cost of chains of fun(V,Out): * Chain [57]: 1 with precondition: [V=0,Out=0] * Chain [56]: 1 with precondition: [V+1=Out,V>=1] * Chain [55]: 1 with precondition: [V=Out,V>=1] #### Cost of chains of fun2(V,Out): * Chain [61]: 0 with precondition: [V=1,Out=1] * Chain [60]: 0 with precondition: [V=2,Out=2] * Chain [59]: 0 with precondition: [V=3,Out=1] * Chain [58]: 0 with precondition: [Out=0,V>=0] #### Cost of chains of fun3(V,V3,Out): * Chain [[62,63],71]: 0 with precondition: [Out=1,V3=V,V3>=1] * Chain [[62,63],70]: 0 with precondition: [Out=2,V>=1,V3>=1,V+V3>=3] * Chain [[62,63],69]: 0 with precondition: [Out=3,V>=1,V3>=1,V+V3>=3] * Chain [[62,63],68]: 0 with precondition: [Out=2,V>=1,V3>=1,V+V3>=3] * Chain [[62,63],67]: 0 with precondition: [Out=3,V>=1,V3>=1,V+V3>=3] * Chain [[62,63],66]: 0 with precondition: [Out=0,V>=1,V3>=1] * Chain [[62,63],65]: 0 with precondition: [Out=2,V>=2,V3>=2] * Chain [[62,63],64]: 0 with precondition: [Out=3,V>=2,V3>=2] * Chain [71]: 0 with precondition: [V=0,V3=0,Out=1] * Chain [70]: 0 with precondition: [V=0,Out=2,V3>=1] * Chain [69]: 0 with precondition: [V=0,Out=3,V3>=1] * Chain [68]: 0 with precondition: [V3=0,Out=2,V>=1] * Chain [67]: 0 with precondition: [V3=0,Out=3,V>=1] * Chain [66]: 0 with precondition: [Out=0,V>=0,V3>=0] * Chain [65]: 0 with precondition: [Out=2,V>=1,V3>=1] * Chain [64]: 0 with precondition: [Out=3,V>=1,V3>=1] #### Cost of chains of fun1(V,V3,Out): * Chain [82]: 1 with precondition: [Out=0,V>=0,V3>=0] * Chain [81]: 1 with precondition: [V=0,V3=0,Out=1] * Chain [80]: 1 with precondition: [V=0,Out=0,V3>=1] * Chain [79]: 1 with precondition: [V=0,Out=1,V3>=1] * Chain [78]: 1 with precondition: [V=0,Out=2,V3>=1] * Chain [77]: 1 with precondition: [V3=0,Out=0,V>=1] * Chain [76]: 1 with precondition: [V3=0,Out=1,V>=1] * Chain [75]: 1 with precondition: [V3=0,Out=2,V>=1] * Chain [74]: 1 with precondition: [Out=0,V=V3,V>=1] * Chain [73]: 1 with precondition: [Out=1,V>=1,V3>=1] * Chain [72]: 1 with precondition: [Out=2,V>=1,V3>=1] #### Cost of chains of fun12(V,V3,V37,V44,Out): * Chain [85]: 1 with precondition: [V=1,V3+V37+V44+2=Out,V3>=0,V37>=0,V44>=0] * Chain [84]: 1 with precondition: [V=2,V3+V37+V44+2=Out,V3>=0,V37>=0,V44>=0] * Chain [83]: 0 with precondition: [Out=0,V>=0,V3>=0,V37>=0,V44>=0] #### Cost of chains of fun11(V,V3,V37,Out): * Chain [93]: 2 with precondition: [Out=0,V>=0,V3>=0,V37>=0] * Chain [92]: 3 with precondition: [V3=0,V37=0,V+1=Out,V>=1] * Chain [91]: 2 with precondition: [V3=0,Out=0,V>=1,V37>=1] * Chain [90]: 3 with precondition: [V3=0,V+V37+1=Out,V>=1,V37>=1] * Chain [89]: 2 with precondition: [V37=0,Out=0,V>=1,V3>=1] * Chain [88]: 3 with precondition: [V37=0,V+1=Out,V>=1,V3>=1] * Chain [87]: 2 with precondition: [Out=0,V3=V37,V>=1,V3>=1] * Chain [86]: 3 with precondition: [V+V37+1=Out,V>=1,V3>=1,V37>=1] #### Cost of chains of split(V,V3,Out): * Chain [[100,101],95]: 10*it(100)+2 Such that:aux(18) =< Out it(100) =< aux(18) with precondition: [V=0,Out=V3+1,Out>=2] * Chain [[99],[100,101],95]: 14*it(99)+2 Such that:aux(19) =< V3+1 it(99) =< aux(19) with precondition: [V=0,Out=0,V3>=2] * Chain [[99],[96,97],95]: 14*it(96)+2 Such that:aux(23) =< V3+1 it(96) =< aux(23) with precondition: [Out=0,V>=1,V3>=2] * Chain [[99],98,[96,97],95]: 14*it(96)+6 Such that:aux(24) =< -V+V3 it(96) =< aux(24) with precondition: [Out=0,V>=1,V3>=V+3] * Chain [[99],98,95]: 4*it(99)+6 Such that:it(99) =< -V+V3 with precondition: [Out=0,V>=1,V3>=V+2] * Chain [[99],95]: 4*it(99)+2 Such that:it(99) =< V3 with precondition: [Out=0,V>=0,V3>=1] * Chain [[99],94]: 4*it(99)+1 Such that:it(99) =< V3 with precondition: [Out=0,V>=0,V3>=1] * Chain [[96,97],95]: 5*it(96)+5*it(97)+2 Such that:it(96) =< Out/2 aux(22) =< Out it(96) =< aux(22) it(97) =< aux(22) with precondition: [Out=V3+1,V>=1,Out>=2] * Chain [98,[96,97],95]: 5*it(96)+5*it(97)+6 Such that:aux(22) =< -V+V3 it(96) =< -V/2+V3/2 it(96) =< aux(22) it(97) =< aux(22) with precondition: [Out=0,V>=1,V3>=V+2] * Chain [98,95]: 6 with precondition: [Out=0,V+1=V3,V>=1] * Chain [95]: 2 with precondition: [V3=0,Out=1,V>=0] * Chain [94]: 1 with precondition: [Out=0,V>=0,V3>=0] #### Cost of chains of fun15(V,V3,V37,V44,Out): * Chain [104]: 1 with precondition: [V=1,V3+V37+V44+2=Out,V3>=0,V37>=0,V44>=0] * Chain [103]: 1 with precondition: [V=2,V3+V37+V44+2=Out,V3>=0,V37>=0,V44>=0] * Chain [102]: 0 with precondition: [Out=0,V>=0,V3>=0,V37>=0,V44>=0] #### Cost of chains of fun14(V,V3,V37,Out): * Chain [112]: 2 with precondition: [Out=0,V>=0,V3>=0,V37>=0] * Chain [111]: 3 with precondition: [V3=0,V37=0,V+1=Out,V>=1] * Chain [110]: 2 with precondition: [V3=0,Out=0,V>=1,V37>=1] * Chain [109]: 3 with precondition: [V3=0,V+V37+1=Out,V>=1,V37>=1] * Chain [108]: 2 with precondition: [V37=0,Out=0,V>=1,V3>=1] * Chain [107]: 3 with precondition: [V37=0,V+1=Out,V>=1,V3>=1] * Chain [106]: 2 with precondition: [Out=0,V3=V37,V>=1,V3>=1] * Chain [105]: 3 with precondition: [V+V37+1=Out,V>=1,V3>=1,V37>=1] #### Cost of chains of splitD(V,V3,Out): * Chain [[119,120],114]: 10*it(119)+2 Such that:aux(30) =< Out it(119) =< aux(30) with precondition: [V=0,Out=V3+1,Out>=2] * Chain [[118],[119,120],114]: 14*it(118)+2 Such that:aux(31) =< V3+1 it(118) =< aux(31) with precondition: [V=0,Out=0,V3>=2] * Chain [[118],[115,116],114]: 14*it(115)+2 Such that:aux(35) =< V3+1 it(115) =< aux(35) with precondition: [Out=0,V>=1,V3>=2] * Chain [[118],117,[115,116],114]: 14*it(115)+6 Such that:aux(36) =< -V+V3 it(115) =< aux(36) with precondition: [Out=0,V>=1,V3>=V+3] * Chain [[118],117,114]: 4*it(118)+6 Such that:it(118) =< -V+V3 with precondition: [Out=0,V>=1,V3>=V+2] * Chain [[118],114]: 4*it(118)+2 Such that:it(118) =< V3 with precondition: [Out=0,V>=0,V3>=1] * Chain [[118],113]: 4*it(118)+1 Such that:it(118) =< V3 with precondition: [Out=0,V>=0,V3>=1] * Chain [[115,116],114]: 5*it(115)+5*it(116)+2 Such that:it(115) =< Out/2 aux(34) =< Out it(115) =< aux(34) it(116) =< aux(34) with precondition: [Out=V3+1,V>=1,Out>=2] * Chain [117,[115,116],114]: 5*it(115)+5*it(116)+6 Such that:aux(34) =< -V+V3 it(115) =< -V/2+V3/2 it(115) =< aux(34) it(116) =< aux(34) with precondition: [Out=0,V>=1,V3>=V+2] * Chain [117,114]: 6 with precondition: [Out=0,V+1=V3,V>=1] * Chain [114]: 2 with precondition: [V3=0,Out=1,V>=0] * Chain [113]: 1 with precondition: [Out=0,V>=0,V3>=0] #### Cost of chains of quicksort(V,Out): * Chain [133]: 10*s(25)+74*s(29)+8 Such that:aux(41) =< V aux(42) =< V/2 s(25) =< aux(42) s(29) =< aux(41) s(25) =< aux(41) with precondition: [Out=0,V>=0] * Chain [multiple(132,[[133]])]: 22 with precondition: [Out=0,V>=1] * Chain [multiple(129,[[133]])]: 23 with precondition: [V=Out,V>=1] * Chain [multiple([121,122,123,124,125,126,130,131],[[133],[multiple(132,[[133]])],[multiple(129,[[133]])],[multiple(128,[[133]])],[multiple(127,[[133]])]])]: 13*it(121)+26*it(123)+13*it(125)+8*it([133])+45*it([multiple(129,[[133]])])+10*s(87)+10*s(88)+2*s(89)+2*s(93)+40*s(95)+4*s(96)+10*s(101)+10*s(102)+10*s(111)+74*s(112)+0 Such that:aux(46) =< V aux(79) =< V+2 aux(80) =< V/2+1 aux(81) =< V/3+2/3 aux(82) =< 2/3*V aux(83) =< 2/5*V it(123) =< aux(82) it(125) =< aux(82) it(121) =< aux(83) it(125) =< aux(83) aux(54) =< aux(46)+2 aux(47) =< aux(46)+1 aux(50) =< aux(46) it([multiple(129,[[133]])]) =< it(123)*(1/3)+it(123)*(1/3)+it(123)*(1/3)+it(123)*(1/3)+aux(81) aux(74) =< it(123)+it(123)+it(123)+it(123)+aux(79) it([multiple(129,[[133]])]) =< it(123)+it(123)+it(123)+it(123)+aux(79) it([133]) =< it(123)*(1/2)+it(123)*(1/2)+it(123)*(1/2)+it(123)*(1/2)+aux(80) it([multiple(129,[[133]])]) =< it(123)*(1/2)+it(123)*(1/2)+it(123)*(1/2)+it(123)*(1/2)+aux(80) s(97) =< it(123)*aux(54) aux(61) =< it(125)*aux(47) s(96) =< it(123)*aux(54) aux(48) =< it(121)*aux(47) s(93) =< it(121)*aux(50) s(89) =< it(121)*aux(46) aux(74) =< it([133])*aux(54) s(101) =< aux(61)*(1/2) s(87) =< aux(48)*(1/2) s(114) =< aux(74)*(1/2) s(111) =< s(114) s(112) =< aux(74) s(111) =< aux(74) s(95) =< s(97) s(101) =< aux(61) s(102) =< aux(61) s(87) =< aux(48) s(88) =< aux(48) with precondition: [V>=2,Out>=0,V>=Out] #### Cost of chains of quicksortD(V,Out): * Chain [146]: 10*s(119)+74*s(123)+8 Such that:aux(85) =< V aux(86) =< V/2 s(119) =< aux(86) s(123) =< aux(85) s(119) =< aux(85) with precondition: [Out=0,V>=0] * Chain [multiple(145,[[146]])]: 22 with precondition: [Out=0,V>=1] * Chain [multiple(142,[[146]])]: 23 with precondition: [V=Out,V>=1] * Chain [multiple([134,135,136,137,138,139,143,144],[[146],[multiple(145,[[146]])],[multiple(142,[[146]])],[multiple(141,[[146]])],[multiple(140,[[146]])]])]: 13*it(134)+26*it(136)+13*it(138)+8*it([146])+45*it([multiple(142,[[146]])])+10*s(181)+10*s(182)+2*s(183)+2*s(187)+40*s(189)+4*s(190)+10*s(195)+10*s(196)+10*s(205)+74*s(206)+0 Such that:aux(90) =< V aux(123) =< V+2 aux(124) =< V/2+1 aux(125) =< V/3+2/3 aux(126) =< 2/3*V aux(127) =< 2/5*V it(136) =< aux(126) it(138) =< aux(126) it(134) =< aux(127) it(138) =< aux(127) aux(98) =< aux(90)+2 aux(91) =< aux(90)+1 aux(94) =< aux(90) it([multiple(142,[[146]])]) =< it(136)*(1/3)+it(136)*(1/3)+it(136)*(1/3)+it(136)*(1/3)+aux(125) aux(118) =< it(136)+it(136)+it(136)+it(136)+aux(123) it([multiple(142,[[146]])]) =< it(136)+it(136)+it(136)+it(136)+aux(123) it([146]) =< it(136)*(1/2)+it(136)*(1/2)+it(136)*(1/2)+it(136)*(1/2)+aux(124) it([multiple(142,[[146]])]) =< it(136)*(1/2)+it(136)*(1/2)+it(136)*(1/2)+it(136)*(1/2)+aux(124) s(191) =< it(136)*aux(98) aux(105) =< it(138)*aux(91) s(190) =< it(136)*aux(98) aux(92) =< it(134)*aux(91) s(187) =< it(134)*aux(94) s(183) =< it(134)*aux(90) aux(118) =< it([146])*aux(98) s(195) =< aux(105)*(1/2) s(181) =< aux(92)*(1/2) s(208) =< aux(118)*(1/2) s(205) =< s(208) s(206) =< aux(118) s(205) =< aux(118) s(189) =< s(191) s(195) =< aux(105) s(196) =< aux(105) s(181) =< aux(92) s(182) =< aux(92) with precondition: [V>=2,Out>=0,V>=Out] #### Cost of chains of testList(V,Out): * Chain [156]: 11 with precondition: [Out=64,V>=0] * Chain [155]: 11 with precondition: [Out=65,V>=0] * Chain [154]: 11 with precondition: [Out=66,V>=0] * Chain [153]: 11 with precondition: [Out=67,V>=0] * Chain [152]: 11 with precondition: [Out=68,V>=0] * Chain [151]: 11 with precondition: [Out=69,V>=0] * Chain [150]: 11 with precondition: [Out=70,V>=0] * Chain [149]: 11 with precondition: [Out=71,V>=0] * Chain [148]: 11 with precondition: [Out=72,V>=0] * Chain [147]: 11 with precondition: [Out=73,V>=0] #### Cost of chains of testQuicksort(V,Out): * Chain [167]: 7742617/3 with precondition: [73>=Out,V>=0,Out>=0] * Chain [166]: 35 with precondition: [Out=64,V>=0] * Chain [165]: 35 with precondition: [Out=65,V>=0] * Chain [164]: 35 with precondition: [Out=66,V>=0] * Chain [163]: 35 with precondition: [Out=67,V>=0] * Chain [162]: 35 with precondition: [Out=68,V>=0] * Chain [161]: 35 with precondition: [Out=69,V>=0] * Chain [160]: 35 with precondition: [Out=70,V>=0] * Chain [159]: 35 with precondition: [Out=71,V>=0] * Chain [158]: 35 with precondition: [Out=72,V>=0] * Chain [157]: 35 with precondition: [Out=73,V>=0] #### Cost of chains of testQuicksort2(V,Out): * Chain [178]: 7742617/3 with precondition: [73>=Out,V>=0,Out>=0] * Chain [177]: 35 with precondition: [Out=64,V>=0] * Chain [176]: 35 with precondition: [Out=65,V>=0] * Chain [175]: 35 with precondition: [Out=66,V>=0] * Chain [174]: 35 with precondition: [Out=67,V>=0] * Chain [173]: 35 with precondition: [Out=68,V>=0] * Chain [172]: 35 with precondition: [Out=69,V>=0] * Chain [171]: 35 with precondition: [Out=70,V>=0] * Chain [170]: 35 with precondition: [Out=71,V>=0] * Chain [169]: 35 with precondition: [Out=72,V>=0] * Chain [168]: 35 with precondition: [Out=73,V>=0] #### Cost of chains of start(V,V3,V37,V44): * Chain [188]: 7002*s(874)+570*s(897)+80*s(909)+652*s(910)+4936*s(917)+540*s(923)+96*s(925)+240*s(928)+112*s(930)+112*s(931)+1120*s(932)+120*s(935)+888*s(936)+2400*s(937)+1120*s(938)+1040*s(1011)+416*s(1012)+520*s(1013)+1350*s(1017)+240*s(1019)+128*s(1022)+64*s(1024)+64*s(1025)+320*s(1026)+320*s(1027)+300*s(1029)+2220*s(1030)+1280*s(1031)+320*s(1032)+320*s(1033)+1260*s(1048)+224*s(1050)+280*s(1060)+2072*s(1061)+104*s(1375)+360*s(1380)+64*s(1382)+80*s(1385)+16*s(1387)+16*s(1388)+80*s(1389)+80*s(1390)+80*s(1392)+592*s(1393)+800*s(1394)+80*s(1395)+80*s(1396)+208*s(1403)+104*s(1404)+156*s(1405)+360*s(1409)+64*s(1411)+16*s(1414)+8*s(1416)+8*s(1417)+40*s(1418)+40*s(1419)+40*s(1421)+296*s(1422)+160*s(1423)+40*s(1424)+40*s(1425)+40*s(1507)+40*s(1508)+320*s(1509)+320*s(1515)+16*s(1534)+8*s(1536)+8*s(1537)+40*s(1538)+40*s(1539)+40*s(1541)+296*s(1542)+160*s(1543)+40*s(1544)+40*s(1545)+720*s(1679)+128*s(1681)+160*s(1691)+1184*s(1692)+360*s(2155)+64*s(2157)+40*s(2167)+296*s(2168)+360*s(2184)+64*s(2186)+80*s(2196)+592*s(2197)+40*s(2289)+296*s(2290)+104*s(2881)+360*s(2886)+64*s(2888)+32*s(2891)+80*s(2895)+80*s(2898)+592*s(2899)+320*s(2900)+80*s(2901)+52*s(2968)+8*s(2980)+8*s(2981)+40*s(2982)+40*s(2983)+40*s(2988)+40*s(2989)+20*s(5285)+56*s(5289)+90*s(5353)+16*s(5355)+20*s(5365)+148*s(5366)+10*s(5403)+46*s(5407)+16*s(5408)+86*s(5409)+10*s(5412)+7742617/3 Such that:aux(462) =< -V+V3 aux(463) =< V aux(464) =< V+1 aux(465) =< V+2 aux(466) =< V+3 aux(467) =< V-V3 aux(468) =< 2*V aux(469) =< 2*V+2 aux(470) =< -V/2+V3/2 aux(471) =< V/2 aux(472) =< V/2+1 aux(473) =< V/2+1/2 aux(474) =< V/2-V3/2 aux(475) =< V/3 aux(476) =< V/3+1 aux(477) =< V/3+2/3 aux(478) =< 2/3*V aux(479) =< 2/3*V+2/3 aux(480) =< 2/5*V aux(481) =< V3 aux(482) =< V3+1 aux(483) =< V3/2+1/2 s(874) =< aux(463) s(5403) =< aux(470) s(897) =< aux(471) s(5285) =< aux(474) s(5412) =< aux(483) s(5407) =< aux(462) s(5408) =< aux(481) s(5403) =< aux(462) s(5409) =< aux(482) s(910) =< aux(464) s(917) =< aux(468) s(920) =< aux(463)+2 s(921) =< aux(463)+1 s(922) =< aux(463) s(1048) =< s(917)*(1/3)+s(917)*(1/3)+s(917)*(1/3)+s(917)*(1/3)+aux(464) s(1049) =< s(917)+s(917)+s(917)+s(917)+aux(464) s(1048) =< s(917)+s(917)+s(917)+s(917)+aux(464) s(1050) =< s(917)*(1/2)+s(917)*(1/2)+s(917)*(1/2)+s(917)*(1/2)+aux(464) s(1048) =< s(917)*(1/2)+s(917)*(1/2)+s(917)*(1/2)+s(917)*(1/2)+aux(464) s(926) =< s(917)*s(920) s(927) =< s(917)*s(921) s(928) =< s(917)*s(920) s(930) =< s(917)*s(922) s(931) =< s(917)*aux(463) s(1049) =< s(1050)*s(920) s(932) =< s(927)*(1/2) s(1059) =< s(1049)*(1/2) s(1060) =< s(1059) s(1061) =< s(1049) s(1060) =< s(1049) s(937) =< s(926) s(932) =< s(927) s(938) =< s(927) s(897) =< aux(463) s(1679) =< s(917)*(1/3)+s(917)*(1/3)+s(917)*(1/3)+s(917)*(1/3)+aux(463) s(1680) =< s(917)+s(917)+s(917)+s(917)+aux(463) s(1679) =< s(917)+s(917)+s(917)+s(917)+aux(463) s(1681) =< s(917)*(1/2)+s(917)*(1/2)+s(917)*(1/2)+s(917)*(1/2)+aux(463) s(1679) =< s(917)*(1/2)+s(917)*(1/2)+s(917)*(1/2)+s(917)*(1/2)+aux(463) s(1680) =< s(1681)*s(920) s(1690) =< s(1680)*(1/2) s(1691) =< s(1690) s(1692) =< s(1680) s(1691) =< s(1680) s(1403) =< aux(479) s(1404) =< aux(479) s(1405) =< aux(469) s(1404) =< aux(469) s(1406) =< aux(464)+2 s(1407) =< aux(464)+1 s(1408) =< aux(464) s(1409) =< s(1403)*(1/3)+s(1403)*(1/3)+s(1403)*(1/3)+s(1403)*(1/3)+aux(476) s(1410) =< s(1403)+s(1403)+s(1403)+s(1403)+aux(466) s(1409) =< s(1403)+s(1403)+s(1403)+s(1403)+aux(466) s(1411) =< s(1403)*(1/2)+s(1403)*(1/2)+s(1403)*(1/2)+s(1403)*(1/2)+aux(466) s(1409) =< s(1403)*(1/2)+s(1403)*(1/2)+s(1403)*(1/2)+s(1403)*(1/2)+aux(466) s(1412) =< s(1403)*s(1406) s(1413) =< s(1404)*s(1407) s(1414) =< s(1403)*s(1406) s(1415) =< s(1405)*s(1407) s(1416) =< s(1405)*s(1408) s(1417) =< s(1405)*aux(464) s(1410) =< s(1411)*s(1406) s(1418) =< s(1413)*(1/2) s(1419) =< s(1415)*(1/2) s(1420) =< s(1410)*(1/2) s(1421) =< s(1420) s(1422) =< s(1410) s(1421) =< s(1410) s(1423) =< s(1412) s(1418) =< s(1413) s(1424) =< s(1413) s(1419) =< s(1415) s(1425) =< s(1415) s(1375) =< aux(468) s(1013) =< aux(480) s(1375) =< aux(480) s(1377) =< aux(468)+2 s(1378) =< aux(468)+1 s(1379) =< aux(468) s(1380) =< s(917)*(1/3)+s(917)*(1/3)+s(917)*(1/3)+s(917)*(1/3)+aux(469) s(1381) =< s(917)+s(917)+s(917)+s(917)+aux(469) s(1380) =< s(917)+s(917)+s(917)+s(917)+aux(469) s(1382) =< s(917)*(1/2)+s(917)*(1/2)+s(917)*(1/2)+s(917)*(1/2)+aux(469) s(1380) =< s(917)*(1/2)+s(917)*(1/2)+s(917)*(1/2)+s(917)*(1/2)+aux(469) s(1383) =< s(917)*s(1377) s(1384) =< s(1375)*s(1378) s(1385) =< s(917)*s(1377) s(1386) =< s(1013)*s(1378) s(1387) =< s(1013)*s(1379) s(1388) =< s(1013)*aux(468) s(1381) =< s(1382)*s(1377) s(1389) =< s(1384)*(1/2) s(1390) =< s(1386)*(1/2) s(1391) =< s(1381)*(1/2) s(1392) =< s(1391) s(1393) =< s(1381) s(1392) =< s(1381) s(1394) =< s(1383) s(1389) =< s(1384) s(1395) =< s(1384) s(1390) =< s(1386) s(1396) =< s(1386) s(1011) =< aux(478) s(2881) =< aux(478) s(2881) =< aux(468) s(2886) =< s(1011)*(1/3)+s(1011)*(1/3)+s(1011)*(1/3)+s(1011)*(1/3)+aux(479) s(2887) =< s(1011)+s(1011)+s(1011)+s(1011)+aux(469) s(2886) =< s(1011)+s(1011)+s(1011)+s(1011)+aux(469) s(2888) =< s(1011)*(1/2)+s(1011)*(1/2)+s(1011)*(1/2)+s(1011)*(1/2)+aux(469) s(2886) =< s(1011)*(1/2)+s(1011)*(1/2)+s(1011)*(1/2)+s(1011)*(1/2)+aux(469) s(2889) =< s(1011)*s(1377) s(2890) =< s(2881)*s(1378) s(2891) =< s(1011)*s(1377) s(1504) =< s(917)*s(1378) s(1507) =< s(917)*s(1379) s(1508) =< s(917)*aux(468) s(2887) =< s(2888)*s(1377) s(2895) =< s(2890)*(1/2) s(1509) =< s(1504)*(1/2) s(2897) =< s(2887)*(1/2) s(2898) =< s(2897) s(2899) =< s(2887) s(2898) =< s(2887) s(2900) =< s(2889) s(2895) =< s(2890) s(2901) =< s(2890) s(1509) =< s(1504) s(1515) =< s(1504) s(2968) =< aux(468) s(2968) =< aux(469) s(2977) =< s(2968)*s(921) s(2979) =< s(1405)*s(921) s(2980) =< s(1405)*s(922) s(2981) =< s(1405)*aux(463) s(2982) =< s(2977)*(1/2) s(2983) =< s(2979)*(1/2) s(2982) =< s(2977) s(2988) =< s(2977) s(2983) =< s(2979) s(2989) =< s(2979) s(1012) =< aux(478) s(1012) =< aux(480) s(5353) =< s(1011)*(1/3)+s(1011)*(1/3)+s(1011)*(1/3)+s(1011)*(1/3)+aux(477) s(5354) =< s(1011)+s(1011)+s(1011)+s(1011)+aux(465) s(5353) =< s(1011)+s(1011)+s(1011)+s(1011)+aux(465) s(5355) =< s(1011)*(1/2)+s(1011)*(1/2)+s(1011)*(1/2)+s(1011)*(1/2)+aux(472) s(5353) =< s(1011)*(1/2)+s(1011)*(1/2)+s(1011)*(1/2)+s(1011)*(1/2)+aux(472) s(1020) =< s(1011)*s(920) s(1021) =< s(1012)*s(921) s(1022) =< s(1011)*s(920) s(1023) =< s(1013)*s(921) s(1024) =< s(1013)*s(922) s(1025) =< s(1013)*aux(463) s(5354) =< s(5355)*s(920) s(1026) =< s(1021)*(1/2) s(1027) =< s(1023)*(1/2) s(5364) =< s(5354)*(1/2) s(5365) =< s(5364) s(5366) =< s(5354) s(5365) =< s(5354) s(1031) =< s(1020) s(1026) =< s(1021) s(1032) =< s(1021) s(1027) =< s(1023) s(1033) =< s(1023) s(5289) =< aux(467) s(5285) =< aux(467) s(1017) =< s(1011)*(1/3)+s(1011)*(1/3)+s(1011)*(1/3)+s(1011)*(1/3)+aux(475) s(1018) =< s(1011)+s(1011)+s(1011)+s(1011)+aux(463) s(1017) =< s(1011)+s(1011)+s(1011)+s(1011)+aux(463) s(1019) =< s(1011)*(1/2)+s(1011)*(1/2)+s(1011)*(1/2)+s(1011)*(1/2)+aux(471) s(1017) =< s(1011)*(1/2)+s(1011)*(1/2)+s(1011)*(1/2)+s(1011)*(1/2)+aux(471) s(1018) =< s(1019)*s(920) s(1028) =< s(1018)*(1/2) s(1029) =< s(1028) s(1030) =< s(1018) s(1029) =< s(1018) s(2184) =< s(917)*(1/3)+s(917)*(1/3)+s(917)*(1/3)+s(917)*(1/3)+aux(468) s(2185) =< s(917)+s(917)+s(917)+s(917)+aux(463) s(2184) =< s(917)+s(917)+s(917)+s(917)+aux(463) s(2186) =< s(917)*(1/2)+s(917)*(1/2)+s(917)*(1/2)+s(917)*(1/2)+aux(468) s(2184) =< s(917)*(1/2)+s(917)*(1/2)+s(917)*(1/2)+s(917)*(1/2)+aux(468) s(2185) =< s(2186)*s(1377) s(2195) =< s(2185)*(1/2) s(2196) =< s(2195) s(2197) =< s(2185) s(2196) =< s(2185) s(2155) =< s(917)*(1/3)+s(917)*(1/3)+s(917)*(1/3)+s(917)*(1/3)+aux(465) s(2156) =< s(917)+s(917)+s(917)+s(917)+aux(465) s(2155) =< s(917)+s(917)+s(917)+s(917)+aux(465) s(2157) =< s(917)*(1/2)+s(917)*(1/2)+s(917)*(1/2)+s(917)*(1/2)+aux(465) s(2155) =< s(917)*(1/2)+s(917)*(1/2)+s(917)*(1/2)+s(917)*(1/2)+aux(465) s(2156) =< s(2157)*s(920) s(2166) =< s(2156)*(1/2) s(2167) =< s(2166) s(2168) =< s(2156) s(2167) =< s(2156) s(2278) =< s(917)+s(917)+s(917)+s(917)+aux(465) s(2278) =< s(2157)*s(1377) s(2288) =< s(2278)*(1/2) s(2289) =< s(2288) s(2290) =< s(2278) s(2289) =< s(2278) s(923) =< s(917)*(1/3)+s(917)*(1/3)+s(917)*(1/3)+s(917)*(1/3)+aux(464) s(924) =< s(917)+s(917)+s(917)+s(917)+aux(464) s(923) =< s(917)+s(917)+s(917)+s(917)+aux(464) s(925) =< s(917)*(1/2)+s(917)*(1/2)+s(917)*(1/2)+s(917)*(1/2)+aux(473) s(923) =< s(917)*(1/2)+s(917)*(1/2)+s(917)*(1/2)+s(917)*(1/2)+aux(473) s(924) =< s(925)*s(920) s(934) =< s(924)*(1/2) s(935) =< s(934) s(936) =< s(924) s(935) =< s(924) s(909) =< aux(468) s(909) =< aux(464) s(1530) =< s(1403)+s(1403)+s(1403)+s(1403)+aux(466) s(1532) =< s(1403)*s(1377) s(1533) =< s(1404)*s(1378) s(1534) =< s(1403)*s(1377) s(1535) =< s(1405)*s(1378) s(1536) =< s(1405)*s(1379) s(1537) =< s(1405)*aux(468) s(1530) =< s(1411)*s(1377) s(1538) =< s(1533)*(1/2) s(1539) =< s(1535)*(1/2) s(1540) =< s(1530)*(1/2) s(1541) =< s(1540) s(1542) =< s(1530) s(1541) =< s(1530) s(1543) =< s(1532) s(1538) =< s(1533) s(1544) =< s(1533) s(1539) =< s(1535) s(1545) =< s(1535) s(5412) =< aux(482) with precondition: [V>=0] * Chain [187]: 6 with precondition: [V=1] * Chain [186]: 1 with precondition: [V=2] * Chain [185]: 0 with precondition: [V=3] * Chain [184]: 60*s(5428)+6 Such that:aux(484) =< V s(5428) =< aux(484) with precondition: [V3=0,V>=0] * Chain [183]: 3 with precondition: [V37=0,V>=1,V3>=1] * Chain [182]: 5 with precondition: [V=V3+1,V>=2] * Chain [181]: 6 with precondition: [V+1=V3,V>=1] * Chain [180]: 1 with precondition: [V=V3,V>=1] * Chain [179]: 2 with precondition: [V3=V37,V>=1,V3>=1] Closed-form bounds of start(V,V3,V37,V44): ------------------------------------- * Chain [188] with precondition: [V>=0] - Upper bound: 12116*V+7742617/3+4604*V*(2*V)+2/3*V*(1888*V)+2/5*V*(608*V)+(2*V+2)*(76*V)+nat(V3)*16+92672*V+3120*V*(2*V)+2/3*V*(944*V)+2/5*V*(304*V)+(2*V+2)*(152*V)+(2/3*V+2/3)*(472*V)+14240*V+448*V+(5836*V+5836)+(76*V+76)*(2*V+2)+(2/3*V+2/3)*(236*V+236)+(1214*V+2428)+(696*V+2088)+nat(V3+1)*86+nat(-V+V3)*46+(4176*V+4176)+(3088*V+3088)+(8*V+16)+(48*V+48)+(120*V+360)+(30*V+60)+nat(V3/2+1/2)*10+nat(-V/2+V3/2)*10+nat(V-V3)*56+nat(V/2-V3/2)*20+405*V+450*V - Complexity: n^2 * Chain [187] with precondition: [V=1] - Upper bound: 6 - Complexity: constant * Chain [186] with precondition: [V=2] - Upper bound: 1 - Complexity: constant * Chain [185] with precondition: [V=3] - Upper bound: 0 - Complexity: constant * Chain [184] with precondition: [V3=0,V>=0] - Upper bound: 60*V+6 - Complexity: n * Chain [183] with precondition: [V37=0,V>=1,V3>=1] - Upper bound: 3 - Complexity: constant * Chain [182] with precondition: [V=V3+1,V>=2] - Upper bound: 5 - Complexity: constant * Chain [181] with precondition: [V+1=V3,V>=1] - Upper bound: 6 - Complexity: constant * Chain [180] with precondition: [V=V3,V>=1] - Upper bound: 1 - Complexity: constant * Chain [179] with precondition: [V3=V37,V>=1,V3>=1] - Upper bound: 2 - Complexity: constant ### Maximum cost of start(V,V3,V37,V44): max([6,12056*V+7742599/3+4604*V*(2*V)+2/3*V*(1888*V)+2/5*V*(608*V)+(2*V+2)*(76*V)+nat(V3)*16+92672*V+3120*V*(2*V)+2/3*V*(944*V)+2/5*V*(304*V)+(2*V+2)*(152*V)+(2/3*V+2/3)*(472*V)+14240*V+448*V+(5836*V+5836)+(76*V+76)*(2*V+2)+(2/3*V+2/3)*(236*V+236)+(1214*V+2428)+(696*V+2088)+nat(V3+1)*86+nat(-V+V3)*46+(4176*V+4176)+(3088*V+3088)+(8*V+16)+(48*V+48)+(120*V+360)+(30*V+60)+nat(V3/2+1/2)*10+nat(-V/2+V3/2)*10+nat(V-V3)*56+nat(V/2-V3/2)*20+405*V+450*V+(60*V+6)]) Asymptotic class: n^2 * Total analysis performed in 33241 ms. ---------------------------------------- (12) BOUNDS(1, n^2) ---------------------------------------- (13) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (14) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^2, INF). The TRS R consists of the following rules: #abs(#0) -> #0 #abs(#neg(@x)) -> #pos(@x) #abs(#pos(@x)) -> #pos(@x) #abs(#s(@x)) -> #pos(#s(@x)) #greater(@x, @y) -> #ckgt(#compare(@x, @y)) append(@l, @ys) -> append#1(@l, @ys) append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) append#1(nil, @ys) -> @ys appendD(@l, @ys) -> appendD#1(@l, @ys) appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) appendD#1(nil, @ys) -> @ys quicksort(@l) -> quicksort#1(@l) quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) quicksort#1(nil) -> nil quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) quicksortD(@l) -> quicksortD#1(@l) quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) quicksortD#1(nil) -> nil quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) split(@pivot, @l) -> split#1(@l, @pivot) split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) split#1(nil, @pivot) -> tuple#2(nil, nil) split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) split#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) split#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) splitD(@pivot, @l) -> splitD#1(@l, @pivot) splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) splitD#1(nil, @pivot) -> tuple#2(nil, nil) splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) splitD#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) splitD#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) testList(@x) -> ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)))))))))) testQuicksort(@x) -> quicksort(testList(#unit)) testQuicksort2(@x) -> quicksort(testList(#unit)) The (relative) TRS S consists of the following rules: #ckgt(#EQ) -> #false #ckgt(#GT) -> #true #ckgt(#LT) -> #false #compare(#0, #0) -> #EQ #compare(#0, #neg(@y)) -> #GT #compare(#0, #pos(@y)) -> #LT #compare(#0, #s(@y)) -> #LT #compare(#neg(@x), #0) -> #LT #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) #compare(#neg(@x), #pos(@y)) -> #LT #compare(#pos(@x), #0) -> #GT #compare(#pos(@x), #neg(@y)) -> #GT #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) #compare(#s(@x), #0) -> #GT #compare(#s(@x), #s(@y)) -> #compare(@x, @y) Rewrite Strategy: INNERMOST ---------------------------------------- (15) SlicingProof (LOWER BOUND(ID)) Sliced the following arguments: testList/0 testQuicksort/0 testQuicksort2/0 ---------------------------------------- (16) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^2, INF). The TRS R consists of the following rules: #abs(#0) -> #0 #abs(#neg(@x)) -> #pos(@x) #abs(#pos(@x)) -> #pos(@x) #abs(#s(@x)) -> #pos(#s(@x)) #greater(@x, @y) -> #ckgt(#compare(@x, @y)) append(@l, @ys) -> append#1(@l, @ys) append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) append#1(nil, @ys) -> @ys appendD(@l, @ys) -> appendD#1(@l, @ys) appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) appendD#1(nil, @ys) -> @ys quicksort(@l) -> quicksort#1(@l) quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) quicksort#1(nil) -> nil quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) quicksortD(@l) -> quicksortD#1(@l) quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) quicksortD#1(nil) -> nil quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) split(@pivot, @l) -> split#1(@l, @pivot) split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) split#1(nil, @pivot) -> tuple#2(nil, nil) split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) split#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) split#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) splitD(@pivot, @l) -> splitD#1(@l, @pivot) splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) splitD#1(nil, @pivot) -> tuple#2(nil, nil) splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) splitD#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) splitD#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) testList -> ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)))))))))) testQuicksort -> quicksort(testList) testQuicksort2 -> quicksort(testList) The (relative) TRS S consists of the following rules: #ckgt(#EQ) -> #false #ckgt(#GT) -> #true #ckgt(#LT) -> #false #compare(#0, #0) -> #EQ #compare(#0, #neg(@y)) -> #GT #compare(#0, #pos(@y)) -> #LT #compare(#0, #s(@y)) -> #LT #compare(#neg(@x), #0) -> #LT #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) #compare(#neg(@x), #pos(@y)) -> #LT #compare(#pos(@x), #0) -> #GT #compare(#pos(@x), #neg(@y)) -> #GT #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) #compare(#s(@x), #0) -> #GT #compare(#s(@x), #s(@y)) -> #compare(@x, @y) Rewrite Strategy: INNERMOST ---------------------------------------- (17) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (18) Obligation: Innermost TRS: Rules: #abs(#0) -> #0 #abs(#neg(@x)) -> #pos(@x) #abs(#pos(@x)) -> #pos(@x) #abs(#s(@x)) -> #pos(#s(@x)) #greater(@x, @y) -> #ckgt(#compare(@x, @y)) append(@l, @ys) -> append#1(@l, @ys) append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) append#1(nil, @ys) -> @ys appendD(@l, @ys) -> appendD#1(@l, @ys) appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) appendD#1(nil, @ys) -> @ys quicksort(@l) -> quicksort#1(@l) quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) quicksort#1(nil) -> nil quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) quicksortD(@l) -> quicksortD#1(@l) quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) quicksortD#1(nil) -> nil quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) split(@pivot, @l) -> split#1(@l, @pivot) split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) split#1(nil, @pivot) -> tuple#2(nil, nil) split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) split#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) split#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) splitD(@pivot, @l) -> splitD#1(@l, @pivot) splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) splitD#1(nil, @pivot) -> tuple#2(nil, nil) splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) splitD#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) splitD#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) testList -> ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)))))))))) testQuicksort -> quicksort(testList) testQuicksort2 -> quicksort(testList) #ckgt(#EQ) -> #false #ckgt(#GT) -> #true #ckgt(#LT) -> #false #compare(#0, #0) -> #EQ #compare(#0, #neg(@y)) -> #GT #compare(#0, #pos(@y)) -> #LT #compare(#0, #s(@y)) -> #LT #compare(#neg(@x), #0) -> #LT #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) #compare(#neg(@x), #pos(@y)) -> #LT #compare(#pos(@x), #0) -> #GT #compare(#pos(@x), #neg(@y)) -> #GT #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) #compare(#s(@x), #0) -> #GT #compare(#s(@x), #s(@y)) -> #compare(@x, @y) Types: #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 :: :::nil testQuicksort :: :::nil testQuicksort2 :: :::nil #EQ :: #EQ:#GT:#LT #GT :: #EQ:#GT:#LT #LT :: #EQ:#GT:#LT hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s hole_#false:#true2_4 :: #false:#true hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT hole_:::nil4_4 :: :::nil hole_tuple#25_4 :: tuple#2 gen_#0:#neg:#pos:#s6_4 :: Nat -> #0:#neg:#pos:#s gen_:::nil7_4 :: Nat -> :::nil ---------------------------------------- (19) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: #compare, append, append#1, appendD, appendD#1, quicksort, quicksort#1, split, quicksortD, quicksortD#1, splitD, split#1, splitD#1 They will be analysed ascendingly in the following order: append = append#1 append < quicksort#1 appendD = appendD#1 appendD < quicksortD#1 quicksort = quicksort#1 split < quicksort#1 split = split#1 quicksortD = quicksortD#1 splitD < quicksortD#1 splitD = splitD#1 ---------------------------------------- (20) Obligation: Innermost TRS: Rules: #abs(#0) -> #0 #abs(#neg(@x)) -> #pos(@x) #abs(#pos(@x)) -> #pos(@x) #abs(#s(@x)) -> #pos(#s(@x)) #greater(@x, @y) -> #ckgt(#compare(@x, @y)) append(@l, @ys) -> append#1(@l, @ys) append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) append#1(nil, @ys) -> @ys appendD(@l, @ys) -> appendD#1(@l, @ys) appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) appendD#1(nil, @ys) -> @ys quicksort(@l) -> quicksort#1(@l) quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) quicksort#1(nil) -> nil quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) quicksortD(@l) -> quicksortD#1(@l) quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) quicksortD#1(nil) -> nil quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) split(@pivot, @l) -> split#1(@l, @pivot) split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) split#1(nil, @pivot) -> tuple#2(nil, nil) split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) split#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) split#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) splitD(@pivot, @l) -> splitD#1(@l, @pivot) splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) splitD#1(nil, @pivot) -> tuple#2(nil, nil) splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) splitD#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) splitD#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) testList -> ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)))))))))) testQuicksort -> quicksort(testList) testQuicksort2 -> quicksort(testList) #ckgt(#EQ) -> #false #ckgt(#GT) -> #true #ckgt(#LT) -> #false #compare(#0, #0) -> #EQ #compare(#0, #neg(@y)) -> #GT #compare(#0, #pos(@y)) -> #LT #compare(#0, #s(@y)) -> #LT #compare(#neg(@x), #0) -> #LT #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) #compare(#neg(@x), #pos(@y)) -> #LT #compare(#pos(@x), #0) -> #GT #compare(#pos(@x), #neg(@y)) -> #GT #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) #compare(#s(@x), #0) -> #GT #compare(#s(@x), #s(@y)) -> #compare(@x, @y) Types: #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 :: :::nil testQuicksort :: :::nil testQuicksort2 :: :::nil #EQ :: #EQ:#GT:#LT #GT :: #EQ:#GT:#LT #LT :: #EQ:#GT:#LT hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s hole_#false:#true2_4 :: #false:#true hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT hole_:::nil4_4 :: :::nil hole_tuple#25_4 :: tuple#2 gen_#0:#neg:#pos:#s6_4 :: Nat -> #0:#neg:#pos:#s gen_:::nil7_4 :: Nat -> :::nil Generator Equations: gen_#0:#neg:#pos:#s6_4(0) <=> #0 gen_#0:#neg:#pos:#s6_4(+(x, 1)) <=> #neg(gen_#0:#neg:#pos:#s6_4(x)) gen_:::nil7_4(0) <=> nil gen_:::nil7_4(+(x, 1)) <=> ::(#0, gen_:::nil7_4(x)) The following defined symbols remain to be analysed: #compare, append, append#1, appendD, appendD#1, quicksort, quicksort#1, split, quicksortD, quicksortD#1, splitD, split#1, splitD#1 They will be analysed ascendingly in the following order: append = append#1 append < quicksort#1 appendD = appendD#1 appendD < quicksortD#1 quicksort = quicksort#1 split < quicksort#1 split = split#1 quicksortD = quicksortD#1 splitD < quicksortD#1 splitD = splitD#1 ---------------------------------------- (21) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: #compare(gen_#0:#neg:#pos:#s6_4(n9_4), gen_#0:#neg:#pos:#s6_4(n9_4)) -> #EQ, rt in Omega(0) Induction Base: #compare(gen_#0:#neg:#pos:#s6_4(0), gen_#0:#neg:#pos:#s6_4(0)) ->_R^Omega(0) #EQ Induction Step: #compare(gen_#0:#neg:#pos:#s6_4(+(n9_4, 1)), gen_#0:#neg:#pos:#s6_4(+(n9_4, 1))) ->_R^Omega(0) #compare(gen_#0:#neg:#pos:#s6_4(n9_4), gen_#0:#neg:#pos:#s6_4(n9_4)) ->_IH #EQ We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (22) Obligation: Innermost TRS: Rules: #abs(#0) -> #0 #abs(#neg(@x)) -> #pos(@x) #abs(#pos(@x)) -> #pos(@x) #abs(#s(@x)) -> #pos(#s(@x)) #greater(@x, @y) -> #ckgt(#compare(@x, @y)) append(@l, @ys) -> append#1(@l, @ys) append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) append#1(nil, @ys) -> @ys appendD(@l, @ys) -> appendD#1(@l, @ys) appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) appendD#1(nil, @ys) -> @ys quicksort(@l) -> quicksort#1(@l) quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) quicksort#1(nil) -> nil quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) quicksortD(@l) -> quicksortD#1(@l) quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) quicksortD#1(nil) -> nil quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) split(@pivot, @l) -> split#1(@l, @pivot) split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) split#1(nil, @pivot) -> tuple#2(nil, nil) split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) split#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) split#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) splitD(@pivot, @l) -> splitD#1(@l, @pivot) splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) splitD#1(nil, @pivot) -> tuple#2(nil, nil) splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) splitD#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) splitD#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) testList -> ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)))))))))) testQuicksort -> quicksort(testList) testQuicksort2 -> quicksort(testList) #ckgt(#EQ) -> #false #ckgt(#GT) -> #true #ckgt(#LT) -> #false #compare(#0, #0) -> #EQ #compare(#0, #neg(@y)) -> #GT #compare(#0, #pos(@y)) -> #LT #compare(#0, #s(@y)) -> #LT #compare(#neg(@x), #0) -> #LT #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) #compare(#neg(@x), #pos(@y)) -> #LT #compare(#pos(@x), #0) -> #GT #compare(#pos(@x), #neg(@y)) -> #GT #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) #compare(#s(@x), #0) -> #GT #compare(#s(@x), #s(@y)) -> #compare(@x, @y) Types: #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 :: :::nil testQuicksort :: :::nil testQuicksort2 :: :::nil #EQ :: #EQ:#GT:#LT #GT :: #EQ:#GT:#LT #LT :: #EQ:#GT:#LT hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s hole_#false:#true2_4 :: #false:#true hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT hole_:::nil4_4 :: :::nil hole_tuple#25_4 :: tuple#2 gen_#0:#neg:#pos:#s6_4 :: Nat -> #0:#neg:#pos:#s gen_:::nil7_4 :: Nat -> :::nil Lemmas: #compare(gen_#0:#neg:#pos:#s6_4(n9_4), gen_#0:#neg:#pos:#s6_4(n9_4)) -> #EQ, rt in Omega(0) Generator Equations: gen_#0:#neg:#pos:#s6_4(0) <=> #0 gen_#0:#neg:#pos:#s6_4(+(x, 1)) <=> #neg(gen_#0:#neg:#pos:#s6_4(x)) gen_:::nil7_4(0) <=> nil gen_:::nil7_4(+(x, 1)) <=> ::(#0, gen_:::nil7_4(x)) The following defined symbols remain to be analysed: splitD#1, append, append#1, appendD, appendD#1, quicksort, quicksort#1, split, quicksortD, quicksortD#1, splitD, split#1 They will be analysed ascendingly in the following order: append = append#1 append < quicksort#1 appendD = appendD#1 appendD < quicksortD#1 quicksort = quicksort#1 split < quicksort#1 split = split#1 quicksortD = quicksortD#1 splitD < quicksortD#1 splitD = splitD#1 ---------------------------------------- (23) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: splitD#1(gen_:::nil7_4(n318812_4), gen_#0:#neg:#pos:#s6_4(0)) -> tuple#2(gen_:::nil7_4(n318812_4), gen_:::nil7_4(0)), rt in Omega(1 + n318812_4) Induction Base: splitD#1(gen_:::nil7_4(0), gen_#0:#neg:#pos:#s6_4(0)) ->_R^Omega(1) tuple#2(nil, nil) Induction Step: splitD#1(gen_:::nil7_4(+(n318812_4, 1)), gen_#0:#neg:#pos:#s6_4(0)) ->_R^Omega(1) splitD#2(splitD(gen_#0:#neg:#pos:#s6_4(0), gen_:::nil7_4(n318812_4)), gen_#0:#neg:#pos:#s6_4(0), #0) ->_R^Omega(1) splitD#2(splitD#1(gen_:::nil7_4(n318812_4), gen_#0:#neg:#pos:#s6_4(0)), gen_#0:#neg:#pos:#s6_4(0), #0) ->_IH splitD#2(tuple#2(gen_:::nil7_4(c318813_4), gen_:::nil7_4(0)), gen_#0:#neg:#pos:#s6_4(0), #0) ->_R^Omega(1) splitD#3(#greater(#0, gen_#0:#neg:#pos:#s6_4(0)), gen_:::nil7_4(n318812_4), gen_:::nil7_4(0), #0) ->_R^Omega(1) splitD#3(#ckgt(#compare(#0, gen_#0:#neg:#pos:#s6_4(0))), gen_:::nil7_4(n318812_4), gen_:::nil7_4(0), #0) ->_L^Omega(0) splitD#3(#ckgt(#EQ), gen_:::nil7_4(n318812_4), gen_:::nil7_4(0), #0) ->_R^Omega(0) splitD#3(#false, gen_:::nil7_4(n318812_4), gen_:::nil7_4(0), #0) ->_R^Omega(1) tuple#2(::(#0, gen_:::nil7_4(n318812_4)), gen_:::nil7_4(0)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (24) Complex Obligation (BEST) ---------------------------------------- (25) Obligation: Proved the lower bound n^1 for the following obligation: Innermost TRS: Rules: #abs(#0) -> #0 #abs(#neg(@x)) -> #pos(@x) #abs(#pos(@x)) -> #pos(@x) #abs(#s(@x)) -> #pos(#s(@x)) #greater(@x, @y) -> #ckgt(#compare(@x, @y)) append(@l, @ys) -> append#1(@l, @ys) append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) append#1(nil, @ys) -> @ys appendD(@l, @ys) -> appendD#1(@l, @ys) appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) appendD#1(nil, @ys) -> @ys quicksort(@l) -> quicksort#1(@l) quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) quicksort#1(nil) -> nil quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) quicksortD(@l) -> quicksortD#1(@l) quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) quicksortD#1(nil) -> nil quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) split(@pivot, @l) -> split#1(@l, @pivot) split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) split#1(nil, @pivot) -> tuple#2(nil, nil) split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) split#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) split#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) splitD(@pivot, @l) -> splitD#1(@l, @pivot) splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) splitD#1(nil, @pivot) -> tuple#2(nil, nil) splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) splitD#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) splitD#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) testList -> ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)))))))))) testQuicksort -> quicksort(testList) testQuicksort2 -> quicksort(testList) #ckgt(#EQ) -> #false #ckgt(#GT) -> #true #ckgt(#LT) -> #false #compare(#0, #0) -> #EQ #compare(#0, #neg(@y)) -> #GT #compare(#0, #pos(@y)) -> #LT #compare(#0, #s(@y)) -> #LT #compare(#neg(@x), #0) -> #LT #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) #compare(#neg(@x), #pos(@y)) -> #LT #compare(#pos(@x), #0) -> #GT #compare(#pos(@x), #neg(@y)) -> #GT #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) #compare(#s(@x), #0) -> #GT #compare(#s(@x), #s(@y)) -> #compare(@x, @y) Types: #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 :: :::nil testQuicksort :: :::nil testQuicksort2 :: :::nil #EQ :: #EQ:#GT:#LT #GT :: #EQ:#GT:#LT #LT :: #EQ:#GT:#LT hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s hole_#false:#true2_4 :: #false:#true hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT hole_:::nil4_4 :: :::nil hole_tuple#25_4 :: tuple#2 gen_#0:#neg:#pos:#s6_4 :: Nat -> #0:#neg:#pos:#s gen_:::nil7_4 :: Nat -> :::nil Lemmas: #compare(gen_#0:#neg:#pos:#s6_4(n9_4), gen_#0:#neg:#pos:#s6_4(n9_4)) -> #EQ, rt in Omega(0) Generator Equations: gen_#0:#neg:#pos:#s6_4(0) <=> #0 gen_#0:#neg:#pos:#s6_4(+(x, 1)) <=> #neg(gen_#0:#neg:#pos:#s6_4(x)) gen_:::nil7_4(0) <=> nil gen_:::nil7_4(+(x, 1)) <=> ::(#0, gen_:::nil7_4(x)) The following defined symbols remain to be analysed: splitD#1, append, append#1, appendD, appendD#1, quicksort, quicksort#1, split, quicksortD, quicksortD#1, splitD, split#1 They will be analysed ascendingly in the following order: append = append#1 append < quicksort#1 appendD = appendD#1 appendD < quicksortD#1 quicksort = quicksort#1 split < quicksort#1 split = split#1 quicksortD = quicksortD#1 splitD < quicksortD#1 splitD = splitD#1 ---------------------------------------- (26) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (27) BOUNDS(n^1, INF) ---------------------------------------- (28) Obligation: Innermost TRS: Rules: #abs(#0) -> #0 #abs(#neg(@x)) -> #pos(@x) #abs(#pos(@x)) -> #pos(@x) #abs(#s(@x)) -> #pos(#s(@x)) #greater(@x, @y) -> #ckgt(#compare(@x, @y)) append(@l, @ys) -> append#1(@l, @ys) append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) append#1(nil, @ys) -> @ys appendD(@l, @ys) -> appendD#1(@l, @ys) appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) appendD#1(nil, @ys) -> @ys quicksort(@l) -> quicksort#1(@l) quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) quicksort#1(nil) -> nil quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) quicksortD(@l) -> quicksortD#1(@l) quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) quicksortD#1(nil) -> nil quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) split(@pivot, @l) -> split#1(@l, @pivot) split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) split#1(nil, @pivot) -> tuple#2(nil, nil) split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) split#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) split#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) splitD(@pivot, @l) -> splitD#1(@l, @pivot) splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) splitD#1(nil, @pivot) -> tuple#2(nil, nil) splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) splitD#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) splitD#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) testList -> ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)))))))))) testQuicksort -> quicksort(testList) testQuicksort2 -> quicksort(testList) #ckgt(#EQ) -> #false #ckgt(#GT) -> #true #ckgt(#LT) -> #false #compare(#0, #0) -> #EQ #compare(#0, #neg(@y)) -> #GT #compare(#0, #pos(@y)) -> #LT #compare(#0, #s(@y)) -> #LT #compare(#neg(@x), #0) -> #LT #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) #compare(#neg(@x), #pos(@y)) -> #LT #compare(#pos(@x), #0) -> #GT #compare(#pos(@x), #neg(@y)) -> #GT #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) #compare(#s(@x), #0) -> #GT #compare(#s(@x), #s(@y)) -> #compare(@x, @y) Types: #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 :: :::nil testQuicksort :: :::nil testQuicksort2 :: :::nil #EQ :: #EQ:#GT:#LT #GT :: #EQ:#GT:#LT #LT :: #EQ:#GT:#LT hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s hole_#false:#true2_4 :: #false:#true hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT hole_:::nil4_4 :: :::nil hole_tuple#25_4 :: tuple#2 gen_#0:#neg:#pos:#s6_4 :: Nat -> #0:#neg:#pos:#s gen_:::nil7_4 :: Nat -> :::nil Lemmas: #compare(gen_#0:#neg:#pos:#s6_4(n9_4), gen_#0:#neg:#pos:#s6_4(n9_4)) -> #EQ, rt in Omega(0) splitD#1(gen_:::nil7_4(n318812_4), gen_#0:#neg:#pos:#s6_4(0)) -> tuple#2(gen_:::nil7_4(n318812_4), gen_:::nil7_4(0)), rt in Omega(1 + n318812_4) Generator Equations: gen_#0:#neg:#pos:#s6_4(0) <=> #0 gen_#0:#neg:#pos:#s6_4(+(x, 1)) <=> #neg(gen_#0:#neg:#pos:#s6_4(x)) gen_:::nil7_4(0) <=> nil gen_:::nil7_4(+(x, 1)) <=> ::(#0, gen_:::nil7_4(x)) The following defined symbols remain to be analysed: splitD, append, append#1, appendD, appendD#1, quicksort, quicksort#1, split, quicksortD, quicksortD#1, split#1 They will be analysed ascendingly in the following order: append = append#1 append < quicksort#1 appendD = appendD#1 appendD < quicksortD#1 quicksort = quicksort#1 split < quicksort#1 split = split#1 quicksortD = quicksortD#1 splitD < quicksortD#1 splitD = splitD#1 ---------------------------------------- (29) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: split#1(gen_:::nil7_4(n320997_4), gen_#0:#neg:#pos:#s6_4(0)) -> tuple#2(gen_:::nil7_4(n320997_4), gen_:::nil7_4(0)), rt in Omega(1 + n320997_4) Induction Base: split#1(gen_:::nil7_4(0), gen_#0:#neg:#pos:#s6_4(0)) ->_R^Omega(1) tuple#2(nil, nil) Induction Step: split#1(gen_:::nil7_4(+(n320997_4, 1)), gen_#0:#neg:#pos:#s6_4(0)) ->_R^Omega(1) split#2(split(gen_#0:#neg:#pos:#s6_4(0), gen_:::nil7_4(n320997_4)), gen_#0:#neg:#pos:#s6_4(0), #0) ->_R^Omega(1) split#2(split#1(gen_:::nil7_4(n320997_4), gen_#0:#neg:#pos:#s6_4(0)), gen_#0:#neg:#pos:#s6_4(0), #0) ->_IH split#2(tuple#2(gen_:::nil7_4(c320998_4), gen_:::nil7_4(0)), gen_#0:#neg:#pos:#s6_4(0), #0) ->_R^Omega(1) split#3(#greater(#0, gen_#0:#neg:#pos:#s6_4(0)), gen_:::nil7_4(n320997_4), gen_:::nil7_4(0), #0) ->_R^Omega(1) split#3(#ckgt(#compare(#0, gen_#0:#neg:#pos:#s6_4(0))), gen_:::nil7_4(n320997_4), gen_:::nil7_4(0), #0) ->_L^Omega(0) split#3(#ckgt(#EQ), gen_:::nil7_4(n320997_4), gen_:::nil7_4(0), #0) ->_R^Omega(0) split#3(#false, gen_:::nil7_4(n320997_4), gen_:::nil7_4(0), #0) ->_R^Omega(1) tuple#2(::(#0, gen_:::nil7_4(n320997_4)), gen_:::nil7_4(0)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (30) Obligation: Innermost TRS: Rules: #abs(#0) -> #0 #abs(#neg(@x)) -> #pos(@x) #abs(#pos(@x)) -> #pos(@x) #abs(#s(@x)) -> #pos(#s(@x)) #greater(@x, @y) -> #ckgt(#compare(@x, @y)) append(@l, @ys) -> append#1(@l, @ys) append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) append#1(nil, @ys) -> @ys appendD(@l, @ys) -> appendD#1(@l, @ys) appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) appendD#1(nil, @ys) -> @ys quicksort(@l) -> quicksort#1(@l) quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) quicksort#1(nil) -> nil quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) quicksortD(@l) -> quicksortD#1(@l) quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) quicksortD#1(nil) -> nil quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) split(@pivot, @l) -> split#1(@l, @pivot) split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) split#1(nil, @pivot) -> tuple#2(nil, nil) split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) split#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) split#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) splitD(@pivot, @l) -> splitD#1(@l, @pivot) splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) splitD#1(nil, @pivot) -> tuple#2(nil, nil) splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) splitD#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) splitD#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) testList -> ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)))))))))) testQuicksort -> quicksort(testList) testQuicksort2 -> quicksort(testList) #ckgt(#EQ) -> #false #ckgt(#GT) -> #true #ckgt(#LT) -> #false #compare(#0, #0) -> #EQ #compare(#0, #neg(@y)) -> #GT #compare(#0, #pos(@y)) -> #LT #compare(#0, #s(@y)) -> #LT #compare(#neg(@x), #0) -> #LT #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) #compare(#neg(@x), #pos(@y)) -> #LT #compare(#pos(@x), #0) -> #GT #compare(#pos(@x), #neg(@y)) -> #GT #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) #compare(#s(@x), #0) -> #GT #compare(#s(@x), #s(@y)) -> #compare(@x, @y) Types: #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 :: :::nil testQuicksort :: :::nil testQuicksort2 :: :::nil #EQ :: #EQ:#GT:#LT #GT :: #EQ:#GT:#LT #LT :: #EQ:#GT:#LT hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s hole_#false:#true2_4 :: #false:#true hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT hole_:::nil4_4 :: :::nil hole_tuple#25_4 :: tuple#2 gen_#0:#neg:#pos:#s6_4 :: Nat -> #0:#neg:#pos:#s gen_:::nil7_4 :: Nat -> :::nil Lemmas: #compare(gen_#0:#neg:#pos:#s6_4(n9_4), gen_#0:#neg:#pos:#s6_4(n9_4)) -> #EQ, rt in Omega(0) splitD#1(gen_:::nil7_4(n318812_4), gen_#0:#neg:#pos:#s6_4(0)) -> tuple#2(gen_:::nil7_4(n318812_4), gen_:::nil7_4(0)), rt in Omega(1 + n318812_4) split#1(gen_:::nil7_4(n320997_4), gen_#0:#neg:#pos:#s6_4(0)) -> tuple#2(gen_:::nil7_4(n320997_4), gen_:::nil7_4(0)), rt in Omega(1 + n320997_4) Generator Equations: gen_#0:#neg:#pos:#s6_4(0) <=> #0 gen_#0:#neg:#pos:#s6_4(+(x, 1)) <=> #neg(gen_#0:#neg:#pos:#s6_4(x)) gen_:::nil7_4(0) <=> nil gen_:::nil7_4(+(x, 1)) <=> ::(#0, gen_:::nil7_4(x)) The following defined symbols remain to be analysed: split, append, append#1, appendD, appendD#1, quicksort, quicksort#1, quicksortD, quicksortD#1 They will be analysed ascendingly in the following order: append = append#1 append < quicksort#1 appendD = appendD#1 appendD < quicksortD#1 quicksort = quicksort#1 split < quicksort#1 split = split#1 quicksortD = quicksortD#1 ---------------------------------------- (31) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: appendD#1(gen_:::nil7_4(n323205_4), gen_:::nil7_4(b)) -> gen_:::nil7_4(+(n323205_4, b)), rt in Omega(1 + n323205_4) Induction Base: appendD#1(gen_:::nil7_4(0), gen_:::nil7_4(b)) ->_R^Omega(1) gen_:::nil7_4(b) Induction Step: appendD#1(gen_:::nil7_4(+(n323205_4, 1)), gen_:::nil7_4(b)) ->_R^Omega(1) ::(#0, appendD(gen_:::nil7_4(n323205_4), gen_:::nil7_4(b))) ->_R^Omega(1) ::(#0, appendD#1(gen_:::nil7_4(n323205_4), gen_:::nil7_4(b))) ->_IH ::(#0, gen_:::nil7_4(+(b, c323206_4))) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (32) Obligation: Innermost TRS: Rules: #abs(#0) -> #0 #abs(#neg(@x)) -> #pos(@x) #abs(#pos(@x)) -> #pos(@x) #abs(#s(@x)) -> #pos(#s(@x)) #greater(@x, @y) -> #ckgt(#compare(@x, @y)) append(@l, @ys) -> append#1(@l, @ys) append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) append#1(nil, @ys) -> @ys appendD(@l, @ys) -> appendD#1(@l, @ys) appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) appendD#1(nil, @ys) -> @ys quicksort(@l) -> quicksort#1(@l) quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) quicksort#1(nil) -> nil quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) quicksortD(@l) -> quicksortD#1(@l) quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) quicksortD#1(nil) -> nil quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) split(@pivot, @l) -> split#1(@l, @pivot) split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) split#1(nil, @pivot) -> tuple#2(nil, nil) split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) split#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) split#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) splitD(@pivot, @l) -> splitD#1(@l, @pivot) splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) splitD#1(nil, @pivot) -> tuple#2(nil, nil) splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) splitD#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) splitD#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) testList -> ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)))))))))) testQuicksort -> quicksort(testList) testQuicksort2 -> quicksort(testList) #ckgt(#EQ) -> #false #ckgt(#GT) -> #true #ckgt(#LT) -> #false #compare(#0, #0) -> #EQ #compare(#0, #neg(@y)) -> #GT #compare(#0, #pos(@y)) -> #LT #compare(#0, #s(@y)) -> #LT #compare(#neg(@x), #0) -> #LT #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) #compare(#neg(@x), #pos(@y)) -> #LT #compare(#pos(@x), #0) -> #GT #compare(#pos(@x), #neg(@y)) -> #GT #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) #compare(#s(@x), #0) -> #GT #compare(#s(@x), #s(@y)) -> #compare(@x, @y) Types: #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 :: :::nil testQuicksort :: :::nil testQuicksort2 :: :::nil #EQ :: #EQ:#GT:#LT #GT :: #EQ:#GT:#LT #LT :: #EQ:#GT:#LT hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s hole_#false:#true2_4 :: #false:#true hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT hole_:::nil4_4 :: :::nil hole_tuple#25_4 :: tuple#2 gen_#0:#neg:#pos:#s6_4 :: Nat -> #0:#neg:#pos:#s gen_:::nil7_4 :: Nat -> :::nil Lemmas: #compare(gen_#0:#neg:#pos:#s6_4(n9_4), gen_#0:#neg:#pos:#s6_4(n9_4)) -> #EQ, rt in Omega(0) splitD#1(gen_:::nil7_4(n318812_4), gen_#0:#neg:#pos:#s6_4(0)) -> tuple#2(gen_:::nil7_4(n318812_4), gen_:::nil7_4(0)), rt in Omega(1 + n318812_4) split#1(gen_:::nil7_4(n320997_4), gen_#0:#neg:#pos:#s6_4(0)) -> tuple#2(gen_:::nil7_4(n320997_4), gen_:::nil7_4(0)), rt in Omega(1 + n320997_4) appendD#1(gen_:::nil7_4(n323205_4), gen_:::nil7_4(b)) -> gen_:::nil7_4(+(n323205_4, b)), rt in Omega(1 + n323205_4) Generator Equations: gen_#0:#neg:#pos:#s6_4(0) <=> #0 gen_#0:#neg:#pos:#s6_4(+(x, 1)) <=> #neg(gen_#0:#neg:#pos:#s6_4(x)) gen_:::nil7_4(0) <=> nil gen_:::nil7_4(+(x, 1)) <=> ::(#0, gen_:::nil7_4(x)) The following defined symbols remain to be analysed: appendD, append, append#1, quicksort, quicksort#1, quicksortD, quicksortD#1 They will be analysed ascendingly in the following order: append = append#1 append < quicksort#1 appendD = appendD#1 appendD < quicksortD#1 quicksort = quicksort#1 quicksortD = quicksortD#1 ---------------------------------------- (33) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: quicksortD#1(gen_:::nil7_4(n324930_4)) -> gen_:::nil7_4(n324930_4), rt in Omega(1 + n324930_4 + n324930_4^2) Induction Base: quicksortD#1(gen_:::nil7_4(0)) ->_R^Omega(1) nil Induction Step: quicksortD#1(gen_:::nil7_4(+(n324930_4, 1))) ->_R^Omega(1) quicksortD#2(splitD(#0, gen_:::nil7_4(n324930_4)), #0) ->_R^Omega(1) quicksortD#2(splitD#1(gen_:::nil7_4(n324930_4), #0), #0) ->_L^Omega(1 + n324930_4) quicksortD#2(tuple#2(gen_:::nil7_4(n324930_4), gen_:::nil7_4(0)), #0) ->_R^Omega(1) appendD(quicksortD(gen_:::nil7_4(n324930_4)), ::(#0, quicksortD(gen_:::nil7_4(0)))) ->_R^Omega(1) appendD(quicksortD#1(gen_:::nil7_4(n324930_4)), ::(#0, quicksortD(gen_:::nil7_4(0)))) ->_IH appendD(gen_:::nil7_4(c324931_4), ::(#0, quicksortD(gen_:::nil7_4(0)))) ->_R^Omega(1) appendD(gen_:::nil7_4(n324930_4), ::(#0, quicksortD#1(gen_:::nil7_4(0)))) ->_R^Omega(1) appendD(gen_:::nil7_4(n324930_4), ::(#0, nil)) ->_R^Omega(1) appendD#1(gen_:::nil7_4(n324930_4), ::(#0, nil)) ->_L^Omega(1 + n324930_4) gen_:::nil7_4(+(n324930_4, +(0, 1))) We have rt in Omega(n^2) and sz in O(n). Thus, we have irc_R in Omega(n^2). ---------------------------------------- (34) Complex Obligation (BEST) ---------------------------------------- (35) Obligation: Proved the lower bound n^2 for the following obligation: Innermost TRS: Rules: #abs(#0) -> #0 #abs(#neg(@x)) -> #pos(@x) #abs(#pos(@x)) -> #pos(@x) #abs(#s(@x)) -> #pos(#s(@x)) #greater(@x, @y) -> #ckgt(#compare(@x, @y)) append(@l, @ys) -> append#1(@l, @ys) append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) append#1(nil, @ys) -> @ys appendD(@l, @ys) -> appendD#1(@l, @ys) appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) appendD#1(nil, @ys) -> @ys quicksort(@l) -> quicksort#1(@l) quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) quicksort#1(nil) -> nil quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) quicksortD(@l) -> quicksortD#1(@l) quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) quicksortD#1(nil) -> nil quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) split(@pivot, @l) -> split#1(@l, @pivot) split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) split#1(nil, @pivot) -> tuple#2(nil, nil) split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) split#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) split#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) splitD(@pivot, @l) -> splitD#1(@l, @pivot) splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) splitD#1(nil, @pivot) -> tuple#2(nil, nil) splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) splitD#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) splitD#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) testList -> ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)))))))))) testQuicksort -> quicksort(testList) testQuicksort2 -> quicksort(testList) #ckgt(#EQ) -> #false #ckgt(#GT) -> #true #ckgt(#LT) -> #false #compare(#0, #0) -> #EQ #compare(#0, #neg(@y)) -> #GT #compare(#0, #pos(@y)) -> #LT #compare(#0, #s(@y)) -> #LT #compare(#neg(@x), #0) -> #LT #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) #compare(#neg(@x), #pos(@y)) -> #LT #compare(#pos(@x), #0) -> #GT #compare(#pos(@x), #neg(@y)) -> #GT #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) #compare(#s(@x), #0) -> #GT #compare(#s(@x), #s(@y)) -> #compare(@x, @y) Types: #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 :: :::nil testQuicksort :: :::nil testQuicksort2 :: :::nil #EQ :: #EQ:#GT:#LT #GT :: #EQ:#GT:#LT #LT :: #EQ:#GT:#LT hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s hole_#false:#true2_4 :: #false:#true hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT hole_:::nil4_4 :: :::nil hole_tuple#25_4 :: tuple#2 gen_#0:#neg:#pos:#s6_4 :: Nat -> #0:#neg:#pos:#s gen_:::nil7_4 :: Nat -> :::nil Lemmas: #compare(gen_#0:#neg:#pos:#s6_4(n9_4), gen_#0:#neg:#pos:#s6_4(n9_4)) -> #EQ, rt in Omega(0) splitD#1(gen_:::nil7_4(n318812_4), gen_#0:#neg:#pos:#s6_4(0)) -> tuple#2(gen_:::nil7_4(n318812_4), gen_:::nil7_4(0)), rt in Omega(1 + n318812_4) split#1(gen_:::nil7_4(n320997_4), gen_#0:#neg:#pos:#s6_4(0)) -> tuple#2(gen_:::nil7_4(n320997_4), gen_:::nil7_4(0)), rt in Omega(1 + n320997_4) appendD#1(gen_:::nil7_4(n323205_4), gen_:::nil7_4(b)) -> gen_:::nil7_4(+(n323205_4, b)), rt in Omega(1 + n323205_4) Generator Equations: gen_#0:#neg:#pos:#s6_4(0) <=> #0 gen_#0:#neg:#pos:#s6_4(+(x, 1)) <=> #neg(gen_#0:#neg:#pos:#s6_4(x)) gen_:::nil7_4(0) <=> nil gen_:::nil7_4(+(x, 1)) <=> ::(#0, gen_:::nil7_4(x)) The following defined symbols remain to be analysed: quicksortD#1, append, append#1, quicksort, quicksort#1, quicksortD They will be analysed ascendingly in the following order: append = append#1 append < quicksort#1 quicksort = quicksort#1 quicksortD = quicksortD#1 ---------------------------------------- (36) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (37) BOUNDS(n^2, INF) ---------------------------------------- (38) Obligation: Innermost TRS: Rules: #abs(#0) -> #0 #abs(#neg(@x)) -> #pos(@x) #abs(#pos(@x)) -> #pos(@x) #abs(#s(@x)) -> #pos(#s(@x)) #greater(@x, @y) -> #ckgt(#compare(@x, @y)) append(@l, @ys) -> append#1(@l, @ys) append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) append#1(nil, @ys) -> @ys appendD(@l, @ys) -> appendD#1(@l, @ys) appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) appendD#1(nil, @ys) -> @ys quicksort(@l) -> quicksort#1(@l) quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) quicksort#1(nil) -> nil quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) quicksortD(@l) -> quicksortD#1(@l) quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) quicksortD#1(nil) -> nil quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) split(@pivot, @l) -> split#1(@l, @pivot) split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) split#1(nil, @pivot) -> tuple#2(nil, nil) split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) split#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) split#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) splitD(@pivot, @l) -> splitD#1(@l, @pivot) splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) splitD#1(nil, @pivot) -> tuple#2(nil, nil) splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) splitD#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) splitD#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) testList -> ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)))))))))) testQuicksort -> quicksort(testList) testQuicksort2 -> quicksort(testList) #ckgt(#EQ) -> #false #ckgt(#GT) -> #true #ckgt(#LT) -> #false #compare(#0, #0) -> #EQ #compare(#0, #neg(@y)) -> #GT #compare(#0, #pos(@y)) -> #LT #compare(#0, #s(@y)) -> #LT #compare(#neg(@x), #0) -> #LT #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) #compare(#neg(@x), #pos(@y)) -> #LT #compare(#pos(@x), #0) -> #GT #compare(#pos(@x), #neg(@y)) -> #GT #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) #compare(#s(@x), #0) -> #GT #compare(#s(@x), #s(@y)) -> #compare(@x, @y) Types: #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 :: :::nil testQuicksort :: :::nil testQuicksort2 :: :::nil #EQ :: #EQ:#GT:#LT #GT :: #EQ:#GT:#LT #LT :: #EQ:#GT:#LT hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s hole_#false:#true2_4 :: #false:#true hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT hole_:::nil4_4 :: :::nil hole_tuple#25_4 :: tuple#2 gen_#0:#neg:#pos:#s6_4 :: Nat -> #0:#neg:#pos:#s gen_:::nil7_4 :: Nat -> :::nil Lemmas: #compare(gen_#0:#neg:#pos:#s6_4(n9_4), gen_#0:#neg:#pos:#s6_4(n9_4)) -> #EQ, rt in Omega(0) splitD#1(gen_:::nil7_4(n318812_4), gen_#0:#neg:#pos:#s6_4(0)) -> tuple#2(gen_:::nil7_4(n318812_4), gen_:::nil7_4(0)), rt in Omega(1 + n318812_4) split#1(gen_:::nil7_4(n320997_4), gen_#0:#neg:#pos:#s6_4(0)) -> tuple#2(gen_:::nil7_4(n320997_4), gen_:::nil7_4(0)), rt in Omega(1 + n320997_4) appendD#1(gen_:::nil7_4(n323205_4), gen_:::nil7_4(b)) -> gen_:::nil7_4(+(n323205_4, b)), rt in Omega(1 + n323205_4) quicksortD#1(gen_:::nil7_4(n324930_4)) -> gen_:::nil7_4(n324930_4), rt in Omega(1 + n324930_4 + n324930_4^2) Generator Equations: gen_#0:#neg:#pos:#s6_4(0) <=> #0 gen_#0:#neg:#pos:#s6_4(+(x, 1)) <=> #neg(gen_#0:#neg:#pos:#s6_4(x)) gen_:::nil7_4(0) <=> nil gen_:::nil7_4(+(x, 1)) <=> ::(#0, gen_:::nil7_4(x)) The following defined symbols remain to be analysed: quicksortD, append, append#1, quicksort, quicksort#1 They will be analysed ascendingly in the following order: append = append#1 append < quicksort#1 quicksort = quicksort#1 quicksortD = quicksortD#1 ---------------------------------------- (39) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: append#1(gen_:::nil7_4(n326285_4), gen_:::nil7_4(b)) -> gen_:::nil7_4(+(n326285_4, b)), rt in Omega(1 + n326285_4) Induction Base: append#1(gen_:::nil7_4(0), gen_:::nil7_4(b)) ->_R^Omega(1) gen_:::nil7_4(b) Induction Step: append#1(gen_:::nil7_4(+(n326285_4, 1)), gen_:::nil7_4(b)) ->_R^Omega(1) ::(#0, append(gen_:::nil7_4(n326285_4), gen_:::nil7_4(b))) ->_R^Omega(1) ::(#0, append#1(gen_:::nil7_4(n326285_4), gen_:::nil7_4(b))) ->_IH ::(#0, gen_:::nil7_4(+(b, c326286_4))) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (40) Obligation: Innermost TRS: Rules: #abs(#0) -> #0 #abs(#neg(@x)) -> #pos(@x) #abs(#pos(@x)) -> #pos(@x) #abs(#s(@x)) -> #pos(#s(@x)) #greater(@x, @y) -> #ckgt(#compare(@x, @y)) append(@l, @ys) -> append#1(@l, @ys) append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) append#1(nil, @ys) -> @ys appendD(@l, @ys) -> appendD#1(@l, @ys) appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) appendD#1(nil, @ys) -> @ys quicksort(@l) -> quicksort#1(@l) quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) quicksort#1(nil) -> nil quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) quicksortD(@l) -> quicksortD#1(@l) quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) quicksortD#1(nil) -> nil quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) split(@pivot, @l) -> split#1(@l, @pivot) split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) split#1(nil, @pivot) -> tuple#2(nil, nil) split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) split#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) split#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) splitD(@pivot, @l) -> splitD#1(@l, @pivot) splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) splitD#1(nil, @pivot) -> tuple#2(nil, nil) splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) splitD#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) splitD#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) testList -> ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)))))))))) testQuicksort -> quicksort(testList) testQuicksort2 -> quicksort(testList) #ckgt(#EQ) -> #false #ckgt(#GT) -> #true #ckgt(#LT) -> #false #compare(#0, #0) -> #EQ #compare(#0, #neg(@y)) -> #GT #compare(#0, #pos(@y)) -> #LT #compare(#0, #s(@y)) -> #LT #compare(#neg(@x), #0) -> #LT #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) #compare(#neg(@x), #pos(@y)) -> #LT #compare(#pos(@x), #0) -> #GT #compare(#pos(@x), #neg(@y)) -> #GT #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) #compare(#s(@x), #0) -> #GT #compare(#s(@x), #s(@y)) -> #compare(@x, @y) Types: #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 :: :::nil testQuicksort :: :::nil testQuicksort2 :: :::nil #EQ :: #EQ:#GT:#LT #GT :: #EQ:#GT:#LT #LT :: #EQ:#GT:#LT hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s hole_#false:#true2_4 :: #false:#true hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT hole_:::nil4_4 :: :::nil hole_tuple#25_4 :: tuple#2 gen_#0:#neg:#pos:#s6_4 :: Nat -> #0:#neg:#pos:#s gen_:::nil7_4 :: Nat -> :::nil Lemmas: #compare(gen_#0:#neg:#pos:#s6_4(n9_4), gen_#0:#neg:#pos:#s6_4(n9_4)) -> #EQ, rt in Omega(0) splitD#1(gen_:::nil7_4(n318812_4), gen_#0:#neg:#pos:#s6_4(0)) -> tuple#2(gen_:::nil7_4(n318812_4), gen_:::nil7_4(0)), rt in Omega(1 + n318812_4) split#1(gen_:::nil7_4(n320997_4), gen_#0:#neg:#pos:#s6_4(0)) -> tuple#2(gen_:::nil7_4(n320997_4), gen_:::nil7_4(0)), rt in Omega(1 + n320997_4) appendD#1(gen_:::nil7_4(n323205_4), gen_:::nil7_4(b)) -> gen_:::nil7_4(+(n323205_4, b)), rt in Omega(1 + n323205_4) quicksortD#1(gen_:::nil7_4(n324930_4)) -> gen_:::nil7_4(n324930_4), rt in Omega(1 + n324930_4 + n324930_4^2) append#1(gen_:::nil7_4(n326285_4), gen_:::nil7_4(b)) -> gen_:::nil7_4(+(n326285_4, b)), rt in Omega(1 + n326285_4) Generator Equations: gen_#0:#neg:#pos:#s6_4(0) <=> #0 gen_#0:#neg:#pos:#s6_4(+(x, 1)) <=> #neg(gen_#0:#neg:#pos:#s6_4(x)) gen_:::nil7_4(0) <=> nil gen_:::nil7_4(+(x, 1)) <=> ::(#0, gen_:::nil7_4(x)) The following defined symbols remain to be analysed: append, quicksort, quicksort#1 They will be analysed ascendingly in the following order: append = append#1 append < quicksort#1 quicksort = quicksort#1 ---------------------------------------- (41) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: quicksort#1(gen_:::nil7_4(n328054_4)) -> gen_:::nil7_4(n328054_4), rt in Omega(1 + n328054_4 + n328054_4^2) Induction Base: quicksort#1(gen_:::nil7_4(0)) ->_R^Omega(1) nil Induction Step: quicksort#1(gen_:::nil7_4(+(n328054_4, 1))) ->_R^Omega(1) quicksort#2(split(#0, gen_:::nil7_4(n328054_4)), #0) ->_R^Omega(1) quicksort#2(split#1(gen_:::nil7_4(n328054_4), #0), #0) ->_L^Omega(1 + n328054_4) quicksort#2(tuple#2(gen_:::nil7_4(n328054_4), gen_:::nil7_4(0)), #0) ->_R^Omega(1) append(quicksort(gen_:::nil7_4(n328054_4)), ::(#0, quicksort(gen_:::nil7_4(0)))) ->_R^Omega(1) append(quicksort#1(gen_:::nil7_4(n328054_4)), ::(#0, quicksort(gen_:::nil7_4(0)))) ->_IH append(gen_:::nil7_4(c328055_4), ::(#0, quicksort(gen_:::nil7_4(0)))) ->_R^Omega(1) append(gen_:::nil7_4(n328054_4), ::(#0, quicksort#1(gen_:::nil7_4(0)))) ->_R^Omega(1) append(gen_:::nil7_4(n328054_4), ::(#0, nil)) ->_R^Omega(1) append#1(gen_:::nil7_4(n328054_4), ::(#0, nil)) ->_L^Omega(1 + n328054_4) gen_:::nil7_4(+(n328054_4, +(0, 1))) We have rt in Omega(n^2) and sz in O(n). Thus, we have irc_R in Omega(n^2). ---------------------------------------- (42) Obligation: Innermost TRS: Rules: #abs(#0) -> #0 #abs(#neg(@x)) -> #pos(@x) #abs(#pos(@x)) -> #pos(@x) #abs(#s(@x)) -> #pos(#s(@x)) #greater(@x, @y) -> #ckgt(#compare(@x, @y)) append(@l, @ys) -> append#1(@l, @ys) append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) append#1(nil, @ys) -> @ys appendD(@l, @ys) -> appendD#1(@l, @ys) appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) appendD#1(nil, @ys) -> @ys quicksort(@l) -> quicksort#1(@l) quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) quicksort#1(nil) -> nil quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) quicksortD(@l) -> quicksortD#1(@l) quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) quicksortD#1(nil) -> nil quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) split(@pivot, @l) -> split#1(@l, @pivot) split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) split#1(nil, @pivot) -> tuple#2(nil, nil) split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) split#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) split#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) splitD(@pivot, @l) -> splitD#1(@l, @pivot) splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) splitD#1(nil, @pivot) -> tuple#2(nil, nil) splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) splitD#3(#false, @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) splitD#3(#true, @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) testList -> ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)))))))))) testQuicksort -> quicksort(testList) testQuicksort2 -> quicksort(testList) #ckgt(#EQ) -> #false #ckgt(#GT) -> #true #ckgt(#LT) -> #false #compare(#0, #0) -> #EQ #compare(#0, #neg(@y)) -> #GT #compare(#0, #pos(@y)) -> #LT #compare(#0, #s(@y)) -> #LT #compare(#neg(@x), #0) -> #LT #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) #compare(#neg(@x), #pos(@y)) -> #LT #compare(#pos(@x), #0) -> #GT #compare(#pos(@x), #neg(@y)) -> #GT #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) #compare(#s(@x), #0) -> #GT #compare(#s(@x), #s(@y)) -> #compare(@x, @y) Types: #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 :: :::nil testQuicksort :: :::nil testQuicksort2 :: :::nil #EQ :: #EQ:#GT:#LT #GT :: #EQ:#GT:#LT #LT :: #EQ:#GT:#LT hole_#0:#neg:#pos:#s1_4 :: #0:#neg:#pos:#s hole_#false:#true2_4 :: #false:#true hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT hole_:::nil4_4 :: :::nil hole_tuple#25_4 :: tuple#2 gen_#0:#neg:#pos:#s6_4 :: Nat -> #0:#neg:#pos:#s gen_:::nil7_4 :: Nat -> :::nil Lemmas: #compare(gen_#0:#neg:#pos:#s6_4(n9_4), gen_#0:#neg:#pos:#s6_4(n9_4)) -> #EQ, rt in Omega(0) splitD#1(gen_:::nil7_4(n318812_4), gen_#0:#neg:#pos:#s6_4(0)) -> tuple#2(gen_:::nil7_4(n318812_4), gen_:::nil7_4(0)), rt in Omega(1 + n318812_4) split#1(gen_:::nil7_4(n320997_4), gen_#0:#neg:#pos:#s6_4(0)) -> tuple#2(gen_:::nil7_4(n320997_4), gen_:::nil7_4(0)), rt in Omega(1 + n320997_4) appendD#1(gen_:::nil7_4(n323205_4), gen_:::nil7_4(b)) -> gen_:::nil7_4(+(n323205_4, b)), rt in Omega(1 + n323205_4) quicksortD#1(gen_:::nil7_4(n324930_4)) -> gen_:::nil7_4(n324930_4), rt in Omega(1 + n324930_4 + n324930_4^2) append#1(gen_:::nil7_4(n326285_4), gen_:::nil7_4(b)) -> gen_:::nil7_4(+(n326285_4, b)), rt in Omega(1 + n326285_4) quicksort#1(gen_:::nil7_4(n328054_4)) -> gen_:::nil7_4(n328054_4), rt in Omega(1 + n328054_4 + n328054_4^2) Generator Equations: gen_#0:#neg:#pos:#s6_4(0) <=> #0 gen_#0:#neg:#pos:#s6_4(+(x, 1)) <=> #neg(gen_#0:#neg:#pos:#s6_4(x)) gen_:::nil7_4(0) <=> nil gen_:::nil7_4(+(x, 1)) <=> ::(#0, gen_:::nil7_4(x)) The following defined symbols remain to be analysed: quicksort They will be analysed ascendingly in the following order: quicksort = quicksort#1