WORST_CASE(Omega(n^1),O(n^2)) proof of /export/starexec/sandbox2/benchmark/theBenchmark.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 704 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, 18.3 s] (12) BOUNDS(1, n^2) (13) RenamingProof [BOTH BOUNDS(ID, ID), 3 ms] (14) CpxRelTRS (15) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (16) typed CpxTrs (17) OrderProof [LOWER BOUND(ID), 0 ms] (18) typed CpxTrs (19) RewriteLemmaProof [LOWER BOUND(ID), 226 ms] (20) typed CpxTrs (21) RewriteLemmaProof [LOWER BOUND(ID), 110 ms] (22) BEST (23) proven lower bound (24) LowerBoundPropagationProof [FINISHED, 0 ms] (25) BOUNDS(n^1, INF) (26) typed CpxTrs ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2). The TRS R consists of the following rules: COND(true, z0) -> c(COND(and(even(z0), gr(z0, 0)), p(z0)), AND(even(z0), gr(z0, 0)), EVEN(z0)) COND(true, z0) -> c1(COND(and(even(z0), gr(z0, 0)), p(z0)), AND(even(z0), gr(z0, 0)), GR(z0, 0)) COND(true, z0) -> c2(COND(and(even(z0), gr(z0, 0)), p(z0)), P(z0)) AND(z0, false) -> c3 AND(false, z0) -> c4 AND(true, true) -> c5 EVEN(0) -> c6 EVEN(s(0)) -> c7 EVEN(s(s(z0))) -> c8(EVEN(z0)) GR(0, z0) -> c9 GR(s(z0), 0) -> c10 GR(s(z0), s(y)) -> c11(GR(z0, y)) P(0) -> c12 P(s(z0)) -> c13 The (relative) TRS S consists of the following rules: cond(true, z0) -> cond(and(even(z0), gr(z0, 0)), p(z0)) and(z0, false) -> false and(false, z0) -> false and(true, true) -> true even(0) -> true even(s(0)) -> false even(s(s(z0))) -> even(z0) gr(0, z0) -> false gr(s(z0), 0) -> true gr(s(z0), s(y)) -> gr(z0, y) p(0) -> 0 p(s(z0)) -> z0 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^2). The TRS R consists of the following rules: COND(true, z0) -> c(COND(and(even(z0), gr(z0, 0)), p(z0)), AND(even(z0), gr(z0, 0)), EVEN(z0)) COND(true, z0) -> c1(COND(and(even(z0), gr(z0, 0)), p(z0)), AND(even(z0), gr(z0, 0)), GR(z0, 0)) COND(true, z0) -> c2(COND(and(even(z0), gr(z0, 0)), p(z0)), P(z0)) AND(z0, false) -> c3 AND(false, z0) -> c4 AND(true, true) -> c5 EVEN(0) -> c6 EVEN(s(0)) -> c7 EVEN(s(s(z0))) -> c8(EVEN(z0)) GR(0, z0) -> c9 GR(s(z0), 0) -> c10 GR(s(z0), s(y)) -> c11(GR(z0, y)) P(0) -> c12 P(s(z0)) -> c13 The (relative) TRS S consists of the following rules: cond(true, z0) -> cond(and(even(z0), gr(z0, 0)), p(z0)) and(z0, false) -> false and(false, z0) -> false and(true, true) -> true even(0) -> true even(s(0)) -> false even(s(s(z0))) -> even(z0) gr(0, z0) -> false gr(s(z0), 0) -> true gr(s(z0), s(y)) -> gr(z0, y) p(0) -> 0 p(s(z0)) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (3) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID)) Transformed relative TRS to weighted TRS ---------------------------------------- (4) Obligation: The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^2). The TRS R consists of the following rules: COND(true, z0) -> c(COND(and(even(z0), gr(z0, 0)), p(z0)), AND(even(z0), gr(z0, 0)), EVEN(z0)) [1] COND(true, z0) -> c1(COND(and(even(z0), gr(z0, 0)), p(z0)), AND(even(z0), gr(z0, 0)), GR(z0, 0)) [1] COND(true, z0) -> c2(COND(and(even(z0), gr(z0, 0)), p(z0)), P(z0)) [1] AND(z0, false) -> c3 [1] AND(false, z0) -> c4 [1] AND(true, true) -> c5 [1] EVEN(0) -> c6 [1] EVEN(s(0)) -> c7 [1] EVEN(s(s(z0))) -> c8(EVEN(z0)) [1] GR(0, z0) -> c9 [1] GR(s(z0), 0) -> c10 [1] GR(s(z0), s(y)) -> c11(GR(z0, y)) [1] P(0) -> c12 [1] P(s(z0)) -> c13 [1] cond(true, z0) -> cond(and(even(z0), gr(z0, 0)), p(z0)) [0] and(z0, false) -> false [0] and(false, z0) -> false [0] and(true, true) -> true [0] even(0) -> true [0] even(s(0)) -> false [0] even(s(s(z0))) -> even(z0) [0] gr(0, z0) -> false [0] gr(s(z0), 0) -> true [0] gr(s(z0), s(y)) -> gr(z0, y) [0] p(0) -> 0 [0] p(s(z0)) -> z0 [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: COND(true, z0) -> c(COND(and(even(z0), gr(z0, 0)), p(z0)), AND(even(z0), gr(z0, 0)), EVEN(z0)) [1] COND(true, z0) -> c1(COND(and(even(z0), gr(z0, 0)), p(z0)), AND(even(z0), gr(z0, 0)), GR(z0, 0)) [1] COND(true, z0) -> c2(COND(and(even(z0), gr(z0, 0)), p(z0)), P(z0)) [1] AND(z0, false) -> c3 [1] AND(false, z0) -> c4 [1] AND(true, true) -> c5 [1] EVEN(0) -> c6 [1] EVEN(s(0)) -> c7 [1] EVEN(s(s(z0))) -> c8(EVEN(z0)) [1] GR(0, z0) -> c9 [1] GR(s(z0), 0) -> c10 [1] GR(s(z0), s(y)) -> c11(GR(z0, y)) [1] P(0) -> c12 [1] P(s(z0)) -> c13 [1] cond(true, z0) -> cond(and(even(z0), gr(z0, 0)), p(z0)) [0] and(z0, false) -> false [0] and(false, z0) -> false [0] and(true, true) -> true [0] even(0) -> true [0] even(s(0)) -> false [0] even(s(s(z0))) -> even(z0) [0] gr(0, z0) -> false [0] gr(s(z0), 0) -> true [0] gr(s(z0), s(y)) -> gr(z0, y) [0] p(0) -> 0 [0] p(s(z0)) -> z0 [0] The TRS has the following type information: COND :: true:false -> 0:s:y -> c:c1:c2 true :: true:false c :: c:c1:c2 -> c3:c4:c5 -> c6:c7:c8 -> c:c1:c2 and :: true:false -> true:false -> true:false even :: 0:s:y -> true:false gr :: 0:s:y -> 0:s:y -> true:false 0 :: 0:s:y p :: 0:s:y -> 0:s:y AND :: true:false -> true:false -> c3:c4:c5 EVEN :: 0:s:y -> c6:c7:c8 c1 :: c:c1:c2 -> c3:c4:c5 -> c9:c10:c11 -> c:c1:c2 GR :: 0:s:y -> 0:s:y -> c9:c10:c11 c2 :: c:c1:c2 -> c12:c13 -> c:c1:c2 P :: 0:s:y -> c12:c13 false :: true:false c3 :: c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 c6 :: c6:c7:c8 s :: 0:s:y -> 0:s:y c7 :: c6:c7:c8 c8 :: c6:c7:c8 -> c6:c7:c8 c9 :: c9:c10:c11 c10 :: c9:c10:c11 y :: 0:s:y c11 :: c9:c10:c11 -> c9:c10:c11 c12 :: c12:c13 c13 :: c12:c13 cond :: true:false -> 0:s:y -> cond 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: cond(v0, v1) -> null_cond [0] and(v0, v1) -> null_and [0] even(v0) -> null_even [0] gr(v0, v1) -> null_gr [0] p(v0) -> null_p [0] COND(v0, v1) -> null_COND [0] AND(v0, v1) -> null_AND [0] EVEN(v0) -> null_EVEN [0] GR(v0, v1) -> null_GR [0] P(v0) -> null_P [0] And the following fresh constants: null_cond, null_and, null_even, null_gr, null_p, null_COND, null_AND, null_EVEN, null_GR, null_P ---------------------------------------- (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: COND(true, z0) -> c(COND(and(even(z0), gr(z0, 0)), p(z0)), AND(even(z0), gr(z0, 0)), EVEN(z0)) [1] COND(true, z0) -> c1(COND(and(even(z0), gr(z0, 0)), p(z0)), AND(even(z0), gr(z0, 0)), GR(z0, 0)) [1] COND(true, z0) -> c2(COND(and(even(z0), gr(z0, 0)), p(z0)), P(z0)) [1] AND(z0, false) -> c3 [1] AND(false, z0) -> c4 [1] AND(true, true) -> c5 [1] EVEN(0) -> c6 [1] EVEN(s(0)) -> c7 [1] EVEN(s(s(z0))) -> c8(EVEN(z0)) [1] GR(0, z0) -> c9 [1] GR(s(z0), 0) -> c10 [1] GR(s(z0), s(y)) -> c11(GR(z0, y)) [1] P(0) -> c12 [1] P(s(z0)) -> c13 [1] cond(true, z0) -> cond(and(even(z0), gr(z0, 0)), p(z0)) [0] and(z0, false) -> false [0] and(false, z0) -> false [0] and(true, true) -> true [0] even(0) -> true [0] even(s(0)) -> false [0] even(s(s(z0))) -> even(z0) [0] gr(0, z0) -> false [0] gr(s(z0), 0) -> true [0] gr(s(z0), s(y)) -> gr(z0, y) [0] p(0) -> 0 [0] p(s(z0)) -> z0 [0] cond(v0, v1) -> null_cond [0] and(v0, v1) -> null_and [0] even(v0) -> null_even [0] gr(v0, v1) -> null_gr [0] p(v0) -> null_p [0] COND(v0, v1) -> null_COND [0] AND(v0, v1) -> null_AND [0] EVEN(v0) -> null_EVEN [0] GR(v0, v1) -> null_GR [0] P(v0) -> null_P [0] The TRS has the following type information: COND :: true:false:null_and:null_even:null_gr -> 0:s:y:null_p -> c:c1:c2:null_COND true :: true:false:null_and:null_even:null_gr c :: c:c1:c2:null_COND -> c3:c4:c5:null_AND -> c6:c7:c8:null_EVEN -> c:c1:c2:null_COND and :: true:false:null_and:null_even:null_gr -> true:false:null_and:null_even:null_gr -> true:false:null_and:null_even:null_gr even :: 0:s:y:null_p -> true:false:null_and:null_even:null_gr gr :: 0:s:y:null_p -> 0:s:y:null_p -> true:false:null_and:null_even:null_gr 0 :: 0:s:y:null_p p :: 0:s:y:null_p -> 0:s:y:null_p AND :: true:false:null_and:null_even:null_gr -> true:false:null_and:null_even:null_gr -> c3:c4:c5:null_AND EVEN :: 0:s:y:null_p -> c6:c7:c8:null_EVEN c1 :: c:c1:c2:null_COND -> c3:c4:c5:null_AND -> c9:c10:c11:null_GR -> c:c1:c2:null_COND GR :: 0:s:y:null_p -> 0:s:y:null_p -> c9:c10:c11:null_GR c2 :: c:c1:c2:null_COND -> c12:c13:null_P -> c:c1:c2:null_COND P :: 0:s:y:null_p -> c12:c13:null_P false :: true:false:null_and:null_even:null_gr c3 :: c3:c4:c5:null_AND c4 :: c3:c4:c5:null_AND c5 :: c3:c4:c5:null_AND c6 :: c6:c7:c8:null_EVEN s :: 0:s:y:null_p -> 0:s:y:null_p c7 :: c6:c7:c8:null_EVEN c8 :: c6:c7:c8:null_EVEN -> c6:c7:c8:null_EVEN c9 :: c9:c10:c11:null_GR c10 :: c9:c10:c11:null_GR y :: 0:s:y:null_p c11 :: c9:c10:c11:null_GR -> c9:c10:c11:null_GR c12 :: c12:c13:null_P c13 :: c12:c13:null_P cond :: true:false:null_and:null_even:null_gr -> 0:s:y:null_p -> null_cond null_cond :: null_cond null_and :: true:false:null_and:null_even:null_gr null_even :: true:false:null_and:null_even:null_gr null_gr :: true:false:null_and:null_even:null_gr null_p :: 0:s:y:null_p null_COND :: c:c1:c2:null_COND null_AND :: c3:c4:c5:null_AND null_EVEN :: c6:c7:c8:null_EVEN null_GR :: c9:c10:c11:null_GR null_P :: c12:c13:null_P 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: true => 2 0 => 0 false => 1 c3 => 1 c4 => 2 c5 => 3 c6 => 0 c7 => 1 c9 => 1 c10 => 0 y => 1 c12 => 1 c13 => 2 null_cond => 0 null_and => 0 null_even => 0 null_gr => 0 null_p => 0 null_COND => 0 null_AND => 0 null_EVEN => 0 null_GR => 0 null_P => 0 ---------------------------------------- (10) Obligation: Complexity RNTS consisting of the following rules: AND(z, z') -{ 1 }-> 3 :|: z = 2, z' = 2 AND(z, z') -{ 1 }-> 2 :|: z = 1, z0 >= 0, z' = z0 AND(z, z') -{ 1 }-> 1 :|: z = z0, z0 >= 0, z' = 1 AND(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 COND(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 COND(z, z') -{ 1 }-> 1 + COND(and(even(z0), gr(z0, 0)), p(z0)) + P(z0) :|: z = 2, z0 >= 0, z' = z0 COND(z, z') -{ 1 }-> 1 + COND(and(even(z0), gr(z0, 0)), p(z0)) + AND(even(z0), gr(z0, 0)) + GR(z0, 0) :|: z = 2, z0 >= 0, z' = z0 COND(z, z') -{ 1 }-> 1 + COND(and(even(z0), gr(z0, 0)), p(z0)) + AND(even(z0), gr(z0, 0)) + EVEN(z0) :|: z = 2, z0 >= 0, z' = z0 EVEN(z) -{ 1 }-> 1 :|: z = 1 + 0 EVEN(z) -{ 1 }-> 0 :|: z = 0 EVEN(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 EVEN(z) -{ 1 }-> 1 + EVEN(z0) :|: z0 >= 0, z = 1 + (1 + z0) GR(z, z') -{ 1 }-> 1 :|: z0 >= 0, z = 0, z' = z0 GR(z, z') -{ 1 }-> 0 :|: z = 1 + z0, z0 >= 0, z' = 0 GR(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 GR(z, z') -{ 1 }-> 1 + GR(z0, 1) :|: z' = 1 + 1, z = 1 + z0, z0 >= 0 P(z) -{ 1 }-> 2 :|: z = 1 + z0, z0 >= 0 P(z) -{ 1 }-> 1 :|: z = 0 P(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 and(z, z') -{ 0 }-> 2 :|: z = 2, z' = 2 and(z, z') -{ 0 }-> 1 :|: z = z0, z0 >= 0, z' = 1 and(z, z') -{ 0 }-> 1 :|: z = 1, z0 >= 0, z' = z0 and(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 cond(z, z') -{ 0 }-> cond(and(even(z0), gr(z0, 0)), p(z0)) :|: z = 2, z0 >= 0, z' = z0 cond(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 even(z) -{ 0 }-> even(z0) :|: z0 >= 0, z = 1 + (1 + z0) even(z) -{ 0 }-> 2 :|: z = 0 even(z) -{ 0 }-> 1 :|: z = 1 + 0 even(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 gr(z, z') -{ 0 }-> gr(z0, 1) :|: z' = 1 + 1, z = 1 + z0, z0 >= 0 gr(z, z') -{ 0 }-> 2 :|: z = 1 + z0, z0 >= 0, z' = 0 gr(z, z') -{ 0 }-> 1 :|: z0 >= 0, z = 0, z' = z0 gr(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 p(z) -{ 0 }-> z0 :|: z = 1 + z0, z0 >= 0 p(z) -{ 0 }-> 0 :|: z = 0 p(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(V1, V),0,[fun(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V),0,[fun1(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V),0,[fun2(V1, Out)],[V1 >= 0]). eq(start(V1, V),0,[fun3(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V),0,[fun4(V1, Out)],[V1 >= 0]). eq(start(V1, V),0,[cond(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V),0,[and(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V),0,[even(V1, Out)],[V1 >= 0]). eq(start(V1, V),0,[gr(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V),0,[p(V1, Out)],[V1 >= 0]). eq(fun(V1, V, Out),1,[even(V2, Ret00100),gr(V2, 0, Ret00101),and(Ret00100, Ret00101, Ret0010),p(V2, Ret0011),fun(Ret0010, Ret0011, Ret001),even(V2, Ret010),gr(V2, 0, Ret011),fun1(Ret010, Ret011, Ret01),fun2(V2, Ret1)],[Out = 1 + Ret001 + Ret01 + Ret1,V1 = 2,V2 >= 0,V = V2]). eq(fun(V1, V, Out),1,[even(V3, Ret001001),gr(V3, 0, Ret001011),and(Ret001001, Ret001011, Ret00102),p(V3, Ret00111),fun(Ret00102, Ret00111, Ret0012),even(V3, Ret0101),gr(V3, 0, Ret0111),fun1(Ret0101, Ret0111, Ret012),fun3(V3, 0, Ret11)],[Out = 1 + Ret0012 + Ret012 + Ret11,V1 = 2,V3 >= 0,V = V3]). eq(fun(V1, V, Out),1,[even(V4, Ret0100),gr(V4, 0, Ret01011),and(Ret0100, Ret01011, Ret0102),p(V4, Ret0112),fun(Ret0102, Ret0112, Ret013),fun4(V4, Ret12)],[Out = 1 + Ret013 + Ret12,V1 = 2,V4 >= 0,V = V4]). eq(fun1(V1, V, Out),1,[],[Out = 1,V1 = V5,V5 >= 0,V = 1]). eq(fun1(V1, V, Out),1,[],[Out = 2,V1 = 1,V6 >= 0,V = V6]). eq(fun1(V1, V, Out),1,[],[Out = 3,V1 = 2,V = 2]). eq(fun2(V1, Out),1,[],[Out = 0,V1 = 0]). eq(fun2(V1, Out),1,[],[Out = 1,V1 = 1]). eq(fun2(V1, Out),1,[fun2(V7, Ret13)],[Out = 1 + Ret13,V7 >= 0,V1 = 2 + V7]). eq(fun3(V1, V, Out),1,[],[Out = 1,V8 >= 0,V1 = 0,V = V8]). eq(fun3(V1, V, Out),1,[],[Out = 0,V1 = 1 + V9,V9 >= 0,V = 0]). eq(fun3(V1, V, Out),1,[fun3(V10, 1, Ret14)],[Out = 1 + Ret14,V = 2,V1 = 1 + V10,V10 >= 0]). eq(fun4(V1, Out),1,[],[Out = 1,V1 = 0]). eq(fun4(V1, Out),1,[],[Out = 2,V1 = 1 + V11,V11 >= 0]). eq(cond(V1, V, Out),0,[even(V12, Ret00),gr(V12, 0, Ret014),and(Ret00, Ret014, Ret0),p(V12, Ret15),cond(Ret0, Ret15, Ret)],[Out = Ret,V1 = 2,V12 >= 0,V = V12]). eq(and(V1, V, Out),0,[],[Out = 1,V1 = V13,V13 >= 0,V = 1]). eq(and(V1, V, Out),0,[],[Out = 1,V1 = 1,V14 >= 0,V = V14]). eq(and(V1, V, Out),0,[],[Out = 2,V1 = 2,V = 2]). eq(even(V1, Out),0,[],[Out = 2,V1 = 0]). eq(even(V1, Out),0,[],[Out = 1,V1 = 1]). eq(even(V1, Out),0,[even(V15, Ret2)],[Out = Ret2,V15 >= 0,V1 = 2 + V15]). eq(gr(V1, V, Out),0,[],[Out = 1,V16 >= 0,V1 = 0,V = V16]). eq(gr(V1, V, Out),0,[],[Out = 2,V1 = 1 + V17,V17 >= 0,V = 0]). eq(gr(V1, V, Out),0,[gr(V18, 1, Ret3)],[Out = Ret3,V = 2,V1 = 1 + V18,V18 >= 0]). eq(p(V1, Out),0,[],[Out = 0,V1 = 0]). eq(p(V1, Out),0,[],[Out = V19,V1 = 1 + V19,V19 >= 0]). eq(cond(V1, V, Out),0,[],[Out = 0,V21 >= 0,V20 >= 0,V1 = V21,V = V20]). eq(and(V1, V, Out),0,[],[Out = 0,V23 >= 0,V22 >= 0,V1 = V23,V = V22]). eq(even(V1, Out),0,[],[Out = 0,V24 >= 0,V1 = V24]). eq(gr(V1, V, Out),0,[],[Out = 0,V25 >= 0,V26 >= 0,V1 = V25,V = V26]). eq(p(V1, Out),0,[],[Out = 0,V27 >= 0,V1 = V27]). eq(fun(V1, V, Out),0,[],[Out = 0,V28 >= 0,V29 >= 0,V1 = V28,V = V29]). eq(fun1(V1, V, Out),0,[],[Out = 0,V31 >= 0,V30 >= 0,V1 = V31,V = V30]). eq(fun2(V1, Out),0,[],[Out = 0,V32 >= 0,V1 = V32]). eq(fun3(V1, V, Out),0,[],[Out = 0,V33 >= 0,V34 >= 0,V1 = V33,V = V34]). eq(fun4(V1, Out),0,[],[Out = 0,V35 >= 0,V1 = V35]). input_output_vars(fun(V1,V,Out),[V1,V],[Out]). input_output_vars(fun1(V1,V,Out),[V1,V],[Out]). input_output_vars(fun2(V1,Out),[V1],[Out]). input_output_vars(fun3(V1,V,Out),[V1,V],[Out]). input_output_vars(fun4(V1,Out),[V1],[Out]). input_output_vars(cond(V1,V,Out),[V1,V],[Out]). input_output_vars(and(V1,V,Out),[V1,V],[Out]). input_output_vars(even(V1,Out),[V1],[Out]). input_output_vars(gr(V1,V,Out),[V1,V],[Out]). input_output_vars(p(V1,Out),[V1],[Out]). CoFloCo proof output: Preprocessing Cost Relations ===================================== #### Computed strongly connected components 0. non_recursive : [and/3] 1. recursive : [even/2] 2. recursive : [gr/3] 3. non_recursive : [p/2] 4. recursive : [cond/3] 5. non_recursive : [fun1/3] 6. recursive : [fun2/2] 7. recursive : [fun3/3] 8. non_recursive : [fun4/2] 9. recursive [non_tail] : [fun/3] 10. non_recursive : [start/2] #### Obtained direct recursion through partial evaluation 0. SCC is partially evaluated into and/3 1. SCC is partially evaluated into even/2 2. SCC is partially evaluated into gr/3 3. SCC is partially evaluated into p/2 4. SCC is partially evaluated into cond/3 5. SCC is partially evaluated into fun1/3 6. SCC is partially evaluated into fun2/2 7. SCC is partially evaluated into fun3/3 8. SCC is partially evaluated into fun4/2 9. SCC is partially evaluated into fun/3 10. SCC is partially evaluated into start/2 Control-Flow Refinement of Cost Relations ===================================== ### Specialization of cost equations and/3 * CE 35 is refined into CE [46] * CE 32 is refined into CE [47] * CE 34 is refined into CE [48] * CE 33 is refined into CE [49] ### Cost equations --> "Loop" of and/3 * CEs [46] --> Loop 33 * CEs [47] --> Loop 34 * CEs [48] --> Loop 35 * CEs [49] --> Loop 36 ### Ranking functions of CR and(V1,V,Out) #### Partial ranking functions of CR and(V1,V,Out) ### Specialization of cost equations even/2 * CE 39 is refined into CE [50] * CE 37 is refined into CE [51] * CE 36 is refined into CE [52] * CE 38 is refined into CE [53] ### Cost equations --> "Loop" of even/2 * CEs [53] --> Loop 37 * CEs [50] --> Loop 38 * CEs [51] --> Loop 39 * CEs [52] --> Loop 40 ### Ranking functions of CR even(V1,Out) * RF of phase [37]: [V1-1] #### Partial ranking functions of CR even(V1,Out) * Partial RF of phase [37]: - RF of loop [37:1]: V1-1 ### Specialization of cost equations gr/3 * CE 43 is refined into CE [54] * CE 41 is refined into CE [55] * CE 40 is refined into CE [56] * CE 42 is refined into CE [57] ### Cost equations --> "Loop" of gr/3 * CEs [57] --> Loop 41 * CEs [54] --> Loop 42 * CEs [55] --> Loop 43 * CEs [56] --> Loop 44 ### Ranking functions of CR gr(V1,V,Out) #### Partial ranking functions of CR gr(V1,V,Out) ### Specialization of cost equations p/2 * CE 45 is refined into CE [58] * CE 44 is refined into CE [59] ### Cost equations --> "Loop" of p/2 * CEs [58] --> Loop 45 * CEs [59] --> Loop 46 ### Ranking functions of CR p(V1,Out) #### Partial ranking functions of CR p(V1,Out) ### Specialization of cost equations cond/3 * CE 31 is refined into CE [60] * CE 30 is refined into CE [61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91] ### Cost equations --> "Loop" of cond/3 * CEs [87] --> Loop 47 * CEs [86] --> Loop 48 * CEs [79,83] --> Loop 49 * CEs [78,82] --> Loop 50 * CEs [64,65,68,69] --> Loop 51 * CEs [66,67,70,71,75,77,81,85,89,91] --> Loop 52 * CEs [61,72] --> Loop 53 * CEs [62,63,73,74,76,80,84,88,90] --> Loop 54 * CEs [60] --> Loop 55 ### Ranking functions of CR cond(V1,V,Out) * RF of phase [47]: [V-1] #### Partial ranking functions of CR cond(V1,V,Out) * Partial RF of phase [47]: - RF of loop [47:1]: V-1 ### Specialization of cost equations fun1/3 * CE 18 is refined into CE [92] * CE 15 is refined into CE [93] * CE 17 is refined into CE [94] * CE 16 is refined into CE [95] ### Cost equations --> "Loop" of fun1/3 * CEs [92] --> Loop 56 * CEs [93] --> Loop 57 * CEs [94] --> Loop 58 * CEs [95] --> Loop 59 ### Ranking functions of CR fun1(V1,V,Out) #### Partial ranking functions of CR fun1(V1,V,Out) ### Specialization of cost equations fun2/2 * CE 20 is refined into CE [96] * CE 19 is refined into CE [97] * CE 22 is refined into CE [98] * CE 21 is refined into CE [99] ### Cost equations --> "Loop" of fun2/2 * CEs [99] --> Loop 60 * CEs [96] --> Loop 61 * CEs [97,98] --> Loop 62 ### Ranking functions of CR fun2(V1,Out) * RF of phase [60]: [V1-1] #### Partial ranking functions of CR fun2(V1,Out) * Partial RF of phase [60]: - RF of loop [60:1]: V1-1 ### Specialization of cost equations fun3/3 * CE 24 is refined into CE [100] * CE 26 is refined into CE [101] * CE 23 is refined into CE [102] * CE 25 is refined into CE [103] ### Cost equations --> "Loop" of fun3/3 * CEs [103] --> Loop 63 * CEs [100,101] --> Loop 64 * CEs [102] --> Loop 65 ### Ranking functions of CR fun3(V1,V,Out) #### Partial ranking functions of CR fun3(V1,V,Out) ### Specialization of cost equations fun4/2 * CE 28 is refined into CE [104] * CE 29 is refined into CE [105] * CE 27 is refined into CE [106] ### Cost equations --> "Loop" of fun4/2 * CEs [104] --> Loop 66 * CEs [105] --> Loop 67 * CEs [106] --> Loop 68 ### Ranking functions of CR fun4(V1,Out) #### Partial ranking functions of CR fun4(V1,Out) ### Specialization of cost equations fun/3 * CE 14 is refined into CE [107] * CE 11 is refined into CE [108,109,110,111,112,113,114,115,116,117,118,119,120,121,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,152,153,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,363,364,365,366,367,368,369,370,371,372,373,374,375,376,377,378,379,380,381,382,383,384,385,386,387,388,389,390,391,392,393,394,395,396,397,398,399,400,401,402,403,404,405,406,407,408,409,410,411,412,413,414,415,416,417,418,419,420,421,422,423,424,425,426,427,428,429,430,431,432,433,434,435,436,437,438,439,440,441,442,443,444,445,446,447,448,449,450,451,452,453,454,455,456,457,458,459,460,461,462,463,464,465,466,467,468,469,470,471,472,473,474,475,476,477,478,479,480,481,482,483,484,485,486,487,488,489,490,491,492,493,494,495,496,497,498,499,500,501,502,503,504,505,506,507,508,509,510,511,512,513,514,515,516,517,518,519,520,521,522,523,524,525,526,527,528,529,530,531,532,533,534,535,536,537,538,539,540,541,542,543,544,545,546,547,548,549,550,551,552,553,554,555,556,557,558,559,560,561,562,563,564,565,566,567,568,569,570,571,572,573,574,575,576,577,578,579,580,581,582,583,584,585,586,587,588,589,590,591,592,593,594,595,596,597,598,599,600,601,602,603,604,605,606,607,608,609,610,611,612,613,614,615,616,617,618,619,620,621,622,623,624,625,626,627,628,629,630,631,632,633,634,635,636,637,638,639,640,641,642,643,644,645,646,647,648,649,650,651,652,653,654,655,656,657,658,659,660,661,662,663,664,665,666,667,668,669,670,671,672,673,674,675,676,677,678,679,680,681,682,683,684,685,686,687,688,689,690,691,692,693,694,695,696,697,698,699,700,701,702,703,704,705,706,707,708,709,710,711,712,713,714,715,716,717,718,719,720,721,722,723,724,725,726,727,728,729,730,731,732,733,734,735,736,737,738,739,740,741,742,743,744,745,746,747,748,749,750,751,752,753,754,755,756,757,758,759,760,761,762,763,764] * CE 12 is refined into CE [765,766,767,768,769,770,771,772,773,774,775,776,777,778,779,780,781,782,783,784,785,786,787,788,789,790,791,792,793,794,795,796,797,798,799,800,801,802,803,804,805,806,807,808,809,810,811,812,813,814,815,816,817,818,819,820,821,822,823,824,825,826,827,828,829,830,831,832,833,834,835,836,837,838,839,840,841,842,843,844,845,846,847,848,849,850,851,852,853,854,855,856,857,858,859,860,861,862,863,864,865,866,867,868,869,870,871,872,873,874,875,876,877,878,879,880,881,882,883,884,885,886,887,888,889,890,891,892,893,894,895,896,897,898,899,900,901,902,903,904,905,906,907,908,909,910,911,912,913,914,915,916,917,918,919,920,921,922,923,924,925,926,927,928,929,930,931,932,933,934,935,936,937,938,939,940,941,942,943,944,945,946,947,948,949,950,951,952,953,954,955,956,957,958,959,960,961,962,963,964,965,966,967,968,969,970,971,972,973,974,975,976,977,978,979,980,981,982,983,984,985,986,987,988,989,990,991,992,993,994,995,996,997,998,999,1000,1001,1002,1003,1004,1005,1006,1007,1008,1009,1010,1011,1012,1013,1014,1015,1016,1017,1018,1019,1020,1021,1022,1023,1024,1025,1026,1027,1028,1029,1030,1031,1032,1033,1034,1035,1036,1037,1038,1039,1040,1041,1042,1043,1044,1045,1046,1047,1048,1049,1050,1051,1052,1053,1054,1055,1056,1057,1058,1059,1060,1061] * CE 13 is refined into CE [1062,1063,1064,1065,1066,1067,1068,1069,1070,1071,1072,1073,1074,1075,1076,1077,1078,1079,1080,1081,1082,1083,1084,1085,1086,1087,1088,1089,1090,1091,1092,1093,1094,1095,1096,1097,1098,1099,1100,1101,1102,1103,1104,1105,1106,1107,1108,1109,1110,1111,1112,1113,1114,1115,1116,1117,1118,1119,1120,1121,1122,1123,1124] ### Cost equations --> "Loop" of fun/3 * CEs [638,644] --> Loop 69 * CEs [632,635,641,647,653,656] --> Loop 70 * CEs [631,634,640,646,652,655] --> Loop 71 * CEs [637,643,650] --> Loop 72 * CEs [649] --> Loop 73 * CEs [648,1023] --> Loop 74 * CEs [636,642,1019,1021,1116] --> Loop 75 * CEs [630,633,639,645,651,654,1017,1018,1020,1022,1024,1025,1115] --> Loop 76 * CEs [611,617] --> Loop 77 * CEs [605,608,614,620,626,629] --> Loop 78 * CEs [604,607,613,619,625,628] --> Loop 79 * CEs [610,616,623] --> Loop 80 * CEs [622] --> Loop 81 * CEs [621,1014] --> Loop 82 * CEs [609,615,1010,1012,1114] --> Loop 83 * CEs [603,606,612,618,624,627,1008,1009,1011,1013,1015,1016,1113] --> Loop 84 * CEs [416,419,425,431,437,440,524,527,533,539,545,548] --> Loop 85 * CEs [415,418,424,430,436,439,523,526,532,538,544,547] --> Loop 86 * CEs [421,427,434,529,535,542] --> Loop 87 * CEs [433,541] --> Loop 88 * CEs [422,428,432,530,536,540,951,987] --> Loop 89 * CEs [420,426,528,534,947,949,983,985,1100,1108] --> Loop 90 * CEs [414,417,423,429,435,438,522,525,531,537,543,546,945,946,948,950,952,953,981,982,984,986,988,989,1099,1107] --> Loop 91 * CEs [389,392,398,404,410,413,497,500,506,512,518,521] --> Loop 92 * CEs [388,391,397,403,409,412,496,499,505,511,517,520] --> Loop 93 * CEs [394,400,407,502,508,515] --> Loop 94 * CEs [406,514] --> Loop 95 * CEs [395,401,405,503,509,513,942,978] --> Loop 96 * CEs [393,399,501,507,938,940,974,976,1098,1106] --> Loop 97 * CEs [387,390,396,402,408,411,495,498,504,510,516,519,936,937,939,941,943,944,972,973,975,977,979,980,1097,1105] --> Loop 98 * CEs [289,295,368,374,476,482,584,590,692,698,746,752] --> Loop 99 * CEs [282,286,292,298,304,307,361,365,371,377,383,386,470,473,479,485,491,494,578,581,587,593,599,602,686,689,695,701,707,710,740,743,749,755,761,764] --> Loop 100 * CEs [281,285,291,297,303,306,360,364,370,376,382,385,469,472,478,484,490,493,577,580,586,592,598,601,685,688,694,700,706,709,739,742,748,754,760,763] --> Loop 101 * CEs [288,294,301,367,373,380,475,481,488,583,589,596,691,697,704,745,751,758] --> Loop 102 * CEs [300,379,487,595,703,757] --> Loop 103 * CEs [299,378,486,594,702,756,896,933,969,1005,1041,1059] --> Loop 104 * CEs [287,293,366,372,474,480,582,588,690,696,744,750,892,894,929,931,965,967,1001,1003,1037,1039,1055,1057,1091,1096,1104,1112,1120,1124] --> Loop 105 * CEs [252,258,331,337,449,455,557,563,665,671,719,725] --> Loop 106 * CEs [245,249,255,261,267,270,324,328,334,340,346,349,443,446,452,458,464,467,551,554,560,566,572,575,659,662,668,674,680,683,713,716,722,728,734,737] --> Loop 107 * CEs [244,248,254,260,266,269,323,327,333,339,345,348,442,445,451,457,463,466,550,553,559,565,571,574,658,661,667,673,679,682,712,715,721,727,733,736] --> Loop 108 * CEs [251,257,264,330,336,343,448,454,461,556,562,569,664,670,677,718,724,731] --> Loop 109 * CEs [263,342,460,568,676,730] --> Loop 110 * CEs [262,341,459,567,675,729,883,920,960,996,1032,1050] --> Loop 111 * CEs [126,130,138,142,174,178,186,190] --> Loop 112 * CEs [127,131,139,143,175,179,187,191,801,803,807,809,825,827,831,833,1069,1071,1077,1079] --> Loop 113 * CEs [128,132,134,136,140,144,146,148,176,180,182,184,188,192,194,196] --> Loop 114 * CEs [129,133,135,137,141,145,147,149,177,181,183,185,189,193,195,197,802,804,805,806,808,810,811,812,826,828,829,830,832,834,835,836,1068,1070,1076,1078] --> Loop 115 * CEs [150,154,162,166,198,202,210,214,234,238,271,275,311,315,350,354] --> Loop 116 * CEs [151,155,163,167,199,203,211,215,235,239,250,256,272,276,312,316,329,335,351,355,447,453,555,561,663,669,717,723,813,815,819,821,837,839,843,845,873,875,879,881,886,888,905,907,916,918,923,925,956,958,992,994,1028,1030,1046,1048,1073,1075,1081,1083,1089,1094,1102,1110,1118,1122] --> Loop 117 * CEs [152,156,158,160,164,168,170,172,200,204,206,208,212,216,218,220,236,240,242,246,273,277,279,283,313,317,321,325,352,356,358,362] --> Loop 118 * CEs [153,157,159,161,165,169,171,173,201,205,207,209,213,217,219,221,237,241,274,278,280,284,290,296,302,305,314,318,353,357,359,363,369,375,381,384,468,471,477,483,489,492,576,579,585,591,597,600,684,687,693,699,705,708,738,741,747,753,759,762,814,816,817,818,820,822,823,824,838,840,841,842,844,846,847,848,874,876,887,889,890,891,893,895,897,898,906,908,924,926,927,928,930,932,934,935,963,964,966,968,970,971,999,1000,1002,1004,1006,1007,1035,1036,1038,1040,1042,1043,1053,1054,1056,1058,1060,1061,1072,1074,1080,1082,1090,1095,1103,1111,1119,1123] --> Loop 119 * CEs [765,771,849,855] --> Loop 120 * CEs [108,111,222,225,766,767,769,772,773,775,850,851,853,856,857,859,1062,1084] --> Loop 121 * CEs [109,110,112,113,223,224,226,227,768,770,774,776,852,854,858,860,1063,1085] --> Loop 122 * CEs [777,783,789,795,861,867,899,909] --> Loop 123 * CEs [114,117,120,123,228,231,308,319,778,779,781,784,785,787,790,791,793,796,797,799,862,863,865,868,869,871,900,901,903,910,911,914,1064,1066,1086,1092] --> Loop 124 * CEs [115,116,118,119,121,122,124,125,229,230,232,233,243,247,253,259,265,268,309,310,320,322,326,332,338,344,347,441,444,450,456,462,465,549,552,558,564,570,573,657,660,666,672,678,681,711,714,720,726,732,735,780,782,786,788,792,794,798,800,864,866,870,872,877,878,880,882,884,885,902,904,912,913,915,917,919,921,922,954,955,957,959,961,962,990,991,993,995,997,998,1026,1027,1029,1031,1033,1034,1044,1045,1047,1049,1051,1052,1065,1067,1087,1088,1093,1101,1109,1117,1121] --> Loop 125 * CEs [107] --> Loop 126 ### Ranking functions of CR fun(V1,V,Out) * RF of phase [69,70,71,72,73,74,75,76]: [V-1] #### Partial ranking functions of CR fun(V1,V,Out) * Partial RF of phase [69,70,71,72,73,74,75,76]: - RF of loop [69:1,71:1,73:1]: V-2 - RF of loop [70:1,72:1,74:1,75:1,76:1]: V-1 ### Specialization of cost equations start/2 * CE 1 is refined into CE [1125,1126,1127,1128,1129,1130,1131,1132,1133,1134,1135,1136,1137,1138,1139,1140,1141,1142,1143,1144] * CE 2 is refined into CE [1145,1146,1147,1148] * CE 3 is refined into CE [1149,1150,1151,1152] * CE 4 is refined into CE [1153,1154,1155,1156] * CE 5 is refined into CE [1157,1158,1159] * CE 6 is refined into CE [1160,1161] * CE 7 is refined into CE [1162,1163,1164,1165] * CE 8 is refined into CE [1166,1167,1168,1169,1170] * CE 9 is refined into CE [1171,1172,1173,1174] * CE 10 is refined into CE [1175,1176] ### Cost equations --> "Loop" of start/2 * CEs [1173] --> Loop 127 * CEs [1146,1155,1163] --> Loop 128 * CEs [1128,1129,1131,1147,1161,1164] --> Loop 129 * CEs [1125,1126,1127,1130,1132,1133,1134,1135,1136,1137,1138,1139,1140,1141,1142,1143] --> Loop 130 * CEs [1145,1149,1154,1162,1167,1172] --> Loop 131 * CEs [1144,1148,1150,1151,1152,1153,1156,1157,1158,1159,1160,1165,1166,1168,1169,1170,1171,1174,1175,1176] --> Loop 132 ### Ranking functions of CR start(V1,V) #### Partial ranking functions of CR start(V1,V) Computing Bounds ===================================== #### Cost of chains of and(V1,V,Out): * Chain [36]: 0 with precondition: [V1=1,Out=1,V>=0] * Chain [35]: 0 with precondition: [V1=2,V=2,Out=2] * Chain [34]: 0 with precondition: [V=1,Out=1,V1>=0] * Chain [33]: 0 with precondition: [Out=0,V1>=0,V>=0] #### Cost of chains of even(V1,Out): * Chain [[37],40]: 0 with precondition: [Out=2,V1>=2] * Chain [[37],39]: 0 with precondition: [Out=1,V1>=3] * Chain [[37],38]: 0 with precondition: [Out=0,V1>=2] * Chain [40]: 0 with precondition: [V1=0,Out=2] * Chain [39]: 0 with precondition: [V1=1,Out=1] * Chain [38]: 0 with precondition: [Out=0,V1>=0] #### Cost of chains of gr(V1,V,Out): * Chain [44]: 0 with precondition: [V1=0,Out=1,V>=0] * Chain [43]: 0 with precondition: [V=0,Out=2,V1>=1] * Chain [42]: 0 with precondition: [Out=0,V1>=0,V>=0] * Chain [41,44]: 0 with precondition: [V1=1,V=2,Out=1] * Chain [41,42]: 0 with precondition: [V=2,Out=0,V1>=1] #### Cost of chains of p(V1,Out): * Chain [46]: 0 with precondition: [Out=0,V1>=0] * Chain [45]: 0 with precondition: [V1=Out+1,V1>=1] #### Cost of chains of cond(V1,V,Out): * Chain [[47],55]: 0 with precondition: [V1=2,Out=0,V>=2] * Chain [[47],54,55]: 0 with precondition: [V1=2,Out=0,V>=2] * Chain [[47],52,55]: 0 with precondition: [V1=2,Out=0,V>=2] * Chain [[47],51,55]: 0 with precondition: [V1=2,Out=0,V>=2] * Chain [[47],50,55]: 0 with precondition: [V1=2,Out=0,V>=4] * Chain [[47],49,55]: 0 with precondition: [V1=2,Out=0,V>=4] * Chain [[47],48,55]: 0 with precondition: [V1=2,Out=0,V>=3] * Chain [[47],48,54,55]: 0 with precondition: [V1=2,Out=0,V>=3] * Chain [[47],48,53,55]: 0 with precondition: [V1=2,Out=0,V>=3] * Chain [55]: 0 with precondition: [Out=0,V1>=0,V>=0] * Chain [54,55]: 0 with precondition: [V1=2,Out=0,V>=0] * Chain [53,55]: 0 with precondition: [V1=2,V=0,Out=0] * Chain [52,55]: 0 with precondition: [V1=2,Out=0,V>=1] * Chain [51,55]: 0 with precondition: [V1=2,V=1,Out=0] * Chain [50,55]: 0 with precondition: [V1=2,Out=0,V>=3] * Chain [49,55]: 0 with precondition: [V1=2,Out=0,V>=3] * Chain [48,55]: 0 with precondition: [V1=2,Out=0,V>=2] * Chain [48,54,55]: 0 with precondition: [V1=2,Out=0,V>=2] * Chain [48,53,55]: 0 with precondition: [V1=2,Out=0,V>=2] #### Cost of chains of fun1(V1,V,Out): * Chain [59]: 1 with precondition: [V1=1,Out=2,V>=0] * Chain [58]: 1 with precondition: [V1=2,V=2,Out=3] * Chain [57]: 1 with precondition: [V=1,Out=1,V1>=0] * Chain [56]: 0 with precondition: [Out=0,V1>=0,V>=0] #### Cost of chains of fun2(V1,Out): * Chain [[60],62]: 1*it(60)+1 Such that:it(60) =< 2*Out with precondition: [Out>=1,V1>=2*Out] * Chain [[60],61]: 1*it(60)+1 Such that:it(60) =< 2*Out with precondition: [V1+1=2*Out,V1>=3] * Chain [62]: 1 with precondition: [Out=0,V1>=0] * Chain [61]: 1 with precondition: [V1=1,Out=1] #### Cost of chains of fun3(V1,V,Out): * Chain [65]: 1 with precondition: [V1=0,Out=1,V>=0] * Chain [64]: 1 with precondition: [Out=0,V1>=0,V>=0] * Chain [63,65]: 2 with precondition: [V1=1,V=2,Out=2] * Chain [63,64]: 2 with precondition: [V=2,Out=1,V1>=1] #### Cost of chains of fun4(V1,Out): * Chain [68]: 1 with precondition: [V1=0,Out=1] * Chain [67]: 0 with precondition: [Out=0,V1>=0] * Chain [66]: 1 with precondition: [Out=2,V1>=1] #### Cost of chains of fun(V1,V,Out): * Chain [[69,70,71,72,73,74,75,76],126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+0 Such that:aux(13) =< V it(69) =< aux(13) aux(7) =< aux(13)+1 aux(6) =< aux(13) s(30) =< it(69)*aux(13) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=2,Out>=1] * Chain [[69,70,71,72,73,74,75,76],125,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+2 Such that:aux(14) =< V it(69) =< aux(14) aux(7) =< aux(14)+1 aux(6) =< aux(14) s(30) =< it(69)*aux(14) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=2,Out>=2] * Chain [[69,70,71,72,73,74,75,76],119,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+2 Such that:aux(15) =< V it(69) =< aux(15) aux(7) =< aux(15)+1 aux(6) =< aux(15) s(30) =< it(69)*aux(15) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=2,Out>=2] * Chain [[69,70,71,72,73,74,75,76],118,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+2 Such that:aux(16) =< V it(69) =< aux(16) aux(7) =< aux(16)+1 aux(6) =< aux(16) s(30) =< it(69)*aux(16) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=2,Out>=V+1] * Chain [[69,70,71,72,73,74,75,76],117,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+3 Such that:aux(17) =< V it(69) =< aux(17) aux(7) =< aux(17)+1 aux(6) =< aux(17) s(30) =< it(69)*aux(17) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=2,Out>=4] * Chain [[69,70,71,72,73,74,75,76],116,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+3 Such that:aux(18) =< V it(69) =< aux(18) aux(7) =< aux(18)+1 aux(6) =< aux(18) s(30) =< it(69)*aux(18) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=2,Out>=V+3] * Chain [[69,70,71,72,73,74,75,76],115,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+2 Such that:aux(19) =< V it(69) =< aux(19) aux(7) =< aux(19)+1 aux(6) =< aux(19) s(30) =< it(69)*aux(19) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=2,Out>=V] * Chain [[69,70,71,72,73,74,75,76],114,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+2 Such that:aux(20) =< V it(69) =< aux(20) aux(7) =< aux(20)+1 aux(6) =< aux(20) s(30) =< it(69)*aux(20) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=2,Out>=V+1] * Chain [[69,70,71,72,73,74,75,76],113,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+3 Such that:aux(21) =< V it(69) =< aux(21) aux(7) =< aux(21)+1 aux(6) =< aux(21) s(30) =< it(69)*aux(21) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=2,Out>=V+2] * Chain [[69,70,71,72,73,74,75,76],112,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+3 Such that:aux(22) =< V it(69) =< aux(22) aux(7) =< aux(22)+1 aux(6) =< aux(22) s(30) =< it(69)*aux(22) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=2,Out>=V+3] * Chain [[69,70,71,72,73,74,75,76],111,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+3 Such that:aux(23) =< V it(69) =< aux(23) aux(7) =< aux(23)+1 aux(6) =< aux(23) s(30) =< it(69)*aux(23) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=5] * Chain [[69,70,71,72,73,74,75,76],110,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+6*s(39)+3 Such that:aux(11) =< V aux(25) =< V+9 s(39) =< aux(25) it(69) =< aux(11) it(69) =< aux(25) aux(7) =< aux(11)+1 aux(6) =< aux(11) s(30) =< it(69)*aux(11) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,2*Out>=V+10] * Chain [[69,70,71,72,73,74,75,76],109,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+12*s(45)+6*s(47)+3 Such that:aux(28) =< V aux(29) =< V+1 s(47) =< aux(28) s(45) =< aux(29) it(69) =< aux(28) it(69) =< aux(29) aux(7) =< aux(28)+1 aux(6) =< aux(28) s(30) =< it(69)*aux(28) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=6] * Chain [[69,70,71,72,73,74,75,76],108,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+36*s(63)+2 Such that:aux(11) =< V aux(31) =< V+3 s(63) =< aux(31) it(69) =< aux(11) it(69) =< aux(31) aux(7) =< aux(11)+1 aux(6) =< aux(11) s(30) =< it(69)*aux(11) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,2*Out>=V+4] * Chain [[69,70,71,72,73,74,75,76],107,126]: 57*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+2 Such that:aux(33) =< V it(69) =< aux(33) aux(7) =< aux(33)+1 aux(6) =< aux(33) s(30) =< it(69)*aux(33) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=3] * Chain [[69,70,71,72,73,74,75,76],106,126]: 33*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+3 Such that:aux(35) =< V it(69) =< aux(35) aux(7) =< aux(35)+1 aux(6) =< aux(35) s(30) =< it(69)*aux(35) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,Out>=5] * Chain [[69,70,71,72,73,74,75,76],105,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+3 Such that:aux(36) =< V it(69) =< aux(36) aux(7) =< aux(36)+1 aux(6) =< aux(36) s(30) =< it(69)*aux(36) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=2,Out>=4] * Chain [[69,70,71,72,73,74,75,76],104,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+3 Such that:aux(37) =< V it(69) =< aux(37) aux(7) =< aux(37)+1 aux(6) =< aux(37) s(30) =< it(69)*aux(37) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=5] * Chain [[69,70,71,72,73,74,75,76],103,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+6*s(147)+3 Such that:aux(11) =< V aux(39) =< V+9 s(147) =< aux(39) it(69) =< aux(11) it(69) =< aux(39) aux(7) =< aux(11)+1 aux(6) =< aux(11) s(30) =< it(69)*aux(11) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,2*Out>=V+10] * Chain [[69,70,71,72,73,74,75,76],102,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+12*s(153)+6*s(155)+3 Such that:aux(42) =< V aux(43) =< V+1 s(155) =< aux(42) s(153) =< aux(43) it(69) =< aux(42) it(69) =< aux(43) aux(7) =< aux(42)+1 aux(6) =< aux(42) s(30) =< it(69)*aux(42) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=6] * Chain [[69,70,71,72,73,74,75,76],101,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+36*s(171)+2 Such that:aux(11) =< V aux(45) =< V+3 s(171) =< aux(45) it(69) =< aux(11) it(69) =< aux(45) aux(7) =< aux(11)+1 aux(6) =< aux(11) s(30) =< it(69)*aux(11) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,2*Out>=V+4] * Chain [[69,70,71,72,73,74,75,76],100,126]: 57*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+2 Such that:aux(47) =< V it(69) =< aux(47) aux(7) =< aux(47)+1 aux(6) =< aux(47) s(30) =< it(69)*aux(47) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=3] * Chain [[69,70,71,72,73,74,75,76],99,126]: 33*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+3 Such that:aux(49) =< V it(69) =< aux(49) aux(7) =< aux(49)+1 aux(6) =< aux(49) s(30) =< it(69)*aux(49) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,Out>=5] * Chain [[69,70,71,72,73,74,75,76],98,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+2 Such that:aux(50) =< V it(69) =< aux(50) aux(7) =< aux(50)+1 aux(6) =< aux(50) s(30) =< it(69)*aux(50) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,Out>=2] * Chain [[69,70,71,72,73,74,75,76],97,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+3 Such that:aux(51) =< V it(69) =< aux(51) aux(7) =< aux(51)+1 aux(6) =< aux(51) s(30) =< it(69)*aux(51) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,Out>=4] * Chain [[69,70,71,72,73,74,75,76],96,126]: 25*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+3 Such that:aux(53) =< V it(69) =< aux(53) aux(7) =< aux(53)+1 aux(6) =< aux(53) s(30) =< it(69)*aux(53) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,Out>=5] * Chain [[69,70,71,72,73,74,75,76],95,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+2*s(259)+3 Such that:aux(11) =< V aux(55) =< V+9 s(259) =< aux(55) it(69) =< aux(11) it(69) =< aux(55) aux(7) =< aux(11)+1 aux(6) =< aux(11) s(30) =< it(69)*aux(11) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,2*Out>=V+10] * Chain [[69,70,71,72,73,74,75,76],94,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+4*s(261)+2*s(263)+3 Such that:aux(58) =< V aux(59) =< V+1 s(263) =< aux(58) s(261) =< aux(59) it(69) =< aux(58) it(69) =< aux(59) aux(7) =< aux(58)+1 aux(6) =< aux(58) s(30) =< it(69)*aux(58) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,Out>=6] * Chain [[69,70,71,72,73,74,75,76],93,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+12*s(267)+2 Such that:aux(11) =< V aux(61) =< V+3 s(267) =< aux(61) it(69) =< aux(11) it(69) =< aux(61) aux(7) =< aux(11)+1 aux(6) =< aux(11) s(30) =< it(69)*aux(11) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,2*Out>=V+4] * Chain [[69,70,71,72,73,74,75,76],92,126]: 33*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+2 Such that:aux(63) =< V it(69) =< aux(63) aux(7) =< aux(63)+1 aux(6) =< aux(63) s(30) =< it(69)*aux(63) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,Out>=3] * Chain [[69,70,71,72,73,74,75,76],91,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+2 Such that:aux(64) =< V it(69) =< aux(64) aux(7) =< aux(64)+1 aux(6) =< aux(64) s(30) =< it(69)*aux(64) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,Out>=2] * Chain [[69,70,71,72,73,74,75,76],90,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+3 Such that:aux(65) =< V it(69) =< aux(65) aux(7) =< aux(65)+1 aux(6) =< aux(65) s(30) =< it(69)*aux(65) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,Out>=4] * Chain [[69,70,71,72,73,74,75,76],89,126]: 25*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+3 Such that:aux(67) =< V it(69) =< aux(67) aux(7) =< aux(67)+1 aux(6) =< aux(67) s(30) =< it(69)*aux(67) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,Out>=5] * Chain [[69,70,71,72,73,74,75,76],88,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+2*s(295)+3 Such that:aux(11) =< V aux(69) =< V+9 s(295) =< aux(69) it(69) =< aux(11) it(69) =< aux(69) aux(7) =< aux(11)+1 aux(6) =< aux(11) s(30) =< it(69)*aux(11) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,2*Out>=V+10] * Chain [[69,70,71,72,73,74,75,76],87,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+4*s(297)+2*s(299)+3 Such that:aux(72) =< V aux(73) =< V+1 s(299) =< aux(72) s(297) =< aux(73) it(69) =< aux(72) it(69) =< aux(73) aux(7) =< aux(72)+1 aux(6) =< aux(72) s(30) =< it(69)*aux(72) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,Out>=6] * Chain [[69,70,71,72,73,74,75,76],86,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+12*s(303)+2 Such that:aux(11) =< V aux(75) =< V+3 s(303) =< aux(75) it(69) =< aux(11) it(69) =< aux(75) aux(7) =< aux(11)+1 aux(6) =< aux(11) s(30) =< it(69)*aux(11) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,2*Out>=V+4] * Chain [[69,70,71,72,73,74,75,76],85,126]: 33*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+2 Such that:aux(77) =< V it(69) =< aux(77) aux(7) =< aux(77)+1 aux(6) =< aux(77) s(30) =< it(69)*aux(77) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,Out>=3] * Chain [[69,70,71,72,73,74,75,76],84,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+2 Such that:aux(78) =< V it(69) =< aux(78) aux(7) =< aux(78)+1 aux(6) =< aux(78) s(30) =< it(69)*aux(78) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=2] * Chain [[69,70,71,72,73,74,75,76],84,125,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+4 Such that:aux(79) =< V it(69) =< aux(79) aux(7) =< aux(79)+1 aux(6) =< aux(79) s(30) =< it(69)*aux(79) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=3] * Chain [[69,70,71,72,73,74,75,76],84,124,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+5 Such that:aux(80) =< V it(69) =< aux(80) aux(7) =< aux(80)+1 aux(6) =< aux(80) s(30) =< it(69)*aux(80) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=4] * Chain [[69,70,71,72,73,74,75,76],84,123,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+5 Such that:aux(81) =< V it(69) =< aux(81) aux(7) =< aux(81)+1 aux(6) =< aux(81) s(30) =< it(69)*aux(81) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=5] * Chain [[69,70,71,72,73,74,75,76],84,122,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+4 Such that:aux(82) =< V it(69) =< aux(82) aux(7) =< aux(82)+1 aux(6) =< aux(82) s(30) =< it(69)*aux(82) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=3] * Chain [[69,70,71,72,73,74,75,76],84,121,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+5 Such that:aux(83) =< V it(69) =< aux(83) aux(7) =< aux(83)+1 aux(6) =< aux(83) s(30) =< it(69)*aux(83) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=4] * Chain [[69,70,71,72,73,74,75,76],84,120,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+5 Such that:aux(84) =< V it(69) =< aux(84) aux(7) =< aux(84)+1 aux(6) =< aux(84) s(30) =< it(69)*aux(84) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=5] * Chain [[69,70,71,72,73,74,75,76],83,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+3 Such that:aux(85) =< V it(69) =< aux(85) aux(7) =< aux(85)+1 aux(6) =< aux(85) s(30) =< it(69)*aux(85) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=4] * Chain [[69,70,71,72,73,74,75,76],83,125,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+5 Such that:aux(86) =< V it(69) =< aux(86) aux(7) =< aux(86)+1 aux(6) =< aux(86) s(30) =< it(69)*aux(86) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=5] * Chain [[69,70,71,72,73,74,75,76],83,124,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+6 Such that:aux(87) =< V it(69) =< aux(87) aux(7) =< aux(87)+1 aux(6) =< aux(87) s(30) =< it(69)*aux(87) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=6] * Chain [[69,70,71,72,73,74,75,76],83,123,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+6 Such that:aux(88) =< V it(69) =< aux(88) aux(7) =< aux(88)+1 aux(6) =< aux(88) s(30) =< it(69)*aux(88) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=7] * Chain [[69,70,71,72,73,74,75,76],83,122,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+5 Such that:aux(89) =< V it(69) =< aux(89) aux(7) =< aux(89)+1 aux(6) =< aux(89) s(30) =< it(69)*aux(89) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=5] * Chain [[69,70,71,72,73,74,75,76],83,121,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+6 Such that:aux(90) =< V it(69) =< aux(90) aux(7) =< aux(90)+1 aux(6) =< aux(90) s(30) =< it(69)*aux(90) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=6] * Chain [[69,70,71,72,73,74,75,76],83,120,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+6 Such that:aux(91) =< V it(69) =< aux(91) aux(7) =< aux(91)+1 aux(6) =< aux(91) s(30) =< it(69)*aux(91) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=7] * Chain [[69,70,71,72,73,74,75,76],82,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+3 Such that:aux(92) =< V it(69) =< aux(92) aux(7) =< aux(92)+1 aux(6) =< aux(92) s(30) =< it(69)*aux(92) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=5] * Chain [[69,70,71,72,73,74,75,76],82,125,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+5 Such that:aux(93) =< V it(69) =< aux(93) aux(7) =< aux(93)+1 aux(6) =< aux(93) s(30) =< it(69)*aux(93) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=6] * Chain [[69,70,71,72,73,74,75,76],82,124,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+6 Such that:aux(94) =< V it(69) =< aux(94) aux(7) =< aux(94)+1 aux(6) =< aux(94) s(30) =< it(69)*aux(94) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=7] * Chain [[69,70,71,72,73,74,75,76],82,123,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+6 Such that:aux(95) =< V it(69) =< aux(95) aux(7) =< aux(95)+1 aux(6) =< aux(95) s(30) =< it(69)*aux(95) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=8] * Chain [[69,70,71,72,73,74,75,76],82,122,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+5 Such that:aux(96) =< V it(69) =< aux(96) aux(7) =< aux(96)+1 aux(6) =< aux(96) s(30) =< it(69)*aux(96) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=6] * Chain [[69,70,71,72,73,74,75,76],82,121,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+6 Such that:aux(97) =< V it(69) =< aux(97) aux(7) =< aux(97)+1 aux(6) =< aux(97) s(30) =< it(69)*aux(97) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=7] * Chain [[69,70,71,72,73,74,75,76],82,120,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+6 Such that:aux(98) =< V it(69) =< aux(98) aux(7) =< aux(98)+1 aux(6) =< aux(98) s(30) =< it(69)*aux(98) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=8] * Chain [[69,70,71,72,73,74,75,76],81,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+1*s(327)+3 Such that:aux(11) =< V aux(99) =< V+9 s(327) =< aux(99) it(69) =< aux(11) it(69) =< aux(99) aux(7) =< aux(11)+1 aux(6) =< aux(11) s(30) =< it(69)*aux(11) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,2*Out>=V+10] * Chain [[69,70,71,72,73,74,75,76],81,125,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+1*s(327)+5 Such that:aux(11) =< V aux(100) =< V+11 s(327) =< aux(100) it(69) =< aux(11) it(69) =< aux(100) aux(7) =< aux(11)+1 aux(6) =< aux(11) s(30) =< it(69)*aux(11) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,2*Out>=V+12] * Chain [[69,70,71,72,73,74,75,76],81,124,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+1*s(327)+6 Such that:aux(11) =< V aux(101) =< V+13 s(327) =< aux(101) it(69) =< aux(11) it(69) =< aux(101) aux(7) =< aux(11)+1 aux(6) =< aux(11) s(30) =< it(69)*aux(11) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,2*Out>=V+14] * Chain [[69,70,71,72,73,74,75,76],81,123,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+1*s(327)+6 Such that:aux(11) =< V aux(102) =< V+15 s(327) =< aux(102) it(69) =< aux(11) it(69) =< aux(102) aux(7) =< aux(11)+1 aux(6) =< aux(11) s(30) =< it(69)*aux(11) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,2*Out>=V+16] * Chain [[69,70,71,72,73,74,75,76],81,122,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+1*s(327)+5 Such that:aux(11) =< V aux(103) =< V+11 s(327) =< aux(103) it(69) =< aux(11) it(69) =< aux(103) aux(7) =< aux(11)+1 aux(6) =< aux(11) s(30) =< it(69)*aux(11) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,2*Out>=V+12] * Chain [[69,70,71,72,73,74,75,76],81,121,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+1*s(327)+6 Such that:aux(11) =< V aux(104) =< V+13 s(327) =< aux(104) it(69) =< aux(11) it(69) =< aux(104) aux(7) =< aux(11)+1 aux(6) =< aux(11) s(30) =< it(69)*aux(11) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,2*Out>=V+14] * Chain [[69,70,71,72,73,74,75,76],81,120,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+1*s(327)+6 Such that:aux(11) =< V aux(105) =< V+15 s(327) =< aux(105) it(69) =< aux(11) it(69) =< aux(105) aux(7) =< aux(11)+1 aux(6) =< aux(11) s(30) =< it(69)*aux(11) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,2*Out>=V+16] * Chain [[69,70,71,72,73,74,75,76],80,126]: 22*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+2*s(328)+3 Such that:aux(106) =< V+1 aux(107) =< V it(69) =< aux(107) s(328) =< aux(106) aux(7) =< aux(107)+1 aux(6) =< aux(107) s(30) =< it(69)*aux(107) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=6] * Chain [[69,70,71,72,73,74,75,76],80,125,126]: 22*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+2*s(328)+5 Such that:aux(106) =< V+1 aux(108) =< V it(69) =< aux(108) s(328) =< aux(106) aux(7) =< aux(108)+1 aux(6) =< aux(108) s(30) =< it(69)*aux(108) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=7] * Chain [[69,70,71,72,73,74,75,76],80,124,126]: 22*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+2*s(328)+6 Such that:aux(106) =< V+1 aux(109) =< V it(69) =< aux(109) s(328) =< aux(106) aux(7) =< aux(109)+1 aux(6) =< aux(109) s(30) =< it(69)*aux(109) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=8] * Chain [[69,70,71,72,73,74,75,76],80,123,126]: 22*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+2*s(328)+6 Such that:aux(106) =< V+1 aux(110) =< V it(69) =< aux(110) s(328) =< aux(106) aux(7) =< aux(110)+1 aux(6) =< aux(110) s(30) =< it(69)*aux(110) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=9] * Chain [[69,70,71,72,73,74,75,76],80,122,126]: 22*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+2*s(328)+5 Such that:aux(106) =< V+1 aux(111) =< V it(69) =< aux(111) s(328) =< aux(106) aux(7) =< aux(111)+1 aux(6) =< aux(111) s(30) =< it(69)*aux(111) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=7] * Chain [[69,70,71,72,73,74,75,76],80,121,126]: 22*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+2*s(328)+6 Such that:aux(106) =< V+1 aux(112) =< V it(69) =< aux(112) s(328) =< aux(106) aux(7) =< aux(112)+1 aux(6) =< aux(112) s(30) =< it(69)*aux(112) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=8] * Chain [[69,70,71,72,73,74,75,76],80,120,126]: 22*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+2*s(328)+6 Such that:aux(106) =< V+1 aux(113) =< V it(69) =< aux(113) s(328) =< aux(106) aux(7) =< aux(113)+1 aux(6) =< aux(113) s(30) =< it(69)*aux(113) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=9] * Chain [[69,70,71,72,73,74,75,76],79,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+6*s(331)+2 Such that:aux(11) =< V aux(115) =< V+3 s(331) =< aux(115) it(69) =< aux(11) it(69) =< aux(115) aux(7) =< aux(11)+1 aux(6) =< aux(11) s(30) =< it(69)*aux(11) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,2*Out>=V+4] * Chain [[69,70,71,72,73,74,75,76],79,125,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+6*s(331)+4 Such that:aux(11) =< V aux(116) =< V+5 s(331) =< aux(116) it(69) =< aux(11) it(69) =< aux(116) aux(7) =< aux(11)+1 aux(6) =< aux(11) s(30) =< it(69)*aux(11) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,2*Out>=V+6] * Chain [[69,70,71,72,73,74,75,76],79,124,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+6*s(331)+5 Such that:aux(11) =< V aux(117) =< V+7 s(331) =< aux(117) it(69) =< aux(11) it(69) =< aux(117) aux(7) =< aux(11)+1 aux(6) =< aux(11) s(30) =< it(69)*aux(11) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,2*Out>=V+8] * Chain [[69,70,71,72,73,74,75,76],79,123,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+6*s(331)+5 Such that:aux(11) =< V aux(118) =< V+9 s(331) =< aux(118) it(69) =< aux(11) it(69) =< aux(118) aux(7) =< aux(11)+1 aux(6) =< aux(11) s(30) =< it(69)*aux(11) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,2*Out>=V+10] * Chain [[69,70,71,72,73,74,75,76],79,122,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+6*s(331)+4 Such that:aux(11) =< V aux(119) =< V+5 s(331) =< aux(119) it(69) =< aux(11) it(69) =< aux(119) aux(7) =< aux(11)+1 aux(6) =< aux(11) s(30) =< it(69)*aux(11) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,2*Out>=V+6] * Chain [[69,70,71,72,73,74,75,76],79,121,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+6*s(331)+5 Such that:aux(11) =< V aux(120) =< V+7 s(331) =< aux(120) it(69) =< aux(11) it(69) =< aux(120) aux(7) =< aux(11)+1 aux(6) =< aux(11) s(30) =< it(69)*aux(11) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,2*Out>=V+8] * Chain [[69,70,71,72,73,74,75,76],79,120,126]: 21*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+6*s(331)+5 Such that:aux(11) =< V aux(121) =< V+9 s(331) =< aux(121) it(69) =< aux(11) it(69) =< aux(121) aux(7) =< aux(11)+1 aux(6) =< aux(11) s(30) =< it(69)*aux(11) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,2*Out>=V+10] * Chain [[69,70,71,72,73,74,75,76],78,126]: 27*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+2 Such that:aux(123) =< V it(69) =< aux(123) aux(7) =< aux(123)+1 aux(6) =< aux(123) s(30) =< it(69)*aux(123) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=3] * Chain [[69,70,71,72,73,74,75,76],78,125,126]: 27*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+4 Such that:aux(124) =< V it(69) =< aux(124) aux(7) =< aux(124)+1 aux(6) =< aux(124) s(30) =< it(69)*aux(124) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=4] * Chain [[69,70,71,72,73,74,75,76],78,124,126]: 27*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+5 Such that:aux(125) =< V it(69) =< aux(125) aux(7) =< aux(125)+1 aux(6) =< aux(125) s(30) =< it(69)*aux(125) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=5] * Chain [[69,70,71,72,73,74,75,76],78,123,126]: 27*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+5 Such that:aux(126) =< V it(69) =< aux(126) aux(7) =< aux(126)+1 aux(6) =< aux(126) s(30) =< it(69)*aux(126) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=6] * Chain [[69,70,71,72,73,74,75,76],78,122,126]: 27*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+4 Such that:aux(127) =< V it(69) =< aux(127) aux(7) =< aux(127)+1 aux(6) =< aux(127) s(30) =< it(69)*aux(127) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=4] * Chain [[69,70,71,72,73,74,75,76],78,121,126]: 27*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+5 Such that:aux(128) =< V it(69) =< aux(128) aux(7) =< aux(128)+1 aux(6) =< aux(128) s(30) =< it(69)*aux(128) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=5] * Chain [[69,70,71,72,73,74,75,76],78,120,126]: 27*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+5 Such that:aux(129) =< V it(69) =< aux(129) aux(7) =< aux(129)+1 aux(6) =< aux(129) s(30) =< it(69)*aux(129) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=3,Out>=6] * Chain [[69,70,71,72,73,74,75,76],77,126]: 23*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+3 Such that:aux(131) =< V it(69) =< aux(131) aux(7) =< aux(131)+1 aux(6) =< aux(131) s(30) =< it(69)*aux(131) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,Out>=5] * Chain [[69,70,71,72,73,74,75,76],77,125,126]: 23*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+5 Such that:aux(132) =< V it(69) =< aux(132) aux(7) =< aux(132)+1 aux(6) =< aux(132) s(30) =< it(69)*aux(132) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,Out>=6] * Chain [[69,70,71,72,73,74,75,76],77,124,126]: 23*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+6 Such that:aux(133) =< V it(69) =< aux(133) aux(7) =< aux(133)+1 aux(6) =< aux(133) s(30) =< it(69)*aux(133) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,Out>=7] * Chain [[69,70,71,72,73,74,75,76],77,123,126]: 23*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+6 Such that:aux(134) =< V it(69) =< aux(134) aux(7) =< aux(134)+1 aux(6) =< aux(134) s(30) =< it(69)*aux(134) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,Out>=8] * Chain [[69,70,71,72,73,74,75,76],77,122,126]: 23*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+5 Such that:aux(135) =< V it(69) =< aux(135) aux(7) =< aux(135)+1 aux(6) =< aux(135) s(30) =< it(69)*aux(135) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,Out>=6] * Chain [[69,70,71,72,73,74,75,76],77,121,126]: 23*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+6 Such that:aux(136) =< V it(69) =< aux(136) aux(7) =< aux(136)+1 aux(6) =< aux(136) s(30) =< it(69)*aux(136) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,Out>=7] * Chain [[69,70,71,72,73,74,75,76],77,120,126]: 23*it(69)+2*s(29)+6*s(31)+8*s(33)+1*s(36)+1*s(38)+6 Such that:aux(137) =< V it(69) =< aux(137) aux(7) =< aux(137)+1 aux(6) =< aux(137) s(30) =< it(69)*aux(137) s(38) =< it(69)*aux(7) s(34) =< it(69)*aux(7) s(36) =< it(69)*aux(6) s(32) =< it(69)*aux(6) s(33) =< s(34) s(31) =< s(32) s(29) =< s(30) with precondition: [V1=2,V>=4,Out>=8] * Chain [126]: 0 with precondition: [Out=0,V1>=0,V>=0] * Chain [125,126]: 2 with precondition: [V1=2,Out=1,V>=0] * Chain [124,126]: 3 with precondition: [V1=2,V=0,Out=2] * Chain [123,126]: 3 with precondition: [V1=2,V=0,Out=3] * Chain [122,126]: 2 with precondition: [V1=2,V=0,Out=1] * Chain [121,126]: 3 with precondition: [V1=2,V=0,Out=2] * Chain [120,126]: 3 with precondition: [V1=2,V=0,Out=3] * Chain [119,126]: 2 with precondition: [V1=2,Out=1,V>=1] * Chain [118,126]: 2 with precondition: [V1=2,V=1,Out=2] * Chain [117,126]: 3 with precondition: [V1=2,Out=3,V>=1] * Chain [116,126]: 3 with precondition: [V1=2,V=1,Out=4] * Chain [115,126]: 2 with precondition: [V1=2,V=1,Out=1] * Chain [114,126]: 2 with precondition: [V1=2,V=1,Out=2] * Chain [113,126]: 3 with precondition: [V1=2,V=1,Out=3] * Chain [112,126]: 3 with precondition: [V1=2,V=1,Out=4] * Chain [111,126]: 3 with precondition: [V1=2,Out=4,V>=2] * Chain [110,126]: 6*s(39)+3 Such that:aux(24) =< 2*Out s(39) =< aux(24) with precondition: [V1=2,V+9=2*Out,V>=3] * Chain [109,126]: 12*s(45)+6*s(47)+3 Such that:aux(26) =< V aux(27) =< V+1 s(47) =< aux(26) s(45) =< aux(27) with precondition: [V1=2,Out>=5,V+8>=2*Out] * Chain [108,126]: 36*s(63)+2 Such that:aux(30) =< 2*Out s(63) =< aux(30) with precondition: [V1=2,V+3=2*Out,V>=3] * Chain [107,126]: 36*s(99)+2 Such that:aux(32) =< V s(99) =< aux(32) with precondition: [V1=2,Out>=2,V+2>=2*Out] * Chain [106,126]: 12*s(135)+3 Such that:aux(34) =< V s(135) =< aux(34) with precondition: [V1=2,V>=3,Out>=4,V+6>=2*Out] * Chain [105,126]: 3 with precondition: [V1=2,Out=3,V>=1] * Chain [104,126]: 3 with precondition: [V1=2,Out=4,V>=2] * Chain [103,126]: 6*s(147)+3 Such that:aux(38) =< 2*Out s(147) =< aux(38) with precondition: [V1=2,V+9=2*Out,V>=3] * Chain [102,126]: 12*s(153)+6*s(155)+3 Such that:aux(40) =< V aux(41) =< V+1 s(155) =< aux(40) s(153) =< aux(41) with precondition: [V1=2,Out>=5,V+8>=2*Out] * Chain [101,126]: 36*s(171)+2 Such that:aux(44) =< 2*Out s(171) =< aux(44) with precondition: [V1=2,V+3=2*Out,V>=3] * Chain [100,126]: 36*s(207)+2 Such that:aux(46) =< V s(207) =< aux(46) with precondition: [V1=2,Out>=2,V+2>=2*Out] * Chain [99,126]: 12*s(243)+3 Such that:aux(48) =< V s(243) =< aux(48) with precondition: [V1=2,V>=3,Out>=4,V+6>=2*Out] * Chain [98,126]: 2 with precondition: [V1=2,Out=1,V>=3] * Chain [97,126]: 3 with precondition: [V1=2,Out=3,V>=3] * Chain [96,126]: 4*s(255)+3 Such that:aux(52) =< V s(255) =< aux(52) with precondition: [V1=2,V>=3,Out>=4,V+6>=2*Out] * Chain [95,126]: 2*s(259)+3 Such that:aux(54) =< 2*Out s(259) =< aux(54) with precondition: [V1=2,V+9=2*Out,V>=3] * Chain [94,126]: 4*s(261)+2*s(263)+3 Such that:aux(56) =< V aux(57) =< V+1 s(263) =< aux(56) s(261) =< aux(57) with precondition: [V1=2,V>=3,Out>=5,V+8>=2*Out] * Chain [93,126]: 12*s(267)+2 Such that:aux(60) =< 2*Out s(267) =< aux(60) with precondition: [V1=2,V+3=2*Out,V>=3] * Chain [92,126]: 12*s(279)+2 Such that:aux(62) =< V s(279) =< aux(62) with precondition: [V1=2,V>=3,Out>=2,V+2>=2*Out] * Chain [91,126]: 2 with precondition: [V1=2,Out=1,V>=3] * Chain [90,126]: 3 with precondition: [V1=2,Out=3,V>=3] * Chain [89,126]: 4*s(291)+3 Such that:aux(66) =< V s(291) =< aux(66) with precondition: [V1=2,V>=3,Out>=4,V+6>=2*Out] * Chain [88,126]: 2*s(295)+3 Such that:aux(68) =< 2*Out s(295) =< aux(68) with precondition: [V1=2,V+9=2*Out,V>=3] * Chain [87,126]: 4*s(297)+2*s(299)+3 Such that:aux(70) =< V aux(71) =< V+1 s(299) =< aux(70) s(297) =< aux(71) with precondition: [V1=2,V>=3,Out>=5,V+8>=2*Out] * Chain [86,126]: 12*s(303)+2 Such that:aux(74) =< 2*Out s(303) =< aux(74) with precondition: [V1=2,V+3=2*Out,V>=3] * Chain [85,126]: 12*s(315)+2 Such that:aux(76) =< V s(315) =< aux(76) with precondition: [V1=2,V>=3,Out>=2,V+2>=2*Out] * Chain [84,126]: 2 with precondition: [V1=2,Out=1,V>=2] * Chain [84,125,126]: 4 with precondition: [V1=2,Out=2,V>=2] * Chain [84,124,126]: 5 with precondition: [V1=2,Out=3,V>=2] * Chain [84,123,126]: 5 with precondition: [V1=2,Out=4,V>=2] * Chain [84,122,126]: 4 with precondition: [V1=2,Out=2,V>=2] * Chain [84,121,126]: 5 with precondition: [V1=2,Out=3,V>=2] * Chain [84,120,126]: 5 with precondition: [V1=2,Out=4,V>=2] * Chain [83,126]: 3 with precondition: [V1=2,Out=3,V>=2] * Chain [83,125,126]: 5 with precondition: [V1=2,Out=4,V>=2] * Chain [83,124,126]: 6 with precondition: [V1=2,Out=5,V>=2] * Chain [83,123,126]: 6 with precondition: [V1=2,Out=6,V>=2] * Chain [83,122,126]: 5 with precondition: [V1=2,Out=4,V>=2] * Chain [83,121,126]: 6 with precondition: [V1=2,Out=5,V>=2] * Chain [83,120,126]: 6 with precondition: [V1=2,Out=6,V>=2] * Chain [82,126]: 3 with precondition: [V1=2,Out=4,V>=2] * Chain [82,125,126]: 5 with precondition: [V1=2,Out=5,V>=2] * Chain [82,124,126]: 6 with precondition: [V1=2,Out=6,V>=2] * Chain [82,123,126]: 6 with precondition: [V1=2,Out=7,V>=2] * Chain [82,122,126]: 5 with precondition: [V1=2,Out=5,V>=2] * Chain [82,121,126]: 6 with precondition: [V1=2,Out=6,V>=2] * Chain [82,120,126]: 6 with precondition: [V1=2,Out=7,V>=2] * Chain [81,126]: 1*s(327)+3 Such that:s(327) =< 2*Out with precondition: [V1=2,V+9=2*Out,V>=3] * Chain [81,125,126]: 1*s(327)+5 Such that:s(327) =< 2*Out with precondition: [V1=2,V+11=2*Out,V>=3] * Chain [81,124,126]: 1*s(327)+6 Such that:s(327) =< 2*Out with precondition: [V1=2,V+13=2*Out,V>=3] * Chain [81,123,126]: 1*s(327)+6 Such that:s(327) =< 2*Out with precondition: [V1=2,V+15=2*Out,V>=3] * Chain [81,122,126]: 1*s(327)+5 Such that:s(327) =< 2*Out with precondition: [V1=2,V+11=2*Out,V>=3] * Chain [81,121,126]: 1*s(327)+6 Such that:s(327) =< 2*Out with precondition: [V1=2,V+13=2*Out,V>=3] * Chain [81,120,126]: 1*s(327)+6 Such that:s(327) =< 2*Out with precondition: [V1=2,V+15=2*Out,V>=3] * Chain [80,126]: 2*s(328)+1*s(330)+3 Such that:s(330) =< V aux(106) =< V+1 s(328) =< aux(106) with precondition: [V1=2,Out>=5,V+8>=2*Out] * Chain [80,125,126]: 2*s(328)+1*s(330)+5 Such that:s(330) =< V aux(106) =< V+1 s(328) =< aux(106) with precondition: [V1=2,Out>=6,V+10>=2*Out] * Chain [80,124,126]: 2*s(328)+1*s(330)+6 Such that:s(330) =< V aux(106) =< V+1 s(328) =< aux(106) with precondition: [V1=2,Out>=7,V+12>=2*Out] * Chain [80,123,126]: 2*s(328)+1*s(330)+6 Such that:s(330) =< V aux(106) =< V+1 s(328) =< aux(106) with precondition: [V1=2,Out>=8,V+14>=2*Out] * Chain [80,122,126]: 2*s(328)+1*s(330)+5 Such that:s(330) =< V aux(106) =< V+1 s(328) =< aux(106) with precondition: [V1=2,Out>=6,V+10>=2*Out] * Chain [80,121,126]: 2*s(328)+1*s(330)+6 Such that:s(330) =< V aux(106) =< V+1 s(328) =< aux(106) with precondition: [V1=2,Out>=7,V+12>=2*Out] * Chain [80,120,126]: 2*s(328)+1*s(330)+6 Such that:s(330) =< V aux(106) =< V+1 s(328) =< aux(106) with precondition: [V1=2,Out>=8,V+14>=2*Out] * Chain [79,126]: 6*s(331)+2 Such that:aux(114) =< 2*Out s(331) =< aux(114) with precondition: [V1=2,V+3=2*Out,V>=3] * Chain [79,125,126]: 6*s(331)+4 Such that:aux(114) =< 2*Out s(331) =< aux(114) with precondition: [V1=2,V+5=2*Out,V>=3] * Chain [79,124,126]: 6*s(331)+5 Such that:aux(114) =< 2*Out s(331) =< aux(114) with precondition: [V1=2,V+7=2*Out,V>=3] * Chain [79,123,126]: 6*s(331)+5 Such that:aux(114) =< 2*Out s(331) =< aux(114) with precondition: [V1=2,V+9=2*Out,V>=3] * Chain [79,122,126]: 6*s(331)+4 Such that:aux(114) =< 2*Out s(331) =< aux(114) with precondition: [V1=2,V+5=2*Out,V>=3] * Chain [79,121,126]: 6*s(331)+5 Such that:aux(114) =< 2*Out s(331) =< aux(114) with precondition: [V1=2,V+7=2*Out,V>=3] * Chain [79,120,126]: 6*s(331)+5 Such that:aux(114) =< 2*Out s(331) =< aux(114) with precondition: [V1=2,V+9=2*Out,V>=3] * Chain [78,126]: 6*s(337)+2 Such that:aux(122) =< V s(337) =< aux(122) with precondition: [V1=2,Out>=2,V+2>=2*Out] * Chain [78,125,126]: 6*s(337)+4 Such that:aux(122) =< V s(337) =< aux(122) with precondition: [V1=2,Out>=3,V+4>=2*Out] * Chain [78,124,126]: 6*s(337)+5 Such that:aux(122) =< V s(337) =< aux(122) with precondition: [V1=2,Out>=4,V+6>=2*Out] * Chain [78,123,126]: 6*s(337)+5 Such that:aux(122) =< V s(337) =< aux(122) with precondition: [V1=2,Out>=5,V+8>=2*Out] * Chain [78,122,126]: 6*s(337)+4 Such that:aux(122) =< V s(337) =< aux(122) with precondition: [V1=2,Out>=3,V+4>=2*Out] * Chain [78,121,126]: 6*s(337)+5 Such that:aux(122) =< V s(337) =< aux(122) with precondition: [V1=2,Out>=4,V+6>=2*Out] * Chain [78,120,126]: 6*s(337)+5 Such that:aux(122) =< V s(337) =< aux(122) with precondition: [V1=2,Out>=5,V+8>=2*Out] * Chain [77,126]: 2*s(343)+3 Such that:aux(130) =< V s(343) =< aux(130) with precondition: [V1=2,V>=3,Out>=4,V+6>=2*Out] * Chain [77,125,126]: 2*s(343)+5 Such that:aux(130) =< V s(343) =< aux(130) with precondition: [V1=2,V>=3,Out>=5,V+8>=2*Out] * Chain [77,124,126]: 2*s(343)+6 Such that:aux(130) =< V s(343) =< aux(130) with precondition: [V1=2,V>=3,Out>=6,V+10>=2*Out] * Chain [77,123,126]: 2*s(343)+6 Such that:aux(130) =< V s(343) =< aux(130) with precondition: [V1=2,V>=3,Out>=7,V+12>=2*Out] * Chain [77,122,126]: 2*s(343)+5 Such that:aux(130) =< V s(343) =< aux(130) with precondition: [V1=2,V>=3,Out>=5,V+8>=2*Out] * Chain [77,121,126]: 2*s(343)+6 Such that:aux(130) =< V s(343) =< aux(130) with precondition: [V1=2,V>=3,Out>=6,V+10>=2*Out] * Chain [77,120,126]: 2*s(343)+6 Such that:aux(130) =< V s(343) =< aux(130) with precondition: [V1=2,V>=3,Out>=7,V+12>=2*Out] #### Cost of chains of start(V1,V): * Chain [132]: 1*s(1649)+1*s(1650)+1 Such that:s(1650) =< V1 s(1649) =< V1+1 with precondition: [V1>=0] * Chain [131]: 2 with precondition: [V1=1] * Chain [130]: 1821*s(1660)+92*s(1661)+67*s(1665)+67*s(1667)+536*s(1669)+402*s(1670)+134*s(1671)+58*s(1672)+147*s(1673)+7*s(1675)+7*s(1677)+56*s(1679)+42*s(1680)+14*s(1681)+24*s(1682)+42*s(1683)+2*s(1685)+2*s(1687)+16*s(1689)+12*s(1690)+4*s(1691)+24*s(1692)+42*s(1693)+2*s(1695)+2*s(1697)+16*s(1699)+12*s(1700)+4*s(1701)+204*s(1702)+105*s(1703)+5*s(1705)+5*s(1707)+40*s(1709)+30*s(1710)+10*s(1711)+4*s(1712)+42*s(1713)+2*s(1715)+2*s(1717)+16*s(1719)+12*s(1720)+4*s(1721)+4*s(1722)+42*s(1723)+2*s(1725)+2*s(1727)+16*s(1729)+12*s(1730)+4*s(1731)+4*s(1732)+42*s(1733)+2*s(1735)+2*s(1737)+16*s(1739)+12*s(1740)+4*s(1741)+84*s(1742)+4*s(1744)+4*s(1746)+32*s(1748)+24*s(1749)+8*s(1750)+6 Such that:s(1651) =< V s(1652) =< V+1 aux(154) =< V+3 aux(155) =< V+5 aux(156) =< V+7 aux(157) =< V+9 aux(158) =< V+11 aux(159) =< V+13 aux(160) =< V+15 s(1660) =< s(1651) s(1661) =< s(1652) s(1662) =< s(1651)+1 s(1663) =< s(1651) s(1664) =< s(1660)*s(1651) s(1665) =< s(1660)*s(1662) s(1666) =< s(1660)*s(1662) s(1667) =< s(1660)*s(1663) s(1668) =< s(1660)*s(1663) s(1669) =< s(1666) s(1670) =< s(1668) s(1671) =< s(1664) s(1672) =< aux(157) s(1673) =< s(1651) s(1673) =< aux(157) s(1674) =< s(1673)*s(1651) s(1675) =< s(1673)*s(1662) s(1676) =< s(1673)*s(1662) s(1677) =< s(1673)*s(1663) s(1678) =< s(1673)*s(1663) s(1679) =< s(1676) s(1680) =< s(1678) s(1681) =< s(1674) s(1682) =< aux(156) s(1683) =< s(1651) s(1683) =< aux(156) s(1684) =< s(1683)*s(1651) s(1685) =< s(1683)*s(1662) s(1686) =< s(1683)*s(1662) s(1687) =< s(1683)*s(1663) s(1688) =< s(1683)*s(1663) s(1689) =< s(1686) s(1690) =< s(1688) s(1691) =< s(1684) s(1692) =< aux(155) s(1693) =< s(1651) s(1693) =< aux(155) s(1694) =< s(1693)*s(1651) s(1695) =< s(1693)*s(1662) s(1696) =< s(1693)*s(1662) s(1697) =< s(1693)*s(1663) s(1698) =< s(1693)*s(1663) s(1699) =< s(1696) s(1700) =< s(1698) s(1701) =< s(1694) s(1702) =< aux(154) s(1703) =< s(1651) s(1703) =< aux(154) s(1704) =< s(1703)*s(1651) s(1705) =< s(1703)*s(1662) s(1706) =< s(1703)*s(1662) s(1707) =< s(1703)*s(1663) s(1708) =< s(1703)*s(1663) s(1709) =< s(1706) s(1710) =< s(1708) s(1711) =< s(1704) s(1712) =< aux(160) s(1713) =< s(1651) s(1713) =< aux(160) s(1714) =< s(1713)*s(1651) s(1715) =< s(1713)*s(1662) s(1716) =< s(1713)*s(1662) s(1717) =< s(1713)*s(1663) s(1718) =< s(1713)*s(1663) s(1719) =< s(1716) s(1720) =< s(1718) s(1721) =< s(1714) s(1722) =< aux(159) s(1723) =< s(1651) s(1723) =< aux(159) s(1724) =< s(1723)*s(1651) s(1725) =< s(1723)*s(1662) s(1726) =< s(1723)*s(1662) s(1727) =< s(1723)*s(1663) s(1728) =< s(1723)*s(1663) s(1729) =< s(1726) s(1730) =< s(1728) s(1731) =< s(1724) s(1732) =< aux(158) s(1733) =< s(1651) s(1733) =< aux(158) s(1734) =< s(1733)*s(1651) s(1735) =< s(1733)*s(1662) s(1736) =< s(1733)*s(1662) s(1737) =< s(1733)*s(1663) s(1738) =< s(1733)*s(1663) s(1739) =< s(1736) s(1740) =< s(1738) s(1741) =< s(1734) s(1742) =< s(1651) s(1742) =< s(1652) s(1743) =< s(1742)*s(1651) s(1744) =< s(1742)*s(1662) s(1745) =< s(1742)*s(1662) s(1746) =< s(1742)*s(1663) s(1747) =< s(1742)*s(1663) s(1748) =< s(1745) s(1749) =< s(1747) s(1750) =< s(1743) with precondition: [V1=2,V>=0] * Chain [129]: 3 with precondition: [V=1,V1>=0] * Chain [128]: 2 with precondition: [V=2,V1>=1] * Chain [127]: 0 with precondition: [V=0,V1>=1] Closed-form bounds of start(V1,V): ------------------------------------- * Chain [132] with precondition: [V1>=0] - Upper bound: 2*V1+2 - Complexity: n * Chain [131] with precondition: [V1=1] - Upper bound: 2 - Complexity: constant * Chain [130] with precondition: [V1=2,V>=0] - Upper bound: 3204*V+6+1674*V*V+(92*V+92)+(204*V+612)+(24*V+120)+(24*V+168)+(58*V+522)+(4*V+44)+(4*V+52)+(4*V+60) - Complexity: n^2 * Chain [129] with precondition: [V=1,V1>=0] - Upper bound: 3 - Complexity: constant * Chain [128] with precondition: [V=2,V1>=1] - Upper bound: 2 - Complexity: constant * Chain [127] with precondition: [V=0,V1>=1] - Upper bound: 0 - Complexity: constant ### Maximum cost of start(V1,V): max([2*V1+2,3,nat(V)*3204+6+nat(V)*1674*nat(V)+nat(V+1)*92+nat(V+3)*204+nat(V+5)*24+nat(V+7)*24+nat(V+9)*58+nat(V+11)*4+nat(V+13)*4+nat(V+15)*4]) Asymptotic class: n^2 * Total analysis performed in 16998 ms. ---------------------------------------- (12) BOUNDS(1, n^2) ---------------------------------------- (13) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (14) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: COND(true, z0) -> c(COND(and(even(z0), gr(z0, 0')), p(z0)), AND(even(z0), gr(z0, 0')), EVEN(z0)) COND(true, z0) -> c1(COND(and(even(z0), gr(z0, 0')), p(z0)), AND(even(z0), gr(z0, 0')), GR(z0, 0')) COND(true, z0) -> c2(COND(and(even(z0), gr(z0, 0')), p(z0)), P(z0)) AND(z0, false) -> c3 AND(false, z0) -> c4 AND(true, true) -> c5 EVEN(0') -> c6 EVEN(s(0')) -> c7 EVEN(s(s(z0))) -> c8(EVEN(z0)) GR(0', z0) -> c9 GR(s(z0), 0') -> c10 GR(s(z0), s(y)) -> c11(GR(z0, y)) P(0') -> c12 P(s(z0)) -> c13 The (relative) TRS S consists of the following rules: cond(true, z0) -> cond(and(even(z0), gr(z0, 0')), p(z0)) and(z0, false) -> false and(false, z0) -> false and(true, true) -> true even(0') -> true even(s(0')) -> false even(s(s(z0))) -> even(z0) gr(0', z0) -> false gr(s(z0), 0') -> true gr(s(z0), s(y)) -> gr(z0, y) p(0') -> 0' p(s(z0)) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (15) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (16) Obligation: Innermost TRS: Rules: COND(true, z0) -> c(COND(and(even(z0), gr(z0, 0')), p(z0)), AND(even(z0), gr(z0, 0')), EVEN(z0)) COND(true, z0) -> c1(COND(and(even(z0), gr(z0, 0')), p(z0)), AND(even(z0), gr(z0, 0')), GR(z0, 0')) COND(true, z0) -> c2(COND(and(even(z0), gr(z0, 0')), p(z0)), P(z0)) AND(z0, false) -> c3 AND(false, z0) -> c4 AND(true, true) -> c5 EVEN(0') -> c6 EVEN(s(0')) -> c7 EVEN(s(s(z0))) -> c8(EVEN(z0)) GR(0', z0) -> c9 GR(s(z0), 0') -> c10 GR(s(z0), s(y)) -> c11(GR(z0, y)) P(0') -> c12 P(s(z0)) -> c13 cond(true, z0) -> cond(and(even(z0), gr(z0, 0')), p(z0)) and(z0, false) -> false and(false, z0) -> false and(true, true) -> true even(0') -> true even(s(0')) -> false even(s(s(z0))) -> even(z0) gr(0', z0) -> false gr(s(z0), 0') -> true gr(s(z0), s(y)) -> gr(z0, y) p(0') -> 0' p(s(z0)) -> z0 Types: COND :: true:false -> 0':s:y -> c:c1:c2 true :: true:false c :: c:c1:c2 -> c3:c4:c5 -> c6:c7:c8 -> c:c1:c2 and :: true:false -> true:false -> true:false even :: 0':s:y -> true:false gr :: 0':s:y -> 0':s:y -> true:false 0' :: 0':s:y p :: 0':s:y -> 0':s:y AND :: true:false -> true:false -> c3:c4:c5 EVEN :: 0':s:y -> c6:c7:c8 c1 :: c:c1:c2 -> c3:c4:c5 -> c9:c10:c11 -> c:c1:c2 GR :: 0':s:y -> 0':s:y -> c9:c10:c11 c2 :: c:c1:c2 -> c12:c13 -> c:c1:c2 P :: 0':s:y -> c12:c13 false :: true:false c3 :: c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 c6 :: c6:c7:c8 s :: 0':s:y -> 0':s:y c7 :: c6:c7:c8 c8 :: c6:c7:c8 -> c6:c7:c8 c9 :: c9:c10:c11 c10 :: c9:c10:c11 y :: 0':s:y c11 :: c9:c10:c11 -> c9:c10:c11 c12 :: c12:c13 c13 :: c12:c13 cond :: true:false -> 0':s:y -> cond hole_c:c1:c21_14 :: c:c1:c2 hole_true:false2_14 :: true:false hole_0':s:y3_14 :: 0':s:y hole_c3:c4:c54_14 :: c3:c4:c5 hole_c6:c7:c85_14 :: c6:c7:c8 hole_c9:c10:c116_14 :: c9:c10:c11 hole_c12:c137_14 :: c12:c13 hole_cond8_14 :: cond gen_c:c1:c29_14 :: Nat -> c:c1:c2 gen_0':s:y10_14 :: Nat -> 0':s:y gen_c6:c7:c811_14 :: Nat -> c6:c7:c8 gen_c9:c10:c1112_14 :: Nat -> c9:c10:c11 ---------------------------------------- (17) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: COND, even, gr, EVEN, GR, cond They will be analysed ascendingly in the following order: even < COND gr < COND EVEN < COND GR < COND even < cond gr < cond ---------------------------------------- (18) Obligation: Innermost TRS: Rules: COND(true, z0) -> c(COND(and(even(z0), gr(z0, 0')), p(z0)), AND(even(z0), gr(z0, 0')), EVEN(z0)) COND(true, z0) -> c1(COND(and(even(z0), gr(z0, 0')), p(z0)), AND(even(z0), gr(z0, 0')), GR(z0, 0')) COND(true, z0) -> c2(COND(and(even(z0), gr(z0, 0')), p(z0)), P(z0)) AND(z0, false) -> c3 AND(false, z0) -> c4 AND(true, true) -> c5 EVEN(0') -> c6 EVEN(s(0')) -> c7 EVEN(s(s(z0))) -> c8(EVEN(z0)) GR(0', z0) -> c9 GR(s(z0), 0') -> c10 GR(s(z0), s(y)) -> c11(GR(z0, y)) P(0') -> c12 P(s(z0)) -> c13 cond(true, z0) -> cond(and(even(z0), gr(z0, 0')), p(z0)) and(z0, false) -> false and(false, z0) -> false and(true, true) -> true even(0') -> true even(s(0')) -> false even(s(s(z0))) -> even(z0) gr(0', z0) -> false gr(s(z0), 0') -> true gr(s(z0), s(y)) -> gr(z0, y) p(0') -> 0' p(s(z0)) -> z0 Types: COND :: true:false -> 0':s:y -> c:c1:c2 true :: true:false c :: c:c1:c2 -> c3:c4:c5 -> c6:c7:c8 -> c:c1:c2 and :: true:false -> true:false -> true:false even :: 0':s:y -> true:false gr :: 0':s:y -> 0':s:y -> true:false 0' :: 0':s:y p :: 0':s:y -> 0':s:y AND :: true:false -> true:false -> c3:c4:c5 EVEN :: 0':s:y -> c6:c7:c8 c1 :: c:c1:c2 -> c3:c4:c5 -> c9:c10:c11 -> c:c1:c2 GR :: 0':s:y -> 0':s:y -> c9:c10:c11 c2 :: c:c1:c2 -> c12:c13 -> c:c1:c2 P :: 0':s:y -> c12:c13 false :: true:false c3 :: c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 c6 :: c6:c7:c8 s :: 0':s:y -> 0':s:y c7 :: c6:c7:c8 c8 :: c6:c7:c8 -> c6:c7:c8 c9 :: c9:c10:c11 c10 :: c9:c10:c11 y :: 0':s:y c11 :: c9:c10:c11 -> c9:c10:c11 c12 :: c12:c13 c13 :: c12:c13 cond :: true:false -> 0':s:y -> cond hole_c:c1:c21_14 :: c:c1:c2 hole_true:false2_14 :: true:false hole_0':s:y3_14 :: 0':s:y hole_c3:c4:c54_14 :: c3:c4:c5 hole_c6:c7:c85_14 :: c6:c7:c8 hole_c9:c10:c116_14 :: c9:c10:c11 hole_c12:c137_14 :: c12:c13 hole_cond8_14 :: cond gen_c:c1:c29_14 :: Nat -> c:c1:c2 gen_0':s:y10_14 :: Nat -> 0':s:y gen_c6:c7:c811_14 :: Nat -> c6:c7:c8 gen_c9:c10:c1112_14 :: Nat -> c9:c10:c11 Generator Equations: gen_c:c1:c29_14(0) <=> hole_c:c1:c21_14 gen_c:c1:c29_14(+(x, 1)) <=> c(gen_c:c1:c29_14(x), c3, c6) gen_0':s:y10_14(0) <=> 0' gen_0':s:y10_14(+(x, 1)) <=> s(gen_0':s:y10_14(x)) gen_c6:c7:c811_14(0) <=> c6 gen_c6:c7:c811_14(+(x, 1)) <=> c8(gen_c6:c7:c811_14(x)) gen_c9:c10:c1112_14(0) <=> c9 gen_c9:c10:c1112_14(+(x, 1)) <=> c11(gen_c9:c10:c1112_14(x)) The following defined symbols remain to be analysed: even, COND, gr, EVEN, GR, cond They will be analysed ascendingly in the following order: even < COND gr < COND EVEN < COND GR < COND even < cond gr < cond ---------------------------------------- (19) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: even(gen_0':s:y10_14(*(2, n14_14))) -> true, rt in Omega(0) Induction Base: even(gen_0':s:y10_14(*(2, 0))) ->_R^Omega(0) true Induction Step: even(gen_0':s:y10_14(*(2, +(n14_14, 1)))) ->_R^Omega(0) even(gen_0':s:y10_14(*(2, n14_14))) ->_IH true We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (20) Obligation: Innermost TRS: Rules: COND(true, z0) -> c(COND(and(even(z0), gr(z0, 0')), p(z0)), AND(even(z0), gr(z0, 0')), EVEN(z0)) COND(true, z0) -> c1(COND(and(even(z0), gr(z0, 0')), p(z0)), AND(even(z0), gr(z0, 0')), GR(z0, 0')) COND(true, z0) -> c2(COND(and(even(z0), gr(z0, 0')), p(z0)), P(z0)) AND(z0, false) -> c3 AND(false, z0) -> c4 AND(true, true) -> c5 EVEN(0') -> c6 EVEN(s(0')) -> c7 EVEN(s(s(z0))) -> c8(EVEN(z0)) GR(0', z0) -> c9 GR(s(z0), 0') -> c10 GR(s(z0), s(y)) -> c11(GR(z0, y)) P(0') -> c12 P(s(z0)) -> c13 cond(true, z0) -> cond(and(even(z0), gr(z0, 0')), p(z0)) and(z0, false) -> false and(false, z0) -> false and(true, true) -> true even(0') -> true even(s(0')) -> false even(s(s(z0))) -> even(z0) gr(0', z0) -> false gr(s(z0), 0') -> true gr(s(z0), s(y)) -> gr(z0, y) p(0') -> 0' p(s(z0)) -> z0 Types: COND :: true:false -> 0':s:y -> c:c1:c2 true :: true:false c :: c:c1:c2 -> c3:c4:c5 -> c6:c7:c8 -> c:c1:c2 and :: true:false -> true:false -> true:false even :: 0':s:y -> true:false gr :: 0':s:y -> 0':s:y -> true:false 0' :: 0':s:y p :: 0':s:y -> 0':s:y AND :: true:false -> true:false -> c3:c4:c5 EVEN :: 0':s:y -> c6:c7:c8 c1 :: c:c1:c2 -> c3:c4:c5 -> c9:c10:c11 -> c:c1:c2 GR :: 0':s:y -> 0':s:y -> c9:c10:c11 c2 :: c:c1:c2 -> c12:c13 -> c:c1:c2 P :: 0':s:y -> c12:c13 false :: true:false c3 :: c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 c6 :: c6:c7:c8 s :: 0':s:y -> 0':s:y c7 :: c6:c7:c8 c8 :: c6:c7:c8 -> c6:c7:c8 c9 :: c9:c10:c11 c10 :: c9:c10:c11 y :: 0':s:y c11 :: c9:c10:c11 -> c9:c10:c11 c12 :: c12:c13 c13 :: c12:c13 cond :: true:false -> 0':s:y -> cond hole_c:c1:c21_14 :: c:c1:c2 hole_true:false2_14 :: true:false hole_0':s:y3_14 :: 0':s:y hole_c3:c4:c54_14 :: c3:c4:c5 hole_c6:c7:c85_14 :: c6:c7:c8 hole_c9:c10:c116_14 :: c9:c10:c11 hole_c12:c137_14 :: c12:c13 hole_cond8_14 :: cond gen_c:c1:c29_14 :: Nat -> c:c1:c2 gen_0':s:y10_14 :: Nat -> 0':s:y gen_c6:c7:c811_14 :: Nat -> c6:c7:c8 gen_c9:c10:c1112_14 :: Nat -> c9:c10:c11 Lemmas: even(gen_0':s:y10_14(*(2, n14_14))) -> true, rt in Omega(0) Generator Equations: gen_c:c1:c29_14(0) <=> hole_c:c1:c21_14 gen_c:c1:c29_14(+(x, 1)) <=> c(gen_c:c1:c29_14(x), c3, c6) gen_0':s:y10_14(0) <=> 0' gen_0':s:y10_14(+(x, 1)) <=> s(gen_0':s:y10_14(x)) gen_c6:c7:c811_14(0) <=> c6 gen_c6:c7:c811_14(+(x, 1)) <=> c8(gen_c6:c7:c811_14(x)) gen_c9:c10:c1112_14(0) <=> c9 gen_c9:c10:c1112_14(+(x, 1)) <=> c11(gen_c9:c10:c1112_14(x)) The following defined symbols remain to be analysed: gr, COND, EVEN, GR, cond They will be analysed ascendingly in the following order: gr < COND EVEN < COND GR < COND gr < cond ---------------------------------------- (21) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: EVEN(gen_0':s:y10_14(*(2, n231_14))) -> gen_c6:c7:c811_14(n231_14), rt in Omega(1 + n231_14) Induction Base: EVEN(gen_0':s:y10_14(*(2, 0))) ->_R^Omega(1) c6 Induction Step: EVEN(gen_0':s:y10_14(*(2, +(n231_14, 1)))) ->_R^Omega(1) c8(EVEN(gen_0':s:y10_14(*(2, n231_14)))) ->_IH c8(gen_c6:c7:c811_14(c232_14)) 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: COND(true, z0) -> c(COND(and(even(z0), gr(z0, 0')), p(z0)), AND(even(z0), gr(z0, 0')), EVEN(z0)) COND(true, z0) -> c1(COND(and(even(z0), gr(z0, 0')), p(z0)), AND(even(z0), gr(z0, 0')), GR(z0, 0')) COND(true, z0) -> c2(COND(and(even(z0), gr(z0, 0')), p(z0)), P(z0)) AND(z0, false) -> c3 AND(false, z0) -> c4 AND(true, true) -> c5 EVEN(0') -> c6 EVEN(s(0')) -> c7 EVEN(s(s(z0))) -> c8(EVEN(z0)) GR(0', z0) -> c9 GR(s(z0), 0') -> c10 GR(s(z0), s(y)) -> c11(GR(z0, y)) P(0') -> c12 P(s(z0)) -> c13 cond(true, z0) -> cond(and(even(z0), gr(z0, 0')), p(z0)) and(z0, false) -> false and(false, z0) -> false and(true, true) -> true even(0') -> true even(s(0')) -> false even(s(s(z0))) -> even(z0) gr(0', z0) -> false gr(s(z0), 0') -> true gr(s(z0), s(y)) -> gr(z0, y) p(0') -> 0' p(s(z0)) -> z0 Types: COND :: true:false -> 0':s:y -> c:c1:c2 true :: true:false c :: c:c1:c2 -> c3:c4:c5 -> c6:c7:c8 -> c:c1:c2 and :: true:false -> true:false -> true:false even :: 0':s:y -> true:false gr :: 0':s:y -> 0':s:y -> true:false 0' :: 0':s:y p :: 0':s:y -> 0':s:y AND :: true:false -> true:false -> c3:c4:c5 EVEN :: 0':s:y -> c6:c7:c8 c1 :: c:c1:c2 -> c3:c4:c5 -> c9:c10:c11 -> c:c1:c2 GR :: 0':s:y -> 0':s:y -> c9:c10:c11 c2 :: c:c1:c2 -> c12:c13 -> c:c1:c2 P :: 0':s:y -> c12:c13 false :: true:false c3 :: c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 c6 :: c6:c7:c8 s :: 0':s:y -> 0':s:y c7 :: c6:c7:c8 c8 :: c6:c7:c8 -> c6:c7:c8 c9 :: c9:c10:c11 c10 :: c9:c10:c11 y :: 0':s:y c11 :: c9:c10:c11 -> c9:c10:c11 c12 :: c12:c13 c13 :: c12:c13 cond :: true:false -> 0':s:y -> cond hole_c:c1:c21_14 :: c:c1:c2 hole_true:false2_14 :: true:false hole_0':s:y3_14 :: 0':s:y hole_c3:c4:c54_14 :: c3:c4:c5 hole_c6:c7:c85_14 :: c6:c7:c8 hole_c9:c10:c116_14 :: c9:c10:c11 hole_c12:c137_14 :: c12:c13 hole_cond8_14 :: cond gen_c:c1:c29_14 :: Nat -> c:c1:c2 gen_0':s:y10_14 :: Nat -> 0':s:y gen_c6:c7:c811_14 :: Nat -> c6:c7:c8 gen_c9:c10:c1112_14 :: Nat -> c9:c10:c11 Lemmas: even(gen_0':s:y10_14(*(2, n14_14))) -> true, rt in Omega(0) Generator Equations: gen_c:c1:c29_14(0) <=> hole_c:c1:c21_14 gen_c:c1:c29_14(+(x, 1)) <=> c(gen_c:c1:c29_14(x), c3, c6) gen_0':s:y10_14(0) <=> 0' gen_0':s:y10_14(+(x, 1)) <=> s(gen_0':s:y10_14(x)) gen_c6:c7:c811_14(0) <=> c6 gen_c6:c7:c811_14(+(x, 1)) <=> c8(gen_c6:c7:c811_14(x)) gen_c9:c10:c1112_14(0) <=> c9 gen_c9:c10:c1112_14(+(x, 1)) <=> c11(gen_c9:c10:c1112_14(x)) The following defined symbols remain to be analysed: EVEN, COND, GR, cond They will be analysed ascendingly in the following order: EVEN < COND GR < COND ---------------------------------------- (24) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (25) BOUNDS(n^1, INF) ---------------------------------------- (26) Obligation: Innermost TRS: Rules: COND(true, z0) -> c(COND(and(even(z0), gr(z0, 0')), p(z0)), AND(even(z0), gr(z0, 0')), EVEN(z0)) COND(true, z0) -> c1(COND(and(even(z0), gr(z0, 0')), p(z0)), AND(even(z0), gr(z0, 0')), GR(z0, 0')) COND(true, z0) -> c2(COND(and(even(z0), gr(z0, 0')), p(z0)), P(z0)) AND(z0, false) -> c3 AND(false, z0) -> c4 AND(true, true) -> c5 EVEN(0') -> c6 EVEN(s(0')) -> c7 EVEN(s(s(z0))) -> c8(EVEN(z0)) GR(0', z0) -> c9 GR(s(z0), 0') -> c10 GR(s(z0), s(y)) -> c11(GR(z0, y)) P(0') -> c12 P(s(z0)) -> c13 cond(true, z0) -> cond(and(even(z0), gr(z0, 0')), p(z0)) and(z0, false) -> false and(false, z0) -> false and(true, true) -> true even(0') -> true even(s(0')) -> false even(s(s(z0))) -> even(z0) gr(0', z0) -> false gr(s(z0), 0') -> true gr(s(z0), s(y)) -> gr(z0, y) p(0') -> 0' p(s(z0)) -> z0 Types: COND :: true:false -> 0':s:y -> c:c1:c2 true :: true:false c :: c:c1:c2 -> c3:c4:c5 -> c6:c7:c8 -> c:c1:c2 and :: true:false -> true:false -> true:false even :: 0':s:y -> true:false gr :: 0':s:y -> 0':s:y -> true:false 0' :: 0':s:y p :: 0':s:y -> 0':s:y AND :: true:false -> true:false -> c3:c4:c5 EVEN :: 0':s:y -> c6:c7:c8 c1 :: c:c1:c2 -> c3:c4:c5 -> c9:c10:c11 -> c:c1:c2 GR :: 0':s:y -> 0':s:y -> c9:c10:c11 c2 :: c:c1:c2 -> c12:c13 -> c:c1:c2 P :: 0':s:y -> c12:c13 false :: true:false c3 :: c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 c6 :: c6:c7:c8 s :: 0':s:y -> 0':s:y c7 :: c6:c7:c8 c8 :: c6:c7:c8 -> c6:c7:c8 c9 :: c9:c10:c11 c10 :: c9:c10:c11 y :: 0':s:y c11 :: c9:c10:c11 -> c9:c10:c11 c12 :: c12:c13 c13 :: c12:c13 cond :: true:false -> 0':s:y -> cond hole_c:c1:c21_14 :: c:c1:c2 hole_true:false2_14 :: true:false hole_0':s:y3_14 :: 0':s:y hole_c3:c4:c54_14 :: c3:c4:c5 hole_c6:c7:c85_14 :: c6:c7:c8 hole_c9:c10:c116_14 :: c9:c10:c11 hole_c12:c137_14 :: c12:c13 hole_cond8_14 :: cond gen_c:c1:c29_14 :: Nat -> c:c1:c2 gen_0':s:y10_14 :: Nat -> 0':s:y gen_c6:c7:c811_14 :: Nat -> c6:c7:c8 gen_c9:c10:c1112_14 :: Nat -> c9:c10:c11 Lemmas: even(gen_0':s:y10_14(*(2, n14_14))) -> true, rt in Omega(0) EVEN(gen_0':s:y10_14(*(2, n231_14))) -> gen_c6:c7:c811_14(n231_14), rt in Omega(1 + n231_14) Generator Equations: gen_c:c1:c29_14(0) <=> hole_c:c1:c21_14 gen_c:c1:c29_14(+(x, 1)) <=> c(gen_c:c1:c29_14(x), c3, c6) gen_0':s:y10_14(0) <=> 0' gen_0':s:y10_14(+(x, 1)) <=> s(gen_0':s:y10_14(x)) gen_c6:c7:c811_14(0) <=> c6 gen_c6:c7:c811_14(+(x, 1)) <=> c8(gen_c6:c7:c811_14(x)) gen_c9:c10:c1112_14(0) <=> c9 gen_c9:c10:c1112_14(+(x, 1)) <=> c11(gen_c9:c10:c1112_14(x)) The following defined symbols remain to be analysed: GR, COND, cond They will be analysed ascendingly in the following order: GR < COND