WORST_CASE(Omega(n^1),O(n^1)) proof of /export/starexec/sandbox2/benchmark/theBenchmark.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 778 ms] (2) CpxRelTRS (3) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (4) CpxWeightedTrs (5) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CpxTypedWeightedTrs (7) CompletionProof [UPPER BOUND(ID), 0 ms] (8) CpxTypedWeightedCompleteTrs (9) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (10) CpxRNTS (11) CompleteCoflocoProof [FINISHED, 57.1 s] (12) BOUNDS(1, n^1) (13) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (14) CpxRelTRS (15) SlicingProof [LOWER BOUND(ID), 0 ms] (16) CpxRelTRS (17) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (18) typed CpxTrs (19) OrderProof [LOWER BOUND(ID), 0 ms] (20) typed CpxTrs (21) RewriteLemmaProof [LOWER BOUND(ID), 319 ms] (22) BEST (23) proven lower bound (24) LowerBoundPropagationProof [FINISHED, 0 ms] (25) BOUNDS(n^1, INF) (26) typed CpxTrs (27) RewriteLemmaProof [LOWER BOUND(ID), 49 ms] (28) typed CpxTrs (29) RewriteLemmaProof [LOWER BOUND(ID), 11 ms] (30) typed CpxTrs (31) RewriteLemmaProof [LOWER BOUND(ID), 64 ms] (32) typed CpxTrs ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: HALF(0) -> c HALF(s(0)) -> c1 HALF(s(s(z0))) -> c2(HALF(z0)) LASTBIT(0) -> c3 LASTBIT(s(0)) -> c4 LASTBIT(s(s(z0))) -> c5(LASTBIT(z0)) ZERO(0) -> c6 ZERO(s(z0)) -> c7 CONV(z0) -> c8(CONVITER(z0, cons(0, nil))) CONVITER(z0, z1) -> c9(IF(zero(z0), z0, z1), ZERO(z0)) IF(true, z0, z1) -> c10 IF(false, z0, z1) -> c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0)) IF(false, z0, z1) -> c12(CONVITER(half(z0), cons(lastbit(z0), z1)), LASTBIT(z0)) The (relative) TRS S consists of the following rules: half(0) -> 0 half(s(0)) -> 0 half(s(s(z0))) -> s(half(z0)) lastbit(0) -> 0 lastbit(s(0)) -> s(0) lastbit(s(s(z0))) -> lastbit(z0) zero(0) -> true zero(s(z0)) -> false conv(z0) -> conviter(z0, cons(0, nil)) conviter(z0, z1) -> if(zero(z0), z0, z1) if(true, z0, z1) -> z1 if(false, z0, z1) -> conviter(half(z0), cons(lastbit(z0), z1)) Rewrite Strategy: INNERMOST ---------------------------------------- (1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID)) proved innermost termination of relative rules ---------------------------------------- (2) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: HALF(0) -> c HALF(s(0)) -> c1 HALF(s(s(z0))) -> c2(HALF(z0)) LASTBIT(0) -> c3 LASTBIT(s(0)) -> c4 LASTBIT(s(s(z0))) -> c5(LASTBIT(z0)) ZERO(0) -> c6 ZERO(s(z0)) -> c7 CONV(z0) -> c8(CONVITER(z0, cons(0, nil))) CONVITER(z0, z1) -> c9(IF(zero(z0), z0, z1), ZERO(z0)) IF(true, z0, z1) -> c10 IF(false, z0, z1) -> c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0)) IF(false, z0, z1) -> c12(CONVITER(half(z0), cons(lastbit(z0), z1)), LASTBIT(z0)) The (relative) TRS S consists of the following rules: half(0) -> 0 half(s(0)) -> 0 half(s(s(z0))) -> s(half(z0)) lastbit(0) -> 0 lastbit(s(0)) -> s(0) lastbit(s(s(z0))) -> lastbit(z0) zero(0) -> true zero(s(z0)) -> false conv(z0) -> conviter(z0, cons(0, nil)) conviter(z0, z1) -> if(zero(z0), z0, z1) if(true, z0, z1) -> z1 if(false, z0, z1) -> conviter(half(z0), cons(lastbit(z0), z1)) Rewrite Strategy: INNERMOST ---------------------------------------- (3) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID)) Transformed relative TRS to weighted TRS ---------------------------------------- (4) Obligation: The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1). The TRS R consists of the following rules: HALF(0) -> c [1] HALF(s(0)) -> c1 [1] HALF(s(s(z0))) -> c2(HALF(z0)) [1] LASTBIT(0) -> c3 [1] LASTBIT(s(0)) -> c4 [1] LASTBIT(s(s(z0))) -> c5(LASTBIT(z0)) [1] ZERO(0) -> c6 [1] ZERO(s(z0)) -> c7 [1] CONV(z0) -> c8(CONVITER(z0, cons(0, nil))) [1] CONVITER(z0, z1) -> c9(IF(zero(z0), z0, z1), ZERO(z0)) [1] IF(true, z0, z1) -> c10 [1] IF(false, z0, z1) -> c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0)) [1] IF(false, z0, z1) -> c12(CONVITER(half(z0), cons(lastbit(z0), z1)), LASTBIT(z0)) [1] half(0) -> 0 [0] half(s(0)) -> 0 [0] half(s(s(z0))) -> s(half(z0)) [0] lastbit(0) -> 0 [0] lastbit(s(0)) -> s(0) [0] lastbit(s(s(z0))) -> lastbit(z0) [0] zero(0) -> true [0] zero(s(z0)) -> false [0] conv(z0) -> conviter(z0, cons(0, nil)) [0] conviter(z0, z1) -> if(zero(z0), z0, z1) [0] if(true, z0, z1) -> z1 [0] if(false, z0, z1) -> conviter(half(z0), cons(lastbit(z0), z1)) [0] Rewrite Strategy: INNERMOST ---------------------------------------- (5) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (6) Obligation: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: HALF(0) -> c [1] HALF(s(0)) -> c1 [1] HALF(s(s(z0))) -> c2(HALF(z0)) [1] LASTBIT(0) -> c3 [1] LASTBIT(s(0)) -> c4 [1] LASTBIT(s(s(z0))) -> c5(LASTBIT(z0)) [1] ZERO(0) -> c6 [1] ZERO(s(z0)) -> c7 [1] CONV(z0) -> c8(CONVITER(z0, cons(0, nil))) [1] CONVITER(z0, z1) -> c9(IF(zero(z0), z0, z1), ZERO(z0)) [1] IF(true, z0, z1) -> c10 [1] IF(false, z0, z1) -> c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0)) [1] IF(false, z0, z1) -> c12(CONVITER(half(z0), cons(lastbit(z0), z1)), LASTBIT(z0)) [1] half(0) -> 0 [0] half(s(0)) -> 0 [0] half(s(s(z0))) -> s(half(z0)) [0] lastbit(0) -> 0 [0] lastbit(s(0)) -> s(0) [0] lastbit(s(s(z0))) -> lastbit(z0) [0] zero(0) -> true [0] zero(s(z0)) -> false [0] conv(z0) -> conviter(z0, cons(0, nil)) [0] conviter(z0, z1) -> if(zero(z0), z0, z1) [0] if(true, z0, z1) -> z1 [0] if(false, z0, z1) -> conviter(half(z0), cons(lastbit(z0), z1)) [0] The TRS has the following type information: HALF :: 0:s -> c:c1:c2 0 :: 0:s c :: c:c1:c2 s :: 0:s -> 0:s c1 :: c:c1:c2 c2 :: c:c1:c2 -> c:c1:c2 LASTBIT :: 0:s -> c3:c4:c5 c3 :: c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 -> c3:c4:c5 ZERO :: 0:s -> c6:c7 c6 :: c6:c7 c7 :: c6:c7 CONV :: 0:s -> c8 c8 :: c9 -> c8 CONVITER :: 0:s -> nil:cons -> c9 cons :: 0:s -> nil:cons -> nil:cons nil :: nil:cons c9 :: c10:c11:c12 -> c6:c7 -> c9 IF :: true:false -> 0:s -> nil:cons -> c10:c11:c12 zero :: 0:s -> true:false true :: true:false c10 :: c10:c11:c12 false :: true:false c11 :: c9 -> c:c1:c2 -> c10:c11:c12 half :: 0:s -> 0:s lastbit :: 0:s -> 0:s c12 :: c9 -> c3:c4:c5 -> c10:c11:c12 conv :: 0:s -> nil:cons conviter :: 0:s -> nil:cons -> nil:cons if :: true:false -> 0:s -> nil:cons -> nil:cons Rewrite Strategy: INNERMOST ---------------------------------------- (7) CompletionProof (UPPER BOUND(ID)) The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added: half(v0) -> null_half [0] lastbit(v0) -> null_lastbit [0] zero(v0) -> null_zero [0] conv(v0) -> null_conv [0] conviter(v0, v1) -> null_conviter [0] if(v0, v1, v2) -> null_if [0] HALF(v0) -> null_HALF [0] LASTBIT(v0) -> null_LASTBIT [0] ZERO(v0) -> null_ZERO [0] IF(v0, v1, v2) -> null_IF [0] And the following fresh constants: null_half, null_lastbit, null_zero, null_conv, null_conviter, null_if, null_HALF, null_LASTBIT, null_ZERO, null_IF, const, const1 ---------------------------------------- (8) Obligation: Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: HALF(0) -> c [1] HALF(s(0)) -> c1 [1] HALF(s(s(z0))) -> c2(HALF(z0)) [1] LASTBIT(0) -> c3 [1] LASTBIT(s(0)) -> c4 [1] LASTBIT(s(s(z0))) -> c5(LASTBIT(z0)) [1] ZERO(0) -> c6 [1] ZERO(s(z0)) -> c7 [1] CONV(z0) -> c8(CONVITER(z0, cons(0, nil))) [1] CONVITER(z0, z1) -> c9(IF(zero(z0), z0, z1), ZERO(z0)) [1] IF(true, z0, z1) -> c10 [1] IF(false, z0, z1) -> c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0)) [1] IF(false, z0, z1) -> c12(CONVITER(half(z0), cons(lastbit(z0), z1)), LASTBIT(z0)) [1] half(0) -> 0 [0] half(s(0)) -> 0 [0] half(s(s(z0))) -> s(half(z0)) [0] lastbit(0) -> 0 [0] lastbit(s(0)) -> s(0) [0] lastbit(s(s(z0))) -> lastbit(z0) [0] zero(0) -> true [0] zero(s(z0)) -> false [0] conv(z0) -> conviter(z0, cons(0, nil)) [0] conviter(z0, z1) -> if(zero(z0), z0, z1) [0] if(true, z0, z1) -> z1 [0] if(false, z0, z1) -> conviter(half(z0), cons(lastbit(z0), z1)) [0] half(v0) -> null_half [0] lastbit(v0) -> null_lastbit [0] zero(v0) -> null_zero [0] conv(v0) -> null_conv [0] conviter(v0, v1) -> null_conviter [0] if(v0, v1, v2) -> null_if [0] HALF(v0) -> null_HALF [0] LASTBIT(v0) -> null_LASTBIT [0] ZERO(v0) -> null_ZERO [0] IF(v0, v1, v2) -> null_IF [0] The TRS has the following type information: HALF :: 0:s:null_half:null_lastbit -> c:c1:c2:null_HALF 0 :: 0:s:null_half:null_lastbit c :: c:c1:c2:null_HALF s :: 0:s:null_half:null_lastbit -> 0:s:null_half:null_lastbit c1 :: c:c1:c2:null_HALF c2 :: c:c1:c2:null_HALF -> c:c1:c2:null_HALF LASTBIT :: 0:s:null_half:null_lastbit -> c3:c4:c5:null_LASTBIT c3 :: c3:c4:c5:null_LASTBIT c4 :: c3:c4:c5:null_LASTBIT c5 :: c3:c4:c5:null_LASTBIT -> c3:c4:c5:null_LASTBIT ZERO :: 0:s:null_half:null_lastbit -> c6:c7:null_ZERO c6 :: c6:c7:null_ZERO c7 :: c6:c7:null_ZERO CONV :: 0:s:null_half:null_lastbit -> c8 c8 :: c9 -> c8 CONVITER :: 0:s:null_half:null_lastbit -> nil:cons:null_conv:null_conviter:null_if -> c9 cons :: 0:s:null_half:null_lastbit -> nil:cons:null_conv:null_conviter:null_if -> nil:cons:null_conv:null_conviter:null_if nil :: nil:cons:null_conv:null_conviter:null_if c9 :: c10:c11:c12:null_IF -> c6:c7:null_ZERO -> c9 IF :: true:false:null_zero -> 0:s:null_half:null_lastbit -> nil:cons:null_conv:null_conviter:null_if -> c10:c11:c12:null_IF zero :: 0:s:null_half:null_lastbit -> true:false:null_zero true :: true:false:null_zero c10 :: c10:c11:c12:null_IF false :: true:false:null_zero c11 :: c9 -> c:c1:c2:null_HALF -> c10:c11:c12:null_IF half :: 0:s:null_half:null_lastbit -> 0:s:null_half:null_lastbit lastbit :: 0:s:null_half:null_lastbit -> 0:s:null_half:null_lastbit c12 :: c9 -> c3:c4:c5:null_LASTBIT -> c10:c11:c12:null_IF conv :: 0:s:null_half:null_lastbit -> nil:cons:null_conv:null_conviter:null_if conviter :: 0:s:null_half:null_lastbit -> nil:cons:null_conv:null_conviter:null_if -> nil:cons:null_conv:null_conviter:null_if if :: true:false:null_zero -> 0:s:null_half:null_lastbit -> nil:cons:null_conv:null_conviter:null_if -> nil:cons:null_conv:null_conviter:null_if null_half :: 0:s:null_half:null_lastbit null_lastbit :: 0:s:null_half:null_lastbit null_zero :: true:false:null_zero null_conv :: nil:cons:null_conv:null_conviter:null_if null_conviter :: nil:cons:null_conv:null_conviter:null_if null_if :: nil:cons:null_conv:null_conviter:null_if null_HALF :: c:c1:c2:null_HALF null_LASTBIT :: c3:c4:c5:null_LASTBIT null_ZERO :: c6:c7:null_ZERO null_IF :: c10:c11:c12:null_IF const :: c8 const1 :: c9 Rewrite Strategy: INNERMOST ---------------------------------------- (9) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: 0 => 0 c => 0 c1 => 1 c3 => 0 c4 => 1 c6 => 1 c7 => 2 nil => 0 true => 2 c10 => 0 false => 1 null_half => 0 null_lastbit => 0 null_zero => 0 null_conv => 0 null_conviter => 0 null_if => 0 null_HALF => 0 null_LASTBIT => 0 null_ZERO => 0 null_IF => 0 const => 0 const1 => 0 ---------------------------------------- (10) Obligation: Complexity RNTS consisting of the following rules: CONV(z) -{ 1 }-> 1 + CONVITER(z0, 1 + 0 + 0) :|: z = z0, z0 >= 0 CONVITER(z, z') -{ 1 }-> 1 + IF(zero(z0), z0, z1) + ZERO(z0) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0 HALF(z) -{ 1 }-> 1 :|: z = 1 + 0 HALF(z) -{ 1 }-> 0 :|: z = 0 HALF(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 HALF(z) -{ 1 }-> 1 + HALF(z0) :|: z0 >= 0, z = 1 + (1 + z0) IF(z, z', z'') -{ 1 }-> 0 :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1 IF(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0 IF(z, z', z'') -{ 1 }-> 1 + CONVITER(half(z0), 1 + lastbit(z0) + z1) + LASTBIT(z0) :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1 IF(z, z', z'') -{ 1 }-> 1 + CONVITER(half(z0), 1 + lastbit(z0) + z1) + HALF(z0) :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1 LASTBIT(z) -{ 1 }-> 1 :|: z = 1 + 0 LASTBIT(z) -{ 1 }-> 0 :|: z = 0 LASTBIT(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 LASTBIT(z) -{ 1 }-> 1 + LASTBIT(z0) :|: z0 >= 0, z = 1 + (1 + z0) ZERO(z) -{ 1 }-> 2 :|: z = 1 + z0, z0 >= 0 ZERO(z) -{ 1 }-> 1 :|: z = 0 ZERO(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 conv(z) -{ 0 }-> conviter(z0, 1 + 0 + 0) :|: z = z0, z0 >= 0 conv(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 conviter(z, z') -{ 0 }-> if(zero(z0), z0, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0 conviter(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 half(z) -{ 0 }-> 0 :|: z = 0 half(z) -{ 0 }-> 0 :|: z = 1 + 0 half(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 half(z) -{ 0 }-> 1 + half(z0) :|: z0 >= 0, z = 1 + (1 + z0) if(z, z', z'') -{ 0 }-> z1 :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1 if(z, z', z'') -{ 0 }-> conviter(half(z0), 1 + lastbit(z0) + z1) :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1 if(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0 lastbit(z) -{ 0 }-> lastbit(z0) :|: z0 >= 0, z = 1 + (1 + z0) lastbit(z) -{ 0 }-> 0 :|: z = 0 lastbit(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 lastbit(z) -{ 0 }-> 1 + 0 :|: z = 1 + 0 zero(z) -{ 0 }-> 2 :|: z = 0 zero(z) -{ 0 }-> 1 :|: z = 1 + z0, z0 >= 0 zero(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 Only complete derivations are relevant for the runtime complexity. ---------------------------------------- (11) CompleteCoflocoProof (FINISHED) Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo: eq(start(V, V5, V9),0,[fun(V, Out)],[V >= 0]). eq(start(V, V5, V9),0,[fun1(V, Out)],[V >= 0]). eq(start(V, V5, V9),0,[fun2(V, Out)],[V >= 0]). eq(start(V, V5, V9),0,[fun3(V, Out)],[V >= 0]). eq(start(V, V5, V9),0,[fun4(V, V5, Out)],[V >= 0,V5 >= 0]). eq(start(V, V5, V9),0,[fun5(V, V5, V9, Out)],[V >= 0,V5 >= 0,V9 >= 0]). eq(start(V, V5, V9),0,[half(V, Out)],[V >= 0]). eq(start(V, V5, V9),0,[lastbit(V, Out)],[V >= 0]). eq(start(V, V5, V9),0,[zero(V, Out)],[V >= 0]). eq(start(V, V5, V9),0,[conv(V, Out)],[V >= 0]). eq(start(V, V5, V9),0,[conviter(V, V5, Out)],[V >= 0,V5 >= 0]). eq(start(V, V5, V9),0,[if(V, V5, V9, Out)],[V >= 0,V5 >= 0,V9 >= 0]). eq(fun(V, Out),1,[],[Out = 0,V = 0]). eq(fun(V, Out),1,[],[Out = 1,V = 1]). eq(fun(V, Out),1,[fun(V1, Ret1)],[Out = 1 + Ret1,V1 >= 0,V = 2 + V1]). eq(fun1(V, Out),1,[],[Out = 0,V = 0]). eq(fun1(V, Out),1,[],[Out = 1,V = 1]). eq(fun1(V, Out),1,[fun1(V2, Ret11)],[Out = 1 + Ret11,V2 >= 0,V = 2 + V2]). eq(fun2(V, Out),1,[],[Out = 1,V = 0]). eq(fun2(V, Out),1,[],[Out = 2,V = 1 + V3,V3 >= 0]). eq(fun3(V, Out),1,[fun4(V4, 1 + 0 + 0, Ret12)],[Out = 1 + Ret12,V = V4,V4 >= 0]). eq(fun4(V, V5, Out),1,[zero(V6, Ret010),fun5(Ret010, V6, V7, Ret01),fun2(V6, Ret13)],[Out = 1 + Ret01 + Ret13,V = V6,V7 >= 0,V5 = V7,V6 >= 0]). eq(fun5(V, V5, V9, Out),1,[],[Out = 0,V = 2,V10 >= 0,V8 >= 0,V5 = V8,V9 = V10]). eq(fun5(V, V5, V9, Out),1,[half(V11, Ret0101),lastbit(V11, Ret01101),fun4(Ret0101, 1 + Ret01101 + V12, Ret011),fun(V11, Ret14)],[Out = 1 + Ret011 + Ret14,V12 >= 0,V = 1,V11 >= 0,V5 = V11,V9 = V12]). eq(fun5(V, V5, V9, Out),1,[half(V14, Ret0102),lastbit(V14, Ret011011),fun4(Ret0102, 1 + Ret011011 + V13, Ret012),fun1(V14, Ret15)],[Out = 1 + Ret012 + Ret15,V13 >= 0,V = 1,V14 >= 0,V5 = V14,V9 = V13]). eq(half(V, Out),0,[],[Out = 0,V = 0]). eq(half(V, Out),0,[],[Out = 0,V = 1]). eq(half(V, Out),0,[half(V15, Ret16)],[Out = 1 + Ret16,V15 >= 0,V = 2 + V15]). eq(lastbit(V, Out),0,[],[Out = 0,V = 0]). eq(lastbit(V, Out),0,[],[Out = 1,V = 1]). eq(lastbit(V, Out),0,[lastbit(V16, Ret)],[Out = Ret,V16 >= 0,V = 2 + V16]). eq(zero(V, Out),0,[],[Out = 2,V = 0]). eq(zero(V, Out),0,[],[Out = 1,V = 1 + V17,V17 >= 0]). eq(conv(V, Out),0,[conviter(V18, 1 + 0 + 0, Ret2)],[Out = Ret2,V = V18,V18 >= 0]). eq(conviter(V, V5, Out),0,[zero(V20, Ret0),if(Ret0, V20, V19, Ret3)],[Out = Ret3,V = V20,V19 >= 0,V5 = V19,V20 >= 0]). eq(if(V, V5, V9, Out),0,[],[Out = V21,V = 2,V21 >= 0,V22 >= 0,V5 = V22,V9 = V21]). eq(if(V, V5, V9, Out),0,[half(V24, Ret02),lastbit(V24, Ret101),conviter(Ret02, 1 + Ret101 + V23, Ret4)],[Out = Ret4,V23 >= 0,V = 1,V24 >= 0,V5 = V24,V9 = V23]). eq(half(V, Out),0,[],[Out = 0,V25 >= 0,V = V25]). eq(lastbit(V, Out),0,[],[Out = 0,V26 >= 0,V = V26]). eq(zero(V, Out),0,[],[Out = 0,V27 >= 0,V = V27]). eq(conv(V, Out),0,[],[Out = 0,V28 >= 0,V = V28]). eq(conviter(V, V5, Out),0,[],[Out = 0,V29 >= 0,V30 >= 0,V = V29,V5 = V30]). eq(if(V, V5, V9, Out),0,[],[Out = 0,V31 >= 0,V9 = V33,V32 >= 0,V = V31,V5 = V32,V33 >= 0]). eq(fun(V, Out),0,[],[Out = 0,V34 >= 0,V = V34]). eq(fun1(V, Out),0,[],[Out = 0,V35 >= 0,V = V35]). eq(fun2(V, Out),0,[],[Out = 0,V36 >= 0,V = V36]). eq(fun5(V, V5, V9, Out),0,[],[Out = 0,V37 >= 0,V9 = V38,V39 >= 0,V = V37,V5 = V39,V38 >= 0]). input_output_vars(fun(V,Out),[V],[Out]). input_output_vars(fun1(V,Out),[V],[Out]). input_output_vars(fun2(V,Out),[V],[Out]). input_output_vars(fun3(V,Out),[V],[Out]). input_output_vars(fun4(V,V5,Out),[V,V5],[Out]). input_output_vars(fun5(V,V5,V9,Out),[V,V5,V9],[Out]). input_output_vars(half(V,Out),[V],[Out]). input_output_vars(lastbit(V,Out),[V],[Out]). input_output_vars(zero(V,Out),[V],[Out]). input_output_vars(conv(V,Out),[V],[Out]). input_output_vars(conviter(V,V5,Out),[V,V5],[Out]). input_output_vars(if(V,V5,V9,Out),[V,V5,V9],[Out]). CoFloCo proof output: Preprocessing Cost Relations ===================================== #### Computed strongly connected components 0. recursive : [half/2] 1. recursive : [lastbit/2] 2. non_recursive : [zero/2] 3. recursive : [conviter/3,if/4] 4. non_recursive : [conv/2] 5. recursive : [fun/2] 6. recursive : [fun1/2] 7. non_recursive : [fun2/2] 8. recursive [non_tail] : [fun4/3,fun5/4] 9. non_recursive : [fun3/2] 10. non_recursive : [start/3] #### Obtained direct recursion through partial evaluation 0. SCC is partially evaluated into half/2 1. SCC is partially evaluated into lastbit/2 2. SCC is partially evaluated into zero/2 3. SCC is partially evaluated into conviter/3 4. SCC is partially evaluated into conv/2 5. SCC is partially evaluated into fun/2 6. SCC is partially evaluated into fun1/2 7. SCC is partially evaluated into fun2/2 8. SCC is partially evaluated into fun4/3 9. SCC is completely evaluated into other SCCs 10. SCC is partially evaluated into start/3 Control-Flow Refinement of Cost Relations ===================================== ### Specialization of cost equations half/2 * CE 16 is refined into CE [46] * CE 17 is refined into CE [47] * CE 18 is refined into CE [48] ### Cost equations --> "Loop" of half/2 * CEs [48] --> Loop 26 * CEs [46,47] --> Loop 27 ### Ranking functions of CR half(V,Out) * RF of phase [26]: [V-1] #### Partial ranking functions of CR half(V,Out) * Partial RF of phase [26]: - RF of loop [26:1]: V-1 ### Specialization of cost equations lastbit/2 * CE 19 is refined into CE [49] * CE 20 is refined into CE [50] * CE 21 is refined into CE [51] ### Cost equations --> "Loop" of lastbit/2 * CEs [51] --> Loop 28 * CEs [49] --> Loop 29 * CEs [50] --> Loop 30 ### Ranking functions of CR lastbit(V,Out) * RF of phase [28]: [V-1] #### Partial ranking functions of CR lastbit(V,Out) * Partial RF of phase [28]: - RF of loop [28:1]: V-1 ### Specialization of cost equations zero/2 * CE 42 is refined into CE [52] * CE 43 is refined into CE [53] * CE 41 is refined into CE [54] ### Cost equations --> "Loop" of zero/2 * CEs [52] --> Loop 31 * CEs [53] --> Loop 32 * CEs [54] --> Loop 33 ### Ranking functions of CR zero(V,Out) #### Partial ranking functions of CR zero(V,Out) ### Specialization of cost equations conviter/3 * CE 36 is refined into CE [55] * CE 34 is refined into CE [56,57,58] * CE 37 is refined into CE [59] * CE 35 is refined into CE [60,61,62,63,64] ### Cost equations --> "Loop" of conviter/3 * CEs [63] --> Loop 34 * CEs [64] --> Loop 35 * CEs [61] --> Loop 36 * CEs [62] --> Loop 37 * CEs [60] --> Loop 38 * CEs [55] --> Loop 39 * CEs [56,57,58,59] --> Loop 40 ### Ranking functions of CR conviter(V,V5,Out) * RF of phase [34,35]: [V-1,2*V+V5-3] #### Partial ranking functions of CR conviter(V,V5,Out) * Partial RF of phase [34,35]: - RF of loop [34:1]: V-1 - RF of loop [35:1]: V-2 2/3*V-5/3 ### Specialization of cost equations conv/2 * CE 44 is refined into CE [65,66,67,68,69,70] * CE 45 is refined into CE [71] ### Cost equations --> "Loop" of conv/2 * CEs [70] --> Loop 41 * CEs [69] --> Loop 42 * CEs [68] --> Loop 43 * CEs [66,71] --> Loop 44 * CEs [67] --> Loop 45 * CEs [65] --> Loop 46 ### Ranking functions of CR conv(V,Out) #### Partial ranking functions of CR conv(V,Out) ### Specialization of cost equations fun/2 * CE 31 is refined into CE [72] * CE 30 is refined into CE [73] * CE 33 is refined into CE [74] * CE 32 is refined into CE [75] ### Cost equations --> "Loop" of fun/2 * CEs [75] --> Loop 47 * CEs [72] --> Loop 48 * CEs [73,74] --> Loop 49 ### Ranking functions of CR fun(V,Out) * RF of phase [47]: [V-1] #### Partial ranking functions of CR fun(V,Out) * Partial RF of phase [47]: - RF of loop [47:1]: V-1 ### Specialization of cost equations fun1/2 * CE 27 is refined into CE [76] * CE 26 is refined into CE [77] * CE 29 is refined into CE [78] * CE 28 is refined into CE [79] ### Cost equations --> "Loop" of fun1/2 * CEs [79] --> Loop 50 * CEs [76] --> Loop 51 * CEs [77,78] --> Loop 52 ### Ranking functions of CR fun1(V,Out) * RF of phase [50]: [V-1] #### Partial ranking functions of CR fun1(V,Out) * Partial RF of phase [50]: - RF of loop [50:1]: V-1 ### Specialization of cost equations fun2/2 * CE 39 is refined into CE [80] * CE 40 is refined into CE [81] * CE 38 is refined into CE [82] ### Cost equations --> "Loop" of fun2/2 * CEs [80] --> Loop 53 * CEs [81] --> Loop 54 * CEs [82] --> Loop 55 ### Ranking functions of CR fun2(V,Out) #### Partial ranking functions of CR fun2(V,Out) ### Specialization of cost equations fun4/3 * CE 22 is refined into CE [83,84,85,86,87,88,89] * CE 25 is refined into CE [90,91] * CE 23 is refined into CE [92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121] * CE 24 is refined into CE [122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151] ### Cost equations --> "Loop" of fun4/3 * CEs [115,145] --> Loop 56 * CEs [114,144] --> Loop 57 * CEs [112,142] --> Loop 58 * CEs [113,143] --> Loop 59 * CEs [111,141] --> Loop 60 * CEs [110,140] --> Loop 61 * CEs [121,151] --> Loop 62 * CEs [120,150] --> Loop 63 * CEs [118,148] --> Loop 64 * CEs [119,149] --> Loop 65 * CEs [117,147] --> Loop 66 * CEs [116,146] --> Loop 67 * CEs [103,133] --> Loop 68 * CEs [102,132] --> Loop 69 * CEs [100,130] --> Loop 70 * CEs [101,131] --> Loop 71 * CEs [99,129] --> Loop 72 * CEs [98,128] --> Loop 73 * CEs [109,139] --> Loop 74 * CEs [108,138] --> Loop 75 * CEs [106,136] --> Loop 76 * CEs [107,137] --> Loop 77 * CEs [105,135] --> Loop 78 * CEs [104,134] --> Loop 79 * CEs [97,127] --> Loop 80 * CEs [96,126] --> Loop 81 * CEs [93,123] --> Loop 82 * CEs [95,125] --> Loop 83 * CEs [92,122] --> Loop 84 * CEs [94,124] --> Loop 85 * CEs [87,89] --> Loop 86 * CEs [83,85,90] --> Loop 87 * CEs [84,86,88,91] --> Loop 88 ### Ranking functions of CR fun4(V,V5,Out) * RF of phase [56,57,58,59,60,61,62,63,64,65,66,67]: [V-1,2*V+V5-3] #### Partial ranking functions of CR fun4(V,V5,Out) * Partial RF of phase [56,57,58,59,60,61,62,63,64,65,66,67]: - RF of loop [56:1,57:1,60:1,61:1]: V-1 - RF of loop [58:1,59:1,62:1,63:1,64:1,65:1,66:1,67:1]: V-2 2/3*V-5/3 ### Specialization of cost equations start/3 * CE 4 is refined into CE [152] * CE 1 is refined into CE [153] * CE 2 is refined into CE [154,155,156,157,158,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,237,238,239,240,241,242,243,244,245,246,247,248,249] * CE 3 is refined into CE [250,251,252,253,254,255,256,257,258,259,260,261,262,263,264,265,266,267,268,269,270,271,272,273,274,275,276,277,278,279,280,281,282,283,284,285,286,287,288,289,290,291,292,293,294,295,296,297,298,299,300,301,302,303,304,305,306,307,308,309,310,311,312,313,314,315,316,317,318,319,320,321,322,323,324,325,326,327,328,329,330,331,332,333,334,335,336,337,338,339,340,341,342,343,344,345] * CE 5 is refined into CE [346,347,348,349,350,351,352,353,354,355,356,357,358,359,360,361] * CE 6 is refined into CE [362,363,364,365] * CE 7 is refined into CE [366,367,368,369] * CE 8 is refined into CE [370,371,372] * CE 9 is refined into CE [373,374,375,376,377,378,379,380,381,382,383,384,385,386] * CE 10 is refined into CE [387,388,389,390,391,392,393,394,395,396,397,398,399,400] * CE 11 is refined into CE [401,402] * CE 12 is refined into CE [403,404,405] * CE 13 is refined into CE [406,407,408] * CE 14 is refined into CE [409,410,411,412,413,414] * CE 15 is refined into CE [415,416,417,418,419,420] ### Cost equations --> "Loop" of start/3 * CEs [152] --> Loop 89 * CEs [154,155,156,157,158,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,237,238,239,240,241,242,243,244,245,246,247,248,249,250,251,252,253,254,255,256,257,258,259,260,261,262,263,264,265,266,267,268,269,270,271,272,273,274,275,276,277,278,279,280,281,282,283,284,285,286,287,288,289,290,291,292,293,294,295,296,297,298,299,300,301,302,303,304,305,306,307,308,309,310,311,312,313,314,315,316,317,318,319,320,321,322,323,324,325,326,327,328,329,330,331,332,333,334,335,336,337,338,339,340,341,342,343,344,345,346,347,348,349,350,351,352,353,354,355,356,357,358,359,360,361,362,366,378,392,403,410,417] --> Loop 90 * CEs [153,363,364,365,367,368,369,370,371,372,373,374,375,376,377,379,380,381,382,383,384,385,386,387,388,389,390,391,393,394,395,396,397,398,399,400,401,402,404,405,406,407,408,409,411,412,413,414,415,416,418,419,420] --> Loop 91 ### Ranking functions of CR start(V,V5,V9) #### Partial ranking functions of CR start(V,V5,V9) Computing Bounds ===================================== #### Cost of chains of half(V,Out): * Chain [[26],27]: 0 with precondition: [Out>=1,V>=2*Out] * Chain [27]: 0 with precondition: [Out=0,V>=0] #### Cost of chains of lastbit(V,Out): * Chain [[28],30]: 0 with precondition: [Out=1,V>=3] * Chain [[28],29]: 0 with precondition: [Out=0,V>=2] * Chain [30]: 0 with precondition: [V=1,Out=1] * Chain [29]: 0 with precondition: [Out=0,V>=0] #### Cost of chains of zero(V,Out): * Chain [33]: 0 with precondition: [V=0,Out=2] * Chain [32]: 0 with precondition: [Out=0,V>=0] * Chain [31]: 0 with precondition: [Out=1,V>=1] #### Cost of chains of conviter(V,V5,Out): * Chain [[34,35],40]: 0 with precondition: [Out=0,V>=2,V5>=0] * Chain [[34,35],38,40]: 0 with precondition: [Out=0,V>=2,V5>=0] * Chain [[34,35],38,39]: 0 with precondition: [V5>=0,Out>=V5+3,V+2*V5+6>=2*Out,V+V5+1>=Out] * Chain [[34,35],37,40]: 0 with precondition: [Out=0,V>=6,V5>=0] * Chain [[34,35],37,39]: 0 with precondition: [V>=6,V5>=0,Out>=V5+3,V+3*V5+6>=3*Out] * Chain [[34,35],36,40]: 0 with precondition: [Out=0,V>=2,V5>=0] * Chain [[34,35],36,39]: 0 with precondition: [V5>=0,Out>=V5+2,V+2*V5+4>=2*Out,V+V5>=Out] * Chain [40]: 0 with precondition: [Out=0,V>=0,V5>=0] * Chain [39]: 0 with precondition: [V=0,V5=Out,V5>=0] * Chain [38,40]: 0 with precondition: [V=1,Out=0,V5>=0] * Chain [38,39]: 0 with precondition: [V=1,Out=V5+2,Out>=2] * Chain [37,40]: 0 with precondition: [Out=0,V>=3,V5>=0] * Chain [37,39]: 0 with precondition: [Out=V5+2,V>=3,Out>=2] * Chain [36,40]: 0 with precondition: [Out=0,V>=1,V5>=0] * Chain [36,39]: 0 with precondition: [Out=V5+1,V>=1,Out>=1] #### Cost of chains of conv(V,Out): * Chain [46]: 0 with precondition: [V=0,Out=1] * Chain [45]: 0 with precondition: [V=1,Out=3] * Chain [44]: 0 with precondition: [Out=0,V>=0] * Chain [43]: 0 with precondition: [Out=2,V>=1] * Chain [42]: 0 with precondition: [Out>=3,V+6>=2*Out,V+1>=Out] * Chain [41]: 0 with precondition: [Out>=4,V+8>=2*Out,V+2>=Out] #### Cost of chains of fun(V,Out): * Chain [[47],49]: 1*it(47)+1 Such that:it(47) =< 2*Out with precondition: [Out>=1,V>=2*Out] * Chain [[47],48]: 1*it(47)+1 Such that:it(47) =< 2*Out with precondition: [V+1=2*Out,V>=3] * Chain [49]: 1 with precondition: [Out=0,V>=0] * Chain [48]: 1 with precondition: [V=1,Out=1] #### Cost of chains of fun1(V,Out): * Chain [[50],52]: 1*it(50)+1 Such that:it(50) =< 2*Out with precondition: [Out>=1,V>=2*Out] * Chain [[50],51]: 1*it(50)+1 Such that:it(50) =< 2*Out with precondition: [V+1=2*Out,V>=3] * Chain [52]: 1 with precondition: [Out=0,V>=0] * Chain [51]: 1 with precondition: [V=1,Out=1] #### Cost of chains of fun2(V,Out): * Chain [55]: 1 with precondition: [V=0,Out=1] * Chain [54]: 0 with precondition: [Out=0,V>=0] * Chain [53]: 1 with precondition: [Out=2,V>=1] #### Cost of chains of fun4(V,V5,Out): * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],88]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+2 Such that:aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(26) =< V aux(27) =< 2*V aux(28) =< 3*V aux(29) =< 2/3*V aux(30) =< 8/3*V it(56) =< aux(26) it(57) =< aux(26) it(58) =< aux(26) it(59) =< aux(26) it(60) =< aux(26) it(62) =< aux(26) it(63) =< aux(26) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(27) it(57) =< aux(27) it(58) =< aux(27) it(59) =< aux(27) it(60) =< aux(27) it(62) =< aux(27) it(63) =< aux(27) s(34) =< aux(27) s(42) =< aux(27) it(60) =< aux(28) it(62) =< aux(28) it(63) =< aux(28) it(58) =< aux(29) it(59) =< aux(29) it(62) =< aux(29) it(63) =< aux(29) it(59) =< aux(30) it(60) =< aux(30) it(62) =< aux(30) it(63) =< aux(30) s(39) =< aux(28) s(37) =< aux(30) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=2,V5>=0,Out>=3,13*V>=4*Out+2] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],86]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+2 Such that:aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(31) =< V aux(32) =< 2*V aux(33) =< 3*V aux(34) =< 2/3*V aux(35) =< 8/3*V it(56) =< aux(31) it(57) =< aux(31) it(58) =< aux(31) it(59) =< aux(31) it(60) =< aux(31) it(62) =< aux(31) it(63) =< aux(31) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(32) it(57) =< aux(32) it(58) =< aux(32) it(59) =< aux(32) it(60) =< aux(32) it(62) =< aux(32) it(63) =< aux(32) s(34) =< aux(32) s(42) =< aux(32) it(60) =< aux(33) it(62) =< aux(33) it(63) =< aux(33) it(58) =< aux(34) it(59) =< aux(34) it(62) =< aux(34) it(63) =< aux(34) it(59) =< aux(35) it(60) =< aux(35) it(62) =< aux(35) it(63) =< aux(35) s(39) =< aux(33) s(37) =< aux(35) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=2,V5>=0,Out>=5,13*V+6>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],85,88]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+5 Such that:aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(36) =< V aux(37) =< 2*V aux(38) =< 3*V aux(39) =< 2/3*V aux(40) =< 8/3*V it(56) =< aux(36) it(57) =< aux(36) it(58) =< aux(36) it(59) =< aux(36) it(60) =< aux(36) it(62) =< aux(36) it(63) =< aux(36) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(37) it(57) =< aux(37) it(58) =< aux(37) it(59) =< aux(37) it(60) =< aux(37) it(62) =< aux(37) it(63) =< aux(37) s(34) =< aux(37) s(42) =< aux(37) it(60) =< aux(38) it(62) =< aux(38) it(63) =< aux(38) it(58) =< aux(39) it(59) =< aux(39) it(62) =< aux(39) it(63) =< aux(39) it(59) =< aux(40) it(60) =< aux(40) it(62) =< aux(40) it(63) =< aux(40) s(39) =< aux(38) s(37) =< aux(40) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=2,V5>=0,Out>=5,13*V+6>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],85,87]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+6 Such that:aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(41) =< V aux(42) =< 2*V aux(43) =< 3*V aux(44) =< 2/3*V aux(45) =< 8/3*V it(56) =< aux(41) it(57) =< aux(41) it(58) =< aux(41) it(59) =< aux(41) it(60) =< aux(41) it(62) =< aux(41) it(63) =< aux(41) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(42) it(57) =< aux(42) it(58) =< aux(42) it(59) =< aux(42) it(60) =< aux(42) it(62) =< aux(42) it(63) =< aux(42) s(34) =< aux(42) s(42) =< aux(42) it(60) =< aux(43) it(62) =< aux(43) it(63) =< aux(43) it(58) =< aux(44) it(59) =< aux(44) it(62) =< aux(44) it(63) =< aux(44) it(59) =< aux(45) it(60) =< aux(45) it(62) =< aux(45) it(63) =< aux(45) s(39) =< aux(43) s(37) =< aux(45) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=2,V5>=0,Out>=6,13*V+10>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],84,88]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+5 Such that:aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(46) =< V aux(47) =< 2*V aux(48) =< 3*V aux(49) =< 2/3*V aux(50) =< 8/3*V it(56) =< aux(46) it(57) =< aux(46) it(58) =< aux(46) it(59) =< aux(46) it(60) =< aux(46) it(62) =< aux(46) it(63) =< aux(46) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(47) it(57) =< aux(47) it(58) =< aux(47) it(59) =< aux(47) it(60) =< aux(47) it(62) =< aux(47) it(63) =< aux(47) s(34) =< aux(47) s(42) =< aux(47) it(60) =< aux(48) it(62) =< aux(48) it(63) =< aux(48) it(58) =< aux(49) it(59) =< aux(49) it(62) =< aux(49) it(63) =< aux(49) it(59) =< aux(50) it(60) =< aux(50) it(62) =< aux(50) it(63) =< aux(50) s(39) =< aux(48) s(37) =< aux(50) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=2,V5>=0,Out>=6,13*V+10>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],84,87]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+6 Such that:aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(51) =< V aux(52) =< 2*V aux(53) =< 3*V aux(54) =< 2/3*V aux(55) =< 8/3*V it(56) =< aux(51) it(57) =< aux(51) it(58) =< aux(51) it(59) =< aux(51) it(60) =< aux(51) it(62) =< aux(51) it(63) =< aux(51) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(52) it(57) =< aux(52) it(58) =< aux(52) it(59) =< aux(52) it(60) =< aux(52) it(62) =< aux(52) it(63) =< aux(52) s(34) =< aux(52) s(42) =< aux(52) it(60) =< aux(53) it(62) =< aux(53) it(63) =< aux(53) it(58) =< aux(54) it(59) =< aux(54) it(62) =< aux(54) it(63) =< aux(54) it(59) =< aux(55) it(60) =< aux(55) it(62) =< aux(55) it(63) =< aux(55) s(39) =< aux(53) s(37) =< aux(55) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=2,V5>=0,Out>=7,13*V+14>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],83,88]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+6 Such that:aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(56) =< V aux(57) =< 2*V aux(58) =< 3*V aux(59) =< 2/3*V aux(60) =< 8/3*V it(56) =< aux(56) it(57) =< aux(56) it(58) =< aux(56) it(59) =< aux(56) it(60) =< aux(56) it(62) =< aux(56) it(63) =< aux(56) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(57) it(57) =< aux(57) it(58) =< aux(57) it(59) =< aux(57) it(60) =< aux(57) it(62) =< aux(57) it(63) =< aux(57) s(34) =< aux(57) s(42) =< aux(57) it(60) =< aux(58) it(62) =< aux(58) it(63) =< aux(58) it(58) =< aux(59) it(59) =< aux(59) it(62) =< aux(59) it(63) =< aux(59) it(59) =< aux(60) it(60) =< aux(60) it(62) =< aux(60) it(63) =< aux(60) s(39) =< aux(58) s(37) =< aux(60) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=2,V5>=0,Out>=7,13*V+14>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],83,87]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+7 Such that:aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(61) =< V aux(62) =< 2*V aux(63) =< 3*V aux(64) =< 2/3*V aux(65) =< 8/3*V it(56) =< aux(61) it(57) =< aux(61) it(58) =< aux(61) it(59) =< aux(61) it(60) =< aux(61) it(62) =< aux(61) it(63) =< aux(61) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(62) it(57) =< aux(62) it(58) =< aux(62) it(59) =< aux(62) it(60) =< aux(62) it(62) =< aux(62) it(63) =< aux(62) s(34) =< aux(62) s(42) =< aux(62) it(60) =< aux(63) it(62) =< aux(63) it(63) =< aux(63) it(58) =< aux(64) it(59) =< aux(64) it(62) =< aux(64) it(63) =< aux(64) it(59) =< aux(65) it(60) =< aux(65) it(62) =< aux(65) it(63) =< aux(65) s(39) =< aux(63) s(37) =< aux(65) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=2,V5>=0,Out>=8,13*V+18>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],82,88]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+6 Such that:aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(66) =< V aux(67) =< 2*V aux(68) =< 3*V aux(69) =< 2/3*V aux(70) =< 8/3*V it(56) =< aux(66) it(57) =< aux(66) it(58) =< aux(66) it(59) =< aux(66) it(60) =< aux(66) it(62) =< aux(66) it(63) =< aux(66) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(67) it(57) =< aux(67) it(58) =< aux(67) it(59) =< aux(67) it(60) =< aux(67) it(62) =< aux(67) it(63) =< aux(67) s(34) =< aux(67) s(42) =< aux(67) it(60) =< aux(68) it(62) =< aux(68) it(63) =< aux(68) it(58) =< aux(69) it(59) =< aux(69) it(62) =< aux(69) it(63) =< aux(69) it(59) =< aux(70) it(60) =< aux(70) it(62) =< aux(70) it(63) =< aux(70) s(39) =< aux(68) s(37) =< aux(70) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=2,V5>=0,Out>=8,13*V+18>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],82,87]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+7 Such that:aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(71) =< V aux(72) =< 2*V aux(73) =< 3*V aux(74) =< 2/3*V aux(75) =< 8/3*V it(56) =< aux(71) it(57) =< aux(71) it(58) =< aux(71) it(59) =< aux(71) it(60) =< aux(71) it(62) =< aux(71) it(63) =< aux(71) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(72) it(57) =< aux(72) it(58) =< aux(72) it(59) =< aux(72) it(60) =< aux(72) it(62) =< aux(72) it(63) =< aux(72) s(34) =< aux(72) s(42) =< aux(72) it(60) =< aux(73) it(62) =< aux(73) it(63) =< aux(73) it(58) =< aux(74) it(59) =< aux(74) it(62) =< aux(74) it(63) =< aux(74) it(59) =< aux(75) it(60) =< aux(75) it(62) =< aux(75) it(63) =< aux(75) s(39) =< aux(73) s(37) =< aux(75) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=2,V5>=0,Out>=9,13*V+22>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],81,88]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+5 Such that:aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(76) =< V aux(77) =< 2*V aux(78) =< 3*V aux(79) =< 2/3*V aux(80) =< 8/3*V it(56) =< aux(76) it(57) =< aux(76) it(58) =< aux(76) it(59) =< aux(76) it(60) =< aux(76) it(62) =< aux(76) it(63) =< aux(76) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(77) it(57) =< aux(77) it(58) =< aux(77) it(59) =< aux(77) it(60) =< aux(77) it(62) =< aux(77) it(63) =< aux(77) s(34) =< aux(77) s(42) =< aux(77) it(60) =< aux(78) it(62) =< aux(78) it(63) =< aux(78) it(58) =< aux(79) it(59) =< aux(79) it(62) =< aux(79) it(63) =< aux(79) it(59) =< aux(80) it(60) =< aux(80) it(62) =< aux(80) it(63) =< aux(80) s(39) =< aux(78) s(37) =< aux(80) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=2,V5>=0,Out>=6,13*V+10>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],81,87]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+6 Such that:aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(81) =< V aux(82) =< 2*V aux(83) =< 3*V aux(84) =< 2/3*V aux(85) =< 8/3*V it(56) =< aux(81) it(57) =< aux(81) it(58) =< aux(81) it(59) =< aux(81) it(60) =< aux(81) it(62) =< aux(81) it(63) =< aux(81) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(82) it(57) =< aux(82) it(58) =< aux(82) it(59) =< aux(82) it(60) =< aux(82) it(62) =< aux(82) it(63) =< aux(82) s(34) =< aux(82) s(42) =< aux(82) it(60) =< aux(83) it(62) =< aux(83) it(63) =< aux(83) it(58) =< aux(84) it(59) =< aux(84) it(62) =< aux(84) it(63) =< aux(84) it(59) =< aux(85) it(60) =< aux(85) it(62) =< aux(85) it(63) =< aux(85) s(39) =< aux(83) s(37) =< aux(85) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=2,V5>=0,Out>=7,13*V+14>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],80,88]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+6 Such that:aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(86) =< V aux(87) =< 2*V aux(88) =< 3*V aux(89) =< 2/3*V aux(90) =< 8/3*V it(56) =< aux(86) it(57) =< aux(86) it(58) =< aux(86) it(59) =< aux(86) it(60) =< aux(86) it(62) =< aux(86) it(63) =< aux(86) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(87) it(57) =< aux(87) it(58) =< aux(87) it(59) =< aux(87) it(60) =< aux(87) it(62) =< aux(87) it(63) =< aux(87) s(34) =< aux(87) s(42) =< aux(87) it(60) =< aux(88) it(62) =< aux(88) it(63) =< aux(88) it(58) =< aux(89) it(59) =< aux(89) it(62) =< aux(89) it(63) =< aux(89) it(59) =< aux(90) it(60) =< aux(90) it(62) =< aux(90) it(63) =< aux(90) s(39) =< aux(88) s(37) =< aux(90) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=2,V5>=0,Out>=8,13*V+18>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],80,87]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+7 Such that:aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(91) =< V aux(92) =< 2*V aux(93) =< 3*V aux(94) =< 2/3*V aux(95) =< 8/3*V it(56) =< aux(91) it(57) =< aux(91) it(58) =< aux(91) it(59) =< aux(91) it(60) =< aux(91) it(62) =< aux(91) it(63) =< aux(91) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(92) it(57) =< aux(92) it(58) =< aux(92) it(59) =< aux(92) it(60) =< aux(92) it(62) =< aux(92) it(63) =< aux(92) s(34) =< aux(92) s(42) =< aux(92) it(60) =< aux(93) it(62) =< aux(93) it(63) =< aux(93) it(58) =< aux(94) it(59) =< aux(94) it(62) =< aux(94) it(63) =< aux(94) it(59) =< aux(95) it(60) =< aux(95) it(62) =< aux(95) it(63) =< aux(95) s(39) =< aux(93) s(37) =< aux(95) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=2,V5>=0,Out>=9,13*V+22>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],79,88]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+5 Such that:aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(96) =< V aux(97) =< 2*V aux(98) =< 3*V aux(99) =< 2/3*V aux(100) =< 8/3*V it(56) =< aux(96) it(57) =< aux(96) it(58) =< aux(96) it(59) =< aux(96) it(60) =< aux(96) it(62) =< aux(96) it(63) =< aux(96) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(97) it(57) =< aux(97) it(58) =< aux(97) it(59) =< aux(97) it(60) =< aux(97) it(62) =< aux(97) it(63) =< aux(97) s(34) =< aux(97) s(42) =< aux(97) it(60) =< aux(98) it(62) =< aux(98) it(63) =< aux(98) it(58) =< aux(99) it(59) =< aux(99) it(62) =< aux(99) it(63) =< aux(99) it(59) =< aux(100) it(60) =< aux(100) it(62) =< aux(100) it(63) =< aux(100) s(39) =< aux(98) s(37) =< aux(100) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=6,V5>=0,Out>=5,7*V>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],79,87]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+6 Such that:aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(101) =< V aux(102) =< 2*V aux(103) =< 3*V aux(104) =< 2/3*V aux(105) =< 8/3*V it(56) =< aux(101) it(57) =< aux(101) it(58) =< aux(101) it(59) =< aux(101) it(60) =< aux(101) it(62) =< aux(101) it(63) =< aux(101) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(102) it(57) =< aux(102) it(58) =< aux(102) it(59) =< aux(102) it(60) =< aux(102) it(62) =< aux(102) it(63) =< aux(102) s(34) =< aux(102) s(42) =< aux(102) it(60) =< aux(103) it(62) =< aux(103) it(63) =< aux(103) it(58) =< aux(104) it(59) =< aux(104) it(62) =< aux(104) it(63) =< aux(104) it(59) =< aux(105) it(60) =< aux(105) it(62) =< aux(105) it(63) =< aux(105) s(39) =< aux(103) s(37) =< aux(105) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=6,V5>=0,Out>=6,7*V+4>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],78,88]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+6 Such that:aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(106) =< V aux(107) =< 2*V aux(108) =< 3*V aux(109) =< 2/3*V aux(110) =< 8/3*V it(56) =< aux(106) it(57) =< aux(106) it(58) =< aux(106) it(59) =< aux(106) it(60) =< aux(106) it(62) =< aux(106) it(63) =< aux(106) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(107) it(57) =< aux(107) it(58) =< aux(107) it(59) =< aux(107) it(60) =< aux(107) it(62) =< aux(107) it(63) =< aux(107) s(34) =< aux(107) s(42) =< aux(107) it(60) =< aux(108) it(62) =< aux(108) it(63) =< aux(108) it(58) =< aux(109) it(59) =< aux(109) it(62) =< aux(109) it(63) =< aux(109) it(59) =< aux(110) it(60) =< aux(110) it(62) =< aux(110) it(63) =< aux(110) s(39) =< aux(108) s(37) =< aux(110) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=6,V5>=0,Out>=7,7*V+8>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],78,87]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+7 Such that:aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(111) =< V aux(112) =< 2*V aux(113) =< 3*V aux(114) =< 2/3*V aux(115) =< 8/3*V it(56) =< aux(111) it(57) =< aux(111) it(58) =< aux(111) it(59) =< aux(111) it(60) =< aux(111) it(62) =< aux(111) it(63) =< aux(111) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(112) it(57) =< aux(112) it(58) =< aux(112) it(59) =< aux(112) it(60) =< aux(112) it(62) =< aux(112) it(63) =< aux(112) s(34) =< aux(112) s(42) =< aux(112) it(60) =< aux(113) it(62) =< aux(113) it(63) =< aux(113) it(58) =< aux(114) it(59) =< aux(114) it(62) =< aux(114) it(63) =< aux(114) it(59) =< aux(115) it(60) =< aux(115) it(62) =< aux(115) it(63) =< aux(115) s(39) =< aux(113) s(37) =< aux(115) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=6,V5>=0,Out>=8,7*V+12>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],77,88]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+2*s(49)+6 Such that:aux(13) =< V aux(14) =< V+11 aux(18) =< 2*V+21 aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(20) =< 3*V aux(21) =< 3*V+33 aux(25) =< 8*V+88 aux(22) =< 2/3*V aux(24) =< 8/3*V aux(117) =< 2*V+22 s(49) =< aux(117) it(56) =< aux(13) it(57) =< aux(13) it(58) =< aux(13) it(59) =< aux(13) it(60) =< aux(13) it(62) =< aux(13) it(63) =< aux(13) it(56) =< aux(14) it(57) =< aux(14) it(58) =< aux(14) it(59) =< aux(14) it(60) =< aux(14) it(62) =< aux(14) it(63) =< aux(14) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(18) it(57) =< aux(18) it(58) =< aux(18) it(59) =< aux(18) it(60) =< aux(18) it(62) =< aux(18) it(63) =< aux(18) it(57) =< aux(117) it(58) =< aux(117) it(59) =< aux(117) it(60) =< aux(117) it(62) =< aux(117) it(63) =< aux(117) s(34) =< aux(117) s(42) =< aux(117) it(60) =< aux(20) it(62) =< aux(20) it(63) =< aux(20) s(40) =< aux(20) it(60) =< aux(21) it(62) =< aux(21) it(63) =< aux(21) s(40) =< aux(21) it(58) =< aux(22) it(59) =< aux(22) it(62) =< aux(22) it(63) =< aux(22) it(59) =< aux(24) it(60) =< aux(24) it(62) =< aux(24) it(63) =< aux(24) s(38) =< aux(24) it(59) =< aux(25) it(60) =< aux(25) it(62) =< aux(25) it(63) =< aux(25) s(38) =< aux(25) s(39) =< s(40) s(37) =< s(38) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=6,V5>=0,Out>=9,7*V+16>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],77,87]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+2*s(49)+7 Such that:aux(13) =< V aux(14) =< V+13 aux(18) =< 2*V+25 aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(20) =< 3*V aux(21) =< 3*V+39 aux(25) =< 8*V+104 aux(22) =< 2/3*V aux(24) =< 8/3*V aux(118) =< 2*V+26 s(49) =< aux(118) it(56) =< aux(13) it(57) =< aux(13) it(58) =< aux(13) it(59) =< aux(13) it(60) =< aux(13) it(62) =< aux(13) it(63) =< aux(13) it(56) =< aux(14) it(57) =< aux(14) it(58) =< aux(14) it(59) =< aux(14) it(60) =< aux(14) it(62) =< aux(14) it(63) =< aux(14) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(18) it(57) =< aux(18) it(58) =< aux(18) it(59) =< aux(18) it(60) =< aux(18) it(62) =< aux(18) it(63) =< aux(18) it(57) =< aux(118) it(58) =< aux(118) it(59) =< aux(118) it(60) =< aux(118) it(62) =< aux(118) it(63) =< aux(118) s(34) =< aux(118) s(42) =< aux(118) it(60) =< aux(20) it(62) =< aux(20) it(63) =< aux(20) s(40) =< aux(20) it(60) =< aux(21) it(62) =< aux(21) it(63) =< aux(21) s(40) =< aux(21) it(58) =< aux(22) it(59) =< aux(22) it(62) =< aux(22) it(63) =< aux(22) it(59) =< aux(24) it(60) =< aux(24) it(62) =< aux(24) it(63) =< aux(24) s(38) =< aux(24) it(59) =< aux(25) it(60) =< aux(25) it(62) =< aux(25) it(63) =< aux(25) s(38) =< aux(25) s(39) =< s(40) s(37) =< s(38) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=6,V5>=0,Out>=10,7*V+20>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],76,88]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+2*s(51)+5 Such that:aux(13) =< V aux(14) =< V+7 aux(18) =< 2*V+13 aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(20) =< 3*V aux(21) =< 3*V+21 aux(25) =< 8*V+56 aux(22) =< 2/3*V aux(24) =< 8/3*V aux(120) =< 2*V+14 s(51) =< aux(120) it(56) =< aux(13) it(57) =< aux(13) it(58) =< aux(13) it(59) =< aux(13) it(60) =< aux(13) it(62) =< aux(13) it(63) =< aux(13) it(56) =< aux(14) it(57) =< aux(14) it(58) =< aux(14) it(59) =< aux(14) it(60) =< aux(14) it(62) =< aux(14) it(63) =< aux(14) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(18) it(57) =< aux(18) it(58) =< aux(18) it(59) =< aux(18) it(60) =< aux(18) it(62) =< aux(18) it(63) =< aux(18) it(57) =< aux(120) it(58) =< aux(120) it(59) =< aux(120) it(60) =< aux(120) it(62) =< aux(120) it(63) =< aux(120) s(34) =< aux(120) s(42) =< aux(120) it(60) =< aux(20) it(62) =< aux(20) it(63) =< aux(20) s(40) =< aux(20) it(60) =< aux(21) it(62) =< aux(21) it(63) =< aux(21) s(40) =< aux(21) it(58) =< aux(22) it(59) =< aux(22) it(62) =< aux(22) it(63) =< aux(22) it(59) =< aux(24) it(60) =< aux(24) it(62) =< aux(24) it(63) =< aux(24) s(38) =< aux(24) it(59) =< aux(25) it(60) =< aux(25) it(62) =< aux(25) it(63) =< aux(25) s(38) =< aux(25) s(39) =< s(40) s(37) =< s(38) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=6,V5>=0,Out>=7,7*V+8>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],76,87]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+2*s(51)+6 Such that:aux(13) =< V aux(14) =< V+9 aux(18) =< 2*V+17 aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(20) =< 3*V aux(21) =< 3*V+27 aux(25) =< 8*V+72 aux(22) =< 2/3*V aux(24) =< 8/3*V aux(121) =< 2*V+18 s(51) =< aux(121) it(56) =< aux(13) it(57) =< aux(13) it(58) =< aux(13) it(59) =< aux(13) it(60) =< aux(13) it(62) =< aux(13) it(63) =< aux(13) it(56) =< aux(14) it(57) =< aux(14) it(58) =< aux(14) it(59) =< aux(14) it(60) =< aux(14) it(62) =< aux(14) it(63) =< aux(14) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(18) it(57) =< aux(18) it(58) =< aux(18) it(59) =< aux(18) it(60) =< aux(18) it(62) =< aux(18) it(63) =< aux(18) it(57) =< aux(121) it(58) =< aux(121) it(59) =< aux(121) it(60) =< aux(121) it(62) =< aux(121) it(63) =< aux(121) s(34) =< aux(121) s(42) =< aux(121) it(60) =< aux(20) it(62) =< aux(20) it(63) =< aux(20) s(40) =< aux(20) it(60) =< aux(21) it(62) =< aux(21) it(63) =< aux(21) s(40) =< aux(21) it(58) =< aux(22) it(59) =< aux(22) it(62) =< aux(22) it(63) =< aux(22) it(59) =< aux(24) it(60) =< aux(24) it(62) =< aux(24) it(63) =< aux(24) s(38) =< aux(24) it(59) =< aux(25) it(60) =< aux(25) it(62) =< aux(25) it(63) =< aux(25) s(38) =< aux(25) s(39) =< s(40) s(37) =< s(38) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=6,V5>=0,Out>=8,7*V+12>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],75,88]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+2*s(53)+5 Such that:aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(25) =< 8*V aux(22) =< 2/3*V aux(24) =< 8/3*V aux(123) =< V aux(124) =< 2*V aux(125) =< 3*V s(53) =< aux(124) it(56) =< aux(123) it(57) =< aux(123) it(58) =< aux(123) it(59) =< aux(123) it(60) =< aux(123) it(62) =< aux(123) it(63) =< aux(123) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(124) it(57) =< aux(124) it(58) =< aux(124) it(59) =< aux(124) it(60) =< aux(124) it(62) =< aux(124) it(63) =< aux(124) s(34) =< aux(124) s(42) =< aux(124) it(60) =< aux(125) it(62) =< aux(125) it(63) =< aux(125) it(58) =< aux(22) it(59) =< aux(22) it(62) =< aux(22) it(63) =< aux(22) it(59) =< aux(24) it(60) =< aux(24) it(62) =< aux(24) it(63) =< aux(24) s(38) =< aux(24) it(59) =< aux(25) it(60) =< aux(25) it(62) =< aux(25) it(63) =< aux(25) s(38) =< aux(25) s(39) =< aux(125) s(37) =< s(38) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=6,V5>=0,Out>=6,7*V+6>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],75,87]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+2*s(53)+6 Such that:aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(25) =< 8*V aux(22) =< 2/3*V aux(24) =< 8/3*V aux(126) =< V aux(127) =< 2*V aux(128) =< 3*V s(53) =< aux(127) it(56) =< aux(126) it(57) =< aux(126) it(58) =< aux(126) it(59) =< aux(126) it(60) =< aux(126) it(62) =< aux(126) it(63) =< aux(126) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(127) it(57) =< aux(127) it(58) =< aux(127) it(59) =< aux(127) it(60) =< aux(127) it(62) =< aux(127) it(63) =< aux(127) s(34) =< aux(127) s(42) =< aux(127) it(60) =< aux(128) it(62) =< aux(128) it(63) =< aux(128) it(58) =< aux(22) it(59) =< aux(22) it(62) =< aux(22) it(63) =< aux(22) it(59) =< aux(24) it(60) =< aux(24) it(62) =< aux(24) it(63) =< aux(24) s(38) =< aux(24) it(59) =< aux(25) it(60) =< aux(25) it(62) =< aux(25) it(63) =< aux(25) s(38) =< aux(25) s(39) =< aux(128) s(37) =< s(38) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=6,V5>=0,Out>=7,7*V+10>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],74,88]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+2*s(55)+6 Such that:aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(25) =< 8*V aux(22) =< 2/3*V aux(24) =< 8/3*V aux(130) =< V aux(131) =< 2*V aux(132) =< 3*V s(55) =< aux(131) it(56) =< aux(130) it(57) =< aux(130) it(58) =< aux(130) it(59) =< aux(130) it(60) =< aux(130) it(62) =< aux(130) it(63) =< aux(130) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(131) it(57) =< aux(131) it(58) =< aux(131) it(59) =< aux(131) it(60) =< aux(131) it(62) =< aux(131) it(63) =< aux(131) s(34) =< aux(131) s(42) =< aux(131) it(60) =< aux(132) it(62) =< aux(132) it(63) =< aux(132) it(58) =< aux(22) it(59) =< aux(22) it(62) =< aux(22) it(63) =< aux(22) it(59) =< aux(24) it(60) =< aux(24) it(62) =< aux(24) it(63) =< aux(24) s(38) =< aux(24) it(59) =< aux(25) it(60) =< aux(25) it(62) =< aux(25) it(63) =< aux(25) s(38) =< aux(25) s(39) =< aux(132) s(37) =< s(38) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=6,V5>=0,Out>=8,7*V+14>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],74,87]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+2*s(55)+7 Such that:aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(25) =< 8*V aux(22) =< 2/3*V aux(24) =< 8/3*V aux(133) =< V aux(134) =< 2*V aux(135) =< 3*V s(55) =< aux(134) it(56) =< aux(133) it(57) =< aux(133) it(58) =< aux(133) it(59) =< aux(133) it(60) =< aux(133) it(62) =< aux(133) it(63) =< aux(133) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(134) it(57) =< aux(134) it(58) =< aux(134) it(59) =< aux(134) it(60) =< aux(134) it(62) =< aux(134) it(63) =< aux(134) s(34) =< aux(134) s(42) =< aux(134) it(60) =< aux(135) it(62) =< aux(135) it(63) =< aux(135) it(58) =< aux(22) it(59) =< aux(22) it(62) =< aux(22) it(63) =< aux(22) it(59) =< aux(24) it(60) =< aux(24) it(62) =< aux(24) it(63) =< aux(24) s(38) =< aux(24) it(59) =< aux(25) it(60) =< aux(25) it(62) =< aux(25) it(63) =< aux(25) s(38) =< aux(25) s(39) =< aux(135) s(37) =< s(38) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=6,V5>=0,Out>=9,7*V+18>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],73,88]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+5 Such that:aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(136) =< V aux(137) =< 2*V aux(138) =< 3*V aux(139) =< 2/3*V aux(140) =< 8/3*V it(56) =< aux(136) it(57) =< aux(136) it(58) =< aux(136) it(59) =< aux(136) it(60) =< aux(136) it(62) =< aux(136) it(63) =< aux(136) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(137) it(57) =< aux(137) it(58) =< aux(137) it(59) =< aux(137) it(60) =< aux(137) it(62) =< aux(137) it(63) =< aux(137) s(34) =< aux(137) s(42) =< aux(137) it(60) =< aux(138) it(62) =< aux(138) it(63) =< aux(138) it(58) =< aux(139) it(59) =< aux(139) it(62) =< aux(139) it(63) =< aux(139) it(59) =< aux(140) it(60) =< aux(140) it(62) =< aux(140) it(63) =< aux(140) s(39) =< aux(138) s(37) =< aux(140) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=2,V5>=0,Out>=5,13*V+6>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],73,87]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+6 Such that:aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(141) =< V aux(142) =< 2*V aux(143) =< 3*V aux(144) =< 2/3*V aux(145) =< 8/3*V it(56) =< aux(141) it(57) =< aux(141) it(58) =< aux(141) it(59) =< aux(141) it(60) =< aux(141) it(62) =< aux(141) it(63) =< aux(141) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(142) it(57) =< aux(142) it(58) =< aux(142) it(59) =< aux(142) it(60) =< aux(142) it(62) =< aux(142) it(63) =< aux(142) s(34) =< aux(142) s(42) =< aux(142) it(60) =< aux(143) it(62) =< aux(143) it(63) =< aux(143) it(58) =< aux(144) it(59) =< aux(144) it(62) =< aux(144) it(63) =< aux(144) it(59) =< aux(145) it(60) =< aux(145) it(62) =< aux(145) it(63) =< aux(145) s(39) =< aux(143) s(37) =< aux(145) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=2,V5>=0,Out>=6,13*V+10>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],72,88]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+6 Such that:aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(146) =< V aux(147) =< 2*V aux(148) =< 3*V aux(149) =< 2/3*V aux(150) =< 8/3*V it(56) =< aux(146) it(57) =< aux(146) it(58) =< aux(146) it(59) =< aux(146) it(60) =< aux(146) it(62) =< aux(146) it(63) =< aux(146) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(147) it(57) =< aux(147) it(58) =< aux(147) it(59) =< aux(147) it(60) =< aux(147) it(62) =< aux(147) it(63) =< aux(147) s(34) =< aux(147) s(42) =< aux(147) it(60) =< aux(148) it(62) =< aux(148) it(63) =< aux(148) it(58) =< aux(149) it(59) =< aux(149) it(62) =< aux(149) it(63) =< aux(149) it(59) =< aux(150) it(60) =< aux(150) it(62) =< aux(150) it(63) =< aux(150) s(39) =< aux(148) s(37) =< aux(150) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=2,V5>=0,Out>=7,13*V+14>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],72,87]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+7 Such that:aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(151) =< V aux(152) =< 2*V aux(153) =< 3*V aux(154) =< 2/3*V aux(155) =< 8/3*V it(56) =< aux(151) it(57) =< aux(151) it(58) =< aux(151) it(59) =< aux(151) it(60) =< aux(151) it(62) =< aux(151) it(63) =< aux(151) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(152) it(57) =< aux(152) it(58) =< aux(152) it(59) =< aux(152) it(60) =< aux(152) it(62) =< aux(152) it(63) =< aux(152) s(34) =< aux(152) s(42) =< aux(152) it(60) =< aux(153) it(62) =< aux(153) it(63) =< aux(153) it(58) =< aux(154) it(59) =< aux(154) it(62) =< aux(154) it(63) =< aux(154) it(59) =< aux(155) it(60) =< aux(155) it(62) =< aux(155) it(63) =< aux(155) s(39) =< aux(153) s(37) =< aux(155) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=2,V5>=0,Out>=8,13*V+18>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],71,88]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+2*s(57)+6 Such that:aux(13) =< V aux(14) =< V+11 aux(18) =< 2*V+21 aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(20) =< 3*V aux(21) =< 3*V+33 aux(25) =< 8*V+88 aux(22) =< 2/3*V aux(24) =< 8/3*V aux(157) =< 2*V+22 s(57) =< aux(157) it(56) =< aux(13) it(57) =< aux(13) it(58) =< aux(13) it(59) =< aux(13) it(60) =< aux(13) it(62) =< aux(13) it(63) =< aux(13) it(56) =< aux(14) it(57) =< aux(14) it(58) =< aux(14) it(59) =< aux(14) it(60) =< aux(14) it(62) =< aux(14) it(63) =< aux(14) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(18) it(57) =< aux(18) it(58) =< aux(18) it(59) =< aux(18) it(60) =< aux(18) it(62) =< aux(18) it(63) =< aux(18) it(57) =< aux(157) it(58) =< aux(157) it(59) =< aux(157) it(60) =< aux(157) it(62) =< aux(157) it(63) =< aux(157) s(34) =< aux(157) s(42) =< aux(157) it(60) =< aux(20) it(62) =< aux(20) it(63) =< aux(20) s(40) =< aux(20) it(60) =< aux(21) it(62) =< aux(21) it(63) =< aux(21) s(40) =< aux(21) it(58) =< aux(22) it(59) =< aux(22) it(62) =< aux(22) it(63) =< aux(22) it(59) =< aux(24) it(60) =< aux(24) it(62) =< aux(24) it(63) =< aux(24) s(38) =< aux(24) it(59) =< aux(25) it(60) =< aux(25) it(62) =< aux(25) it(63) =< aux(25) s(38) =< aux(25) s(39) =< s(40) s(37) =< s(38) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=6,V5>=0,Out>=9,7*V+16>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],71,87]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+2*s(57)+7 Such that:aux(13) =< V aux(14) =< V+13 aux(18) =< 2*V+25 aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(20) =< 3*V aux(21) =< 3*V+39 aux(25) =< 8*V+104 aux(22) =< 2/3*V aux(24) =< 8/3*V aux(158) =< 2*V+26 s(57) =< aux(158) it(56) =< aux(13) it(57) =< aux(13) it(58) =< aux(13) it(59) =< aux(13) it(60) =< aux(13) it(62) =< aux(13) it(63) =< aux(13) it(56) =< aux(14) it(57) =< aux(14) it(58) =< aux(14) it(59) =< aux(14) it(60) =< aux(14) it(62) =< aux(14) it(63) =< aux(14) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(18) it(57) =< aux(18) it(58) =< aux(18) it(59) =< aux(18) it(60) =< aux(18) it(62) =< aux(18) it(63) =< aux(18) it(57) =< aux(158) it(58) =< aux(158) it(59) =< aux(158) it(60) =< aux(158) it(62) =< aux(158) it(63) =< aux(158) s(34) =< aux(158) s(42) =< aux(158) it(60) =< aux(20) it(62) =< aux(20) it(63) =< aux(20) s(40) =< aux(20) it(60) =< aux(21) it(62) =< aux(21) it(63) =< aux(21) s(40) =< aux(21) it(58) =< aux(22) it(59) =< aux(22) it(62) =< aux(22) it(63) =< aux(22) it(59) =< aux(24) it(60) =< aux(24) it(62) =< aux(24) it(63) =< aux(24) s(38) =< aux(24) it(59) =< aux(25) it(60) =< aux(25) it(62) =< aux(25) it(63) =< aux(25) s(38) =< aux(25) s(39) =< s(40) s(37) =< s(38) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=6,V5>=0,Out>=10,7*V+20>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],70,88]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+2*s(59)+5 Such that:aux(13) =< V aux(14) =< V+7 aux(18) =< 2*V+13 aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(20) =< 3*V aux(21) =< 3*V+21 aux(25) =< 8*V+56 aux(22) =< 2/3*V aux(24) =< 8/3*V aux(160) =< 2*V+14 s(59) =< aux(160) it(56) =< aux(13) it(57) =< aux(13) it(58) =< aux(13) it(59) =< aux(13) it(60) =< aux(13) it(62) =< aux(13) it(63) =< aux(13) it(56) =< aux(14) it(57) =< aux(14) it(58) =< aux(14) it(59) =< aux(14) it(60) =< aux(14) it(62) =< aux(14) it(63) =< aux(14) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(18) it(57) =< aux(18) it(58) =< aux(18) it(59) =< aux(18) it(60) =< aux(18) it(62) =< aux(18) it(63) =< aux(18) it(57) =< aux(160) it(58) =< aux(160) it(59) =< aux(160) it(60) =< aux(160) it(62) =< aux(160) it(63) =< aux(160) s(34) =< aux(160) s(42) =< aux(160) it(60) =< aux(20) it(62) =< aux(20) it(63) =< aux(20) s(40) =< aux(20) it(60) =< aux(21) it(62) =< aux(21) it(63) =< aux(21) s(40) =< aux(21) it(58) =< aux(22) it(59) =< aux(22) it(62) =< aux(22) it(63) =< aux(22) it(59) =< aux(24) it(60) =< aux(24) it(62) =< aux(24) it(63) =< aux(24) s(38) =< aux(24) it(59) =< aux(25) it(60) =< aux(25) it(62) =< aux(25) it(63) =< aux(25) s(38) =< aux(25) s(39) =< s(40) s(37) =< s(38) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=6,V5>=0,Out>=7,7*V+8>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],70,87]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+2*s(59)+6 Such that:aux(13) =< V aux(14) =< V+9 aux(18) =< 2*V+17 aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(20) =< 3*V aux(21) =< 3*V+27 aux(25) =< 8*V+72 aux(22) =< 2/3*V aux(24) =< 8/3*V aux(161) =< 2*V+18 s(59) =< aux(161) it(56) =< aux(13) it(57) =< aux(13) it(58) =< aux(13) it(59) =< aux(13) it(60) =< aux(13) it(62) =< aux(13) it(63) =< aux(13) it(56) =< aux(14) it(57) =< aux(14) it(58) =< aux(14) it(59) =< aux(14) it(60) =< aux(14) it(62) =< aux(14) it(63) =< aux(14) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(18) it(57) =< aux(18) it(58) =< aux(18) it(59) =< aux(18) it(60) =< aux(18) it(62) =< aux(18) it(63) =< aux(18) it(57) =< aux(161) it(58) =< aux(161) it(59) =< aux(161) it(60) =< aux(161) it(62) =< aux(161) it(63) =< aux(161) s(34) =< aux(161) s(42) =< aux(161) it(60) =< aux(20) it(62) =< aux(20) it(63) =< aux(20) s(40) =< aux(20) it(60) =< aux(21) it(62) =< aux(21) it(63) =< aux(21) s(40) =< aux(21) it(58) =< aux(22) it(59) =< aux(22) it(62) =< aux(22) it(63) =< aux(22) it(59) =< aux(24) it(60) =< aux(24) it(62) =< aux(24) it(63) =< aux(24) s(38) =< aux(24) it(59) =< aux(25) it(60) =< aux(25) it(62) =< aux(25) it(63) =< aux(25) s(38) =< aux(25) s(39) =< s(40) s(37) =< s(38) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=6,V5>=0,Out>=8,7*V+12>=4*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],69,88]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+2*s(61)+5 Such that:aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(25) =< 8*V aux(22) =< 2/3*V aux(24) =< 8/3*V aux(163) =< V aux(164) =< 2*V aux(165) =< 3*V s(61) =< aux(164) it(56) =< aux(163) it(57) =< aux(163) it(58) =< aux(163) it(59) =< aux(163) it(60) =< aux(163) it(62) =< aux(163) it(63) =< aux(163) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(164) it(57) =< aux(164) it(58) =< aux(164) it(59) =< aux(164) it(60) =< aux(164) it(62) =< aux(164) it(63) =< aux(164) s(34) =< aux(164) s(42) =< aux(164) it(60) =< aux(165) it(62) =< aux(165) it(63) =< aux(165) it(58) =< aux(22) it(59) =< aux(22) it(62) =< aux(22) it(63) =< aux(22) it(59) =< aux(24) it(60) =< aux(24) it(62) =< aux(24) it(63) =< aux(24) s(38) =< aux(24) it(59) =< aux(25) it(60) =< aux(25) it(62) =< aux(25) it(63) =< aux(25) s(38) =< aux(25) s(39) =< aux(165) s(37) =< s(38) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=4,V5>=0,Out>=6,17*V+16>=8*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],69,87]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+2*s(61)+6 Such that:aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(25) =< 8*V aux(22) =< 2/3*V aux(24) =< 8/3*V aux(166) =< V aux(167) =< 2*V aux(168) =< 3*V s(61) =< aux(167) it(56) =< aux(166) it(57) =< aux(166) it(58) =< aux(166) it(59) =< aux(166) it(60) =< aux(166) it(62) =< aux(166) it(63) =< aux(166) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(167) it(57) =< aux(167) it(58) =< aux(167) it(59) =< aux(167) it(60) =< aux(167) it(62) =< aux(167) it(63) =< aux(167) s(34) =< aux(167) s(42) =< aux(167) it(60) =< aux(168) it(62) =< aux(168) it(63) =< aux(168) it(58) =< aux(22) it(59) =< aux(22) it(62) =< aux(22) it(63) =< aux(22) it(59) =< aux(24) it(60) =< aux(24) it(62) =< aux(24) it(63) =< aux(24) s(38) =< aux(24) it(59) =< aux(25) it(60) =< aux(25) it(62) =< aux(25) it(63) =< aux(25) s(38) =< aux(25) s(39) =< aux(168) s(37) =< s(38) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=4,V5>=0,Out>=7,17*V+24>=8*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],68,88]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+2*s(63)+6 Such that:aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(25) =< 8*V aux(22) =< 2/3*V aux(24) =< 8/3*V aux(170) =< V aux(171) =< 2*V aux(172) =< 3*V s(63) =< aux(171) it(56) =< aux(170) it(57) =< aux(170) it(58) =< aux(170) it(59) =< aux(170) it(60) =< aux(170) it(62) =< aux(170) it(63) =< aux(170) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(171) it(57) =< aux(171) it(58) =< aux(171) it(59) =< aux(171) it(60) =< aux(171) it(62) =< aux(171) it(63) =< aux(171) s(34) =< aux(171) s(42) =< aux(171) it(60) =< aux(172) it(62) =< aux(172) it(63) =< aux(172) it(58) =< aux(22) it(59) =< aux(22) it(62) =< aux(22) it(63) =< aux(22) it(59) =< aux(24) it(60) =< aux(24) it(62) =< aux(24) it(63) =< aux(24) s(38) =< aux(24) it(59) =< aux(25) it(60) =< aux(25) it(62) =< aux(25) it(63) =< aux(25) s(38) =< aux(25) s(39) =< aux(172) s(37) =< s(38) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=4,V5>=0,Out>=8,17*V+32>=8*Out] * Chain [[56,57,58,59,60,61,62,63,64,65,66,67],68,87]: 4*it(56)+3*it(57)+3*it(58)+4*it(59)+7*it(60)+4*it(62)+17*it(63)+4*s(33)+4*s(37)+4*s(39)+4*s(41)+2*s(63)+7 Such that:aux(15) =< 2*V+2/5 aux(16) =< 2*V+36/13 aux(17) =< 2*V+V5 aux(25) =< 8*V aux(22) =< 2/3*V aux(24) =< 8/3*V aux(173) =< V aux(174) =< 2*V aux(175) =< 3*V s(63) =< aux(174) it(56) =< aux(173) it(57) =< aux(173) it(58) =< aux(173) it(59) =< aux(173) it(60) =< aux(173) it(62) =< aux(173) it(63) =< aux(173) it(63) =< aux(15) s(42) =< aux(15) it(57) =< aux(16) it(58) =< aux(16) it(59) =< aux(16) it(60) =< aux(16) it(62) =< aux(16) it(63) =< aux(16) s(34) =< aux(16) it(56) =< aux(17) it(57) =< aux(17) it(58) =< aux(17) it(59) =< aux(17) it(60) =< aux(17) it(62) =< aux(17) it(63) =< aux(17) it(56) =< aux(174) it(57) =< aux(174) it(58) =< aux(174) it(59) =< aux(174) it(60) =< aux(174) it(62) =< aux(174) it(63) =< aux(174) s(34) =< aux(174) s(42) =< aux(174) it(60) =< aux(175) it(62) =< aux(175) it(63) =< aux(175) it(58) =< aux(22) it(59) =< aux(22) it(62) =< aux(22) it(63) =< aux(22) it(59) =< aux(24) it(60) =< aux(24) it(62) =< aux(24) it(63) =< aux(24) s(38) =< aux(24) it(59) =< aux(25) it(60) =< aux(25) it(62) =< aux(25) it(63) =< aux(25) s(38) =< aux(25) s(39) =< aux(175) s(37) =< s(38) s(41) =< s(42) s(33) =< s(34) with precondition: [V>=4,V5>=0,Out>=9,17*V+40>=8*Out] * Chain [88]: 2 with precondition: [Out=1,V>=0,V5>=0] * Chain [87]: 3 with precondition: [V=0,Out=2,V5>=0] * Chain [86]: 2 with precondition: [Out=3,V>=1,V5>=0] * Chain [85,88]: 5 with precondition: [V=1,Out=3,V5>=0] * Chain [85,87]: 6 with precondition: [V=1,Out=4,V5>=0] * Chain [84,88]: 5 with precondition: [V=1,Out=4,V5>=0] * Chain [84,87]: 6 with precondition: [V=1,Out=5,V5>=0] * Chain [83,88]: 6 with precondition: [V=1,Out=5,V5>=0] * Chain [83,87]: 7 with precondition: [V=1,Out=6,V5>=0] * Chain [82,88]: 6 with precondition: [V=1,Out=6,V5>=0] * Chain [82,87]: 7 with precondition: [V=1,Out=7,V5>=0] * Chain [81,88]: 5 with precondition: [V=1,Out=4,V5>=0] * Chain [81,87]: 6 with precondition: [V=1,Out=5,V5>=0] * Chain [80,88]: 6 with precondition: [V=1,Out=6,V5>=0] * Chain [80,87]: 7 with precondition: [V=1,Out=7,V5>=0] * Chain [79,88]: 5 with precondition: [Out=3,V>=3,V5>=0] * Chain [79,87]: 6 with precondition: [Out=4,V>=3,V5>=0] * Chain [78,88]: 6 with precondition: [Out=5,V>=3,V5>=0] * Chain [78,87]: 7 with precondition: [Out=6,V>=3,V5>=0] * Chain [77,88]: 2*s(49)+6 Such that:aux(116) =< 2*Out s(49) =< aux(116) with precondition: [V+11=2*Out,V>=3,V5>=0] * Chain [77,87]: 2*s(49)+7 Such that:aux(116) =< 2*Out s(49) =< aux(116) with precondition: [V+13=2*Out,V>=3,V5>=0] * Chain [76,88]: 2*s(51)+5 Such that:aux(119) =< 2*Out s(51) =< aux(119) with precondition: [V+7=2*Out,V>=3,V5>=0] * Chain [76,87]: 2*s(51)+6 Such that:aux(119) =< 2*Out s(51) =< aux(119) with precondition: [V+9=2*Out,V>=3,V5>=0] * Chain [75,88]: 2*s(53)+5 Such that:aux(122) =< V s(53) =< aux(122) with precondition: [V>=3,V5>=0,Out>=4,V+6>=2*Out] * Chain [75,87]: 2*s(53)+6 Such that:aux(122) =< V s(53) =< aux(122) with precondition: [V>=3,V5>=0,Out>=5,V+8>=2*Out] * Chain [74,88]: 2*s(55)+6 Such that:aux(129) =< V s(55) =< aux(129) with precondition: [V>=3,V5>=0,Out>=6,V+10>=2*Out] * Chain [74,87]: 2*s(55)+7 Such that:aux(129) =< V s(55) =< aux(129) with precondition: [V>=3,V5>=0,Out>=7,V+12>=2*Out] * Chain [73,88]: 5 with precondition: [Out=3,V>=1,V5>=0] * Chain [73,87]: 6 with precondition: [Out=4,V>=1,V5>=0] * Chain [72,88]: 6 with precondition: [Out=5,V>=1,V5>=0] * Chain [72,87]: 7 with precondition: [Out=6,V>=1,V5>=0] * Chain [71,88]: 2*s(57)+6 Such that:aux(156) =< 2*Out s(57) =< aux(156) with precondition: [V+11=2*Out,V>=3,V5>=0] * Chain [71,87]: 2*s(57)+7 Such that:aux(156) =< 2*Out s(57) =< aux(156) with precondition: [V+13=2*Out,V>=3,V5>=0] * Chain [70,88]: 2*s(59)+5 Such that:aux(159) =< 2*Out s(59) =< aux(159) with precondition: [V+7=2*Out,V>=3,V5>=0] * Chain [70,87]: 2*s(59)+6 Such that:aux(159) =< 2*Out s(59) =< aux(159) with precondition: [V+9=2*Out,V>=3,V5>=0] * Chain [69,88]: 2*s(61)+5 Such that:aux(162) =< V s(61) =< aux(162) with precondition: [V5>=0,Out>=4,V+6>=2*Out] * Chain [69,87]: 2*s(61)+6 Such that:aux(162) =< V s(61) =< aux(162) with precondition: [V5>=0,Out>=5,V+8>=2*Out] * Chain [68,88]: 2*s(63)+6 Such that:aux(169) =< V s(63) =< aux(169) with precondition: [V5>=0,Out>=6,V+10>=2*Out] * Chain [68,87]: 2*s(63)+7 Such that:aux(169) =< V s(63) =< aux(169) with precondition: [V5>=0,Out>=7,V+12>=2*Out] #### Cost of chains of start(V,V5,V9): * Chain [91]: 2*s(975)+34*s(976)+8*s(1010)+8*s(1011)+6*s(1012)+6*s(1013)+8*s(1014)+14*s(1015)+8*s(1016)+34*s(1017)+16*s(1022)+16*s(1023)+16*s(1024)+16*s(1025)+8*s(1026)+8*s(1027)+6*s(1028)+6*s(1029)+8*s(1030)+14*s(1031)+8*s(1032)+34*s(1033)+16*s(1038)+16*s(1039)+16*s(1040)+16*s(1041)+8*s(1042)+8*s(1043)+6*s(1044)+6*s(1045)+8*s(1046)+14*s(1047)+8*s(1048)+34*s(1049)+16*s(1054)+16*s(1055)+16*s(1056)+16*s(1057)+8*s(1058)+8*s(1059)+6*s(1060)+6*s(1061)+8*s(1062)+14*s(1063)+8*s(1064)+34*s(1065)+16*s(1070)+16*s(1071)+16*s(1072)+16*s(1073)+32*s(1074)+120*s(1075)+90*s(1076)+90*s(1077)+32*s(1078)+56*s(1079)+32*s(1080)+136*s(1081)+240*s(1085)+64*s(1086)+240*s(1087)+240*s(1088)+88*s(1089)+154*s(1090)+88*s(1091)+374*s(1092)+176*s(1093)+8*s(1094)+8*s(1126)+8*s(1149)+8*s(1151)+8*s(1247)+6*s(1248)+6*s(1249)+8*s(1250)+14*s(1251)+8*s(1252)+34*s(1253)+8*s(1263)+6*s(1264)+6*s(1265)+8*s(1266)+14*s(1267)+8*s(1268)+34*s(1269)+8*s(1279)+6*s(1280)+6*s(1281)+8*s(1282)+14*s(1283)+8*s(1284)+34*s(1285)+8*s(1295)+6*s(1296)+6*s(1297)+8*s(1298)+14*s(1299)+8*s(1300)+34*s(1301)+120*s(1311)+90*s(1312)+90*s(1313)+32*s(1314)+56*s(1315)+32*s(1316)+136*s(1317)+88*s(1325)+154*s(1326)+88*s(1327)+374*s(1328)+8 Such that:aux(249) =< V aux(250) =< V+1 aux(251) =< V+7 aux(252) =< V+9 aux(253) =< V+11 aux(254) =< V+13 aux(255) =< 2*V aux(256) =< 2*V+1 aux(257) =< 2*V+13 aux(258) =< 2*V+14 aux(259) =< 2*V+17 aux(260) =< 2*V+18 aux(261) =< 2*V+21 aux(262) =< 2*V+22 aux(263) =< 2*V+25 aux(264) =< 2*V+26 aux(265) =< 2*V+2/5 aux(266) =< 2*V+36/13 aux(267) =< 2*V+V5 aux(268) =< 3*V aux(269) =< 3*V+21 aux(270) =< 3*V+27 aux(271) =< 3*V+33 aux(272) =< 3*V+39 aux(273) =< 8*V aux(274) =< 8*V+56 aux(275) =< 8*V+72 aux(276) =< 8*V+88 aux(277) =< 8*V+104 aux(278) =< 2/3*V aux(279) =< 8/3*V aux(280) =< 13/2*V aux(281) =< 13/2*V+3 aux(282) =< 13/2*V+5 s(976) =< aux(249) s(975) =< aux(250) s(1010) =< aux(260) s(1011) =< aux(249) s(1012) =< aux(249) s(1013) =< aux(249) s(1014) =< aux(249) s(1015) =< aux(249) s(1016) =< aux(249) s(1017) =< aux(249) s(1011) =< aux(252) s(1012) =< aux(252) s(1013) =< aux(252) s(1014) =< aux(252) s(1015) =< aux(252) s(1016) =< aux(252) s(1017) =< aux(252) s(1017) =< aux(265) s(1018) =< aux(265) s(1012) =< aux(266) s(1013) =< aux(266) s(1014) =< aux(266) s(1015) =< aux(266) s(1016) =< aux(266) s(1017) =< aux(266) s(1019) =< aux(266) s(1011) =< aux(256) s(1012) =< aux(256) s(1013) =< aux(256) s(1014) =< aux(256) s(1015) =< aux(256) s(1016) =< aux(256) s(1017) =< aux(256) s(1011) =< aux(259) s(1012) =< aux(259) s(1013) =< aux(259) s(1014) =< aux(259) s(1015) =< aux(259) s(1016) =< aux(259) s(1017) =< aux(259) s(1012) =< aux(260) s(1013) =< aux(260) s(1014) =< aux(260) s(1015) =< aux(260) s(1016) =< aux(260) s(1017) =< aux(260) s(1019) =< aux(260) s(1018) =< aux(260) s(1015) =< aux(268) s(1016) =< aux(268) s(1017) =< aux(268) s(1020) =< aux(268) s(1015) =< aux(270) s(1016) =< aux(270) s(1017) =< aux(270) s(1020) =< aux(270) s(1013) =< aux(278) s(1014) =< aux(278) s(1016) =< aux(278) s(1017) =< aux(278) s(1014) =< aux(279) s(1015) =< aux(279) s(1016) =< aux(279) s(1017) =< aux(279) s(1021) =< aux(279) s(1014) =< aux(275) s(1015) =< aux(275) s(1016) =< aux(275) s(1017) =< aux(275) s(1021) =< aux(275) s(1022) =< s(1020) s(1023) =< s(1021) s(1024) =< s(1018) s(1025) =< s(1019) s(1026) =< aux(258) s(1027) =< aux(249) s(1028) =< aux(249) s(1029) =< aux(249) s(1030) =< aux(249) s(1031) =< aux(249) s(1032) =< aux(249) s(1033) =< aux(249) s(1027) =< aux(251) s(1028) =< aux(251) s(1029) =< aux(251) s(1030) =< aux(251) s(1031) =< aux(251) s(1032) =< aux(251) s(1033) =< aux(251) s(1033) =< aux(265) s(1034) =< aux(265) s(1028) =< aux(266) s(1029) =< aux(266) s(1030) =< aux(266) s(1031) =< aux(266) s(1032) =< aux(266) s(1033) =< aux(266) s(1035) =< aux(266) s(1027) =< aux(256) s(1028) =< aux(256) s(1029) =< aux(256) s(1030) =< aux(256) s(1031) =< aux(256) s(1032) =< aux(256) s(1033) =< aux(256) s(1027) =< aux(257) s(1028) =< aux(257) s(1029) =< aux(257) s(1030) =< aux(257) s(1031) =< aux(257) s(1032) =< aux(257) s(1033) =< aux(257) s(1028) =< aux(258) s(1029) =< aux(258) s(1030) =< aux(258) s(1031) =< aux(258) s(1032) =< aux(258) s(1033) =< aux(258) s(1035) =< aux(258) s(1034) =< aux(258) s(1031) =< aux(268) s(1032) =< aux(268) s(1033) =< aux(268) s(1036) =< aux(268) s(1031) =< aux(269) s(1032) =< aux(269) s(1033) =< aux(269) s(1036) =< aux(269) s(1029) =< aux(278) s(1030) =< aux(278) s(1032) =< aux(278) s(1033) =< aux(278) s(1030) =< aux(279) s(1031) =< aux(279) s(1032) =< aux(279) s(1033) =< aux(279) s(1037) =< aux(279) s(1030) =< aux(274) s(1031) =< aux(274) s(1032) =< aux(274) s(1033) =< aux(274) s(1037) =< aux(274) s(1038) =< s(1036) s(1039) =< s(1037) s(1040) =< s(1034) s(1041) =< s(1035) s(1042) =< aux(264) s(1043) =< aux(249) s(1044) =< aux(249) s(1045) =< aux(249) s(1046) =< aux(249) s(1047) =< aux(249) s(1048) =< aux(249) s(1049) =< aux(249) s(1043) =< aux(254) s(1044) =< aux(254) s(1045) =< aux(254) s(1046) =< aux(254) s(1047) =< aux(254) s(1048) =< aux(254) s(1049) =< aux(254) s(1049) =< aux(265) s(1050) =< aux(265) s(1044) =< aux(266) s(1045) =< aux(266) s(1046) =< aux(266) s(1047) =< aux(266) s(1048) =< aux(266) s(1049) =< aux(266) s(1051) =< aux(266) s(1043) =< aux(256) s(1044) =< aux(256) s(1045) =< aux(256) s(1046) =< aux(256) s(1047) =< aux(256) s(1048) =< aux(256) s(1049) =< aux(256) s(1043) =< aux(263) s(1044) =< aux(263) s(1045) =< aux(263) s(1046) =< aux(263) s(1047) =< aux(263) s(1048) =< aux(263) s(1049) =< aux(263) s(1044) =< aux(264) s(1045) =< aux(264) s(1046) =< aux(264) s(1047) =< aux(264) s(1048) =< aux(264) s(1049) =< aux(264) s(1051) =< aux(264) s(1050) =< aux(264) s(1047) =< aux(268) s(1048) =< aux(268) s(1049) =< aux(268) s(1052) =< aux(268) s(1047) =< aux(272) s(1048) =< aux(272) s(1049) =< aux(272) s(1052) =< aux(272) s(1045) =< aux(278) s(1046) =< aux(278) s(1048) =< aux(278) s(1049) =< aux(278) s(1046) =< aux(279) s(1047) =< aux(279) s(1048) =< aux(279) s(1049) =< aux(279) s(1053) =< aux(279) s(1046) =< aux(277) s(1047) =< aux(277) s(1048) =< aux(277) s(1049) =< aux(277) s(1053) =< aux(277) s(1054) =< s(1052) s(1055) =< s(1053) s(1056) =< s(1050) s(1057) =< s(1051) s(1058) =< aux(262) s(1059) =< aux(249) s(1060) =< aux(249) s(1061) =< aux(249) s(1062) =< aux(249) s(1063) =< aux(249) s(1064) =< aux(249) s(1065) =< aux(249) s(1059) =< aux(253) s(1060) =< aux(253) s(1061) =< aux(253) s(1062) =< aux(253) s(1063) =< aux(253) s(1064) =< aux(253) s(1065) =< aux(253) s(1065) =< aux(265) s(1066) =< aux(265) s(1060) =< aux(266) s(1061) =< aux(266) s(1062) =< aux(266) s(1063) =< aux(266) s(1064) =< aux(266) s(1065) =< aux(266) s(1067) =< aux(266) s(1059) =< aux(256) s(1060) =< aux(256) s(1061) =< aux(256) s(1062) =< aux(256) s(1063) =< aux(256) s(1064) =< aux(256) s(1065) =< aux(256) s(1059) =< aux(261) s(1060) =< aux(261) s(1061) =< aux(261) s(1062) =< aux(261) s(1063) =< aux(261) s(1064) =< aux(261) s(1065) =< aux(261) s(1060) =< aux(262) s(1061) =< aux(262) s(1062) =< aux(262) s(1063) =< aux(262) s(1064) =< aux(262) s(1065) =< aux(262) s(1067) =< aux(262) s(1066) =< aux(262) s(1063) =< aux(268) s(1064) =< aux(268) s(1065) =< aux(268) s(1068) =< aux(268) s(1063) =< aux(271) s(1064) =< aux(271) s(1065) =< aux(271) s(1068) =< aux(271) s(1061) =< aux(278) s(1062) =< aux(278) s(1064) =< aux(278) s(1065) =< aux(278) s(1062) =< aux(279) s(1063) =< aux(279) s(1064) =< aux(279) s(1065) =< aux(279) s(1069) =< aux(279) s(1062) =< aux(276) s(1063) =< aux(276) s(1064) =< aux(276) s(1065) =< aux(276) s(1069) =< aux(276) s(1070) =< s(1068) s(1071) =< s(1069) s(1072) =< s(1066) s(1073) =< s(1067) s(1074) =< aux(255) s(1075) =< aux(249) s(1076) =< aux(249) s(1077) =< aux(249) s(1078) =< aux(249) s(1079) =< aux(249) s(1080) =< aux(249) s(1081) =< aux(249) s(1081) =< aux(265) s(1082) =< aux(265) s(1076) =< aux(266) s(1077) =< aux(266) s(1078) =< aux(266) s(1079) =< aux(266) s(1080) =< aux(266) s(1081) =< aux(266) s(1083) =< aux(266) s(1075) =< aux(256) s(1076) =< aux(256) s(1077) =< aux(256) s(1078) =< aux(256) s(1079) =< aux(256) s(1080) =< aux(256) s(1081) =< aux(256) s(1075) =< aux(255) s(1076) =< aux(255) s(1077) =< aux(255) s(1078) =< aux(255) s(1079) =< aux(255) s(1080) =< aux(255) s(1081) =< aux(255) s(1083) =< aux(255) s(1082) =< aux(255) s(1079) =< aux(268) s(1080) =< aux(268) s(1081) =< aux(268) s(1077) =< aux(278) s(1078) =< aux(278) s(1080) =< aux(278) s(1081) =< aux(278) s(1078) =< aux(279) s(1079) =< aux(279) s(1080) =< aux(279) s(1081) =< aux(279) s(1084) =< aux(279) s(1078) =< aux(273) s(1079) =< aux(273) s(1080) =< aux(273) s(1081) =< aux(273) s(1084) =< aux(273) s(1085) =< aux(268) s(1086) =< s(1084) s(1087) =< s(1082) s(1088) =< s(1083) s(1089) =< aux(249) s(1090) =< aux(249) s(1091) =< aux(249) s(1092) =< aux(249) s(1092) =< aux(265) s(1089) =< aux(266) s(1090) =< aux(266) s(1091) =< aux(266) s(1092) =< aux(266) s(1089) =< aux(256) s(1090) =< aux(256) s(1091) =< aux(256) s(1092) =< aux(256) s(1089) =< aux(255) s(1090) =< aux(255) s(1091) =< aux(255) s(1092) =< aux(255) s(1090) =< aux(268) s(1091) =< aux(268) s(1092) =< aux(268) s(1089) =< aux(278) s(1091) =< aux(278) s(1092) =< aux(278) s(1089) =< aux(279) s(1090) =< aux(279) s(1091) =< aux(279) s(1092) =< aux(279) s(1093) =< aux(279) s(1094) =< aux(280) s(1126) =< aux(281) s(1149) =< aux(282) s(1247) =< aux(249) s(1248) =< aux(249) s(1249) =< aux(249) s(1250) =< aux(249) s(1251) =< aux(249) s(1252) =< aux(249) s(1253) =< aux(249) s(1247) =< aux(252) s(1248) =< aux(252) s(1249) =< aux(252) s(1250) =< aux(252) s(1251) =< aux(252) s(1252) =< aux(252) s(1253) =< aux(252) s(1253) =< aux(265) s(1248) =< aux(266) s(1249) =< aux(266) s(1250) =< aux(266) s(1251) =< aux(266) s(1252) =< aux(266) s(1253) =< aux(266) s(1247) =< aux(267) s(1248) =< aux(267) s(1249) =< aux(267) s(1250) =< aux(267) s(1251) =< aux(267) s(1252) =< aux(267) s(1253) =< aux(267) s(1247) =< aux(259) s(1248) =< aux(259) s(1249) =< aux(259) s(1250) =< aux(259) s(1251) =< aux(259) s(1252) =< aux(259) s(1253) =< aux(259) s(1248) =< aux(260) s(1249) =< aux(260) s(1250) =< aux(260) s(1251) =< aux(260) s(1252) =< aux(260) s(1253) =< aux(260) s(1251) =< aux(268) s(1252) =< aux(268) s(1253) =< aux(268) s(1251) =< aux(270) s(1252) =< aux(270) s(1253) =< aux(270) s(1249) =< aux(278) s(1250) =< aux(278) s(1252) =< aux(278) s(1253) =< aux(278) s(1250) =< aux(279) s(1251) =< aux(279) s(1252) =< aux(279) s(1253) =< aux(279) s(1250) =< aux(275) s(1251) =< aux(275) s(1252) =< aux(275) s(1253) =< aux(275) s(1263) =< aux(249) s(1264) =< aux(249) s(1265) =< aux(249) s(1266) =< aux(249) s(1267) =< aux(249) s(1268) =< aux(249) s(1269) =< aux(249) s(1263) =< aux(251) s(1264) =< aux(251) s(1265) =< aux(251) s(1266) =< aux(251) s(1267) =< aux(251) s(1268) =< aux(251) s(1269) =< aux(251) s(1269) =< aux(265) s(1264) =< aux(266) s(1265) =< aux(266) s(1266) =< aux(266) s(1267) =< aux(266) s(1268) =< aux(266) s(1269) =< aux(266) s(1263) =< aux(267) s(1264) =< aux(267) s(1265) =< aux(267) s(1266) =< aux(267) s(1267) =< aux(267) s(1268) =< aux(267) s(1269) =< aux(267) s(1263) =< aux(257) s(1264) =< aux(257) s(1265) =< aux(257) s(1266) =< aux(257) s(1267) =< aux(257) s(1268) =< aux(257) s(1269) =< aux(257) s(1264) =< aux(258) s(1265) =< aux(258) s(1266) =< aux(258) s(1267) =< aux(258) s(1268) =< aux(258) s(1269) =< aux(258) s(1267) =< aux(268) s(1268) =< aux(268) s(1269) =< aux(268) s(1267) =< aux(269) s(1268) =< aux(269) s(1269) =< aux(269) s(1265) =< aux(278) s(1266) =< aux(278) s(1268) =< aux(278) s(1269) =< aux(278) s(1266) =< aux(279) s(1267) =< aux(279) s(1268) =< aux(279) s(1269) =< aux(279) s(1266) =< aux(274) s(1267) =< aux(274) s(1268) =< aux(274) s(1269) =< aux(274) s(1279) =< aux(249) s(1280) =< aux(249) s(1281) =< aux(249) s(1282) =< aux(249) s(1283) =< aux(249) s(1284) =< aux(249) s(1285) =< aux(249) s(1279) =< aux(254) s(1280) =< aux(254) s(1281) =< aux(254) s(1282) =< aux(254) s(1283) =< aux(254) s(1284) =< aux(254) s(1285) =< aux(254) s(1285) =< aux(265) s(1280) =< aux(266) s(1281) =< aux(266) s(1282) =< aux(266) s(1283) =< aux(266) s(1284) =< aux(266) s(1285) =< aux(266) s(1279) =< aux(267) s(1280) =< aux(267) s(1281) =< aux(267) s(1282) =< aux(267) s(1283) =< aux(267) s(1284) =< aux(267) s(1285) =< aux(267) s(1279) =< aux(263) s(1280) =< aux(263) s(1281) =< aux(263) s(1282) =< aux(263) s(1283) =< aux(263) s(1284) =< aux(263) s(1285) =< aux(263) s(1280) =< aux(264) s(1281) =< aux(264) s(1282) =< aux(264) s(1283) =< aux(264) s(1284) =< aux(264) s(1285) =< aux(264) s(1283) =< aux(268) s(1284) =< aux(268) s(1285) =< aux(268) s(1283) =< aux(272) s(1284) =< aux(272) s(1285) =< aux(272) s(1281) =< aux(278) s(1282) =< aux(278) s(1284) =< aux(278) s(1285) =< aux(278) s(1282) =< aux(279) s(1283) =< aux(279) s(1284) =< aux(279) s(1285) =< aux(279) s(1282) =< aux(277) s(1283) =< aux(277) s(1284) =< aux(277) s(1285) =< aux(277) s(1295) =< aux(249) s(1296) =< aux(249) s(1297) =< aux(249) s(1298) =< aux(249) s(1299) =< aux(249) s(1300) =< aux(249) s(1301) =< aux(249) s(1295) =< aux(253) s(1296) =< aux(253) s(1297) =< aux(253) s(1298) =< aux(253) s(1299) =< aux(253) s(1300) =< aux(253) s(1301) =< aux(253) s(1301) =< aux(265) s(1296) =< aux(266) s(1297) =< aux(266) s(1298) =< aux(266) s(1299) =< aux(266) s(1300) =< aux(266) s(1301) =< aux(266) s(1295) =< aux(267) s(1296) =< aux(267) s(1297) =< aux(267) s(1298) =< aux(267) s(1299) =< aux(267) s(1300) =< aux(267) s(1301) =< aux(267) s(1295) =< aux(261) s(1296) =< aux(261) s(1297) =< aux(261) s(1298) =< aux(261) s(1299) =< aux(261) s(1300) =< aux(261) s(1301) =< aux(261) s(1296) =< aux(262) s(1297) =< aux(262) s(1298) =< aux(262) s(1299) =< aux(262) s(1300) =< aux(262) s(1301) =< aux(262) s(1299) =< aux(268) s(1300) =< aux(268) s(1301) =< aux(268) s(1299) =< aux(271) s(1300) =< aux(271) s(1301) =< aux(271) s(1297) =< aux(278) s(1298) =< aux(278) s(1300) =< aux(278) s(1301) =< aux(278) s(1298) =< aux(279) s(1299) =< aux(279) s(1300) =< aux(279) s(1301) =< aux(279) s(1298) =< aux(276) s(1299) =< aux(276) s(1300) =< aux(276) s(1301) =< aux(276) s(1311) =< aux(249) s(1312) =< aux(249) s(1313) =< aux(249) s(1314) =< aux(249) s(1315) =< aux(249) s(1316) =< aux(249) s(1317) =< aux(249) s(1317) =< aux(265) s(1312) =< aux(266) s(1313) =< aux(266) s(1314) =< aux(266) s(1315) =< aux(266) s(1316) =< aux(266) s(1317) =< aux(266) s(1311) =< aux(267) s(1312) =< aux(267) s(1313) =< aux(267) s(1314) =< aux(267) s(1315) =< aux(267) s(1316) =< aux(267) s(1317) =< aux(267) s(1311) =< aux(255) s(1312) =< aux(255) s(1313) =< aux(255) s(1314) =< aux(255) s(1315) =< aux(255) s(1316) =< aux(255) s(1317) =< aux(255) s(1315) =< aux(268) s(1316) =< aux(268) s(1317) =< aux(268) s(1313) =< aux(278) s(1314) =< aux(278) s(1316) =< aux(278) s(1317) =< aux(278) s(1314) =< aux(279) s(1315) =< aux(279) s(1316) =< aux(279) s(1317) =< aux(279) s(1314) =< aux(273) s(1315) =< aux(273) s(1316) =< aux(273) s(1317) =< aux(273) s(1325) =< aux(249) s(1326) =< aux(249) s(1327) =< aux(249) s(1328) =< aux(249) s(1328) =< aux(265) s(1325) =< aux(266) s(1326) =< aux(266) s(1327) =< aux(266) s(1328) =< aux(266) s(1325) =< aux(267) s(1326) =< aux(267) s(1327) =< aux(267) s(1328) =< aux(267) s(1325) =< aux(255) s(1326) =< aux(255) s(1327) =< aux(255) s(1328) =< aux(255) s(1326) =< aux(268) s(1327) =< aux(268) s(1328) =< aux(268) s(1325) =< aux(278) s(1327) =< aux(278) s(1328) =< aux(278) s(1325) =< aux(279) s(1326) =< aux(279) s(1327) =< aux(279) s(1328) =< aux(279) s(1151) =< aux(251) with precondition: [V>=0] * Chain [90]: 60*s(1451)+252*s(1452)+192*s(1501)+48*s(1502)+48*s(1503)+36*s(1504)+36*s(1505)+48*s(1506)+84*s(1507)+48*s(1508)+204*s(1509)+96*s(1514)+96*s(1515)+96*s(1516)+96*s(1517)+48*s(1518)+48*s(1519)+36*s(1520)+36*s(1521)+48*s(1522)+84*s(1523)+48*s(1524)+204*s(1525)+96*s(1530)+96*s(1531)+96*s(1532)+96*s(1533)+48*s(1534)+48*s(1535)+36*s(1536)+36*s(1537)+48*s(1538)+84*s(1539)+48*s(1540)+204*s(1541)+96*s(1546)+96*s(1547)+96*s(1548)+96*s(1549)+48*s(1550)+48*s(1551)+36*s(1552)+36*s(1553)+48*s(1554)+84*s(1555)+48*s(1556)+204*s(1557)+96*s(1562)+96*s(1563)+96*s(1564)+96*s(1565)+720*s(1567)+540*s(1568)+540*s(1569)+192*s(1570)+336*s(1571)+192*s(1572)+816*s(1573)+1440*s(1577)+384*s(1578)+1440*s(1579)+1440*s(1580)+528*s(1581)+924*s(1582)+528*s(1583)+2244*s(1584)+1056*s(1585)+48*s(1586)+48*s(1852)+48*s(1941)+48*s(1991)+48*s(2237)+36*s(2238)+36*s(2239)+48*s(2240)+84*s(2241)+48*s(2242)+204*s(2243)+48*s(2253)+36*s(2254)+36*s(2255)+48*s(2256)+84*s(2257)+48*s(2258)+204*s(2259)+48*s(2269)+36*s(2270)+36*s(2271)+48*s(2272)+84*s(2273)+48*s(2274)+204*s(2275)+48*s(2285)+36*s(2286)+36*s(2287)+48*s(2288)+84*s(2289)+48*s(2290)+204*s(2291)+720*s(2301)+540*s(2302)+540*s(2303)+192*s(2304)+336*s(2305)+192*s(2306)+816*s(2307)+528*s(2315)+924*s(2316)+528*s(2317)+2244*s(2318)+9 Such that:aux(307) =< V5 aux(308) =< V5+1 aux(309) =< V5+13 aux(310) =< V5+14 aux(311) =< V5+17 aux(312) =< V5+18 aux(313) =< V5+21 aux(314) =< V5+22 aux(315) =< V5+25 aux(316) =< V5+26 aux(317) =< V5+2/5 aux(318) =< V5+36/13 aux(319) =< V5+V9+1 aux(320) =< V5+V9+2 aux(321) =< 4*V5 aux(322) =< 4*V5+56 aux(323) =< 4*V5+72 aux(324) =< 4*V5+88 aux(325) =< 4*V5+104 aux(326) =< V5/2 aux(327) =< V5/2+7 aux(328) =< V5/2+9 aux(329) =< V5/2+11 aux(330) =< V5/2+13 aux(331) =< V5/3 aux(332) =< 3/2*V5 aux(333) =< 3/2*V5+21 aux(334) =< 3/2*V5+27 aux(335) =< 3/2*V5+33 aux(336) =< 3/2*V5+39 aux(337) =< 4/3*V5 aux(338) =< 13/4*V5 aux(339) =< 13/4*V5+3 aux(340) =< 13/4*V5+5 s(1452) =< aux(307) s(1451) =< aux(308) s(1501) =< aux(326) s(1502) =< aux(312) s(1503) =< aux(326) s(1504) =< aux(326) s(1505) =< aux(326) s(1506) =< aux(326) s(1507) =< aux(326) s(1508) =< aux(326) s(1509) =< aux(326) s(1503) =< aux(328) s(1504) =< aux(328) s(1505) =< aux(328) s(1506) =< aux(328) s(1507) =< aux(328) s(1508) =< aux(328) s(1509) =< aux(328) s(1509) =< aux(317) s(1510) =< aux(317) s(1504) =< aux(318) s(1505) =< aux(318) s(1506) =< aux(318) s(1507) =< aux(318) s(1508) =< aux(318) s(1509) =< aux(318) s(1511) =< aux(318) s(1503) =< aux(319) s(1504) =< aux(319) s(1505) =< aux(319) s(1506) =< aux(319) s(1507) =< aux(319) s(1508) =< aux(319) s(1509) =< aux(319) s(1503) =< aux(311) s(1504) =< aux(311) s(1505) =< aux(311) s(1506) =< aux(311) s(1507) =< aux(311) s(1508) =< aux(311) s(1509) =< aux(311) s(1504) =< aux(312) s(1505) =< aux(312) s(1506) =< aux(312) s(1507) =< aux(312) s(1508) =< aux(312) s(1509) =< aux(312) s(1511) =< aux(312) s(1510) =< aux(312) s(1507) =< aux(332) s(1508) =< aux(332) s(1509) =< aux(332) s(1512) =< aux(332) s(1507) =< aux(334) s(1508) =< aux(334) s(1509) =< aux(334) s(1512) =< aux(334) s(1505) =< aux(331) s(1506) =< aux(331) s(1508) =< aux(331) s(1509) =< aux(331) s(1506) =< aux(337) s(1507) =< aux(337) s(1508) =< aux(337) s(1509) =< aux(337) s(1513) =< aux(337) s(1506) =< aux(323) s(1507) =< aux(323) s(1508) =< aux(323) s(1509) =< aux(323) s(1513) =< aux(323) s(1514) =< s(1512) s(1515) =< s(1513) s(1516) =< s(1510) s(1517) =< s(1511) s(1518) =< aux(310) s(1519) =< aux(326) s(1520) =< aux(326) s(1521) =< aux(326) s(1522) =< aux(326) s(1523) =< aux(326) s(1524) =< aux(326) s(1525) =< aux(326) s(1519) =< aux(327) s(1520) =< aux(327) s(1521) =< aux(327) s(1522) =< aux(327) s(1523) =< aux(327) s(1524) =< aux(327) s(1525) =< aux(327) s(1525) =< aux(317) s(1526) =< aux(317) s(1520) =< aux(318) s(1521) =< aux(318) s(1522) =< aux(318) s(1523) =< aux(318) s(1524) =< aux(318) s(1525) =< aux(318) s(1527) =< aux(318) s(1519) =< aux(319) s(1520) =< aux(319) s(1521) =< aux(319) s(1522) =< aux(319) s(1523) =< aux(319) s(1524) =< aux(319) s(1525) =< aux(319) s(1519) =< aux(309) s(1520) =< aux(309) s(1521) =< aux(309) s(1522) =< aux(309) s(1523) =< aux(309) s(1524) =< aux(309) s(1525) =< aux(309) s(1520) =< aux(310) s(1521) =< aux(310) s(1522) =< aux(310) s(1523) =< aux(310) s(1524) =< aux(310) s(1525) =< aux(310) s(1527) =< aux(310) s(1526) =< aux(310) s(1523) =< aux(332) s(1524) =< aux(332) s(1525) =< aux(332) s(1528) =< aux(332) s(1523) =< aux(333) s(1524) =< aux(333) s(1525) =< aux(333) s(1528) =< aux(333) s(1521) =< aux(331) s(1522) =< aux(331) s(1524) =< aux(331) s(1525) =< aux(331) s(1522) =< aux(337) s(1523) =< aux(337) s(1524) =< aux(337) s(1525) =< aux(337) s(1529) =< aux(337) s(1522) =< aux(322) s(1523) =< aux(322) s(1524) =< aux(322) s(1525) =< aux(322) s(1529) =< aux(322) s(1530) =< s(1528) s(1531) =< s(1529) s(1532) =< s(1526) s(1533) =< s(1527) s(1534) =< aux(316) s(1535) =< aux(326) s(1536) =< aux(326) s(1537) =< aux(326) s(1538) =< aux(326) s(1539) =< aux(326) s(1540) =< aux(326) s(1541) =< aux(326) s(1535) =< aux(330) s(1536) =< aux(330) s(1537) =< aux(330) s(1538) =< aux(330) s(1539) =< aux(330) s(1540) =< aux(330) s(1541) =< aux(330) s(1541) =< aux(317) s(1542) =< aux(317) s(1536) =< aux(318) s(1537) =< aux(318) s(1538) =< aux(318) s(1539) =< aux(318) s(1540) =< aux(318) s(1541) =< aux(318) s(1543) =< aux(318) s(1535) =< aux(319) s(1536) =< aux(319) s(1537) =< aux(319) s(1538) =< aux(319) s(1539) =< aux(319) s(1540) =< aux(319) s(1541) =< aux(319) s(1535) =< aux(315) s(1536) =< aux(315) s(1537) =< aux(315) s(1538) =< aux(315) s(1539) =< aux(315) s(1540) =< aux(315) s(1541) =< aux(315) s(1536) =< aux(316) s(1537) =< aux(316) s(1538) =< aux(316) s(1539) =< aux(316) s(1540) =< aux(316) s(1541) =< aux(316) s(1543) =< aux(316) s(1542) =< aux(316) s(1539) =< aux(332) s(1540) =< aux(332) s(1541) =< aux(332) s(1544) =< aux(332) s(1539) =< aux(336) s(1540) =< aux(336) s(1541) =< aux(336) s(1544) =< aux(336) s(1537) =< aux(331) s(1538) =< aux(331) s(1540) =< aux(331) s(1541) =< aux(331) s(1538) =< aux(337) s(1539) =< aux(337) s(1540) =< aux(337) s(1541) =< aux(337) s(1545) =< aux(337) s(1538) =< aux(325) s(1539) =< aux(325) s(1540) =< aux(325) s(1541) =< aux(325) s(1545) =< aux(325) s(1546) =< s(1544) s(1547) =< s(1545) s(1548) =< s(1542) s(1549) =< s(1543) s(1550) =< aux(314) s(1551) =< aux(326) s(1552) =< aux(326) s(1553) =< aux(326) s(1554) =< aux(326) s(1555) =< aux(326) s(1556) =< aux(326) s(1557) =< aux(326) s(1551) =< aux(329) s(1552) =< aux(329) s(1553) =< aux(329) s(1554) =< aux(329) s(1555) =< aux(329) s(1556) =< aux(329) s(1557) =< aux(329) s(1557) =< aux(317) s(1558) =< aux(317) s(1552) =< aux(318) s(1553) =< aux(318) s(1554) =< aux(318) s(1555) =< aux(318) s(1556) =< aux(318) s(1557) =< aux(318) s(1559) =< aux(318) s(1551) =< aux(319) s(1552) =< aux(319) s(1553) =< aux(319) s(1554) =< aux(319) s(1555) =< aux(319) s(1556) =< aux(319) s(1557) =< aux(319) s(1551) =< aux(313) s(1552) =< aux(313) s(1553) =< aux(313) s(1554) =< aux(313) s(1555) =< aux(313) s(1556) =< aux(313) s(1557) =< aux(313) s(1552) =< aux(314) s(1553) =< aux(314) s(1554) =< aux(314) s(1555) =< aux(314) s(1556) =< aux(314) s(1557) =< aux(314) s(1559) =< aux(314) s(1558) =< aux(314) s(1555) =< aux(332) s(1556) =< aux(332) s(1557) =< aux(332) s(1560) =< aux(332) s(1555) =< aux(335) s(1556) =< aux(335) s(1557) =< aux(335) s(1560) =< aux(335) s(1553) =< aux(331) s(1554) =< aux(331) s(1556) =< aux(331) s(1557) =< aux(331) s(1554) =< aux(337) s(1555) =< aux(337) s(1556) =< aux(337) s(1557) =< aux(337) s(1561) =< aux(337) s(1554) =< aux(324) s(1555) =< aux(324) s(1556) =< aux(324) s(1557) =< aux(324) s(1561) =< aux(324) s(1562) =< s(1560) s(1563) =< s(1561) s(1564) =< s(1558) s(1565) =< s(1559) s(1567) =< aux(326) s(1568) =< aux(326) s(1569) =< aux(326) s(1570) =< aux(326) s(1571) =< aux(326) s(1572) =< aux(326) s(1573) =< aux(326) s(1573) =< aux(317) s(1574) =< aux(317) s(1568) =< aux(318) s(1569) =< aux(318) s(1570) =< aux(318) s(1571) =< aux(318) s(1572) =< aux(318) s(1573) =< aux(318) s(1575) =< aux(318) s(1567) =< aux(319) s(1568) =< aux(319) s(1569) =< aux(319) s(1570) =< aux(319) s(1571) =< aux(319) s(1572) =< aux(319) s(1573) =< aux(319) s(1567) =< aux(307) s(1568) =< aux(307) s(1569) =< aux(307) s(1570) =< aux(307) s(1571) =< aux(307) s(1572) =< aux(307) s(1573) =< aux(307) s(1575) =< aux(307) s(1574) =< aux(307) s(1571) =< aux(332) s(1572) =< aux(332) s(1573) =< aux(332) s(1569) =< aux(331) s(1570) =< aux(331) s(1572) =< aux(331) s(1573) =< aux(331) s(1570) =< aux(337) s(1571) =< aux(337) s(1572) =< aux(337) s(1573) =< aux(337) s(1576) =< aux(337) s(1570) =< aux(321) s(1571) =< aux(321) s(1572) =< aux(321) s(1573) =< aux(321) s(1576) =< aux(321) s(1577) =< aux(332) s(1578) =< s(1576) s(1579) =< s(1574) s(1580) =< s(1575) s(1581) =< aux(326) s(1582) =< aux(326) s(1583) =< aux(326) s(1584) =< aux(326) s(1584) =< aux(317) s(1581) =< aux(318) s(1582) =< aux(318) s(1583) =< aux(318) s(1584) =< aux(318) s(1581) =< aux(319) s(1582) =< aux(319) s(1583) =< aux(319) s(1584) =< aux(319) s(1581) =< aux(307) s(1582) =< aux(307) s(1583) =< aux(307) s(1584) =< aux(307) s(1582) =< aux(332) s(1583) =< aux(332) s(1584) =< aux(332) s(1581) =< aux(331) s(1583) =< aux(331) s(1584) =< aux(331) s(1581) =< aux(337) s(1582) =< aux(337) s(1583) =< aux(337) s(1584) =< aux(337) s(1585) =< aux(337) s(1586) =< aux(338) s(1852) =< aux(339) s(1941) =< aux(340) s(1991) =< aux(327) s(2237) =< aux(326) s(2238) =< aux(326) s(2239) =< aux(326) s(2240) =< aux(326) s(2241) =< aux(326) s(2242) =< aux(326) s(2243) =< aux(326) s(2237) =< aux(328) s(2238) =< aux(328) s(2239) =< aux(328) s(2240) =< aux(328) s(2241) =< aux(328) s(2242) =< aux(328) s(2243) =< aux(328) s(2243) =< aux(317) s(2238) =< aux(318) s(2239) =< aux(318) s(2240) =< aux(318) s(2241) =< aux(318) s(2242) =< aux(318) s(2243) =< aux(318) s(2237) =< aux(320) s(2238) =< aux(320) s(2239) =< aux(320) s(2240) =< aux(320) s(2241) =< aux(320) s(2242) =< aux(320) s(2243) =< aux(320) s(2237) =< aux(311) s(2238) =< aux(311) s(2239) =< aux(311) s(2240) =< aux(311) s(2241) =< aux(311) s(2242) =< aux(311) s(2243) =< aux(311) s(2238) =< aux(312) s(2239) =< aux(312) s(2240) =< aux(312) s(2241) =< aux(312) s(2242) =< aux(312) s(2243) =< aux(312) s(2241) =< aux(332) s(2242) =< aux(332) s(2243) =< aux(332) s(2241) =< aux(334) s(2242) =< aux(334) s(2243) =< aux(334) s(2239) =< aux(331) s(2240) =< aux(331) s(2242) =< aux(331) s(2243) =< aux(331) s(2240) =< aux(337) s(2241) =< aux(337) s(2242) =< aux(337) s(2243) =< aux(337) s(2240) =< aux(323) s(2241) =< aux(323) s(2242) =< aux(323) s(2243) =< aux(323) s(2253) =< aux(326) s(2254) =< aux(326) s(2255) =< aux(326) s(2256) =< aux(326) s(2257) =< aux(326) s(2258) =< aux(326) s(2259) =< aux(326) s(2253) =< aux(327) s(2254) =< aux(327) s(2255) =< aux(327) s(2256) =< aux(327) s(2257) =< aux(327) s(2258) =< aux(327) s(2259) =< aux(327) s(2259) =< aux(317) s(2254) =< aux(318) s(2255) =< aux(318) s(2256) =< aux(318) s(2257) =< aux(318) s(2258) =< aux(318) s(2259) =< aux(318) s(2253) =< aux(320) s(2254) =< aux(320) s(2255) =< aux(320) s(2256) =< aux(320) s(2257) =< aux(320) s(2258) =< aux(320) s(2259) =< aux(320) s(2253) =< aux(309) s(2254) =< aux(309) s(2255) =< aux(309) s(2256) =< aux(309) s(2257) =< aux(309) s(2258) =< aux(309) s(2259) =< aux(309) s(2254) =< aux(310) s(2255) =< aux(310) s(2256) =< aux(310) s(2257) =< aux(310) s(2258) =< aux(310) s(2259) =< aux(310) s(2257) =< aux(332) s(2258) =< aux(332) s(2259) =< aux(332) s(2257) =< aux(333) s(2258) =< aux(333) s(2259) =< aux(333) s(2255) =< aux(331) s(2256) =< aux(331) s(2258) =< aux(331) s(2259) =< aux(331) s(2256) =< aux(337) s(2257) =< aux(337) s(2258) =< aux(337) s(2259) =< aux(337) s(2256) =< aux(322) s(2257) =< aux(322) s(2258) =< aux(322) s(2259) =< aux(322) s(2269) =< aux(326) s(2270) =< aux(326) s(2271) =< aux(326) s(2272) =< aux(326) s(2273) =< aux(326) s(2274) =< aux(326) s(2275) =< aux(326) s(2269) =< aux(330) s(2270) =< aux(330) s(2271) =< aux(330) s(2272) =< aux(330) s(2273) =< aux(330) s(2274) =< aux(330) s(2275) =< aux(330) s(2275) =< aux(317) s(2270) =< aux(318) s(2271) =< aux(318) s(2272) =< aux(318) s(2273) =< aux(318) s(2274) =< aux(318) s(2275) =< aux(318) s(2269) =< aux(320) s(2270) =< aux(320) s(2271) =< aux(320) s(2272) =< aux(320) s(2273) =< aux(320) s(2274) =< aux(320) s(2275) =< aux(320) s(2269) =< aux(315) s(2270) =< aux(315) s(2271) =< aux(315) s(2272) =< aux(315) s(2273) =< aux(315) s(2274) =< aux(315) s(2275) =< aux(315) s(2270) =< aux(316) s(2271) =< aux(316) s(2272) =< aux(316) s(2273) =< aux(316) s(2274) =< aux(316) s(2275) =< aux(316) s(2273) =< aux(332) s(2274) =< aux(332) s(2275) =< aux(332) s(2273) =< aux(336) s(2274) =< aux(336) s(2275) =< aux(336) s(2271) =< aux(331) s(2272) =< aux(331) s(2274) =< aux(331) s(2275) =< aux(331) s(2272) =< aux(337) s(2273) =< aux(337) s(2274) =< aux(337) s(2275) =< aux(337) s(2272) =< aux(325) s(2273) =< aux(325) s(2274) =< aux(325) s(2275) =< aux(325) s(2285) =< aux(326) s(2286) =< aux(326) s(2287) =< aux(326) s(2288) =< aux(326) s(2289) =< aux(326) s(2290) =< aux(326) s(2291) =< aux(326) s(2285) =< aux(329) s(2286) =< aux(329) s(2287) =< aux(329) s(2288) =< aux(329) s(2289) =< aux(329) s(2290) =< aux(329) s(2291) =< aux(329) s(2291) =< aux(317) s(2286) =< aux(318) s(2287) =< aux(318) s(2288) =< aux(318) s(2289) =< aux(318) s(2290) =< aux(318) s(2291) =< aux(318) s(2285) =< aux(320) s(2286) =< aux(320) s(2287) =< aux(320) s(2288) =< aux(320) s(2289) =< aux(320) s(2290) =< aux(320) s(2291) =< aux(320) s(2285) =< aux(313) s(2286) =< aux(313) s(2287) =< aux(313) s(2288) =< aux(313) s(2289) =< aux(313) s(2290) =< aux(313) s(2291) =< aux(313) s(2286) =< aux(314) s(2287) =< aux(314) s(2288) =< aux(314) s(2289) =< aux(314) s(2290) =< aux(314) s(2291) =< aux(314) s(2289) =< aux(332) s(2290) =< aux(332) s(2291) =< aux(332) s(2289) =< aux(335) s(2290) =< aux(335) s(2291) =< aux(335) s(2287) =< aux(331) s(2288) =< aux(331) s(2290) =< aux(331) s(2291) =< aux(331) s(2288) =< aux(337) s(2289) =< aux(337) s(2290) =< aux(337) s(2291) =< aux(337) s(2288) =< aux(324) s(2289) =< aux(324) s(2290) =< aux(324) s(2291) =< aux(324) s(2301) =< aux(326) s(2302) =< aux(326) s(2303) =< aux(326) s(2304) =< aux(326) s(2305) =< aux(326) s(2306) =< aux(326) s(2307) =< aux(326) s(2307) =< aux(317) s(2302) =< aux(318) s(2303) =< aux(318) s(2304) =< aux(318) s(2305) =< aux(318) s(2306) =< aux(318) s(2307) =< aux(318) s(2301) =< aux(320) s(2302) =< aux(320) s(2303) =< aux(320) s(2304) =< aux(320) s(2305) =< aux(320) s(2306) =< aux(320) s(2307) =< aux(320) s(2301) =< aux(307) s(2302) =< aux(307) s(2303) =< aux(307) s(2304) =< aux(307) s(2305) =< aux(307) s(2306) =< aux(307) s(2307) =< aux(307) s(2305) =< aux(332) s(2306) =< aux(332) s(2307) =< aux(332) s(2303) =< aux(331) s(2304) =< aux(331) s(2306) =< aux(331) s(2307) =< aux(331) s(2304) =< aux(337) s(2305) =< aux(337) s(2306) =< aux(337) s(2307) =< aux(337) s(2304) =< aux(321) s(2305) =< aux(321) s(2306) =< aux(321) s(2307) =< aux(321) s(2315) =< aux(326) s(2316) =< aux(326) s(2317) =< aux(326) s(2318) =< aux(326) s(2318) =< aux(317) s(2315) =< aux(318) s(2316) =< aux(318) s(2317) =< aux(318) s(2318) =< aux(318) s(2315) =< aux(320) s(2316) =< aux(320) s(2317) =< aux(320) s(2318) =< aux(320) s(2315) =< aux(307) s(2316) =< aux(307) s(2317) =< aux(307) s(2318) =< aux(307) s(2316) =< aux(332) s(2317) =< aux(332) s(2318) =< aux(332) s(2315) =< aux(331) s(2317) =< aux(331) s(2318) =< aux(331) s(2315) =< aux(337) s(2316) =< aux(337) s(2317) =< aux(337) s(2318) =< aux(337) with precondition: [V=1] * Chain [89]: 1 with precondition: [V=2,V5>=0,V9>=0] Closed-form bounds of start(V,V5,V9): ------------------------------------- * Chain [91] with precondition: [V>=0] - Upper bound: 19376/3*V+112674/65 - Complexity: n * Chain [90] with precondition: [V=1] - Upper bound: nat(V5)*252+9+nat(3/2*V5)*1824+nat(4/3*V5)*1824+nat(13/4*V5)*48+nat(V5+1)*60+nat(V5+14)*48+nat(V5+18)*48+nat(V5+22)*48+nat(V5+26)*48+nat(V5+2/5)*1824+nat(V5+36/13)*1824+nat(13/4*V5+3)*48+nat(13/4*V5+5)*48+nat(V5/2+7)*48+nat(V5/2)*19344 - Complexity: n * Chain [89] with precondition: [V=2,V5>=0,V9>=0] - Upper bound: 1 - Complexity: constant ### Maximum cost of start(V,V5,V9): max([19376/3*V+112609/65,nat(V5)*252+8+nat(3/2*V5)*1824+nat(4/3*V5)*1824+nat(13/4*V5)*48+nat(V5+1)*60+nat(V5+14)*48+nat(V5+18)*48+nat(V5+22)*48+nat(V5+26)*48+nat(V5+2/5)*1824+nat(V5+36/13)*1824+nat(13/4*V5+3)*48+nat(13/4*V5+5)*48+nat(V5/2+7)*48+nat(V5/2)*19344])+1 Asymptotic class: n * Total analysis performed in 47029 ms. ---------------------------------------- (12) BOUNDS(1, n^1) ---------------------------------------- (13) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (14) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: HALF(0') -> c HALF(s(0')) -> c1 HALF(s(s(z0))) -> c2(HALF(z0)) LASTBIT(0') -> c3 LASTBIT(s(0')) -> c4 LASTBIT(s(s(z0))) -> c5(LASTBIT(z0)) ZERO(0') -> c6 ZERO(s(z0)) -> c7 CONV(z0) -> c8(CONVITER(z0, cons(0', nil))) CONVITER(z0, z1) -> c9(IF(zero(z0), z0, z1), ZERO(z0)) IF(true, z0, z1) -> c10 IF(false, z0, z1) -> c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0)) IF(false, z0, z1) -> c12(CONVITER(half(z0), cons(lastbit(z0), z1)), LASTBIT(z0)) The (relative) TRS S consists of the following rules: half(0') -> 0' half(s(0')) -> 0' half(s(s(z0))) -> s(half(z0)) lastbit(0') -> 0' lastbit(s(0')) -> s(0') lastbit(s(s(z0))) -> lastbit(z0) zero(0') -> true zero(s(z0)) -> false conv(z0) -> conviter(z0, cons(0', nil)) conviter(z0, z1) -> if(zero(z0), z0, z1) if(true, z0, z1) -> z1 if(false, z0, z1) -> conviter(half(z0), cons(lastbit(z0), z1)) Rewrite Strategy: INNERMOST ---------------------------------------- (15) SlicingProof (LOWER BOUND(ID)) Sliced the following arguments: cons/1 IF/2 ---------------------------------------- (16) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: HALF(0') -> c HALF(s(0')) -> c1 HALF(s(s(z0))) -> c2(HALF(z0)) LASTBIT(0') -> c3 LASTBIT(s(0')) -> c4 LASTBIT(s(s(z0))) -> c5(LASTBIT(z0)) ZERO(0') -> c6 ZERO(s(z0)) -> c7 CONV(z0) -> c8(CONVITER(z0, cons(0'))) CONVITER(z0, z1) -> c9(IF(zero(z0), z0), ZERO(z0)) IF(true, z0) -> c10 IF(false, z0) -> c11(CONVITER(half(z0), cons(lastbit(z0))), HALF(z0)) IF(false, z0) -> c12(CONVITER(half(z0), cons(lastbit(z0))), LASTBIT(z0)) The (relative) TRS S consists of the following rules: half(0') -> 0' half(s(0')) -> 0' half(s(s(z0))) -> s(half(z0)) lastbit(0') -> 0' lastbit(s(0')) -> s(0') lastbit(s(s(z0))) -> lastbit(z0) zero(0') -> true zero(s(z0)) -> false conv(z0) -> conviter(z0, cons(0')) conviter(z0, z1) -> if(zero(z0), z0, z1) if(true, z0, z1) -> z1 if(false, z0, z1) -> conviter(half(z0), cons(lastbit(z0))) Rewrite Strategy: INNERMOST ---------------------------------------- (17) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (18) Obligation: Innermost TRS: Rules: HALF(0') -> c HALF(s(0')) -> c1 HALF(s(s(z0))) -> c2(HALF(z0)) LASTBIT(0') -> c3 LASTBIT(s(0')) -> c4 LASTBIT(s(s(z0))) -> c5(LASTBIT(z0)) ZERO(0') -> c6 ZERO(s(z0)) -> c7 CONV(z0) -> c8(CONVITER(z0, cons(0'))) CONVITER(z0, z1) -> c9(IF(zero(z0), z0), ZERO(z0)) IF(true, z0) -> c10 IF(false, z0) -> c11(CONVITER(half(z0), cons(lastbit(z0))), HALF(z0)) IF(false, z0) -> c12(CONVITER(half(z0), cons(lastbit(z0))), LASTBIT(z0)) half(0') -> 0' half(s(0')) -> 0' half(s(s(z0))) -> s(half(z0)) lastbit(0') -> 0' lastbit(s(0')) -> s(0') lastbit(s(s(z0))) -> lastbit(z0) zero(0') -> true zero(s(z0)) -> false conv(z0) -> conviter(z0, cons(0')) conviter(z0, z1) -> if(zero(z0), z0, z1) if(true, z0, z1) -> z1 if(false, z0, z1) -> conviter(half(z0), cons(lastbit(z0))) Types: HALF :: 0':s -> c:c1:c2 0' :: 0':s c :: c:c1:c2 s :: 0':s -> 0':s c1 :: c:c1:c2 c2 :: c:c1:c2 -> c:c1:c2 LASTBIT :: 0':s -> c3:c4:c5 c3 :: c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 -> c3:c4:c5 ZERO :: 0':s -> c6:c7 c6 :: c6:c7 c7 :: c6:c7 CONV :: 0':s -> c8 c8 :: c9 -> c8 CONVITER :: 0':s -> cons -> c9 cons :: 0':s -> cons c9 :: c10:c11:c12 -> c6:c7 -> c9 IF :: true:false -> 0':s -> c10:c11:c12 zero :: 0':s -> true:false true :: true:false c10 :: c10:c11:c12 false :: true:false c11 :: c9 -> c:c1:c2 -> c10:c11:c12 half :: 0':s -> 0':s lastbit :: 0':s -> 0':s c12 :: c9 -> c3:c4:c5 -> c10:c11:c12 conv :: 0':s -> cons conviter :: 0':s -> cons -> cons if :: true:false -> 0':s -> cons -> cons hole_c:c1:c21_13 :: c:c1:c2 hole_0':s2_13 :: 0':s hole_c3:c4:c53_13 :: c3:c4:c5 hole_c6:c74_13 :: c6:c7 hole_c85_13 :: c8 hole_c96_13 :: c9 hole_cons7_13 :: cons hole_c10:c11:c128_13 :: c10:c11:c12 hole_true:false9_13 :: true:false gen_c:c1:c210_13 :: Nat -> c:c1:c2 gen_0':s11_13 :: Nat -> 0':s gen_c3:c4:c512_13 :: Nat -> c3:c4:c5 ---------------------------------------- (19) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: HALF, LASTBIT, CONVITER, IF, half, lastbit, conviter They will be analysed ascendingly in the following order: HALF < IF LASTBIT < IF CONVITER = IF half < IF lastbit < IF half < conviter lastbit < conviter ---------------------------------------- (20) Obligation: Innermost TRS: Rules: HALF(0') -> c HALF(s(0')) -> c1 HALF(s(s(z0))) -> c2(HALF(z0)) LASTBIT(0') -> c3 LASTBIT(s(0')) -> c4 LASTBIT(s(s(z0))) -> c5(LASTBIT(z0)) ZERO(0') -> c6 ZERO(s(z0)) -> c7 CONV(z0) -> c8(CONVITER(z0, cons(0'))) CONVITER(z0, z1) -> c9(IF(zero(z0), z0), ZERO(z0)) IF(true, z0) -> c10 IF(false, z0) -> c11(CONVITER(half(z0), cons(lastbit(z0))), HALF(z0)) IF(false, z0) -> c12(CONVITER(half(z0), cons(lastbit(z0))), LASTBIT(z0)) half(0') -> 0' half(s(0')) -> 0' half(s(s(z0))) -> s(half(z0)) lastbit(0') -> 0' lastbit(s(0')) -> s(0') lastbit(s(s(z0))) -> lastbit(z0) zero(0') -> true zero(s(z0)) -> false conv(z0) -> conviter(z0, cons(0')) conviter(z0, z1) -> if(zero(z0), z0, z1) if(true, z0, z1) -> z1 if(false, z0, z1) -> conviter(half(z0), cons(lastbit(z0))) Types: HALF :: 0':s -> c:c1:c2 0' :: 0':s c :: c:c1:c2 s :: 0':s -> 0':s c1 :: c:c1:c2 c2 :: c:c1:c2 -> c:c1:c2 LASTBIT :: 0':s -> c3:c4:c5 c3 :: c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 -> c3:c4:c5 ZERO :: 0':s -> c6:c7 c6 :: c6:c7 c7 :: c6:c7 CONV :: 0':s -> c8 c8 :: c9 -> c8 CONVITER :: 0':s -> cons -> c9 cons :: 0':s -> cons c9 :: c10:c11:c12 -> c6:c7 -> c9 IF :: true:false -> 0':s -> c10:c11:c12 zero :: 0':s -> true:false true :: true:false c10 :: c10:c11:c12 false :: true:false c11 :: c9 -> c:c1:c2 -> c10:c11:c12 half :: 0':s -> 0':s lastbit :: 0':s -> 0':s c12 :: c9 -> c3:c4:c5 -> c10:c11:c12 conv :: 0':s -> cons conviter :: 0':s -> cons -> cons if :: true:false -> 0':s -> cons -> cons hole_c:c1:c21_13 :: c:c1:c2 hole_0':s2_13 :: 0':s hole_c3:c4:c53_13 :: c3:c4:c5 hole_c6:c74_13 :: c6:c7 hole_c85_13 :: c8 hole_c96_13 :: c9 hole_cons7_13 :: cons hole_c10:c11:c128_13 :: c10:c11:c12 hole_true:false9_13 :: true:false gen_c:c1:c210_13 :: Nat -> c:c1:c2 gen_0':s11_13 :: Nat -> 0':s gen_c3:c4:c512_13 :: Nat -> c3:c4:c5 Generator Equations: gen_c:c1:c210_13(0) <=> c gen_c:c1:c210_13(+(x, 1)) <=> c2(gen_c:c1:c210_13(x)) gen_0':s11_13(0) <=> 0' gen_0':s11_13(+(x, 1)) <=> s(gen_0':s11_13(x)) gen_c3:c4:c512_13(0) <=> c3 gen_c3:c4:c512_13(+(x, 1)) <=> c5(gen_c3:c4:c512_13(x)) The following defined symbols remain to be analysed: HALF, LASTBIT, CONVITER, IF, half, lastbit, conviter They will be analysed ascendingly in the following order: HALF < IF LASTBIT < IF CONVITER = IF half < IF lastbit < IF half < conviter lastbit < conviter ---------------------------------------- (21) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: HALF(gen_0':s11_13(*(2, n14_13))) -> gen_c:c1:c210_13(n14_13), rt in Omega(1 + n14_13) Induction Base: HALF(gen_0':s11_13(*(2, 0))) ->_R^Omega(1) c Induction Step: HALF(gen_0':s11_13(*(2, +(n14_13, 1)))) ->_R^Omega(1) c2(HALF(gen_0':s11_13(*(2, n14_13)))) ->_IH c2(gen_c:c1:c210_13(c15_13)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (22) Complex Obligation (BEST) ---------------------------------------- (23) Obligation: Proved the lower bound n^1 for the following obligation: Innermost TRS: Rules: HALF(0') -> c HALF(s(0')) -> c1 HALF(s(s(z0))) -> c2(HALF(z0)) LASTBIT(0') -> c3 LASTBIT(s(0')) -> c4 LASTBIT(s(s(z0))) -> c5(LASTBIT(z0)) ZERO(0') -> c6 ZERO(s(z0)) -> c7 CONV(z0) -> c8(CONVITER(z0, cons(0'))) CONVITER(z0, z1) -> c9(IF(zero(z0), z0), ZERO(z0)) IF(true, z0) -> c10 IF(false, z0) -> c11(CONVITER(half(z0), cons(lastbit(z0))), HALF(z0)) IF(false, z0) -> c12(CONVITER(half(z0), cons(lastbit(z0))), LASTBIT(z0)) half(0') -> 0' half(s(0')) -> 0' half(s(s(z0))) -> s(half(z0)) lastbit(0') -> 0' lastbit(s(0')) -> s(0') lastbit(s(s(z0))) -> lastbit(z0) zero(0') -> true zero(s(z0)) -> false conv(z0) -> conviter(z0, cons(0')) conviter(z0, z1) -> if(zero(z0), z0, z1) if(true, z0, z1) -> z1 if(false, z0, z1) -> conviter(half(z0), cons(lastbit(z0))) Types: HALF :: 0':s -> c:c1:c2 0' :: 0':s c :: c:c1:c2 s :: 0':s -> 0':s c1 :: c:c1:c2 c2 :: c:c1:c2 -> c:c1:c2 LASTBIT :: 0':s -> c3:c4:c5 c3 :: c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 -> c3:c4:c5 ZERO :: 0':s -> c6:c7 c6 :: c6:c7 c7 :: c6:c7 CONV :: 0':s -> c8 c8 :: c9 -> c8 CONVITER :: 0':s -> cons -> c9 cons :: 0':s -> cons c9 :: c10:c11:c12 -> c6:c7 -> c9 IF :: true:false -> 0':s -> c10:c11:c12 zero :: 0':s -> true:false true :: true:false c10 :: c10:c11:c12 false :: true:false c11 :: c9 -> c:c1:c2 -> c10:c11:c12 half :: 0':s -> 0':s lastbit :: 0':s -> 0':s c12 :: c9 -> c3:c4:c5 -> c10:c11:c12 conv :: 0':s -> cons conviter :: 0':s -> cons -> cons if :: true:false -> 0':s -> cons -> cons hole_c:c1:c21_13 :: c:c1:c2 hole_0':s2_13 :: 0':s hole_c3:c4:c53_13 :: c3:c4:c5 hole_c6:c74_13 :: c6:c7 hole_c85_13 :: c8 hole_c96_13 :: c9 hole_cons7_13 :: cons hole_c10:c11:c128_13 :: c10:c11:c12 hole_true:false9_13 :: true:false gen_c:c1:c210_13 :: Nat -> c:c1:c2 gen_0':s11_13 :: Nat -> 0':s gen_c3:c4:c512_13 :: Nat -> c3:c4:c5 Generator Equations: gen_c:c1:c210_13(0) <=> c gen_c:c1:c210_13(+(x, 1)) <=> c2(gen_c:c1:c210_13(x)) gen_0':s11_13(0) <=> 0' gen_0':s11_13(+(x, 1)) <=> s(gen_0':s11_13(x)) gen_c3:c4:c512_13(0) <=> c3 gen_c3:c4:c512_13(+(x, 1)) <=> c5(gen_c3:c4:c512_13(x)) The following defined symbols remain to be analysed: HALF, LASTBIT, CONVITER, IF, half, lastbit, conviter They will be analysed ascendingly in the following order: HALF < IF LASTBIT < IF CONVITER = IF half < IF lastbit < IF half < conviter lastbit < conviter ---------------------------------------- (24) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (25) BOUNDS(n^1, INF) ---------------------------------------- (26) Obligation: Innermost TRS: Rules: HALF(0') -> c HALF(s(0')) -> c1 HALF(s(s(z0))) -> c2(HALF(z0)) LASTBIT(0') -> c3 LASTBIT(s(0')) -> c4 LASTBIT(s(s(z0))) -> c5(LASTBIT(z0)) ZERO(0') -> c6 ZERO(s(z0)) -> c7 CONV(z0) -> c8(CONVITER(z0, cons(0'))) CONVITER(z0, z1) -> c9(IF(zero(z0), z0), ZERO(z0)) IF(true, z0) -> c10 IF(false, z0) -> c11(CONVITER(half(z0), cons(lastbit(z0))), HALF(z0)) IF(false, z0) -> c12(CONVITER(half(z0), cons(lastbit(z0))), LASTBIT(z0)) half(0') -> 0' half(s(0')) -> 0' half(s(s(z0))) -> s(half(z0)) lastbit(0') -> 0' lastbit(s(0')) -> s(0') lastbit(s(s(z0))) -> lastbit(z0) zero(0') -> true zero(s(z0)) -> false conv(z0) -> conviter(z0, cons(0')) conviter(z0, z1) -> if(zero(z0), z0, z1) if(true, z0, z1) -> z1 if(false, z0, z1) -> conviter(half(z0), cons(lastbit(z0))) Types: HALF :: 0':s -> c:c1:c2 0' :: 0':s c :: c:c1:c2 s :: 0':s -> 0':s c1 :: c:c1:c2 c2 :: c:c1:c2 -> c:c1:c2 LASTBIT :: 0':s -> c3:c4:c5 c3 :: c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 -> c3:c4:c5 ZERO :: 0':s -> c6:c7 c6 :: c6:c7 c7 :: c6:c7 CONV :: 0':s -> c8 c8 :: c9 -> c8 CONVITER :: 0':s -> cons -> c9 cons :: 0':s -> cons c9 :: c10:c11:c12 -> c6:c7 -> c9 IF :: true:false -> 0':s -> c10:c11:c12 zero :: 0':s -> true:false true :: true:false c10 :: c10:c11:c12 false :: true:false c11 :: c9 -> c:c1:c2 -> c10:c11:c12 half :: 0':s -> 0':s lastbit :: 0':s -> 0':s c12 :: c9 -> c3:c4:c5 -> c10:c11:c12 conv :: 0':s -> cons conviter :: 0':s -> cons -> cons if :: true:false -> 0':s -> cons -> cons hole_c:c1:c21_13 :: c:c1:c2 hole_0':s2_13 :: 0':s hole_c3:c4:c53_13 :: c3:c4:c5 hole_c6:c74_13 :: c6:c7 hole_c85_13 :: c8 hole_c96_13 :: c9 hole_cons7_13 :: cons hole_c10:c11:c128_13 :: c10:c11:c12 hole_true:false9_13 :: true:false gen_c:c1:c210_13 :: Nat -> c:c1:c2 gen_0':s11_13 :: Nat -> 0':s gen_c3:c4:c512_13 :: Nat -> c3:c4:c5 Lemmas: HALF(gen_0':s11_13(*(2, n14_13))) -> gen_c:c1:c210_13(n14_13), rt in Omega(1 + n14_13) Generator Equations: gen_c:c1:c210_13(0) <=> c gen_c:c1:c210_13(+(x, 1)) <=> c2(gen_c:c1:c210_13(x)) gen_0':s11_13(0) <=> 0' gen_0':s11_13(+(x, 1)) <=> s(gen_0':s11_13(x)) gen_c3:c4:c512_13(0) <=> c3 gen_c3:c4:c512_13(+(x, 1)) <=> c5(gen_c3:c4:c512_13(x)) The following defined symbols remain to be analysed: LASTBIT, CONVITER, IF, half, lastbit, conviter They will be analysed ascendingly in the following order: LASTBIT < IF CONVITER = IF half < IF lastbit < IF half < conviter lastbit < conviter ---------------------------------------- (27) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: LASTBIT(gen_0':s11_13(*(2, n448_13))) -> gen_c3:c4:c512_13(n448_13), rt in Omega(1 + n448_13) Induction Base: LASTBIT(gen_0':s11_13(*(2, 0))) ->_R^Omega(1) c3 Induction Step: LASTBIT(gen_0':s11_13(*(2, +(n448_13, 1)))) ->_R^Omega(1) c5(LASTBIT(gen_0':s11_13(*(2, n448_13)))) ->_IH c5(gen_c3:c4:c512_13(c449_13)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (28) Obligation: Innermost TRS: Rules: HALF(0') -> c HALF(s(0')) -> c1 HALF(s(s(z0))) -> c2(HALF(z0)) LASTBIT(0') -> c3 LASTBIT(s(0')) -> c4 LASTBIT(s(s(z0))) -> c5(LASTBIT(z0)) ZERO(0') -> c6 ZERO(s(z0)) -> c7 CONV(z0) -> c8(CONVITER(z0, cons(0'))) CONVITER(z0, z1) -> c9(IF(zero(z0), z0), ZERO(z0)) IF(true, z0) -> c10 IF(false, z0) -> c11(CONVITER(half(z0), cons(lastbit(z0))), HALF(z0)) IF(false, z0) -> c12(CONVITER(half(z0), cons(lastbit(z0))), LASTBIT(z0)) half(0') -> 0' half(s(0')) -> 0' half(s(s(z0))) -> s(half(z0)) lastbit(0') -> 0' lastbit(s(0')) -> s(0') lastbit(s(s(z0))) -> lastbit(z0) zero(0') -> true zero(s(z0)) -> false conv(z0) -> conviter(z0, cons(0')) conviter(z0, z1) -> if(zero(z0), z0, z1) if(true, z0, z1) -> z1 if(false, z0, z1) -> conviter(half(z0), cons(lastbit(z0))) Types: HALF :: 0':s -> c:c1:c2 0' :: 0':s c :: c:c1:c2 s :: 0':s -> 0':s c1 :: c:c1:c2 c2 :: c:c1:c2 -> c:c1:c2 LASTBIT :: 0':s -> c3:c4:c5 c3 :: c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 -> c3:c4:c5 ZERO :: 0':s -> c6:c7 c6 :: c6:c7 c7 :: c6:c7 CONV :: 0':s -> c8 c8 :: c9 -> c8 CONVITER :: 0':s -> cons -> c9 cons :: 0':s -> cons c9 :: c10:c11:c12 -> c6:c7 -> c9 IF :: true:false -> 0':s -> c10:c11:c12 zero :: 0':s -> true:false true :: true:false c10 :: c10:c11:c12 false :: true:false c11 :: c9 -> c:c1:c2 -> c10:c11:c12 half :: 0':s -> 0':s lastbit :: 0':s -> 0':s c12 :: c9 -> c3:c4:c5 -> c10:c11:c12 conv :: 0':s -> cons conviter :: 0':s -> cons -> cons if :: true:false -> 0':s -> cons -> cons hole_c:c1:c21_13 :: c:c1:c2 hole_0':s2_13 :: 0':s hole_c3:c4:c53_13 :: c3:c4:c5 hole_c6:c74_13 :: c6:c7 hole_c85_13 :: c8 hole_c96_13 :: c9 hole_cons7_13 :: cons hole_c10:c11:c128_13 :: c10:c11:c12 hole_true:false9_13 :: true:false gen_c:c1:c210_13 :: Nat -> c:c1:c2 gen_0':s11_13 :: Nat -> 0':s gen_c3:c4:c512_13 :: Nat -> c3:c4:c5 Lemmas: HALF(gen_0':s11_13(*(2, n14_13))) -> gen_c:c1:c210_13(n14_13), rt in Omega(1 + n14_13) LASTBIT(gen_0':s11_13(*(2, n448_13))) -> gen_c3:c4:c512_13(n448_13), rt in Omega(1 + n448_13) Generator Equations: gen_c:c1:c210_13(0) <=> c gen_c:c1:c210_13(+(x, 1)) <=> c2(gen_c:c1:c210_13(x)) gen_0':s11_13(0) <=> 0' gen_0':s11_13(+(x, 1)) <=> s(gen_0':s11_13(x)) gen_c3:c4:c512_13(0) <=> c3 gen_c3:c4:c512_13(+(x, 1)) <=> c5(gen_c3:c4:c512_13(x)) The following defined symbols remain to be analysed: half, CONVITER, IF, lastbit, conviter They will be analysed ascendingly in the following order: CONVITER = IF half < IF lastbit < IF half < conviter lastbit < conviter ---------------------------------------- (29) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: half(gen_0':s11_13(*(2, n954_13))) -> gen_0':s11_13(n954_13), rt in Omega(0) Induction Base: half(gen_0':s11_13(*(2, 0))) ->_R^Omega(0) 0' Induction Step: half(gen_0':s11_13(*(2, +(n954_13, 1)))) ->_R^Omega(0) s(half(gen_0':s11_13(*(2, n954_13)))) ->_IH s(gen_0':s11_13(c955_13)) We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (30) Obligation: Innermost TRS: Rules: HALF(0') -> c HALF(s(0')) -> c1 HALF(s(s(z0))) -> c2(HALF(z0)) LASTBIT(0') -> c3 LASTBIT(s(0')) -> c4 LASTBIT(s(s(z0))) -> c5(LASTBIT(z0)) ZERO(0') -> c6 ZERO(s(z0)) -> c7 CONV(z0) -> c8(CONVITER(z0, cons(0'))) CONVITER(z0, z1) -> c9(IF(zero(z0), z0), ZERO(z0)) IF(true, z0) -> c10 IF(false, z0) -> c11(CONVITER(half(z0), cons(lastbit(z0))), HALF(z0)) IF(false, z0) -> c12(CONVITER(half(z0), cons(lastbit(z0))), LASTBIT(z0)) half(0') -> 0' half(s(0')) -> 0' half(s(s(z0))) -> s(half(z0)) lastbit(0') -> 0' lastbit(s(0')) -> s(0') lastbit(s(s(z0))) -> lastbit(z0) zero(0') -> true zero(s(z0)) -> false conv(z0) -> conviter(z0, cons(0')) conviter(z0, z1) -> if(zero(z0), z0, z1) if(true, z0, z1) -> z1 if(false, z0, z1) -> conviter(half(z0), cons(lastbit(z0))) Types: HALF :: 0':s -> c:c1:c2 0' :: 0':s c :: c:c1:c2 s :: 0':s -> 0':s c1 :: c:c1:c2 c2 :: c:c1:c2 -> c:c1:c2 LASTBIT :: 0':s -> c3:c4:c5 c3 :: c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 -> c3:c4:c5 ZERO :: 0':s -> c6:c7 c6 :: c6:c7 c7 :: c6:c7 CONV :: 0':s -> c8 c8 :: c9 -> c8 CONVITER :: 0':s -> cons -> c9 cons :: 0':s -> cons c9 :: c10:c11:c12 -> c6:c7 -> c9 IF :: true:false -> 0':s -> c10:c11:c12 zero :: 0':s -> true:false true :: true:false c10 :: c10:c11:c12 false :: true:false c11 :: c9 -> c:c1:c2 -> c10:c11:c12 half :: 0':s -> 0':s lastbit :: 0':s -> 0':s c12 :: c9 -> c3:c4:c5 -> c10:c11:c12 conv :: 0':s -> cons conviter :: 0':s -> cons -> cons if :: true:false -> 0':s -> cons -> cons hole_c:c1:c21_13 :: c:c1:c2 hole_0':s2_13 :: 0':s hole_c3:c4:c53_13 :: c3:c4:c5 hole_c6:c74_13 :: c6:c7 hole_c85_13 :: c8 hole_c96_13 :: c9 hole_cons7_13 :: cons hole_c10:c11:c128_13 :: c10:c11:c12 hole_true:false9_13 :: true:false gen_c:c1:c210_13 :: Nat -> c:c1:c2 gen_0':s11_13 :: Nat -> 0':s gen_c3:c4:c512_13 :: Nat -> c3:c4:c5 Lemmas: HALF(gen_0':s11_13(*(2, n14_13))) -> gen_c:c1:c210_13(n14_13), rt in Omega(1 + n14_13) LASTBIT(gen_0':s11_13(*(2, n448_13))) -> gen_c3:c4:c512_13(n448_13), rt in Omega(1 + n448_13) half(gen_0':s11_13(*(2, n954_13))) -> gen_0':s11_13(n954_13), rt in Omega(0) Generator Equations: gen_c:c1:c210_13(0) <=> c gen_c:c1:c210_13(+(x, 1)) <=> c2(gen_c:c1:c210_13(x)) gen_0':s11_13(0) <=> 0' gen_0':s11_13(+(x, 1)) <=> s(gen_0':s11_13(x)) gen_c3:c4:c512_13(0) <=> c3 gen_c3:c4:c512_13(+(x, 1)) <=> c5(gen_c3:c4:c512_13(x)) The following defined symbols remain to be analysed: lastbit, CONVITER, IF, conviter They will be analysed ascendingly in the following order: CONVITER = IF lastbit < IF lastbit < conviter ---------------------------------------- (31) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: lastbit(gen_0':s11_13(*(2, n1406_13))) -> gen_0':s11_13(0), rt in Omega(0) Induction Base: lastbit(gen_0':s11_13(*(2, 0))) ->_R^Omega(0) 0' Induction Step: lastbit(gen_0':s11_13(*(2, +(n1406_13, 1)))) ->_R^Omega(0) lastbit(gen_0':s11_13(*(2, n1406_13))) ->_IH gen_0':s11_13(0) We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (32) Obligation: Innermost TRS: Rules: HALF(0') -> c HALF(s(0')) -> c1 HALF(s(s(z0))) -> c2(HALF(z0)) LASTBIT(0') -> c3 LASTBIT(s(0')) -> c4 LASTBIT(s(s(z0))) -> c5(LASTBIT(z0)) ZERO(0') -> c6 ZERO(s(z0)) -> c7 CONV(z0) -> c8(CONVITER(z0, cons(0'))) CONVITER(z0, z1) -> c9(IF(zero(z0), z0), ZERO(z0)) IF(true, z0) -> c10 IF(false, z0) -> c11(CONVITER(half(z0), cons(lastbit(z0))), HALF(z0)) IF(false, z0) -> c12(CONVITER(half(z0), cons(lastbit(z0))), LASTBIT(z0)) half(0') -> 0' half(s(0')) -> 0' half(s(s(z0))) -> s(half(z0)) lastbit(0') -> 0' lastbit(s(0')) -> s(0') lastbit(s(s(z0))) -> lastbit(z0) zero(0') -> true zero(s(z0)) -> false conv(z0) -> conviter(z0, cons(0')) conviter(z0, z1) -> if(zero(z0), z0, z1) if(true, z0, z1) -> z1 if(false, z0, z1) -> conviter(half(z0), cons(lastbit(z0))) Types: HALF :: 0':s -> c:c1:c2 0' :: 0':s c :: c:c1:c2 s :: 0':s -> 0':s c1 :: c:c1:c2 c2 :: c:c1:c2 -> c:c1:c2 LASTBIT :: 0':s -> c3:c4:c5 c3 :: c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 -> c3:c4:c5 ZERO :: 0':s -> c6:c7 c6 :: c6:c7 c7 :: c6:c7 CONV :: 0':s -> c8 c8 :: c9 -> c8 CONVITER :: 0':s -> cons -> c9 cons :: 0':s -> cons c9 :: c10:c11:c12 -> c6:c7 -> c9 IF :: true:false -> 0':s -> c10:c11:c12 zero :: 0':s -> true:false true :: true:false c10 :: c10:c11:c12 false :: true:false c11 :: c9 -> c:c1:c2 -> c10:c11:c12 half :: 0':s -> 0':s lastbit :: 0':s -> 0':s c12 :: c9 -> c3:c4:c5 -> c10:c11:c12 conv :: 0':s -> cons conviter :: 0':s -> cons -> cons if :: true:false -> 0':s -> cons -> cons hole_c:c1:c21_13 :: c:c1:c2 hole_0':s2_13 :: 0':s hole_c3:c4:c53_13 :: c3:c4:c5 hole_c6:c74_13 :: c6:c7 hole_c85_13 :: c8 hole_c96_13 :: c9 hole_cons7_13 :: cons hole_c10:c11:c128_13 :: c10:c11:c12 hole_true:false9_13 :: true:false gen_c:c1:c210_13 :: Nat -> c:c1:c2 gen_0':s11_13 :: Nat -> 0':s gen_c3:c4:c512_13 :: Nat -> c3:c4:c5 Lemmas: HALF(gen_0':s11_13(*(2, n14_13))) -> gen_c:c1:c210_13(n14_13), rt in Omega(1 + n14_13) LASTBIT(gen_0':s11_13(*(2, n448_13))) -> gen_c3:c4:c512_13(n448_13), rt in Omega(1 + n448_13) half(gen_0':s11_13(*(2, n954_13))) -> gen_0':s11_13(n954_13), rt in Omega(0) lastbit(gen_0':s11_13(*(2, n1406_13))) -> gen_0':s11_13(0), rt in Omega(0) Generator Equations: gen_c:c1:c210_13(0) <=> c gen_c:c1:c210_13(+(x, 1)) <=> c2(gen_c:c1:c210_13(x)) gen_0':s11_13(0) <=> 0' gen_0':s11_13(+(x, 1)) <=> s(gen_0':s11_13(x)) gen_c3:c4:c512_13(0) <=> c3 gen_c3:c4:c512_13(+(x, 1)) <=> c5(gen_c3:c4:c512_13(x)) The following defined symbols remain to be analysed: conviter, CONVITER, IF They will be analysed ascendingly in the following order: CONVITER = IF