WORST_CASE(Omega(n^1),O(n^2)) proof of /export/starexec/sandbox/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), 532 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, 5573 ms] (12) BOUNDS(1, n^2) (13) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (14) CpxRelTRS (15) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (16) typed CpxTrs (17) OrderProof [LOWER BOUND(ID), 16 ms] (18) typed CpxTrs (19) RewriteLemmaProof [LOWER BOUND(ID), 283 ms] (20) typed CpxTrs (21) RewriteLemmaProof [LOWER BOUND(ID), 124 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, z1) -> c(COND(gr(z0, z1), p(z0), s(z1)), GR(z0, z1)) COND(true, z0, z1) -> c1(COND(gr(z0, z1), p(z0), s(z1)), P(z0)) GR(0, z0) -> c2 GR(s(z0), 0) -> c3 GR(s(z0), s(z1)) -> c4(GR(z0, z1)) P(0) -> c5 P(s(z0)) -> c6 The (relative) TRS S consists of the following rules: cond(true, z0, z1) -> cond(gr(z0, z1), p(z0), s(z1)) gr(0, z0) -> false gr(s(z0), 0) -> true gr(s(z0), s(z1)) -> gr(z0, z1) 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, z1) -> c(COND(gr(z0, z1), p(z0), s(z1)), GR(z0, z1)) COND(true, z0, z1) -> c1(COND(gr(z0, z1), p(z0), s(z1)), P(z0)) GR(0, z0) -> c2 GR(s(z0), 0) -> c3 GR(s(z0), s(z1)) -> c4(GR(z0, z1)) P(0) -> c5 P(s(z0)) -> c6 The (relative) TRS S consists of the following rules: cond(true, z0, z1) -> cond(gr(z0, z1), p(z0), s(z1)) gr(0, z0) -> false gr(s(z0), 0) -> true gr(s(z0), s(z1)) -> gr(z0, z1) 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, z1) -> c(COND(gr(z0, z1), p(z0), s(z1)), GR(z0, z1)) [1] COND(true, z0, z1) -> c1(COND(gr(z0, z1), p(z0), s(z1)), P(z0)) [1] GR(0, z0) -> c2 [1] GR(s(z0), 0) -> c3 [1] GR(s(z0), s(z1)) -> c4(GR(z0, z1)) [1] P(0) -> c5 [1] P(s(z0)) -> c6 [1] cond(true, z0, z1) -> cond(gr(z0, z1), p(z0), s(z1)) [0] gr(0, z0) -> false [0] gr(s(z0), 0) -> true [0] gr(s(z0), s(z1)) -> gr(z0, z1) [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, z1) -> c(COND(gr(z0, z1), p(z0), s(z1)), GR(z0, z1)) [1] COND(true, z0, z1) -> c1(COND(gr(z0, z1), p(z0), s(z1)), P(z0)) [1] GR(0, z0) -> c2 [1] GR(s(z0), 0) -> c3 [1] GR(s(z0), s(z1)) -> c4(GR(z0, z1)) [1] P(0) -> c5 [1] P(s(z0)) -> c6 [1] cond(true, z0, z1) -> cond(gr(z0, z1), p(z0), s(z1)) [0] gr(0, z0) -> false [0] gr(s(z0), 0) -> true [0] gr(s(z0), s(z1)) -> gr(z0, z1) [0] p(0) -> 0 [0] p(s(z0)) -> z0 [0] The TRS has the following type information: COND :: true:false -> s:0 -> s:0 -> c:c1 true :: true:false c :: c:c1 -> c2:c3:c4 -> c:c1 gr :: s:0 -> s:0 -> true:false p :: s:0 -> s:0 s :: s:0 -> s:0 GR :: s:0 -> s:0 -> c2:c3:c4 c1 :: c:c1 -> c5:c6 -> c:c1 P :: s:0 -> c5:c6 0 :: s:0 c2 :: c2:c3:c4 c3 :: c2:c3:c4 c4 :: c2:c3:c4 -> c2:c3:c4 c5 :: c5:c6 c6 :: c5:c6 cond :: true:false -> s:0 -> s:0 -> cond false :: true:false 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, v2) -> null_cond [0] gr(v0, v1) -> null_gr [0] p(v0) -> null_p [0] COND(v0, v1, v2) -> null_COND [0] GR(v0, v1) -> null_GR [0] P(v0) -> null_P [0] And the following fresh constants: null_cond, null_gr, null_p, null_COND, 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, z1) -> c(COND(gr(z0, z1), p(z0), s(z1)), GR(z0, z1)) [1] COND(true, z0, z1) -> c1(COND(gr(z0, z1), p(z0), s(z1)), P(z0)) [1] GR(0, z0) -> c2 [1] GR(s(z0), 0) -> c3 [1] GR(s(z0), s(z1)) -> c4(GR(z0, z1)) [1] P(0) -> c5 [1] P(s(z0)) -> c6 [1] cond(true, z0, z1) -> cond(gr(z0, z1), p(z0), s(z1)) [0] gr(0, z0) -> false [0] gr(s(z0), 0) -> true [0] gr(s(z0), s(z1)) -> gr(z0, z1) [0] p(0) -> 0 [0] p(s(z0)) -> z0 [0] cond(v0, v1, v2) -> null_cond [0] gr(v0, v1) -> null_gr [0] p(v0) -> null_p [0] COND(v0, v1, v2) -> null_COND [0] GR(v0, v1) -> null_GR [0] P(v0) -> null_P [0] The TRS has the following type information: COND :: true:false:null_gr -> s:0:null_p -> s:0:null_p -> c:c1:null_COND true :: true:false:null_gr c :: c:c1:null_COND -> c2:c3:c4:null_GR -> c:c1:null_COND gr :: s:0:null_p -> s:0:null_p -> true:false:null_gr p :: s:0:null_p -> s:0:null_p s :: s:0:null_p -> s:0:null_p GR :: s:0:null_p -> s:0:null_p -> c2:c3:c4:null_GR c1 :: c:c1:null_COND -> c5:c6:null_P -> c:c1:null_COND P :: s:0:null_p -> c5:c6:null_P 0 :: s:0:null_p c2 :: c2:c3:c4:null_GR c3 :: c2:c3:c4:null_GR c4 :: c2:c3:c4:null_GR -> c2:c3:c4:null_GR c5 :: c5:c6:null_P c6 :: c5:c6:null_P cond :: true:false:null_gr -> s:0:null_p -> s:0:null_p -> null_cond false :: true:false:null_gr null_cond :: null_cond null_gr :: true:false:null_gr null_p :: s:0:null_p null_COND :: c:c1:null_COND null_GR :: c2:c3:c4:null_GR null_P :: c5:c6: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 c2 => 0 c3 => 1 c5 => 1 c6 => 2 false => 1 null_cond => 0 null_gr => 0 null_p => 0 null_COND => 0 null_GR => 0 null_P => 0 ---------------------------------------- (10) Obligation: Complexity RNTS consisting of the following rules: COND(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0 COND(z, z', z'') -{ 1 }-> 1 + COND(gr(z0, z1), p(z0), 1 + z1) + P(z0) :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1 COND(z, z', z'') -{ 1 }-> 1 + COND(gr(z0, z1), p(z0), 1 + z1) + GR(z0, z1) :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1 GR(z, z') -{ 1 }-> 1 :|: z = 1 + z0, z0 >= 0, z' = 0 GR(z, z') -{ 1 }-> 0 :|: z0 >= 0, z = 0, z' = z0 GR(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 GR(z, z') -{ 1 }-> 1 + GR(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1 P(z) -{ 1 }-> 2 :|: z = 1 + z0, z0 >= 0 P(z) -{ 1 }-> 1 :|: z = 0 P(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 cond(z, z', z'') -{ 0 }-> cond(gr(z0, z1), p(z0), 1 + z1) :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1 cond(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0 gr(z, z') -{ 0 }-> gr(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1 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, V2),0,[fun(V1, V, V2, Out)],[V1 >= 0,V >= 0,V2 >= 0]). eq(start(V1, V, V2),0,[fun1(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V2),0,[fun2(V1, Out)],[V1 >= 0]). eq(start(V1, V, V2),0,[cond(V1, V, V2, Out)],[V1 >= 0,V >= 0,V2 >= 0]). eq(start(V1, V, V2),0,[gr(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V2),0,[p(V1, Out)],[V1 >= 0]). eq(fun(V1, V, V2, Out),1,[gr(V4, V3, Ret010),p(V4, Ret011),fun(Ret010, Ret011, 1 + V3, Ret01),fun1(V4, V3, Ret1)],[Out = 1 + Ret01 + Ret1,V1 = 2,V3 >= 0,V4 >= 0,V = V4,V2 = V3]). eq(fun(V1, V, V2, Out),1,[gr(V6, V5, Ret0101),p(V6, Ret0111),fun(Ret0101, Ret0111, 1 + V5, Ret012),fun2(V6, Ret11)],[Out = 1 + Ret012 + Ret11,V1 = 2,V5 >= 0,V6 >= 0,V = V6,V2 = V5]). eq(fun1(V1, V, Out),1,[],[Out = 0,V7 >= 0,V1 = 0,V = V7]). eq(fun1(V1, V, Out),1,[],[Out = 1,V1 = 1 + V8,V8 >= 0,V = 0]). eq(fun1(V1, V, Out),1,[fun1(V9, V10, Ret12)],[Out = 1 + Ret12,V10 >= 0,V1 = 1 + V9,V9 >= 0,V = 1 + V10]). eq(fun2(V1, Out),1,[],[Out = 1,V1 = 0]). eq(fun2(V1, Out),1,[],[Out = 2,V1 = 1 + V11,V11 >= 0]). eq(cond(V1, V, V2, Out),0,[gr(V12, V13, Ret0),p(V12, Ret13),cond(Ret0, Ret13, 1 + V13, Ret)],[Out = Ret,V1 = 2,V13 >= 0,V12 >= 0,V = V12,V2 = V13]). eq(gr(V1, V, Out),0,[],[Out = 1,V14 >= 0,V1 = 0,V = V14]). eq(gr(V1, V, Out),0,[],[Out = 2,V1 = 1 + V15,V15 >= 0,V = 0]). eq(gr(V1, V, Out),0,[gr(V17, V16, Ret2)],[Out = Ret2,V16 >= 0,V1 = 1 + V17,V17 >= 0,V = 1 + V16]). eq(p(V1, Out),0,[],[Out = 0,V1 = 0]). eq(p(V1, Out),0,[],[Out = V18,V1 = 1 + V18,V18 >= 0]). eq(cond(V1, V, V2, Out),0,[],[Out = 0,V20 >= 0,V2 = V21,V19 >= 0,V1 = V20,V = V19,V21 >= 0]). eq(gr(V1, V, Out),0,[],[Out = 0,V23 >= 0,V22 >= 0,V1 = V23,V = V22]). eq(p(V1, Out),0,[],[Out = 0,V24 >= 0,V1 = V24]). eq(fun(V1, V, V2, Out),0,[],[Out = 0,V25 >= 0,V2 = V26,V27 >= 0,V1 = V25,V = V27,V26 >= 0]). eq(fun1(V1, V, Out),0,[],[Out = 0,V28 >= 0,V29 >= 0,V1 = V28,V = V29]). eq(fun2(V1, Out),0,[],[Out = 0,V30 >= 0,V1 = V30]). input_output_vars(fun(V1,V,V2,Out),[V1,V,V2],[Out]). input_output_vars(fun1(V1,V,Out),[V1,V],[Out]). input_output_vars(fun2(V1,Out),[V1],[Out]). input_output_vars(cond(V1,V,V2,Out),[V1,V,V2],[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. recursive : [gr/3] 1. non_recursive : [p/2] 2. recursive : [cond/4] 3. recursive : [fun1/3] 4. non_recursive : [fun2/2] 5. recursive [non_tail] : [fun/4] 6. non_recursive : [start/3] #### Obtained direct recursion through partial evaluation 0. SCC is partially evaluated into gr/3 1. SCC is partially evaluated into p/2 2. SCC is partially evaluated into cond/4 3. SCC is partially evaluated into fun1/3 4. SCC is partially evaluated into fun2/2 5. SCC is partially evaluated into fun/4 6. SCC is partially evaluated into start/3 Control-Flow Refinement of Cost Relations ===================================== ### Specialization of cost equations gr/3 * CE 22 is refined into CE [25] * CE 20 is refined into CE [26] * CE 19 is refined into CE [27] * CE 21 is refined into CE [28] ### Cost equations --> "Loop" of gr/3 * CEs [28] --> Loop 18 * CEs [25] --> Loop 19 * CEs [26] --> Loop 20 * CEs [27] --> Loop 21 ### Ranking functions of CR gr(V1,V,Out) * RF of phase [18]: [V,V1] #### Partial ranking functions of CR gr(V1,V,Out) * Partial RF of phase [18]: - RF of loop [18:1]: V V1 ### Specialization of cost equations p/2 * CE 24 is refined into CE [29] * CE 23 is refined into CE [30] ### Cost equations --> "Loop" of p/2 * CEs [29] --> Loop 22 * CEs [30] --> Loop 23 ### Ranking functions of CR p(V1,Out) #### Partial ranking functions of CR p(V1,Out) ### Specialization of cost equations cond/4 * CE 18 is refined into CE [31] * CE 17 is refined into CE [32,33,34,35,36,37,38,39,40] ### Cost equations --> "Loop" of cond/4 * CEs [40] --> Loop 24 * CEs [39] --> Loop 25 * CEs [38] --> Loop 26 * CEs [37] --> Loop 27 * CEs [36] --> Loop 28 * CEs [35] --> Loop 29 * CEs [34] --> Loop 30 * CEs [33] --> Loop 31 * CEs [32] --> Loop 32 * CEs [31] --> Loop 33 ### Ranking functions of CR cond(V1,V,V2,Out) * RF of phase [24]: [V-1,V/2-V2/2] #### Partial ranking functions of CR cond(V1,V,V2,Out) * Partial RF of phase [24]: - RF of loop [24:1]: V-1 V/2-V2/2 ### Specialization of cost equations fun1/3 * CE 11 is refined into CE [41] * CE 10 is refined into CE [42] * CE 13 is refined into CE [43] * CE 12 is refined into CE [44] ### Cost equations --> "Loop" of fun1/3 * CEs [44] --> Loop 34 * CEs [41] --> Loop 35 * CEs [42,43] --> Loop 36 ### Ranking functions of CR fun1(V1,V,Out) * RF of phase [34]: [V,V1] #### Partial ranking functions of CR fun1(V1,V,Out) * Partial RF of phase [34]: - RF of loop [34:1]: V V1 ### Specialization of cost equations fun2/2 * CE 15 is refined into CE [45] * CE 16 is refined into CE [46] * CE 14 is refined into CE [47] ### Cost equations --> "Loop" of fun2/2 * CEs [45] --> Loop 37 * CEs [46] --> Loop 38 * CEs [47] --> Loop 39 ### Ranking functions of CR fun2(V1,Out) #### Partial ranking functions of CR fun2(V1,Out) ### Specialization of cost equations fun/4 * CE 9 is refined into CE [48] * CE 7 is refined into CE [49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71] * CE 8 is refined into CE [72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90] ### Cost equations --> "Loop" of fun/4 * CEs [71] --> Loop 40 * CEs [70] --> Loop 41 * CEs [90] --> Loop 42 * CEs [69,89] --> Loop 43 * CEs [88] --> Loop 44 * CEs [66,87] --> Loop 45 * CEs [68] --> Loop 46 * CEs [67] --> Loop 47 * CEs [65] --> Loop 48 * CEs [86] --> Loop 49 * CEs [64,85] --> Loop 50 * CEs [63] --> Loop 51 * CEs [84] --> Loop 52 * CEs [62,83] --> Loop 53 * CEs [61] --> Loop 54 * CEs [60] --> Loop 55 * CEs [82] --> Loop 56 * CEs [59,81] --> Loop 57 * CEs [57] --> Loop 58 * CEs [80] --> Loop 59 * CEs [55,79] --> Loop 60 * CEs [56] --> Loop 61 * CEs [77] --> Loop 62 * CEs [52] --> Loop 63 * CEs [53,76] --> Loop 64 * CEs [75] --> Loop 65 * CEs [50] --> Loop 66 * CEs [51,74] --> Loop 67 * CEs [58] --> Loop 68 * CEs [54] --> Loop 69 * CEs [72] --> Loop 70 * CEs [49,73] --> Loop 71 * CEs [78] --> Loop 72 * CEs [48] --> Loop 73 ### Ranking functions of CR fun(V1,V,V2,Out) * RF of phase [40,41,42,43]: [V-1,V/2-V2/2] #### Partial ranking functions of CR fun(V1,V,V2,Out) * Partial RF of phase [40,41,42,43]: - RF of loop [40:1,41:1,42:1,43:1]: V-1 V/2-V2/2 ### Specialization of cost equations start/3 * CE 1 is refined into CE [91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112] * CE 2 is refined into CE [113,114,115,116] * CE 3 is refined into CE [117,118,119] * CE 4 is refined into CE [120,121,122] * CE 5 is refined into CE [123,124,125,126,127] * CE 6 is refined into CE [128,129] ### Cost equations --> "Loop" of start/3 * CEs [113,124] --> Loop 74 * CEs [93,95,96,97,98,99,100,101,102,103,104,121,122] --> Loop 75 * CEs [91,92,94,105,106,107,108,109,110,111] --> Loop 76 * CEs [112,114,115,116,117,118,119,120,123,125,126,127,128,129] --> Loop 77 ### Ranking functions of CR start(V1,V,V2) #### Partial ranking functions of CR start(V1,V,V2) Computing Bounds ===================================== #### Cost of chains of gr(V1,V,Out): * Chain [[18],21]: 0 with precondition: [Out=1,V1>=1,V>=V1] * Chain [[18],20]: 0 with precondition: [Out=2,V>=1,V1>=V+1] * Chain [[18],19]: 0 with precondition: [Out=0,V1>=1,V>=1] * Chain [21]: 0 with precondition: [V1=0,Out=1,V>=0] * Chain [20]: 0 with precondition: [V=0,Out=2,V1>=1] * Chain [19]: 0 with precondition: [Out=0,V1>=0,V>=0] #### Cost of chains of p(V1,Out): * Chain [23]: 0 with precondition: [Out=0,V1>=0] * Chain [22]: 0 with precondition: [V1=Out+1,V1>=1] #### Cost of chains of cond(V1,V,V2,Out): * Chain [[24],33]: 0 with precondition: [V1=2,Out=0,V2>=1,V>=V2+1] * Chain [[24],29,33]: 0 with precondition: [V1=2,Out=0,V2>=1,V>=V2+1] * Chain [[24],28,33]: 0 with precondition: [V1=2,Out=0,V2>=1,V>=V2+1] * Chain [[24],27,33]: 0 with precondition: [V1=2,Out=0,V2>=1,V>=V2+1] * Chain [[24],26,33]: 0 with precondition: [V1=2,Out=0,V2>=1,V>=V2+1] * Chain [[24],25,33]: 0 with precondition: [V1=2,Out=0,V2>=1,V>=V2+3] * Chain [[24],25,32,33]: 0 with precondition: [V1=2,Out=0,V2>=1,V>=V2+3] * Chain [[24],25,29,33]: 0 with precondition: [V1=2,Out=0,V2>=1,V>=V2+3] * Chain [33]: 0 with precondition: [Out=0,V1>=0,V>=0,V2>=0] * Chain [32,33]: 0 with precondition: [V1=2,V=0,Out=0,V2>=0] * Chain [31,33]: 0 with precondition: [V1=2,V2=0,Out=0,V>=1] * Chain [31,32,33]: 0 with precondition: [V1=2,V2=0,Out=0,V>=1] * Chain [31,29,33]: 0 with precondition: [V1=2,V2=0,Out=0,V>=1] * Chain [30,[24],33]: 0 with precondition: [V1=2,V2=0,Out=0,V>=3] * Chain [30,[24],29,33]: 0 with precondition: [V1=2,V2=0,Out=0,V>=3] * Chain [30,[24],28,33]: 0 with precondition: [V1=2,V2=0,Out=0,V>=3] * Chain [30,[24],27,33]: 0 with precondition: [V1=2,V2=0,Out=0,V>=3] * Chain [30,[24],26,33]: 0 with precondition: [V1=2,V2=0,Out=0,V>=3] * Chain [30,[24],25,33]: 0 with precondition: [V1=2,V2=0,Out=0,V>=5] * Chain [30,[24],25,32,33]: 0 with precondition: [V1=2,V2=0,Out=0,V>=5] * Chain [30,[24],25,29,33]: 0 with precondition: [V1=2,V2=0,Out=0,V>=5] * Chain [30,33]: 0 with precondition: [V1=2,V2=0,Out=0,V>=1] * Chain [30,32,33]: 0 with precondition: [V1=2,V=1,V2=0,Out=0] * Chain [30,29,33]: 0 with precondition: [V1=2,V2=0,Out=0,V>=1] * Chain [30,28,33]: 0 with precondition: [V1=2,V2=0,Out=0,V>=2] * Chain [30,27,33]: 0 with precondition: [V1=2,V=2,V2=0,Out=0] * Chain [30,26,33]: 0 with precondition: [V1=2,V=2,V2=0,Out=0] * Chain [30,25,33]: 0 with precondition: [V1=2,V2=0,Out=0,V>=3] * Chain [30,25,32,33]: 0 with precondition: [V1=2,V2=0,Out=0,V>=3] * Chain [30,25,29,33]: 0 with precondition: [V1=2,V2=0,Out=0,V>=3] * Chain [29,33]: 0 with precondition: [V1=2,Out=0,V>=0,V2>=0] * Chain [28,33]: 0 with precondition: [V1=2,Out=0,V>=1,V2>=0] * Chain [27,33]: 0 with precondition: [V1=2,Out=0,V>=1,V2>=V] * Chain [26,33]: 0 with precondition: [V1=2,Out=0,V>=1,V2>=V] * Chain [25,33]: 0 with precondition: [V1=2,Out=0,V2>=1,V>=V2+1] * Chain [25,32,33]: 0 with precondition: [V1=2,Out=0,V2>=1,V>=V2+1] * Chain [25,29,33]: 0 with precondition: [V1=2,Out=0,V2>=1,V>=V2+1] #### Cost of chains of fun1(V1,V,Out): * Chain [[34],36]: 1*it(34)+1 Such that:it(34) =< Out with precondition: [Out>=1,V1>=Out,V>=Out] * Chain [[34],35]: 1*it(34)+1 Such that:it(34) =< Out with precondition: [V+1=Out,V>=1,V1>=V+1] * Chain [36]: 1 with precondition: [Out=0,V1>=0,V>=0] * Chain [35]: 1 with precondition: [V=0,Out=1,V1>=1] #### Cost of chains of fun2(V1,Out): * Chain [39]: 1 with precondition: [V1=0,Out=1] * Chain [38]: 0 with precondition: [Out=0,V1>=0] * Chain [37]: 1 with precondition: [Out=2,V1>=1] #### Cost of chains of fun(V1,V,V2,Out): * Chain [[40,41,42,43],73]: 8*it(40)+1*s(5)+1*s(6)+0 Such that:aux(3) =< V aux(5) =< V/2-V2/2 aux(1) =< V/2+V2/2+1/2 aux(7) =< V/2-V2/2+1/2 it(40) =< aux(3) it(40) =< aux(7) it(40) =< aux(5) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,Out>=1,V>=V2+1] * Chain [[40,41,42,43],61,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(7)+2 Such that:aux(3) =< V aux(1) =< V/2+V2/2+1/2 s(7) =< V/2+V2/2+3/2 aux(8) =< V/2-V2/2 it(40) =< aux(3) it(40) =< aux(8) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,V>=V2+3,Out>=V2+4] * Chain [[40,41,42,43],60,73]: 8*it(40)+1*s(5)+1*s(6)+2 Such that:aux(3) =< V aux(5) =< V/2-V2/2 aux(1) =< V/2+V2/2+1/2 aux(9) =< V/2-V2/2+1/2 it(40) =< aux(3) it(40) =< aux(9) it(40) =< aux(5) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,Out>=2,V>=V2+1] * Chain [[40,41,42,43],59,73]: 8*it(40)+1*s(5)+1*s(6)+2 Such that:aux(3) =< V aux(5) =< V/2-V2/2 aux(1) =< V/2+V2/2+1/2 aux(10) =< V/2-V2/2+1/2 it(40) =< aux(3) it(40) =< aux(10) it(40) =< aux(5) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,Out>=4,V>=V2+1] * Chain [[40,41,42,43],58,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(8)+2 Such that:aux(5) =< V/2-V2/2 aux(1) =< V/2+V2/2+1/2 aux(11) =< V s(8) =< aux(11) it(40) =< aux(11) it(40) =< aux(5) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,Out>=3,V>=V2+1] * Chain [[40,41,42,43],57,73]: 8*it(40)+1*s(5)+1*s(6)+2 Such that:aux(3) =< V aux(5) =< V/2-V2/2 aux(1) =< V/2+V2/2+1/2 aux(12) =< V/2-V2/2+1/2 it(40) =< aux(3) it(40) =< aux(12) it(40) =< aux(5) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,Out>=2,V>=V2+1] * Chain [[40,41,42,43],56,73]: 8*it(40)+1*s(5)+1*s(6)+2 Such that:aux(3) =< V aux(5) =< V/2-V2/2 aux(1) =< V/2+V2/2+1/2 aux(13) =< V/2-V2/2+1/2 it(40) =< aux(3) it(40) =< aux(13) it(40) =< aux(5) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,Out>=4,V>=V2+1] * Chain [[40,41,42,43],55,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(9)+2 Such that:aux(3) =< V aux(1) =< V/2+V2/2+1/2 s(9) =< V/2+V2/2+3/2 aux(14) =< V/2-V2/2 it(40) =< aux(3) it(40) =< aux(14) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,V>=V2+3,Out>=V2+4] * Chain [[40,41,42,43],54,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(10)+2 Such that:aux(3) =< V aux(5) =< V/2-V2/2 aux(1) =< V/2+V2/2+1/2 s(10) =< V/2+V2/2+3/2 aux(15) =< V/2-V2/2+1/2 it(40) =< aux(3) it(40) =< aux(15) it(40) =< aux(5) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,Out>=3,V>=V2+1] * Chain [[40,41,42,43],53,73]: 8*it(40)+1*s(5)+1*s(6)+2 Such that:aux(3) =< V aux(5) =< V/2-V2/2 aux(1) =< V/2+V2/2+1/2 aux(16) =< V/2-V2/2+1/2 it(40) =< aux(3) it(40) =< aux(16) it(40) =< aux(5) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,Out>=2,V>=V2+1,V2+2*Out>=V+2] * Chain [[40,41,42,43],52,73]: 8*it(40)+1*s(5)+1*s(6)+2 Such that:aux(3) =< V aux(5) =< V/2-V2/2 aux(1) =< V/2+V2/2+1/2 aux(17) =< V/2-V2/2+1/2 it(40) =< aux(3) it(40) =< aux(17) it(40) =< aux(5) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,Out>=4,V>=V2+1,V2+2*Out>=V+6] * Chain [[40,41,42,43],51,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(11)+2 Such that:aux(5) =< V/2-V2/2 aux(1) =< V/2+V2/2+1/2 aux(18) =< V s(11) =< aux(18) it(40) =< aux(18) it(40) =< aux(5) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,Out>=3,V>=V2+1,V2+2*Out>=V+4] * Chain [[40,41,42,43],50,73]: 8*it(40)+1*s(5)+1*s(6)+2 Such that:aux(3) =< V aux(5) =< V/2-V2/2 aux(1) =< V/2+V2/2+1/2 aux(19) =< V/2-V2/2+1/2 it(40) =< aux(3) it(40) =< aux(19) it(40) =< aux(5) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,Out>=2,V>=V2+1,V2+2*Out>=V+2] * Chain [[40,41,42,43],49,73]: 8*it(40)+1*s(5)+1*s(6)+2 Such that:aux(3) =< V aux(5) =< V/2-V2/2 aux(1) =< V/2+V2/2+1/2 aux(20) =< V/2-V2/2+1/2 it(40) =< aux(3) it(40) =< aux(20) it(40) =< aux(5) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,Out>=4,V>=V2+1,V2+2*Out>=V+6] * Chain [[40,41,42,43],48,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(12)+2 Such that:aux(5) =< V/2-V2/2 aux(1) =< V/2+V2/2+1/2 aux(21) =< V s(12) =< aux(21) it(40) =< aux(21) it(40) =< aux(5) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,Out>=3,V>=V2+1,V2+2*Out>=V+4] * Chain [[40,41,42,43],47,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(13)+2 Such that:aux(3) =< V aux(1) =< V/2+V2/2+1/2 s(13) =< V/2+V2/2+3/2 aux(22) =< V/2-V2/2 it(40) =< aux(3) it(40) =< aux(22) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,V>=V2+3,Out>=V2+4] * Chain [[40,41,42,43],47,72,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(13)+4 Such that:aux(3) =< V aux(1) =< V/2+V2/2+1/2 s(13) =< V/2+V2/2+7/2 aux(23) =< V/2-V2/2 it(40) =< aux(3) it(40) =< aux(23) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,V>=V2+3,Out>=V2+6] * Chain [[40,41,42,43],47,71,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(13)+4 Such that:aux(3) =< V aux(1) =< V/2+V2/2+1/2 s(13) =< V/2+V2/2+5/2 aux(24) =< V/2-V2/2 it(40) =< aux(3) it(40) =< aux(24) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,V>=V2+3,Out>=V2+5] * Chain [[40,41,42,43],47,70,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(13)+4 Such that:aux(3) =< V aux(1) =< V/2+V2/2+1/2 s(13) =< V/2+V2/2+7/2 aux(25) =< V/2-V2/2 it(40) =< aux(3) it(40) =< aux(25) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,V>=V2+3,Out>=V2+6] * Chain [[40,41,42,43],47,60,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(13)+4 Such that:aux(3) =< V aux(1) =< V/2+V2/2+1/2 s(13) =< V/2+V2/2+5/2 aux(26) =< V/2-V2/2 it(40) =< aux(3) it(40) =< aux(26) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,V>=V2+3,Out>=V2+5] * Chain [[40,41,42,43],46,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(14)+2 Such that:aux(3) =< V aux(27) =< V/2-V2/2 aux(28) =< V/2+V2/2+1/2 s(14) =< aux(28) it(40) =< aux(3) it(40) =< aux(27) aux(2) =< aux(28) s(5) =< it(40)*aux(28) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,Out>=3,V>=V2+3] * Chain [[40,41,42,43],46,72,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(14)+4 Such that:aux(3) =< V aux(29) =< V/2-V2/2 aux(30) =< V/2+V2/2+1/2 s(14) =< aux(30) it(40) =< aux(3) it(40) =< aux(29) aux(2) =< aux(30) s(5) =< it(40)*aux(30) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,Out>=5,V>=V2+3] * Chain [[40,41,42,43],46,71,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(14)+4 Such that:aux(3) =< V aux(31) =< V/2-V2/2 aux(32) =< V/2+V2/2+1/2 s(14) =< aux(32) it(40) =< aux(3) it(40) =< aux(31) aux(2) =< aux(32) s(5) =< it(40)*aux(32) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,Out>=4,V>=V2+3] * Chain [[40,41,42,43],46,70,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(14)+4 Such that:aux(3) =< V aux(33) =< V/2-V2/2 aux(34) =< V/2+V2/2+1/2 s(14) =< aux(34) it(40) =< aux(3) it(40) =< aux(33) aux(2) =< aux(34) s(5) =< it(40)*aux(34) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,Out>=5,V>=V2+3] * Chain [[40,41,42,43],46,60,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(14)+4 Such that:aux(3) =< V aux(35) =< V/2-V2/2 aux(36) =< V/2+V2/2+1/2 s(14) =< aux(36) it(40) =< aux(3) it(40) =< aux(35) aux(2) =< aux(36) s(5) =< it(40)*aux(36) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,Out>=4,V>=V2+3] * Chain [[40,41,42,43],45,73]: 8*it(40)+1*s(5)+1*s(6)+2 Such that:aux(3) =< V aux(1) =< V/2+V2/2+1/2 aux(37) =< V/2-V2/2 it(40) =< aux(3) it(40) =< aux(37) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,Out>=2,V>=V2+3] * Chain [[40,41,42,43],45,72,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+V2/2+1/2 aux(38) =< V/2-V2/2 it(40) =< aux(3) it(40) =< aux(38) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,Out>=4,V>=V2+3] * Chain [[40,41,42,43],45,71,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+V2/2+1/2 aux(39) =< V/2-V2/2 it(40) =< aux(3) it(40) =< aux(39) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,Out>=3,V>=V2+3] * Chain [[40,41,42,43],45,70,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+V2/2+1/2 aux(40) =< V/2-V2/2 it(40) =< aux(3) it(40) =< aux(40) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,Out>=4,V>=V2+3] * Chain [[40,41,42,43],45,60,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+V2/2+1/2 aux(41) =< V/2-V2/2 it(40) =< aux(3) it(40) =< aux(41) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,Out>=3,V>=V2+3] * Chain [[40,41,42,43],44,73]: 8*it(40)+1*s(5)+1*s(6)+2 Such that:aux(3) =< V aux(1) =< V/2+V2/2+1/2 aux(42) =< V/2-V2/2 it(40) =< aux(3) it(40) =< aux(42) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,Out>=4,V>=V2+3] * Chain [[40,41,42,43],44,72,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+V2/2+1/2 aux(43) =< V/2-V2/2 it(40) =< aux(3) it(40) =< aux(43) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,Out>=6,V>=V2+3] * Chain [[40,41,42,43],44,71,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+V2/2+1/2 aux(44) =< V/2-V2/2 it(40) =< aux(3) it(40) =< aux(44) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,Out>=5,V>=V2+3] * Chain [[40,41,42,43],44,70,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+V2/2+1/2 aux(45) =< V/2-V2/2 it(40) =< aux(3) it(40) =< aux(45) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,Out>=6,V>=V2+3] * Chain [[40,41,42,43],44,60,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+V2/2+1/2 aux(46) =< V/2-V2/2 it(40) =< aux(3) it(40) =< aux(46) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2>=1,Out>=5,V>=V2+3] * Chain [73]: 0 with precondition: [Out=0,V1>=0,V>=0,V2>=0] * Chain [72,73]: 2 with precondition: [V1=2,V=0,Out=2,V2>=0] * Chain [71,73]: 2 with precondition: [V1=2,V=0,Out=1,V2>=0] * Chain [70,73]: 2 with precondition: [V1=2,V=0,Out=2,V2>=0] * Chain [69,73]: 2 with precondition: [V1=2,V2=0,Out=2,V>=1] * Chain [68,73]: 2 with precondition: [V1=2,V2=0,Out=2,V>=1] * Chain [67,73]: 2 with precondition: [V1=2,V2=0,Out=1,V>=1] * Chain [67,72,73]: 4 with precondition: [V1=2,V2=0,Out=3,V>=1] * Chain [67,71,73]: 4 with precondition: [V1=2,V2=0,Out=2,V>=1] * Chain [67,70,73]: 4 with precondition: [V1=2,V2=0,Out=3,V>=1] * Chain [67,60,73]: 4 with precondition: [V1=2,V2=0,Out=2,V>=1] * Chain [66,73]: 2 with precondition: [V1=2,V2=0,Out=2,V>=1] * Chain [66,72,73]: 4 with precondition: [V1=2,V2=0,Out=4,V>=1] * Chain [66,71,73]: 4 with precondition: [V1=2,V2=0,Out=3,V>=1] * Chain [66,70,73]: 4 with precondition: [V1=2,V2=0,Out=4,V>=1] * Chain [66,60,73]: 4 with precondition: [V1=2,V2=0,Out=3,V>=1] * Chain [65,73]: 2 with precondition: [V1=2,V2=0,Out=3,V>=1] * Chain [65,72,73]: 4 with precondition: [V1=2,V2=0,Out=5,V>=1] * Chain [65,71,73]: 4 with precondition: [V1=2,V2=0,Out=4,V>=1] * Chain [65,70,73]: 4 with precondition: [V1=2,V2=0,Out=5,V>=1] * Chain [65,60,73]: 4 with precondition: [V1=2,V2=0,Out=4,V>=1] * Chain [64,[40,41,42,43],73]: 8*it(40)+1*s(5)+1*s(6)+2 Such that:aux(3) =< V aux(1) =< V/2+1/2 aux(47) =< V/2 it(40) =< aux(3) it(40) =< aux(47) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=2] * Chain [64,[40,41,42,43],61,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(7)+4 Such that:aux(3) =< V aux(8) =< V/2 aux(1) =< V/2+1/2 s(7) =< V/2+3/2 it(40) =< aux(3) it(40) =< aux(8) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=6] * Chain [64,[40,41,42,43],60,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+1/2 aux(48) =< V/2 it(40) =< aux(3) it(40) =< aux(48) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=3] * Chain [64,[40,41,42,43],59,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+1/2 aux(49) =< V/2 it(40) =< aux(3) it(40) =< aux(49) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=5] * Chain [64,[40,41,42,43],58,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(8)+4 Such that:aux(11) =< V aux(5) =< V/2 aux(1) =< V/2+1/2 s(8) =< aux(11) it(40) =< aux(11) it(40) =< aux(5) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=4] * Chain [64,[40,41,42,43],57,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+1/2 aux(50) =< V/2 it(40) =< aux(3) it(40) =< aux(50) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=3] * Chain [64,[40,41,42,43],56,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+1/2 aux(51) =< V/2 it(40) =< aux(3) it(40) =< aux(51) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=5] * Chain [64,[40,41,42,43],55,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(9)+4 Such that:aux(3) =< V aux(14) =< V/2 aux(1) =< V/2+1/2 s(9) =< V/2+3/2 it(40) =< aux(3) it(40) =< aux(14) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=6] * Chain [64,[40,41,42,43],54,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(10)+4 Such that:aux(3) =< V aux(1) =< V/2+1/2 s(10) =< V/2+3/2 aux(52) =< V/2 it(40) =< aux(3) it(40) =< aux(52) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=4] * Chain [64,[40,41,42,43],53,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+1/2 aux(53) =< V/2 it(40) =< aux(3) it(40) =< aux(53) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=3,2*Out>=V+2] * Chain [64,[40,41,42,43],52,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+1/2 aux(54) =< V/2 it(40) =< aux(3) it(40) =< aux(54) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=5,2*Out>=V+6] * Chain [64,[40,41,42,43],51,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(11)+4 Such that:aux(18) =< V aux(5) =< V/2 aux(1) =< V/2+1/2 s(11) =< aux(18) it(40) =< aux(18) it(40) =< aux(5) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=4,2*Out>=V+4] * Chain [64,[40,41,42,43],50,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+1/2 aux(55) =< V/2 it(40) =< aux(3) it(40) =< aux(55) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=3,2*Out>=V+2] * Chain [64,[40,41,42,43],49,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+1/2 aux(56) =< V/2 it(40) =< aux(3) it(40) =< aux(56) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=5,2*Out>=V+6] * Chain [64,[40,41,42,43],48,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(12)+4 Such that:aux(21) =< V aux(5) =< V/2 aux(1) =< V/2+1/2 s(12) =< aux(21) it(40) =< aux(21) it(40) =< aux(5) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=4,2*Out>=V+4] * Chain [64,[40,41,42,43],47,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(13)+4 Such that:aux(3) =< V aux(22) =< V/2 aux(1) =< V/2+1/2 s(13) =< V/2+3/2 it(40) =< aux(3) it(40) =< aux(22) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=6] * Chain [64,[40,41,42,43],47,72,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(13)+6 Such that:aux(3) =< V aux(23) =< V/2 aux(1) =< V/2+1/2 s(13) =< V/2+7/2 it(40) =< aux(3) it(40) =< aux(23) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=8] * Chain [64,[40,41,42,43],47,71,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(13)+6 Such that:aux(3) =< V aux(24) =< V/2 aux(1) =< V/2+1/2 s(13) =< V/2+5/2 it(40) =< aux(3) it(40) =< aux(24) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=7] * Chain [64,[40,41,42,43],47,70,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(13)+6 Such that:aux(3) =< V aux(25) =< V/2 aux(1) =< V/2+1/2 s(13) =< V/2+7/2 it(40) =< aux(3) it(40) =< aux(25) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=8] * Chain [64,[40,41,42,43],47,60,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(13)+6 Such that:aux(3) =< V aux(26) =< V/2 aux(1) =< V/2+1/2 s(13) =< V/2+5/2 it(40) =< aux(3) it(40) =< aux(26) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=7] * Chain [64,[40,41,42,43],46,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(14)+4 Such that:aux(3) =< V aux(27) =< V/2 aux(28) =< V/2+1/2 s(14) =< aux(28) it(40) =< aux(3) it(40) =< aux(27) aux(2) =< aux(28) s(5) =< it(40)*aux(28) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=4] * Chain [64,[40,41,42,43],46,72,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(14)+6 Such that:aux(3) =< V aux(29) =< V/2 aux(30) =< V/2+1/2 s(14) =< aux(30) it(40) =< aux(3) it(40) =< aux(29) aux(2) =< aux(30) s(5) =< it(40)*aux(30) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=6] * Chain [64,[40,41,42,43],46,71,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(14)+6 Such that:aux(3) =< V aux(31) =< V/2 aux(32) =< V/2+1/2 s(14) =< aux(32) it(40) =< aux(3) it(40) =< aux(31) aux(2) =< aux(32) s(5) =< it(40)*aux(32) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=5] * Chain [64,[40,41,42,43],46,70,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(14)+6 Such that:aux(3) =< V aux(33) =< V/2 aux(34) =< V/2+1/2 s(14) =< aux(34) it(40) =< aux(3) it(40) =< aux(33) aux(2) =< aux(34) s(5) =< it(40)*aux(34) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=6] * Chain [64,[40,41,42,43],46,60,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(14)+6 Such that:aux(3) =< V aux(35) =< V/2 aux(36) =< V/2+1/2 s(14) =< aux(36) it(40) =< aux(3) it(40) =< aux(35) aux(2) =< aux(36) s(5) =< it(40)*aux(36) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=5] * Chain [64,[40,41,42,43],45,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(37) =< V/2 aux(1) =< V/2+1/2 it(40) =< aux(3) it(40) =< aux(37) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=3] * Chain [64,[40,41,42,43],45,72,73]: 8*it(40)+1*s(5)+1*s(6)+6 Such that:aux(3) =< V aux(38) =< V/2 aux(1) =< V/2+1/2 it(40) =< aux(3) it(40) =< aux(38) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=5] * Chain [64,[40,41,42,43],45,71,73]: 8*it(40)+1*s(5)+1*s(6)+6 Such that:aux(3) =< V aux(39) =< V/2 aux(1) =< V/2+1/2 it(40) =< aux(3) it(40) =< aux(39) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=4] * Chain [64,[40,41,42,43],45,70,73]: 8*it(40)+1*s(5)+1*s(6)+6 Such that:aux(3) =< V aux(40) =< V/2 aux(1) =< V/2+1/2 it(40) =< aux(3) it(40) =< aux(40) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=5] * Chain [64,[40,41,42,43],45,60,73]: 8*it(40)+1*s(5)+1*s(6)+6 Such that:aux(3) =< V aux(41) =< V/2 aux(1) =< V/2+1/2 it(40) =< aux(3) it(40) =< aux(41) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=4] * Chain [64,[40,41,42,43],44,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(42) =< V/2 aux(1) =< V/2+1/2 it(40) =< aux(3) it(40) =< aux(42) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=5] * Chain [64,[40,41,42,43],44,72,73]: 8*it(40)+1*s(5)+1*s(6)+6 Such that:aux(3) =< V aux(43) =< V/2 aux(1) =< V/2+1/2 it(40) =< aux(3) it(40) =< aux(43) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=7] * Chain [64,[40,41,42,43],44,71,73]: 8*it(40)+1*s(5)+1*s(6)+6 Such that:aux(3) =< V aux(44) =< V/2 aux(1) =< V/2+1/2 it(40) =< aux(3) it(40) =< aux(44) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=6] * Chain [64,[40,41,42,43],44,70,73]: 8*it(40)+1*s(5)+1*s(6)+6 Such that:aux(3) =< V aux(45) =< V/2 aux(1) =< V/2+1/2 it(40) =< aux(3) it(40) =< aux(45) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=7] * Chain [64,[40,41,42,43],44,60,73]: 8*it(40)+1*s(5)+1*s(6)+6 Such that:aux(3) =< V aux(46) =< V/2 aux(1) =< V/2+1/2 it(40) =< aux(3) it(40) =< aux(46) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=6] * Chain [64,73]: 2 with precondition: [V1=2,V2=0,Out=1,V>=1] * Chain [64,72,73]: 4 with precondition: [V1=2,V=1,V2=0,Out=3] * Chain [64,71,73]: 4 with precondition: [V1=2,V=1,V2=0,Out=2] * Chain [64,70,73]: 4 with precondition: [V1=2,V=1,V2=0,Out=3] * Chain [64,61,73]: 1*s(7)+4 Such that:s(7) =< 3 with precondition: [V1=2,V2=0,Out=4,V>=3] * Chain [64,60,73]: 4 with precondition: [V1=2,V2=0,Out=2,V>=1] * Chain [64,59,73]: 4 with precondition: [V1=2,V2=0,Out=4,V>=2] * Chain [64,58,73]: 1*s(8)+4 Such that:s(8) =< V with precondition: [V1=2,V2=0,Out=3,V>=2] * Chain [64,57,73]: 4 with precondition: [V1=2,V2=0,Out=2,V>=2] * Chain [64,56,73]: 4 with precondition: [V1=2,V2=0,Out=4,V>=2] * Chain [64,55,73]: 1*s(9)+4 Such that:s(9) =< 3 with precondition: [V1=2,V2=0,Out=4,V>=3] * Chain [64,54,73]: 1*s(10)+4 Such that:s(10) =< 2 with precondition: [V1=2,V2=0,Out=3,V>=2] * Chain [64,53,73]: 4 with precondition: [V1=2,V=2,V2=0,Out=2] * Chain [64,52,73]: 4 with precondition: [V1=2,V=2,V2=0,Out=4] * Chain [64,51,73]: 1*s(11)+4 Such that:s(11) =< 1 with precondition: [V1=2,V=2,V2=0,Out=3] * Chain [64,50,73]: 4 with precondition: [V1=2,V=2,V2=0,Out=2] * Chain [64,49,73]: 4 with precondition: [V1=2,V=2,V2=0,Out=4] * Chain [64,48,73]: 1*s(12)+4 Such that:s(12) =< 1 with precondition: [V1=2,V=2,V2=0,Out=3] * Chain [64,47,73]: 1*s(13)+4 Such that:s(13) =< 3 with precondition: [V1=2,V2=0,Out=4,V>=3] * Chain [64,47,72,73]: 1*s(13)+6 Such that:s(13) =< 5 with precondition: [V1=2,V2=0,Out=6,V>=3] * Chain [64,47,71,73]: 1*s(13)+6 Such that:s(13) =< 4 with precondition: [V1=2,V2=0,Out=5,V>=3] * Chain [64,47,70,73]: 1*s(13)+6 Such that:s(13) =< 5 with precondition: [V1=2,V2=0,Out=6,V>=3] * Chain [64,47,60,73]: 1*s(13)+6 Such that:s(13) =< 4 with precondition: [V1=2,V2=0,Out=5,V>=3] * Chain [64,46,73]: 1*s(14)+4 Such that:s(14) =< 2 with precondition: [V1=2,V2=0,Out=3,V>=3] * Chain [64,46,72,73]: 1*s(14)+6 Such that:s(14) =< 2 with precondition: [V1=2,V2=0,Out=5,V>=3] * Chain [64,46,71,73]: 1*s(14)+6 Such that:s(14) =< 2 with precondition: [V1=2,V2=0,Out=4,V>=3] * Chain [64,46,70,73]: 1*s(14)+6 Such that:s(14) =< 2 with precondition: [V1=2,V2=0,Out=5,V>=3] * Chain [64,46,60,73]: 1*s(14)+6 Such that:s(14) =< 2 with precondition: [V1=2,V2=0,Out=4,V>=3] * Chain [64,45,73]: 4 with precondition: [V1=2,V2=0,Out=2,V>=3] * Chain [64,45,72,73]: 6 with precondition: [V1=2,V2=0,Out=4,V>=3] * Chain [64,45,71,73]: 6 with precondition: [V1=2,V2=0,Out=3,V>=3] * Chain [64,45,70,73]: 6 with precondition: [V1=2,V2=0,Out=4,V>=3] * Chain [64,45,60,73]: 6 with precondition: [V1=2,V2=0,Out=3,V>=3] * Chain [64,44,73]: 4 with precondition: [V1=2,V2=0,Out=4,V>=3] * Chain [64,44,72,73]: 6 with precondition: [V1=2,V2=0,Out=6,V>=3] * Chain [64,44,71,73]: 6 with precondition: [V1=2,V2=0,Out=5,V>=3] * Chain [64,44,70,73]: 6 with precondition: [V1=2,V2=0,Out=6,V>=3] * Chain [64,44,60,73]: 6 with precondition: [V1=2,V2=0,Out=5,V>=3] * Chain [63,[40,41,42,43],73]: 8*it(40)+1*s(5)+1*s(6)+2 Such that:aux(3) =< V aux(1) =< V/2+1/2 aux(57) =< V/2 it(40) =< aux(3) it(40) =< aux(57) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=3] * Chain [63,[40,41,42,43],61,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(7)+4 Such that:aux(3) =< V aux(8) =< V/2 aux(1) =< V/2+1/2 s(7) =< V/2+3/2 it(40) =< aux(3) it(40) =< aux(8) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=7] * Chain [63,[40,41,42,43],60,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+1/2 aux(58) =< V/2 it(40) =< aux(3) it(40) =< aux(58) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=4] * Chain [63,[40,41,42,43],59,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+1/2 aux(59) =< V/2 it(40) =< aux(3) it(40) =< aux(59) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=6] * Chain [63,[40,41,42,43],58,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(8)+4 Such that:aux(11) =< V aux(5) =< V/2 aux(1) =< V/2+1/2 s(8) =< aux(11) it(40) =< aux(11) it(40) =< aux(5) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=5] * Chain [63,[40,41,42,43],57,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+1/2 aux(60) =< V/2 it(40) =< aux(3) it(40) =< aux(60) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=4] * Chain [63,[40,41,42,43],56,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+1/2 aux(61) =< V/2 it(40) =< aux(3) it(40) =< aux(61) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=6] * Chain [63,[40,41,42,43],55,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(9)+4 Such that:aux(3) =< V aux(14) =< V/2 aux(1) =< V/2+1/2 s(9) =< V/2+3/2 it(40) =< aux(3) it(40) =< aux(14) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=7] * Chain [63,[40,41,42,43],54,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(10)+4 Such that:aux(3) =< V aux(1) =< V/2+1/2 s(10) =< V/2+3/2 aux(62) =< V/2 it(40) =< aux(3) it(40) =< aux(62) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=5] * Chain [63,[40,41,42,43],53,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+1/2 aux(63) =< V/2 it(40) =< aux(3) it(40) =< aux(63) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=4,2*Out>=V+4] * Chain [63,[40,41,42,43],52,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+1/2 aux(64) =< V/2 it(40) =< aux(3) it(40) =< aux(64) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=6,2*Out>=V+8] * Chain [63,[40,41,42,43],51,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(11)+4 Such that:aux(18) =< V aux(5) =< V/2 aux(1) =< V/2+1/2 s(11) =< aux(18) it(40) =< aux(18) it(40) =< aux(5) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=5,2*Out>=V+6] * Chain [63,[40,41,42,43],50,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+1/2 aux(65) =< V/2 it(40) =< aux(3) it(40) =< aux(65) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=4,2*Out>=V+4] * Chain [63,[40,41,42,43],49,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+1/2 aux(66) =< V/2 it(40) =< aux(3) it(40) =< aux(66) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=6,2*Out>=V+8] * Chain [63,[40,41,42,43],48,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(12)+4 Such that:aux(21) =< V aux(5) =< V/2 aux(1) =< V/2+1/2 s(12) =< aux(21) it(40) =< aux(21) it(40) =< aux(5) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=5,2*Out>=V+6] * Chain [63,[40,41,42,43],47,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(13)+4 Such that:aux(3) =< V aux(22) =< V/2 aux(1) =< V/2+1/2 s(13) =< V/2+3/2 it(40) =< aux(3) it(40) =< aux(22) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=7] * Chain [63,[40,41,42,43],47,72,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(13)+6 Such that:aux(3) =< V aux(23) =< V/2 aux(1) =< V/2+1/2 s(13) =< V/2+7/2 it(40) =< aux(3) it(40) =< aux(23) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=9] * Chain [63,[40,41,42,43],47,71,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(13)+6 Such that:aux(3) =< V aux(24) =< V/2 aux(1) =< V/2+1/2 s(13) =< V/2+5/2 it(40) =< aux(3) it(40) =< aux(24) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=8] * Chain [63,[40,41,42,43],47,70,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(13)+6 Such that:aux(3) =< V aux(25) =< V/2 aux(1) =< V/2+1/2 s(13) =< V/2+7/2 it(40) =< aux(3) it(40) =< aux(25) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=9] * Chain [63,[40,41,42,43],47,60,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(13)+6 Such that:aux(3) =< V aux(26) =< V/2 aux(1) =< V/2+1/2 s(13) =< V/2+5/2 it(40) =< aux(3) it(40) =< aux(26) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=8] * Chain [63,[40,41,42,43],46,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(14)+4 Such that:aux(3) =< V aux(27) =< V/2 aux(28) =< V/2+1/2 s(14) =< aux(28) it(40) =< aux(3) it(40) =< aux(27) aux(2) =< aux(28) s(5) =< it(40)*aux(28) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=5] * Chain [63,[40,41,42,43],46,72,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(14)+6 Such that:aux(3) =< V aux(29) =< V/2 aux(30) =< V/2+1/2 s(14) =< aux(30) it(40) =< aux(3) it(40) =< aux(29) aux(2) =< aux(30) s(5) =< it(40)*aux(30) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=7] * Chain [63,[40,41,42,43],46,71,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(14)+6 Such that:aux(3) =< V aux(31) =< V/2 aux(32) =< V/2+1/2 s(14) =< aux(32) it(40) =< aux(3) it(40) =< aux(31) aux(2) =< aux(32) s(5) =< it(40)*aux(32) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=6] * Chain [63,[40,41,42,43],46,70,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(14)+6 Such that:aux(3) =< V aux(33) =< V/2 aux(34) =< V/2+1/2 s(14) =< aux(34) it(40) =< aux(3) it(40) =< aux(33) aux(2) =< aux(34) s(5) =< it(40)*aux(34) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=7] * Chain [63,[40,41,42,43],46,60,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(14)+6 Such that:aux(3) =< V aux(35) =< V/2 aux(36) =< V/2+1/2 s(14) =< aux(36) it(40) =< aux(3) it(40) =< aux(35) aux(2) =< aux(36) s(5) =< it(40)*aux(36) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=6] * Chain [63,[40,41,42,43],45,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(37) =< V/2 aux(1) =< V/2+1/2 it(40) =< aux(3) it(40) =< aux(37) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=4] * Chain [63,[40,41,42,43],45,72,73]: 8*it(40)+1*s(5)+1*s(6)+6 Such that:aux(3) =< V aux(38) =< V/2 aux(1) =< V/2+1/2 it(40) =< aux(3) it(40) =< aux(38) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=6] * Chain [63,[40,41,42,43],45,71,73]: 8*it(40)+1*s(5)+1*s(6)+6 Such that:aux(3) =< V aux(39) =< V/2 aux(1) =< V/2+1/2 it(40) =< aux(3) it(40) =< aux(39) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=5] * Chain [63,[40,41,42,43],45,70,73]: 8*it(40)+1*s(5)+1*s(6)+6 Such that:aux(3) =< V aux(40) =< V/2 aux(1) =< V/2+1/2 it(40) =< aux(3) it(40) =< aux(40) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=6] * Chain [63,[40,41,42,43],45,60,73]: 8*it(40)+1*s(5)+1*s(6)+6 Such that:aux(3) =< V aux(41) =< V/2 aux(1) =< V/2+1/2 it(40) =< aux(3) it(40) =< aux(41) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=5] * Chain [63,[40,41,42,43],44,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(42) =< V/2 aux(1) =< V/2+1/2 it(40) =< aux(3) it(40) =< aux(42) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=6] * Chain [63,[40,41,42,43],44,72,73]: 8*it(40)+1*s(5)+1*s(6)+6 Such that:aux(3) =< V aux(43) =< V/2 aux(1) =< V/2+1/2 it(40) =< aux(3) it(40) =< aux(43) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=8] * Chain [63,[40,41,42,43],44,71,73]: 8*it(40)+1*s(5)+1*s(6)+6 Such that:aux(3) =< V aux(44) =< V/2 aux(1) =< V/2+1/2 it(40) =< aux(3) it(40) =< aux(44) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=7] * Chain [63,[40,41,42,43],44,70,73]: 8*it(40)+1*s(5)+1*s(6)+6 Such that:aux(3) =< V aux(45) =< V/2 aux(1) =< V/2+1/2 it(40) =< aux(3) it(40) =< aux(45) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=8] * Chain [63,[40,41,42,43],44,60,73]: 8*it(40)+1*s(5)+1*s(6)+6 Such that:aux(3) =< V aux(46) =< V/2 aux(1) =< V/2+1/2 it(40) =< aux(3) it(40) =< aux(46) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=7] * Chain [63,73]: 2 with precondition: [V1=2,V2=0,Out=2,V>=1] * Chain [63,72,73]: 4 with precondition: [V1=2,V=1,V2=0,Out=4] * Chain [63,71,73]: 4 with precondition: [V1=2,V=1,V2=0,Out=3] * Chain [63,70,73]: 4 with precondition: [V1=2,V=1,V2=0,Out=4] * Chain [63,61,73]: 1*s(7)+4 Such that:s(7) =< 3 with precondition: [V1=2,V2=0,Out=5,V>=3] * Chain [63,60,73]: 4 with precondition: [V1=2,V2=0,Out=3,V>=1] * Chain [63,59,73]: 4 with precondition: [V1=2,V2=0,Out=5,V>=2] * Chain [63,58,73]: 1*s(8)+4 Such that:s(8) =< V with precondition: [V1=2,V2=0,Out=4,V>=2] * Chain [63,57,73]: 4 with precondition: [V1=2,V2=0,Out=3,V>=2] * Chain [63,56,73]: 4 with precondition: [V1=2,V2=0,Out=5,V>=2] * Chain [63,55,73]: 1*s(9)+4 Such that:s(9) =< 3 with precondition: [V1=2,V2=0,Out=5,V>=3] * Chain [63,54,73]: 1*s(10)+4 Such that:s(10) =< 2 with precondition: [V1=2,V2=0,Out=4,V>=2] * Chain [63,53,73]: 4 with precondition: [V1=2,V=2,V2=0,Out=3] * Chain [63,52,73]: 4 with precondition: [V1=2,V=2,V2=0,Out=5] * Chain [63,51,73]: 1*s(11)+4 Such that:s(11) =< 1 with precondition: [V1=2,V=2,V2=0,Out=4] * Chain [63,50,73]: 4 with precondition: [V1=2,V=2,V2=0,Out=3] * Chain [63,49,73]: 4 with precondition: [V1=2,V=2,V2=0,Out=5] * Chain [63,48,73]: 1*s(12)+4 Such that:s(12) =< 1 with precondition: [V1=2,V=2,V2=0,Out=4] * Chain [63,47,73]: 1*s(13)+4 Such that:s(13) =< 3 with precondition: [V1=2,V2=0,Out=5,V>=3] * Chain [63,47,72,73]: 1*s(13)+6 Such that:s(13) =< 5 with precondition: [V1=2,V2=0,Out=7,V>=3] * Chain [63,47,71,73]: 1*s(13)+6 Such that:s(13) =< 4 with precondition: [V1=2,V2=0,Out=6,V>=3] * Chain [63,47,70,73]: 1*s(13)+6 Such that:s(13) =< 5 with precondition: [V1=2,V2=0,Out=7,V>=3] * Chain [63,47,60,73]: 1*s(13)+6 Such that:s(13) =< 4 with precondition: [V1=2,V2=0,Out=6,V>=3] * Chain [63,46,73]: 1*s(14)+4 Such that:s(14) =< 2 with precondition: [V1=2,V2=0,Out=4,V>=3] * Chain [63,46,72,73]: 1*s(14)+6 Such that:s(14) =< 2 with precondition: [V1=2,V2=0,Out=6,V>=3] * Chain [63,46,71,73]: 1*s(14)+6 Such that:s(14) =< 2 with precondition: [V1=2,V2=0,Out=5,V>=3] * Chain [63,46,70,73]: 1*s(14)+6 Such that:s(14) =< 2 with precondition: [V1=2,V2=0,Out=6,V>=3] * Chain [63,46,60,73]: 1*s(14)+6 Such that:s(14) =< 2 with precondition: [V1=2,V2=0,Out=5,V>=3] * Chain [63,45,73]: 4 with precondition: [V1=2,V2=0,Out=3,V>=3] * Chain [63,45,72,73]: 6 with precondition: [V1=2,V2=0,Out=5,V>=3] * Chain [63,45,71,73]: 6 with precondition: [V1=2,V2=0,Out=4,V>=3] * Chain [63,45,70,73]: 6 with precondition: [V1=2,V2=0,Out=5,V>=3] * Chain [63,45,60,73]: 6 with precondition: [V1=2,V2=0,Out=4,V>=3] * Chain [63,44,73]: 4 with precondition: [V1=2,V2=0,Out=5,V>=3] * Chain [63,44,72,73]: 6 with precondition: [V1=2,V2=0,Out=7,V>=3] * Chain [63,44,71,73]: 6 with precondition: [V1=2,V2=0,Out=6,V>=3] * Chain [63,44,70,73]: 6 with precondition: [V1=2,V2=0,Out=7,V>=3] * Chain [63,44,60,73]: 6 with precondition: [V1=2,V2=0,Out=6,V>=3] * Chain [62,[40,41,42,43],73]: 8*it(40)+1*s(5)+1*s(6)+2 Such that:aux(3) =< V aux(1) =< V/2+1/2 aux(67) =< V/2 it(40) =< aux(3) it(40) =< aux(67) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=4] * Chain [62,[40,41,42,43],61,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(7)+4 Such that:aux(3) =< V aux(8) =< V/2 aux(1) =< V/2+1/2 s(7) =< V/2+3/2 it(40) =< aux(3) it(40) =< aux(8) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=8] * Chain [62,[40,41,42,43],60,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+1/2 aux(68) =< V/2 it(40) =< aux(3) it(40) =< aux(68) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=5] * Chain [62,[40,41,42,43],59,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+1/2 aux(69) =< V/2 it(40) =< aux(3) it(40) =< aux(69) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=7] * Chain [62,[40,41,42,43],58,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(8)+4 Such that:aux(11) =< V aux(5) =< V/2 aux(1) =< V/2+1/2 s(8) =< aux(11) it(40) =< aux(11) it(40) =< aux(5) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=6] * Chain [62,[40,41,42,43],57,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+1/2 aux(70) =< V/2 it(40) =< aux(3) it(40) =< aux(70) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=5] * Chain [62,[40,41,42,43],56,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+1/2 aux(71) =< V/2 it(40) =< aux(3) it(40) =< aux(71) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=7] * Chain [62,[40,41,42,43],55,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(9)+4 Such that:aux(3) =< V aux(14) =< V/2 aux(1) =< V/2+1/2 s(9) =< V/2+3/2 it(40) =< aux(3) it(40) =< aux(14) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=8] * Chain [62,[40,41,42,43],54,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(10)+4 Such that:aux(3) =< V aux(1) =< V/2+1/2 s(10) =< V/2+3/2 aux(72) =< V/2 it(40) =< aux(3) it(40) =< aux(72) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=6] * Chain [62,[40,41,42,43],53,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+1/2 aux(73) =< V/2 it(40) =< aux(3) it(40) =< aux(73) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=5,2*Out>=V+6] * Chain [62,[40,41,42,43],52,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+1/2 aux(74) =< V/2 it(40) =< aux(3) it(40) =< aux(74) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=7,2*Out>=V+10] * Chain [62,[40,41,42,43],51,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(11)+4 Such that:aux(18) =< V aux(5) =< V/2 aux(1) =< V/2+1/2 s(11) =< aux(18) it(40) =< aux(18) it(40) =< aux(5) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=6,2*Out>=V+8] * Chain [62,[40,41,42,43],50,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+1/2 aux(75) =< V/2 it(40) =< aux(3) it(40) =< aux(75) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=5,2*Out>=V+6] * Chain [62,[40,41,42,43],49,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(1) =< V/2+1/2 aux(76) =< V/2 it(40) =< aux(3) it(40) =< aux(76) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=7,2*Out>=V+10] * Chain [62,[40,41,42,43],48,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(12)+4 Such that:aux(21) =< V aux(5) =< V/2 aux(1) =< V/2+1/2 s(12) =< aux(21) it(40) =< aux(21) it(40) =< aux(5) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=3,Out>=6,2*Out>=V+8] * Chain [62,[40,41,42,43],47,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(13)+4 Such that:aux(3) =< V aux(22) =< V/2 aux(1) =< V/2+1/2 s(13) =< V/2+3/2 it(40) =< aux(3) it(40) =< aux(22) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=8] * Chain [62,[40,41,42,43],47,72,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(13)+6 Such that:aux(3) =< V aux(23) =< V/2 aux(1) =< V/2+1/2 s(13) =< V/2+7/2 it(40) =< aux(3) it(40) =< aux(23) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=10] * Chain [62,[40,41,42,43],47,71,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(13)+6 Such that:aux(3) =< V aux(24) =< V/2 aux(1) =< V/2+1/2 s(13) =< V/2+5/2 it(40) =< aux(3) it(40) =< aux(24) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=9] * Chain [62,[40,41,42,43],47,70,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(13)+6 Such that:aux(3) =< V aux(25) =< V/2 aux(1) =< V/2+1/2 s(13) =< V/2+7/2 it(40) =< aux(3) it(40) =< aux(25) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=10] * Chain [62,[40,41,42,43],47,60,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(13)+6 Such that:aux(3) =< V aux(26) =< V/2 aux(1) =< V/2+1/2 s(13) =< V/2+5/2 it(40) =< aux(3) it(40) =< aux(26) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=9] * Chain [62,[40,41,42,43],46,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(14)+4 Such that:aux(3) =< V aux(27) =< V/2 aux(28) =< V/2+1/2 s(14) =< aux(28) it(40) =< aux(3) it(40) =< aux(27) aux(2) =< aux(28) s(5) =< it(40)*aux(28) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=6] * Chain [62,[40,41,42,43],46,72,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(14)+6 Such that:aux(3) =< V aux(29) =< V/2 aux(30) =< V/2+1/2 s(14) =< aux(30) it(40) =< aux(3) it(40) =< aux(29) aux(2) =< aux(30) s(5) =< it(40)*aux(30) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=8] * Chain [62,[40,41,42,43],46,71,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(14)+6 Such that:aux(3) =< V aux(31) =< V/2 aux(32) =< V/2+1/2 s(14) =< aux(32) it(40) =< aux(3) it(40) =< aux(31) aux(2) =< aux(32) s(5) =< it(40)*aux(32) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=7] * Chain [62,[40,41,42,43],46,70,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(14)+6 Such that:aux(3) =< V aux(33) =< V/2 aux(34) =< V/2+1/2 s(14) =< aux(34) it(40) =< aux(3) it(40) =< aux(33) aux(2) =< aux(34) s(5) =< it(40)*aux(34) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=8] * Chain [62,[40,41,42,43],46,60,73]: 8*it(40)+1*s(5)+1*s(6)+1*s(14)+6 Such that:aux(3) =< V aux(35) =< V/2 aux(36) =< V/2+1/2 s(14) =< aux(36) it(40) =< aux(3) it(40) =< aux(35) aux(2) =< aux(36) s(5) =< it(40)*aux(36) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=7] * Chain [62,[40,41,42,43],45,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(37) =< V/2 aux(1) =< V/2+1/2 it(40) =< aux(3) it(40) =< aux(37) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=5] * Chain [62,[40,41,42,43],45,72,73]: 8*it(40)+1*s(5)+1*s(6)+6 Such that:aux(3) =< V aux(38) =< V/2 aux(1) =< V/2+1/2 it(40) =< aux(3) it(40) =< aux(38) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=7] * Chain [62,[40,41,42,43],45,71,73]: 8*it(40)+1*s(5)+1*s(6)+6 Such that:aux(3) =< V aux(39) =< V/2 aux(1) =< V/2+1/2 it(40) =< aux(3) it(40) =< aux(39) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=6] * Chain [62,[40,41,42,43],45,70,73]: 8*it(40)+1*s(5)+1*s(6)+6 Such that:aux(3) =< V aux(40) =< V/2 aux(1) =< V/2+1/2 it(40) =< aux(3) it(40) =< aux(40) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=7] * Chain [62,[40,41,42,43],45,60,73]: 8*it(40)+1*s(5)+1*s(6)+6 Such that:aux(3) =< V aux(41) =< V/2 aux(1) =< V/2+1/2 it(40) =< aux(3) it(40) =< aux(41) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=6] * Chain [62,[40,41,42,43],44,73]: 8*it(40)+1*s(5)+1*s(6)+4 Such that:aux(3) =< V aux(42) =< V/2 aux(1) =< V/2+1/2 it(40) =< aux(3) it(40) =< aux(42) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=7] * Chain [62,[40,41,42,43],44,72,73]: 8*it(40)+1*s(5)+1*s(6)+6 Such that:aux(3) =< V aux(43) =< V/2 aux(1) =< V/2+1/2 it(40) =< aux(3) it(40) =< aux(43) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=9] * Chain [62,[40,41,42,43],44,71,73]: 8*it(40)+1*s(5)+1*s(6)+6 Such that:aux(3) =< V aux(44) =< V/2 aux(1) =< V/2+1/2 it(40) =< aux(3) it(40) =< aux(44) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=8] * Chain [62,[40,41,42,43],44,70,73]: 8*it(40)+1*s(5)+1*s(6)+6 Such that:aux(3) =< V aux(45) =< V/2 aux(1) =< V/2+1/2 it(40) =< aux(3) it(40) =< aux(45) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=9] * Chain [62,[40,41,42,43],44,60,73]: 8*it(40)+1*s(5)+1*s(6)+6 Such that:aux(3) =< V aux(46) =< V/2 aux(1) =< V/2+1/2 it(40) =< aux(3) it(40) =< aux(46) aux(2) =< aux(1) s(5) =< it(40)*aux(1) s(6) =< it(40)*aux(2) with precondition: [V1=2,V2=0,V>=5,Out>=8] * Chain [62,73]: 2 with precondition: [V1=2,V2=0,Out=3,V>=1] * Chain [62,72,73]: 4 with precondition: [V1=2,V=1,V2=0,Out=5] * Chain [62,71,73]: 4 with precondition: [V1=2,V=1,V2=0,Out=4] * Chain [62,70,73]: 4 with precondition: [V1=2,V=1,V2=0,Out=5] * Chain [62,61,73]: 1*s(7)+4 Such that:s(7) =< 3 with precondition: [V1=2,V2=0,Out=6,V>=3] * Chain [62,60,73]: 4 with precondition: [V1=2,V2=0,Out=4,V>=1] * Chain [62,59,73]: 4 with precondition: [V1=2,V2=0,Out=6,V>=2] * Chain [62,58,73]: 1*s(8)+4 Such that:s(8) =< V with precondition: [V1=2,V2=0,Out=5,V>=2] * Chain [62,57,73]: 4 with precondition: [V1=2,V2=0,Out=4,V>=2] * Chain [62,56,73]: 4 with precondition: [V1=2,V2=0,Out=6,V>=2] * Chain [62,55,73]: 1*s(9)+4 Such that:s(9) =< 3 with precondition: [V1=2,V2=0,Out=6,V>=3] * Chain [62,54,73]: 1*s(10)+4 Such that:s(10) =< 2 with precondition: [V1=2,V2=0,Out=5,V>=2] * Chain [62,53,73]: 4 with precondition: [V1=2,V=2,V2=0,Out=4] * Chain [62,52,73]: 4 with precondition: [V1=2,V=2,V2=0,Out=6] * Chain [62,51,73]: 1*s(11)+4 Such that:s(11) =< 1 with precondition: [V1=2,V=2,V2=0,Out=5] * Chain [62,50,73]: 4 with precondition: [V1=2,V=2,V2=0,Out=4] * Chain [62,49,73]: 4 with precondition: [V1=2,V=2,V2=0,Out=6] * Chain [62,48,73]: 1*s(12)+4 Such that:s(12) =< 1 with precondition: [V1=2,V=2,V2=0,Out=5] * Chain [62,47,73]: 1*s(13)+4 Such that:s(13) =< 3 with precondition: [V1=2,V2=0,Out=6,V>=3] * Chain [62,47,72,73]: 1*s(13)+6 Such that:s(13) =< 5 with precondition: [V1=2,V2=0,Out=8,V>=3] * Chain [62,47,71,73]: 1*s(13)+6 Such that:s(13) =< 4 with precondition: [V1=2,V2=0,Out=7,V>=3] * Chain [62,47,70,73]: 1*s(13)+6 Such that:s(13) =< 5 with precondition: [V1=2,V2=0,Out=8,V>=3] * Chain [62,47,60,73]: 1*s(13)+6 Such that:s(13) =< 4 with precondition: [V1=2,V2=0,Out=7,V>=3] * Chain [62,46,73]: 1*s(14)+4 Such that:s(14) =< 2 with precondition: [V1=2,V2=0,Out=5,V>=3] * Chain [62,46,72,73]: 1*s(14)+6 Such that:s(14) =< 2 with precondition: [V1=2,V2=0,Out=7,V>=3] * Chain [62,46,71,73]: 1*s(14)+6 Such that:s(14) =< 2 with precondition: [V1=2,V2=0,Out=6,V>=3] * Chain [62,46,70,73]: 1*s(14)+6 Such that:s(14) =< 2 with precondition: [V1=2,V2=0,Out=7,V>=3] * Chain [62,46,60,73]: 1*s(14)+6 Such that:s(14) =< 2 with precondition: [V1=2,V2=0,Out=6,V>=3] * Chain [62,45,73]: 4 with precondition: [V1=2,V2=0,Out=4,V>=3] * Chain [62,45,72,73]: 6 with precondition: [V1=2,V2=0,Out=6,V>=3] * Chain [62,45,71,73]: 6 with precondition: [V1=2,V2=0,Out=5,V>=3] * Chain [62,45,70,73]: 6 with precondition: [V1=2,V2=0,Out=6,V>=3] * Chain [62,45,60,73]: 6 with precondition: [V1=2,V2=0,Out=5,V>=3] * Chain [62,44,73]: 4 with precondition: [V1=2,V2=0,Out=6,V>=3] * Chain [62,44,72,73]: 6 with precondition: [V1=2,V2=0,Out=8,V>=3] * Chain [62,44,71,73]: 6 with precondition: [V1=2,V2=0,Out=7,V>=3] * Chain [62,44,70,73]: 6 with precondition: [V1=2,V2=0,Out=8,V>=3] * Chain [62,44,60,73]: 6 with precondition: [V1=2,V2=0,Out=7,V>=3] * Chain [61,73]: 1*s(7)+2 Such that:s(7) =< Out with precondition: [V1=2,Out=V2+2,Out>=3,V+1>=Out] * Chain [60,73]: 2 with precondition: [V1=2,Out=1,V>=0,V2>=0] * Chain [59,73]: 2 with precondition: [V1=2,Out=3,V>=1,V2>=0] * Chain [58,73]: 1*s(8)+2 Such that:s(8) =< V with precondition: [V1=2,Out>=2,V+1>=Out,V2+1>=Out] * Chain [57,73]: 2 with precondition: [V1=2,Out=1,V>=1,V2>=0] * Chain [56,73]: 2 with precondition: [V1=2,Out=3,V>=1,V2>=0] * Chain [55,73]: 1*s(9)+2 Such that:s(9) =< Out with precondition: [V1=2,Out=V2+2,Out>=3,V+1>=Out] * Chain [54,73]: 1*s(10)+2 Such that:s(10) =< V2+1 with precondition: [V1=2,Out>=2,V+1>=Out,V2+1>=Out] * Chain [53,73]: 2 with precondition: [V1=2,Out=1,V>=1,V2>=V] * Chain [52,73]: 2 with precondition: [V1=2,Out=3,V>=1,V2>=V] * Chain [51,73]: 1*s(11)+2 Such that:s(11) =< V with precondition: [V1=2,Out>=2,V2>=V,V+1>=Out] * Chain [50,73]: 2 with precondition: [V1=2,Out=1,V>=1,V2>=V] * Chain [49,73]: 2 with precondition: [V1=2,Out=3,V>=1,V2>=V] * Chain [48,73]: 1*s(12)+2 Such that:s(12) =< V with precondition: [V1=2,Out>=2,V2>=V,V+1>=Out] * Chain [47,73]: 1*s(13)+2 Such that:s(13) =< Out with precondition: [V1=2,Out=V2+2,Out>=3,V+1>=Out] * Chain [47,72,73]: 1*s(13)+4 Such that:s(13) =< Out with precondition: [V1=2,Out=V2+4,Out>=5,V+3>=Out] * Chain [47,71,73]: 1*s(13)+4 Such that:s(13) =< Out with precondition: [V1=2,Out=V2+3,Out>=4,V+2>=Out] * Chain [47,70,73]: 1*s(13)+4 Such that:s(13) =< Out with precondition: [V1=2,Out=V2+4,Out>=5,V+3>=Out] * Chain [47,60,73]: 1*s(13)+4 Such that:s(13) =< Out with precondition: [V1=2,Out=V2+3,Out>=4,V+2>=Out] * Chain [46,73]: 1*s(14)+2 Such that:s(14) =< V2+1 with precondition: [V1=2,Out>=2,V>=V2+1,V2+1>=Out] * Chain [46,72,73]: 1*s(14)+4 Such that:s(14) =< V2+1 with precondition: [V1=2,Out>=4,V>=V2+1,V2+3>=Out] * Chain [46,71,73]: 1*s(14)+4 Such that:s(14) =< V2+1 with precondition: [V1=2,Out>=3,V>=V2+1,V2+2>=Out] * Chain [46,70,73]: 1*s(14)+4 Such that:s(14) =< V2+1 with precondition: [V1=2,Out>=4,V>=V2+1,V2+3>=Out] * Chain [46,60,73]: 1*s(14)+4 Such that:s(14) =< V2+1 with precondition: [V1=2,Out>=3,V>=V2+1,V2+2>=Out] * Chain [45,73]: 2 with precondition: [V1=2,Out=1,V2>=1,V>=V2+1] * Chain [45,72,73]: 4 with precondition: [V1=2,Out=3,V2>=1,V>=V2+1] * Chain [45,71,73]: 4 with precondition: [V1=2,Out=2,V2>=1,V>=V2+1] * Chain [45,70,73]: 4 with precondition: [V1=2,Out=3,V2>=1,V>=V2+1] * Chain [45,60,73]: 4 with precondition: [V1=2,Out=2,V2>=1,V>=V2+1] * Chain [44,73]: 2 with precondition: [V1=2,Out=3,V2>=1,V>=V2+1] * Chain [44,72,73]: 4 with precondition: [V1=2,Out=5,V2>=1,V>=V2+1] * Chain [44,71,73]: 4 with precondition: [V1=2,Out=4,V2>=1,V>=V2+1] * Chain [44,70,73]: 4 with precondition: [V1=2,Out=5,V2>=1,V>=V2+1] * Chain [44,60,73]: 4 with precondition: [V1=2,Out=4,V2>=1,V>=V2+1] #### Cost of chains of start(V1,V,V2): * Chain [77]: 1*s(1133)+1*s(1134)+1 Such that:s(1134) =< V s(1133) =< V+1 with precondition: [V1>=0] * Chain [76]: 7*s(1135)+2*s(1137)+4*s(1146)+2*s(1147)+2*s(1148)+6*s(1149)+200*s(1150)+25*s(1152)+25*s(1153)+5*s(1154)+80*s(1155)+10*s(1156)+10*s(1157)+3*s(1160)+2*s(1162)+2*s(1164)+6 Such that:s(1136) =< 2 s(1139) =< V/2-V2/2 s(1140) =< V/2-V2/2+1/2 s(1141) =< V/2+V2/2+1/2 s(1142) =< V/2+V2/2+3/2 s(1143) =< V/2+V2/2+5/2 s(1144) =< V/2+V2/2+7/2 s(1159) =< V2+2 s(1161) =< V2+3 s(1163) =< V2+4 aux(112) =< V aux(113) =< V2+1 s(1135) =< aux(112) s(1149) =< aux(113) s(1137) =< s(1136) s(1146) =< s(1142) s(1147) =< s(1143) s(1148) =< s(1144) s(1150) =< aux(112) s(1150) =< s(1139) s(1151) =< s(1141) s(1152) =< s(1150)*s(1141) s(1153) =< s(1150)*s(1151) s(1154) =< s(1141) s(1155) =< aux(112) s(1155) =< s(1140) s(1155) =< s(1139) s(1156) =< s(1155)*s(1141) s(1157) =< s(1155)*s(1151) s(1160) =< s(1159) s(1162) =< s(1161) s(1164) =< s(1163) with precondition: [V1=2,V>=0,V2>=0] * Chain [75]: 11*s(1168)+12*s(1171)+6*s(1172)+4*s(1179)+2*s(1191)+12*s(1192)+6*s(1193)+6*s(1194)+840*s(1195)+105*s(1197)+105*s(1198)+15*s(1199)+41 Such that:s(1182) =< 5 s(1184) =< V/2 s(1185) =< V/2+1/2 s(1186) =< V/2+3/2 s(1187) =< V/2+5/2 s(1188) =< V/2+7/2 aux(114) =< 2 aux(115) =< 3 aux(116) =< 4 aux(117) =< V s(1168) =< aux(117) s(1171) =< aux(114) s(1172) =< aux(115) s(1179) =< aux(116) s(1191) =< s(1182) s(1192) =< s(1186) s(1193) =< s(1187) s(1194) =< s(1188) s(1195) =< aux(117) s(1195) =< s(1184) s(1196) =< s(1185) s(1197) =< s(1195)*s(1185) s(1198) =< s(1195)*s(1196) s(1199) =< s(1185) with precondition: [V1=2,V2=0,V>=1] * Chain [74]: 1 with precondition: [V=0,V1>=1] Closed-form bounds of start(V1,V,V2): ------------------------------------- * Chain [77] with precondition: [V1>=0] - Upper bound: nat(V)+1+nat(V+1) - Complexity: n * Chain [76] with precondition: [V1=2,V>=0,V2>=0] - Upper bound: 287*V+10+(V/2+V2/2+1/2)*(70*V)+(6*V2+6)+(3*V2+6)+(2*V2+6)+(2*V2+8)+(5/2*V+5/2*V2+5/2)+(2*V+2*V2+6)+(V+V2+5)+(V+V2+7) - Complexity: n^2 * Chain [75] with precondition: [V1=2,V2=0,V>=1] - Upper bound: 851*V+109+(V/2+1/2)*(210*V)+(15/2*V+15/2)+(6*V+18)+(3*V+15)+(3*V+21) - Complexity: n^2 * Chain [74] with precondition: [V=0,V1>=1] - Upper bound: 1 - Complexity: constant ### Maximum cost of start(V1,V,V2): nat(V)+max([nat(V+1),nat(V)*286+9+max([nat(V)*564+99+nat(V)*210*nat(V/2+1/2)+nat(V/2+1/2)*15+nat(V/2+3/2)*12+nat(V/2+5/2)*6+nat(V/2+7/2)*6,nat(V)*70*nat(V/2+V2/2+1/2)+nat(V2+1)*6+nat(V2+2)*3+nat(V2+3)*2+nat(V2+4)*2+nat(V/2+V2/2+1/2)*5+nat(V/2+V2/2+3/2)*4+nat(V/2+V2/2+5/2)*2+nat(V/2+V2/2+7/2)*2])])+1 Asymptotic class: n^2 * Total analysis performed in 5287 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, z1) -> c(COND(gr(z0, z1), p(z0), s(z1)), GR(z0, z1)) COND(true, z0, z1) -> c1(COND(gr(z0, z1), p(z0), s(z1)), P(z0)) GR(0', z0) -> c2 GR(s(z0), 0') -> c3 GR(s(z0), s(z1)) -> c4(GR(z0, z1)) P(0') -> c5 P(s(z0)) -> c6 The (relative) TRS S consists of the following rules: cond(true, z0, z1) -> cond(gr(z0, z1), p(z0), s(z1)) gr(0', z0) -> false gr(s(z0), 0') -> true gr(s(z0), s(z1)) -> gr(z0, z1) 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, z1) -> c(COND(gr(z0, z1), p(z0), s(z1)), GR(z0, z1)) COND(true, z0, z1) -> c1(COND(gr(z0, z1), p(z0), s(z1)), P(z0)) GR(0', z0) -> c2 GR(s(z0), 0') -> c3 GR(s(z0), s(z1)) -> c4(GR(z0, z1)) P(0') -> c5 P(s(z0)) -> c6 cond(true, z0, z1) -> cond(gr(z0, z1), p(z0), s(z1)) gr(0', z0) -> false gr(s(z0), 0') -> true gr(s(z0), s(z1)) -> gr(z0, z1) p(0') -> 0' p(s(z0)) -> z0 Types: COND :: true:false -> s:0' -> s:0' -> c:c1 true :: true:false c :: c:c1 -> c2:c3:c4 -> c:c1 gr :: s:0' -> s:0' -> true:false p :: s:0' -> s:0' s :: s:0' -> s:0' GR :: s:0' -> s:0' -> c2:c3:c4 c1 :: c:c1 -> c5:c6 -> c:c1 P :: s:0' -> c5:c6 0' :: s:0' c2 :: c2:c3:c4 c3 :: c2:c3:c4 c4 :: c2:c3:c4 -> c2:c3:c4 c5 :: c5:c6 c6 :: c5:c6 cond :: true:false -> s:0' -> s:0' -> cond false :: true:false hole_c:c11_7 :: c:c1 hole_true:false2_7 :: true:false hole_s:0'3_7 :: s:0' hole_c2:c3:c44_7 :: c2:c3:c4 hole_c5:c65_7 :: c5:c6 hole_cond6_7 :: cond gen_c:c17_7 :: Nat -> c:c1 gen_s:0'8_7 :: Nat -> s:0' gen_c2:c3:c49_7 :: Nat -> c2:c3:c4 ---------------------------------------- (17) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: COND, gr, GR, cond They will be analysed ascendingly in the following order: gr < COND GR < COND gr < cond ---------------------------------------- (18) Obligation: Innermost TRS: Rules: COND(true, z0, z1) -> c(COND(gr(z0, z1), p(z0), s(z1)), GR(z0, z1)) COND(true, z0, z1) -> c1(COND(gr(z0, z1), p(z0), s(z1)), P(z0)) GR(0', z0) -> c2 GR(s(z0), 0') -> c3 GR(s(z0), s(z1)) -> c4(GR(z0, z1)) P(0') -> c5 P(s(z0)) -> c6 cond(true, z0, z1) -> cond(gr(z0, z1), p(z0), s(z1)) gr(0', z0) -> false gr(s(z0), 0') -> true gr(s(z0), s(z1)) -> gr(z0, z1) p(0') -> 0' p(s(z0)) -> z0 Types: COND :: true:false -> s:0' -> s:0' -> c:c1 true :: true:false c :: c:c1 -> c2:c3:c4 -> c:c1 gr :: s:0' -> s:0' -> true:false p :: s:0' -> s:0' s :: s:0' -> s:0' GR :: s:0' -> s:0' -> c2:c3:c4 c1 :: c:c1 -> c5:c6 -> c:c1 P :: s:0' -> c5:c6 0' :: s:0' c2 :: c2:c3:c4 c3 :: c2:c3:c4 c4 :: c2:c3:c4 -> c2:c3:c4 c5 :: c5:c6 c6 :: c5:c6 cond :: true:false -> s:0' -> s:0' -> cond false :: true:false hole_c:c11_7 :: c:c1 hole_true:false2_7 :: true:false hole_s:0'3_7 :: s:0' hole_c2:c3:c44_7 :: c2:c3:c4 hole_c5:c65_7 :: c5:c6 hole_cond6_7 :: cond gen_c:c17_7 :: Nat -> c:c1 gen_s:0'8_7 :: Nat -> s:0' gen_c2:c3:c49_7 :: Nat -> c2:c3:c4 Generator Equations: gen_c:c17_7(0) <=> hole_c:c11_7 gen_c:c17_7(+(x, 1)) <=> c(gen_c:c17_7(x), c2) gen_s:0'8_7(0) <=> 0' gen_s:0'8_7(+(x, 1)) <=> s(gen_s:0'8_7(x)) gen_c2:c3:c49_7(0) <=> c2 gen_c2:c3:c49_7(+(x, 1)) <=> c4(gen_c2:c3:c49_7(x)) The following defined symbols remain to be analysed: gr, COND, GR, cond They will be analysed ascendingly in the following order: gr < COND GR < COND gr < cond ---------------------------------------- (19) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: gr(gen_s:0'8_7(n11_7), gen_s:0'8_7(n11_7)) -> false, rt in Omega(0) Induction Base: gr(gen_s:0'8_7(0), gen_s:0'8_7(0)) ->_R^Omega(0) false Induction Step: gr(gen_s:0'8_7(+(n11_7, 1)), gen_s:0'8_7(+(n11_7, 1))) ->_R^Omega(0) gr(gen_s:0'8_7(n11_7), gen_s:0'8_7(n11_7)) ->_IH false 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, z1) -> c(COND(gr(z0, z1), p(z0), s(z1)), GR(z0, z1)) COND(true, z0, z1) -> c1(COND(gr(z0, z1), p(z0), s(z1)), P(z0)) GR(0', z0) -> c2 GR(s(z0), 0') -> c3 GR(s(z0), s(z1)) -> c4(GR(z0, z1)) P(0') -> c5 P(s(z0)) -> c6 cond(true, z0, z1) -> cond(gr(z0, z1), p(z0), s(z1)) gr(0', z0) -> false gr(s(z0), 0') -> true gr(s(z0), s(z1)) -> gr(z0, z1) p(0') -> 0' p(s(z0)) -> z0 Types: COND :: true:false -> s:0' -> s:0' -> c:c1 true :: true:false c :: c:c1 -> c2:c3:c4 -> c:c1 gr :: s:0' -> s:0' -> true:false p :: s:0' -> s:0' s :: s:0' -> s:0' GR :: s:0' -> s:0' -> c2:c3:c4 c1 :: c:c1 -> c5:c6 -> c:c1 P :: s:0' -> c5:c6 0' :: s:0' c2 :: c2:c3:c4 c3 :: c2:c3:c4 c4 :: c2:c3:c4 -> c2:c3:c4 c5 :: c5:c6 c6 :: c5:c6 cond :: true:false -> s:0' -> s:0' -> cond false :: true:false hole_c:c11_7 :: c:c1 hole_true:false2_7 :: true:false hole_s:0'3_7 :: s:0' hole_c2:c3:c44_7 :: c2:c3:c4 hole_c5:c65_7 :: c5:c6 hole_cond6_7 :: cond gen_c:c17_7 :: Nat -> c:c1 gen_s:0'8_7 :: Nat -> s:0' gen_c2:c3:c49_7 :: Nat -> c2:c3:c4 Lemmas: gr(gen_s:0'8_7(n11_7), gen_s:0'8_7(n11_7)) -> false, rt in Omega(0) Generator Equations: gen_c:c17_7(0) <=> hole_c:c11_7 gen_c:c17_7(+(x, 1)) <=> c(gen_c:c17_7(x), c2) gen_s:0'8_7(0) <=> 0' gen_s:0'8_7(+(x, 1)) <=> s(gen_s:0'8_7(x)) gen_c2:c3:c49_7(0) <=> c2 gen_c2:c3:c49_7(+(x, 1)) <=> c4(gen_c2:c3:c49_7(x)) The following defined symbols remain to be analysed: GR, COND, cond They will be analysed ascendingly in the following order: GR < COND ---------------------------------------- (21) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: GR(gen_s:0'8_7(n296_7), gen_s:0'8_7(n296_7)) -> gen_c2:c3:c49_7(n296_7), rt in Omega(1 + n296_7) Induction Base: GR(gen_s:0'8_7(0), gen_s:0'8_7(0)) ->_R^Omega(1) c2 Induction Step: GR(gen_s:0'8_7(+(n296_7, 1)), gen_s:0'8_7(+(n296_7, 1))) ->_R^Omega(1) c4(GR(gen_s:0'8_7(n296_7), gen_s:0'8_7(n296_7))) ->_IH c4(gen_c2:c3:c49_7(c297_7)) 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, z1) -> c(COND(gr(z0, z1), p(z0), s(z1)), GR(z0, z1)) COND(true, z0, z1) -> c1(COND(gr(z0, z1), p(z0), s(z1)), P(z0)) GR(0', z0) -> c2 GR(s(z0), 0') -> c3 GR(s(z0), s(z1)) -> c4(GR(z0, z1)) P(0') -> c5 P(s(z0)) -> c6 cond(true, z0, z1) -> cond(gr(z0, z1), p(z0), s(z1)) gr(0', z0) -> false gr(s(z0), 0') -> true gr(s(z0), s(z1)) -> gr(z0, z1) p(0') -> 0' p(s(z0)) -> z0 Types: COND :: true:false -> s:0' -> s:0' -> c:c1 true :: true:false c :: c:c1 -> c2:c3:c4 -> c:c1 gr :: s:0' -> s:0' -> true:false p :: s:0' -> s:0' s :: s:0' -> s:0' GR :: s:0' -> s:0' -> c2:c3:c4 c1 :: c:c1 -> c5:c6 -> c:c1 P :: s:0' -> c5:c6 0' :: s:0' c2 :: c2:c3:c4 c3 :: c2:c3:c4 c4 :: c2:c3:c4 -> c2:c3:c4 c5 :: c5:c6 c6 :: c5:c6 cond :: true:false -> s:0' -> s:0' -> cond false :: true:false hole_c:c11_7 :: c:c1 hole_true:false2_7 :: true:false hole_s:0'3_7 :: s:0' hole_c2:c3:c44_7 :: c2:c3:c4 hole_c5:c65_7 :: c5:c6 hole_cond6_7 :: cond gen_c:c17_7 :: Nat -> c:c1 gen_s:0'8_7 :: Nat -> s:0' gen_c2:c3:c49_7 :: Nat -> c2:c3:c4 Lemmas: gr(gen_s:0'8_7(n11_7), gen_s:0'8_7(n11_7)) -> false, rt in Omega(0) Generator Equations: gen_c:c17_7(0) <=> hole_c:c11_7 gen_c:c17_7(+(x, 1)) <=> c(gen_c:c17_7(x), c2) gen_s:0'8_7(0) <=> 0' gen_s:0'8_7(+(x, 1)) <=> s(gen_s:0'8_7(x)) gen_c2:c3:c49_7(0) <=> c2 gen_c2:c3:c49_7(+(x, 1)) <=> c4(gen_c2:c3:c49_7(x)) The following defined symbols remain to be analysed: GR, COND, cond They will be analysed ascendingly in the following order: GR < COND ---------------------------------------- (24) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (25) BOUNDS(n^1, INF) ---------------------------------------- (26) Obligation: Innermost TRS: Rules: COND(true, z0, z1) -> c(COND(gr(z0, z1), p(z0), s(z1)), GR(z0, z1)) COND(true, z0, z1) -> c1(COND(gr(z0, z1), p(z0), s(z1)), P(z0)) GR(0', z0) -> c2 GR(s(z0), 0') -> c3 GR(s(z0), s(z1)) -> c4(GR(z0, z1)) P(0') -> c5 P(s(z0)) -> c6 cond(true, z0, z1) -> cond(gr(z0, z1), p(z0), s(z1)) gr(0', z0) -> false gr(s(z0), 0') -> true gr(s(z0), s(z1)) -> gr(z0, z1) p(0') -> 0' p(s(z0)) -> z0 Types: COND :: true:false -> s:0' -> s:0' -> c:c1 true :: true:false c :: c:c1 -> c2:c3:c4 -> c:c1 gr :: s:0' -> s:0' -> true:false p :: s:0' -> s:0' s :: s:0' -> s:0' GR :: s:0' -> s:0' -> c2:c3:c4 c1 :: c:c1 -> c5:c6 -> c:c1 P :: s:0' -> c5:c6 0' :: s:0' c2 :: c2:c3:c4 c3 :: c2:c3:c4 c4 :: c2:c3:c4 -> c2:c3:c4 c5 :: c5:c6 c6 :: c5:c6 cond :: true:false -> s:0' -> s:0' -> cond false :: true:false hole_c:c11_7 :: c:c1 hole_true:false2_7 :: true:false hole_s:0'3_7 :: s:0' hole_c2:c3:c44_7 :: c2:c3:c4 hole_c5:c65_7 :: c5:c6 hole_cond6_7 :: cond gen_c:c17_7 :: Nat -> c:c1 gen_s:0'8_7 :: Nat -> s:0' gen_c2:c3:c49_7 :: Nat -> c2:c3:c4 Lemmas: gr(gen_s:0'8_7(n11_7), gen_s:0'8_7(n11_7)) -> false, rt in Omega(0) GR(gen_s:0'8_7(n296_7), gen_s:0'8_7(n296_7)) -> gen_c2:c3:c49_7(n296_7), rt in Omega(1 + n296_7) Generator Equations: gen_c:c17_7(0) <=> hole_c:c11_7 gen_c:c17_7(+(x, 1)) <=> c(gen_c:c17_7(x), c2) gen_s:0'8_7(0) <=> 0' gen_s:0'8_7(+(x, 1)) <=> s(gen_s:0'8_7(x)) gen_c2:c3:c49_7(0) <=> c2 gen_c2:c3:c49_7(+(x, 1)) <=> c4(gen_c2:c3:c49_7(x)) The following defined symbols remain to be analysed: COND, cond