0 CpxRelTRS
↳1 RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxTypedWeightedTrs
↳5 CompletionProof (UPPER BOUND(ID), 0 ms)
↳6 CpxTypedWeightedCompleteTrs
↳7 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 15 ms)
↳8 CpxRNTS
↳9 CompleteCoflocoProof (⇔, 4474 ms)
↳10 BOUNDS(1, n^2)
#equal(@x, @y) → #eq(@x, @y)
and(@x, @y) → #and(@x, @y)
eq(@l1, @l2) → eq#1(@l1, @l2)
eq#1(::(@x, @xs), @l2) → eq#3(@l2, @x, @xs)
eq#1(nil, @l2) → eq#2(@l2)
eq#2(::(@y, @ys)) → #false
eq#2(nil) → #true
eq#3(::(@y, @ys), @x, @xs) → and(#equal(@x, @y), eq(@xs, @ys))
eq#3(nil, @x, @xs) → #false
nub(@l) → nub#1(@l)
nub#1(::(@x, @xs)) → ::(@x, nub(remove(@x, @xs)))
nub#1(nil) → nil
remove(@x, @l) → remove#1(@l, @x)
remove#1(::(@y, @ys), @x) → remove#2(eq(@x, @y), @x, @y, @ys)
remove#1(nil, @x) → nil
remove#2(#false, @x, @y, @ys) → ::(@y, remove(@x, @ys))
remove#2(#true, @x, @y, @ys) → remove(@x, @ys)
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), nil) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, nil) → #true
#equal(@x, @y) → #eq(@x, @y) [1]
and(@x, @y) → #and(@x, @y) [1]
eq(@l1, @l2) → eq#1(@l1, @l2) [1]
eq#1(::(@x, @xs), @l2) → eq#3(@l2, @x, @xs) [1]
eq#1(nil, @l2) → eq#2(@l2) [1]
eq#2(::(@y, @ys)) → #false [1]
eq#2(nil) → #true [1]
eq#3(::(@y, @ys), @x, @xs) → and(#equal(@x, @y), eq(@xs, @ys)) [1]
eq#3(nil, @x, @xs) → #false [1]
nub(@l) → nub#1(@l) [1]
nub#1(::(@x, @xs)) → ::(@x, nub(remove(@x, @xs))) [1]
nub#1(nil) → nil [1]
remove(@x, @l) → remove#1(@l, @x) [1]
remove#1(::(@y, @ys), @x) → remove#2(eq(@x, @y), @x, @y, @ys) [1]
remove#1(nil, @x) → nil [1]
remove#2(#false, @x, @y, @ys) → ::(@y, remove(@x, @ys)) [1]
remove#2(#true, @x, @y, @ys) → remove(@x, @ys) [1]
#and(#false, #false) → #false [0]
#and(#false, #true) → #false [0]
#and(#true, #false) → #false [0]
#and(#true, #true) → #true [0]
#eq(#0, #0) → #true [0]
#eq(#0, #neg(@y)) → #false [0]
#eq(#0, #pos(@y)) → #false [0]
#eq(#0, #s(@y)) → #false [0]
#eq(#neg(@x), #0) → #false [0]
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y) [0]
#eq(#neg(@x), #pos(@y)) → #false [0]
#eq(#pos(@x), #0) → #false [0]
#eq(#pos(@x), #neg(@y)) → #false [0]
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y) [0]
#eq(#s(@x), #0) → #false [0]
#eq(#s(@x), #s(@y)) → #eq(@x, @y) [0]
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) [0]
#eq(::(@x_1, @x_2), nil) → #false [0]
#eq(nil, ::(@y_1, @y_2)) → #false [0]
#eq(nil, nil) → #true [0]
#equal(@x, @y) → #eq(@x, @y) [1]
and(@x, @y) → #and(@x, @y) [1]
eq(@l1, @l2) → eq#1(@l1, @l2) [1]
eq#1(::(@x, @xs), @l2) → eq#3(@l2, @x, @xs) [1]
eq#1(nil, @l2) → eq#2(@l2) [1]
eq#2(::(@y, @ys)) → #false [1]
eq#2(nil) → #true [1]
eq#3(::(@y, @ys), @x, @xs) → and(#equal(@x, @y), eq(@xs, @ys)) [1]
eq#3(nil, @x, @xs) → #false [1]
nub(@l) → nub#1(@l) [1]
nub#1(::(@x, @xs)) → ::(@x, nub(remove(@x, @xs))) [1]
nub#1(nil) → nil [1]
remove(@x, @l) → remove#1(@l, @x) [1]
remove#1(::(@y, @ys), @x) → remove#2(eq(@x, @y), @x, @y, @ys) [1]
remove#1(nil, @x) → nil [1]
remove#2(#false, @x, @y, @ys) → ::(@y, remove(@x, @ys)) [1]
remove#2(#true, @x, @y, @ys) → remove(@x, @ys) [1]
#and(#false, #false) → #false [0]
#and(#false, #true) → #false [0]
#and(#true, #false) → #false [0]
#and(#true, #true) → #true [0]
#eq(#0, #0) → #true [0]
#eq(#0, #neg(@y)) → #false [0]
#eq(#0, #pos(@y)) → #false [0]
#eq(#0, #s(@y)) → #false [0]
#eq(#neg(@x), #0) → #false [0]
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y) [0]
#eq(#neg(@x), #pos(@y)) → #false [0]
#eq(#pos(@x), #0) → #false [0]
#eq(#pos(@x), #neg(@y)) → #false [0]
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y) [0]
#eq(#s(@x), #0) → #false [0]
#eq(#s(@x), #s(@y)) → #eq(@x, @y) [0]
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) [0]
#eq(::(@x_1, @x_2), nil) → #false [0]
#eq(nil, ::(@y_1, @y_2)) → #false [0]
#eq(nil, nil) → #true [0]
| #equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true #eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true and :: #false:#true → #false:#true → #false:#true #and :: #false:#true → #false:#true → #false:#true eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true eq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true :: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s eq#3 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true nil :: :::nil:#0:#neg:#pos:#s eq#2 :: :::nil:#0:#neg:#pos:#s → #false:#true #false :: #false:#true #true :: #false:#true nub :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s nub#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s remove :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s remove#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s remove#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s #0 :: :::nil:#0:#neg:#pos:#s #neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s #pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s #s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s |
#and(v0, v1) → null_#and [0]
#eq(v0, v1) → null_#eq [0]
eq#1(v0, v1) → null_eq#1 [0]
eq#2(v0) → null_eq#2 [0]
eq#3(v0, v1, v2) → null_eq#3 [0]
nub#1(v0) → null_nub#1 [0]
remove#1(v0, v1) → null_remove#1 [0]
remove#2(v0, v1, v2, v3) → null_remove#2 [0]
null_#and, null_#eq, null_eq#1, null_eq#2, null_eq#3, null_nub#1, null_remove#1, null_remove#2
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
nil => 1
#false => 1
#true => 2
#0 => 0
null_#and => 0
null_#eq => 0
null_eq#1 => 0
null_eq#2 => 0
null_eq#3 => 0
null_nub#1 => 0
null_remove#1 => 0
null_remove#2 => 0
#and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
#and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
#and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
#and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
#and(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
#eq(z, z') -{ 0 }→ 2 :|: z = 0, z' = 0
#eq(z, z') -{ 0 }→ 2 :|: z = 1, z' = 1
#eq(z, z') -{ 0 }→ 1 :|: z = 0, z' = 1 + @y, @y >= 0
#eq(z, z') -{ 0 }→ 1 :|: @x >= 0, z = 1 + @x, z' = 0
#eq(z, z') -{ 0 }→ 1 :|: @x >= 0, z = 1 + @x, z' = 1 + @y, @y >= 0
#eq(z, z') -{ 0 }→ 1 :|: @x_1 >= 0, z = 1 + @x_1 + @x_2, @x_2 >= 0, z' = 1
#eq(z, z') -{ 0 }→ 1 :|: z = 1, @y_1 >= 0, @y_2 >= 0, z' = 1 + @y_1 + @y_2
#eq(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
#eq(z, z') -{ 0 }→ #eq(@x, @y) :|: @x >= 0, z = 1 + @x, z' = 1 + @y, @y >= 0
#eq(z, z') -{ 0 }→ #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) :|: @x_1 >= 0, z = 1 + @x_1 + @x_2, @y_1 >= 0, @x_2 >= 0, @y_2 >= 0, z' = 1 + @y_1 + @y_2
#equal(z, z') -{ 1 }→ #eq(@x, @y) :|: z = @x, @x >= 0, z' = @y, @y >= 0
and(z, z') -{ 1 }→ #and(@x, @y) :|: z = @x, @x >= 0, z' = @y, @y >= 0
eq(z, z') -{ 1 }→ eq#1(@l1, @l2) :|: @l1 >= 0, z' = @l2, @l2 >= 0, z = @l1
eq#1(z, z') -{ 1 }→ eq#3(@l2, @x, @xs) :|: z' = @l2, @x >= 0, z = 1 + @x + @xs, @l2 >= 0, @xs >= 0
eq#1(z, z') -{ 1 }→ eq#2(@l2) :|: z' = @l2, z = 1, @l2 >= 0
eq#1(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
eq#2(z) -{ 1 }→ 2 :|: z = 1
eq#2(z) -{ 1 }→ 1 :|: z = 1 + @y + @ys, @y >= 0, @ys >= 0
eq#2(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
eq#3(z, z', z'') -{ 1 }→ and(#equal(@x, @y), eq(@xs, @ys)) :|: z = 1 + @y + @ys, @x >= 0, @xs >= 0, @y >= 0, z' = @x, z'' = @xs, @ys >= 0
eq#3(z, z', z'') -{ 1 }→ 1 :|: @x >= 0, z = 1, @xs >= 0, z' = @x, z'' = @xs
eq#3(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
nub(z) -{ 1 }→ nub#1(@l) :|: z = @l, @l >= 0
nub#1(z) -{ 1 }→ 1 :|: z = 1
nub#1(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
nub#1(z) -{ 1 }→ 1 + @x + nub(remove(@x, @xs)) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0
remove(z, z') -{ 1 }→ remove#1(@l, @x) :|: z = @x, @l >= 0, @x >= 0, z' = @l
remove#1(z, z') -{ 1 }→ remove#2(eq(@x, @y), @x, @y, @ys) :|: z = 1 + @y + @ys, @x >= 0, @y >= 0, z' = @x, @ys >= 0
remove#1(z, z') -{ 1 }→ 1 :|: @x >= 0, z = 1, z' = @x
remove#1(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
remove#2(z, z', z'', z1) -{ 1 }→ remove(@x, @ys) :|: z = 2, @x >= 0, z1 = @ys, @y >= 0, z' = @x, @ys >= 0, z'' = @y
remove#2(z, z', z'', z1) -{ 0 }→ 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
remove#2(z, z', z'', z1) -{ 1 }→ 1 + @y + remove(@x, @ys) :|: @x >= 0, z = 1, z1 = @ys, @y >= 0, z' = @x, @ys >= 0, z'' = @y
| eq(start(V, V1, V14, V30),0,[fun(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V14, V30),0,[and(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V14, V30),0,[eq(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V14, V30),0,[fun3(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V14, V30),0,[fun5(V, Out)],[V >= 0]). eq(start(V, V1, V14, V30),0,[fun4(V, V1, V14, Out)],[V >= 0,V1 >= 0,V14 >= 0]). eq(start(V, V1, V14, V30),0,[nub(V, Out)],[V >= 0]). eq(start(V, V1, V14, V30),0,[fun6(V, Out)],[V >= 0]). eq(start(V, V1, V14, V30),0,[remove(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V14, V30),0,[fun7(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V14, V30),0,[fun8(V, V1, V14, V30, Out)],[V >= 0,V1 >= 0,V14 >= 0,V30 >= 0]). eq(start(V, V1, V14, V30),0,[fun2(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V14, V30),0,[fun1(V, V1, Out)],[V >= 0,V1 >= 0]). eq(fun(V, V1, Out),1,[fun1(V2, V3, Ret)],[Out = Ret,V = V2,V2 >= 0,V1 = V3,V3 >= 0]). eq(and(V, V1, Out),1,[fun2(V4, V5, Ret1)],[Out = Ret1,V = V4,V4 >= 0,V1 = V5,V5 >= 0]). eq(eq(V, V1, Out),1,[fun3(V6, V7, Ret2)],[Out = Ret2,V6 >= 0,V1 = V7,V7 >= 0,V = V6]). eq(fun3(V, V1, Out),1,[fun4(V8, V9, V10, Ret3)],[Out = Ret3,V1 = V8,V9 >= 0,V = 1 + V10 + V9,V8 >= 0,V10 >= 0]). eq(fun3(V, V1, Out),1,[fun5(V11, Ret4)],[Out = Ret4,V1 = V11,V = 1,V11 >= 0]). eq(fun5(V, Out),1,[],[Out = 1,V = 1 + V12 + V13,V12 >= 0,V13 >= 0]). eq(fun5(V, Out),1,[],[Out = 2,V = 1]). eq(fun4(V, V1, V14, Out),1,[fun(V15, V16, Ret0),eq(V17, V18, Ret11),and(Ret0, Ret11, Ret5)],[Out = Ret5,V = 1 + V16 + V18,V15 >= 0,V17 >= 0,V16 >= 0,V1 = V15,V14 = V17,V18 >= 0]). eq(fun4(V, V1, V14, Out),1,[],[Out = 1,V19 >= 0,V = 1,V20 >= 0,V1 = V19,V14 = V20]). eq(nub(V, Out),1,[fun6(V21, Ret6)],[Out = Ret6,V = V21,V21 >= 0]). eq(fun6(V, Out),1,[remove(V22, V23, Ret10),nub(Ret10, Ret12)],[Out = 1 + Ret12 + V22,V22 >= 0,V = 1 + V22 + V23,V23 >= 0]). eq(fun6(V, Out),1,[],[Out = 1,V = 1]). eq(remove(V, V1, Out),1,[fun7(V24, V25, Ret7)],[Out = Ret7,V = V25,V24 >= 0,V25 >= 0,V1 = V24]). eq(fun7(V, V1, Out),1,[eq(V26, V27, Ret01),fun8(Ret01, V26, V27, V28, Ret8)],[Out = Ret8,V = 1 + V27 + V28,V26 >= 0,V27 >= 0,V1 = V26,V28 >= 0]). eq(fun7(V, V1, Out),1,[],[Out = 1,V29 >= 0,V = 1,V1 = V29]). eq(fun8(V, V1, V14, V30, Out),1,[remove(V32, V33, Ret13)],[Out = 1 + Ret13 + V31,V32 >= 0,V = 1,V30 = V33,V31 >= 0,V1 = V32,V33 >= 0,V14 = V31]). eq(fun8(V, V1, V14, V30, Out),1,[remove(V34, V35, Ret9)],[Out = Ret9,V = 2,V34 >= 0,V30 = V35,V36 >= 0,V1 = V34,V35 >= 0,V14 = V36]). eq(fun2(V, V1, Out),0,[],[Out = 1,V = 1,V1 = 1]). eq(fun2(V, V1, Out),0,[],[Out = 1,V1 = 2,V = 1]). eq(fun2(V, V1, Out),0,[],[Out = 1,V = 2,V1 = 1]). eq(fun2(V, V1, Out),0,[],[Out = 2,V = 2,V1 = 2]). eq(fun1(V, V1, Out),0,[],[Out = 2,V = 0,V1 = 0]). eq(fun1(V, V1, Out),0,[],[Out = 1,V = 0,V1 = 1 + V37,V37 >= 0]). eq(fun1(V, V1, Out),0,[],[Out = 1,V38 >= 0,V = 1 + V38,V1 = 0]). eq(fun1(V, V1, Out),0,[fun1(V39, V40, Ret14)],[Out = Ret14,V39 >= 0,V = 1 + V39,V1 = 1 + V40,V40 >= 0]). eq(fun1(V, V1, Out),0,[],[Out = 1,V41 >= 0,V = 1 + V41,V1 = 1 + V42,V42 >= 0]). eq(fun1(V, V1, Out),0,[fun1(V43, V44, Ret02),fun1(V45, V46, Ret15),fun2(Ret02, Ret15, Ret16)],[Out = Ret16,V43 >= 0,V = 1 + V43 + V45,V44 >= 0,V45 >= 0,V46 >= 0,V1 = 1 + V44 + V46]). eq(fun1(V, V1, Out),0,[],[Out = 1,V47 >= 0,V = 1 + V47 + V48,V48 >= 0,V1 = 1]). eq(fun1(V, V1, Out),0,[],[Out = 1,V = 1,V49 >= 0,V50 >= 0,V1 = 1 + V49 + V50]). eq(fun1(V, V1, Out),0,[],[Out = 2,V = 1,V1 = 1]). eq(fun2(V, V1, Out),0,[],[Out = 0,V51 >= 0,V52 >= 0,V = V51,V1 = V52]). eq(fun1(V, V1, Out),0,[],[Out = 0,V53 >= 0,V54 >= 0,V = V53,V1 = V54]). eq(fun3(V, V1, Out),0,[],[Out = 0,V55 >= 0,V56 >= 0,V = V55,V1 = V56]). eq(fun5(V, Out),0,[],[Out = 0,V57 >= 0,V = V57]). eq(fun4(V, V1, V14, Out),0,[],[Out = 0,V58 >= 0,V14 = V59,V60 >= 0,V = V58,V1 = V60,V59 >= 0]). eq(fun6(V, Out),0,[],[Out = 0,V61 >= 0,V = V61]). eq(fun7(V, V1, Out),0,[],[Out = 0,V62 >= 0,V63 >= 0,V = V62,V1 = V63]). eq(fun8(V, V1, V14, V30, Out),0,[],[Out = 0,V30 = V64,V65 >= 0,V14 = V66,V67 >= 0,V = V65,V1 = V67,V66 >= 0,V64 >= 0]). input_output_vars(fun(V,V1,Out),[V,V1],[Out]). input_output_vars(and(V,V1,Out),[V,V1],[Out]). input_output_vars(eq(V,V1,Out),[V,V1],[Out]). input_output_vars(fun3(V,V1,Out),[V,V1],[Out]). input_output_vars(fun5(V,Out),[V],[Out]). input_output_vars(fun4(V,V1,V14,Out),[V,V1,V14],[Out]). input_output_vars(nub(V,Out),[V],[Out]). input_output_vars(fun6(V,Out),[V],[Out]). input_output_vars(remove(V,V1,Out),[V,V1],[Out]). input_output_vars(fun7(V,V1,Out),[V,V1],[Out]). input_output_vars(fun8(V,V1,V14,V30,Out),[V,V1,V14,V30],[Out]). input_output_vars(fun2(V,V1,Out),[V,V1],[Out]). input_output_vars(fun1(V,V1,Out),[V,V1],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. non_recursive : [fun2/3]
1. non_recursive : [and/3]
2. recursive [non_tail,multiple] : [fun1/3]
3. non_recursive : [fun/3]
4. non_recursive : [fun5/2]
5. recursive [non_tail] : [eq/3,fun3/3,fun4/4]
6. recursive : [fun7/3,fun8/5,remove/3]
7. recursive : [fun6/2,nub/2]
8. non_recursive : [start/4]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into fun2/3
1. SCC is completely evaluated into other SCCs
2. SCC is partially evaluated into fun1/3
3. SCC is completely evaluated into other SCCs
4. SCC is partially evaluated into fun5/2
5. SCC is partially evaluated into eq/3
6. SCC is partially evaluated into remove/3
7. SCC is partially evaluated into nub/2
8. SCC is partially evaluated into start/4
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations fun2/3
* CE 48 is refined into CE [52]
* CE 47 is refined into CE [53]
* CE 46 is refined into CE [54]
* CE 45 is refined into CE [55]
* CE 44 is refined into CE [56]
### Cost equations --> "Loop" of fun2/3
* CEs [52] --> Loop 31
* CEs [53] --> Loop 32
* CEs [54] --> Loop 33
* CEs [55] --> Loop 34
* CEs [56] --> Loop 35
### Ranking functions of CR fun2(V,V1,Out)
#### Partial ranking functions of CR fun2(V,V1,Out)
### Specialization of cost equations fun1/3
* CE 40 is refined into CE [57]
* CE 43 is refined into CE [58]
* CE 38 is refined into CE [59]
* CE 42 is refined into CE [60]
* CE 37 is refined into CE [61]
* CE 36 is refined into CE [62]
* CE 41 is refined into CE [63,64,65,66,67]
* CE 39 is refined into CE [68]
### Cost equations --> "Loop" of fun1/3
* CEs [68] --> Loop 36
* CEs [66] --> Loop 37
* CEs [65] --> Loop 38
* CEs [64] --> Loop 39
* CEs [63] --> Loop 40
* CEs [67] --> Loop 41
* CEs [57] --> Loop 42
* CEs [58] --> Loop 43
* CEs [59] --> Loop 44
* CEs [60] --> Loop 45
* CEs [61] --> Loop 46
* CEs [62] --> Loop 47
### Ranking functions of CR fun1(V,V1,Out)
* RF of phase [36,37,38,39,40,41]: [V,V1]
#### Partial ranking functions of CR fun1(V,V1,Out)
* Partial RF of phase [36,37,38,39,40,41]:
- RF of loop [36:1,37:1,37:2,38:1,38:2,39:1,39:2,40:1,40:2,41:1,41:2]:
V
V1
### Specialization of cost equations fun5/2
* CE 49 is refined into CE [69]
* CE 51 is refined into CE [70]
* CE 50 is refined into CE [71]
### Cost equations --> "Loop" of fun5/2
* CEs [69] --> Loop 48
* CEs [70] --> Loop 49
* CEs [71] --> Loop 50
### Ranking functions of CR fun5(V,Out)
#### Partial ranking functions of CR fun5(V,Out)
### Specialization of cost equations eq/3
* CE 31 is refined into CE [72]
* CE 34 is refined into CE [73]
* CE 32 is refined into CE [74]
* CE 35 is refined into CE [75,76,77]
* CE 33 is refined into CE [78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95]
### Cost equations --> "Loop" of eq/3
* CEs [87] --> Loop 51
* CEs [79] --> Loop 52
* CEs [85,94] --> Loop 53
* CEs [90] --> Loop 54
* CEs [82] --> Loop 55
* CEs [84,86,93] --> Loop 56
* CEs [89] --> Loop 57
* CEs [81] --> Loop 58
* CEs [78] --> Loop 59
* CEs [91] --> Loop 60
* CEs [83] --> Loop 61
* CEs [80,88,92,95] --> Loop 62
* CEs [74] --> Loop 63
* CEs [77] --> Loop 64
* CEs [72,73,76] --> Loop 65
* CEs [75] --> Loop 66
### Ranking functions of CR eq(V,V1,Out)
* RF of phase [51,52]: [V,V1]
* RF of phase [56,57,58,59]: [V,V1]
* RF of phase [60,61,62]: [V,V1]
#### Partial ranking functions of CR eq(V,V1,Out)
* Partial RF of phase [51,52]:
- RF of loop [51:1]:
V-1
V1-1
- RF of loop [52:1]:
V
V1
* Partial RF of phase [56,57,58,59]:
- RF of loop [56:1]:
V-1
V1-1
- RF of loop [57:1]:
V/2-1/2
- RF of loop [57:1,59:1]:
V1
- RF of loop [58:1]:
V1/2-1/2
- RF of loop [58:1,59:1]:
V
* Partial RF of phase [60,61,62]:
- RF of loop [60:1]:
V/2-1/2
- RF of loop [60:1,62:1]:
V1
- RF of loop [61:1]:
V1/2-1/2
- RF of loop [61:1,62:1]:
V
### Specialization of cost equations remove/3
* CE 23 is refined into CE [96,97,98,99,100,101,102]
* CE 26 is refined into CE [103]
* CE 27 is refined into CE [104]
* CE 25 is refined into CE [105,106,107,108]
* CE 24 is refined into CE [109,110]
### Cost equations --> "Loop" of remove/3
* CEs [110] --> Loop 67
* CEs [107] --> Loop 68
* CEs [106,108] --> Loop 69
* CEs [105] --> Loop 70
* CEs [109] --> Loop 71
* CEs [104] --> Loop 72
* CEs [96,97,98,99,100,101,102,103] --> Loop 73
### Ranking functions of CR remove(V,V1,Out)
* RF of phase [67,68,69,70,71]: [V1/2-1/2]
#### Partial ranking functions of CR remove(V,V1,Out)
* Partial RF of phase [67,68,69,70,71]:
- RF of loop [67:1,69:1]:
V1/3-2/3
- RF of loop [68:1,70:1,71:1]:
V1/2-1/2
### Specialization of cost equations nub/2
* CE 30 is refined into CE [111,112,113]
* CE 28 is refined into CE [114]
* CE 29 is refined into CE [115]
### Cost equations --> "Loop" of nub/2
* CEs [114] --> Loop 74
* CEs [115] --> Loop 75
* CEs [113] --> Loop 76
* CEs [111] --> Loop 77
* CEs [112] --> Loop 78
### Ranking functions of CR nub(V,Out)
* RF of phase [76]: [V-3]
#### Partial ranking functions of CR nub(V,Out)
* Partial RF of phase [76]:
- RF of loop [76:1]:
V-3
### Specialization of cost equations start/4
* CE 11 is refined into CE [116]
* CE 7 is refined into CE [117,118,119]
* CE 2 is refined into CE [120]
* CE 3 is refined into CE [121]
* CE 4 is refined into CE [122,123,124,125,126,127,128,129]
* CE 5 is refined into CE [130,131,132,133,134,135,136]
* CE 6 is refined into CE [137,138,139,140,141,142]
* CE 8 is refined into CE [143,144,145,146,147,148,149,150,151,152,153,154]
* CE 9 is refined into CE [155,156,157]
* CE 10 is refined into CE [158]
* CE 12 is refined into CE [159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200,201,202,203,204,205,206,207,208,209,210,211,212,213,214,215,216,217,218,219,220,221,222,223,224,225,226,227,228,229,230,231,232,233,234,235,236]
* CE 13 is refined into CE [237,238,239,240,241,242,243,244,245,246,247,248,249,250,251,252,253,254,255,256,257,258,259,260,261,262,263,264,265,266,267,268,269,270,271,272,273,274,275,276,277,278,279,280,281,282,283,284,285,286,287,288,289,290,291,292,293,294,295,296,297,298,299,300,301,302,303,304,305,306,307,308,309,310,311,312,313,314]
* CE 14 is refined into CE [315,316,317]
* CE 15 is refined into CE [318,319,320,321,322,323]
* CE 16 is refined into CE [324,325,326,327,328]
* CE 17 is refined into CE [329,330,331,332,333,334,335]
* CE 18 is refined into CE [336,337,338]
* CE 19 is refined into CE [339,340,341,342,343]
* CE 20 is refined into CE [344,345,346]
* CE 21 is refined into CE [347,348,349,350,351]
* CE 22 is refined into CE [352,353,354,355,356,357]
### Cost equations --> "Loop" of start/4
* CEs [167,168,212,213] --> Loop 79
* CEs [165,166,204,205,210,211,333] --> Loop 80
* CEs [239,240,250,251,252,253,263,264,265,266,267,268,284,285,295,296,302,303,304,305] --> Loop 81
* CEs [152] --> Loop 82
* CEs [137,149,290,291] --> Loop 83
* CEs [245,246] --> Loop 84
* CEs [117,118,119] --> Loop 85
* CEs [282,283,288,289] --> Loop 86
* CEs [159,160,161,162,172,173,174,175,327,350] --> Loop 87
* CEs [116,130,131,138,139,143,144,145,326,332,344,349] --> Loop 88
* CEs [237,238,241,242,243,244,247,248,249,254,255,256,257,258,259,260,261,262,321,355] --> Loop 89
* CEs [121,155,156,157,315,316,317,324,325,329,330,336,347,348] --> Loop 90
* CEs [319,353] --> Loop 91
* CEs [120,122,123,124,125,126,127,128,129,132,133,134,135,136,140,141,142,146,147,148,150,151,153,154,158,163,164,169,170,171,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200,201,202,203,206,207,208,209,214,215,216,217,218,219,220,221,222,223,224,225,226,227,228,229,230,231,232,233,234,235,236,269,270,271,272,273,274,275,276,277,278,279,280,281,286,287,292,293,294,297,298,299,300,301,306,307,308,309,310,311,312,313,314,318,320,322,323,328,331,334,335,337,338,339,340,341,342,343,345,346,351,352,354,356,357] --> Loop 92
### Ranking functions of CR start(V,V1,V14,V30)
#### Partial ranking functions of CR start(V,V1,V14,V30)
Computing Bounds
=====================================
#### Cost of chains of fun2(V,V1,Out):
* Chain [35]: 0
with precondition: [V=1,V1=1,Out=1]
* Chain [34]: 0
with precondition: [V=1,V1=2,Out=1]
* Chain [33]: 0
with precondition: [V=2,V1=1,Out=1]
* Chain [32]: 0
with precondition: [V=2,V1=2,Out=2]
* Chain [31]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of fun1(V,V1,Out):
* Chain [47]: 0
with precondition: [V=0,V1=0,Out=2]
* Chain [46]: 0
with precondition: [V=0,Out=1,V1>=1]
* Chain [45]: 0
with precondition: [V=1,V1=1,Out=2]
* Chain [44]: 0
with precondition: [V1=0,Out=1,V>=1]
* Chain [43]: 0
with precondition: [Out=0,V>=0,V1>=0]
* Chain [42]: 0
with precondition: [Out=1,V>=1,V1>=1]
* Chain [multiple([36,37,38,39,40,41],[[47],[46],[45],[44],[43],[42]])]: 0
with precondition: [2>=Out,V>=1,V1>=1,Out>=0]
#### Cost of chains of fun5(V,Out):
* Chain [50]: 1
with precondition: [V=1,Out=2]
* Chain [49]: 0
with precondition: [Out=0,V>=0]
* Chain [48]: 1
with precondition: [Out=1,V>=1]
#### Cost of chains of eq(V,V1,Out):
* Chain [[60,61,62],[56,57,58,59],64]: 30*it(56)+5*it(60)+3
Such that:it(60) =< V/2
aux(26) =< V
aux(27) =< V1
it(56) =< aux(26)
it(56) =< aux(27)
it(60) =< aux(26)
it(60) =< aux(27)
with precondition: [Out=0,V>=3,V1>=3]
* Chain [[60,61,62],[56,57,58,59],63]: 35*it(56)+3
Such that:aux(30) =< V
aux(31) =< V1
it(56) =< aux(30)
it(56) =< aux(31)
with precondition: [Out=0,V>=3,V1>=3]
* Chain [[60,61,62],[56,57,58,59],55,[51,52],66]: 45*it(51)+8
Such that:aux(40) =< V
aux(41) =< V1
it(51) =< aux(40)
it(51) =< aux(41)
with precondition: [Out=0,V>=5,V1>=6]
* Chain [[60,61,62],[56,57,58,59],55,66]: 35*it(56)+8
Such that:aux(44) =< V
aux(45) =< V1
it(56) =< aux(44)
it(56) =< aux(45)
with precondition: [Out=0,V>=4,V1>=5]
* Chain [[60,61,62],[56,57,58,59],54,[51,52],66]: 45*it(51)+8
Such that:aux(48) =< V
aux(49) =< V1
it(51) =< aux(48)
it(51) =< aux(49)
with precondition: [Out=0,V>=6,V1>=5]
* Chain [[60,61,62],[56,57,58,59],54,66]: 35*it(56)+8
Such that:aux(52) =< V
aux(53) =< V1
it(56) =< aux(52)
it(56) =< aux(53)
with precondition: [Out=0,V>=5,V1>=4]
* Chain [[60,61,62],[56,57,58,59],53,[51,52],66]: 45*it(51)+8
Such that:aux(56) =< V
aux(57) =< V1
it(51) =< aux(56)
it(51) =< aux(57)
with precondition: [Out=0,V>=6,V1>=6]
* Chain [[60,61,62],[56,57,58,59],53,66]: 35*it(56)+8
Such that:aux(60) =< V
aux(61) =< V1
it(56) =< aux(60)
it(56) =< aux(61)
with precondition: [Out=0,V>=5,V1>=5]
* Chain [[60,61,62],[51,52],66]: 25*it(51)+3
Such that:aux(62) =< V
aux(63) =< V1
it(51) =< aux(62)
it(51) =< aux(63)
with precondition: [Out=0,V>=3,V1>=3]
* Chain [[60,61,62],66]: 5*it(60)+5*it(61)+5*it(62)+3
Such that:it(60) =< V/2
it(61) =< V1/2
aux(64) =< V
aux(65) =< V1
it(60) =< aux(64)
it(61) =< aux(64)
it(62) =< aux(64)
it(60) =< aux(65)
it(61) =< aux(65)
it(62) =< aux(65)
with precondition: [Out=0,V>=2,V1>=2]
* Chain [[60,61,62],65]: 5*it(60)+5*it(61)+5*it(62)+2
Such that:it(60) =< V/2
it(61) =< V1/2
aux(66) =< V
aux(67) =< V1
it(60) =< aux(66)
it(61) =< aux(66)
it(62) =< aux(66)
it(60) =< aux(67)
it(61) =< aux(67)
it(62) =< aux(67)
with precondition: [Out=0,V>=1,V1>=1]
* Chain [[60,61,62],64]: 5*it(60)+5*it(61)+5*it(62)+3
Such that:it(60) =< V/2
it(61) =< V1/2
aux(68) =< V
aux(69) =< V1
it(60) =< aux(68)
it(61) =< aux(68)
it(62) =< aux(68)
it(60) =< aux(69)
it(61) =< aux(69)
it(62) =< aux(69)
with precondition: [Out=0,V>=2,V1>=2]
* Chain [[60,61,62],63]: 5*it(60)+5*it(61)+5*it(62)+3
Such that:it(60) =< V/2
it(61) =< V1/2
aux(70) =< V
aux(71) =< V1
it(60) =< aux(70)
it(61) =< aux(70)
it(62) =< aux(70)
it(60) =< aux(71)
it(61) =< aux(71)
it(62) =< aux(71)
with precondition: [Out=0,V>=2,V1>=2]
* Chain [[60,61,62],55,[51,52],66]: 25*it(51)+8
Such that:aux(72) =< V
aux(73) =< V1
it(51) =< aux(72)
it(51) =< aux(73)
with precondition: [Out=0,V>=4,V1>=5]
* Chain [[60,61,62],55,66]: 5*it(60)+5*it(61)+5*it(62)+8
Such that:it(60) =< V/2
it(61) =< V1/2
aux(74) =< V
aux(75) =< V1
it(60) =< aux(74)
it(61) =< aux(74)
it(62) =< aux(74)
it(60) =< aux(75)
it(61) =< aux(75)
it(62) =< aux(75)
with precondition: [Out=0,V>=3,V1>=4]
* Chain [[60,61,62],54,[51,52],66]: 25*it(51)+8
Such that:aux(76) =< V
aux(77) =< V1
it(51) =< aux(76)
it(51) =< aux(77)
with precondition: [Out=0,V>=5,V1>=4]
* Chain [[60,61,62],54,66]: 5*it(60)+5*it(61)+5*it(62)+8
Such that:it(60) =< V/2
it(61) =< V1/2
aux(78) =< V
aux(79) =< V1
it(60) =< aux(78)
it(61) =< aux(78)
it(62) =< aux(78)
it(60) =< aux(79)
it(61) =< aux(79)
it(62) =< aux(79)
with precondition: [Out=0,V>=4,V1>=3]
* Chain [[60,61,62],53,[51,52],66]: 25*it(51)+8
Such that:aux(80) =< V
aux(81) =< V1
it(51) =< aux(80)
it(51) =< aux(81)
with precondition: [Out=0,V>=5,V1>=5]
* Chain [[60,61,62],53,66]: 5*it(60)+5*it(61)+5*it(62)+8
Such that:it(60) =< V/2
it(61) =< V1/2
aux(82) =< V
aux(83) =< V1
it(60) =< aux(82)
it(61) =< aux(82)
it(62) =< aux(82)
it(60) =< aux(83)
it(61) =< aux(83)
it(62) =< aux(83)
with precondition: [Out=0,V>=4,V1>=4]
* Chain [[56,57,58,59],64]: 10*it(56)+5*it(57)+5*it(58)+3
Such that:it(57) =< V/2
it(58) =< V1/2
aux(20) =< V
aux(21) =< V1
it(56) =< aux(20)
it(57) =< aux(20)
it(58) =< aux(20)
it(56) =< aux(21)
it(57) =< aux(21)
it(58) =< aux(21)
with precondition: [Out=1,V>=2,V1>=2]
* Chain [[56,57,58,59],63]: 10*it(56)+5*it(57)+5*it(58)+3
Such that:it(57) =< V/2
it(58) =< V1/2
aux(28) =< V
aux(29) =< V1
it(56) =< aux(28)
it(57) =< aux(28)
it(58) =< aux(28)
it(56) =< aux(29)
it(57) =< aux(29)
it(58) =< aux(29)
with precondition: [Out=1,V>=2,V1>=2]
* Chain [[56,57,58,59],55,[51,52],66]: 30*it(51)+8
Such that:aux(38) =< V
aux(39) =< V1
it(51) =< aux(38)
it(51) =< aux(39)
with precondition: [Out=1,V>=4,V1>=5]
* Chain [[56,57,58,59],55,66]: 10*it(56)+5*it(57)+5*it(58)+8
Such that:it(57) =< V/2
it(58) =< V1/2
aux(42) =< V
aux(43) =< V1
it(56) =< aux(42)
it(57) =< aux(42)
it(58) =< aux(42)
it(56) =< aux(43)
it(57) =< aux(43)
it(58) =< aux(43)
with precondition: [Out=1,V>=3,V1>=4]
* Chain [[56,57,58,59],54,[51,52],66]: 30*it(51)+8
Such that:aux(46) =< V
aux(47) =< V1
it(51) =< aux(46)
it(51) =< aux(47)
with precondition: [Out=1,V>=5,V1>=4]
* Chain [[56,57,58,59],54,66]: 10*it(56)+5*it(57)+5*it(58)+8
Such that:it(57) =< V/2
it(58) =< V1/2
aux(50) =< V
aux(51) =< V1
it(56) =< aux(50)
it(57) =< aux(50)
it(58) =< aux(50)
it(56) =< aux(51)
it(57) =< aux(51)
it(58) =< aux(51)
with precondition: [Out=1,V>=4,V1>=3]
* Chain [[56,57,58,59],53,[51,52],66]: 30*it(51)+8
Such that:aux(54) =< V
aux(55) =< V1
it(51) =< aux(54)
it(51) =< aux(55)
with precondition: [Out=1,V>=5,V1>=5]
* Chain [[56,57,58,59],53,66]: 10*it(56)+5*it(57)+5*it(58)+8
Such that:it(57) =< V/2
it(58) =< V1/2
aux(58) =< V
aux(59) =< V1
it(56) =< aux(58)
it(57) =< aux(58)
it(58) =< aux(58)
it(56) =< aux(59)
it(57) =< aux(59)
it(58) =< aux(59)
with precondition: [Out=1,V>=4,V1>=4]
* Chain [[51,52],66]: 10*it(51)+3
Such that:aux(36) =< V
aux(37) =< V1
it(51) =< aux(36)
it(51) =< aux(37)
with precondition: [Out=2,V>=2,V1>=2]
* Chain [66]: 3
with precondition: [V=1,V1=1,Out=2]
* Chain [65]: 2
with precondition: [Out=0,V>=0,V1>=0]
* Chain [64]: 3
with precondition: [V=1,Out=1,V1>=1]
* Chain [63]: 3
with precondition: [V1=1,Out=1,V>=1]
* Chain [55,[51,52],66]: 10*it(51)+8
Such that:aux(36) =< V
aux(37) =< V1
it(51) =< aux(36)
it(51) =< aux(37)
with precondition: [Out=1,V>=3,V1>=4]
* Chain [55,66]: 8
with precondition: [V=2,Out=1,V1>=3]
* Chain [54,[51,52],66]: 10*it(51)+8
Such that:aux(36) =< V
aux(37) =< V1
it(51) =< aux(36)
it(51) =< aux(37)
with precondition: [Out=1,V>=4,V1>=3]
* Chain [54,66]: 8
with precondition: [V1=2,Out=1,V>=3]
* Chain [53,[51,52],66]: 10*it(51)+8
Such that:aux(36) =< V
aux(37) =< V1
it(51) =< aux(36)
it(51) =< aux(37)
with precondition: [Out=1,V>=4,V1>=4]
* Chain [53,66]: 8
with precondition: [Out=1,V>=3,V1>=3]
#### Cost of chains of remove(V,V1,Out):
* Chain [[67,68,69,70,71],73]: 17*it(67)+18*it(68)+65*s(120)+680*s(121)+10*s(153)+25*s(156)+25*s(157)+170*s(158)+10
Such that:aux(93) =< V/2
aux(104) =< V1/3
aux(106) =< V
aux(107) =< V1
aux(108) =< V1/2
s(120) =< aux(93)
s(121) =< aux(107)
s(121) =< aux(106)
s(120) =< aux(106)
s(120) =< aux(107)
it(68) =< aux(107)
it(67) =< aux(107)
it(67) =< aux(108)
it(68) =< aux(108)
it(67) =< aux(104)
aux(97) =< aux(106)
s(161) =< aux(107)* (1/2)
s(155) =< it(67)*aux(106)
aux(98) =< it(67)*aux(97)
s(162) =< aux(98)* (1/2)
s(156) =< s(162)
s(157) =< s(161)
s(158) =< aux(98)
s(158) =< aux(107)
s(156) =< aux(98)
s(157) =< aux(98)
s(156) =< aux(107)
s(157) =< aux(107)
s(153) =< s(155)
s(153) =< aux(107)
with precondition: [V>=1,V1>=2,Out>=0,V1>=Out]
* Chain [[67,68,69,70,71],72]: 6*it(67)+18*it(68)+11*it(69)+10*s(153)+25*s(156)+25*s(157)+170*s(158)+2
Such that:aux(96) =< V
aux(109) =< V1
aux(110) =< V1/2
aux(111) =< V1/3
it(68) =< aux(109)
it(69) =< aux(109)
it(67) =< aux(110)
it(68) =< aux(110)
it(69) =< aux(110)
it(67) =< aux(111)
it(69) =< aux(111)
aux(97) =< aux(96)
s(161) =< aux(109)* (1/2)
s(155) =< it(67)*aux(96)
aux(98) =< it(69)*aux(97)
s(162) =< aux(98)* (1/2)
s(156) =< s(162)
s(157) =< s(161)
s(158) =< aux(98)
s(158) =< aux(109)
s(156) =< aux(98)
s(157) =< aux(98)
s(156) =< aux(109)
s(157) =< aux(109)
s(153) =< s(155)
s(153) =< aux(109)
with precondition: [V>=1,V1>=3,Out>=1,V1>=Out]
* Chain [73]: 65*s(120)+60*s(121)+620*s(122)+10
Such that:aux(92) =< V
aux(93) =< V/2
aux(94) =< V1
aux(95) =< V1/2
s(120) =< aux(93)
s(121) =< aux(95)
s(122) =< aux(92)
s(122) =< aux(94)
s(120) =< aux(92)
s(121) =< aux(92)
s(120) =< aux(94)
s(121) =< aux(94)
with precondition: [Out=0,V>=0,V1>=0]
* Chain [72]: 2
with precondition: [V1=1,Out=1,V>=0]
#### Cost of chains of nub(V,Out):
* Chain [[76],78,74]: 757*it(76)+815*s(236)+50*s(237)+50*s(238)+340*s(239)+20*s(240)+13
Such that:aux(120) =< V
it(76) =< aux(120)
aux(118) =< aux(120)
s(241) =< it(76)*aux(118)
s(236) =< s(241)
s(244) =< s(241)* (1/2)
s(242) =< s(236)*aux(120)
s(243) =< s(236)*aux(118)
s(245) =< s(243)* (1/2)
s(237) =< s(245)
s(238) =< s(244)
s(239) =< s(243)
s(239) =< s(241)
s(237) =< s(243)
s(238) =< s(243)
s(237) =< s(241)
s(238) =< s(241)
s(240) =< s(242)
s(240) =< s(241)
with precondition: [V>=4,Out>=3,V>=Out]
* Chain [[76],77,78,74]: 12*it(76)+745*s(201)+815*s(236)+50*s(237)+50*s(238)+340*s(239)+20*s(240)+17
Such that:aux(116) =< 1
aux(121) =< V
it(76) =< aux(121)
s(201) =< aux(116)
aux(118) =< aux(121)
s(241) =< it(76)*aux(118)
s(236) =< s(241)
s(244) =< s(241)* (1/2)
s(242) =< s(236)*aux(121)
s(243) =< s(236)*aux(118)
s(245) =< s(243)* (1/2)
s(237) =< s(245)
s(238) =< s(244)
s(239) =< s(243)
s(239) =< s(241)
s(237) =< s(243)
s(238) =< s(243)
s(237) =< s(241)
s(238) =< s(241)
s(240) =< s(242)
s(240) =< s(241)
with precondition: [Out>=4,V>=Out]
* Chain [[76],77,75]: 12*it(76)+815*s(236)+50*s(237)+50*s(238)+340*s(239)+20*s(240)+6
Such that:aux(122) =< V
it(76) =< aux(122)
aux(118) =< aux(122)
s(241) =< it(76)*aux(118)
s(236) =< s(241)
s(244) =< s(241)* (1/2)
s(242) =< s(236)*aux(122)
s(243) =< s(236)*aux(118)
s(245) =< s(243)* (1/2)
s(237) =< s(245)
s(238) =< s(244)
s(239) =< s(243)
s(239) =< s(241)
s(237) =< s(243)
s(238) =< s(243)
s(237) =< s(241)
s(238) =< s(241)
s(240) =< s(242)
s(240) =< s(241)
with precondition: [Out>=4,V>=Out]
* Chain [[76],77,74]: 12*it(76)+815*s(236)+50*s(237)+50*s(238)+340*s(239)+20*s(240)+5
Such that:aux(123) =< V
it(76) =< aux(123)
aux(118) =< aux(123)
s(241) =< it(76)*aux(118)
s(236) =< s(241)
s(244) =< s(241)* (1/2)
s(242) =< s(236)*aux(123)
s(243) =< s(236)*aux(118)
s(245) =< s(243)* (1/2)
s(237) =< s(245)
s(238) =< s(244)
s(239) =< s(243)
s(239) =< s(241)
s(237) =< s(243)
s(238) =< s(243)
s(237) =< s(241)
s(238) =< s(241)
s(240) =< s(242)
s(240) =< s(241)
with precondition: [Out>=3,V>=Out+1]
* Chain [[76],75]: 12*it(76)+815*s(236)+50*s(237)+50*s(238)+340*s(239)+20*s(240)+2
Such that:aux(124) =< V
it(76) =< aux(124)
aux(118) =< aux(124)
s(241) =< it(76)*aux(118)
s(236) =< s(241)
s(244) =< s(241)* (1/2)
s(242) =< s(236)*aux(124)
s(243) =< s(236)*aux(118)
s(245) =< s(243)* (1/2)
s(237) =< s(245)
s(238) =< s(244)
s(239) =< s(243)
s(239) =< s(241)
s(237) =< s(243)
s(238) =< s(243)
s(237) =< s(241)
s(238) =< s(241)
s(240) =< s(242)
s(240) =< s(241)
with precondition: [Out>=3,V>=Out+1]
* Chain [[76],74]: 12*it(76)+815*s(236)+50*s(237)+50*s(238)+340*s(239)+20*s(240)+1
Such that:aux(125) =< V
it(76) =< aux(125)
aux(118) =< aux(125)
s(241) =< it(76)*aux(118)
s(236) =< s(241)
s(244) =< s(241)* (1/2)
s(242) =< s(236)*aux(125)
s(243) =< s(236)*aux(118)
s(245) =< s(243)* (1/2)
s(237) =< s(245)
s(238) =< s(244)
s(239) =< s(243)
s(239) =< s(241)
s(237) =< s(243)
s(238) =< s(243)
s(237) =< s(241)
s(238) =< s(241)
s(240) =< s(242)
s(240) =< s(241)
with precondition: [Out>=2,V>=Out+2]
* Chain [78,74]: 745*s(201)+13
Such that:aux(116) =< V
s(201) =< aux(116)
with precondition: [Out>=1,V>=Out]
* Chain [77,78,74]: 745*s(201)+17
Such that:aux(116) =< 1
s(201) =< aux(116)
with precondition: [V=Out,V>=2]
* Chain [77,75]: 6
with precondition: [V=Out,V>=2]
* Chain [77,74]: 5
with precondition: [V=Out+1,V>=2]
* Chain [75]: 2
with precondition: [V=1,Out=1]
* Chain [74]: 1
with precondition: [Out=0,V>=0]
#### Cost of chains of start(V,V1,V14,V30):
* Chain [92]: 3040*s(319)+4075*s(323)+250*s(328)+250*s(329)+1700*s(330)+100*s(331)+7804*s(336)+352*s(344)+200*s(352)+200*s(353)+1360*s(354)+80*s(355)+9780*s(366)+600*s(371)+600*s(372)+4080*s(373)+240*s(374)+50*s(451)+50*s(452)+340*s(453)+20*s(454)+1290*s(476)+965*s(477)+13225*s(478)+100*s(518)+100*s(519)+680*s(520)+40*s(521)+56*s(588)+12*s(589)+100*s(595)+100*s(596)+680*s(597)+20*s(598)+20*s(602)+360*s(797)+340*s(798)+3200*s(799)+36*s(958)+28*s(959)+6*s(960)+50*s(966)+50*s(967)+340*s(968)+10*s(969)+10*s(973)+773
Such that:s(957) =< V1/3
aux(144) =< 1
aux(145) =< V
aux(146) =< V/2
aux(147) =< V/3
aux(148) =< V1
aux(149) =< V1/2
aux(150) =< V14
aux(151) =< V14/2
s(319) =< aux(144)
s(321) =< aux(144)
s(322) =< s(319)*s(321)
s(323) =< s(322)
s(324) =< s(322)* (1/2)
s(325) =< s(323)*aux(144)
s(326) =< s(323)*s(321)
s(327) =< s(326)* (1/2)
s(328) =< s(327)
s(329) =< s(324)
s(330) =< s(326)
s(330) =< s(322)
s(328) =< s(326)
s(329) =< s(326)
s(328) =< s(322)
s(329) =< s(322)
s(331) =< s(325)
s(331) =< s(322)
s(336) =< aux(145)
s(347) =< aux(145)
s(365) =< s(336)*s(347)
s(366) =< s(365)
s(367) =< s(365)* (1/2)
s(368) =< s(366)*aux(145)
s(369) =< s(366)*s(347)
s(370) =< s(369)* (1/2)
s(371) =< s(370)
s(372) =< s(367)
s(373) =< s(369)
s(373) =< s(365)
s(371) =< s(369)
s(372) =< s(369)
s(371) =< s(365)
s(372) =< s(365)
s(374) =< s(368)
s(374) =< s(365)
s(344) =< aux(145)
s(344) =< aux(146)
s(348) =< aux(145)* (1/2)
s(349) =< s(344)*aux(145)
s(350) =< s(344)*s(347)
s(351) =< s(350)* (1/2)
s(352) =< s(351)
s(353) =< s(348)
s(354) =< s(350)
s(354) =< aux(145)
s(352) =< s(350)
s(353) =< s(350)
s(352) =< aux(145)
s(353) =< aux(145)
s(355) =< s(349)
s(355) =< aux(145)
s(448) =< s(336)*aux(145)
s(451) =< s(367)
s(452) =< s(348)
s(453) =< s(365)
s(453) =< aux(145)
s(451) =< s(365)
s(452) =< s(365)
s(451) =< aux(145)
s(452) =< aux(145)
s(454) =< s(448)
s(454) =< aux(145)
s(513) =< aux(148)
s(515) =< s(336)*aux(148)
s(516) =< s(336)*s(513)
s(517) =< s(516)* (1/2)
s(518) =< s(517)
s(519) =< s(348)
s(520) =< s(516)
s(520) =< aux(145)
s(518) =< s(516)
s(519) =< s(516)
s(518) =< aux(145)
s(519) =< aux(145)
s(521) =< s(515)
s(521) =< aux(145)
s(476) =< aux(149)
s(478) =< aux(145)
s(478) =< aux(148)
s(476) =< aux(148)
s(476) =< aux(145)
s(477) =< aux(146)
s(477) =< aux(148)
s(477) =< aux(145)
s(588) =< aux(145)
s(589) =< aux(146)
s(588) =< aux(146)
s(589) =< aux(147)
s(588) =< aux(147)
s(592) =< s(589)*aux(148)
s(593) =< s(588)*s(513)
s(594) =< s(593)* (1/2)
s(595) =< s(594)
s(596) =< s(348)
s(597) =< s(593)
s(597) =< aux(145)
s(595) =< s(593)
s(596) =< s(593)
s(595) =< aux(145)
s(596) =< aux(145)
s(598) =< s(592)
s(598) =< aux(145)
s(601) =< s(588)*aux(148)
s(602) =< s(601)
s(602) =< aux(145)
s(797) =< aux(151)
s(798) =< aux(146)
s(799) =< aux(150)
s(799) =< aux(145)
s(797) =< aux(150)
s(798) =< aux(150)
s(797) =< aux(145)
s(798) =< aux(145)
s(958) =< aux(148)
s(959) =< aux(148)
s(960) =< aux(149)
s(958) =< aux(149)
s(959) =< aux(149)
s(960) =< s(957)
s(959) =< s(957)
s(962) =< aux(148)* (1/2)
s(963) =< s(960)*aux(145)
s(964) =< s(959)*s(347)
s(965) =< s(964)* (1/2)
s(966) =< s(965)
s(967) =< s(962)
s(968) =< s(964)
s(968) =< aux(148)
s(966) =< s(964)
s(967) =< s(964)
s(966) =< aux(148)
s(967) =< aux(148)
s(969) =< s(963)
s(969) =< aux(148)
s(972) =< s(959)*aux(145)
s(973) =< s(972)
s(973) =< aux(148)
with precondition: [V>=0]
* Chain [91]: 1
with precondition: [V=0,V1>=1]
* Chain [90]: 130*s(978)+60*s(979)+1300*s(980)+36*s(986)+28*s(987)+6*s(988)+50*s(994)+50*s(995)+340*s(996)+10*s(997)+10*s(1001)+11
Such that:s(985) =< V30/3
aux(152) =< V1
aux(153) =< V1/2
aux(154) =< V30
aux(155) =< V30/2
s(978) =< aux(153)
s(979) =< aux(155)
s(980) =< aux(152)
s(980) =< aux(154)
s(978) =< aux(152)
s(979) =< aux(152)
s(978) =< aux(154)
s(979) =< aux(154)
s(986) =< aux(154)
s(987) =< aux(154)
s(988) =< aux(155)
s(986) =< aux(155)
s(987) =< aux(155)
s(988) =< s(985)
s(987) =< s(985)
s(989) =< aux(152)
s(990) =< aux(154)* (1/2)
s(991) =< s(988)*aux(152)
s(992) =< s(987)*s(989)
s(993) =< s(992)* (1/2)
s(994) =< s(993)
s(995) =< s(990)
s(996) =< s(992)
s(996) =< aux(154)
s(994) =< s(992)
s(995) =< s(992)
s(994) =< aux(154)
s(995) =< aux(154)
s(997) =< s(991)
s(997) =< aux(154)
s(1000) =< s(987)*aux(152)
s(1001) =< s(1000)
s(1001) =< aux(154)
with precondition: [V=1]
* Chain [89]: 180*s(1006)+170*s(1007)+1600*s(1008)+11
Such that:aux(156) =< V
aux(157) =< V/2
aux(158) =< V14
aux(159) =< V14/2
s(1006) =< aux(159)
s(1007) =< aux(157)
s(1008) =< aux(158)
s(1008) =< aux(156)
s(1006) =< aux(158)
s(1007) =< aux(158)
s(1006) =< aux(156)
s(1007) =< aux(156)
with precondition: [V1=0,V>=1]
* Chain [88]: 260*s(1060)+120*s(1061)+2600*s(1062)+72*s(1068)+56*s(1069)+12*s(1070)+100*s(1076)+100*s(1077)+680*s(1078)+20*s(1079)+20*s(1083)+15
Such that:aux(160) =< 1
aux(161) =< 1/2
aux(162) =< V
aux(163) =< V/2
aux(164) =< V/3
s(1060) =< aux(161)
s(1061) =< aux(163)
s(1062) =< aux(160)
s(1062) =< aux(162)
s(1060) =< aux(160)
s(1061) =< aux(160)
s(1060) =< aux(162)
s(1061) =< aux(162)
s(1068) =< aux(162)
s(1069) =< aux(162)
s(1070) =< aux(163)
s(1068) =< aux(163)
s(1069) =< aux(163)
s(1070) =< aux(164)
s(1069) =< aux(164)
s(1071) =< aux(160)
s(1072) =< aux(162)* (1/2)
s(1073) =< s(1070)*aux(160)
s(1074) =< s(1069)*s(1071)
s(1075) =< s(1074)* (1/2)
s(1076) =< s(1075)
s(1077) =< s(1072)
s(1078) =< s(1074)
s(1078) =< aux(162)
s(1076) =< s(1074)
s(1077) =< s(1074)
s(1076) =< aux(162)
s(1077) =< aux(162)
s(1079) =< s(1073)
s(1079) =< aux(162)
s(1082) =< s(1069)*aux(160)
s(1083) =< s(1082)
s(1083) =< aux(162)
with precondition: [V1=1,V>=0]
* Chain [87]: 7
with precondition: [V=2,V1>=2]
* Chain [86]: 6
with precondition: [V=2,V1>=1,V14>=1]
* Chain [85]: 130*s(1116)+60*s(1117)+1300*s(1118)+36*s(1124)+28*s(1125)+6*s(1126)+50*s(1132)+50*s(1133)+340*s(1134)+10*s(1135)+10*s(1139)+11
Such that:s(1123) =< V30/3
aux(165) =< V1
aux(166) =< V1/2
aux(167) =< V30
aux(168) =< V30/2
s(1116) =< aux(166)
s(1117) =< aux(168)
s(1118) =< aux(165)
s(1118) =< aux(167)
s(1116) =< aux(165)
s(1117) =< aux(165)
s(1116) =< aux(167)
s(1117) =< aux(167)
s(1124) =< aux(167)
s(1125) =< aux(167)
s(1126) =< aux(168)
s(1124) =< aux(168)
s(1125) =< aux(168)
s(1126) =< s(1123)
s(1125) =< s(1123)
s(1127) =< aux(165)
s(1128) =< aux(167)* (1/2)
s(1129) =< s(1126)*aux(165)
s(1130) =< s(1125)*s(1127)
s(1131) =< s(1130)* (1/2)
s(1132) =< s(1131)
s(1133) =< s(1128)
s(1134) =< s(1130)
s(1134) =< aux(167)
s(1132) =< s(1130)
s(1133) =< s(1130)
s(1132) =< aux(167)
s(1133) =< aux(167)
s(1135) =< s(1129)
s(1135) =< aux(167)
s(1138) =< s(1125)*aux(165)
s(1139) =< s(1138)
s(1139) =< aux(167)
with precondition: [V=2,V1>=0,V14>=0,V30>=0]
* Chain [84]: 11
with precondition: [V=3,V1=0,V14>=3]
* Chain [83]: 11
with precondition: [V=3,V1>=1]
* Chain [82]: 12
with precondition: [V=4,V1>=3]
* Chain [81]: 6
with precondition: [V14=1,V>=2,V1>=0]
* Chain [80]: 8
with precondition: [V1=2,V>=2]
* Chain [79]: 12
with precondition: [V1=3,V>=4]
Closed-form bounds of start(V,V1,V14,V30):
-------------------------------------
* Chain [92] with precondition: [V>=0]
- Upper bound: 25352*V+9938+15000*V*V+nat(V1)*499+nat(V14)*3200+1317/2*V+nat(V1/2)*1296+nat(V14/2)*360
- Complexity: n^2
* Chain [91] with precondition: [V=0,V1>=1]
- Upper bound: 1
- Complexity: constant
* Chain [90] with precondition: [V=1]
- Upper bound: nat(V1)*1300+11+nat(V30)*499+nat(V1/2)*130+nat(V30/2)*66
- Complexity: n
* Chain [89] with precondition: [V1=0,V>=1]
- Upper bound: nat(V14)*1600+11+85*V+nat(V14/2)*180
- Complexity: n
* Chain [88] with precondition: [V1=1,V>=0]
- Upper bound: 944*V+2865
- Complexity: n
* Chain [87] with precondition: [V=2,V1>=2]
- Upper bound: 7
- Complexity: constant
* Chain [86] with precondition: [V=2,V1>=1,V14>=1]
- Upper bound: 6
- Complexity: constant
* Chain [85] with precondition: [V=2,V1>=0,V14>=0,V30>=0]
- Upper bound: 1365*V1+532*V30+11
- Complexity: n
* Chain [84] with precondition: [V=3,V1=0,V14>=3]
- Upper bound: 11
- Complexity: constant
* Chain [83] with precondition: [V=3,V1>=1]
- Upper bound: 11
- Complexity: constant
* Chain [82] with precondition: [V=4,V1>=3]
- Upper bound: 12
- Complexity: constant
* Chain [81] with precondition: [V14=1,V>=2,V1>=0]
- Upper bound: 6
- Complexity: constant
* Chain [80] with precondition: [V1=2,V>=2]
- Upper bound: 8
- Complexity: constant
* Chain [79] with precondition: [V1=3,V>=4]
- Upper bound: 12
- Complexity: constant
### Maximum cost of start(V,V1,V14,V30): max([max([11,nat(V1)*1300+10+nat(V30)*499+nat(V1/2)*130+nat(V30/2)*66]),16*V+10+max([nat(V14)*1600+69*V+nat(V14/2)*180,24424*V+7073+15000*V*V+nat(V1)*499+nat(V14)*3200+1285/2*V+nat(V1/2)*1296+nat(V14/2)*360+ (928*V+2854)])])+1
Asymptotic class: n^2
* Total analysis performed in 3767 ms.