WORST_CASE(Omega(n^1),O(n^1)) 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^1). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 1413 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, 17.4 s] (12) BOUNDS(1, n^1) (13) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (14) CpxRelTRS (15) SlicingProof [LOWER BOUND(ID), 0 ms] (16) CpxRelTRS (17) TypeInferenceProof [BOTH BOUNDS(ID, ID), 4 ms] (18) typed CpxTrs (19) OrderProof [LOWER BOUND(ID), 24 ms] (20) typed CpxTrs (21) RewriteLemmaProof [LOWER BOUND(ID), 342 ms] (22) BEST (23) proven lower bound (24) LowerBoundPropagationProof [FINISHED, 0 ms] (25) BOUNDS(n^1, INF) (26) typed CpxTrs (27) RewriteLemmaProof [LOWER BOUND(ID), 67 ms] (28) typed CpxTrs (29) RewriteLemmaProof [LOWER BOUND(ID), 29 ms] (30) typed CpxTrs (31) RewriteLemmaProof [LOWER BOUND(ID), 65 ms] (32) typed CpxTrs ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: GE(z0, 0) -> c GE(0, s(z0)) -> c1 GE(s(z0), s(z1)) -> c2(GE(z0, z1)) MINUS(z0, 0) -> c3 MINUS(0, z0) -> c4 MINUS(s(z0), s(z1)) -> c5(MINUS(z0, z1)) ID_INC(z0) -> c6 ID_INC(z0) -> c7 QUOT(z0, z1) -> c8(DIV(z0, z1, 0)) DIV(z0, z1, z2) -> c9(IF(ge(z1, s(0)), ge(z0, z1), z0, z1, z2), GE(z1, s(0))) DIV(z0, z1, z2) -> c10(IF(ge(z1, s(0)), ge(z0, z1), z0, z1, z2), GE(z0, z1)) IF(false, z0, z1, z2, z3) -> c11 IF(true, false, z0, z1, z2) -> c12 IF(true, true, z0, z1, z2) -> c13(DIV(minus(z0, z1), z1, id_inc(z2)), MINUS(z0, z1)) IF(true, true, z0, z1, z2) -> c14(DIV(minus(z0, z1), z1, id_inc(z2)), ID_INC(z2)) The (relative) TRS S consists of the following rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) minus(z0, 0) -> z0 minus(0, z0) -> 0 minus(s(z0), s(z1)) -> minus(z0, z1) id_inc(z0) -> z0 id_inc(z0) -> s(z0) quot(z0, z1) -> div(z0, z1, 0) div(z0, z1, z2) -> if(ge(z1, s(0)), ge(z0, z1), z0, z1, z2) if(false, z0, z1, z2, z3) -> div_by_zero if(true, false, z0, z1, z2) -> z2 if(true, true, z0, z1, z2) -> div(minus(z0, z1), z1, id_inc(z2)) Rewrite Strategy: INNERMOST ---------------------------------------- (1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID)) proved innermost termination of relative rules ---------------------------------------- (2) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: GE(z0, 0) -> c GE(0, s(z0)) -> c1 GE(s(z0), s(z1)) -> c2(GE(z0, z1)) MINUS(z0, 0) -> c3 MINUS(0, z0) -> c4 MINUS(s(z0), s(z1)) -> c5(MINUS(z0, z1)) ID_INC(z0) -> c6 ID_INC(z0) -> c7 QUOT(z0, z1) -> c8(DIV(z0, z1, 0)) DIV(z0, z1, z2) -> c9(IF(ge(z1, s(0)), ge(z0, z1), z0, z1, z2), GE(z1, s(0))) DIV(z0, z1, z2) -> c10(IF(ge(z1, s(0)), ge(z0, z1), z0, z1, z2), GE(z0, z1)) IF(false, z0, z1, z2, z3) -> c11 IF(true, false, z0, z1, z2) -> c12 IF(true, true, z0, z1, z2) -> c13(DIV(minus(z0, z1), z1, id_inc(z2)), MINUS(z0, z1)) IF(true, true, z0, z1, z2) -> c14(DIV(minus(z0, z1), z1, id_inc(z2)), ID_INC(z2)) The (relative) TRS S consists of the following rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) minus(z0, 0) -> z0 minus(0, z0) -> 0 minus(s(z0), s(z1)) -> minus(z0, z1) id_inc(z0) -> z0 id_inc(z0) -> s(z0) quot(z0, z1) -> div(z0, z1, 0) div(z0, z1, z2) -> if(ge(z1, s(0)), ge(z0, z1), z0, z1, z2) if(false, z0, z1, z2, z3) -> div_by_zero if(true, false, z0, z1, z2) -> z2 if(true, true, z0, z1, z2) -> div(minus(z0, z1), z1, id_inc(z2)) Rewrite Strategy: INNERMOST ---------------------------------------- (3) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID)) Transformed relative TRS to weighted TRS ---------------------------------------- (4) Obligation: The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1). The TRS R consists of the following rules: GE(z0, 0) -> c [1] GE(0, s(z0)) -> c1 [1] GE(s(z0), s(z1)) -> c2(GE(z0, z1)) [1] MINUS(z0, 0) -> c3 [1] MINUS(0, z0) -> c4 [1] MINUS(s(z0), s(z1)) -> c5(MINUS(z0, z1)) [1] ID_INC(z0) -> c6 [1] ID_INC(z0) -> c7 [1] QUOT(z0, z1) -> c8(DIV(z0, z1, 0)) [1] DIV(z0, z1, z2) -> c9(IF(ge(z1, s(0)), ge(z0, z1), z0, z1, z2), GE(z1, s(0))) [1] DIV(z0, z1, z2) -> c10(IF(ge(z1, s(0)), ge(z0, z1), z0, z1, z2), GE(z0, z1)) [1] IF(false, z0, z1, z2, z3) -> c11 [1] IF(true, false, z0, z1, z2) -> c12 [1] IF(true, true, z0, z1, z2) -> c13(DIV(minus(z0, z1), z1, id_inc(z2)), MINUS(z0, z1)) [1] IF(true, true, z0, z1, z2) -> c14(DIV(minus(z0, z1), z1, id_inc(z2)), ID_INC(z2)) [1] ge(z0, 0) -> true [0] ge(0, s(z0)) -> false [0] ge(s(z0), s(z1)) -> ge(z0, z1) [0] minus(z0, 0) -> z0 [0] minus(0, z0) -> 0 [0] minus(s(z0), s(z1)) -> minus(z0, z1) [0] id_inc(z0) -> z0 [0] id_inc(z0) -> s(z0) [0] quot(z0, z1) -> div(z0, z1, 0) [0] div(z0, z1, z2) -> if(ge(z1, s(0)), ge(z0, z1), z0, z1, z2) [0] if(false, z0, z1, z2, z3) -> div_by_zero [0] if(true, false, z0, z1, z2) -> z2 [0] if(true, true, z0, z1, z2) -> div(minus(z0, z1), z1, id_inc(z2)) [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: GE(z0, 0) -> c [1] GE(0, s(z0)) -> c1 [1] GE(s(z0), s(z1)) -> c2(GE(z0, z1)) [1] MINUS(z0, 0) -> c3 [1] MINUS(0, z0) -> c4 [1] MINUS(s(z0), s(z1)) -> c5(MINUS(z0, z1)) [1] ID_INC(z0) -> c6 [1] ID_INC(z0) -> c7 [1] QUOT(z0, z1) -> c8(DIV(z0, z1, 0)) [1] DIV(z0, z1, z2) -> c9(IF(ge(z1, s(0)), ge(z0, z1), z0, z1, z2), GE(z1, s(0))) [1] DIV(z0, z1, z2) -> c10(IF(ge(z1, s(0)), ge(z0, z1), z0, z1, z2), GE(z0, z1)) [1] IF(false, z0, z1, z2, z3) -> c11 [1] IF(true, false, z0, z1, z2) -> c12 [1] IF(true, true, z0, z1, z2) -> c13(DIV(minus(z0, z1), z1, id_inc(z2)), MINUS(z0, z1)) [1] IF(true, true, z0, z1, z2) -> c14(DIV(minus(z0, z1), z1, id_inc(z2)), ID_INC(z2)) [1] ge(z0, 0) -> true [0] ge(0, s(z0)) -> false [0] ge(s(z0), s(z1)) -> ge(z0, z1) [0] minus(z0, 0) -> z0 [0] minus(0, z0) -> 0 [0] minus(s(z0), s(z1)) -> minus(z0, z1) [0] id_inc(z0) -> z0 [0] id_inc(z0) -> s(z0) [0] quot(z0, z1) -> div(z0, z1, 0) [0] div(z0, z1, z2) -> if(ge(z1, s(0)), ge(z0, z1), z0, z1, z2) [0] if(false, z0, z1, z2, z3) -> div_by_zero [0] if(true, false, z0, z1, z2) -> z2 [0] if(true, true, z0, z1, z2) -> div(minus(z0, z1), z1, id_inc(z2)) [0] The TRS has the following type information: GE :: 0:s:div_by_zero -> 0:s:div_by_zero -> c:c1:c2 0 :: 0:s:div_by_zero c :: c:c1:c2 s :: 0:s:div_by_zero -> 0:s:div_by_zero c1 :: c:c1:c2 c2 :: c:c1:c2 -> c:c1:c2 MINUS :: 0:s:div_by_zero -> 0:s:div_by_zero -> c3:c4:c5 c3 :: c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 -> c3:c4:c5 ID_INC :: 0:s:div_by_zero -> c6:c7 c6 :: c6:c7 c7 :: c6:c7 QUOT :: 0:s:div_by_zero -> 0:s:div_by_zero -> c8 c8 :: c9:c10 -> c8 DIV :: 0:s:div_by_zero -> 0:s:div_by_zero -> 0:s:div_by_zero -> c9:c10 c9 :: c11:c12:c13:c14 -> c:c1:c2 -> c9:c10 IF :: false:true -> false:true -> 0:s:div_by_zero -> 0:s:div_by_zero -> 0:s:div_by_zero -> c11:c12:c13:c14 ge :: 0:s:div_by_zero -> 0:s:div_by_zero -> false:true c10 :: c11:c12:c13:c14 -> c:c1:c2 -> c9:c10 false :: false:true c11 :: c11:c12:c13:c14 true :: false:true c12 :: c11:c12:c13:c14 c13 :: c9:c10 -> c3:c4:c5 -> c11:c12:c13:c14 minus :: 0:s:div_by_zero -> 0:s:div_by_zero -> 0:s:div_by_zero id_inc :: 0:s:div_by_zero -> 0:s:div_by_zero c14 :: c9:c10 -> c6:c7 -> c11:c12:c13:c14 quot :: 0:s:div_by_zero -> 0:s:div_by_zero -> 0:s:div_by_zero div :: 0:s:div_by_zero -> 0:s:div_by_zero -> 0:s:div_by_zero -> 0:s:div_by_zero if :: false:true -> false:true -> 0:s:div_by_zero -> 0:s:div_by_zero -> 0:s:div_by_zero -> 0:s:div_by_zero div_by_zero :: 0:s:div_by_zero 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: ge(v0, v1) -> null_ge [0] minus(v0, v1) -> null_minus [0] id_inc(v0) -> null_id_inc [0] quot(v0, v1) -> null_quot [0] div(v0, v1, v2) -> null_div [0] if(v0, v1, v2, v3, v4) -> null_if [0] GE(v0, v1) -> null_GE [0] MINUS(v0, v1) -> null_MINUS [0] IF(v0, v1, v2, v3, v4) -> null_IF [0] And the following fresh constants: null_ge, null_minus, null_id_inc, null_quot, null_div, null_if, null_GE, null_MINUS, null_IF, const, const1 ---------------------------------------- (8) Obligation: Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: GE(z0, 0) -> c [1] GE(0, s(z0)) -> c1 [1] GE(s(z0), s(z1)) -> c2(GE(z0, z1)) [1] MINUS(z0, 0) -> c3 [1] MINUS(0, z0) -> c4 [1] MINUS(s(z0), s(z1)) -> c5(MINUS(z0, z1)) [1] ID_INC(z0) -> c6 [1] ID_INC(z0) -> c7 [1] QUOT(z0, z1) -> c8(DIV(z0, z1, 0)) [1] DIV(z0, z1, z2) -> c9(IF(ge(z1, s(0)), ge(z0, z1), z0, z1, z2), GE(z1, s(0))) [1] DIV(z0, z1, z2) -> c10(IF(ge(z1, s(0)), ge(z0, z1), z0, z1, z2), GE(z0, z1)) [1] IF(false, z0, z1, z2, z3) -> c11 [1] IF(true, false, z0, z1, z2) -> c12 [1] IF(true, true, z0, z1, z2) -> c13(DIV(minus(z0, z1), z1, id_inc(z2)), MINUS(z0, z1)) [1] IF(true, true, z0, z1, z2) -> c14(DIV(minus(z0, z1), z1, id_inc(z2)), ID_INC(z2)) [1] ge(z0, 0) -> true [0] ge(0, s(z0)) -> false [0] ge(s(z0), s(z1)) -> ge(z0, z1) [0] minus(z0, 0) -> z0 [0] minus(0, z0) -> 0 [0] minus(s(z0), s(z1)) -> minus(z0, z1) [0] id_inc(z0) -> z0 [0] id_inc(z0) -> s(z0) [0] quot(z0, z1) -> div(z0, z1, 0) [0] div(z0, z1, z2) -> if(ge(z1, s(0)), ge(z0, z1), z0, z1, z2) [0] if(false, z0, z1, z2, z3) -> div_by_zero [0] if(true, false, z0, z1, z2) -> z2 [0] if(true, true, z0, z1, z2) -> div(minus(z0, z1), z1, id_inc(z2)) [0] ge(v0, v1) -> null_ge [0] minus(v0, v1) -> null_minus [0] id_inc(v0) -> null_id_inc [0] quot(v0, v1) -> null_quot [0] div(v0, v1, v2) -> null_div [0] if(v0, v1, v2, v3, v4) -> null_if [0] GE(v0, v1) -> null_GE [0] MINUS(v0, v1) -> null_MINUS [0] IF(v0, v1, v2, v3, v4) -> null_IF [0] The TRS has the following type information: GE :: 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if -> c:c1:c2:null_GE 0 :: 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if c :: c:c1:c2:null_GE s :: 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if c1 :: c:c1:c2:null_GE c2 :: c:c1:c2:null_GE -> c:c1:c2:null_GE MINUS :: 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if -> c3:c4:c5:null_MINUS c3 :: c3:c4:c5:null_MINUS c4 :: c3:c4:c5:null_MINUS c5 :: c3:c4:c5:null_MINUS -> c3:c4:c5:null_MINUS ID_INC :: 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if -> c6:c7 c6 :: c6:c7 c7 :: c6:c7 QUOT :: 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if -> c8 c8 :: c9:c10 -> c8 DIV :: 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if -> c9:c10 c9 :: c11:c12:c13:c14:null_IF -> c:c1:c2:null_GE -> c9:c10 IF :: false:true:null_ge -> false:true:null_ge -> 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if -> c11:c12:c13:c14:null_IF ge :: 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if -> false:true:null_ge c10 :: c11:c12:c13:c14:null_IF -> c:c1:c2:null_GE -> c9:c10 false :: false:true:null_ge c11 :: c11:c12:c13:c14:null_IF true :: false:true:null_ge c12 :: c11:c12:c13:c14:null_IF c13 :: c9:c10 -> c3:c4:c5:null_MINUS -> c11:c12:c13:c14:null_IF minus :: 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if id_inc :: 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if c14 :: c9:c10 -> c6:c7 -> c11:c12:c13:c14:null_IF quot :: 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if div :: 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if if :: false:true:null_ge -> false:true:null_ge -> 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if -> 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if div_by_zero :: 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if null_ge :: false:true:null_ge null_minus :: 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if null_id_inc :: 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if null_quot :: 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if null_div :: 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if null_if :: 0:s:div_by_zero:null_minus:null_id_inc:null_quot:null_div:null_if null_GE :: c:c1:c2:null_GE null_MINUS :: c3:c4:c5:null_MINUS null_IF :: c11:c12:c13:c14:null_IF const :: c8 const1 :: c9:c10 Rewrite Strategy: INNERMOST ---------------------------------------- (9) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: 0 => 0 c => 0 c1 => 1 c3 => 0 c4 => 1 c6 => 0 c7 => 1 false => 1 c11 => 0 true => 2 c12 => 1 div_by_zero => 1 null_ge => 0 null_minus => 0 null_id_inc => 0 null_quot => 0 null_div => 0 null_if => 0 null_GE => 0 null_MINUS => 0 null_IF => 0 const => 0 const1 => 0 ---------------------------------------- (10) Obligation: Complexity RNTS consisting of the following rules: DIV(z, z', z'') -{ 1 }-> 1 + IF(ge(z1, 1 + 0), ge(z0, z1), z0, z1, z2) + GE(z0, z1) :|: z'' = z2, z = z0, z1 >= 0, z' = z1, z0 >= 0, z2 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(ge(z1, 1 + 0), ge(z0, z1), z0, z1, z2) + GE(z1, 1 + 0) :|: z'' = z2, z = z0, z1 >= 0, z' = z1, z0 >= 0, z2 >= 0 GE(z, z') -{ 1 }-> 1 :|: z0 >= 0, z' = 1 + z0, z = 0 GE(z, z') -{ 1 }-> 0 :|: z = z0, z0 >= 0, z' = 0 GE(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 GE(z, z') -{ 1 }-> 1 + GE(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1 ID_INC(z) -{ 1 }-> 1 :|: z = z0, z0 >= 0 ID_INC(z) -{ 1 }-> 0 :|: z = z0, z0 >= 0 IF(z, z', z'', z4, z5) -{ 1 }-> 1 :|: z = 2, z1 >= 0, z'' = z0, z0 >= 0, z' = 1, z4 = z1, z5 = z2, z2 >= 0 IF(z, z', z'', z4, z5) -{ 1 }-> 0 :|: z1 >= 0, z = 1, z0 >= 0, z5 = z3, z' = z0, z2 >= 0, z3 >= 0, z'' = z1, z4 = z2 IF(z, z', z'', z4, z5) -{ 0 }-> 0 :|: z5 = v4, v0 >= 0, v4 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, z4 = v3, v2 >= 0, v3 >= 0 IF(z, z', z'', z4, z5) -{ 1 }-> 1 + DIV(minus(z0, z1), z1, id_inc(z2)) + MINUS(z0, z1) :|: z = 2, z1 >= 0, z' = 2, z'' = z0, z0 >= 0, z4 = z1, z5 = z2, z2 >= 0 IF(z, z', z'', z4, z5) -{ 1 }-> 1 + DIV(minus(z0, z1), z1, id_inc(z2)) + ID_INC(z2) :|: z = 2, z1 >= 0, z' = 2, z'' = z0, z0 >= 0, z4 = z1, z5 = z2, z2 >= 0 MINUS(z, z') -{ 1 }-> 1 :|: z0 >= 0, z = 0, z' = z0 MINUS(z, z') -{ 1 }-> 0 :|: z = z0, z0 >= 0, z' = 0 MINUS(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 MINUS(z, z') -{ 1 }-> 1 + MINUS(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1 QUOT(z, z') -{ 1 }-> 1 + DIV(z0, z1, 0) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0 div(z, z', z'') -{ 0 }-> if(ge(z1, 1 + 0), ge(z0, z1), z0, z1, z2) :|: z'' = z2, z = z0, z1 >= 0, z' = z1, z0 >= 0, z2 >= 0 div(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0 ge(z, z') -{ 0 }-> ge(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1 ge(z, z') -{ 0 }-> 2 :|: z = z0, z0 >= 0, z' = 0 ge(z, z') -{ 0 }-> 1 :|: z0 >= 0, z' = 1 + z0, z = 0 ge(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 id_inc(z) -{ 0 }-> z0 :|: z = z0, z0 >= 0 id_inc(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 id_inc(z) -{ 0 }-> 1 + z0 :|: z = z0, z0 >= 0 if(z, z', z'', z4, z5) -{ 0 }-> z2 :|: z = 2, z1 >= 0, z'' = z0, z0 >= 0, z' = 1, z4 = z1, z5 = z2, z2 >= 0 if(z, z', z'', z4, z5) -{ 0 }-> div(minus(z0, z1), z1, id_inc(z2)) :|: z = 2, z1 >= 0, z' = 2, z'' = z0, z0 >= 0, z4 = z1, z5 = z2, z2 >= 0 if(z, z', z'', z4, z5) -{ 0 }-> 1 :|: z1 >= 0, z = 1, z0 >= 0, z5 = z3, z' = z0, z2 >= 0, z3 >= 0, z'' = z1, z4 = z2 if(z, z', z'', z4, z5) -{ 0 }-> 0 :|: z5 = v4, v0 >= 0, v4 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, z4 = v3, v2 >= 0, v3 >= 0 minus(z, z') -{ 0 }-> z0 :|: z = z0, z0 >= 0, z' = 0 minus(z, z') -{ 0 }-> minus(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1 minus(z, z') -{ 0 }-> 0 :|: z0 >= 0, z = 0, z' = z0 minus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 quot(z, z') -{ 0 }-> div(z0, z1, 0) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0 quot(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 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, V15, V22, V23),0,[fun(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V15, V22, V23),0,[fun1(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V15, V22, V23),0,[fun2(V1, Out)],[V1 >= 0]). eq(start(V1, V, V15, V22, V23),0,[fun3(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V15, V22, V23),0,[fun4(V1, V, V15, Out)],[V1 >= 0,V >= 0,V15 >= 0]). eq(start(V1, V, V15, V22, V23),0,[fun5(V1, V, V15, V22, V23, Out)],[V1 >= 0,V >= 0,V15 >= 0,V22 >= 0,V23 >= 0]). eq(start(V1, V, V15, V22, V23),0,[ge(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V15, V22, V23),0,[minus(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V15, V22, V23),0,[fun6(V1, Out)],[V1 >= 0]). eq(start(V1, V, V15, V22, V23),0,[quot(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V15, V22, V23),0,[div(V1, V, V15, Out)],[V1 >= 0,V >= 0,V15 >= 0]). eq(start(V1, V, V15, V22, V23),0,[if(V1, V, V15, V22, V23, Out)],[V1 >= 0,V >= 0,V15 >= 0,V22 >= 0,V23 >= 0]). eq(fun(V1, V, Out),1,[],[Out = 0,V1 = V2,V2 >= 0,V = 0]). eq(fun(V1, V, Out),1,[],[Out = 1,V3 >= 0,V = 1 + V3,V1 = 0]). eq(fun(V1, V, Out),1,[fun(V5, V4, Ret1)],[Out = 1 + Ret1,V4 >= 0,V1 = 1 + V5,V5 >= 0,V = 1 + V4]). eq(fun1(V1, V, Out),1,[],[Out = 0,V1 = V6,V6 >= 0,V = 0]). eq(fun1(V1, V, Out),1,[],[Out = 1,V7 >= 0,V1 = 0,V = V7]). eq(fun1(V1, V, Out),1,[fun1(V8, V9, Ret11)],[Out = 1 + Ret11,V9 >= 0,V1 = 1 + V8,V8 >= 0,V = 1 + V9]). eq(fun2(V1, Out),1,[],[Out = 0,V1 = V10,V10 >= 0]). eq(fun2(V1, Out),1,[],[Out = 1,V1 = V11,V11 >= 0]). eq(fun3(V1, V, Out),1,[fun4(V13, V12, 0, Ret12)],[Out = 1 + Ret12,V1 = V13,V12 >= 0,V = V12,V13 >= 0]). eq(fun4(V1, V, V15, Out),1,[ge(V16, 1 + 0, Ret010),ge(V14, V16, Ret011),fun5(Ret010, Ret011, V14, V16, V17, Ret01),fun(V16, 1 + 0, Ret13)],[Out = 1 + Ret01 + Ret13,V15 = V17,V1 = V14,V16 >= 0,V = V16,V14 >= 0,V17 >= 0]). eq(fun4(V1, V, V15, Out),1,[ge(V18, 1 + 0, Ret0101),ge(V20, V18, Ret0111),fun5(Ret0101, Ret0111, V20, V18, V19, Ret012),fun(V20, V18, Ret14)],[Out = 1 + Ret012 + Ret14,V15 = V19,V1 = V20,V18 >= 0,V = V18,V20 >= 0,V19 >= 0]). eq(fun5(V1, V, V15, V22, V23, Out),1,[],[Out = 0,V21 >= 0,V1 = 1,V25 >= 0,V23 = V26,V = V25,V24 >= 0,V26 >= 0,V15 = V21,V22 = V24]). eq(fun5(V1, V, V15, V22, V23, Out),1,[],[Out = 1,V1 = 2,V27 >= 0,V15 = V28,V28 >= 0,V = 1,V22 = V27,V23 = V29,V29 >= 0]). eq(fun5(V1, V, V15, V22, V23, Out),1,[minus(V31, V30, Ret0102),fun6(V32, Ret0121),fun4(Ret0102, V30, Ret0121, Ret013),fun1(V31, V30, Ret15)],[Out = 1 + Ret013 + Ret15,V1 = 2,V30 >= 0,V = 2,V15 = V31,V31 >= 0,V22 = V30,V23 = V32,V32 >= 0]). eq(fun5(V1, V, V15, V22, V23, Out),1,[minus(V34, V35, Ret0103),fun6(V33, Ret0122),fun4(Ret0103, V35, Ret0122, Ret014),fun2(V33, Ret16)],[Out = 1 + Ret014 + Ret16,V1 = 2,V35 >= 0,V = 2,V15 = V34,V34 >= 0,V22 = V35,V23 = V33,V33 >= 0]). eq(ge(V1, V, Out),0,[],[Out = 2,V1 = V36,V36 >= 0,V = 0]). eq(ge(V1, V, Out),0,[],[Out = 1,V37 >= 0,V = 1 + V37,V1 = 0]). eq(ge(V1, V, Out),0,[ge(V39, V38, Ret)],[Out = Ret,V38 >= 0,V1 = 1 + V39,V39 >= 0,V = 1 + V38]). eq(minus(V1, V, Out),0,[],[Out = V40,V1 = V40,V40 >= 0,V = 0]). eq(minus(V1, V, Out),0,[],[Out = 0,V41 >= 0,V1 = 0,V = V41]). eq(minus(V1, V, Out),0,[minus(V42, V43, Ret2)],[Out = Ret2,V43 >= 0,V1 = 1 + V42,V42 >= 0,V = 1 + V43]). eq(fun6(V1, Out),0,[],[Out = V44,V1 = V44,V44 >= 0]). eq(fun6(V1, Out),0,[],[Out = 1 + V45,V1 = V45,V45 >= 0]). eq(quot(V1, V, Out),0,[div(V46, V47, 0, Ret3)],[Out = Ret3,V1 = V46,V47 >= 0,V = V47,V46 >= 0]). eq(div(V1, V, V15, Out),0,[ge(V49, 1 + 0, Ret0),ge(V50, V49, Ret17),if(Ret0, Ret17, V50, V49, V48, Ret4)],[Out = Ret4,V15 = V48,V1 = V50,V49 >= 0,V = V49,V50 >= 0,V48 >= 0]). eq(if(V1, V, V15, V22, V23, Out),0,[],[Out = 1,V52 >= 0,V1 = 1,V53 >= 0,V23 = V54,V = V53,V51 >= 0,V54 >= 0,V15 = V52,V22 = V51]). eq(if(V1, V, V15, V22, V23, Out),0,[],[Out = V55,V1 = 2,V56 >= 0,V15 = V57,V57 >= 0,V = 1,V22 = V56,V23 = V55,V55 >= 0]). eq(if(V1, V, V15, V22, V23, Out),0,[minus(V59, V60, Ret02),fun6(V58, Ret21),div(Ret02, V60, Ret21, Ret5)],[Out = Ret5,V1 = 2,V60 >= 0,V = 2,V15 = V59,V59 >= 0,V22 = V60,V23 = V58,V58 >= 0]). eq(ge(V1, V, Out),0,[],[Out = 0,V62 >= 0,V61 >= 0,V1 = V62,V = V61]). eq(minus(V1, V, Out),0,[],[Out = 0,V64 >= 0,V63 >= 0,V1 = V64,V = V63]). eq(fun6(V1, Out),0,[],[Out = 0,V65 >= 0,V1 = V65]). eq(quot(V1, V, Out),0,[],[Out = 0,V66 >= 0,V67 >= 0,V1 = V66,V = V67]). eq(div(V1, V, V15, Out),0,[],[Out = 0,V68 >= 0,V15 = V70,V69 >= 0,V1 = V68,V = V69,V70 >= 0]). eq(if(V1, V, V15, V22, V23, Out),0,[],[Out = 0,V23 = V74,V72 >= 0,V74 >= 0,V15 = V73,V71 >= 0,V1 = V72,V = V71,V22 = V75,V73 >= 0,V75 >= 0]). eq(fun(V1, V, Out),0,[],[Out = 0,V77 >= 0,V76 >= 0,V1 = V77,V = V76]). eq(fun1(V1, V, Out),0,[],[Out = 0,V78 >= 0,V79 >= 0,V1 = V78,V = V79]). eq(fun5(V1, V, V15, V22, V23, Out),0,[],[Out = 0,V23 = V83,V80 >= 0,V83 >= 0,V15 = V82,V81 >= 0,V1 = V80,V = V81,V22 = V84,V82 >= 0,V84 >= 0]). 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,V,V15,Out),[V1,V,V15],[Out]). input_output_vars(fun5(V1,V,V15,V22,V23,Out),[V1,V,V15,V22,V23],[Out]). input_output_vars(ge(V1,V,Out),[V1,V],[Out]). input_output_vars(minus(V1,V,Out),[V1,V],[Out]). input_output_vars(fun6(V1,Out),[V1],[Out]). input_output_vars(quot(V1,V,Out),[V1,V],[Out]). input_output_vars(div(V1,V,V15,Out),[V1,V,V15],[Out]). input_output_vars(if(V1,V,V15,V22,V23,Out),[V1,V,V15,V22,V23],[Out]). CoFloCo proof output: Preprocessing Cost Relations ===================================== #### Computed strongly connected components 0. recursive : [ge/3] 1. non_recursive : [fun6/2] 2. recursive : [minus/3] 3. recursive : [(div)/4,if/6] 4. recursive : [fun/3] 5. recursive : [fun1/3] 6. non_recursive : [fun2/2] 7. recursive [non_tail] : [fun4/4,fun5/6] 8. non_recursive : [fun3/3] 9. non_recursive : [quot/3] 10. non_recursive : [start/5] #### Obtained direct recursion through partial evaluation 0. SCC is partially evaluated into ge/3 1. SCC is partially evaluated into fun6/2 2. SCC is partially evaluated into minus/3 3. SCC is partially evaluated into (div)/4 4. SCC is partially evaluated into fun/3 5. SCC is partially evaluated into fun1/3 6. SCC is partially evaluated into fun2/2 7. SCC is partially evaluated into fun4/4 8. SCC is completely evaluated into other SCCs 9. SCC is partially evaluated into quot/3 10. SCC is partially evaluated into start/5 Control-Flow Refinement of Cost Relations ===================================== ### Specialization of cost equations ge/3 * CE 51 is refined into CE [54] * CE 48 is refined into CE [55] * CE 49 is refined into CE [56] * CE 50 is refined into CE [57] ### Cost equations --> "Loop" of ge/3 * CEs [57] --> Loop 29 * CEs [54] --> Loop 30 * CEs [55] --> Loop 31 * CEs [56] --> Loop 32 ### Ranking functions of CR ge(V1,V,Out) * RF of phase [29]: [V,V1] #### Partial ranking functions of CR ge(V1,V,Out) * Partial RF of phase [29]: - RF of loop [29:1]: V V1 ### Specialization of cost equations fun6/2 * CE 20 is refined into CE [58] * CE 21 is refined into CE [59] * CE 22 is refined into CE [60] ### Cost equations --> "Loop" of fun6/2 * CEs [58] --> Loop 33 * CEs [59] --> Loop 34 * CEs [60] --> Loop 35 ### Ranking functions of CR fun6(V1,Out) #### Partial ranking functions of CR fun6(V1,Out) ### Specialization of cost equations minus/3 * CE 18 is refined into CE [61] * CE 17 is refined into CE [62] * CE 19 is refined into CE [63] ### Cost equations --> "Loop" of minus/3 * CEs [63] --> Loop 36 * CEs [61] --> Loop 37 * CEs [62] --> Loop 38 ### Ranking functions of CR minus(V1,V,Out) * RF of phase [36]: [V,V1] #### Partial ranking functions of CR minus(V1,V,Out) * Partial RF of phase [36]: - RF of loop [36:1]: V V1 ### Specialization of cost equations (div)/4 * CE 41 is refined into CE [64,65] * CE 42 is refined into CE [66,67] * CE 39 is refined into CE [68,69,70,71,72,73,74,75,76,77,78] * CE 43 is refined into CE [79] * CE 40 is refined into CE [80,81,82,83,84,85] ### Cost equations --> "Loop" of (div)/4 * CEs [85] --> Loop 39 * CEs [84] --> Loop 40 * CEs [83] --> Loop 41 * CEs [82] --> Loop 42 * CEs [81] --> Loop 43 * CEs [80] --> Loop 44 * CEs [65] --> Loop 45 * CEs [66,67] --> Loop 46 * CEs [68,69,71] --> Loop 47 * CEs [64] --> Loop 48 * CEs [70,72,73,74,75,76,77,78,79] --> Loop 49 ### Ranking functions of CR div(V1,V,V15,Out) * RF of phase [39,40,41]: [V1,V1-V+1] #### Partial ranking functions of CR div(V1,V,V15,Out) * Partial RF of phase [39,40,41]: - RF of loop [39:1,40:1,41:1]: V1 V1-V+1 ### Specialization of cost equations fun/3 * CE 44 is refined into CE [86] * CE 47 is refined into CE [87] * CE 45 is refined into CE [88] * CE 46 is refined into CE [89] ### Cost equations --> "Loop" of fun/3 * CEs [89] --> Loop 50 * CEs [86,87] --> Loop 51 * CEs [88] --> Loop 52 ### Ranking functions of CR fun(V1,V,Out) * RF of phase [50]: [V,V1] #### Partial ranking functions of CR fun(V1,V,Out) * Partial RF of phase [50]: - RF of loop [50:1]: V V1 ### Specialization of cost equations fun1/3 * CE 35 is refined into CE [90] * CE 38 is refined into CE [91] * CE 36 is refined into CE [92] * CE 37 is refined into CE [93] ### Cost equations --> "Loop" of fun1/3 * CEs [93] --> Loop 53 * CEs [90,91] --> Loop 54 * CEs [92] --> Loop 55 ### Ranking functions of CR fun1(V1,V,Out) * RF of phase [53]: [V,V1] #### Partial ranking functions of CR fun1(V1,V,Out) * Partial RF of phase [53]: - RF of loop [53:1]: V V1 ### Specialization of cost equations fun2/2 * CE 34 is refined into CE [94] * CE 33 is refined into CE [95] ### Cost equations --> "Loop" of fun2/2 * CEs [94] --> Loop 56 * CEs [95] --> Loop 57 ### Ranking functions of CR fun2(V1,Out) #### Partial ranking functions of CR fun2(V1,Out) ### Specialization of cost equations fun4/4 * CE 23 is refined into CE [96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120] * CE 24 is refined into CE [121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143] * CE 29 is refined into CE [144,145,146,147,148] * CE 30 is refined into CE [149,150,151,152] * CE 31 is refined into CE [153,154] * CE 32 is refined into CE [155,156,157,158] * CE 25 is refined into CE [159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182] * CE 26 is refined into CE [183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200,201,202,203,204,205,206] * CE 27 is refined into CE [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] * CE 28 is refined into CE [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] ### Cost equations --> "Loop" of fun4/4 * CEs [182,206,242,278] --> Loop 58 * CEs [180,181,204,205,238,241,274,277] --> Loop 59 * CEs [179,203,237,273] --> Loop 60 * CEs [178,202,236,272] --> Loop 61 * CEs [176,177,200,201,232,235,268,271] --> Loop 62 * CEs [175,199,231,267] --> Loop 63 * CEs [174,198,230,266] --> Loop 64 * CEs [172,173,196,197,226,229,262,265] --> Loop 65 * CEs [171,195,225,261] --> Loop 66 * CEs [194] --> Loop 67 * CEs [168,169,192,193,220,223,256,259] --> Loop 68 * CEs [167,191,219,255] --> Loop 69 * CEs [190] --> Loop 70 * CEs [164,165,188,189,214,217,250,253] --> Loop 71 * CEs [163,187,213,249] --> Loop 72 * CEs [170,221,224,239,257,260,275] --> Loop 73 * CEs [222,240,258,276] --> Loop 74 * CEs [166,215,218,233,251,254,269] --> Loop 75 * CEs [216,234,252,270] --> Loop 76 * CEs [186] --> Loop 77 * CEs [160,161,184,185,208,211,244,247] --> Loop 78 * CEs [159,183,207,243] --> Loop 79 * CEs [162,209,212,227,245,248,263] --> Loop 80 * CEs [210,228,246,264] --> Loop 81 * CEs [109,120] --> Loop 82 * CEs [104,107,115,118] --> Loop 83 * CEs [103,106,114,117] --> Loop 84 * CEs [147] --> Loop 85 * CEs [148,152] --> Loop 86 * CEs [121,123,127,129,155,157] --> Loop 87 * CEs [96,97,100,122,124,128,153,154,156,158] --> Loop 88 * CEs [144,150] --> Loop 89 * CEs [98,101,110,112,126,131,133,135,137,139,141,143,145,146,149,151] --> Loop 90 * CEs [99,102,105,108,111,113,116,119,125,130,132,134,136,138,140,142] --> Loop 91 ### Ranking functions of CR fun4(V1,V,V15,Out) * RF of phase [58,59,60,61,62,63,64,65,66]: [V1,V1-V+1] #### Partial ranking functions of CR fun4(V1,V,V15,Out) * Partial RF of phase [58,59,60,61,62,63,64,65,66]: - RF of loop [58:1,59:1,60:1,61:1,62:1,63:1,64:1,65:1,66:1]: V1 V1-V+1 ### Specialization of cost equations quot/3 * CE 52 is refined into CE [279,280,281,282,283,284,285] * CE 53 is refined into CE [286] ### Cost equations --> "Loop" of quot/3 * CEs [282,285] --> Loop 92 * CEs [281] --> Loop 93 * CEs [279,280,283,284,286] --> Loop 94 ### Ranking functions of CR quot(V1,V,Out) #### Partial ranking functions of CR quot(V1,V,Out) ### Specialization of cost equations start/5 * CE 2 is refined into CE [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] * CE 3 is refined into CE [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] * CE 6 is refined into CE [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] * CE 4 is refined into CE [599] * CE 1 is refined into CE [600] * CE 5 is refined into CE [601] * CE 7 is refined into CE [602,603,604,605] * CE 8 is refined into CE [606,607,608,609] * CE 9 is refined into CE [610,611] * CE 10 is refined into CE [612,613,614,615,616,617,618,619,620,621,622,623,624,625,626,627] * CE 11 is refined into CE [628,629,630,631,632,633,634,635,636,637,638,639,640,641,642,643] * CE 12 is refined into CE [644,645,646,647,648] * CE 13 is refined into CE [649,650,651] * CE 14 is refined into CE [652,653,654] * CE 15 is refined into CE [655,656,657] * CE 16 is refined into CE [658,659,660,661,662,663,664] ### Cost equations --> "Loop" of start/5 * CEs [614,630,645,649,655,660] --> Loop 95 * CEs [323,324,353,354,383,384,467,468,469,471,474,500,501,502,504,507,533,534,535,537,540,581,587,593] --> Loop 96 * CEs [339,340,341,342,343,344,369,370,371,372,373,374,399,400,401,402,403,404,486,487,488,489,490,491,519,520,521,522,523,524,552,553,554,555,556,557] --> Loop 97 * CEs [287,288,289,290,291,292,293,294,295,296,297,298,303,304,311,312,319,320,414,416,418,420,422,424,434,448,462,566,567,568,569,570,571,574,577,580] --> Loop 98 * CEs [299,300,301,302,305,306,307,308,309,310,313,314,315,316,317,318,321,322,325,326,327,328,329,330,331,332,333,334,335,336,337,338,345,346,347,348,349,350,351,352,355,356,357,358,359,360,361,362,363,364,365,366,367,368,375,376,377,378,379,380,381,382,385,386,387,388,389,390,391,392,393,394,395,396,397,398,405,406,407,408,409,410,411,412,413,415,417,419,421,423,425,426,427,428,429,430,431,432,433,435,436,437,438,439,440,441,442,443,444,445,446,447,449,450,451,452,453,454,455,456,457,458,459,460,461,463,464,465,466,470,472,473,475,476,477,478,479,480,481,482,483,484,485,492,493,494,495,496,497,498,499,503,505,506,508,509,510,511,512,513,514,515,516,517,518,525,526,527,528,529,530,531,532,536,538,539,541,542,543,544,545,546,547,548,549,550,551,558,559,560,561,562,563,564,565,572,573,575,576,578,579,582,583,584,585,586,588,589,590,591,592,594,595,596,597,598,621,622,623,637,638,639] --> Loop 99 * CEs [599] --> Loop 100 * CEs [601] --> Loop 101 * CEs [600,602,603,604,605,606,607,608,609,610,611,612,613,615,616,617,618,619,620,624,625,626,627,628,629,631,632,633,634,635,636,640,641,642,643,644,646,647,648,650,651,652,653,654,656,657,658,659,661,662,663,664] --> Loop 102 ### Ranking functions of CR start(V1,V,V15,V22,V23) #### Partial ranking functions of CR start(V1,V,V15,V22,V23) Computing Bounds ===================================== #### Cost of chains of ge(V1,V,Out): * Chain [[29],32]: 0 with precondition: [Out=1,V1>=1,V>=V1+1] * Chain [[29],31]: 0 with precondition: [Out=2,V>=1,V1>=V] * Chain [[29],30]: 0 with precondition: [Out=0,V1>=1,V>=1] * Chain [32]: 0 with precondition: [V1=0,Out=1,V>=1] * Chain [31]: 0 with precondition: [V=0,Out=2,V1>=0] * Chain [30]: 0 with precondition: [Out=0,V1>=0,V>=0] #### Cost of chains of fun6(V1,Out): * Chain [35]: 0 with precondition: [Out=0,V1>=0] * Chain [34]: 0 with precondition: [V1+1=Out,V1>=0] * Chain [33]: 0 with precondition: [V1=Out,V1>=0] #### Cost of chains of minus(V1,V,Out): * Chain [[36],38]: 0 with precondition: [V1=Out+V,V>=1,V1>=V] * Chain [[36],37]: 0 with precondition: [Out=0,V1>=1,V>=1] * Chain [38]: 0 with precondition: [V=0,V1=Out,V1>=0] * Chain [37]: 0 with precondition: [Out=0,V1>=0,V>=0] #### Cost of chains of div(V1,V,V15,Out): * Chain [[39,40,41],49]: 0 with precondition: [Out=0,V>=1,V15>=0,V1>=V] * Chain [[39,40,41],48]: 0 with precondition: [V>=1,V15>=0,Out>=0,V1>=V,V1+V15+1>=Out+V] * Chain [[39,40,41],45]: 0 with precondition: [V>=2,V15>=0,Out>=0,V1>=V+1,V1+2*V15+1>=2*Out+V] * Chain [[39,40,41],44,49]: 0 with precondition: [Out=0,V>=1,V15>=0,V1>=2*V] * Chain [[39,40,41],44,48]: 0 with precondition: [Out=0,V>=1,V15>=0,V1>=2*V] * Chain [[39,40,41],43,49]: 0 with precondition: [Out=0,V>=1,V15>=0,V1>=2*V] * Chain [[39,40,41],43,48]: 0 with precondition: [V>=1,V15>=0,Out>=1,V1>=2*V,V1+V15+2>=2*V+Out] * Chain [[39,40,41],42,49]: 0 with precondition: [Out=0,V>=1,V15>=0,V1>=2*V] * Chain [[39,40,41],42,48]: 0 with precondition: [V>=1,V15>=0,Out>=0,V1>=2*V,V1+V15+1>=2*V+Out] * Chain [49]: 0 with precondition: [Out=0,V1>=0,V>=0,V15>=0] * Chain [48]: 0 with precondition: [V1=0,V15=Out,V>=1,V15>=0] * Chain [47]: 0 with precondition: [V=0,Out=0,V1>=0,V15>=0] * Chain [46]: 0 with precondition: [V=0,Out=1,V1>=0,V15>=0] * Chain [45]: 0 with precondition: [V15=Out,V1>=1,V15>=0,V>=V1+1] * Chain [44,49]: 0 with precondition: [Out=0,V>=1,V15>=0,V1>=V] * Chain [44,48]: 0 with precondition: [Out=0,V>=1,V15>=0,V1>=V] * Chain [43,49]: 0 with precondition: [Out=0,V>=1,V15>=0,V1>=V] * Chain [43,48]: 0 with precondition: [Out=V15+1,V>=1,Out>=1,V1>=V] * Chain [42,49]: 0 with precondition: [Out=0,V>=1,V15>=0,V1>=V] * Chain [42,48]: 0 with precondition: [V15=Out,V>=1,V15>=0,V1>=V] #### Cost of chains of fun(V1,V,Out): * Chain [[50],52]: 1*it(50)+1 Such that:it(50) =< Out with precondition: [V1+1=Out,V1>=1,V>=V1+1] * Chain [[50],51]: 1*it(50)+1 Such that:it(50) =< Out with precondition: [Out>=1,V1>=Out,V>=Out] * Chain [52]: 1 with precondition: [V1=0,Out=1,V>=1] * Chain [51]: 1 with precondition: [Out=0,V1>=0,V>=0] #### Cost of chains of fun1(V1,V,Out): * Chain [[53],55]: 1*it(53)+1 Such that:it(53) =< Out with precondition: [V1+1=Out,V1>=1,V>=V1] * Chain [[53],54]: 1*it(53)+1 Such that:it(53) =< Out with precondition: [Out>=1,V1>=Out,V>=Out] * Chain [55]: 1 with precondition: [V1=0,Out=1,V>=0] * Chain [54]: 1 with precondition: [Out=0,V1>=0,V>=0] #### Cost of chains of fun2(V1,Out): * Chain [57]: 1 with precondition: [Out=0,V1>=0] * Chain [56]: 1 with precondition: [Out=1,V1>=0] #### Cost of chains of fun4(V1,V,V15,Out): * Chain [[58,59,60,61,62,63,64,65,66],91]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+2 Such that:aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(31) =< V1 aux(20) =< aux(31) it(58) =< aux(31) it(65) =< aux(31) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) s(78) =< aux(31) s(85) =< aux(31) s(63) =< aux(20) s(83) =< s(85) s(62) =< aux(31) with precondition: [V>=1,V15>=0,Out>=3,V1>=V,4*V1+3>=2*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],90]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+11 Such that:aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(33) =< V1 aux(20) =< aux(33) it(58) =< aux(33) it(65) =< aux(33) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) s(78) =< aux(33) s(85) =< aux(33) s(63) =< aux(20) s(83) =< s(85) s(62) =< aux(33) with precondition: [V>=1,V15>=0,Out>=4,V1>=V,4*V1+4>=2*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],89]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+4 Such that:aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(34) =< V1 aux(20) =< aux(34) it(58) =< aux(34) it(65) =< aux(34) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) s(78) =< aux(34) s(85) =< aux(34) s(63) =< aux(20) s(83) =< s(85) s(62) =< aux(34) with precondition: [V>=1,V15>=0,Out>=5,V1>=V,4*V1+5>=2*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],86]: 28*it(58)+8*it(65)+20*s(62)+12*s(63)+1*s(78)+4*s(83)+1*s(97)+3 Such that:s(97) =< 1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(35) =< V1 s(62) =< aux(35) aux(20) =< aux(35) it(58) =< aux(35) it(65) =< aux(35) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) s(78) =< aux(35) s(85) =< aux(35) s(63) =< aux(20) s(83) =< s(85) with precondition: [V>=2,V15>=0,Out>=5,V1>=V+1,3*V1+2>=Out+V] * Chain [[58,59,60,61,62,63,64,65,66],85]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+1*s(98)+3 Such that:aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(36) =< V1+1 s(98) =< aux(36) aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(36) it(58) =< aux(36) it(65) =< aux(36) s(64) =< aux(36) s(78) =< aux(36) s(85) =< aux(36) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=2,V15>=0,Out>=6,V1>=V+1,3*V1+3>=Out+V] * Chain [[58,59,60,61,62,63,64,65,66],84]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+4*s(99)+2 Such that:aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(38) =< V1+1 s(99) =< aux(38) aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(38) it(58) =< aux(38) it(65) =< aux(38) s(64) =< aux(38) s(78) =< aux(38) s(85) =< aux(38) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=2,V15>=0,Out>=5,V1>=V+1,3*V1+2>=Out+V] * Chain [[58,59,60,61,62,63,64,65,66],83]: 28*it(58)+8*it(65)+23*s(62)+12*s(63)+1*s(78)+4*s(83)+2 Such that:aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(40) =< V1 s(62) =< aux(40) aux(20) =< aux(40) it(58) =< aux(40) it(65) =< aux(40) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) s(78) =< aux(40) s(85) =< aux(40) s(63) =< aux(20) s(83) =< s(85) with precondition: [V>=1,V15>=0,Out>=4,V1>=V+1,4*V1>=2*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],82]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+2*s(107)+2 Such that:aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(41) =< V aux(42) =< V1-V s(107) =< aux(41) aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(42) it(58) =< aux(42) it(65) =< aux(42) s(64) =< aux(42) s(78) =< aux(42) s(85) =< aux(42) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=4,V1>=2*V,4*V1+3>=5*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],81,91]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+4*s(109)+2*s(110)+2*s(114)+6 Such that:aux(43) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(44) =< V aux(45) =< V+1 aux(46) =< V1-V s(114) =< aux(43) s(110) =< aux(44) s(109) =< aux(45) aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(46) it(58) =< aux(46) it(65) =< aux(46) s(64) =< aux(46) s(78) =< aux(46) s(85) =< aux(46) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,V1>=2*V,Out>=V+7,4*V1+6>=4*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],81,90]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+4*s(109)+2*s(110)+2*s(114)+15 Such that:aux(43) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(44) =< V aux(45) =< V+1 aux(47) =< V1-V s(114) =< aux(43) s(110) =< aux(44) s(109) =< aux(45) aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(47) it(58) =< aux(47) it(65) =< aux(47) s(64) =< aux(47) s(78) =< aux(47) s(85) =< aux(47) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,V1>=2*V,Out>=V+8,4*V1+7>=4*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],81,89]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+4*s(109)+2*s(110)+2*s(114)+8 Such that:aux(43) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(44) =< V aux(45) =< V+1 aux(48) =< V1-V s(114) =< aux(43) s(110) =< aux(44) s(109) =< aux(45) aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(48) it(58) =< aux(48) it(65) =< aux(48) s(64) =< aux(48) s(78) =< aux(48) s(85) =< aux(48) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,V1>=2*V,Out>=V+9,4*V1+8>=4*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],80,91]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+4*s(117)+4*s(118)+1*s(124)+6 Such that:s(124) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(52) =< V aux(53) =< V1+1 s(117) =< aux(52) s(118) =< aux(53) aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(53) it(58) =< aux(53) it(65) =< aux(53) s(64) =< aux(53) s(78) =< aux(53) s(85) =< aux(53) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=7,V1>=2*V,4*V1+5>=4*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],80,90]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+4*s(117)+4*s(118)+1*s(124)+15 Such that:s(124) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(54) =< V aux(55) =< V1+1 s(117) =< aux(54) s(118) =< aux(55) aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(55) it(58) =< aux(55) it(65) =< aux(55) s(64) =< aux(55) s(78) =< aux(55) s(85) =< aux(55) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=8,V1>=2*V,4*V1+6>=4*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],80,89]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+4*s(117)+4*s(118)+1*s(124)+8 Such that:s(124) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(56) =< V aux(57) =< V1+1 s(117) =< aux(56) s(118) =< aux(57) aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(57) it(58) =< aux(57) it(65) =< aux(57) s(64) =< aux(57) s(78) =< aux(57) s(85) =< aux(57) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=9,V1>=2*V,4*V1+7>=4*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],79,91]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+6 Such that:aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(58) =< V1-V aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(58) it(58) =< aux(58) it(65) =< aux(58) s(64) =< aux(58) s(78) =< aux(58) s(85) =< aux(58) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=5,V1>=2*V,4*V1+5>=6*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],79,90]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+15 Such that:aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(59) =< V1-V aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(59) it(58) =< aux(59) it(65) =< aux(59) s(64) =< aux(59) s(78) =< aux(59) s(85) =< aux(59) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=6,V1>=2*V,4*V1+6>=6*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],79,89]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+8 Such that:aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(60) =< V1-V aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(60) it(58) =< aux(60) it(65) =< aux(60) s(64) =< aux(60) s(78) =< aux(60) s(85) =< aux(60) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=7,V1>=2*V,4*V1+7>=6*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],78,91]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+4*s(126)+2*s(127)+6 Such that:aux(61) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(62) =< V aux(63) =< V1-V s(127) =< aux(61) s(126) =< aux(62) aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(63) it(58) =< aux(63) it(65) =< aux(63) s(64) =< aux(63) s(78) =< aux(63) s(85) =< aux(63) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=6,V1>=2*V,4*V1+5>=5*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],78,90]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+4*s(126)+2*s(127)+15 Such that:aux(61) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(62) =< V aux(64) =< V1-V s(127) =< aux(61) s(126) =< aux(62) aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(64) it(58) =< aux(64) it(65) =< aux(64) s(64) =< aux(64) s(78) =< aux(64) s(85) =< aux(64) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=7,V1>=2*V,4*V1+6>=5*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],78,89]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+4*s(126)+2*s(127)+8 Such that:aux(61) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(62) =< V aux(65) =< V1-V s(127) =< aux(61) s(126) =< aux(62) aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(65) it(58) =< aux(65) it(65) =< aux(65) s(64) =< aux(65) s(78) =< aux(65) s(85) =< aux(65) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=8,V1>=2*V,4*V1+7>=5*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],77,91]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+1*s(132)+6 Such that:s(132) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(66) =< V1-V aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(66) it(58) =< aux(66) it(65) =< aux(66) s(64) =< aux(66) s(78) =< aux(66) s(85) =< aux(66) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=7,V1>=2*V,4*V1+7>=6*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],77,90]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+1*s(132)+15 Such that:s(132) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(67) =< V1-V aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(67) it(58) =< aux(67) it(65) =< aux(67) s(64) =< aux(67) s(78) =< aux(67) s(85) =< aux(67) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=8,V1>=2*V,4*V1+8>=6*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],77,89]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+1*s(132)+8 Such that:s(132) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(68) =< V1-V aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(68) it(58) =< aux(68) it(65) =< aux(68) s(64) =< aux(68) s(78) =< aux(68) s(85) =< aux(68) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=9,V1>=2*V,4*V1+9>=6*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],76,91]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+4*s(133)+2*s(134)+2*s(138)+6 Such that:aux(69) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(70) =< V aux(71) =< V+1 aux(72) =< V1-V s(138) =< aux(69) s(134) =< aux(70) s(133) =< aux(71) aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(72) it(58) =< aux(72) it(65) =< aux(72) s(64) =< aux(72) s(78) =< aux(72) s(85) =< aux(72) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,V1>=2*V,Out>=V+7,4*V1+6>=4*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],76,90]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+4*s(133)+2*s(134)+2*s(138)+15 Such that:aux(69) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(70) =< V aux(71) =< V+1 aux(73) =< V1-V s(138) =< aux(69) s(134) =< aux(70) s(133) =< aux(71) aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(73) it(58) =< aux(73) it(65) =< aux(73) s(64) =< aux(73) s(78) =< aux(73) s(85) =< aux(73) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,V1>=2*V,Out>=V+8,4*V1+7>=4*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],76,89]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+4*s(133)+2*s(134)+2*s(138)+8 Such that:aux(69) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(70) =< V aux(71) =< V+1 aux(74) =< V1-V s(138) =< aux(69) s(134) =< aux(70) s(133) =< aux(71) aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(74) it(58) =< aux(74) it(65) =< aux(74) s(64) =< aux(74) s(78) =< aux(74) s(85) =< aux(74) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,V1>=2*V,Out>=V+9,4*V1+8>=4*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],75,91]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+4*s(141)+4*s(142)+1*s(148)+6 Such that:s(148) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(76) =< V aux(77) =< V+1 aux(78) =< V1-V s(141) =< aux(76) s(142) =< aux(77) aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(78) it(58) =< aux(78) it(65) =< aux(78) s(64) =< aux(78) s(78) =< aux(78) s(85) =< aux(78) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=7,V1>=2*V,4*V1+5>=4*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],75,90]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+4*s(141)+4*s(142)+1*s(148)+15 Such that:s(148) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(76) =< V aux(77) =< V+1 aux(79) =< V1-V s(141) =< aux(76) s(142) =< aux(77) aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(79) it(58) =< aux(79) it(65) =< aux(79) s(64) =< aux(79) s(78) =< aux(79) s(85) =< aux(79) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=8,V1>=2*V,4*V1+6>=4*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],75,89]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+4*s(141)+4*s(142)+1*s(148)+8 Such that:s(148) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(76) =< V aux(77) =< V+1 aux(80) =< V1-V s(141) =< aux(76) s(142) =< aux(77) aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(80) it(58) =< aux(80) it(65) =< aux(80) s(64) =< aux(80) s(78) =< aux(80) s(85) =< aux(80) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=9,V1>=2*V,4*V1+7>=4*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],74,91]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+4*s(150)+2*s(151)+2*s(155)+6 Such that:aux(81) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(82) =< V aux(83) =< V+1 aux(84) =< V1-V s(155) =< aux(81) s(151) =< aux(82) s(150) =< aux(83) aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(84) it(58) =< aux(84) it(65) =< aux(84) s(64) =< aux(84) s(78) =< aux(84) s(85) =< aux(84) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,V1>=2*V,Out>=V+7,4*V1+6>=4*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],74,90]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+4*s(150)+2*s(151)+2*s(155)+15 Such that:aux(81) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(82) =< V aux(83) =< V+1 aux(85) =< V1-V s(155) =< aux(81) s(151) =< aux(82) s(150) =< aux(83) aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(85) it(58) =< aux(85) it(65) =< aux(85) s(64) =< aux(85) s(78) =< aux(85) s(85) =< aux(85) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,V1>=2*V,Out>=V+8,4*V1+7>=4*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],74,89]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+4*s(150)+2*s(151)+2*s(155)+8 Such that:aux(81) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(82) =< V aux(83) =< V+1 aux(86) =< V1-V s(155) =< aux(81) s(151) =< aux(82) s(150) =< aux(83) aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(86) it(58) =< aux(86) it(65) =< aux(86) s(64) =< aux(86) s(78) =< aux(86) s(85) =< aux(86) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,V1>=2*V,Out>=V+9,4*V1+8>=4*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],73,91]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+4*s(158)+4*s(159)+1*s(165)+6 Such that:s(165) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(88) =< V aux(89) =< V+1 aux(90) =< V1-V s(158) =< aux(88) s(159) =< aux(89) aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(90) it(58) =< aux(90) it(65) =< aux(90) s(64) =< aux(90) s(78) =< aux(90) s(85) =< aux(90) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=7,V1>=2*V,4*V1+5>=4*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],73,90]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+4*s(158)+4*s(159)+1*s(165)+15 Such that:s(165) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(88) =< V aux(89) =< V+1 aux(91) =< V1-V s(158) =< aux(88) s(159) =< aux(89) aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(91) it(58) =< aux(91) it(65) =< aux(91) s(64) =< aux(91) s(78) =< aux(91) s(85) =< aux(91) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=8,V1>=2*V,4*V1+6>=4*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],73,89]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+4*s(158)+4*s(159)+1*s(165)+8 Such that:s(165) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(88) =< V aux(89) =< V+1 aux(92) =< V1-V s(158) =< aux(88) s(159) =< aux(89) aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(92) it(58) =< aux(92) it(65) =< aux(92) s(64) =< aux(92) s(78) =< aux(92) s(85) =< aux(92) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=9,V1>=2*V,4*V1+7>=4*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],72,91]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+6 Such that:aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(93) =< V1-V aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(93) it(58) =< aux(93) it(65) =< aux(93) s(64) =< aux(93) s(78) =< aux(93) s(85) =< aux(93) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=5,V1>=2*V,4*V1+5>=6*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],72,90]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+15 Such that:aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(94) =< V1-V aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(94) it(58) =< aux(94) it(65) =< aux(94) s(64) =< aux(94) s(78) =< aux(94) s(85) =< aux(94) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=6,V1>=2*V,4*V1+6>=6*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],72,89]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+8 Such that:aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(95) =< V1-V aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(95) it(58) =< aux(95) it(65) =< aux(95) s(64) =< aux(95) s(78) =< aux(95) s(85) =< aux(95) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=7,V1>=2*V,4*V1+7>=6*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],71,91]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+4*s(167)+2*s(168)+6 Such that:aux(96) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(97) =< V aux(98) =< V1-V s(168) =< aux(96) s(167) =< aux(97) aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(98) it(58) =< aux(98) it(65) =< aux(98) s(64) =< aux(98) s(78) =< aux(98) s(85) =< aux(98) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=6,V1>=2*V,4*V1+5>=5*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],71,90]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+4*s(167)+2*s(168)+15 Such that:aux(96) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(97) =< V aux(99) =< V1-V s(168) =< aux(96) s(167) =< aux(97) aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(99) it(58) =< aux(99) it(65) =< aux(99) s(64) =< aux(99) s(78) =< aux(99) s(85) =< aux(99) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=7,V1>=2*V,4*V1+6>=5*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],71,89]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+4*s(167)+2*s(168)+8 Such that:aux(96) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(97) =< V aux(100) =< V1-V s(168) =< aux(96) s(167) =< aux(97) aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(100) it(58) =< aux(100) it(65) =< aux(100) s(64) =< aux(100) s(78) =< aux(100) s(85) =< aux(100) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=8,V1>=2*V,4*V1+7>=5*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],70,91]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+1*s(173)+6 Such that:s(173) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(101) =< V1-V aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(101) it(58) =< aux(101) it(65) =< aux(101) s(64) =< aux(101) s(78) =< aux(101) s(85) =< aux(101) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=7,V1>=2*V,4*V1+7>=6*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],70,90]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+1*s(173)+15 Such that:s(173) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(102) =< V1-V aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(102) it(58) =< aux(102) it(65) =< aux(102) s(64) =< aux(102) s(78) =< aux(102) s(85) =< aux(102) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=8,V1>=2*V,4*V1+8>=6*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],70,89]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+1*s(173)+8 Such that:s(173) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(103) =< V1-V aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(103) it(58) =< aux(103) it(65) =< aux(103) s(64) =< aux(103) s(78) =< aux(103) s(85) =< aux(103) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=9,V1>=2*V,4*V1+9>=6*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],69,91]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+6 Such that:aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(104) =< V1-V aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(104) it(58) =< aux(104) it(65) =< aux(104) s(64) =< aux(104) s(78) =< aux(104) s(85) =< aux(104) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=5,V1>=2*V,4*V1+5>=6*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],69,90]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+15 Such that:aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(105) =< V1-V aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(105) it(58) =< aux(105) it(65) =< aux(105) s(64) =< aux(105) s(78) =< aux(105) s(85) =< aux(105) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=6,V1>=2*V,4*V1+6>=6*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],69,89]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+8 Such that:aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(106) =< V1-V aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(106) it(58) =< aux(106) it(65) =< aux(106) s(64) =< aux(106) s(78) =< aux(106) s(85) =< aux(106) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=7,V1>=2*V,4*V1+7>=6*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],68,91]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+4*s(174)+2*s(175)+6 Such that:aux(107) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(108) =< V aux(109) =< V1-V s(175) =< aux(107) s(174) =< aux(108) aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(109) it(58) =< aux(109) it(65) =< aux(109) s(64) =< aux(109) s(78) =< aux(109) s(85) =< aux(109) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=6,V1>=2*V,4*V1+5>=5*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],68,90]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+4*s(174)+2*s(175)+15 Such that:aux(107) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(108) =< V aux(110) =< V1-V s(175) =< aux(107) s(174) =< aux(108) aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(110) it(58) =< aux(110) it(65) =< aux(110) s(64) =< aux(110) s(78) =< aux(110) s(85) =< aux(110) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=7,V1>=2*V,4*V1+6>=5*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],68,89]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+4*s(174)+2*s(175)+8 Such that:aux(107) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(108) =< V aux(111) =< V1-V s(175) =< aux(107) s(174) =< aux(108) aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(111) it(58) =< aux(111) it(65) =< aux(111) s(64) =< aux(111) s(78) =< aux(111) s(85) =< aux(111) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=8,V1>=2*V,4*V1+7>=5*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],67,91]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+1*s(180)+6 Such that:s(180) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(112) =< V1-V aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(112) it(58) =< aux(112) it(65) =< aux(112) s(64) =< aux(112) s(78) =< aux(112) s(85) =< aux(112) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=7,V1>=2*V,4*V1+7>=6*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],67,90]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+1*s(180)+15 Such that:s(180) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(113) =< V1-V aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(113) it(58) =< aux(113) it(65) =< aux(113) s(64) =< aux(113) s(78) =< aux(113) s(85) =< aux(113) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=8,V1>=2*V,4*V1+8>=6*V+Out] * Chain [[58,59,60,61,62,63,64,65,66],67,89]: 28*it(58)+8*it(65)+19*s(62)+12*s(63)+1*s(78)+4*s(83)+1*s(180)+8 Such that:s(180) =< 1 aux(26) =< V1 aux(27) =< V1+3/4 aux(28) =< V1-V+1 aux(114) =< V1-V aux(20) =< aux(26) it(58) =< aux(26) it(65) =< aux(26) s(64) =< aux(26) it(65) =< aux(27) s(78) =< aux(27) s(85) =< aux(27) aux(20) =< aux(28) it(58) =< aux(28) it(65) =< aux(28) aux(20) =< aux(114) it(58) =< aux(114) it(65) =< aux(114) s(64) =< aux(114) s(78) =< aux(114) s(85) =< aux(114) s(63) =< aux(20) s(83) =< s(85) s(62) =< s(64) with precondition: [V>=1,V15>=0,Out>=9,V1>=2*V,4*V1+9>=6*V+Out] * Chain [91]: 2 with precondition: [Out=1,V1>=0,V>=0,V15>=0] * Chain [90]: 11 with precondition: [Out=2,V1>=0,V>=1,V15>=0] * Chain [89]: 4 with precondition: [V1=0,Out=3,V>=1,V15>=0] * Chain [88]: 3 with precondition: [V=0,Out=1,V1>=0,V15>=0] * Chain [87]: 3 with precondition: [V=0,Out=2,V1>=0,V15>=0] * Chain [86]: 1*s(96)+1*s(97)+3 Such that:s(97) =< 1 s(96) =< V1 with precondition: [V15>=0,Out>=3,V>=V1+1,V1+2>=Out] * Chain [85]: 1*s(98)+3 Such that:s(98) =< V1+1 with precondition: [V1+3=Out,V1>=1,V15>=0,V>=V1+1] * Chain [84]: 4*s(99)+2 Such that:aux(37) =< V1+1 s(99) =< aux(37) with precondition: [V1+2=Out,V1>=1,V15>=0,V>=V1+1] * Chain [83]: 4*s(103)+2 Such that:aux(39) =< V1 s(103) =< aux(39) with precondition: [V15>=0,Out>=2,V1+1>=Out,V+1>=Out] * Chain [82]: 2*s(107)+2 Such that:aux(41) =< V s(107) =< aux(41) with precondition: [V15>=0,Out>=2,V1>=V,V+1>=Out] * Chain [81,91]: 4*s(109)+2*s(110)+2*s(114)+6 Such that:aux(43) =< 1 aux(44) =< V aux(45) =< V+1 s(114) =< aux(43) s(110) =< aux(44) s(109) =< aux(45) with precondition: [V1=V,V15>=0,Out>=V1+5,2*V1+4>=Out] * Chain [81,90]: 4*s(109)+2*s(110)+2*s(114)+15 Such that:aux(43) =< 1 aux(44) =< V aux(45) =< V+1 s(114) =< aux(43) s(110) =< aux(44) s(109) =< aux(45) with precondition: [V1=V,V15>=0,Out>=V1+6,2*V1+5>=Out] * Chain [81,89]: 4*s(109)+2*s(110)+2*s(114)+8 Such that:aux(43) =< 1 aux(44) =< V aux(45) =< V+1 s(114) =< aux(43) s(110) =< aux(44) s(109) =< aux(45) with precondition: [V1=V,V15>=0,Out>=V1+7,2*V1+6>=Out] * Chain [80,91]: 4*s(117)+4*s(118)+1*s(124)+6 Such that:s(124) =< 1 aux(50) =< V1+1 aux(52) =< V s(117) =< aux(52) s(118) =< aux(50) with precondition: [V15>=0,Out>=5,V1>=V,2*V+3>=Out] * Chain [80,90]: 4*s(117)+4*s(118)+1*s(124)+15 Such that:s(124) =< 1 aux(50) =< V1+1 aux(54) =< V s(117) =< aux(54) s(118) =< aux(50) with precondition: [V15>=0,Out>=6,V1>=V,2*V+4>=Out] * Chain [80,89]: 4*s(117)+4*s(118)+1*s(124)+8 Such that:s(124) =< 1 aux(50) =< V1+1 aux(56) =< V s(117) =< aux(56) s(118) =< aux(50) with precondition: [V15>=0,Out>=7,V1>=V,2*V+5>=Out] * Chain [79,91]: 6 with precondition: [Out=3,V>=1,V15>=0,V1>=V] * Chain [79,90]: 15 with precondition: [Out=4,V>=1,V15>=0,V1>=V] * Chain [79,89]: 8 with precondition: [Out=5,V>=1,V15>=0,V1>=V] * Chain [78,91]: 4*s(126)+2*s(127)+6 Such that:aux(61) =< 1 aux(62) =< V s(127) =< aux(61) s(126) =< aux(62) with precondition: [V15>=0,Out>=4,V1>=V,V+3>=Out] * Chain [78,90]: 4*s(126)+2*s(127)+15 Such that:aux(61) =< 1 aux(62) =< V s(127) =< aux(61) s(126) =< aux(62) with precondition: [V15>=0,Out>=5,V1>=V,V+4>=Out] * Chain [78,89]: 4*s(126)+2*s(127)+8 Such that:aux(61) =< 1 aux(62) =< V s(127) =< aux(61) s(126) =< aux(62) with precondition: [V15>=0,Out>=6,V1>=V,V+5>=Out] * Chain [77,91]: 1*s(132)+6 Such that:s(132) =< 1 with precondition: [Out=5,V>=1,V15>=0,V1>=V] * Chain [77,90]: 1*s(132)+15 Such that:s(132) =< 1 with precondition: [Out=6,V>=1,V15>=0,V1>=V] * Chain [77,89]: 1*s(132)+8 Such that:s(132) =< 1 with precondition: [Out=7,V>=1,V15>=0,V1>=V] * Chain [76,91]: 4*s(133)+2*s(134)+2*s(138)+6 Such that:aux(69) =< 1 aux(70) =< V aux(71) =< V+1 s(138) =< aux(69) s(134) =< aux(70) s(133) =< aux(71) with precondition: [V1=V,V15>=0,Out>=V1+5,2*V1+4>=Out] * Chain [76,90]: 4*s(133)+2*s(134)+2*s(138)+15 Such that:aux(69) =< 1 aux(70) =< V aux(71) =< V+1 s(138) =< aux(69) s(134) =< aux(70) s(133) =< aux(71) with precondition: [V1=V,V15>=0,Out>=V1+6,2*V1+5>=Out] * Chain [76,89]: 4*s(133)+2*s(134)+2*s(138)+8 Such that:aux(69) =< 1 aux(70) =< V aux(71) =< V+1 s(138) =< aux(69) s(134) =< aux(70) s(133) =< aux(71) with precondition: [V1=V,V15>=0,Out>=V1+7,2*V1+6>=Out] * Chain [75,91]: 4*s(141)+4*s(142)+1*s(148)+6 Such that:s(148) =< 1 aux(76) =< V aux(77) =< V+1 s(141) =< aux(76) s(142) =< aux(77) with precondition: [V15>=0,Out>=5,V1>=V,2*V+3>=Out] * Chain [75,90]: 4*s(141)+4*s(142)+1*s(148)+15 Such that:s(148) =< 1 aux(76) =< V aux(77) =< V+1 s(141) =< aux(76) s(142) =< aux(77) with precondition: [V15>=0,Out>=6,V1>=V,2*V+4>=Out] * Chain [75,89]: 4*s(141)+4*s(142)+1*s(148)+8 Such that:s(148) =< 1 aux(76) =< V aux(77) =< V+1 s(141) =< aux(76) s(142) =< aux(77) with precondition: [V15>=0,Out>=7,V1>=V,2*V+5>=Out] * Chain [74,91]: 4*s(150)+2*s(151)+2*s(155)+6 Such that:aux(81) =< 1 aux(82) =< V aux(83) =< V+1 s(155) =< aux(81) s(151) =< aux(82) s(150) =< aux(83) with precondition: [V1=V,V15>=0,Out>=V1+5,2*V1+4>=Out] * Chain [74,90]: 4*s(150)+2*s(151)+2*s(155)+15 Such that:aux(81) =< 1 aux(82) =< V aux(83) =< V+1 s(155) =< aux(81) s(151) =< aux(82) s(150) =< aux(83) with precondition: [V1=V,V15>=0,Out>=V1+6,2*V1+5>=Out] * Chain [74,89]: 4*s(150)+2*s(151)+2*s(155)+8 Such that:aux(81) =< 1 aux(82) =< V aux(83) =< V+1 s(155) =< aux(81) s(151) =< aux(82) s(150) =< aux(83) with precondition: [V1=V,V15>=0,Out>=V1+7,2*V1+6>=Out] * Chain [73,91]: 4*s(158)+4*s(159)+1*s(165)+6 Such that:s(165) =< 1 aux(88) =< V aux(89) =< V+1 s(158) =< aux(88) s(159) =< aux(89) with precondition: [V15>=0,Out>=5,V1>=V,2*V+3>=Out] * Chain [73,90]: 4*s(158)+4*s(159)+1*s(165)+15 Such that:s(165) =< 1 aux(88) =< V aux(89) =< V+1 s(158) =< aux(88) s(159) =< aux(89) with precondition: [V15>=0,Out>=6,V1>=V,2*V+4>=Out] * Chain [73,89]: 4*s(158)+4*s(159)+1*s(165)+8 Such that:s(165) =< 1 aux(88) =< V aux(89) =< V+1 s(158) =< aux(88) s(159) =< aux(89) with precondition: [V15>=0,Out>=7,V1>=V,2*V+5>=Out] * Chain [72,91]: 6 with precondition: [Out=3,V>=1,V15>=0,V1>=V] * Chain [72,90]: 15 with precondition: [Out=4,V>=1,V15>=0,V1>=V] * Chain [72,89]: 8 with precondition: [Out=5,V>=1,V15>=0,V1>=V] * Chain [71,91]: 4*s(167)+2*s(168)+6 Such that:aux(96) =< 1 aux(97) =< V s(168) =< aux(96) s(167) =< aux(97) with precondition: [V15>=0,Out>=4,V1>=V,V+3>=Out] * Chain [71,90]: 4*s(167)+2*s(168)+15 Such that:aux(96) =< 1 aux(97) =< V s(168) =< aux(96) s(167) =< aux(97) with precondition: [V15>=0,Out>=5,V1>=V,V+4>=Out] * Chain [71,89]: 4*s(167)+2*s(168)+8 Such that:aux(96) =< 1 aux(97) =< V s(168) =< aux(96) s(167) =< aux(97) with precondition: [V15>=0,Out>=6,V1>=V,V+5>=Out] * Chain [70,91]: 1*s(173)+6 Such that:s(173) =< 1 with precondition: [Out=5,V>=1,V15>=0,V1>=V] * Chain [70,90]: 1*s(173)+15 Such that:s(173) =< 1 with precondition: [Out=6,V>=1,V15>=0,V1>=V] * Chain [70,89]: 1*s(173)+8 Such that:s(173) =< 1 with precondition: [Out=7,V>=1,V15>=0,V1>=V] * Chain [69,91]: 6 with precondition: [Out=3,V>=1,V15>=0,V1>=V] * Chain [69,90]: 15 with precondition: [Out=4,V>=1,V15>=0,V1>=V] * Chain [69,89]: 8 with precondition: [Out=5,V>=1,V15>=0,V1>=V] * Chain [68,91]: 4*s(174)+2*s(175)+6 Such that:aux(107) =< 1 aux(108) =< V s(175) =< aux(107) s(174) =< aux(108) with precondition: [V15>=0,Out>=4,V1>=V,V+3>=Out] * Chain [68,90]: 4*s(174)+2*s(175)+15 Such that:aux(107) =< 1 aux(108) =< V s(175) =< aux(107) s(174) =< aux(108) with precondition: [V15>=0,Out>=5,V1>=V,V+4>=Out] * Chain [68,89]: 4*s(174)+2*s(175)+8 Such that:aux(107) =< 1 aux(108) =< V s(175) =< aux(107) s(174) =< aux(108) with precondition: [V15>=0,Out>=6,V1>=V,V+5>=Out] * Chain [67,91]: 1*s(180)+6 Such that:s(180) =< 1 with precondition: [Out=5,V>=1,V15>=0,V1>=V] * Chain [67,90]: 1*s(180)+15 Such that:s(180) =< 1 with precondition: [Out=6,V>=1,V15>=0,V1>=V] * Chain [67,89]: 1*s(180)+8 Such that:s(180) =< 1 with precondition: [Out=7,V>=1,V15>=0,V1>=V] #### Cost of chains of quot(V1,V,Out): * Chain [94]: 0 with precondition: [Out=0,V1>=0,V>=0] * Chain [93]: 0 with precondition: [V=0,Out=1,V1>=0] * Chain [92]: 0 with precondition: [V>=1,Out>=0,V1>=V,V1+1>=Out+V] #### Cost of chains of start(V1,V,V15,V22,V23): * Chain [102]: 70*s(1158)+334*s(1159)+172*s(1170)+168*s(1172)+2408*s(1175)+688*s(1176)+86*s(1178)+1032*s(1180)+344*s(1181)+1634*s(1182)+280*s(1184)+80*s(1185)+10*s(1187)+120*s(1189)+40*s(1190)+190*s(1191)+210*s(1192)+280*s(1194)+80*s(1195)+10*s(1196)+120*s(1198)+40*s(1199)+19 Such that:aux(157) =< 1 aux(158) =< V1 aux(159) =< V1+1 aux(160) =< V1+3/4 aux(161) =< V1-V aux(162) =< V1-V+1 aux(163) =< V aux(164) =< V+1 s(1170) =< aux(157) s(1192) =< aux(158) s(1158) =< aux(159) s(1159) =< aux(163) s(1172) =< aux(164) s(1174) =< aux(158) s(1175) =< aux(158) s(1176) =< aux(158) s(1177) =< aux(158) s(1176) =< aux(160) s(1178) =< aux(160) s(1179) =< aux(160) s(1174) =< aux(162) s(1175) =< aux(162) s(1176) =< aux(162) s(1174) =< aux(161) s(1175) =< aux(161) s(1176) =< aux(161) s(1177) =< aux(161) s(1178) =< aux(161) s(1179) =< aux(161) s(1180) =< s(1174) s(1181) =< s(1179) s(1182) =< s(1177) s(1183) =< aux(158) s(1184) =< aux(158) s(1185) =< aux(158) s(1186) =< aux(158) s(1185) =< aux(160) s(1187) =< aux(160) s(1188) =< aux(160) s(1183) =< aux(162) s(1184) =< aux(162) s(1185) =< aux(162) s(1183) =< aux(159) s(1184) =< aux(159) s(1185) =< aux(159) s(1186) =< aux(159) s(1187) =< aux(159) s(1188) =< aux(159) s(1189) =< s(1183) s(1190) =< s(1188) s(1191) =< s(1186) s(1193) =< aux(158) s(1194) =< aux(158) s(1195) =< aux(158) s(1195) =< aux(160) s(1196) =< aux(160) s(1197) =< aux(160) s(1193) =< aux(162) s(1194) =< aux(162) s(1195) =< aux(162) s(1196) =< aux(158) s(1197) =< aux(158) s(1198) =< s(1193) s(1199) =< s(1197) with precondition: [V1>=0] * Chain [101]: 1 with precondition: [V1=1,V>=0,V15>=0,V22>=0,V23>=0] * Chain [100]: 1 with precondition: [V1=2,V=1,V15>=0,V22>=0,V23>=0] * Chain [99]: 1068*s(1454)+2025*s(1455)+1008*s(1456)+408*s(1457)+14448*s(1459)+4128*s(1460)+516*s(1462)+6192*s(1464)+2064*s(1465)+9804*s(1466)+1680*s(1468)+480*s(1469)+60*s(1471)+720*s(1473)+240*s(1474)+1140*s(1475)+1260*s(1476)+1680*s(1478)+480*s(1479)+60*s(1480)+720*s(1482)+240*s(1483)+9*s(2298)+9*s(2299)+18*s(3205)+36*s(3206)+18*s(3223)+36*s(3224)+20 Such that:aux(180) =< 1 aux(181) =< V1 aux(182) =< V1+1 aux(183) =< V aux(184) =< V+1 aux(185) =< V15 aux(186) =< V15+1 aux(187) =< V15-2*V22 aux(188) =< V15-2*V22+1 aux(189) =< V15-V22 aux(190) =< V15-V22+1 aux(191) =< V15-V22+3/4 aux(192) =< V22 aux(193) =< V22+1 s(1454) =< aux(180) s(2299) =< aux(185) s(2298) =< aux(186) s(1476) =< aux(189) s(1457) =< aux(190) s(1455) =< aux(192) s(1456) =< aux(193) s(1458) =< aux(189) s(1459) =< aux(189) s(1460) =< aux(189) s(1461) =< aux(189) s(1460) =< aux(191) s(1462) =< aux(191) s(1463) =< aux(191) s(1458) =< aux(188) s(1459) =< aux(188) s(1460) =< aux(188) s(1458) =< aux(187) s(1459) =< aux(187) s(1460) =< aux(187) s(1461) =< aux(187) s(1462) =< aux(187) s(1463) =< aux(187) s(1464) =< s(1458) s(1465) =< s(1463) s(1466) =< s(1461) s(1467) =< aux(189) s(1468) =< aux(189) s(1469) =< aux(189) s(1470) =< aux(189) s(1469) =< aux(191) s(1471) =< aux(191) s(1472) =< aux(191) s(1467) =< aux(188) s(1468) =< aux(188) s(1469) =< aux(188) s(1467) =< aux(190) s(1468) =< aux(190) s(1469) =< aux(190) s(1470) =< aux(190) s(1471) =< aux(190) s(1472) =< aux(190) s(1473) =< s(1467) s(1474) =< s(1472) s(1475) =< s(1470) s(1477) =< aux(189) s(1478) =< aux(189) s(1479) =< aux(189) s(1479) =< aux(191) s(1480) =< aux(191) s(1481) =< aux(191) s(1477) =< aux(188) s(1478) =< aux(188) s(1479) =< aux(188) s(1480) =< aux(189) s(1481) =< aux(189) s(1482) =< s(1477) s(1483) =< s(1481) s(3205) =< aux(183) s(3206) =< aux(184) s(3223) =< aux(181) s(3224) =< aux(182) with precondition: [V1=V,V1>=1] * Chain [98]: 5 with precondition: [V1=2,V=2,V22=0,V15>=0,V23>=0] * Chain [97]: 216*s(3240)+225*s(3241)+432*s(3242)+17 Such that:aux(203) =< 1 aux(204) =< V22 aux(205) =< V22+1 s(3240) =< aux(203) s(3241) =< aux(204) s(3242) =< aux(205) with precondition: [V1=2,V=2,V15=2*V22,V15>=2,V23>=0] * Chain [96]: 9*s(3462)+3*s(3463)+13 Such that:aux(206) =< V22 aux(207) =< V22+1 s(3463) =< aux(206) s(3462) =< aux(207) with precondition: [V1=2,V=2,V15=V22,V15>=1,V23>=0] * Chain [95]: 4 with precondition: [V=0,V1>=0] Closed-form bounds of start(V1,V,V15,V22,V23): ------------------------------------- * Chain [102] with precondition: [V1>=0] - Upper bound: 7122*V1+191+nat(V)*334+(70*V1+70)+(530*V1+795/2)+nat(V+1)*168 - Complexity: n * Chain [101] with precondition: [V1=1,V>=0,V15>=0,V22>=0,V23>=0] - Upper bound: 1 - Complexity: constant * Chain [100] with precondition: [V1=2,V=1,V15>=0,V22>=0,V23>=0] - Upper bound: 1 - Complexity: constant * Chain [99] with precondition: [V1=V,V1>=1] - Upper bound: 18*V1+18*V+1088+nat(V15)*9+nat(V22)*2025+(36*V1+36)+(36*V+36)+nat(V15+1)*9+nat(V22+1)*1008+nat(V15-V22+1)*408+nat(V15-V22+3/4)*3180+nat(V15-V22)*42732 - Complexity: n * Chain [98] with precondition: [V1=2,V=2,V22=0,V15>=0,V23>=0] - Upper bound: 5 - Complexity: constant * Chain [97] with precondition: [V1=2,V=2,V15=2*V22,V15>=2,V23>=0] - Upper bound: 657*V22+665 - Complexity: n * Chain [96] with precondition: [V1=2,V=2,V15=V22,V15>=1,V23>=0] - Upper bound: 12*V22+22 - Complexity: n * Chain [95] with precondition: [V=0,V1>=0] - Upper bound: 4 - Complexity: constant ### Maximum cost of start(V1,V,V15,V22,V23): max([max([4,7122*V1+190+nat(V)*334+(70*V1+70)+(530*V1+795/2)+nat(V+1)*168]),18*V1+855+nat(V)*18+nat(V15)*9+nat(V22)*1800+(36*V1+36)+nat(V+1)*36+nat(V15+1)*9+nat(V22+1)*576+nat(V15-V22+1)*408+nat(V15-V22+3/4)*3180+nat(V15-V22)*42732+(nat(V22)*222+220+nat(V22+1)*423)+(nat(V22)*3+12+nat(V22+1)*9)])+1 Asymptotic class: n * Total analysis performed in 14773 ms. ---------------------------------------- (12) BOUNDS(1, n^1) ---------------------------------------- (13) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (14) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: GE(z0, 0') -> c GE(0', s(z0)) -> c1 GE(s(z0), s(z1)) -> c2(GE(z0, z1)) MINUS(z0, 0') -> c3 MINUS(0', z0) -> c4 MINUS(s(z0), s(z1)) -> c5(MINUS(z0, z1)) ID_INC(z0) -> c6 ID_INC(z0) -> c7 QUOT(z0, z1) -> c8(DIV(z0, z1, 0')) DIV(z0, z1, z2) -> c9(IF(ge(z1, s(0')), ge(z0, z1), z0, z1, z2), GE(z1, s(0'))) DIV(z0, z1, z2) -> c10(IF(ge(z1, s(0')), ge(z0, z1), z0, z1, z2), GE(z0, z1)) IF(false, z0, z1, z2, z3) -> c11 IF(true, false, z0, z1, z2) -> c12 IF(true, true, z0, z1, z2) -> c13(DIV(minus(z0, z1), z1, id_inc(z2)), MINUS(z0, z1)) IF(true, true, z0, z1, z2) -> c14(DIV(minus(z0, z1), z1, id_inc(z2)), ID_INC(z2)) The (relative) TRS S consists of the following rules: ge(z0, 0') -> true ge(0', s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) minus(z0, 0') -> z0 minus(0', z0) -> 0' minus(s(z0), s(z1)) -> minus(z0, z1) id_inc(z0) -> z0 id_inc(z0) -> s(z0) quot(z0, z1) -> div(z0, z1, 0') div(z0, z1, z2) -> if(ge(z1, s(0')), ge(z0, z1), z0, z1, z2) if(false, z0, z1, z2, z3) -> div_by_zero if(true, false, z0, z1, z2) -> z2 if(true, true, z0, z1, z2) -> div(minus(z0, z1), z1, id_inc(z2)) Rewrite Strategy: INNERMOST ---------------------------------------- (15) SlicingProof (LOWER BOUND(ID)) Sliced the following arguments: ID_INC/0 ---------------------------------------- (16) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: GE(z0, 0') -> c GE(0', s(z0)) -> c1 GE(s(z0), s(z1)) -> c2(GE(z0, z1)) MINUS(z0, 0') -> c3 MINUS(0', z0) -> c4 MINUS(s(z0), s(z1)) -> c5(MINUS(z0, z1)) ID_INC -> c6 ID_INC -> c7 QUOT(z0, z1) -> c8(DIV(z0, z1, 0')) DIV(z0, z1, z2) -> c9(IF(ge(z1, s(0')), ge(z0, z1), z0, z1, z2), GE(z1, s(0'))) DIV(z0, z1, z2) -> c10(IF(ge(z1, s(0')), ge(z0, z1), z0, z1, z2), GE(z0, z1)) IF(false, z0, z1, z2, z3) -> c11 IF(true, false, z0, z1, z2) -> c12 IF(true, true, z0, z1, z2) -> c13(DIV(minus(z0, z1), z1, id_inc(z2)), MINUS(z0, z1)) IF(true, true, z0, z1, z2) -> c14(DIV(minus(z0, z1), z1, id_inc(z2)), ID_INC) The (relative) TRS S consists of the following rules: ge(z0, 0') -> true ge(0', s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) minus(z0, 0') -> z0 minus(0', z0) -> 0' minus(s(z0), s(z1)) -> minus(z0, z1) id_inc(z0) -> z0 id_inc(z0) -> s(z0) quot(z0, z1) -> div(z0, z1, 0') div(z0, z1, z2) -> if(ge(z1, s(0')), ge(z0, z1), z0, z1, z2) if(false, z0, z1, z2, z3) -> div_by_zero if(true, false, z0, z1, z2) -> z2 if(true, true, z0, z1, z2) -> div(minus(z0, z1), z1, id_inc(z2)) Rewrite Strategy: INNERMOST ---------------------------------------- (17) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (18) Obligation: Innermost TRS: Rules: GE(z0, 0') -> c GE(0', s(z0)) -> c1 GE(s(z0), s(z1)) -> c2(GE(z0, z1)) MINUS(z0, 0') -> c3 MINUS(0', z0) -> c4 MINUS(s(z0), s(z1)) -> c5(MINUS(z0, z1)) ID_INC -> c6 ID_INC -> c7 QUOT(z0, z1) -> c8(DIV(z0, z1, 0')) DIV(z0, z1, z2) -> c9(IF(ge(z1, s(0')), ge(z0, z1), z0, z1, z2), GE(z1, s(0'))) DIV(z0, z1, z2) -> c10(IF(ge(z1, s(0')), ge(z0, z1), z0, z1, z2), GE(z0, z1)) IF(false, z0, z1, z2, z3) -> c11 IF(true, false, z0, z1, z2) -> c12 IF(true, true, z0, z1, z2) -> c13(DIV(minus(z0, z1), z1, id_inc(z2)), MINUS(z0, z1)) IF(true, true, z0, z1, z2) -> c14(DIV(minus(z0, z1), z1, id_inc(z2)), ID_INC) ge(z0, 0') -> true ge(0', s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) minus(z0, 0') -> z0 minus(0', z0) -> 0' minus(s(z0), s(z1)) -> minus(z0, z1) id_inc(z0) -> z0 id_inc(z0) -> s(z0) quot(z0, z1) -> div(z0, z1, 0') div(z0, z1, z2) -> if(ge(z1, s(0')), ge(z0, z1), z0, z1, z2) if(false, z0, z1, z2, z3) -> div_by_zero if(true, false, z0, z1, z2) -> z2 if(true, true, z0, z1, z2) -> div(minus(z0, z1), z1, id_inc(z2)) Types: GE :: 0':s:div_by_zero -> 0':s:div_by_zero -> c:c1:c2 0' :: 0':s:div_by_zero c :: c:c1:c2 s :: 0':s:div_by_zero -> 0':s:div_by_zero c1 :: c:c1:c2 c2 :: c:c1:c2 -> c:c1:c2 MINUS :: 0':s:div_by_zero -> 0':s:div_by_zero -> c3:c4:c5 c3 :: c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 -> c3:c4:c5 ID_INC :: c6:c7 c6 :: c6:c7 c7 :: c6:c7 QUOT :: 0':s:div_by_zero -> 0':s:div_by_zero -> c8 c8 :: c9:c10 -> c8 DIV :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero -> c9:c10 c9 :: c11:c12:c13:c14 -> c:c1:c2 -> c9:c10 IF :: false:true -> false:true -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero -> c11:c12:c13:c14 ge :: 0':s:div_by_zero -> 0':s:div_by_zero -> false:true c10 :: c11:c12:c13:c14 -> c:c1:c2 -> c9:c10 false :: false:true c11 :: c11:c12:c13:c14 true :: false:true c12 :: c11:c12:c13:c14 c13 :: c9:c10 -> c3:c4:c5 -> c11:c12:c13:c14 minus :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero id_inc :: 0':s:div_by_zero -> 0':s:div_by_zero c14 :: c9:c10 -> c6:c7 -> c11:c12:c13:c14 quot :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero div :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero if :: false:true -> false:true -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero div_by_zero :: 0':s:div_by_zero hole_c:c1:c21_15 :: c:c1:c2 hole_0':s:div_by_zero2_15 :: 0':s:div_by_zero hole_c3:c4:c53_15 :: c3:c4:c5 hole_c6:c74_15 :: c6:c7 hole_c85_15 :: c8 hole_c9:c106_15 :: c9:c10 hole_c11:c12:c13:c147_15 :: c11:c12:c13:c14 hole_false:true8_15 :: false:true gen_c:c1:c29_15 :: Nat -> c:c1:c2 gen_0':s:div_by_zero10_15 :: Nat -> 0':s:div_by_zero gen_c3:c4:c511_15 :: Nat -> c3:c4:c5 ---------------------------------------- (19) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: GE, MINUS, DIV, ge, minus, div They will be analysed ascendingly in the following order: GE < DIV MINUS < DIV ge < DIV minus < DIV ge < div minus < div ---------------------------------------- (20) Obligation: Innermost TRS: Rules: GE(z0, 0') -> c GE(0', s(z0)) -> c1 GE(s(z0), s(z1)) -> c2(GE(z0, z1)) MINUS(z0, 0') -> c3 MINUS(0', z0) -> c4 MINUS(s(z0), s(z1)) -> c5(MINUS(z0, z1)) ID_INC -> c6 ID_INC -> c7 QUOT(z0, z1) -> c8(DIV(z0, z1, 0')) DIV(z0, z1, z2) -> c9(IF(ge(z1, s(0')), ge(z0, z1), z0, z1, z2), GE(z1, s(0'))) DIV(z0, z1, z2) -> c10(IF(ge(z1, s(0')), ge(z0, z1), z0, z1, z2), GE(z0, z1)) IF(false, z0, z1, z2, z3) -> c11 IF(true, false, z0, z1, z2) -> c12 IF(true, true, z0, z1, z2) -> c13(DIV(minus(z0, z1), z1, id_inc(z2)), MINUS(z0, z1)) IF(true, true, z0, z1, z2) -> c14(DIV(minus(z0, z1), z1, id_inc(z2)), ID_INC) ge(z0, 0') -> true ge(0', s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) minus(z0, 0') -> z0 minus(0', z0) -> 0' minus(s(z0), s(z1)) -> minus(z0, z1) id_inc(z0) -> z0 id_inc(z0) -> s(z0) quot(z0, z1) -> div(z0, z1, 0') div(z0, z1, z2) -> if(ge(z1, s(0')), ge(z0, z1), z0, z1, z2) if(false, z0, z1, z2, z3) -> div_by_zero if(true, false, z0, z1, z2) -> z2 if(true, true, z0, z1, z2) -> div(minus(z0, z1), z1, id_inc(z2)) Types: GE :: 0':s:div_by_zero -> 0':s:div_by_zero -> c:c1:c2 0' :: 0':s:div_by_zero c :: c:c1:c2 s :: 0':s:div_by_zero -> 0':s:div_by_zero c1 :: c:c1:c2 c2 :: c:c1:c2 -> c:c1:c2 MINUS :: 0':s:div_by_zero -> 0':s:div_by_zero -> c3:c4:c5 c3 :: c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 -> c3:c4:c5 ID_INC :: c6:c7 c6 :: c6:c7 c7 :: c6:c7 QUOT :: 0':s:div_by_zero -> 0':s:div_by_zero -> c8 c8 :: c9:c10 -> c8 DIV :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero -> c9:c10 c9 :: c11:c12:c13:c14 -> c:c1:c2 -> c9:c10 IF :: false:true -> false:true -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero -> c11:c12:c13:c14 ge :: 0':s:div_by_zero -> 0':s:div_by_zero -> false:true c10 :: c11:c12:c13:c14 -> c:c1:c2 -> c9:c10 false :: false:true c11 :: c11:c12:c13:c14 true :: false:true c12 :: c11:c12:c13:c14 c13 :: c9:c10 -> c3:c4:c5 -> c11:c12:c13:c14 minus :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero id_inc :: 0':s:div_by_zero -> 0':s:div_by_zero c14 :: c9:c10 -> c6:c7 -> c11:c12:c13:c14 quot :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero div :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero if :: false:true -> false:true -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero div_by_zero :: 0':s:div_by_zero hole_c:c1:c21_15 :: c:c1:c2 hole_0':s:div_by_zero2_15 :: 0':s:div_by_zero hole_c3:c4:c53_15 :: c3:c4:c5 hole_c6:c74_15 :: c6:c7 hole_c85_15 :: c8 hole_c9:c106_15 :: c9:c10 hole_c11:c12:c13:c147_15 :: c11:c12:c13:c14 hole_false:true8_15 :: false:true gen_c:c1:c29_15 :: Nat -> c:c1:c2 gen_0':s:div_by_zero10_15 :: Nat -> 0':s:div_by_zero gen_c3:c4:c511_15 :: Nat -> c3:c4:c5 Generator Equations: gen_c:c1:c29_15(0) <=> c gen_c:c1:c29_15(+(x, 1)) <=> c2(gen_c:c1:c29_15(x)) gen_0':s:div_by_zero10_15(0) <=> 0' gen_0':s:div_by_zero10_15(+(x, 1)) <=> s(gen_0':s:div_by_zero10_15(x)) gen_c3:c4:c511_15(0) <=> c3 gen_c3:c4:c511_15(+(x, 1)) <=> c5(gen_c3:c4:c511_15(x)) The following defined symbols remain to be analysed: GE, MINUS, DIV, ge, minus, div They will be analysed ascendingly in the following order: GE < DIV MINUS < DIV ge < DIV minus < DIV ge < div minus < div ---------------------------------------- (21) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: GE(gen_0':s:div_by_zero10_15(n13_15), gen_0':s:div_by_zero10_15(n13_15)) -> gen_c:c1:c29_15(n13_15), rt in Omega(1 + n13_15) Induction Base: GE(gen_0':s:div_by_zero10_15(0), gen_0':s:div_by_zero10_15(0)) ->_R^Omega(1) c Induction Step: GE(gen_0':s:div_by_zero10_15(+(n13_15, 1)), gen_0':s:div_by_zero10_15(+(n13_15, 1))) ->_R^Omega(1) c2(GE(gen_0':s:div_by_zero10_15(n13_15), gen_0':s:div_by_zero10_15(n13_15))) ->_IH c2(gen_c:c1:c29_15(c14_15)) 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: GE(z0, 0') -> c GE(0', s(z0)) -> c1 GE(s(z0), s(z1)) -> c2(GE(z0, z1)) MINUS(z0, 0') -> c3 MINUS(0', z0) -> c4 MINUS(s(z0), s(z1)) -> c5(MINUS(z0, z1)) ID_INC -> c6 ID_INC -> c7 QUOT(z0, z1) -> c8(DIV(z0, z1, 0')) DIV(z0, z1, z2) -> c9(IF(ge(z1, s(0')), ge(z0, z1), z0, z1, z2), GE(z1, s(0'))) DIV(z0, z1, z2) -> c10(IF(ge(z1, s(0')), ge(z0, z1), z0, z1, z2), GE(z0, z1)) IF(false, z0, z1, z2, z3) -> c11 IF(true, false, z0, z1, z2) -> c12 IF(true, true, z0, z1, z2) -> c13(DIV(minus(z0, z1), z1, id_inc(z2)), MINUS(z0, z1)) IF(true, true, z0, z1, z2) -> c14(DIV(minus(z0, z1), z1, id_inc(z2)), ID_INC) ge(z0, 0') -> true ge(0', s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) minus(z0, 0') -> z0 minus(0', z0) -> 0' minus(s(z0), s(z1)) -> minus(z0, z1) id_inc(z0) -> z0 id_inc(z0) -> s(z0) quot(z0, z1) -> div(z0, z1, 0') div(z0, z1, z2) -> if(ge(z1, s(0')), ge(z0, z1), z0, z1, z2) if(false, z0, z1, z2, z3) -> div_by_zero if(true, false, z0, z1, z2) -> z2 if(true, true, z0, z1, z2) -> div(minus(z0, z1), z1, id_inc(z2)) Types: GE :: 0':s:div_by_zero -> 0':s:div_by_zero -> c:c1:c2 0' :: 0':s:div_by_zero c :: c:c1:c2 s :: 0':s:div_by_zero -> 0':s:div_by_zero c1 :: c:c1:c2 c2 :: c:c1:c2 -> c:c1:c2 MINUS :: 0':s:div_by_zero -> 0':s:div_by_zero -> c3:c4:c5 c3 :: c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 -> c3:c4:c5 ID_INC :: c6:c7 c6 :: c6:c7 c7 :: c6:c7 QUOT :: 0':s:div_by_zero -> 0':s:div_by_zero -> c8 c8 :: c9:c10 -> c8 DIV :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero -> c9:c10 c9 :: c11:c12:c13:c14 -> c:c1:c2 -> c9:c10 IF :: false:true -> false:true -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero -> c11:c12:c13:c14 ge :: 0':s:div_by_zero -> 0':s:div_by_zero -> false:true c10 :: c11:c12:c13:c14 -> c:c1:c2 -> c9:c10 false :: false:true c11 :: c11:c12:c13:c14 true :: false:true c12 :: c11:c12:c13:c14 c13 :: c9:c10 -> c3:c4:c5 -> c11:c12:c13:c14 minus :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero id_inc :: 0':s:div_by_zero -> 0':s:div_by_zero c14 :: c9:c10 -> c6:c7 -> c11:c12:c13:c14 quot :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero div :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero if :: false:true -> false:true -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero div_by_zero :: 0':s:div_by_zero hole_c:c1:c21_15 :: c:c1:c2 hole_0':s:div_by_zero2_15 :: 0':s:div_by_zero hole_c3:c4:c53_15 :: c3:c4:c5 hole_c6:c74_15 :: c6:c7 hole_c85_15 :: c8 hole_c9:c106_15 :: c9:c10 hole_c11:c12:c13:c147_15 :: c11:c12:c13:c14 hole_false:true8_15 :: false:true gen_c:c1:c29_15 :: Nat -> c:c1:c2 gen_0':s:div_by_zero10_15 :: Nat -> 0':s:div_by_zero gen_c3:c4:c511_15 :: Nat -> c3:c4:c5 Generator Equations: gen_c:c1:c29_15(0) <=> c gen_c:c1:c29_15(+(x, 1)) <=> c2(gen_c:c1:c29_15(x)) gen_0':s:div_by_zero10_15(0) <=> 0' gen_0':s:div_by_zero10_15(+(x, 1)) <=> s(gen_0':s:div_by_zero10_15(x)) gen_c3:c4:c511_15(0) <=> c3 gen_c3:c4:c511_15(+(x, 1)) <=> c5(gen_c3:c4:c511_15(x)) The following defined symbols remain to be analysed: GE, MINUS, DIV, ge, minus, div They will be analysed ascendingly in the following order: GE < DIV MINUS < DIV ge < DIV minus < DIV ge < div minus < div ---------------------------------------- (24) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (25) BOUNDS(n^1, INF) ---------------------------------------- (26) Obligation: Innermost TRS: Rules: GE(z0, 0') -> c GE(0', s(z0)) -> c1 GE(s(z0), s(z1)) -> c2(GE(z0, z1)) MINUS(z0, 0') -> c3 MINUS(0', z0) -> c4 MINUS(s(z0), s(z1)) -> c5(MINUS(z0, z1)) ID_INC -> c6 ID_INC -> c7 QUOT(z0, z1) -> c8(DIV(z0, z1, 0')) DIV(z0, z1, z2) -> c9(IF(ge(z1, s(0')), ge(z0, z1), z0, z1, z2), GE(z1, s(0'))) DIV(z0, z1, z2) -> c10(IF(ge(z1, s(0')), ge(z0, z1), z0, z1, z2), GE(z0, z1)) IF(false, z0, z1, z2, z3) -> c11 IF(true, false, z0, z1, z2) -> c12 IF(true, true, z0, z1, z2) -> c13(DIV(minus(z0, z1), z1, id_inc(z2)), MINUS(z0, z1)) IF(true, true, z0, z1, z2) -> c14(DIV(minus(z0, z1), z1, id_inc(z2)), ID_INC) ge(z0, 0') -> true ge(0', s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) minus(z0, 0') -> z0 minus(0', z0) -> 0' minus(s(z0), s(z1)) -> minus(z0, z1) id_inc(z0) -> z0 id_inc(z0) -> s(z0) quot(z0, z1) -> div(z0, z1, 0') div(z0, z1, z2) -> if(ge(z1, s(0')), ge(z0, z1), z0, z1, z2) if(false, z0, z1, z2, z3) -> div_by_zero if(true, false, z0, z1, z2) -> z2 if(true, true, z0, z1, z2) -> div(minus(z0, z1), z1, id_inc(z2)) Types: GE :: 0':s:div_by_zero -> 0':s:div_by_zero -> c:c1:c2 0' :: 0':s:div_by_zero c :: c:c1:c2 s :: 0':s:div_by_zero -> 0':s:div_by_zero c1 :: c:c1:c2 c2 :: c:c1:c2 -> c:c1:c2 MINUS :: 0':s:div_by_zero -> 0':s:div_by_zero -> c3:c4:c5 c3 :: c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 -> c3:c4:c5 ID_INC :: c6:c7 c6 :: c6:c7 c7 :: c6:c7 QUOT :: 0':s:div_by_zero -> 0':s:div_by_zero -> c8 c8 :: c9:c10 -> c8 DIV :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero -> c9:c10 c9 :: c11:c12:c13:c14 -> c:c1:c2 -> c9:c10 IF :: false:true -> false:true -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero -> c11:c12:c13:c14 ge :: 0':s:div_by_zero -> 0':s:div_by_zero -> false:true c10 :: c11:c12:c13:c14 -> c:c1:c2 -> c9:c10 false :: false:true c11 :: c11:c12:c13:c14 true :: false:true c12 :: c11:c12:c13:c14 c13 :: c9:c10 -> c3:c4:c5 -> c11:c12:c13:c14 minus :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero id_inc :: 0':s:div_by_zero -> 0':s:div_by_zero c14 :: c9:c10 -> c6:c7 -> c11:c12:c13:c14 quot :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero div :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero if :: false:true -> false:true -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero div_by_zero :: 0':s:div_by_zero hole_c:c1:c21_15 :: c:c1:c2 hole_0':s:div_by_zero2_15 :: 0':s:div_by_zero hole_c3:c4:c53_15 :: c3:c4:c5 hole_c6:c74_15 :: c6:c7 hole_c85_15 :: c8 hole_c9:c106_15 :: c9:c10 hole_c11:c12:c13:c147_15 :: c11:c12:c13:c14 hole_false:true8_15 :: false:true gen_c:c1:c29_15 :: Nat -> c:c1:c2 gen_0':s:div_by_zero10_15 :: Nat -> 0':s:div_by_zero gen_c3:c4:c511_15 :: Nat -> c3:c4:c5 Lemmas: GE(gen_0':s:div_by_zero10_15(n13_15), gen_0':s:div_by_zero10_15(n13_15)) -> gen_c:c1:c29_15(n13_15), rt in Omega(1 + n13_15) Generator Equations: gen_c:c1:c29_15(0) <=> c gen_c:c1:c29_15(+(x, 1)) <=> c2(gen_c:c1:c29_15(x)) gen_0':s:div_by_zero10_15(0) <=> 0' gen_0':s:div_by_zero10_15(+(x, 1)) <=> s(gen_0':s:div_by_zero10_15(x)) gen_c3:c4:c511_15(0) <=> c3 gen_c3:c4:c511_15(+(x, 1)) <=> c5(gen_c3:c4:c511_15(x)) The following defined symbols remain to be analysed: MINUS, DIV, ge, minus, div They will be analysed ascendingly in the following order: MINUS < DIV ge < DIV minus < DIV ge < div minus < div ---------------------------------------- (27) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: MINUS(gen_0':s:div_by_zero10_15(n664_15), gen_0':s:div_by_zero10_15(n664_15)) -> gen_c3:c4:c511_15(n664_15), rt in Omega(1 + n664_15) Induction Base: MINUS(gen_0':s:div_by_zero10_15(0), gen_0':s:div_by_zero10_15(0)) ->_R^Omega(1) c3 Induction Step: MINUS(gen_0':s:div_by_zero10_15(+(n664_15, 1)), gen_0':s:div_by_zero10_15(+(n664_15, 1))) ->_R^Omega(1) c5(MINUS(gen_0':s:div_by_zero10_15(n664_15), gen_0':s:div_by_zero10_15(n664_15))) ->_IH c5(gen_c3:c4:c511_15(c665_15)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (28) Obligation: Innermost TRS: Rules: GE(z0, 0') -> c GE(0', s(z0)) -> c1 GE(s(z0), s(z1)) -> c2(GE(z0, z1)) MINUS(z0, 0') -> c3 MINUS(0', z0) -> c4 MINUS(s(z0), s(z1)) -> c5(MINUS(z0, z1)) ID_INC -> c6 ID_INC -> c7 QUOT(z0, z1) -> c8(DIV(z0, z1, 0')) DIV(z0, z1, z2) -> c9(IF(ge(z1, s(0')), ge(z0, z1), z0, z1, z2), GE(z1, s(0'))) DIV(z0, z1, z2) -> c10(IF(ge(z1, s(0')), ge(z0, z1), z0, z1, z2), GE(z0, z1)) IF(false, z0, z1, z2, z3) -> c11 IF(true, false, z0, z1, z2) -> c12 IF(true, true, z0, z1, z2) -> c13(DIV(minus(z0, z1), z1, id_inc(z2)), MINUS(z0, z1)) IF(true, true, z0, z1, z2) -> c14(DIV(minus(z0, z1), z1, id_inc(z2)), ID_INC) ge(z0, 0') -> true ge(0', s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) minus(z0, 0') -> z0 minus(0', z0) -> 0' minus(s(z0), s(z1)) -> minus(z0, z1) id_inc(z0) -> z0 id_inc(z0) -> s(z0) quot(z0, z1) -> div(z0, z1, 0') div(z0, z1, z2) -> if(ge(z1, s(0')), ge(z0, z1), z0, z1, z2) if(false, z0, z1, z2, z3) -> div_by_zero if(true, false, z0, z1, z2) -> z2 if(true, true, z0, z1, z2) -> div(minus(z0, z1), z1, id_inc(z2)) Types: GE :: 0':s:div_by_zero -> 0':s:div_by_zero -> c:c1:c2 0' :: 0':s:div_by_zero c :: c:c1:c2 s :: 0':s:div_by_zero -> 0':s:div_by_zero c1 :: c:c1:c2 c2 :: c:c1:c2 -> c:c1:c2 MINUS :: 0':s:div_by_zero -> 0':s:div_by_zero -> c3:c4:c5 c3 :: c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 -> c3:c4:c5 ID_INC :: c6:c7 c6 :: c6:c7 c7 :: c6:c7 QUOT :: 0':s:div_by_zero -> 0':s:div_by_zero -> c8 c8 :: c9:c10 -> c8 DIV :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero -> c9:c10 c9 :: c11:c12:c13:c14 -> c:c1:c2 -> c9:c10 IF :: false:true -> false:true -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero -> c11:c12:c13:c14 ge :: 0':s:div_by_zero -> 0':s:div_by_zero -> false:true c10 :: c11:c12:c13:c14 -> c:c1:c2 -> c9:c10 false :: false:true c11 :: c11:c12:c13:c14 true :: false:true c12 :: c11:c12:c13:c14 c13 :: c9:c10 -> c3:c4:c5 -> c11:c12:c13:c14 minus :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero id_inc :: 0':s:div_by_zero -> 0':s:div_by_zero c14 :: c9:c10 -> c6:c7 -> c11:c12:c13:c14 quot :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero div :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero if :: false:true -> false:true -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero div_by_zero :: 0':s:div_by_zero hole_c:c1:c21_15 :: c:c1:c2 hole_0':s:div_by_zero2_15 :: 0':s:div_by_zero hole_c3:c4:c53_15 :: c3:c4:c5 hole_c6:c74_15 :: c6:c7 hole_c85_15 :: c8 hole_c9:c106_15 :: c9:c10 hole_c11:c12:c13:c147_15 :: c11:c12:c13:c14 hole_false:true8_15 :: false:true gen_c:c1:c29_15 :: Nat -> c:c1:c2 gen_0':s:div_by_zero10_15 :: Nat -> 0':s:div_by_zero gen_c3:c4:c511_15 :: Nat -> c3:c4:c5 Lemmas: GE(gen_0':s:div_by_zero10_15(n13_15), gen_0':s:div_by_zero10_15(n13_15)) -> gen_c:c1:c29_15(n13_15), rt in Omega(1 + n13_15) MINUS(gen_0':s:div_by_zero10_15(n664_15), gen_0':s:div_by_zero10_15(n664_15)) -> gen_c3:c4:c511_15(n664_15), rt in Omega(1 + n664_15) Generator Equations: gen_c:c1:c29_15(0) <=> c gen_c:c1:c29_15(+(x, 1)) <=> c2(gen_c:c1:c29_15(x)) gen_0':s:div_by_zero10_15(0) <=> 0' gen_0':s:div_by_zero10_15(+(x, 1)) <=> s(gen_0':s:div_by_zero10_15(x)) gen_c3:c4:c511_15(0) <=> c3 gen_c3:c4:c511_15(+(x, 1)) <=> c5(gen_c3:c4:c511_15(x)) The following defined symbols remain to be analysed: ge, DIV, minus, div They will be analysed ascendingly in the following order: ge < DIV minus < DIV ge < div minus < div ---------------------------------------- (29) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: ge(gen_0':s:div_by_zero10_15(n1237_15), gen_0':s:div_by_zero10_15(n1237_15)) -> true, rt in Omega(0) Induction Base: ge(gen_0':s:div_by_zero10_15(0), gen_0':s:div_by_zero10_15(0)) ->_R^Omega(0) true Induction Step: ge(gen_0':s:div_by_zero10_15(+(n1237_15, 1)), gen_0':s:div_by_zero10_15(+(n1237_15, 1))) ->_R^Omega(0) ge(gen_0':s:div_by_zero10_15(n1237_15), gen_0':s:div_by_zero10_15(n1237_15)) ->_IH true We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (30) Obligation: Innermost TRS: Rules: GE(z0, 0') -> c GE(0', s(z0)) -> c1 GE(s(z0), s(z1)) -> c2(GE(z0, z1)) MINUS(z0, 0') -> c3 MINUS(0', z0) -> c4 MINUS(s(z0), s(z1)) -> c5(MINUS(z0, z1)) ID_INC -> c6 ID_INC -> c7 QUOT(z0, z1) -> c8(DIV(z0, z1, 0')) DIV(z0, z1, z2) -> c9(IF(ge(z1, s(0')), ge(z0, z1), z0, z1, z2), GE(z1, s(0'))) DIV(z0, z1, z2) -> c10(IF(ge(z1, s(0')), ge(z0, z1), z0, z1, z2), GE(z0, z1)) IF(false, z0, z1, z2, z3) -> c11 IF(true, false, z0, z1, z2) -> c12 IF(true, true, z0, z1, z2) -> c13(DIV(minus(z0, z1), z1, id_inc(z2)), MINUS(z0, z1)) IF(true, true, z0, z1, z2) -> c14(DIV(minus(z0, z1), z1, id_inc(z2)), ID_INC) ge(z0, 0') -> true ge(0', s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) minus(z0, 0') -> z0 minus(0', z0) -> 0' minus(s(z0), s(z1)) -> minus(z0, z1) id_inc(z0) -> z0 id_inc(z0) -> s(z0) quot(z0, z1) -> div(z0, z1, 0') div(z0, z1, z2) -> if(ge(z1, s(0')), ge(z0, z1), z0, z1, z2) if(false, z0, z1, z2, z3) -> div_by_zero if(true, false, z0, z1, z2) -> z2 if(true, true, z0, z1, z2) -> div(minus(z0, z1), z1, id_inc(z2)) Types: GE :: 0':s:div_by_zero -> 0':s:div_by_zero -> c:c1:c2 0' :: 0':s:div_by_zero c :: c:c1:c2 s :: 0':s:div_by_zero -> 0':s:div_by_zero c1 :: c:c1:c2 c2 :: c:c1:c2 -> c:c1:c2 MINUS :: 0':s:div_by_zero -> 0':s:div_by_zero -> c3:c4:c5 c3 :: c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 -> c3:c4:c5 ID_INC :: c6:c7 c6 :: c6:c7 c7 :: c6:c7 QUOT :: 0':s:div_by_zero -> 0':s:div_by_zero -> c8 c8 :: c9:c10 -> c8 DIV :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero -> c9:c10 c9 :: c11:c12:c13:c14 -> c:c1:c2 -> c9:c10 IF :: false:true -> false:true -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero -> c11:c12:c13:c14 ge :: 0':s:div_by_zero -> 0':s:div_by_zero -> false:true c10 :: c11:c12:c13:c14 -> c:c1:c2 -> c9:c10 false :: false:true c11 :: c11:c12:c13:c14 true :: false:true c12 :: c11:c12:c13:c14 c13 :: c9:c10 -> c3:c4:c5 -> c11:c12:c13:c14 minus :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero id_inc :: 0':s:div_by_zero -> 0':s:div_by_zero c14 :: c9:c10 -> c6:c7 -> c11:c12:c13:c14 quot :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero div :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero if :: false:true -> false:true -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero div_by_zero :: 0':s:div_by_zero hole_c:c1:c21_15 :: c:c1:c2 hole_0':s:div_by_zero2_15 :: 0':s:div_by_zero hole_c3:c4:c53_15 :: c3:c4:c5 hole_c6:c74_15 :: c6:c7 hole_c85_15 :: c8 hole_c9:c106_15 :: c9:c10 hole_c11:c12:c13:c147_15 :: c11:c12:c13:c14 hole_false:true8_15 :: false:true gen_c:c1:c29_15 :: Nat -> c:c1:c2 gen_0':s:div_by_zero10_15 :: Nat -> 0':s:div_by_zero gen_c3:c4:c511_15 :: Nat -> c3:c4:c5 Lemmas: GE(gen_0':s:div_by_zero10_15(n13_15), gen_0':s:div_by_zero10_15(n13_15)) -> gen_c:c1:c29_15(n13_15), rt in Omega(1 + n13_15) MINUS(gen_0':s:div_by_zero10_15(n664_15), gen_0':s:div_by_zero10_15(n664_15)) -> gen_c3:c4:c511_15(n664_15), rt in Omega(1 + n664_15) ge(gen_0':s:div_by_zero10_15(n1237_15), gen_0':s:div_by_zero10_15(n1237_15)) -> true, rt in Omega(0) Generator Equations: gen_c:c1:c29_15(0) <=> c gen_c:c1:c29_15(+(x, 1)) <=> c2(gen_c:c1:c29_15(x)) gen_0':s:div_by_zero10_15(0) <=> 0' gen_0':s:div_by_zero10_15(+(x, 1)) <=> s(gen_0':s:div_by_zero10_15(x)) gen_c3:c4:c511_15(0) <=> c3 gen_c3:c4:c511_15(+(x, 1)) <=> c5(gen_c3:c4:c511_15(x)) The following defined symbols remain to be analysed: minus, DIV, div They will be analysed ascendingly in the following order: minus < DIV minus < div ---------------------------------------- (31) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: minus(gen_0':s:div_by_zero10_15(n1671_15), gen_0':s:div_by_zero10_15(n1671_15)) -> gen_0':s:div_by_zero10_15(0), rt in Omega(0) Induction Base: minus(gen_0':s:div_by_zero10_15(0), gen_0':s:div_by_zero10_15(0)) ->_R^Omega(0) gen_0':s:div_by_zero10_15(0) Induction Step: minus(gen_0':s:div_by_zero10_15(+(n1671_15, 1)), gen_0':s:div_by_zero10_15(+(n1671_15, 1))) ->_R^Omega(0) minus(gen_0':s:div_by_zero10_15(n1671_15), gen_0':s:div_by_zero10_15(n1671_15)) ->_IH gen_0':s:div_by_zero10_15(0) We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (32) Obligation: Innermost TRS: Rules: GE(z0, 0') -> c GE(0', s(z0)) -> c1 GE(s(z0), s(z1)) -> c2(GE(z0, z1)) MINUS(z0, 0') -> c3 MINUS(0', z0) -> c4 MINUS(s(z0), s(z1)) -> c5(MINUS(z0, z1)) ID_INC -> c6 ID_INC -> c7 QUOT(z0, z1) -> c8(DIV(z0, z1, 0')) DIV(z0, z1, z2) -> c9(IF(ge(z1, s(0')), ge(z0, z1), z0, z1, z2), GE(z1, s(0'))) DIV(z0, z1, z2) -> c10(IF(ge(z1, s(0')), ge(z0, z1), z0, z1, z2), GE(z0, z1)) IF(false, z0, z1, z2, z3) -> c11 IF(true, false, z0, z1, z2) -> c12 IF(true, true, z0, z1, z2) -> c13(DIV(minus(z0, z1), z1, id_inc(z2)), MINUS(z0, z1)) IF(true, true, z0, z1, z2) -> c14(DIV(minus(z0, z1), z1, id_inc(z2)), ID_INC) ge(z0, 0') -> true ge(0', s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) minus(z0, 0') -> z0 minus(0', z0) -> 0' minus(s(z0), s(z1)) -> minus(z0, z1) id_inc(z0) -> z0 id_inc(z0) -> s(z0) quot(z0, z1) -> div(z0, z1, 0') div(z0, z1, z2) -> if(ge(z1, s(0')), ge(z0, z1), z0, z1, z2) if(false, z0, z1, z2, z3) -> div_by_zero if(true, false, z0, z1, z2) -> z2 if(true, true, z0, z1, z2) -> div(minus(z0, z1), z1, id_inc(z2)) Types: GE :: 0':s:div_by_zero -> 0':s:div_by_zero -> c:c1:c2 0' :: 0':s:div_by_zero c :: c:c1:c2 s :: 0':s:div_by_zero -> 0':s:div_by_zero c1 :: c:c1:c2 c2 :: c:c1:c2 -> c:c1:c2 MINUS :: 0':s:div_by_zero -> 0':s:div_by_zero -> c3:c4:c5 c3 :: c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 -> c3:c4:c5 ID_INC :: c6:c7 c6 :: c6:c7 c7 :: c6:c7 QUOT :: 0':s:div_by_zero -> 0':s:div_by_zero -> c8 c8 :: c9:c10 -> c8 DIV :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero -> c9:c10 c9 :: c11:c12:c13:c14 -> c:c1:c2 -> c9:c10 IF :: false:true -> false:true -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero -> c11:c12:c13:c14 ge :: 0':s:div_by_zero -> 0':s:div_by_zero -> false:true c10 :: c11:c12:c13:c14 -> c:c1:c2 -> c9:c10 false :: false:true c11 :: c11:c12:c13:c14 true :: false:true c12 :: c11:c12:c13:c14 c13 :: c9:c10 -> c3:c4:c5 -> c11:c12:c13:c14 minus :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero id_inc :: 0':s:div_by_zero -> 0':s:div_by_zero c14 :: c9:c10 -> c6:c7 -> c11:c12:c13:c14 quot :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero div :: 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero if :: false:true -> false:true -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero -> 0':s:div_by_zero div_by_zero :: 0':s:div_by_zero hole_c:c1:c21_15 :: c:c1:c2 hole_0':s:div_by_zero2_15 :: 0':s:div_by_zero hole_c3:c4:c53_15 :: c3:c4:c5 hole_c6:c74_15 :: c6:c7 hole_c85_15 :: c8 hole_c9:c106_15 :: c9:c10 hole_c11:c12:c13:c147_15 :: c11:c12:c13:c14 hole_false:true8_15 :: false:true gen_c:c1:c29_15 :: Nat -> c:c1:c2 gen_0':s:div_by_zero10_15 :: Nat -> 0':s:div_by_zero gen_c3:c4:c511_15 :: Nat -> c3:c4:c5 Lemmas: GE(gen_0':s:div_by_zero10_15(n13_15), gen_0':s:div_by_zero10_15(n13_15)) -> gen_c:c1:c29_15(n13_15), rt in Omega(1 + n13_15) MINUS(gen_0':s:div_by_zero10_15(n664_15), gen_0':s:div_by_zero10_15(n664_15)) -> gen_c3:c4:c511_15(n664_15), rt in Omega(1 + n664_15) ge(gen_0':s:div_by_zero10_15(n1237_15), gen_0':s:div_by_zero10_15(n1237_15)) -> true, rt in Omega(0) minus(gen_0':s:div_by_zero10_15(n1671_15), gen_0':s:div_by_zero10_15(n1671_15)) -> gen_0':s:div_by_zero10_15(0), rt in Omega(0) Generator Equations: gen_c:c1:c29_15(0) <=> c gen_c:c1:c29_15(+(x, 1)) <=> c2(gen_c:c1:c29_15(x)) gen_0':s:div_by_zero10_15(0) <=> 0' gen_0':s:div_by_zero10_15(+(x, 1)) <=> s(gen_0':s:div_by_zero10_15(x)) gen_c3:c4:c511_15(0) <=> c3 gen_c3:c4:c511_15(+(x, 1)) <=> c5(gen_c3:c4:c511_15(x)) The following defined symbols remain to be analysed: DIV, div