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

(0) Obligation:

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


The TRS R consists of the following rules:

#less(@x, @y) → #cklt(#compare(@x, @y))
findMin(@l) → findMin#1(@l)
findMin#1(::(@x, @xs)) → findMin#2(findMin(@xs), @x)
findMin#1(nil) → nil
findMin#2(::(@y, @ys), @x) → findMin#3(#less(@x, @y), @x, @y, @ys)
findMin#2(nil, @x) → ::(@x, nil)
findMin#3(#false, @x, @y, @ys) → ::(@y, ::(@x, @ys))
findMin#3(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
minSort(@l) → minSort#1(findMin(@l))
minSort#1(::(@x, @xs)) → ::(@x, minSort(@xs))
minSort#1(nil) → nil

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

#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#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) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed relative TRS to weighted TRS

(2) Obligation:

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


The TRS R consists of the following rules:

#less(@x, @y) → #cklt(#compare(@x, @y)) [1]
findMin(@l) → findMin#1(@l) [1]
findMin#1(::(@x, @xs)) → findMin#2(findMin(@xs), @x) [1]
findMin#1(nil) → nil [1]
findMin#2(::(@y, @ys), @x) → findMin#3(#less(@x, @y), @x, @y, @ys) [1]
findMin#2(nil, @x) → ::(@x, nil) [1]
findMin#3(#false, @x, @y, @ys) → ::(@y, ::(@x, @ys)) [1]
findMin#3(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys)) [1]
minSort(@l) → minSort#1(findMin(@l)) [1]
minSort#1(::(@x, @xs)) → ::(@x, minSort(@xs)) [1]
minSort#1(nil) → nil [1]
#cklt(#EQ) → #false [0]
#cklt(#GT) → #false [0]
#cklt(#LT) → #true [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

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

Infered types.

(4) Obligation:

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

#less(@x, @y) → #cklt(#compare(@x, @y)) [1]
findMin(@l) → findMin#1(@l) [1]
findMin#1(::(@x, @xs)) → findMin#2(findMin(@xs), @x) [1]
findMin#1(nil) → nil [1]
findMin#2(::(@y, @ys), @x) → findMin#3(#less(@x, @y), @x, @y, @ys) [1]
findMin#2(nil, @x) → ::(@x, nil) [1]
findMin#3(#false, @x, @y, @ys) → ::(@y, ::(@x, @ys)) [1]
findMin#3(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys)) [1]
minSort(@l) → minSort#1(findMin(@l)) [1]
minSort#1(::(@x, @xs)) → ::(@x, minSort(@xs)) [1]
minSort#1(nil) → nil [1]
#cklt(#EQ) → #false [0]
#cklt(#GT) → #false [0]
#cklt(#LT) → #true [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:

#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true #cklt :: #EQ:#GT:#LT → #false:#true #compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT findMin :: :::nil → :::nil findMin#1 :: :::nil → :::nil :: :: #0:#neg:#pos:#s → :::nil → :::nil findMin#2 :: :::nil → #0:#neg:#pos:#s → :::nil nil :: :::nil findMin#3 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil #false :: #false:#true #true :: #false:#true minSort :: :::nil → :::nil minSort#1 :: :::nil → :::nil #EQ :: #EQ:#GT:#LT #GT :: #EQ:#GT:#LT #LT :: #EQ:#GT:#LT #0 :: #0:#neg:#pos:#s #neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s #pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s #s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s

Rewrite Strategy: INNERMOST

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

The transformation into a RNTS is sound, since:

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

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

minSort
minSort#1

(c) The following functions are completely defined:

#less
findMin
findMin#1
findMin#2
findMin#3
#cklt
#compare

Due to the following rules being added:

#cklt(v0) → null_#cklt [0]
#compare(v0, v1) → null_#compare [0]
findMin#3(v0, v1, v2, v3) → nil [0]

And the following fresh constants:

null_#cklt, null_#compare

(6) Obligation:

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

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: #less(@x, @y) → #cklt(#compare(@x, @y)) [1] findMin(@l) → findMin#1(@l) [1] findMin#1(::(@x, @xs)) → findMin#2(findMin(@xs), @x) [1] findMin#1(nil) → nil [1] findMin#2(::(@y, @ys), @x) → findMin#3(#less(@x, @y), @x, @y, @ys) [1] findMin#2(nil, @x) → ::(@x, nil) [1] findMin#3(#false, @x, @y, @ys) → ::(@y, ::(@x, @ys)) [1] findMin#3(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys)) [1] minSort(@l) → minSort#1(findMin(@l)) [1] minSort#1(::(@x, @xs)) → ::(@x, minSort(@xs)) [1] minSort#1(nil) → nil [1] #cklt(#EQ) → #false [0] #cklt(#GT) → #false [0] #cklt(#LT) → #true [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] #cklt(v0) → null_#cklt [0] #compare(v0, v1) → null_#compare [0] findMin#3(v0, v1, v2, v3) → nil [0] The TRS has the following type information: #less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true:null_#cklt #cklt :: #EQ:#GT:#LT:null_#compare → #false:#true:null_#cklt #compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT:null_#compare findMin :: :::nil → :::nil findMin#1 :: :::nil → :::nil :: :: #0:#neg:#pos:#s → :::nil → :::nil findMin#2 :: :::nil → #0:#neg:#pos:#s → :::nil nil :: :::nil findMin#3 :: #false:#true:null_#cklt → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil #false :: #false:#true:null_#cklt #true :: #false:#true:null_#cklt minSort :: :::nil → :::nil minSort#1 :: :::nil → :::nil #EQ :: #EQ:#GT:#LT:null_#compare #GT :: #EQ:#GT:#LT:null_#compare #LT :: #EQ:#GT:#LT:null_#compare #0 :: #0:#neg:#pos:#s #neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s #pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s #s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s null_#cklt :: #false:#true:null_#cklt null_#compare :: #EQ:#GT:#LT:null_#compare Rewrite Strategy: INNERMOST

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

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

(8) Obligation:

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

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: #less(#0, #0) → #cklt(#EQ) [1] #less(#0, #neg(@y')) → #cklt(#GT) [1] #less(#0, #pos(@y'')) → #cklt(#LT) [1] #less(#0, #s(@y1)) → #cklt(#LT) [1] #less(#neg(@x'), #0) → #cklt(#LT) [1] #less(#neg(@x''), #neg(@y2)) → #cklt(#compare(@y2, @x'')) [1] #less(#neg(@x1), #pos(@y3)) → #cklt(#LT) [1] #less(#pos(@x2), #0) → #cklt(#GT) [1] #less(#pos(@x3), #neg(@y4)) → #cklt(#GT) [1] #less(#pos(@x4), #pos(@y5)) → #cklt(#compare(@x4, @y5)) [1] #less(#s(@x5), #0) → #cklt(#GT) [1] #less(#s(@x6), #s(@y6)) → #cklt(#compare(@x6, @y6)) [1] #less(@x, @y) → #cklt(null_#compare) [1] findMin(@l) → findMin#1(@l) [1] findMin#1(::(@x, @xs)) → findMin#2(findMin#1(@xs), @x) [2] findMin#1(nil) → nil [1] findMin#2(::(@y, @ys), @x) → findMin#3(#cklt(#compare(@x, @y)), @x, @y, @ys) [2] findMin#2(nil, @x) → ::(@x, nil) [1] findMin#3(#false, @x, @y, @ys) → ::(@y, ::(@x, @ys)) [1] findMin#3(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys)) [1] minSort(@l) → minSort#1(findMin#1(@l)) [2] minSort#1(::(@x, @xs)) → ::(@x, minSort(@xs)) [1] minSort#1(nil) → nil [1] #cklt(#EQ) → #false [0] #cklt(#GT) → #false [0] #cklt(#LT) → #true [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] #cklt(v0) → null_#cklt [0] #compare(v0, v1) → null_#compare [0] findMin#3(v0, v1, v2, v3) → nil [0] The TRS has the following type information: #less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true:null_#cklt #cklt :: #EQ:#GT:#LT:null_#compare → #false:#true:null_#cklt #compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT:null_#compare findMin :: :::nil → :::nil findMin#1 :: :::nil → :::nil :: :: #0:#neg:#pos:#s → :::nil → :::nil findMin#2 :: :::nil → #0:#neg:#pos:#s → :::nil nil :: :::nil findMin#3 :: #false:#true:null_#cklt → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil #false :: #false:#true:null_#cklt #true :: #false:#true:null_#cklt minSort :: :::nil → :::nil minSort#1 :: :::nil → :::nil #EQ :: #EQ:#GT:#LT:null_#compare #GT :: #EQ:#GT:#LT:null_#compare #LT :: #EQ:#GT:#LT:null_#compare #0 :: #0:#neg:#pos:#s #neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s #pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s #s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s null_#cklt :: #false:#true:null_#cklt null_#compare :: #EQ:#GT:#LT:null_#compare Rewrite Strategy: INNERMOST

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

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

nil => 0
#false => 1
#true => 2
#EQ => 1
#GT => 2
#LT => 3
#0 => 0
null_#cklt => 0
null_#compare => 0

(10) Obligation:

Complexity RNTS consisting of the following rules:

#cklt(z) -{ 0 }→ 2 :|: z = 3
#cklt(z) -{ 0 }→ 1 :|: z = 1
#cklt(z) -{ 0 }→ 1 :|: z = 2
#cklt(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
#less(z, z') -{ 1 }→ #cklt(3) :|: z' = 1 + @y'', @y'' >= 0, z = 0
#less(z, z') -{ 1 }→ #cklt(3) :|: z' = 1 + @y1, @y1 >= 0, z = 0
#less(z, z') -{ 1 }→ #cklt(3) :|: z = 1 + @x', @x' >= 0, z' = 0
#less(z, z') -{ 1 }→ #cklt(3) :|: @y3 >= 0, @x1 >= 0, z' = 1 + @y3, z = 1 + @x1
#less(z, z') -{ 1 }→ #cklt(2) :|: @y' >= 0, z' = 1 + @y', z = 0
#less(z, z') -{ 1 }→ #cklt(2) :|: @x2 >= 0, z = 1 + @x2, z' = 0
#less(z, z') -{ 1 }→ #cklt(2) :|: @x3 >= 0, z' = 1 + @y4, z = 1 + @x3, @y4 >= 0
#less(z, z') -{ 1 }→ #cklt(2) :|: z = 1 + @x5, @x5 >= 0, z' = 0
#less(z, z') -{ 1 }→ #cklt(1) :|: z = 0, z' = 0
#less(z, z') -{ 1 }→ #cklt(0) :|: z = @x, @x >= 0, z' = @y, @y >= 0
#less(z, z') -{ 1 }→ #cklt(#compare(@x4, @y5)) :|: z' = 1 + @y5, @y5 >= 0, z = 1 + @x4, @x4 >= 0
#less(z, z') -{ 1 }→ #cklt(#compare(@x6, @y6)) :|: z = 1 + @x6, z' = 1 + @y6, @x6 >= 0, @y6 >= 0
#less(z, z') -{ 1 }→ #cklt(#compare(@y2, @x'')) :|: z = 1 + @x'', z' = 1 + @y2, @y2 >= 0, @x'' >= 0
findMin(z) -{ 1 }→ findMin#1(@l) :|: z = @l, @l >= 0
findMin#1(z) -{ 2 }→ findMin#2(findMin#1(@xs), @x) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0
findMin#1(z) -{ 1 }→ 0 :|: z = 0
findMin#2(z, z') -{ 2 }→ findMin#3(#cklt(#compare(@x, @y)), @x, @y, @ys) :|: z = 1 + @y + @ys, @x >= 0, @y >= 0, z' = @x, @ys >= 0
findMin#2(z, z') -{ 1 }→ 1 + @x + 0 :|: @x >= 0, z = 0, z' = @x
findMin#3(z, z', z'', z1) -{ 0 }→ 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + @x + (1 + @y + @ys) :|: z = 2, @x >= 0, z1 = @ys, @y >= 0, z' = @x, @ys >= 0, z'' = @y
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + @y + (1 + @x + @ys) :|: @x >= 0, z = 1, z1 = @ys, @y >= 0, z' = @x, @ys >= 0, z'' = @y
minSort(z) -{ 2 }→ minSort#1(findMin#1(@l)) :|: z = @l, @l >= 0
minSort#1(z) -{ 1 }→ 0 :|: z = 0
minSort#1(z) -{ 1 }→ 1 + @x + minSort(@xs) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0

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

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

findMin#3(z, z', z'', z1) -{ 1 }→ 1 + @y + (1 + @x + @ys) :|: @x >= 0, z = 1, z1 = @ys, @y >= 0, z' = @x, @ys >= 0, z'' = @y
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + @x + (1 + @y + @ys) :|: z = 2, @x >= 0, z1 = @ys, @y >= 0, z' = @x, @ys >= 0, z'' = @y
findMin#3(z, z', z'', z1) -{ 0 }→ 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
#cklt(z) -{ 0 }→ 1 :|: z = 1
#cklt(z) -{ 0 }→ 1 :|: z = 2
#cklt(z) -{ 0 }→ 2 :|: z = 3
#cklt(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0

(12) Obligation:

Complexity RNTS consisting of the following rules:

#cklt(z) -{ 0 }→ 2 :|: z = 3
#cklt(z) -{ 0 }→ 1 :|: z = 1
#cklt(z) -{ 0 }→ 1 :|: z = 2
#cklt(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
#less(z, z') -{ 1 }→ 2 :|: z' = 1 + @y'', @y'' >= 0, z = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z' = 1 + @y1, @y1 >= 0, z = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z = 1 + @x', @x' >= 0, z' = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: @y3 >= 0, @x1 >= 0, z' = 1 + @y3, z = 1 + @x1, 3 = 3
#less(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0, 1 = 1
#less(z, z') -{ 1 }→ 1 :|: @y' >= 0, z' = 1 + @y', z = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: @x2 >= 0, z = 1 + @x2, z' = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: @x3 >= 0, z' = 1 + @y4, z = 1 + @x3, @y4 >= 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z = 1 + @x5, @x5 >= 0, z' = 0, 2 = 2
#less(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0, v0 >= 0, 1 = v0
#less(z, z') -{ 1 }→ 0 :|: @y' >= 0, z' = 1 + @y', z = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z' = 1 + @y'', @y'' >= 0, z = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z' = 1 + @y1, @y1 >= 0, z = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z = 1 + @x', @x' >= 0, z' = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: @y3 >= 0, @x1 >= 0, z' = 1 + @y3, z = 1 + @x1, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: @x2 >= 0, z = 1 + @x2, z' = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: @x3 >= 0, z' = 1 + @y4, z = 1 + @x3, @y4 >= 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z = 1 + @x5, @x5 >= 0, z' = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z = @x, @x >= 0, z' = @y, @y >= 0, v0 >= 0, 0 = v0
#less(z, z') -{ 1 }→ #cklt(#compare(@x4, @y5)) :|: z' = 1 + @y5, @y5 >= 0, z = 1 + @x4, @x4 >= 0
#less(z, z') -{ 1 }→ #cklt(#compare(@x6, @y6)) :|: z = 1 + @x6, z' = 1 + @y6, @x6 >= 0, @y6 >= 0
#less(z, z') -{ 1 }→ #cklt(#compare(@y2, @x'')) :|: z = 1 + @x'', z' = 1 + @y2, @y2 >= 0, @x'' >= 0
findMin(z) -{ 1 }→ findMin#1(@l) :|: z = @l, @l >= 0
findMin#1(z) -{ 2 }→ findMin#2(findMin#1(@xs), @x) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0
findMin#1(z) -{ 1 }→ 0 :|: z = 0
findMin#2(z, z') -{ 2 }→ findMin#3(#cklt(#compare(@x, @y)), @x, @y, @ys) :|: z = 1 + @y + @ys, @x >= 0, @y >= 0, z' = @x, @ys >= 0
findMin#2(z, z') -{ 1 }→ 1 + @x + 0 :|: @x >= 0, z = 0, z' = @x
findMin#3(z, z', z'', z1) -{ 0 }→ 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + @x + (1 + @y + @ys) :|: z = 2, @x >= 0, z1 = @ys, @y >= 0, z' = @x, @ys >= 0, z'' = @y
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + @y + (1 + @x + @ys) :|: @x >= 0, z = 1, z1 = @ys, @y >= 0, z' = @x, @ys >= 0, z'' = @y
minSort(z) -{ 2 }→ minSort#1(findMin#1(@l)) :|: z = @l, @l >= 0
minSort#1(z) -{ 1 }→ 0 :|: z = 0
minSort#1(z) -{ 1 }→ 1 + @x + minSort(@xs) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0

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

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

(14) Obligation:

Complexity RNTS consisting of the following rules:

#cklt(z) -{ 0 }→ 2 :|: z = 3
#cklt(z) -{ 0 }→ 1 :|: z = 1
#cklt(z) -{ 0 }→ 1 :|: z = 2
#cklt(z) -{ 0 }→ 0 :|: z >= 0
#compare(z, z') -{ 0 }→ 3 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
#compare(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
#compare(z, z') -{ 0 }→ #compare(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ #compare(z' - 1, z - 1) :|: z - 1 >= 0, z' - 1 >= 0
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z - 1 >= 0, z' = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z - 1 >= 0, 3 = 3
#less(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0, 1 = 1
#less(z, z') -{ 1 }→ 1 :|: z' - 1 >= 0, z = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' - 1 >= 0, 2 = 2
#less(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0, v0 >= 0, 1 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z - 1 >= 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' - 1 >= 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z >= 0, z' >= 0, v0 >= 0, 0 = v0
#less(z, z') -{ 1 }→ #cklt(#compare(z - 1, z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ #cklt(#compare(z' - 1, z - 1)) :|: z' - 1 >= 0, z - 1 >= 0
findMin(z) -{ 1 }→ findMin#1(z) :|: z >= 0
findMin#1(z) -{ 2 }→ findMin#2(findMin#1(@xs), @x) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0
findMin#1(z) -{ 1 }→ 0 :|: z = 0
findMin#2(z, z') -{ 2 }→ findMin#3(#cklt(#compare(z', @y)), z', @y, @ys) :|: z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
findMin#2(z, z') -{ 1 }→ 1 + z' + 0 :|: z' >= 0, z = 0
findMin#3(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z' + (1 + z'' + z1) :|: z = 2, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z'' + (1 + z' + z1) :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
minSort(z) -{ 2 }→ minSort#1(findMin#1(z)) :|: z >= 0
minSort#1(z) -{ 1 }→ 0 :|: z = 0
minSort#1(z) -{ 1 }→ 1 + @x + minSort(@xs) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0

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

Found the following analysis order by SCC decomposition:

{ #compare } { findMin#3 } { #cklt } { #less } { findMin#2 } { findMin#1 } { minSort#1, minSort } { findMin }

(16) Obligation:

Complexity RNTS consisting of the following rules:

#cklt(z) -{ 0 }→ 2 :|: z = 3
#cklt(z) -{ 0 }→ 1 :|: z = 1
#cklt(z) -{ 0 }→ 1 :|: z = 2
#cklt(z) -{ 0 }→ 0 :|: z >= 0
#compare(z, z') -{ 0 }→ 3 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
#compare(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
#compare(z, z') -{ 0 }→ #compare(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ #compare(z' - 1, z - 1) :|: z - 1 >= 0, z' - 1 >= 0
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z - 1 >= 0, z' = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z - 1 >= 0, 3 = 3
#less(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0, 1 = 1
#less(z, z') -{ 1 }→ 1 :|: z' - 1 >= 0, z = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' - 1 >= 0, 2 = 2
#less(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0, v0 >= 0, 1 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z - 1 >= 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' - 1 >= 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z >= 0, z' >= 0, v0 >= 0, 0 = v0
#less(z, z') -{ 1 }→ #cklt(#compare(z - 1, z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ #cklt(#compare(z' - 1, z - 1)) :|: z' - 1 >= 0, z - 1 >= 0
findMin(z) -{ 1 }→ findMin#1(z) :|: z >= 0
findMin#1(z) -{ 2 }→ findMin#2(findMin#1(@xs), @x) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0
findMin#1(z) -{ 1 }→ 0 :|: z = 0
findMin#2(z, z') -{ 2 }→ findMin#3(#cklt(#compare(z', @y)), z', @y, @ys) :|: z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
findMin#2(z, z') -{ 1 }→ 1 + z' + 0 :|: z' >= 0, z = 0
findMin#3(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z' + (1 + z'' + z1) :|: z = 2, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z'' + (1 + z' + z1) :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
minSort(z) -{ 2 }→ minSort#1(findMin#1(z)) :|: z >= 0
minSort#1(z) -{ 1 }→ 0 :|: z = 0
minSort#1(z) -{ 1 }→ 1 + @x + minSort(@xs) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0

Function symbols to be analyzed: {#compare}, {findMin#3}, {#cklt}, {#less}, {findMin#2}, {findMin#1}, {minSort#1,minSort}, {findMin}

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

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

(18) Obligation:

Complexity RNTS consisting of the following rules:

#cklt(z) -{ 0 }→ 2 :|: z = 3
#cklt(z) -{ 0 }→ 1 :|: z = 1
#cklt(z) -{ 0 }→ 1 :|: z = 2
#cklt(z) -{ 0 }→ 0 :|: z >= 0
#compare(z, z') -{ 0 }→ 3 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
#compare(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
#compare(z, z') -{ 0 }→ #compare(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ #compare(z' - 1, z - 1) :|: z - 1 >= 0, z' - 1 >= 0
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z - 1 >= 0, z' = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z - 1 >= 0, 3 = 3
#less(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0, 1 = 1
#less(z, z') -{ 1 }→ 1 :|: z' - 1 >= 0, z = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' - 1 >= 0, 2 = 2
#less(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0, v0 >= 0, 1 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z - 1 >= 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' - 1 >= 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z >= 0, z' >= 0, v0 >= 0, 0 = v0
#less(z, z') -{ 1 }→ #cklt(#compare(z - 1, z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ #cklt(#compare(z' - 1, z - 1)) :|: z' - 1 >= 0, z - 1 >= 0
findMin(z) -{ 1 }→ findMin#1(z) :|: z >= 0
findMin#1(z) -{ 2 }→ findMin#2(findMin#1(@xs), @x) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0
findMin#1(z) -{ 1 }→ 0 :|: z = 0
findMin#2(z, z') -{ 2 }→ findMin#3(#cklt(#compare(z', @y)), z', @y, @ys) :|: z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
findMin#2(z, z') -{ 1 }→ 1 + z' + 0 :|: z' >= 0, z = 0
findMin#3(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z' + (1 + z'' + z1) :|: z = 2, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z'' + (1 + z' + z1) :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
minSort(z) -{ 2 }→ minSort#1(findMin#1(z)) :|: z >= 0
minSort#1(z) -{ 1 }→ 0 :|: z = 0
minSort#1(z) -{ 1 }→ 1 + @x + minSort(@xs) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0

Function symbols to be analyzed: {#compare}, {findMin#3}, {#cklt}, {#less}, {findMin#2}, {findMin#1}, {minSort#1,minSort}, {findMin}
Previous analysis results are:

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

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

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

(20) Obligation:

Complexity RNTS consisting of the following rules:

#cklt(z) -{ 0 }→ 2 :|: z = 3
#cklt(z) -{ 0 }→ 1 :|: z = 1
#cklt(z) -{ 0 }→ 1 :|: z = 2
#cklt(z) -{ 0 }→ 0 :|: z >= 0
#compare(z, z') -{ 0 }→ 3 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
#compare(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
#compare(z, z') -{ 0 }→ #compare(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ #compare(z' - 1, z - 1) :|: z - 1 >= 0, z' - 1 >= 0
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z - 1 >= 0, z' = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z - 1 >= 0, 3 = 3
#less(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0, 1 = 1
#less(z, z') -{ 1 }→ 1 :|: z' - 1 >= 0, z = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' - 1 >= 0, 2 = 2
#less(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0, v0 >= 0, 1 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z - 1 >= 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' - 1 >= 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z >= 0, z' >= 0, v0 >= 0, 0 = v0
#less(z, z') -{ 1 }→ #cklt(#compare(z - 1, z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ #cklt(#compare(z' - 1, z - 1)) :|: z' - 1 >= 0, z - 1 >= 0
findMin(z) -{ 1 }→ findMin#1(z) :|: z >= 0
findMin#1(z) -{ 2 }→ findMin#2(findMin#1(@xs), @x) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0
findMin#1(z) -{ 1 }→ 0 :|: z = 0
findMin#2(z, z') -{ 2 }→ findMin#3(#cklt(#compare(z', @y)), z', @y, @ys) :|: z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
findMin#2(z, z') -{ 1 }→ 1 + z' + 0 :|: z' >= 0, z = 0
findMin#3(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z' + (1 + z'' + z1) :|: z = 2, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z'' + (1 + z' + z1) :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
minSort(z) -{ 2 }→ minSort#1(findMin#1(z)) :|: z >= 0
minSort#1(z) -{ 1 }→ 0 :|: z = 0
minSort#1(z) -{ 1 }→ 1 + @x + minSort(@xs) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0

Function symbols to be analyzed: {findMin#3}, {#cklt}, {#less}, {findMin#2}, {findMin#1}, {minSort#1,minSort}, {findMin}
Previous analysis results are:

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

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

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

(22) Obligation:

Complexity RNTS consisting of the following rules:

#cklt(z) -{ 0 }→ 2 :|: z = 3
#cklt(z) -{ 0 }→ 1 :|: z = 1
#cklt(z) -{ 0 }→ 1 :|: z = 2
#cklt(z) -{ 0 }→ 0 :|: z >= 0
#compare(z, z') -{ 0 }→ s :|: s >= 0, s <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ s' :|: s' >= 0, s' <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
#compare(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z - 1 >= 0, z' = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z - 1 >= 0, 3 = 3
#less(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0, 1 = 1
#less(z, z') -{ 1 }→ 1 :|: z' - 1 >= 0, z = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' - 1 >= 0, 2 = 2
#less(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0, v0 >= 0, 1 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z - 1 >= 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' - 1 >= 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z >= 0, z' >= 0, v0 >= 0, 0 = v0
#less(z, z') -{ 1 }→ #cklt(s'') :|: s'' >= 0, s'' <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ #cklt(s1) :|: s1 >= 0, s1 <= 3, z' - 1 >= 0, z - 1 >= 0
findMin(z) -{ 1 }→ findMin#1(z) :|: z >= 0
findMin#1(z) -{ 2 }→ findMin#2(findMin#1(@xs), @x) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0
findMin#1(z) -{ 1 }→ 0 :|: z = 0
findMin#2(z, z') -{ 2 }→ findMin#3(#cklt(s2), z', @y, @ys) :|: s2 >= 0, s2 <= 3, z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
findMin#2(z, z') -{ 1 }→ 1 + z' + 0 :|: z' >= 0, z = 0
findMin#3(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z' + (1 + z'' + z1) :|: z = 2, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z'' + (1 + z' + z1) :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
minSort(z) -{ 2 }→ minSort#1(findMin#1(z)) :|: z >= 0
minSort#1(z) -{ 1 }→ 0 :|: z = 0
minSort#1(z) -{ 1 }→ 1 + @x + minSort(@xs) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0

Function symbols to be analyzed: {findMin#3}, {#cklt}, {#less}, {findMin#2}, {findMin#1}, {minSort#1,minSort}, {findMin}
Previous analysis results are:

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

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

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

(24) Obligation:

Complexity RNTS consisting of the following rules:

#cklt(z) -{ 0 }→ 2 :|: z = 3
#cklt(z) -{ 0 }→ 1 :|: z = 1
#cklt(z) -{ 0 }→ 1 :|: z = 2
#cklt(z) -{ 0 }→ 0 :|: z >= 0
#compare(z, z') -{ 0 }→ s :|: s >= 0, s <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ s' :|: s' >= 0, s' <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
#compare(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z - 1 >= 0, z' = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z - 1 >= 0, 3 = 3
#less(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0, 1 = 1
#less(z, z') -{ 1 }→ 1 :|: z' - 1 >= 0, z = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' - 1 >= 0, 2 = 2
#less(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0, v0 >= 0, 1 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z - 1 >= 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' - 1 >= 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z >= 0, z' >= 0, v0 >= 0, 0 = v0
#less(z, z') -{ 1 }→ #cklt(s'') :|: s'' >= 0, s'' <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ #cklt(s1) :|: s1 >= 0, s1 <= 3, z' - 1 >= 0, z - 1 >= 0
findMin(z) -{ 1 }→ findMin#1(z) :|: z >= 0
findMin#1(z) -{ 2 }→ findMin#2(findMin#1(@xs), @x) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0
findMin#1(z) -{ 1 }→ 0 :|: z = 0
findMin#2(z, z') -{ 2 }→ findMin#3(#cklt(s2), z', @y, @ys) :|: s2 >= 0, s2 <= 3, z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
findMin#2(z, z') -{ 1 }→ 1 + z' + 0 :|: z' >= 0, z = 0
findMin#3(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z' + (1 + z'' + z1) :|: z = 2, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z'' + (1 + z' + z1) :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
minSort(z) -{ 2 }→ minSort#1(findMin#1(z)) :|: z >= 0
minSort#1(z) -{ 1 }→ 0 :|: z = 0
minSort#1(z) -{ 1 }→ 1 + @x + minSort(@xs) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0

Function symbols to be analyzed: {findMin#3}, {#cklt}, {#less}, {findMin#2}, {findMin#1}, {minSort#1,minSort}, {findMin}
Previous analysis results are:

#compare: runtime: O(1) [0], size: O(1) [3] findMin#3: runtime: ?, size: O(n1) [2 + z' + z'' + z1]

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

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

(26) Obligation:

Complexity RNTS consisting of the following rules:

#cklt(z) -{ 0 }→ 2 :|: z = 3
#cklt(z) -{ 0 }→ 1 :|: z = 1
#cklt(z) -{ 0 }→ 1 :|: z = 2
#cklt(z) -{ 0 }→ 0 :|: z >= 0
#compare(z, z') -{ 0 }→ s :|: s >= 0, s <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ s' :|: s' >= 0, s' <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
#compare(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z - 1 >= 0, z' = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z - 1 >= 0, 3 = 3
#less(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0, 1 = 1
#less(z, z') -{ 1 }→ 1 :|: z' - 1 >= 0, z = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' - 1 >= 0, 2 = 2
#less(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0, v0 >= 0, 1 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z - 1 >= 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' - 1 >= 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z >= 0, z' >= 0, v0 >= 0, 0 = v0
#less(z, z') -{ 1 }→ #cklt(s'') :|: s'' >= 0, s'' <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ #cklt(s1) :|: s1 >= 0, s1 <= 3, z' - 1 >= 0, z - 1 >= 0
findMin(z) -{ 1 }→ findMin#1(z) :|: z >= 0
findMin#1(z) -{ 2 }→ findMin#2(findMin#1(@xs), @x) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0
findMin#1(z) -{ 1 }→ 0 :|: z = 0
findMin#2(z, z') -{ 2 }→ findMin#3(#cklt(s2), z', @y, @ys) :|: s2 >= 0, s2 <= 3, z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
findMin#2(z, z') -{ 1 }→ 1 + z' + 0 :|: z' >= 0, z = 0
findMin#3(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z' + (1 + z'' + z1) :|: z = 2, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z'' + (1 + z' + z1) :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
minSort(z) -{ 2 }→ minSort#1(findMin#1(z)) :|: z >= 0
minSort#1(z) -{ 1 }→ 0 :|: z = 0
minSort#1(z) -{ 1 }→ 1 + @x + minSort(@xs) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0

Function symbols to be analyzed: {#cklt}, {#less}, {findMin#2}, {findMin#1}, {minSort#1,minSort}, {findMin}
Previous analysis results are:

#compare: runtime: O(1) [0], size: O(1) [3] findMin#3: runtime: O(1) [1], size: O(n1) [2 + z' + z'' + z1]

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

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

(28) Obligation:

Complexity RNTS consisting of the following rules:

#cklt(z) -{ 0 }→ 2 :|: z = 3
#cklt(z) -{ 0 }→ 1 :|: z = 1
#cklt(z) -{ 0 }→ 1 :|: z = 2
#cklt(z) -{ 0 }→ 0 :|: z >= 0
#compare(z, z') -{ 0 }→ s :|: s >= 0, s <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ s' :|: s' >= 0, s' <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
#compare(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z - 1 >= 0, z' = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z - 1 >= 0, 3 = 3
#less(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0, 1 = 1
#less(z, z') -{ 1 }→ 1 :|: z' - 1 >= 0, z = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' - 1 >= 0, 2 = 2
#less(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0, v0 >= 0, 1 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z - 1 >= 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' - 1 >= 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z >= 0, z' >= 0, v0 >= 0, 0 = v0
#less(z, z') -{ 1 }→ #cklt(s'') :|: s'' >= 0, s'' <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ #cklt(s1) :|: s1 >= 0, s1 <= 3, z' - 1 >= 0, z - 1 >= 0
findMin(z) -{ 1 }→ findMin#1(z) :|: z >= 0
findMin#1(z) -{ 2 }→ findMin#2(findMin#1(@xs), @x) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0
findMin#1(z) -{ 1 }→ 0 :|: z = 0
findMin#2(z, z') -{ 2 }→ findMin#3(#cklt(s2), z', @y, @ys) :|: s2 >= 0, s2 <= 3, z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
findMin#2(z, z') -{ 1 }→ 1 + z' + 0 :|: z' >= 0, z = 0
findMin#3(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z' + (1 + z'' + z1) :|: z = 2, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z'' + (1 + z' + z1) :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
minSort(z) -{ 2 }→ minSort#1(findMin#1(z)) :|: z >= 0
minSort#1(z) -{ 1 }→ 0 :|: z = 0
minSort#1(z) -{ 1 }→ 1 + @x + minSort(@xs) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0

Function symbols to be analyzed: {#cklt}, {#less}, {findMin#2}, {findMin#1}, {minSort#1,minSort}, {findMin}
Previous analysis results are:

#compare: runtime: O(1) [0], size: O(1) [3] findMin#3: runtime: O(1) [1], size: O(n1) [2 + z' + z'' + z1]

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

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

(30) Obligation:

Complexity RNTS consisting of the following rules:

#cklt(z) -{ 0 }→ 2 :|: z = 3
#cklt(z) -{ 0 }→ 1 :|: z = 1
#cklt(z) -{ 0 }→ 1 :|: z = 2
#cklt(z) -{ 0 }→ 0 :|: z >= 0
#compare(z, z') -{ 0 }→ s :|: s >= 0, s <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ s' :|: s' >= 0, s' <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
#compare(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z - 1 >= 0, z' = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z - 1 >= 0, 3 = 3
#less(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0, 1 = 1
#less(z, z') -{ 1 }→ 1 :|: z' - 1 >= 0, z = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' - 1 >= 0, 2 = 2
#less(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0, v0 >= 0, 1 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z - 1 >= 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' - 1 >= 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z >= 0, z' >= 0, v0 >= 0, 0 = v0
#less(z, z') -{ 1 }→ #cklt(s'') :|: s'' >= 0, s'' <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ #cklt(s1) :|: s1 >= 0, s1 <= 3, z' - 1 >= 0, z - 1 >= 0
findMin(z) -{ 1 }→ findMin#1(z) :|: z >= 0
findMin#1(z) -{ 2 }→ findMin#2(findMin#1(@xs), @x) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0
findMin#1(z) -{ 1 }→ 0 :|: z = 0
findMin#2(z, z') -{ 2 }→ findMin#3(#cklt(s2), z', @y, @ys) :|: s2 >= 0, s2 <= 3, z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
findMin#2(z, z') -{ 1 }→ 1 + z' + 0 :|: z' >= 0, z = 0
findMin#3(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z' + (1 + z'' + z1) :|: z = 2, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z'' + (1 + z' + z1) :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
minSort(z) -{ 2 }→ minSort#1(findMin#1(z)) :|: z >= 0
minSort#1(z) -{ 1 }→ 0 :|: z = 0
minSort#1(z) -{ 1 }→ 1 + @x + minSort(@xs) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0

Function symbols to be analyzed: {#cklt}, {#less}, {findMin#2}, {findMin#1}, {minSort#1,minSort}, {findMin}
Previous analysis results are:

#compare: runtime: O(1) [0], size: O(1) [3] findMin#3: runtime: O(1) [1], size: O(n1) [2 + z' + z'' + z1] #cklt: runtime: ?, size: O(1) [2]

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

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

(32) Obligation:

Complexity RNTS consisting of the following rules:

#cklt(z) -{ 0 }→ 2 :|: z = 3
#cklt(z) -{ 0 }→ 1 :|: z = 1
#cklt(z) -{ 0 }→ 1 :|: z = 2
#cklt(z) -{ 0 }→ 0 :|: z >= 0
#compare(z, z') -{ 0 }→ s :|: s >= 0, s <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ s' :|: s' >= 0, s' <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
#compare(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z - 1 >= 0, z' = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z - 1 >= 0, 3 = 3
#less(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0, 1 = 1
#less(z, z') -{ 1 }→ 1 :|: z' - 1 >= 0, z = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' - 1 >= 0, 2 = 2
#less(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0, v0 >= 0, 1 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z - 1 >= 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' - 1 >= 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z >= 0, z' >= 0, v0 >= 0, 0 = v0
#less(z, z') -{ 1 }→ #cklt(s'') :|: s'' >= 0, s'' <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ #cklt(s1) :|: s1 >= 0, s1 <= 3, z' - 1 >= 0, z - 1 >= 0
findMin(z) -{ 1 }→ findMin#1(z) :|: z >= 0
findMin#1(z) -{ 2 }→ findMin#2(findMin#1(@xs), @x) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0
findMin#1(z) -{ 1 }→ 0 :|: z = 0
findMin#2(z, z') -{ 2 }→ findMin#3(#cklt(s2), z', @y, @ys) :|: s2 >= 0, s2 <= 3, z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
findMin#2(z, z') -{ 1 }→ 1 + z' + 0 :|: z' >= 0, z = 0
findMin#3(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z' + (1 + z'' + z1) :|: z = 2, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z'' + (1 + z' + z1) :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
minSort(z) -{ 2 }→ minSort#1(findMin#1(z)) :|: z >= 0
minSort#1(z) -{ 1 }→ 0 :|: z = 0
minSort#1(z) -{ 1 }→ 1 + @x + minSort(@xs) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0

Function symbols to be analyzed: {#less}, {findMin#2}, {findMin#1}, {minSort#1,minSort}, {findMin}
Previous analysis results are:

#compare: runtime: O(1) [0], size: O(1) [3] findMin#3: runtime: O(1) [1], size: O(n1) [2 + z' + z'' + z1] #cklt: runtime: O(1) [0], size: O(1) [2]

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

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

(34) Obligation:

Complexity RNTS consisting of the following rules:

#cklt(z) -{ 0 }→ 2 :|: z = 3
#cklt(z) -{ 0 }→ 1 :|: z = 1
#cklt(z) -{ 0 }→ 1 :|: z = 2
#cklt(z) -{ 0 }→ 0 :|: z >= 0
#compare(z, z') -{ 0 }→ s :|: s >= 0, s <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ s' :|: s' >= 0, s' <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
#compare(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
#less(z, z') -{ 1 }→ s3 :|: s3 >= 0, s3 <= 2, s'' >= 0, s'' <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ s4 :|: s4 >= 0, s4 <= 2, s1 >= 0, s1 <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z - 1 >= 0, z' = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z - 1 >= 0, 3 = 3
#less(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0, 1 = 1
#less(z, z') -{ 1 }→ 1 :|: z' - 1 >= 0, z = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' - 1 >= 0, 2 = 2
#less(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0, v0 >= 0, 1 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z - 1 >= 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' - 1 >= 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z >= 0, z' >= 0, v0 >= 0, 0 = v0
findMin(z) -{ 1 }→ findMin#1(z) :|: z >= 0
findMin#1(z) -{ 2 }→ findMin#2(findMin#1(@xs), @x) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0
findMin#1(z) -{ 1 }→ 0 :|: z = 0
findMin#2(z, z') -{ 3 }→ s6 :|: s5 >= 0, s5 <= 2, s6 >= 0, s6 <= 1 * z' + 1 * @y + 1 * @ys + 2, s2 >= 0, s2 <= 3, z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
findMin#2(z, z') -{ 1 }→ 1 + z' + 0 :|: z' >= 0, z = 0
findMin#3(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z' + (1 + z'' + z1) :|: z = 2, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z'' + (1 + z' + z1) :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
minSort(z) -{ 2 }→ minSort#1(findMin#1(z)) :|: z >= 0
minSort#1(z) -{ 1 }→ 0 :|: z = 0
minSort#1(z) -{ 1 }→ 1 + @x + minSort(@xs) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0

Function symbols to be analyzed: {#less}, {findMin#2}, {findMin#1}, {minSort#1,minSort}, {findMin}
Previous analysis results are:

#compare: runtime: O(1) [0], size: O(1) [3] findMin#3: runtime: O(1) [1], size: O(n1) [2 + z' + z'' + z1] #cklt: runtime: O(1) [0], size: O(1) [2]

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

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

(36) Obligation:

Complexity RNTS consisting of the following rules:

#cklt(z) -{ 0 }→ 2 :|: z = 3
#cklt(z) -{ 0 }→ 1 :|: z = 1
#cklt(z) -{ 0 }→ 1 :|: z = 2
#cklt(z) -{ 0 }→ 0 :|: z >= 0
#compare(z, z') -{ 0 }→ s :|: s >= 0, s <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ s' :|: s' >= 0, s' <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
#compare(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
#less(z, z') -{ 1 }→ s3 :|: s3 >= 0, s3 <= 2, s'' >= 0, s'' <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ s4 :|: s4 >= 0, s4 <= 2, s1 >= 0, s1 <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z - 1 >= 0, z' = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z - 1 >= 0, 3 = 3
#less(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0, 1 = 1
#less(z, z') -{ 1 }→ 1 :|: z' - 1 >= 0, z = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' - 1 >= 0, 2 = 2
#less(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0, v0 >= 0, 1 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z - 1 >= 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' - 1 >= 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z >= 0, z' >= 0, v0 >= 0, 0 = v0
findMin(z) -{ 1 }→ findMin#1(z) :|: z >= 0
findMin#1(z) -{ 2 }→ findMin#2(findMin#1(@xs), @x) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0
findMin#1(z) -{ 1 }→ 0 :|: z = 0
findMin#2(z, z') -{ 3 }→ s6 :|: s5 >= 0, s5 <= 2, s6 >= 0, s6 <= 1 * z' + 1 * @y + 1 * @ys + 2, s2 >= 0, s2 <= 3, z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
findMin#2(z, z') -{ 1 }→ 1 + z' + 0 :|: z' >= 0, z = 0
findMin#3(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z' + (1 + z'' + z1) :|: z = 2, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z'' + (1 + z' + z1) :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
minSort(z) -{ 2 }→ minSort#1(findMin#1(z)) :|: z >= 0
minSort#1(z) -{ 1 }→ 0 :|: z = 0
minSort#1(z) -{ 1 }→ 1 + @x + minSort(@xs) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0

Function symbols to be analyzed: {#less}, {findMin#2}, {findMin#1}, {minSort#1,minSort}, {findMin}
Previous analysis results are:

#compare: runtime: O(1) [0], size: O(1) [3] findMin#3: runtime: O(1) [1], size: O(n1) [2 + z' + z'' + z1] #cklt: runtime: O(1) [0], size: O(1) [2] #less: runtime: ?, size: O(1) [2]

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

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

(38) Obligation:

Complexity RNTS consisting of the following rules:

#cklt(z) -{ 0 }→ 2 :|: z = 3
#cklt(z) -{ 0 }→ 1 :|: z = 1
#cklt(z) -{ 0 }→ 1 :|: z = 2
#cklt(z) -{ 0 }→ 0 :|: z >= 0
#compare(z, z') -{ 0 }→ s :|: s >= 0, s <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ s' :|: s' >= 0, s' <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
#compare(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
#less(z, z') -{ 1 }→ s3 :|: s3 >= 0, s3 <= 2, s'' >= 0, s'' <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ s4 :|: s4 >= 0, s4 <= 2, s1 >= 0, s1 <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z - 1 >= 0, z' = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z - 1 >= 0, 3 = 3
#less(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0, 1 = 1
#less(z, z') -{ 1 }→ 1 :|: z' - 1 >= 0, z = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' - 1 >= 0, 2 = 2
#less(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0, v0 >= 0, 1 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z - 1 >= 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' - 1 >= 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z >= 0, z' >= 0, v0 >= 0, 0 = v0
findMin(z) -{ 1 }→ findMin#1(z) :|: z >= 0
findMin#1(z) -{ 2 }→ findMin#2(findMin#1(@xs), @x) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0
findMin#1(z) -{ 1 }→ 0 :|: z = 0
findMin#2(z, z') -{ 3 }→ s6 :|: s5 >= 0, s5 <= 2, s6 >= 0, s6 <= 1 * z' + 1 * @y + 1 * @ys + 2, s2 >= 0, s2 <= 3, z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
findMin#2(z, z') -{ 1 }→ 1 + z' + 0 :|: z' >= 0, z = 0
findMin#3(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z' + (1 + z'' + z1) :|: z = 2, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z'' + (1 + z' + z1) :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
minSort(z) -{ 2 }→ minSort#1(findMin#1(z)) :|: z >= 0
minSort#1(z) -{ 1 }→ 0 :|: z = 0
minSort#1(z) -{ 1 }→ 1 + @x + minSort(@xs) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0

Function symbols to be analyzed: {findMin#2}, {findMin#1}, {minSort#1,minSort}, {findMin}
Previous analysis results are:

#compare: runtime: O(1) [0], size: O(1) [3] findMin#3: runtime: O(1) [1], size: O(n1) [2 + z' + z'' + z1] #cklt: runtime: O(1) [0], size: O(1) [2] #less: runtime: O(1) [1], size: O(1) [2]

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

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

(40) Obligation:

Complexity RNTS consisting of the following rules:

#cklt(z) -{ 0 }→ 2 :|: z = 3
#cklt(z) -{ 0 }→ 1 :|: z = 1
#cklt(z) -{ 0 }→ 1 :|: z = 2
#cklt(z) -{ 0 }→ 0 :|: z >= 0
#compare(z, z') -{ 0 }→ s :|: s >= 0, s <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ s' :|: s' >= 0, s' <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
#compare(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
#less(z, z') -{ 1 }→ s3 :|: s3 >= 0, s3 <= 2, s'' >= 0, s'' <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ s4 :|: s4 >= 0, s4 <= 2, s1 >= 0, s1 <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z - 1 >= 0, z' = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z - 1 >= 0, 3 = 3
#less(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0, 1 = 1
#less(z, z') -{ 1 }→ 1 :|: z' - 1 >= 0, z = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' - 1 >= 0, 2 = 2
#less(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0, v0 >= 0, 1 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z - 1 >= 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' - 1 >= 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z >= 0, z' >= 0, v0 >= 0, 0 = v0
findMin(z) -{ 1 }→ findMin#1(z) :|: z >= 0
findMin#1(z) -{ 2 }→ findMin#2(findMin#1(@xs), @x) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0
findMin#1(z) -{ 1 }→ 0 :|: z = 0
findMin#2(z, z') -{ 3 }→ s6 :|: s5 >= 0, s5 <= 2, s6 >= 0, s6 <= 1 * z' + 1 * @y + 1 * @ys + 2, s2 >= 0, s2 <= 3, z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
findMin#2(z, z') -{ 1 }→ 1 + z' + 0 :|: z' >= 0, z = 0
findMin#3(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z' + (1 + z'' + z1) :|: z = 2, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z'' + (1 + z' + z1) :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
minSort(z) -{ 2 }→ minSort#1(findMin#1(z)) :|: z >= 0
minSort#1(z) -{ 1 }→ 0 :|: z = 0
minSort#1(z) -{ 1 }→ 1 + @x + minSort(@xs) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0

Function symbols to be analyzed: {findMin#2}, {findMin#1}, {minSort#1,minSort}, {findMin}
Previous analysis results are:

#compare: runtime: O(1) [0], size: O(1) [3] findMin#3: runtime: O(1) [1], size: O(n1) [2 + z' + z'' + z1] #cklt: runtime: O(1) [0], size: O(1) [2] #less: runtime: O(1) [1], size: O(1) [2]

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

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

(42) Obligation:

Complexity RNTS consisting of the following rules:

#cklt(z) -{ 0 }→ 2 :|: z = 3
#cklt(z) -{ 0 }→ 1 :|: z = 1
#cklt(z) -{ 0 }→ 1 :|: z = 2
#cklt(z) -{ 0 }→ 0 :|: z >= 0
#compare(z, z') -{ 0 }→ s :|: s >= 0, s <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ s' :|: s' >= 0, s' <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
#compare(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
#less(z, z') -{ 1 }→ s3 :|: s3 >= 0, s3 <= 2, s'' >= 0, s'' <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ s4 :|: s4 >= 0, s4 <= 2, s1 >= 0, s1 <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z - 1 >= 0, z' = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z - 1 >= 0, 3 = 3
#less(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0, 1 = 1
#less(z, z') -{ 1 }→ 1 :|: z' - 1 >= 0, z = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' - 1 >= 0, 2 = 2
#less(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0, v0 >= 0, 1 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z - 1 >= 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' - 1 >= 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z >= 0, z' >= 0, v0 >= 0, 0 = v0
findMin(z) -{ 1 }→ findMin#1(z) :|: z >= 0
findMin#1(z) -{ 2 }→ findMin#2(findMin#1(@xs), @x) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0
findMin#1(z) -{ 1 }→ 0 :|: z = 0
findMin#2(z, z') -{ 3 }→ s6 :|: s5 >= 0, s5 <= 2, s6 >= 0, s6 <= 1 * z' + 1 * @y + 1 * @ys + 2, s2 >= 0, s2 <= 3, z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
findMin#2(z, z') -{ 1 }→ 1 + z' + 0 :|: z' >= 0, z = 0
findMin#3(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z' + (1 + z'' + z1) :|: z = 2, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z'' + (1 + z' + z1) :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
minSort(z) -{ 2 }→ minSort#1(findMin#1(z)) :|: z >= 0
minSort#1(z) -{ 1 }→ 0 :|: z = 0
minSort#1(z) -{ 1 }→ 1 + @x + minSort(@xs) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0

Function symbols to be analyzed: {findMin#2}, {findMin#1}, {minSort#1,minSort}, {findMin}
Previous analysis results are:

#compare: runtime: O(1) [0], size: O(1) [3] findMin#3: runtime: O(1) [1], size: O(n1) [2 + z' + z'' + z1] #cklt: runtime: O(1) [0], size: O(1) [2] #less: runtime: O(1) [1], size: O(1) [2] findMin#2: runtime: ?, size: O(n1) [1 + z + z']

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

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

(44) Obligation:

Complexity RNTS consisting of the following rules:

#cklt(z) -{ 0 }→ 2 :|: z = 3
#cklt(z) -{ 0 }→ 1 :|: z = 1
#cklt(z) -{ 0 }→ 1 :|: z = 2
#cklt(z) -{ 0 }→ 0 :|: z >= 0
#compare(z, z') -{ 0 }→ s :|: s >= 0, s <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ s' :|: s' >= 0, s' <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
#compare(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
#less(z, z') -{ 1 }→ s3 :|: s3 >= 0, s3 <= 2, s'' >= 0, s'' <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ s4 :|: s4 >= 0, s4 <= 2, s1 >= 0, s1 <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z - 1 >= 0, z' = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z - 1 >= 0, 3 = 3
#less(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0, 1 = 1
#less(z, z') -{ 1 }→ 1 :|: z' - 1 >= 0, z = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' - 1 >= 0, 2 = 2
#less(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0, v0 >= 0, 1 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z - 1 >= 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' - 1 >= 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z >= 0, z' >= 0, v0 >= 0, 0 = v0
findMin(z) -{ 1 }→ findMin#1(z) :|: z >= 0
findMin#1(z) -{ 2 }→ findMin#2(findMin#1(@xs), @x) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0
findMin#1(z) -{ 1 }→ 0 :|: z = 0
findMin#2(z, z') -{ 3 }→ s6 :|: s5 >= 0, s5 <= 2, s6 >= 0, s6 <= 1 * z' + 1 * @y + 1 * @ys + 2, s2 >= 0, s2 <= 3, z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
findMin#2(z, z') -{ 1 }→ 1 + z' + 0 :|: z' >= 0, z = 0
findMin#3(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z' + (1 + z'' + z1) :|: z = 2, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z'' + (1 + z' + z1) :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
minSort(z) -{ 2 }→ minSort#1(findMin#1(z)) :|: z >= 0
minSort#1(z) -{ 1 }→ 0 :|: z = 0
minSort#1(z) -{ 1 }→ 1 + @x + minSort(@xs) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0

Function symbols to be analyzed: {findMin#1}, {minSort#1,minSort}, {findMin}
Previous analysis results are:

#compare: runtime: O(1) [0], size: O(1) [3] findMin#3: runtime: O(1) [1], size: O(n1) [2 + z' + z'' + z1] #cklt: runtime: O(1) [0], size: O(1) [2] #less: runtime: O(1) [1], size: O(1) [2] findMin#2: runtime: O(1) [3], size: O(n1) [1 + z + z']

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

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

(46) Obligation:

Complexity RNTS consisting of the following rules:

#cklt(z) -{ 0 }→ 2 :|: z = 3
#cklt(z) -{ 0 }→ 1 :|: z = 1
#cklt(z) -{ 0 }→ 1 :|: z = 2
#cklt(z) -{ 0 }→ 0 :|: z >= 0
#compare(z, z') -{ 0 }→ s :|: s >= 0, s <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ s' :|: s' >= 0, s' <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
#compare(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
#less(z, z') -{ 1 }→ s3 :|: s3 >= 0, s3 <= 2, s'' >= 0, s'' <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ s4 :|: s4 >= 0, s4 <= 2, s1 >= 0, s1 <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z - 1 >= 0, z' = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z - 1 >= 0, 3 = 3
#less(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0, 1 = 1
#less(z, z') -{ 1 }→ 1 :|: z' - 1 >= 0, z = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' - 1 >= 0, 2 = 2
#less(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0, v0 >= 0, 1 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z - 1 >= 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' - 1 >= 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z >= 0, z' >= 0, v0 >= 0, 0 = v0
findMin(z) -{ 1 }→ findMin#1(z) :|: z >= 0
findMin#1(z) -{ 2 }→ findMin#2(findMin#1(@xs), @x) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0
findMin#1(z) -{ 1 }→ 0 :|: z = 0
findMin#2(z, z') -{ 3 }→ s6 :|: s5 >= 0, s5 <= 2, s6 >= 0, s6 <= 1 * z' + 1 * @y + 1 * @ys + 2, s2 >= 0, s2 <= 3, z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
findMin#2(z, z') -{ 1 }→ 1 + z' + 0 :|: z' >= 0, z = 0
findMin#3(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z' + (1 + z'' + z1) :|: z = 2, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z'' + (1 + z' + z1) :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
minSort(z) -{ 2 }→ minSort#1(findMin#1(z)) :|: z >= 0
minSort#1(z) -{ 1 }→ 0 :|: z = 0
minSort#1(z) -{ 1 }→ 1 + @x + minSort(@xs) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0

Function symbols to be analyzed: {findMin#1}, {minSort#1,minSort}, {findMin}
Previous analysis results are:

#compare: runtime: O(1) [0], size: O(1) [3] findMin#3: runtime: O(1) [1], size: O(n1) [2 + z' + z'' + z1] #cklt: runtime: O(1) [0], size: O(1) [2] #less: runtime: O(1) [1], size: O(1) [2] findMin#2: runtime: O(1) [3], size: O(n1) [1 + z + z']

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

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

(48) Obligation:

Complexity RNTS consisting of the following rules:

#cklt(z) -{ 0 }→ 2 :|: z = 3
#cklt(z) -{ 0 }→ 1 :|: z = 1
#cklt(z) -{ 0 }→ 1 :|: z = 2
#cklt(z) -{ 0 }→ 0 :|: z >= 0
#compare(z, z') -{ 0 }→ s :|: s >= 0, s <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ s' :|: s' >= 0, s' <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
#compare(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
#less(z, z') -{ 1 }→ s3 :|: s3 >= 0, s3 <= 2, s'' >= 0, s'' <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ s4 :|: s4 >= 0, s4 <= 2, s1 >= 0, s1 <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z - 1 >= 0, z' = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z - 1 >= 0, 3 = 3
#less(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0, 1 = 1
#less(z, z') -{ 1 }→ 1 :|: z' - 1 >= 0, z = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' - 1 >= 0, 2 = 2
#less(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0, v0 >= 0, 1 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z - 1 >= 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' - 1 >= 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z >= 0, z' >= 0, v0 >= 0, 0 = v0
findMin(z) -{ 1 }→ findMin#1(z) :|: z >= 0
findMin#1(z) -{ 2 }→ findMin#2(findMin#1(@xs), @x) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0
findMin#1(z) -{ 1 }→ 0 :|: z = 0
findMin#2(z, z') -{ 3 }→ s6 :|: s5 >= 0, s5 <= 2, s6 >= 0, s6 <= 1 * z' + 1 * @y + 1 * @ys + 2, s2 >= 0, s2 <= 3, z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
findMin#2(z, z') -{ 1 }→ 1 + z' + 0 :|: z' >= 0, z = 0
findMin#3(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z' + (1 + z'' + z1) :|: z = 2, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z'' + (1 + z' + z1) :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
minSort(z) -{ 2 }→ minSort#1(findMin#1(z)) :|: z >= 0
minSort#1(z) -{ 1 }→ 0 :|: z = 0
minSort#1(z) -{ 1 }→ 1 + @x + minSort(@xs) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0

Function symbols to be analyzed: {findMin#1}, {minSort#1,minSort}, {findMin}
Previous analysis results are:

#compare: runtime: O(1) [0], size: O(1) [3] findMin#3: runtime: O(1) [1], size: O(n1) [2 + z' + z'' + z1] #cklt: runtime: O(1) [0], size: O(1) [2] #less: runtime: O(1) [1], size: O(1) [2] findMin#2: runtime: O(1) [3], size: O(n1) [1 + z + z'] findMin#1: runtime: ?, size: O(n1) [z]

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

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

(50) Obligation:

Complexity RNTS consisting of the following rules:

#cklt(z) -{ 0 }→ 2 :|: z = 3
#cklt(z) -{ 0 }→ 1 :|: z = 1
#cklt(z) -{ 0 }→ 1 :|: z = 2
#cklt(z) -{ 0 }→ 0 :|: z >= 0
#compare(z, z') -{ 0 }→ s :|: s >= 0, s <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ s' :|: s' >= 0, s' <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
#compare(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
#less(z, z') -{ 1 }→ s3 :|: s3 >= 0, s3 <= 2, s'' >= 0, s'' <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ s4 :|: s4 >= 0, s4 <= 2, s1 >= 0, s1 <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z - 1 >= 0, z' = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z - 1 >= 0, 3 = 3
#less(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0, 1 = 1
#less(z, z') -{ 1 }→ 1 :|: z' - 1 >= 0, z = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' - 1 >= 0, 2 = 2
#less(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0, v0 >= 0, 1 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z - 1 >= 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' - 1 >= 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z >= 0, z' >= 0, v0 >= 0, 0 = v0
findMin(z) -{ 1 }→ findMin#1(z) :|: z >= 0
findMin#1(z) -{ 2 }→ findMin#2(findMin#1(@xs), @x) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0
findMin#1(z) -{ 1 }→ 0 :|: z = 0
findMin#2(z, z') -{ 3 }→ s6 :|: s5 >= 0, s5 <= 2, s6 >= 0, s6 <= 1 * z' + 1 * @y + 1 * @ys + 2, s2 >= 0, s2 <= 3, z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
findMin#2(z, z') -{ 1 }→ 1 + z' + 0 :|: z' >= 0, z = 0
findMin#3(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z' + (1 + z'' + z1) :|: z = 2, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z'' + (1 + z' + z1) :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
minSort(z) -{ 2 }→ minSort#1(findMin#1(z)) :|: z >= 0
minSort#1(z) -{ 1 }→ 0 :|: z = 0
minSort#1(z) -{ 1 }→ 1 + @x + minSort(@xs) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0

Function symbols to be analyzed: {minSort#1,minSort}, {findMin}
Previous analysis results are:

#compare: runtime: O(1) [0], size: O(1) [3] findMin#3: runtime: O(1) [1], size: O(n1) [2 + z' + z'' + z1] #cklt: runtime: O(1) [0], size: O(1) [2] #less: runtime: O(1) [1], size: O(1) [2] findMin#2: runtime: O(1) [3], size: O(n1) [1 + z + z'] findMin#1: runtime: O(n1) [1 + 5·z], size: O(n1) [z]

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

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

(52) Obligation:

Complexity RNTS consisting of the following rules:

#cklt(z) -{ 0 }→ 2 :|: z = 3
#cklt(z) -{ 0 }→ 1 :|: z = 1
#cklt(z) -{ 0 }→ 1 :|: z = 2
#cklt(z) -{ 0 }→ 0 :|: z >= 0
#compare(z, z') -{ 0 }→ s :|: s >= 0, s <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ s' :|: s' >= 0, s' <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
#compare(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
#less(z, z') -{ 1 }→ s3 :|: s3 >= 0, s3 <= 2, s'' >= 0, s'' <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ s4 :|: s4 >= 0, s4 <= 2, s1 >= 0, s1 <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z - 1 >= 0, z' = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z - 1 >= 0, 3 = 3
#less(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0, 1 = 1
#less(z, z') -{ 1 }→ 1 :|: z' - 1 >= 0, z = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' - 1 >= 0, 2 = 2
#less(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0, v0 >= 0, 1 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z - 1 >= 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' - 1 >= 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z >= 0, z' >= 0, v0 >= 0, 0 = v0
findMin(z) -{ 2 + 5·z }→ s7 :|: s7 >= 0, s7 <= 1 * z, z >= 0
findMin#1(z) -{ 6 + 5·@xs }→ s9 :|: s8 >= 0, s8 <= 1 * @xs, s9 >= 0, s9 <= 1 * s8 + 1 * @x + 1, @x >= 0, z = 1 + @x + @xs, @xs >= 0
findMin#1(z) -{ 1 }→ 0 :|: z = 0
findMin#2(z, z') -{ 3 }→ s6 :|: s5 >= 0, s5 <= 2, s6 >= 0, s6 <= 1 * z' + 1 * @y + 1 * @ys + 2, s2 >= 0, s2 <= 3, z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
findMin#2(z, z') -{ 1 }→ 1 + z' + 0 :|: z' >= 0, z = 0
findMin#3(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z' + (1 + z'' + z1) :|: z = 2, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z'' + (1 + z' + z1) :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
minSort(z) -{ 3 + 5·z }→ minSort#1(s10) :|: s10 >= 0, s10 <= 1 * z, z >= 0
minSort#1(z) -{ 1 }→ 0 :|: z = 0
minSort#1(z) -{ 1 }→ 1 + @x + minSort(@xs) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0

Function symbols to be analyzed: {minSort#1,minSort}, {findMin}
Previous analysis results are:

#compare: runtime: O(1) [0], size: O(1) [3] findMin#3: runtime: O(1) [1], size: O(n1) [2 + z' + z'' + z1] #cklt: runtime: O(1) [0], size: O(1) [2] #less: runtime: O(1) [1], size: O(1) [2] findMin#2: runtime: O(1) [3], size: O(n1) [1 + z + z'] findMin#1: runtime: O(n1) [1 + 5·z], size: O(n1) [z]

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

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

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

(54) Obligation:

Complexity RNTS consisting of the following rules:

#cklt(z) -{ 0 }→ 2 :|: z = 3
#cklt(z) -{ 0 }→ 1 :|: z = 1
#cklt(z) -{ 0 }→ 1 :|: z = 2
#cklt(z) -{ 0 }→ 0 :|: z >= 0
#compare(z, z') -{ 0 }→ s :|: s >= 0, s <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ s' :|: s' >= 0, s' <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
#compare(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
#less(z, z') -{ 1 }→ s3 :|: s3 >= 0, s3 <= 2, s'' >= 0, s'' <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ s4 :|: s4 >= 0, s4 <= 2, s1 >= 0, s1 <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z - 1 >= 0, z' = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z - 1 >= 0, 3 = 3
#less(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0, 1 = 1
#less(z, z') -{ 1 }→ 1 :|: z' - 1 >= 0, z = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' - 1 >= 0, 2 = 2
#less(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0, v0 >= 0, 1 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z - 1 >= 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' - 1 >= 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z >= 0, z' >= 0, v0 >= 0, 0 = v0
findMin(z) -{ 2 + 5·z }→ s7 :|: s7 >= 0, s7 <= 1 * z, z >= 0
findMin#1(z) -{ 6 + 5·@xs }→ s9 :|: s8 >= 0, s8 <= 1 * @xs, s9 >= 0, s9 <= 1 * s8 + 1 * @x + 1, @x >= 0, z = 1 + @x + @xs, @xs >= 0
findMin#1(z) -{ 1 }→ 0 :|: z = 0
findMin#2(z, z') -{ 3 }→ s6 :|: s5 >= 0, s5 <= 2, s6 >= 0, s6 <= 1 * z' + 1 * @y + 1 * @ys + 2, s2 >= 0, s2 <= 3, z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
findMin#2(z, z') -{ 1 }→ 1 + z' + 0 :|: z' >= 0, z = 0
findMin#3(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z' + (1 + z'' + z1) :|: z = 2, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z'' + (1 + z' + z1) :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
minSort(z) -{ 3 + 5·z }→ minSort#1(s10) :|: s10 >= 0, s10 <= 1 * z, z >= 0
minSort#1(z) -{ 1 }→ 0 :|: z = 0
minSort#1(z) -{ 1 }→ 1 + @x + minSort(@xs) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0

Function symbols to be analyzed: {minSort#1,minSort}, {findMin}
Previous analysis results are:

#compare: runtime: O(1) [0], size: O(1) [3] findMin#3: runtime: O(1) [1], size: O(n1) [2 + z' + z'' + z1] #cklt: runtime: O(1) [0], size: O(1) [2] #less: runtime: O(1) [1], size: O(1) [2] findMin#2: runtime: O(1) [3], size: O(n1) [1 + z + z'] findMin#1: runtime: O(n1) [1 + 5·z], size: O(n1) [z] minSort#1: runtime: ?, size: O(n1) [z] minSort: runtime: ?, size: O(n1) [z]

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

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

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

(56) Obligation:

Complexity RNTS consisting of the following rules:

#cklt(z) -{ 0 }→ 2 :|: z = 3
#cklt(z) -{ 0 }→ 1 :|: z = 1
#cklt(z) -{ 0 }→ 1 :|: z = 2
#cklt(z) -{ 0 }→ 0 :|: z >= 0
#compare(z, z') -{ 0 }→ s :|: s >= 0, s <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ s' :|: s' >= 0, s' <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
#compare(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
#less(z, z') -{ 1 }→ s3 :|: s3 >= 0, s3 <= 2, s'' >= 0, s'' <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ s4 :|: s4 >= 0, s4 <= 2, s1 >= 0, s1 <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z - 1 >= 0, z' = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z - 1 >= 0, 3 = 3
#less(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0, 1 = 1
#less(z, z') -{ 1 }→ 1 :|: z' - 1 >= 0, z = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' - 1 >= 0, 2 = 2
#less(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0, v0 >= 0, 1 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z - 1 >= 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' - 1 >= 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z >= 0, z' >= 0, v0 >= 0, 0 = v0
findMin(z) -{ 2 + 5·z }→ s7 :|: s7 >= 0, s7 <= 1 * z, z >= 0
findMin#1(z) -{ 6 + 5·@xs }→ s9 :|: s8 >= 0, s8 <= 1 * @xs, s9 >= 0, s9 <= 1 * s8 + 1 * @x + 1, @x >= 0, z = 1 + @x + @xs, @xs >= 0
findMin#1(z) -{ 1 }→ 0 :|: z = 0
findMin#2(z, z') -{ 3 }→ s6 :|: s5 >= 0, s5 <= 2, s6 >= 0, s6 <= 1 * z' + 1 * @y + 1 * @ys + 2, s2 >= 0, s2 <= 3, z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
findMin#2(z, z') -{ 1 }→ 1 + z' + 0 :|: z' >= 0, z = 0
findMin#3(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z' + (1 + z'' + z1) :|: z = 2, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z'' + (1 + z' + z1) :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
minSort(z) -{ 3 + 5·z }→ minSort#1(s10) :|: s10 >= 0, s10 <= 1 * z, z >= 0
minSort#1(z) -{ 1 }→ 0 :|: z = 0
minSort#1(z) -{ 1 }→ 1 + @x + minSort(@xs) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0

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

#compare: runtime: O(1) [0], size: O(1) [3] findMin#3: runtime: O(1) [1], size: O(n1) [2 + z' + z'' + z1] #cklt: runtime: O(1) [0], size: O(1) [2] #less: runtime: O(1) [1], size: O(1) [2] findMin#2: runtime: O(1) [3], size: O(n1) [1 + z + z'] findMin#1: runtime: O(n1) [1 + 5·z], size: O(n1) [z] minSort#1: runtime: O(n2) [4 + 8·z + 5·z2], size: O(n1) [z] minSort: runtime: O(n2) [7 + 13·z + 5·z2], size: O(n1) [z]

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

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

(58) Obligation:

Complexity RNTS consisting of the following rules:

#cklt(z) -{ 0 }→ 2 :|: z = 3
#cklt(z) -{ 0 }→ 1 :|: z = 1
#cklt(z) -{ 0 }→ 1 :|: z = 2
#cklt(z) -{ 0 }→ 0 :|: z >= 0
#compare(z, z') -{ 0 }→ s :|: s >= 0, s <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ s' :|: s' >= 0, s' <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
#compare(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
#less(z, z') -{ 1 }→ s3 :|: s3 >= 0, s3 <= 2, s'' >= 0, s'' <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ s4 :|: s4 >= 0, s4 <= 2, s1 >= 0, s1 <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z - 1 >= 0, z' = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z - 1 >= 0, 3 = 3
#less(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0, 1 = 1
#less(z, z') -{ 1 }→ 1 :|: z' - 1 >= 0, z = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' - 1 >= 0, 2 = 2
#less(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0, v0 >= 0, 1 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z - 1 >= 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' - 1 >= 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z >= 0, z' >= 0, v0 >= 0, 0 = v0
findMin(z) -{ 2 + 5·z }→ s7 :|: s7 >= 0, s7 <= 1 * z, z >= 0
findMin#1(z) -{ 6 + 5·@xs }→ s9 :|: s8 >= 0, s8 <= 1 * @xs, s9 >= 0, s9 <= 1 * s8 + 1 * @x + 1, @x >= 0, z = 1 + @x + @xs, @xs >= 0
findMin#1(z) -{ 1 }→ 0 :|: z = 0
findMin#2(z, z') -{ 3 }→ s6 :|: s5 >= 0, s5 <= 2, s6 >= 0, s6 <= 1 * z' + 1 * @y + 1 * @ys + 2, s2 >= 0, s2 <= 3, z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
findMin#2(z, z') -{ 1 }→ 1 + z' + 0 :|: z' >= 0, z = 0
findMin#3(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z' + (1 + z'' + z1) :|: z = 2, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z'' + (1 + z' + z1) :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
minSort(z) -{ 7 + 8·s10 + 5·s10² + 5·z }→ s11 :|: s11 >= 0, s11 <= 1 * s10, s10 >= 0, s10 <= 1 * z, z >= 0
minSort#1(z) -{ 1 }→ 0 :|: z = 0
minSort#1(z) -{ 8 + 13·@xs + 5·@xs² }→ 1 + @x + s12 :|: s12 >= 0, s12 <= 1 * @xs, @x >= 0, z = 1 + @x + @xs, @xs >= 0

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

#compare: runtime: O(1) [0], size: O(1) [3] findMin#3: runtime: O(1) [1], size: O(n1) [2 + z' + z'' + z1] #cklt: runtime: O(1) [0], size: O(1) [2] #less: runtime: O(1) [1], size: O(1) [2] findMin#2: runtime: O(1) [3], size: O(n1) [1 + z + z'] findMin#1: runtime: O(n1) [1 + 5·z], size: O(n1) [z] minSort#1: runtime: O(n2) [4 + 8·z + 5·z2], size: O(n1) [z] minSort: runtime: O(n2) [7 + 13·z + 5·z2], size: O(n1) [z]

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

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

(60) Obligation:

Complexity RNTS consisting of the following rules:

#cklt(z) -{ 0 }→ 2 :|: z = 3
#cklt(z) -{ 0 }→ 1 :|: z = 1
#cklt(z) -{ 0 }→ 1 :|: z = 2
#cklt(z) -{ 0 }→ 0 :|: z >= 0
#compare(z, z') -{ 0 }→ s :|: s >= 0, s <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ s' :|: s' >= 0, s' <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
#compare(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
#less(z, z') -{ 1 }→ s3 :|: s3 >= 0, s3 <= 2, s'' >= 0, s'' <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ s4 :|: s4 >= 0, s4 <= 2, s1 >= 0, s1 <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z - 1 >= 0, z' = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z - 1 >= 0, 3 = 3
#less(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0, 1 = 1
#less(z, z') -{ 1 }→ 1 :|: z' - 1 >= 0, z = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' - 1 >= 0, 2 = 2
#less(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0, v0 >= 0, 1 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z - 1 >= 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' - 1 >= 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z >= 0, z' >= 0, v0 >= 0, 0 = v0
findMin(z) -{ 2 + 5·z }→ s7 :|: s7 >= 0, s7 <= 1 * z, z >= 0
findMin#1(z) -{ 6 + 5·@xs }→ s9 :|: s8 >= 0, s8 <= 1 * @xs, s9 >= 0, s9 <= 1 * s8 + 1 * @x + 1, @x >= 0, z = 1 + @x + @xs, @xs >= 0
findMin#1(z) -{ 1 }→ 0 :|: z = 0
findMin#2(z, z') -{ 3 }→ s6 :|: s5 >= 0, s5 <= 2, s6 >= 0, s6 <= 1 * z' + 1 * @y + 1 * @ys + 2, s2 >= 0, s2 <= 3, z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
findMin#2(z, z') -{ 1 }→ 1 + z' + 0 :|: z' >= 0, z = 0
findMin#3(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z' + (1 + z'' + z1) :|: z = 2, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z'' + (1 + z' + z1) :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
minSort(z) -{ 7 + 8·s10 + 5·s10² + 5·z }→ s11 :|: s11 >= 0, s11 <= 1 * s10, s10 >= 0, s10 <= 1 * z, z >= 0
minSort#1(z) -{ 1 }→ 0 :|: z = 0
minSort#1(z) -{ 8 + 13·@xs + 5·@xs² }→ 1 + @x + s12 :|: s12 >= 0, s12 <= 1 * @xs, @x >= 0, z = 1 + @x + @xs, @xs >= 0

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

#compare: runtime: O(1) [0], size: O(1) [3] findMin#3: runtime: O(1) [1], size: O(n1) [2 + z' + z'' + z1] #cklt: runtime: O(1) [0], size: O(1) [2] #less: runtime: O(1) [1], size: O(1) [2] findMin#2: runtime: O(1) [3], size: O(n1) [1 + z + z'] findMin#1: runtime: O(n1) [1 + 5·z], size: O(n1) [z] minSort#1: runtime: O(n2) [4 + 8·z + 5·z2], size: O(n1) [z] minSort: runtime: O(n2) [7 + 13·z + 5·z2], size: O(n1) [z] findMin: runtime: ?, size: O(n1) [z]

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

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

(62) Obligation:

Complexity RNTS consisting of the following rules:

#cklt(z) -{ 0 }→ 2 :|: z = 3
#cklt(z) -{ 0 }→ 1 :|: z = 1
#cklt(z) -{ 0 }→ 1 :|: z = 2
#cklt(z) -{ 0 }→ 0 :|: z >= 0
#compare(z, z') -{ 0 }→ s :|: s >= 0, s <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ s' :|: s' >= 0, s' <= 3, z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 3 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z = 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' = 0
#compare(z, z') -{ 0 }→ 2 :|: z - 1 >= 0, z' - 1 >= 0
#compare(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
#compare(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
#less(z, z') -{ 1 }→ s3 :|: s3 >= 0, s3 <= 2, s'' >= 0, s'' <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ s4 :|: s4 >= 0, s4 <= 2, s1 >= 0, s1 <= 3, z' - 1 >= 0, z - 1 >= 0
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z - 1 >= 0, z' = 0, 3 = 3
#less(z, z') -{ 1 }→ 2 :|: z' - 1 >= 0, z - 1 >= 0, 3 = 3
#less(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0, 1 = 1
#less(z, z') -{ 1 }→ 1 :|: z' - 1 >= 0, z = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' = 0, 2 = 2
#less(z, z') -{ 1 }→ 1 :|: z - 1 >= 0, z' - 1 >= 0, 2 = 2
#less(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0, v0 >= 0, 1 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z - 1 >= 0, v0 >= 0, 3 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' - 1 >= 0, v0 >= 0, 2 = v0
#less(z, z') -{ 1 }→ 0 :|: z >= 0, z' >= 0, v0 >= 0, 0 = v0
findMin(z) -{ 2 + 5·z }→ s7 :|: s7 >= 0, s7 <= 1 * z, z >= 0
findMin#1(z) -{ 6 + 5·@xs }→ s9 :|: s8 >= 0, s8 <= 1 * @xs, s9 >= 0, s9 <= 1 * s8 + 1 * @x + 1, @x >= 0, z = 1 + @x + @xs, @xs >= 0
findMin#1(z) -{ 1 }→ 0 :|: z = 0
findMin#2(z, z') -{ 3 }→ s6 :|: s5 >= 0, s5 <= 2, s6 >= 0, s6 <= 1 * z' + 1 * @y + 1 * @ys + 2, s2 >= 0, s2 <= 3, z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
findMin#2(z, z') -{ 1 }→ 1 + z' + 0 :|: z' >= 0, z = 0
findMin#3(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z' + (1 + z'' + z1) :|: z = 2, z' >= 0, z'' >= 0, z1 >= 0
findMin#3(z, z', z'', z1) -{ 1 }→ 1 + z'' + (1 + z' + z1) :|: z' >= 0, z = 1, z'' >= 0, z1 >= 0
minSort(z) -{ 7 + 8·s10 + 5·s10² + 5·z }→ s11 :|: s11 >= 0, s11 <= 1 * s10, s10 >= 0, s10 <= 1 * z, z >= 0
minSort#1(z) -{ 1 }→ 0 :|: z = 0
minSort#1(z) -{ 8 + 13·@xs + 5·@xs² }→ 1 + @x + s12 :|: s12 >= 0, s12 <= 1 * @xs, @x >= 0, z = 1 + @x + @xs, @xs >= 0

Function symbols to be analyzed:
Previous analysis results are:

#compare: runtime: O(1) [0], size: O(1) [3] findMin#3: runtime: O(1) [1], size: O(n1) [2 + z' + z'' + z1] #cklt: runtime: O(1) [0], size: O(1) [2] #less: runtime: O(1) [1], size: O(1) [2] findMin#2: runtime: O(1) [3], size: O(n1) [1 + z + z'] findMin#1: runtime: O(n1) [1 + 5·z], size: O(n1) [z] minSort#1: runtime: O(n2) [4 + 8·z + 5·z2], size: O(n1) [z] minSort: runtime: O(n2) [7 + 13·z + 5·z2], size: O(n1) [z] findMin: runtime: O(n1) [2 + 5·z], size: O(n1) [z]

(63) FinalProof (EQUIVALENT transformation)

Computed overall runtime complexity

(64) BOUNDS(1, n^2)