WORST_CASE(Omega(n^1),O(n^2)) proof of input_LIUeIBo1SG.trs # AProVE Commit ID: 5b976082cb74a395683ed8cc7acf94bd611ab29f fuhs 20230524 unpublished The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, n^2). (0) CpxTRS (1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (2) CdtProblem (3) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms] (4) CdtProblem (5) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CdtProblem (7) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CpxRelTRS (9) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (10) CpxWeightedTrs (11) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (12) CpxTypedWeightedTrs (13) CompletionProof [UPPER BOUND(ID), 0 ms] (14) CpxTypedWeightedCompleteTrs (15) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (16) CpxTypedWeightedCompleteTrs (17) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (18) CpxRNTS (19) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms] (20) CpxRNTS (21) CpxRntsAnalysisOrderProof [BOTH BOUNDS(ID, ID), 0 ms] (22) CpxRNTS (23) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (24) CpxRNTS (25) IntTrsBoundProof [UPPER BOUND(ID), 262 ms] (26) CpxRNTS (27) IntTrsBoundProof [UPPER BOUND(ID), 64 ms] (28) CpxRNTS (29) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (30) CpxRNTS (31) IntTrsBoundProof [UPPER BOUND(ID), 281 ms] (32) CpxRNTS (33) IntTrsBoundProof [UPPER BOUND(ID), 54 ms] (34) CpxRNTS (35) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (36) CpxRNTS (37) IntTrsBoundProof [UPPER BOUND(ID), 180 ms] (38) CpxRNTS (39) IntTrsBoundProof [UPPER BOUND(ID), 94 ms] (40) CpxRNTS (41) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (42) CpxRNTS (43) IntTrsBoundProof [UPPER BOUND(ID), 76 ms] (44) CpxRNTS (45) IntTrsBoundProof [UPPER BOUND(ID), 3 ms] (46) CpxRNTS (47) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (48) CpxRNTS (49) IntTrsBoundProof [UPPER BOUND(ID), 368 ms] (50) CpxRNTS (51) IntTrsBoundProof [UPPER BOUND(ID), 23 ms] (52) CpxRNTS (53) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (54) CpxRNTS (55) IntTrsBoundProof [UPPER BOUND(ID), 198 ms] (56) CpxRNTS (57) IntTrsBoundProof [UPPER BOUND(ID), 84 ms] (58) CpxRNTS (59) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (60) CpxRNTS (61) IntTrsBoundProof [UPPER BOUND(ID), 5941 ms] (62) CpxRNTS (63) IntTrsBoundProof [UPPER BOUND(ID), 4261 ms] (64) CpxRNTS (65) FinalProof [FINISHED, 0 ms] (66) BOUNDS(1, n^2) (67) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms] (68) CdtProblem (69) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (70) CpxRelTRS (71) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (72) CpxRelTRS (73) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (74) typed CpxTrs (75) OrderProof [LOWER BOUND(ID), 12 ms] (76) typed CpxTrs (77) RewriteLemmaProof [LOWER BOUND(ID), 308 ms] (78) typed CpxTrs (79) RewriteLemmaProof [LOWER BOUND(ID), 46 ms] (80) typed CpxTrs (81) RewriteLemmaProof [LOWER BOUND(ID), 106 ms] (82) BEST (83) proven lower bound (84) LowerBoundPropagationProof [FINISHED, 0 ms] (85) BOUNDS(n^1, INF) (86) typed CpxTrs (87) RewriteLemmaProof [LOWER BOUND(ID), 62 ms] (88) typed CpxTrs (89) RewriteLemmaProof [LOWER BOUND(ID), 76 ms] (90) typed CpxTrs (91) RewriteLemmaProof [LOWER BOUND(ID), 56 ms] (92) typed CpxTrs ---------------------------------------- (0) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, n^2). The TRS R consists of the following rules: division(x, y) -> div(x, y, 0) div(x, y, z) -> if(lt(x, y), x, y, inc(z)) if(true, x, y, z) -> z if(false, x, s(y), z) -> div(minus(x, s(y)), s(y), z) minus(x, 0) -> x minus(s(x), s(y)) -> minus(x, y) lt(x, 0) -> false lt(0, s(y)) -> true lt(s(x), s(y)) -> lt(x, y) inc(0) -> s(0) inc(s(x)) -> s(inc(x)) S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (1) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (2) Obligation: Complexity Dependency Tuples Problem Rules: division(z0, z1) -> div(z0, z1, 0) div(z0, z1, z2) -> if(lt(z0, z1), z0, z1, inc(z2)) if(true, z0, z1, z2) -> z2 if(false, z0, s(z1), z2) -> div(minus(z0, s(z1)), s(z1), z2) minus(z0, 0) -> z0 minus(s(z0), s(z1)) -> minus(z0, z1) lt(z0, 0) -> false lt(0, s(z0)) -> true lt(s(z0), s(z1)) -> lt(z0, z1) inc(0) -> s(0) inc(s(z0)) -> s(inc(z0)) Tuples: DIVISION(z0, z1) -> c(DIV(z0, z1, 0)) DIV(z0, z1, z2) -> c1(IF(lt(z0, z1), z0, z1, inc(z2)), LT(z0, z1)) DIV(z0, z1, z2) -> c2(IF(lt(z0, z1), z0, z1, inc(z2)), INC(z2)) IF(true, z0, z1, z2) -> c3 IF(false, z0, s(z1), z2) -> c4(DIV(minus(z0, s(z1)), s(z1), z2), MINUS(z0, s(z1))) MINUS(z0, 0) -> c5 MINUS(s(z0), s(z1)) -> c6(MINUS(z0, z1)) LT(z0, 0) -> c7 LT(0, s(z0)) -> c8 LT(s(z0), s(z1)) -> c9(LT(z0, z1)) INC(0) -> c10 INC(s(z0)) -> c11(INC(z0)) S tuples: DIVISION(z0, z1) -> c(DIV(z0, z1, 0)) DIV(z0, z1, z2) -> c1(IF(lt(z0, z1), z0, z1, inc(z2)), LT(z0, z1)) DIV(z0, z1, z2) -> c2(IF(lt(z0, z1), z0, z1, inc(z2)), INC(z2)) IF(true, z0, z1, z2) -> c3 IF(false, z0, s(z1), z2) -> c4(DIV(minus(z0, s(z1)), s(z1), z2), MINUS(z0, s(z1))) MINUS(z0, 0) -> c5 MINUS(s(z0), s(z1)) -> c6(MINUS(z0, z1)) LT(z0, 0) -> c7 LT(0, s(z0)) -> c8 LT(s(z0), s(z1)) -> c9(LT(z0, z1)) INC(0) -> c10 INC(s(z0)) -> c11(INC(z0)) K tuples:none Defined Rule Symbols: division_2, div_3, if_4, minus_2, lt_2, inc_1 Defined Pair Symbols: DIVISION_2, DIV_3, IF_4, MINUS_2, LT_2, INC_1 Compound Symbols: c_1, c1_2, c2_2, c3, c4_2, c5, c6_1, c7, c8, c9_1, c10, c11_1 ---------------------------------------- (3) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 1 leading nodes: DIVISION(z0, z1) -> c(DIV(z0, z1, 0)) Removed 5 trailing nodes: LT(z0, 0) -> c7 MINUS(z0, 0) -> c5 LT(0, s(z0)) -> c8 INC(0) -> c10 IF(true, z0, z1, z2) -> c3 ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: division(z0, z1) -> div(z0, z1, 0) div(z0, z1, z2) -> if(lt(z0, z1), z0, z1, inc(z2)) if(true, z0, z1, z2) -> z2 if(false, z0, s(z1), z2) -> div(minus(z0, s(z1)), s(z1), z2) minus(z0, 0) -> z0 minus(s(z0), s(z1)) -> minus(z0, z1) lt(z0, 0) -> false lt(0, s(z0)) -> true lt(s(z0), s(z1)) -> lt(z0, z1) inc(0) -> s(0) inc(s(z0)) -> s(inc(z0)) Tuples: DIV(z0, z1, z2) -> c1(IF(lt(z0, z1), z0, z1, inc(z2)), LT(z0, z1)) DIV(z0, z1, z2) -> c2(IF(lt(z0, z1), z0, z1, inc(z2)), INC(z2)) IF(false, z0, s(z1), z2) -> c4(DIV(minus(z0, s(z1)), s(z1), z2), MINUS(z0, s(z1))) MINUS(s(z0), s(z1)) -> c6(MINUS(z0, z1)) LT(s(z0), s(z1)) -> c9(LT(z0, z1)) INC(s(z0)) -> c11(INC(z0)) S tuples: DIV(z0, z1, z2) -> c1(IF(lt(z0, z1), z0, z1, inc(z2)), LT(z0, z1)) DIV(z0, z1, z2) -> c2(IF(lt(z0, z1), z0, z1, inc(z2)), INC(z2)) IF(false, z0, s(z1), z2) -> c4(DIV(minus(z0, s(z1)), s(z1), z2), MINUS(z0, s(z1))) MINUS(s(z0), s(z1)) -> c6(MINUS(z0, z1)) LT(s(z0), s(z1)) -> c9(LT(z0, z1)) INC(s(z0)) -> c11(INC(z0)) K tuples:none Defined Rule Symbols: division_2, div_3, if_4, minus_2, lt_2, inc_1 Defined Pair Symbols: DIV_3, IF_4, MINUS_2, LT_2, INC_1 Compound Symbols: c1_2, c2_2, c4_2, c6_1, c9_1, c11_1 ---------------------------------------- (5) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: division(z0, z1) -> div(z0, z1, 0) div(z0, z1, z2) -> if(lt(z0, z1), z0, z1, inc(z2)) if(true, z0, z1, z2) -> z2 if(false, z0, s(z1), z2) -> div(minus(z0, s(z1)), s(z1), z2) ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: lt(z0, 0) -> false lt(0, s(z0)) -> true lt(s(z0), s(z1)) -> lt(z0, z1) inc(0) -> s(0) inc(s(z0)) -> s(inc(z0)) minus(s(z0), s(z1)) -> minus(z0, z1) minus(z0, 0) -> z0 Tuples: DIV(z0, z1, z2) -> c1(IF(lt(z0, z1), z0, z1, inc(z2)), LT(z0, z1)) DIV(z0, z1, z2) -> c2(IF(lt(z0, z1), z0, z1, inc(z2)), INC(z2)) IF(false, z0, s(z1), z2) -> c4(DIV(minus(z0, s(z1)), s(z1), z2), MINUS(z0, s(z1))) MINUS(s(z0), s(z1)) -> c6(MINUS(z0, z1)) LT(s(z0), s(z1)) -> c9(LT(z0, z1)) INC(s(z0)) -> c11(INC(z0)) S tuples: DIV(z0, z1, z2) -> c1(IF(lt(z0, z1), z0, z1, inc(z2)), LT(z0, z1)) DIV(z0, z1, z2) -> c2(IF(lt(z0, z1), z0, z1, inc(z2)), INC(z2)) IF(false, z0, s(z1), z2) -> c4(DIV(minus(z0, s(z1)), s(z1), z2), MINUS(z0, s(z1))) MINUS(s(z0), s(z1)) -> c6(MINUS(z0, z1)) LT(s(z0), s(z1)) -> c9(LT(z0, z1)) INC(s(z0)) -> c11(INC(z0)) K tuples:none Defined Rule Symbols: lt_2, inc_1, minus_2 Defined Pair Symbols: DIV_3, IF_4, MINUS_2, LT_2, INC_1 Compound Symbols: c1_2, c2_2, c4_2, c6_1, c9_1, c11_1 ---------------------------------------- (7) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID)) Converted S to standard rules, and D \ S as well as R to relative rules. ---------------------------------------- (8) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^2). The TRS R consists of the following rules: DIV(z0, z1, z2) -> c1(IF(lt(z0, z1), z0, z1, inc(z2)), LT(z0, z1)) DIV(z0, z1, z2) -> c2(IF(lt(z0, z1), z0, z1, inc(z2)), INC(z2)) IF(false, z0, s(z1), z2) -> c4(DIV(minus(z0, s(z1)), s(z1), z2), MINUS(z0, s(z1))) MINUS(s(z0), s(z1)) -> c6(MINUS(z0, z1)) LT(s(z0), s(z1)) -> c9(LT(z0, z1)) INC(s(z0)) -> c11(INC(z0)) The (relative) TRS S consists of the following rules: lt(z0, 0) -> false lt(0, s(z0)) -> true lt(s(z0), s(z1)) -> lt(z0, z1) inc(0) -> s(0) inc(s(z0)) -> s(inc(z0)) minus(s(z0), s(z1)) -> minus(z0, z1) minus(z0, 0) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (9) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID)) Transformed relative TRS to weighted TRS ---------------------------------------- (10) Obligation: The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^2). The TRS R consists of the following rules: DIV(z0, z1, z2) -> c1(IF(lt(z0, z1), z0, z1, inc(z2)), LT(z0, z1)) [1] DIV(z0, z1, z2) -> c2(IF(lt(z0, z1), z0, z1, inc(z2)), INC(z2)) [1] IF(false, z0, s(z1), z2) -> c4(DIV(minus(z0, s(z1)), s(z1), z2), MINUS(z0, s(z1))) [1] MINUS(s(z0), s(z1)) -> c6(MINUS(z0, z1)) [1] LT(s(z0), s(z1)) -> c9(LT(z0, z1)) [1] INC(s(z0)) -> c11(INC(z0)) [1] lt(z0, 0) -> false [0] lt(0, s(z0)) -> true [0] lt(s(z0), s(z1)) -> lt(z0, z1) [0] inc(0) -> s(0) [0] inc(s(z0)) -> s(inc(z0)) [0] minus(s(z0), s(z1)) -> minus(z0, z1) [0] minus(z0, 0) -> z0 [0] Rewrite Strategy: INNERMOST ---------------------------------------- (11) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (12) Obligation: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: DIV(z0, z1, z2) -> c1(IF(lt(z0, z1), z0, z1, inc(z2)), LT(z0, z1)) [1] DIV(z0, z1, z2) -> c2(IF(lt(z0, z1), z0, z1, inc(z2)), INC(z2)) [1] IF(false, z0, s(z1), z2) -> c4(DIV(minus(z0, s(z1)), s(z1), z2), MINUS(z0, s(z1))) [1] MINUS(s(z0), s(z1)) -> c6(MINUS(z0, z1)) [1] LT(s(z0), s(z1)) -> c9(LT(z0, z1)) [1] INC(s(z0)) -> c11(INC(z0)) [1] lt(z0, 0) -> false [0] lt(0, s(z0)) -> true [0] lt(s(z0), s(z1)) -> lt(z0, z1) [0] inc(0) -> s(0) [0] inc(s(z0)) -> s(inc(z0)) [0] minus(s(z0), s(z1)) -> minus(z0, z1) [0] minus(z0, 0) -> z0 [0] The TRS has the following type information: DIV :: s:0 -> s:0 -> s:0 -> c1:c2 c1 :: c4 -> c9 -> c1:c2 IF :: false:true -> s:0 -> s:0 -> s:0 -> c4 lt :: s:0 -> s:0 -> false:true inc :: s:0 -> s:0 LT :: s:0 -> s:0 -> c9 c2 :: c4 -> c11 -> c1:c2 INC :: s:0 -> c11 false :: false:true s :: s:0 -> s:0 c4 :: c1:c2 -> c6 -> c4 minus :: s:0 -> s:0 -> s:0 MINUS :: s:0 -> s:0 -> c6 c6 :: c6 -> c6 c9 :: c9 -> c9 c11 :: c11 -> c11 0 :: s:0 true :: false:true Rewrite Strategy: INNERMOST ---------------------------------------- (13) CompletionProof (UPPER BOUND(ID)) The transformation into a RNTS is sound, since: (a) The obligation is a constructor system where every type has a constant constructor, (b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols: DIV_3 IF_4 MINUS_2 LT_2 INC_1 (c) The following functions are completely defined: lt_2 inc_1 minus_2 Due to the following rules being added: lt(v0, v1) -> null_lt [0] inc(v0) -> 0 [0] minus(v0, v1) -> 0 [0] And the following fresh constants: null_lt, const, const1, const2, const3, const4 ---------------------------------------- (14) Obligation: Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: DIV(z0, z1, z2) -> c1(IF(lt(z0, z1), z0, z1, inc(z2)), LT(z0, z1)) [1] DIV(z0, z1, z2) -> c2(IF(lt(z0, z1), z0, z1, inc(z2)), INC(z2)) [1] IF(false, z0, s(z1), z2) -> c4(DIV(minus(z0, s(z1)), s(z1), z2), MINUS(z0, s(z1))) [1] MINUS(s(z0), s(z1)) -> c6(MINUS(z0, z1)) [1] LT(s(z0), s(z1)) -> c9(LT(z0, z1)) [1] INC(s(z0)) -> c11(INC(z0)) [1] lt(z0, 0) -> false [0] lt(0, s(z0)) -> true [0] lt(s(z0), s(z1)) -> lt(z0, z1) [0] inc(0) -> s(0) [0] inc(s(z0)) -> s(inc(z0)) [0] minus(s(z0), s(z1)) -> minus(z0, z1) [0] minus(z0, 0) -> z0 [0] lt(v0, v1) -> null_lt [0] inc(v0) -> 0 [0] minus(v0, v1) -> 0 [0] The TRS has the following type information: DIV :: s:0 -> s:0 -> s:0 -> c1:c2 c1 :: c4 -> c9 -> c1:c2 IF :: false:true:null_lt -> s:0 -> s:0 -> s:0 -> c4 lt :: s:0 -> s:0 -> false:true:null_lt inc :: s:0 -> s:0 LT :: s:0 -> s:0 -> c9 c2 :: c4 -> c11 -> c1:c2 INC :: s:0 -> c11 false :: false:true:null_lt s :: s:0 -> s:0 c4 :: c1:c2 -> c6 -> c4 minus :: s:0 -> s:0 -> s:0 MINUS :: s:0 -> s:0 -> c6 c6 :: c6 -> c6 c9 :: c9 -> c9 c11 :: c11 -> c11 0 :: s:0 true :: false:true:null_lt null_lt :: false:true:null_lt const :: c1:c2 const1 :: c4 const2 :: c9 const3 :: c11 const4 :: c6 Rewrite Strategy: INNERMOST ---------------------------------------- (15) NarrowingProof (BOTH BOUNDS(ID, ID)) Narrowed the inner basic terms of all right-hand sides by a single narrowing step. ---------------------------------------- (16) Obligation: Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: DIV(z0, 0, 0) -> c1(IF(false, z0, 0, s(0)), LT(z0, 0)) [1] DIV(z0, 0, s(z01)) -> c1(IF(false, z0, 0, s(inc(z01))), LT(z0, 0)) [1] DIV(z0, 0, z2) -> c1(IF(false, z0, 0, 0), LT(z0, 0)) [1] DIV(0, s(z0'), 0) -> c1(IF(true, 0, s(z0'), s(0)), LT(0, s(z0'))) [1] DIV(0, s(z0'), s(z02)) -> c1(IF(true, 0, s(z0'), s(inc(z02))), LT(0, s(z0'))) [1] DIV(0, s(z0'), z2) -> c1(IF(true, 0, s(z0'), 0), LT(0, s(z0'))) [1] DIV(s(z0''), s(z1'), 0) -> c1(IF(lt(z0'', z1'), s(z0''), s(z1'), s(0)), LT(s(z0''), s(z1'))) [1] DIV(s(z0''), s(z1'), s(z03)) -> c1(IF(lt(z0'', z1'), s(z0''), s(z1'), s(inc(z03))), LT(s(z0''), s(z1'))) [1] DIV(s(z0''), s(z1'), z2) -> c1(IF(lt(z0'', z1'), s(z0''), s(z1'), 0), LT(s(z0''), s(z1'))) [1] DIV(z0, z1, 0) -> c1(IF(null_lt, z0, z1, s(0)), LT(z0, z1)) [1] DIV(z0, z1, s(z04)) -> c1(IF(null_lt, z0, z1, s(inc(z04))), LT(z0, z1)) [1] DIV(z0, z1, z2) -> c1(IF(null_lt, z0, z1, 0), LT(z0, z1)) [1] DIV(z0, 0, 0) -> c2(IF(false, z0, 0, s(0)), INC(0)) [1] DIV(z0, 0, s(z07)) -> c2(IF(false, z0, 0, s(inc(z07))), INC(s(z07))) [1] DIV(z0, 0, z2) -> c2(IF(false, z0, 0, 0), INC(z2)) [1] DIV(0, s(z05), 0) -> c2(IF(true, 0, s(z05), s(0)), INC(0)) [1] DIV(0, s(z05), s(z08)) -> c2(IF(true, 0, s(z05), s(inc(z08))), INC(s(z08))) [1] DIV(0, s(z05), z2) -> c2(IF(true, 0, s(z05), 0), INC(z2)) [1] DIV(s(z06), s(z1''), 0) -> c2(IF(lt(z06, z1''), s(z06), s(z1''), s(0)), INC(0)) [1] DIV(s(z06), s(z1''), s(z09)) -> c2(IF(lt(z06, z1''), s(z06), s(z1''), s(inc(z09))), INC(s(z09))) [1] DIV(s(z06), s(z1''), z2) -> c2(IF(lt(z06, z1''), s(z06), s(z1''), 0), INC(z2)) [1] DIV(z0, z1, 0) -> c2(IF(null_lt, z0, z1, s(0)), INC(0)) [1] DIV(z0, z1, s(z010)) -> c2(IF(null_lt, z0, z1, s(inc(z010))), INC(s(z010))) [1] DIV(z0, z1, z2) -> c2(IF(null_lt, z0, z1, 0), INC(z2)) [1] IF(false, s(z011), s(z1), z2) -> c4(DIV(minus(z011, z1), s(z1), z2), MINUS(s(z011), s(z1))) [1] IF(false, z0, s(z1), z2) -> c4(DIV(0, s(z1), z2), MINUS(z0, s(z1))) [1] MINUS(s(z0), s(z1)) -> c6(MINUS(z0, z1)) [1] LT(s(z0), s(z1)) -> c9(LT(z0, z1)) [1] INC(s(z0)) -> c11(INC(z0)) [1] lt(z0, 0) -> false [0] lt(0, s(z0)) -> true [0] lt(s(z0), s(z1)) -> lt(z0, z1) [0] inc(0) -> s(0) [0] inc(s(z0)) -> s(inc(z0)) [0] minus(s(z0), s(z1)) -> minus(z0, z1) [0] minus(z0, 0) -> z0 [0] lt(v0, v1) -> null_lt [0] inc(v0) -> 0 [0] minus(v0, v1) -> 0 [0] The TRS has the following type information: DIV :: s:0 -> s:0 -> s:0 -> c1:c2 c1 :: c4 -> c9 -> c1:c2 IF :: false:true:null_lt -> s:0 -> s:0 -> s:0 -> c4 lt :: s:0 -> s:0 -> false:true:null_lt inc :: s:0 -> s:0 LT :: s:0 -> s:0 -> c9 c2 :: c4 -> c11 -> c1:c2 INC :: s:0 -> c11 false :: false:true:null_lt s :: s:0 -> s:0 c4 :: c1:c2 -> c6 -> c4 minus :: s:0 -> s:0 -> s:0 MINUS :: s:0 -> s:0 -> c6 c6 :: c6 -> c6 c9 :: c9 -> c9 c11 :: c11 -> c11 0 :: s:0 true :: false:true:null_lt null_lt :: false:true:null_lt const :: c1:c2 const1 :: c4 const2 :: c9 const3 :: c11 const4 :: c6 Rewrite Strategy: INNERMOST ---------------------------------------- (17) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: false => 1 0 => 0 true => 2 null_lt => 0 const => 0 const1 => 0 const2 => 0 const3 => 0 const4 => 0 ---------------------------------------- (18) Obligation: Complexity RNTS consisting of the following rules: DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z0'', z1'), 1 + z0'', 1 + z1', 0) + LT(1 + z0'', 1 + z1') :|: z'' = z2, z' = 1 + z1', z1' >= 0, z0'' >= 0, z2 >= 0, z = 1 + z0'' DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z0'', z1'), 1 + z0'', 1 + z1', 1 + inc(z03)) + LT(1 + z0'', 1 + z1') :|: z'' = 1 + z03, z' = 1 + z1', z1' >= 0, z0'' >= 0, z03 >= 0, z = 1 + z0'' DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z0'', z1'), 1 + z0'', 1 + z1', 1 + 0) + LT(1 + z0'', 1 + z1') :|: z'' = 0, z' = 1 + z1', z1' >= 0, z0'' >= 0, z = 1 + z0'' DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z06, z1''), 1 + z06, 1 + z1'', 0) + INC(z2) :|: z'' = z2, z' = 1 + z1'', z06 >= 0, z2 >= 0, z = 1 + z06, z1'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z06, z1''), 1 + z06, 1 + z1'', 1 + inc(z09)) + INC(1 + z09) :|: z' = 1 + z1'', z'' = 1 + z09, z06 >= 0, z09 >= 0, z = 1 + z06, z1'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z06, z1''), 1 + z06, 1 + z1'', 1 + 0) + INC(0) :|: z'' = 0, z' = 1 + z1'', z06 >= 0, z = 1 + z06, z1'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + z0', 0) + LT(0, 1 + z0') :|: z'' = z2, z0' >= 0, z = 0, z' = 1 + z0', z2 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + z0', 1 + inc(z02)) + LT(0, 1 + z0') :|: z0' >= 0, z02 >= 0, z = 0, z' = 1 + z0', z'' = 1 + z02 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + z0', 1 + 0) + LT(0, 1 + z0') :|: z'' = 0, z0' >= 0, z = 0, z' = 1 + z0' DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + z05, 0) + INC(z2) :|: z'' = z2, z05 >= 0, z = 0, z' = 1 + z05, z2 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + z05, 1 + inc(z08)) + INC(1 + z08) :|: z08 >= 0, z'' = 1 + z08, z05 >= 0, z = 0, z' = 1 + z05 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + z05, 1 + 0) + INC(0) :|: z'' = 0, z05 >= 0, z = 0, z' = 1 + z05 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z0, 0, 0) + LT(z0, 0) :|: z'' = z2, z = z0, z0 >= 0, z2 >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z0, 0, 0) + INC(z2) :|: z'' = z2, z = z0, z0 >= 0, z2 >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z0, 0, 1 + inc(z01)) + LT(z0, 0) :|: z = z0, z01 >= 0, z0 >= 0, z' = 0, z'' = 1 + z01 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z0, 0, 1 + inc(z07)) + INC(1 + z07) :|: z = z0, z07 >= 0, z'' = 1 + z07, z0 >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z0, 0, 1 + 0) + LT(z0, 0) :|: z'' = 0, z = z0, z0 >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z0, 0, 1 + 0) + INC(0) :|: z'' = 0, z = z0, z0 >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z0, z1, 0) + LT(z0, z1) :|: z'' = z2, z = z0, z1 >= 0, z' = z1, z0 >= 0, z2 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z0, z1, 0) + INC(z2) :|: z'' = z2, z = z0, z1 >= 0, z' = z1, z0 >= 0, z2 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z0, z1, 1 + inc(z010)) + INC(1 + z010) :|: z = z0, z1 >= 0, z'' = 1 + z010, z' = z1, z0 >= 0, z010 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z0, z1, 1 + inc(z04)) + LT(z0, z1) :|: z'' = 1 + z04, z04 >= 0, z = z0, z1 >= 0, z' = z1, z0 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z0, z1, 1 + 0) + LT(z0, z1) :|: z'' = 0, z = z0, z1 >= 0, z' = z1, z0 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z0, z1, 1 + 0) + INC(0) :|: z'' = 0, z = z0, z1 >= 0, z' = z1, z0 >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(minus(z011, z1), 1 + z1, z2) + MINUS(1 + z011, 1 + z1) :|: z011 >= 0, z1 >= 0, z = 1, z' = 1 + z011, z'' = 1 + z1, z3 = z2, z2 >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(0, 1 + z1, z2) + MINUS(z0, 1 + z1) :|: z1 >= 0, z = 1, z0 >= 0, z'' = 1 + z1, z3 = z2, z' = z0, z2 >= 0 INC(z) -{ 1 }-> 1 + INC(z0) :|: z = 1 + z0, z0 >= 0 LT(z, z') -{ 1 }-> 1 + LT(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1 MINUS(z, z') -{ 1 }-> 1 + MINUS(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1 inc(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 inc(z) -{ 0 }-> 1 + inc(z0) :|: z = 1 + z0, z0 >= 0 inc(z) -{ 0 }-> 1 + 0 :|: z = 0 lt(z, z') -{ 0 }-> lt(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1 lt(z, z') -{ 0 }-> 2 :|: z0 >= 0, z' = 1 + z0, z = 0 lt(z, z') -{ 0 }-> 1 :|: z = z0, z0 >= 0, z' = 0 lt(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 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 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 ---------------------------------------- (19) SimplificationProof (BOTH BOUNDS(ID, ID)) Simplified the RNTS by moving equalities from the constraints into the right-hand sides. ---------------------------------------- (20) Obligation: Complexity RNTS consisting of the following rules: DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + LT(1 + (z - 1), 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + INC(z'') :|: z - 1 >= 0, z'' >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + inc(z'' - 1)) + LT(1 + (z - 1), 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z - 1 >= 0, z'' - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + LT(1 + (z - 1), 1 + (z' - 1)) :|: z'' = 0, z' - 1 >= 0, z - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + INC(0) :|: z'' = 0, z - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + LT(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + INC(z'') :|: z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + inc(z'' - 1)) + LT(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z'' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z'' - 1 >= 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + LT(0, 1 + (z' - 1)) :|: z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + INC(0) :|: z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + LT(z, 0) :|: z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + INC(z'') :|: z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + inc(z'' - 1)) + LT(z, 0) :|: z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + LT(z, 0) :|: z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + INC(0) :|: z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 0) + LT(z, z') :|: z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 0) + INC(z'') :|: z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + inc(z'' - 1)) + LT(z, z') :|: z'' - 1 >= 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z' >= 0, z >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + LT(z, z') :|: z'' = 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + INC(0) :|: z'' = 0, z' >= 0, z >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(minus(z' - 1, z'' - 1), 1 + (z'' - 1), z3) + MINUS(1 + (z' - 1), 1 + (z'' - 1)) :|: z' - 1 >= 0, z'' - 1 >= 0, z = 1, z3 >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(0, 1 + (z'' - 1), z3) + MINUS(z', 1 + (z'' - 1)) :|: z'' - 1 >= 0, z = 1, z' >= 0, z3 >= 0 INC(z) -{ 1 }-> 1 + INC(z - 1) :|: z - 1 >= 0 LT(z, z') -{ 1 }-> 1 + LT(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 MINUS(z, z') -{ 1 }-> 1 + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 inc(z) -{ 0 }-> 0 :|: z >= 0 inc(z) -{ 0 }-> 1 + inc(z - 1) :|: z - 1 >= 0 inc(z) -{ 0 }-> 1 + 0 :|: z = 0 lt(z, z') -{ 0 }-> lt(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 lt(z, z') -{ 0 }-> 2 :|: z' - 1 >= 0, z = 0 lt(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0 lt(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 minus(z, z') -{ 0 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 ---------------------------------------- (21) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID)) Found the following analysis order by SCC decomposition: { minus } { inc } { LT } { INC } { lt } { MINUS } { IF, DIV } ---------------------------------------- (22) Obligation: Complexity RNTS consisting of the following rules: DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + LT(1 + (z - 1), 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + INC(z'') :|: z - 1 >= 0, z'' >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + inc(z'' - 1)) + LT(1 + (z - 1), 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z - 1 >= 0, z'' - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + LT(1 + (z - 1), 1 + (z' - 1)) :|: z'' = 0, z' - 1 >= 0, z - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + INC(0) :|: z'' = 0, z - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + LT(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + INC(z'') :|: z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + inc(z'' - 1)) + LT(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z'' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z'' - 1 >= 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + LT(0, 1 + (z' - 1)) :|: z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + INC(0) :|: z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + LT(z, 0) :|: z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + INC(z'') :|: z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + inc(z'' - 1)) + LT(z, 0) :|: z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + LT(z, 0) :|: z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + INC(0) :|: z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 0) + LT(z, z') :|: z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 0) + INC(z'') :|: z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + inc(z'' - 1)) + LT(z, z') :|: z'' - 1 >= 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z' >= 0, z >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + LT(z, z') :|: z'' = 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + INC(0) :|: z'' = 0, z' >= 0, z >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(minus(z' - 1, z'' - 1), 1 + (z'' - 1), z3) + MINUS(1 + (z' - 1), 1 + (z'' - 1)) :|: z' - 1 >= 0, z'' - 1 >= 0, z = 1, z3 >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(0, 1 + (z'' - 1), z3) + MINUS(z', 1 + (z'' - 1)) :|: z'' - 1 >= 0, z = 1, z' >= 0, z3 >= 0 INC(z) -{ 1 }-> 1 + INC(z - 1) :|: z - 1 >= 0 LT(z, z') -{ 1 }-> 1 + LT(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 MINUS(z, z') -{ 1 }-> 1 + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 inc(z) -{ 0 }-> 0 :|: z >= 0 inc(z) -{ 0 }-> 1 + inc(z - 1) :|: z - 1 >= 0 inc(z) -{ 0 }-> 1 + 0 :|: z = 0 lt(z, z') -{ 0 }-> lt(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 lt(z, z') -{ 0 }-> 2 :|: z' - 1 >= 0, z = 0 lt(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0 lt(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 minus(z, z') -{ 0 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 Function symbols to be analyzed: {minus}, {inc}, {LT}, {INC}, {lt}, {MINUS}, {IF,DIV} ---------------------------------------- (23) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (24) Obligation: Complexity RNTS consisting of the following rules: DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + LT(1 + (z - 1), 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + INC(z'') :|: z - 1 >= 0, z'' >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + inc(z'' - 1)) + LT(1 + (z - 1), 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z - 1 >= 0, z'' - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + LT(1 + (z - 1), 1 + (z' - 1)) :|: z'' = 0, z' - 1 >= 0, z - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + INC(0) :|: z'' = 0, z - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + LT(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + INC(z'') :|: z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + inc(z'' - 1)) + LT(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z'' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z'' - 1 >= 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + LT(0, 1 + (z' - 1)) :|: z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + INC(0) :|: z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + LT(z, 0) :|: z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + INC(z'') :|: z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + inc(z'' - 1)) + LT(z, 0) :|: z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + LT(z, 0) :|: z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + INC(0) :|: z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 0) + LT(z, z') :|: z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 0) + INC(z'') :|: z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + inc(z'' - 1)) + LT(z, z') :|: z'' - 1 >= 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z' >= 0, z >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + LT(z, z') :|: z'' = 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + INC(0) :|: z'' = 0, z' >= 0, z >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(minus(z' - 1, z'' - 1), 1 + (z'' - 1), z3) + MINUS(1 + (z' - 1), 1 + (z'' - 1)) :|: z' - 1 >= 0, z'' - 1 >= 0, z = 1, z3 >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(0, 1 + (z'' - 1), z3) + MINUS(z', 1 + (z'' - 1)) :|: z'' - 1 >= 0, z = 1, z' >= 0, z3 >= 0 INC(z) -{ 1 }-> 1 + INC(z - 1) :|: z - 1 >= 0 LT(z, z') -{ 1 }-> 1 + LT(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 MINUS(z, z') -{ 1 }-> 1 + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 inc(z) -{ 0 }-> 0 :|: z >= 0 inc(z) -{ 0 }-> 1 + inc(z - 1) :|: z - 1 >= 0 inc(z) -{ 0 }-> 1 + 0 :|: z = 0 lt(z, z') -{ 0 }-> lt(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 lt(z, z') -{ 0 }-> 2 :|: z' - 1 >= 0, z = 0 lt(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0 lt(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 minus(z, z') -{ 0 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 Function symbols to be analyzed: {minus}, {inc}, {LT}, {INC}, {lt}, {MINUS}, {IF,DIV} ---------------------------------------- (25) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using KoAT for: minus after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: z ---------------------------------------- (26) Obligation: Complexity RNTS consisting of the following rules: DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + LT(1 + (z - 1), 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + INC(z'') :|: z - 1 >= 0, z'' >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + inc(z'' - 1)) + LT(1 + (z - 1), 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z - 1 >= 0, z'' - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + LT(1 + (z - 1), 1 + (z' - 1)) :|: z'' = 0, z' - 1 >= 0, z - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + INC(0) :|: z'' = 0, z - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + LT(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + INC(z'') :|: z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + inc(z'' - 1)) + LT(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z'' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z'' - 1 >= 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + LT(0, 1 + (z' - 1)) :|: z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + INC(0) :|: z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + LT(z, 0) :|: z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + INC(z'') :|: z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + inc(z'' - 1)) + LT(z, 0) :|: z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + LT(z, 0) :|: z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + INC(0) :|: z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 0) + LT(z, z') :|: z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 0) + INC(z'') :|: z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + inc(z'' - 1)) + LT(z, z') :|: z'' - 1 >= 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z' >= 0, z >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + LT(z, z') :|: z'' = 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + INC(0) :|: z'' = 0, z' >= 0, z >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(minus(z' - 1, z'' - 1), 1 + (z'' - 1), z3) + MINUS(1 + (z' - 1), 1 + (z'' - 1)) :|: z' - 1 >= 0, z'' - 1 >= 0, z = 1, z3 >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(0, 1 + (z'' - 1), z3) + MINUS(z', 1 + (z'' - 1)) :|: z'' - 1 >= 0, z = 1, z' >= 0, z3 >= 0 INC(z) -{ 1 }-> 1 + INC(z - 1) :|: z - 1 >= 0 LT(z, z') -{ 1 }-> 1 + LT(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 MINUS(z, z') -{ 1 }-> 1 + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 inc(z) -{ 0 }-> 0 :|: z >= 0 inc(z) -{ 0 }-> 1 + inc(z - 1) :|: z - 1 >= 0 inc(z) -{ 0 }-> 1 + 0 :|: z = 0 lt(z, z') -{ 0 }-> lt(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 lt(z, z') -{ 0 }-> 2 :|: z' - 1 >= 0, z = 0 lt(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0 lt(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 minus(z, z') -{ 0 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 Function symbols to be analyzed: {minus}, {inc}, {LT}, {INC}, {lt}, {MINUS}, {IF,DIV} Previous analysis results are: minus: runtime: ?, size: O(n^1) [z] ---------------------------------------- (27) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: minus after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 0 ---------------------------------------- (28) Obligation: Complexity RNTS consisting of the following rules: DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + LT(1 + (z - 1), 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + INC(z'') :|: z - 1 >= 0, z'' >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + inc(z'' - 1)) + LT(1 + (z - 1), 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z - 1 >= 0, z'' - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + LT(1 + (z - 1), 1 + (z' - 1)) :|: z'' = 0, z' - 1 >= 0, z - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + INC(0) :|: z'' = 0, z - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + LT(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + INC(z'') :|: z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + inc(z'' - 1)) + LT(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z'' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z'' - 1 >= 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + LT(0, 1 + (z' - 1)) :|: z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + INC(0) :|: z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + LT(z, 0) :|: z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + INC(z'') :|: z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + inc(z'' - 1)) + LT(z, 0) :|: z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + LT(z, 0) :|: z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + INC(0) :|: z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 0) + LT(z, z') :|: z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 0) + INC(z'') :|: z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + inc(z'' - 1)) + LT(z, z') :|: z'' - 1 >= 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z' >= 0, z >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + LT(z, z') :|: z'' = 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + INC(0) :|: z'' = 0, z' >= 0, z >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(minus(z' - 1, z'' - 1), 1 + (z'' - 1), z3) + MINUS(1 + (z' - 1), 1 + (z'' - 1)) :|: z' - 1 >= 0, z'' - 1 >= 0, z = 1, z3 >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(0, 1 + (z'' - 1), z3) + MINUS(z', 1 + (z'' - 1)) :|: z'' - 1 >= 0, z = 1, z' >= 0, z3 >= 0 INC(z) -{ 1 }-> 1 + INC(z - 1) :|: z - 1 >= 0 LT(z, z') -{ 1 }-> 1 + LT(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 MINUS(z, z') -{ 1 }-> 1 + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 inc(z) -{ 0 }-> 0 :|: z >= 0 inc(z) -{ 0 }-> 1 + inc(z - 1) :|: z - 1 >= 0 inc(z) -{ 0 }-> 1 + 0 :|: z = 0 lt(z, z') -{ 0 }-> lt(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 lt(z, z') -{ 0 }-> 2 :|: z' - 1 >= 0, z = 0 lt(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0 lt(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 minus(z, z') -{ 0 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 Function symbols to be analyzed: {inc}, {LT}, {INC}, {lt}, {MINUS}, {IF,DIV} Previous analysis results are: minus: runtime: O(1) [0], size: O(n^1) [z] ---------------------------------------- (29) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (30) Obligation: Complexity RNTS consisting of the following rules: DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + LT(1 + (z - 1), 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + INC(z'') :|: z - 1 >= 0, z'' >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + inc(z'' - 1)) + LT(1 + (z - 1), 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z - 1 >= 0, z'' - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + LT(1 + (z - 1), 1 + (z' - 1)) :|: z'' = 0, z' - 1 >= 0, z - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + INC(0) :|: z'' = 0, z - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + LT(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + INC(z'') :|: z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + inc(z'' - 1)) + LT(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z'' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z'' - 1 >= 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + LT(0, 1 + (z' - 1)) :|: z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + INC(0) :|: z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + LT(z, 0) :|: z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + INC(z'') :|: z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + inc(z'' - 1)) + LT(z, 0) :|: z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + LT(z, 0) :|: z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + INC(0) :|: z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 0) + LT(z, z') :|: z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 0) + INC(z'') :|: z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + inc(z'' - 1)) + LT(z, z') :|: z'' - 1 >= 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z' >= 0, z >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + LT(z, z') :|: z'' = 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + INC(0) :|: z'' = 0, z' >= 0, z >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(s, 1 + (z'' - 1), z3) + MINUS(1 + (z' - 1), 1 + (z'' - 1)) :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z'' - 1 >= 0, z = 1, z3 >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(0, 1 + (z'' - 1), z3) + MINUS(z', 1 + (z'' - 1)) :|: z'' - 1 >= 0, z = 1, z' >= 0, z3 >= 0 INC(z) -{ 1 }-> 1 + INC(z - 1) :|: z - 1 >= 0 LT(z, z') -{ 1 }-> 1 + LT(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 MINUS(z, z') -{ 1 }-> 1 + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 inc(z) -{ 0 }-> 0 :|: z >= 0 inc(z) -{ 0 }-> 1 + inc(z - 1) :|: z - 1 >= 0 inc(z) -{ 0 }-> 1 + 0 :|: z = 0 lt(z, z') -{ 0 }-> lt(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 lt(z, z') -{ 0 }-> 2 :|: z' - 1 >= 0, z = 0 lt(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0 lt(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 minus(z, z') -{ 0 }-> s' :|: s' >= 0, s' <= z - 1, z' - 1 >= 0, z - 1 >= 0 minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 Function symbols to be analyzed: {inc}, {LT}, {INC}, {lt}, {MINUS}, {IF,DIV} Previous analysis results are: minus: runtime: O(1) [0], size: O(n^1) [z] ---------------------------------------- (31) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: inc after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: 1 + z ---------------------------------------- (32) Obligation: Complexity RNTS consisting of the following rules: DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + LT(1 + (z - 1), 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + INC(z'') :|: z - 1 >= 0, z'' >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + inc(z'' - 1)) + LT(1 + (z - 1), 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z - 1 >= 0, z'' - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + LT(1 + (z - 1), 1 + (z' - 1)) :|: z'' = 0, z' - 1 >= 0, z - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + INC(0) :|: z'' = 0, z - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + LT(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + INC(z'') :|: z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + inc(z'' - 1)) + LT(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z'' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z'' - 1 >= 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + LT(0, 1 + (z' - 1)) :|: z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + INC(0) :|: z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + LT(z, 0) :|: z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + INC(z'') :|: z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + inc(z'' - 1)) + LT(z, 0) :|: z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + LT(z, 0) :|: z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + INC(0) :|: z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 0) + LT(z, z') :|: z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 0) + INC(z'') :|: z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + inc(z'' - 1)) + LT(z, z') :|: z'' - 1 >= 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z' >= 0, z >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + LT(z, z') :|: z'' = 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + INC(0) :|: z'' = 0, z' >= 0, z >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(s, 1 + (z'' - 1), z3) + MINUS(1 + (z' - 1), 1 + (z'' - 1)) :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z'' - 1 >= 0, z = 1, z3 >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(0, 1 + (z'' - 1), z3) + MINUS(z', 1 + (z'' - 1)) :|: z'' - 1 >= 0, z = 1, z' >= 0, z3 >= 0 INC(z) -{ 1 }-> 1 + INC(z - 1) :|: z - 1 >= 0 LT(z, z') -{ 1 }-> 1 + LT(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 MINUS(z, z') -{ 1 }-> 1 + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 inc(z) -{ 0 }-> 0 :|: z >= 0 inc(z) -{ 0 }-> 1 + inc(z - 1) :|: z - 1 >= 0 inc(z) -{ 0 }-> 1 + 0 :|: z = 0 lt(z, z') -{ 0 }-> lt(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 lt(z, z') -{ 0 }-> 2 :|: z' - 1 >= 0, z = 0 lt(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0 lt(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 minus(z, z') -{ 0 }-> s' :|: s' >= 0, s' <= z - 1, z' - 1 >= 0, z - 1 >= 0 minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 Function symbols to be analyzed: {inc}, {LT}, {INC}, {lt}, {MINUS}, {IF,DIV} Previous analysis results are: minus: runtime: O(1) [0], size: O(n^1) [z] inc: runtime: ?, size: O(n^1) [1 + z] ---------------------------------------- (33) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: inc after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 0 ---------------------------------------- (34) Obligation: Complexity RNTS consisting of the following rules: DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + LT(1 + (z - 1), 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + INC(z'') :|: z - 1 >= 0, z'' >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + inc(z'' - 1)) + LT(1 + (z - 1), 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z - 1 >= 0, z'' - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + LT(1 + (z - 1), 1 + (z' - 1)) :|: z'' = 0, z' - 1 >= 0, z - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + INC(0) :|: z'' = 0, z - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + LT(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + INC(z'') :|: z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + inc(z'' - 1)) + LT(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z'' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z'' - 1 >= 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + LT(0, 1 + (z' - 1)) :|: z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + INC(0) :|: z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + LT(z, 0) :|: z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + INC(z'') :|: z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + inc(z'' - 1)) + LT(z, 0) :|: z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + LT(z, 0) :|: z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + INC(0) :|: z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 0) + LT(z, z') :|: z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 0) + INC(z'') :|: z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + inc(z'' - 1)) + LT(z, z') :|: z'' - 1 >= 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + inc(z'' - 1)) + INC(1 + (z'' - 1)) :|: z' >= 0, z >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + LT(z, z') :|: z'' = 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + INC(0) :|: z'' = 0, z' >= 0, z >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(s, 1 + (z'' - 1), z3) + MINUS(1 + (z' - 1), 1 + (z'' - 1)) :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z'' - 1 >= 0, z = 1, z3 >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(0, 1 + (z'' - 1), z3) + MINUS(z', 1 + (z'' - 1)) :|: z'' - 1 >= 0, z = 1, z' >= 0, z3 >= 0 INC(z) -{ 1 }-> 1 + INC(z - 1) :|: z - 1 >= 0 LT(z, z') -{ 1 }-> 1 + LT(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 MINUS(z, z') -{ 1 }-> 1 + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 inc(z) -{ 0 }-> 0 :|: z >= 0 inc(z) -{ 0 }-> 1 + inc(z - 1) :|: z - 1 >= 0 inc(z) -{ 0 }-> 1 + 0 :|: z = 0 lt(z, z') -{ 0 }-> lt(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 lt(z, z') -{ 0 }-> 2 :|: z' - 1 >= 0, z = 0 lt(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0 lt(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 minus(z, z') -{ 0 }-> s' :|: s' >= 0, s' <= z - 1, z' - 1 >= 0, z - 1 >= 0 minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 Function symbols to be analyzed: {LT}, {INC}, {lt}, {MINUS}, {IF,DIV} Previous analysis results are: minus: runtime: O(1) [0], size: O(n^1) [z] inc: runtime: O(1) [0], size: O(n^1) [1 + z] ---------------------------------------- (35) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (36) Obligation: Complexity RNTS consisting of the following rules: DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + LT(1 + (z - 1), 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + INC(z'') :|: z - 1 >= 0, z'' >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + s2) + LT(1 + (z - 1), 1 + (z' - 1)) :|: s2 >= 0, s2 <= z'' - 1 + 1, z' - 1 >= 0, z - 1 >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + s6) + INC(1 + (z'' - 1)) :|: s6 >= 0, s6 <= z'' - 1 + 1, z - 1 >= 0, z'' - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + LT(1 + (z - 1), 1 + (z' - 1)) :|: z'' = 0, z' - 1 >= 0, z - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + INC(0) :|: z'' = 0, z - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + LT(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + INC(z'') :|: z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + s1) + LT(0, 1 + (z' - 1)) :|: s1 >= 0, s1 <= z'' - 1 + 1, z' - 1 >= 0, z'' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + s5) + INC(1 + (z'' - 1)) :|: s5 >= 0, s5 <= z'' - 1 + 1, z'' - 1 >= 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + LT(0, 1 + (z' - 1)) :|: z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + INC(0) :|: z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + LT(z, 0) :|: z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + INC(z'') :|: z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + s'') + LT(z, 0) :|: s'' >= 0, s'' <= z'' - 1 + 1, z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + s4) + INC(1 + (z'' - 1)) :|: s4 >= 0, s4 <= z'' - 1 + 1, z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + LT(z, 0) :|: z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + INC(0) :|: z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 0) + LT(z, z') :|: z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 0) + INC(z'') :|: z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + s3) + LT(z, z') :|: s3 >= 0, s3 <= z'' - 1 + 1, z'' - 1 >= 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + s7) + INC(1 + (z'' - 1)) :|: s7 >= 0, s7 <= z'' - 1 + 1, z' >= 0, z >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + LT(z, z') :|: z'' = 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + INC(0) :|: z'' = 0, z' >= 0, z >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(s, 1 + (z'' - 1), z3) + MINUS(1 + (z' - 1), 1 + (z'' - 1)) :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z'' - 1 >= 0, z = 1, z3 >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(0, 1 + (z'' - 1), z3) + MINUS(z', 1 + (z'' - 1)) :|: z'' - 1 >= 0, z = 1, z' >= 0, z3 >= 0 INC(z) -{ 1 }-> 1 + INC(z - 1) :|: z - 1 >= 0 LT(z, z') -{ 1 }-> 1 + LT(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 MINUS(z, z') -{ 1 }-> 1 + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 inc(z) -{ 0 }-> 0 :|: z >= 0 inc(z) -{ 0 }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1 + 1, z - 1 >= 0 inc(z) -{ 0 }-> 1 + 0 :|: z = 0 lt(z, z') -{ 0 }-> lt(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 lt(z, z') -{ 0 }-> 2 :|: z' - 1 >= 0, z = 0 lt(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0 lt(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 minus(z, z') -{ 0 }-> s' :|: s' >= 0, s' <= z - 1, z' - 1 >= 0, z - 1 >= 0 minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 Function symbols to be analyzed: {LT}, {INC}, {lt}, {MINUS}, {IF,DIV} Previous analysis results are: minus: runtime: O(1) [0], size: O(n^1) [z] inc: runtime: O(1) [0], size: O(n^1) [1 + z] ---------------------------------------- (37) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: LT after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 0 ---------------------------------------- (38) Obligation: Complexity RNTS consisting of the following rules: DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + LT(1 + (z - 1), 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + INC(z'') :|: z - 1 >= 0, z'' >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + s2) + LT(1 + (z - 1), 1 + (z' - 1)) :|: s2 >= 0, s2 <= z'' - 1 + 1, z' - 1 >= 0, z - 1 >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + s6) + INC(1 + (z'' - 1)) :|: s6 >= 0, s6 <= z'' - 1 + 1, z - 1 >= 0, z'' - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + LT(1 + (z - 1), 1 + (z' - 1)) :|: z'' = 0, z' - 1 >= 0, z - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + INC(0) :|: z'' = 0, z - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + LT(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + INC(z'') :|: z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + s1) + LT(0, 1 + (z' - 1)) :|: s1 >= 0, s1 <= z'' - 1 + 1, z' - 1 >= 0, z'' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + s5) + INC(1 + (z'' - 1)) :|: s5 >= 0, s5 <= z'' - 1 + 1, z'' - 1 >= 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + LT(0, 1 + (z' - 1)) :|: z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + INC(0) :|: z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + LT(z, 0) :|: z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + INC(z'') :|: z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + s'') + LT(z, 0) :|: s'' >= 0, s'' <= z'' - 1 + 1, z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + s4) + INC(1 + (z'' - 1)) :|: s4 >= 0, s4 <= z'' - 1 + 1, z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + LT(z, 0) :|: z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + INC(0) :|: z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 0) + LT(z, z') :|: z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 0) + INC(z'') :|: z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + s3) + LT(z, z') :|: s3 >= 0, s3 <= z'' - 1 + 1, z'' - 1 >= 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + s7) + INC(1 + (z'' - 1)) :|: s7 >= 0, s7 <= z'' - 1 + 1, z' >= 0, z >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + LT(z, z') :|: z'' = 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + INC(0) :|: z'' = 0, z' >= 0, z >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(s, 1 + (z'' - 1), z3) + MINUS(1 + (z' - 1), 1 + (z'' - 1)) :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z'' - 1 >= 0, z = 1, z3 >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(0, 1 + (z'' - 1), z3) + MINUS(z', 1 + (z'' - 1)) :|: z'' - 1 >= 0, z = 1, z' >= 0, z3 >= 0 INC(z) -{ 1 }-> 1 + INC(z - 1) :|: z - 1 >= 0 LT(z, z') -{ 1 }-> 1 + LT(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 MINUS(z, z') -{ 1 }-> 1 + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 inc(z) -{ 0 }-> 0 :|: z >= 0 inc(z) -{ 0 }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1 + 1, z - 1 >= 0 inc(z) -{ 0 }-> 1 + 0 :|: z = 0 lt(z, z') -{ 0 }-> lt(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 lt(z, z') -{ 0 }-> 2 :|: z' - 1 >= 0, z = 0 lt(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0 lt(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 minus(z, z') -{ 0 }-> s' :|: s' >= 0, s' <= z - 1, z' - 1 >= 0, z - 1 >= 0 minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 Function symbols to be analyzed: {LT}, {INC}, {lt}, {MINUS}, {IF,DIV} Previous analysis results are: minus: runtime: O(1) [0], size: O(n^1) [z] inc: runtime: O(1) [0], size: O(n^1) [1 + z] LT: runtime: ?, size: O(1) [0] ---------------------------------------- (39) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: LT after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: z' ---------------------------------------- (40) Obligation: Complexity RNTS consisting of the following rules: DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + LT(1 + (z - 1), 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + INC(z'') :|: z - 1 >= 0, z'' >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + s2) + LT(1 + (z - 1), 1 + (z' - 1)) :|: s2 >= 0, s2 <= z'' - 1 + 1, z' - 1 >= 0, z - 1 >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + s6) + INC(1 + (z'' - 1)) :|: s6 >= 0, s6 <= z'' - 1 + 1, z - 1 >= 0, z'' - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + LT(1 + (z - 1), 1 + (z' - 1)) :|: z'' = 0, z' - 1 >= 0, z - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + INC(0) :|: z'' = 0, z - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + LT(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + INC(z'') :|: z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + s1) + LT(0, 1 + (z' - 1)) :|: s1 >= 0, s1 <= z'' - 1 + 1, z' - 1 >= 0, z'' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + s5) + INC(1 + (z'' - 1)) :|: s5 >= 0, s5 <= z'' - 1 + 1, z'' - 1 >= 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + LT(0, 1 + (z' - 1)) :|: z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + INC(0) :|: z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + LT(z, 0) :|: z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + INC(z'') :|: z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + s'') + LT(z, 0) :|: s'' >= 0, s'' <= z'' - 1 + 1, z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + s4) + INC(1 + (z'' - 1)) :|: s4 >= 0, s4 <= z'' - 1 + 1, z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + LT(z, 0) :|: z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + INC(0) :|: z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 0) + LT(z, z') :|: z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 0) + INC(z'') :|: z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + s3) + LT(z, z') :|: s3 >= 0, s3 <= z'' - 1 + 1, z'' - 1 >= 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + s7) + INC(1 + (z'' - 1)) :|: s7 >= 0, s7 <= z'' - 1 + 1, z' >= 0, z >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + LT(z, z') :|: z'' = 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + INC(0) :|: z'' = 0, z' >= 0, z >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(s, 1 + (z'' - 1), z3) + MINUS(1 + (z' - 1), 1 + (z'' - 1)) :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z'' - 1 >= 0, z = 1, z3 >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(0, 1 + (z'' - 1), z3) + MINUS(z', 1 + (z'' - 1)) :|: z'' - 1 >= 0, z = 1, z' >= 0, z3 >= 0 INC(z) -{ 1 }-> 1 + INC(z - 1) :|: z - 1 >= 0 LT(z, z') -{ 1 }-> 1 + LT(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 MINUS(z, z') -{ 1 }-> 1 + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 inc(z) -{ 0 }-> 0 :|: z >= 0 inc(z) -{ 0 }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1 + 1, z - 1 >= 0 inc(z) -{ 0 }-> 1 + 0 :|: z = 0 lt(z, z') -{ 0 }-> lt(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 lt(z, z') -{ 0 }-> 2 :|: z' - 1 >= 0, z = 0 lt(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0 lt(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 minus(z, z') -{ 0 }-> s' :|: s' >= 0, s' <= z - 1, z' - 1 >= 0, z - 1 >= 0 minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 Function symbols to be analyzed: {INC}, {lt}, {MINUS}, {IF,DIV} Previous analysis results are: minus: runtime: O(1) [0], size: O(n^1) [z] inc: runtime: O(1) [0], size: O(n^1) [1 + z] LT: runtime: O(n^1) [z'], size: O(1) [0] ---------------------------------------- (41) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (42) Obligation: Complexity RNTS consisting of the following rules: DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + s17 :|: s17 >= 0, s17 <= 0, z' - 1 >= 0, z - 1 >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + INC(z'') :|: z - 1 >= 0, z'' >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + s2) + s16 :|: s16 >= 0, s16 <= 0, s2 >= 0, s2 <= z'' - 1 + 1, z' - 1 >= 0, z - 1 >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + s6) + INC(1 + (z'' - 1)) :|: s6 >= 0, s6 <= z'' - 1 + 1, z - 1 >= 0, z'' - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + s15 :|: s15 >= 0, s15 <= 0, z'' = 0, z' - 1 >= 0, z - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + INC(0) :|: z'' = 0, z - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + s14 :|: s14 >= 0, s14 <= 0, z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + INC(z'') :|: z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + s1) + s13 :|: s13 >= 0, s13 <= 0, s1 >= 0, s1 <= z'' - 1 + 1, z' - 1 >= 0, z'' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + s5) + INC(1 + (z'' - 1)) :|: s5 >= 0, s5 <= z'' - 1 + 1, z'' - 1 >= 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + s12 :|: s12 >= 0, s12 <= 0, z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + INC(0) :|: z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + s11 :|: s11 >= 0, s11 <= 0, z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + INC(z'') :|: z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + s'') + s10 :|: s10 >= 0, s10 <= 0, s'' >= 0, s'' <= z'' - 1 + 1, z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + s4) + INC(1 + (z'' - 1)) :|: s4 >= 0, s4 <= z'' - 1 + 1, z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + s9 :|: s9 >= 0, s9 <= 0, z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + INC(0) :|: z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 0) + s20 :|: s20 >= 0, s20 <= 0, z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 0) + INC(z'') :|: z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 1 + s3) + s19 :|: s19 >= 0, s19 <= 0, s3 >= 0, s3 <= z'' - 1 + 1, z'' - 1 >= 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + s7) + INC(1 + (z'' - 1)) :|: s7 >= 0, s7 <= z'' - 1 + 1, z' >= 0, z >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 1 + 0) + s18 :|: s18 >= 0, s18 <= 0, z'' = 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + INC(0) :|: z'' = 0, z' >= 0, z >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(s, 1 + (z'' - 1), z3) + MINUS(1 + (z' - 1), 1 + (z'' - 1)) :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z'' - 1 >= 0, z = 1, z3 >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(0, 1 + (z'' - 1), z3) + MINUS(z', 1 + (z'' - 1)) :|: z'' - 1 >= 0, z = 1, z' >= 0, z3 >= 0 INC(z) -{ 1 }-> 1 + INC(z - 1) :|: z - 1 >= 0 LT(z, z') -{ z' }-> 1 + s21 :|: s21 >= 0, s21 <= 0, z' - 1 >= 0, z - 1 >= 0 MINUS(z, z') -{ 1 }-> 1 + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 inc(z) -{ 0 }-> 0 :|: z >= 0 inc(z) -{ 0 }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1 + 1, z - 1 >= 0 inc(z) -{ 0 }-> 1 + 0 :|: z = 0 lt(z, z') -{ 0 }-> lt(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 lt(z, z') -{ 0 }-> 2 :|: z' - 1 >= 0, z = 0 lt(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0 lt(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 minus(z, z') -{ 0 }-> s' :|: s' >= 0, s' <= z - 1, z' - 1 >= 0, z - 1 >= 0 minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 Function symbols to be analyzed: {INC}, {lt}, {MINUS}, {IF,DIV} Previous analysis results are: minus: runtime: O(1) [0], size: O(n^1) [z] inc: runtime: O(1) [0], size: O(n^1) [1 + z] LT: runtime: O(n^1) [z'], size: O(1) [0] ---------------------------------------- (43) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: INC after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 0 ---------------------------------------- (44) Obligation: Complexity RNTS consisting of the following rules: DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + s17 :|: s17 >= 0, s17 <= 0, z' - 1 >= 0, z - 1 >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + INC(z'') :|: z - 1 >= 0, z'' >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + s2) + s16 :|: s16 >= 0, s16 <= 0, s2 >= 0, s2 <= z'' - 1 + 1, z' - 1 >= 0, z - 1 >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + s6) + INC(1 + (z'' - 1)) :|: s6 >= 0, s6 <= z'' - 1 + 1, z - 1 >= 0, z'' - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + s15 :|: s15 >= 0, s15 <= 0, z'' = 0, z' - 1 >= 0, z - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + INC(0) :|: z'' = 0, z - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + s14 :|: s14 >= 0, s14 <= 0, z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + INC(z'') :|: z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + s1) + s13 :|: s13 >= 0, s13 <= 0, s1 >= 0, s1 <= z'' - 1 + 1, z' - 1 >= 0, z'' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + s5) + INC(1 + (z'' - 1)) :|: s5 >= 0, s5 <= z'' - 1 + 1, z'' - 1 >= 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + s12 :|: s12 >= 0, s12 <= 0, z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + INC(0) :|: z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + s11 :|: s11 >= 0, s11 <= 0, z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + INC(z'') :|: z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + s'') + s10 :|: s10 >= 0, s10 <= 0, s'' >= 0, s'' <= z'' - 1 + 1, z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + s4) + INC(1 + (z'' - 1)) :|: s4 >= 0, s4 <= z'' - 1 + 1, z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + s9 :|: s9 >= 0, s9 <= 0, z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + INC(0) :|: z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 0) + s20 :|: s20 >= 0, s20 <= 0, z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 0) + INC(z'') :|: z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 1 + s3) + s19 :|: s19 >= 0, s19 <= 0, s3 >= 0, s3 <= z'' - 1 + 1, z'' - 1 >= 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + s7) + INC(1 + (z'' - 1)) :|: s7 >= 0, s7 <= z'' - 1 + 1, z' >= 0, z >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 1 + 0) + s18 :|: s18 >= 0, s18 <= 0, z'' = 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + INC(0) :|: z'' = 0, z' >= 0, z >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(s, 1 + (z'' - 1), z3) + MINUS(1 + (z' - 1), 1 + (z'' - 1)) :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z'' - 1 >= 0, z = 1, z3 >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(0, 1 + (z'' - 1), z3) + MINUS(z', 1 + (z'' - 1)) :|: z'' - 1 >= 0, z = 1, z' >= 0, z3 >= 0 INC(z) -{ 1 }-> 1 + INC(z - 1) :|: z - 1 >= 0 LT(z, z') -{ z' }-> 1 + s21 :|: s21 >= 0, s21 <= 0, z' - 1 >= 0, z - 1 >= 0 MINUS(z, z') -{ 1 }-> 1 + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 inc(z) -{ 0 }-> 0 :|: z >= 0 inc(z) -{ 0 }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1 + 1, z - 1 >= 0 inc(z) -{ 0 }-> 1 + 0 :|: z = 0 lt(z, z') -{ 0 }-> lt(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 lt(z, z') -{ 0 }-> 2 :|: z' - 1 >= 0, z = 0 lt(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0 lt(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 minus(z, z') -{ 0 }-> s' :|: s' >= 0, s' <= z - 1, z' - 1 >= 0, z - 1 >= 0 minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 Function symbols to be analyzed: {INC}, {lt}, {MINUS}, {IF,DIV} Previous analysis results are: minus: runtime: O(1) [0], size: O(n^1) [z] inc: runtime: O(1) [0], size: O(n^1) [1 + z] LT: runtime: O(n^1) [z'], size: O(1) [0] INC: runtime: ?, size: O(1) [0] ---------------------------------------- (45) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: INC after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: z ---------------------------------------- (46) Obligation: Complexity RNTS consisting of the following rules: DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + s17 :|: s17 >= 0, s17 <= 0, z' - 1 >= 0, z - 1 >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + INC(z'') :|: z - 1 >= 0, z'' >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + s2) + s16 :|: s16 >= 0, s16 <= 0, s2 >= 0, s2 <= z'' - 1 + 1, z' - 1 >= 0, z - 1 >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + s6) + INC(1 + (z'' - 1)) :|: s6 >= 0, s6 <= z'' - 1 + 1, z - 1 >= 0, z'' - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + s15 :|: s15 >= 0, s15 <= 0, z'' = 0, z' - 1 >= 0, z - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + INC(0) :|: z'' = 0, z - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + s14 :|: s14 >= 0, s14 <= 0, z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + INC(z'') :|: z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + s1) + s13 :|: s13 >= 0, s13 <= 0, s1 >= 0, s1 <= z'' - 1 + 1, z' - 1 >= 0, z'' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + s5) + INC(1 + (z'' - 1)) :|: s5 >= 0, s5 <= z'' - 1 + 1, z'' - 1 >= 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + s12 :|: s12 >= 0, s12 <= 0, z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + INC(0) :|: z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + s11 :|: s11 >= 0, s11 <= 0, z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + INC(z'') :|: z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + s'') + s10 :|: s10 >= 0, s10 <= 0, s'' >= 0, s'' <= z'' - 1 + 1, z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + s4) + INC(1 + (z'' - 1)) :|: s4 >= 0, s4 <= z'' - 1 + 1, z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + s9 :|: s9 >= 0, s9 <= 0, z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + INC(0) :|: z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 0) + s20 :|: s20 >= 0, s20 <= 0, z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 0) + INC(z'') :|: z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 1 + s3) + s19 :|: s19 >= 0, s19 <= 0, s3 >= 0, s3 <= z'' - 1 + 1, z'' - 1 >= 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + s7) + INC(1 + (z'' - 1)) :|: s7 >= 0, s7 <= z'' - 1 + 1, z' >= 0, z >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 1 + 0) + s18 :|: s18 >= 0, s18 <= 0, z'' = 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + INC(0) :|: z'' = 0, z' >= 0, z >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(s, 1 + (z'' - 1), z3) + MINUS(1 + (z' - 1), 1 + (z'' - 1)) :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z'' - 1 >= 0, z = 1, z3 >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(0, 1 + (z'' - 1), z3) + MINUS(z', 1 + (z'' - 1)) :|: z'' - 1 >= 0, z = 1, z' >= 0, z3 >= 0 INC(z) -{ 1 }-> 1 + INC(z - 1) :|: z - 1 >= 0 LT(z, z') -{ z' }-> 1 + s21 :|: s21 >= 0, s21 <= 0, z' - 1 >= 0, z - 1 >= 0 MINUS(z, z') -{ 1 }-> 1 + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 inc(z) -{ 0 }-> 0 :|: z >= 0 inc(z) -{ 0 }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1 + 1, z - 1 >= 0 inc(z) -{ 0 }-> 1 + 0 :|: z = 0 lt(z, z') -{ 0 }-> lt(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 lt(z, z') -{ 0 }-> 2 :|: z' - 1 >= 0, z = 0 lt(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0 lt(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 minus(z, z') -{ 0 }-> s' :|: s' >= 0, s' <= z - 1, z' - 1 >= 0, z - 1 >= 0 minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 Function symbols to be analyzed: {lt}, {MINUS}, {IF,DIV} Previous analysis results are: minus: runtime: O(1) [0], size: O(n^1) [z] inc: runtime: O(1) [0], size: O(n^1) [1 + z] LT: runtime: O(n^1) [z'], size: O(1) [0] INC: runtime: O(n^1) [z], size: O(1) [0] ---------------------------------------- (47) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (48) Obligation: Complexity RNTS consisting of the following rules: DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + s17 :|: s17 >= 0, s17 <= 0, z' - 1 >= 0, z - 1 >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + s30 :|: s30 >= 0, s30 <= 0, z - 1 >= 0, z'' >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + s2) + s16 :|: s16 >= 0, s16 <= 0, s2 >= 0, s2 <= z'' - 1 + 1, z' - 1 >= 0, z - 1 >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + s6) + s29 :|: s29 >= 0, s29 <= 0, s6 >= 0, s6 <= z'' - 1 + 1, z - 1 >= 0, z'' - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + s15 :|: s15 >= 0, s15 <= 0, z'' = 0, z' - 1 >= 0, z - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + s28 :|: s28 >= 0, s28 <= 0, z'' = 0, z - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + s14 :|: s14 >= 0, s14 <= 0, z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + s27 :|: s27 >= 0, s27 <= 0, z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + s1) + s13 :|: s13 >= 0, s13 <= 0, s1 >= 0, s1 <= z'' - 1 + 1, z' - 1 >= 0, z'' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + s5) + s26 :|: s26 >= 0, s26 <= 0, s5 >= 0, s5 <= z'' - 1 + 1, z'' - 1 >= 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + s12 :|: s12 >= 0, s12 <= 0, z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + s25 :|: s25 >= 0, s25 <= 0, z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + s11 :|: s11 >= 0, s11 <= 0, z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(1, z, 0, 0) + s24 :|: s24 >= 0, s24 <= 0, z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + s'') + s10 :|: s10 >= 0, s10 <= 0, s'' >= 0, s'' <= z'' - 1 + 1, z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(1, z, 0, 1 + s4) + s23 :|: s23 >= 0, s23 <= 0, s4 >= 0, s4 <= z'' - 1 + 1, z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + s22 :|: s22 >= 0, s22 <= 0, z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + s9 :|: s9 >= 0, s9 <= 0, z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 0) + s20 :|: s20 >= 0, s20 <= 0, z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(0, z, z', 0) + s33 :|: s33 >= 0, s33 <= 0, z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 1 + s3) + s19 :|: s19 >= 0, s19 <= 0, s3 >= 0, s3 <= z'' - 1 + 1, z'' - 1 >= 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(0, z, z', 1 + s7) + s32 :|: s32 >= 0, s32 <= 0, s7 >= 0, s7 <= z'' - 1 + 1, z' >= 0, z >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 1 + 0) + s18 :|: s18 >= 0, s18 <= 0, z'' = 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + s31 :|: s31 >= 0, s31 <= 0, z'' = 0, z' >= 0, z >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(s, 1 + (z'' - 1), z3) + MINUS(1 + (z' - 1), 1 + (z'' - 1)) :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z'' - 1 >= 0, z = 1, z3 >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(0, 1 + (z'' - 1), z3) + MINUS(z', 1 + (z'' - 1)) :|: z'' - 1 >= 0, z = 1, z' >= 0, z3 >= 0 INC(z) -{ z }-> 1 + s34 :|: s34 >= 0, s34 <= 0, z - 1 >= 0 LT(z, z') -{ z' }-> 1 + s21 :|: s21 >= 0, s21 <= 0, z' - 1 >= 0, z - 1 >= 0 MINUS(z, z') -{ 1 }-> 1 + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 inc(z) -{ 0 }-> 0 :|: z >= 0 inc(z) -{ 0 }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1 + 1, z - 1 >= 0 inc(z) -{ 0 }-> 1 + 0 :|: z = 0 lt(z, z') -{ 0 }-> lt(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 lt(z, z') -{ 0 }-> 2 :|: z' - 1 >= 0, z = 0 lt(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0 lt(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 minus(z, z') -{ 0 }-> s' :|: s' >= 0, s' <= z - 1, z' - 1 >= 0, z - 1 >= 0 minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 Function symbols to be analyzed: {lt}, {MINUS}, {IF,DIV} Previous analysis results are: minus: runtime: O(1) [0], size: O(n^1) [z] inc: runtime: O(1) [0], size: O(n^1) [1 + z] LT: runtime: O(n^1) [z'], size: O(1) [0] INC: runtime: O(n^1) [z], size: O(1) [0] ---------------------------------------- (49) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: lt after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 2 ---------------------------------------- (50) Obligation: Complexity RNTS consisting of the following rules: DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + s17 :|: s17 >= 0, s17 <= 0, z' - 1 >= 0, z - 1 >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + s30 :|: s30 >= 0, s30 <= 0, z - 1 >= 0, z'' >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + s2) + s16 :|: s16 >= 0, s16 <= 0, s2 >= 0, s2 <= z'' - 1 + 1, z' - 1 >= 0, z - 1 >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + s6) + s29 :|: s29 >= 0, s29 <= 0, s6 >= 0, s6 <= z'' - 1 + 1, z - 1 >= 0, z'' - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + s15 :|: s15 >= 0, s15 <= 0, z'' = 0, z' - 1 >= 0, z - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + s28 :|: s28 >= 0, s28 <= 0, z'' = 0, z - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + s14 :|: s14 >= 0, s14 <= 0, z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + s27 :|: s27 >= 0, s27 <= 0, z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + s1) + s13 :|: s13 >= 0, s13 <= 0, s1 >= 0, s1 <= z'' - 1 + 1, z' - 1 >= 0, z'' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + s5) + s26 :|: s26 >= 0, s26 <= 0, s5 >= 0, s5 <= z'' - 1 + 1, z'' - 1 >= 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + s12 :|: s12 >= 0, s12 <= 0, z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + s25 :|: s25 >= 0, s25 <= 0, z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + s11 :|: s11 >= 0, s11 <= 0, z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(1, z, 0, 0) + s24 :|: s24 >= 0, s24 <= 0, z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + s'') + s10 :|: s10 >= 0, s10 <= 0, s'' >= 0, s'' <= z'' - 1 + 1, z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(1, z, 0, 1 + s4) + s23 :|: s23 >= 0, s23 <= 0, s4 >= 0, s4 <= z'' - 1 + 1, z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + s22 :|: s22 >= 0, s22 <= 0, z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + s9 :|: s9 >= 0, s9 <= 0, z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 0) + s20 :|: s20 >= 0, s20 <= 0, z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(0, z, z', 0) + s33 :|: s33 >= 0, s33 <= 0, z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 1 + s3) + s19 :|: s19 >= 0, s19 <= 0, s3 >= 0, s3 <= z'' - 1 + 1, z'' - 1 >= 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(0, z, z', 1 + s7) + s32 :|: s32 >= 0, s32 <= 0, s7 >= 0, s7 <= z'' - 1 + 1, z' >= 0, z >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 1 + 0) + s18 :|: s18 >= 0, s18 <= 0, z'' = 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + s31 :|: s31 >= 0, s31 <= 0, z'' = 0, z' >= 0, z >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(s, 1 + (z'' - 1), z3) + MINUS(1 + (z' - 1), 1 + (z'' - 1)) :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z'' - 1 >= 0, z = 1, z3 >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(0, 1 + (z'' - 1), z3) + MINUS(z', 1 + (z'' - 1)) :|: z'' - 1 >= 0, z = 1, z' >= 0, z3 >= 0 INC(z) -{ z }-> 1 + s34 :|: s34 >= 0, s34 <= 0, z - 1 >= 0 LT(z, z') -{ z' }-> 1 + s21 :|: s21 >= 0, s21 <= 0, z' - 1 >= 0, z - 1 >= 0 MINUS(z, z') -{ 1 }-> 1 + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 inc(z) -{ 0 }-> 0 :|: z >= 0 inc(z) -{ 0 }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1 + 1, z - 1 >= 0 inc(z) -{ 0 }-> 1 + 0 :|: z = 0 lt(z, z') -{ 0 }-> lt(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 lt(z, z') -{ 0 }-> 2 :|: z' - 1 >= 0, z = 0 lt(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0 lt(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 minus(z, z') -{ 0 }-> s' :|: s' >= 0, s' <= z - 1, z' - 1 >= 0, z - 1 >= 0 minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 Function symbols to be analyzed: {lt}, {MINUS}, {IF,DIV} Previous analysis results are: minus: runtime: O(1) [0], size: O(n^1) [z] inc: runtime: O(1) [0], size: O(n^1) [1 + z] LT: runtime: O(n^1) [z'], size: O(1) [0] INC: runtime: O(n^1) [z], size: O(1) [0] lt: runtime: ?, size: O(1) [2] ---------------------------------------- (51) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: lt after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 0 ---------------------------------------- (52) Obligation: Complexity RNTS consisting of the following rules: DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + s17 :|: s17 >= 0, s17 <= 0, z' - 1 >= 0, z - 1 >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 0) + s30 :|: s30 >= 0, s30 <= 0, z - 1 >= 0, z'' >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + s2) + s16 :|: s16 >= 0, s16 <= 0, s2 >= 0, s2 <= z'' - 1 + 1, z' - 1 >= 0, z - 1 >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + s6) + s29 :|: s29 >= 0, s29 <= 0, s6 >= 0, s6 <= z'' - 1 + 1, z - 1 >= 0, z'' - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + s15 :|: s15 >= 0, s15 <= 0, z'' = 0, z' - 1 >= 0, z - 1 >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(lt(z - 1, z' - 1), 1 + (z - 1), 1 + (z' - 1), 1 + 0) + s28 :|: s28 >= 0, s28 <= 0, z'' = 0, z - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + s14 :|: s14 >= 0, s14 <= 0, z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + s27 :|: s27 >= 0, s27 <= 0, z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + s1) + s13 :|: s13 >= 0, s13 <= 0, s1 >= 0, s1 <= z'' - 1 + 1, z' - 1 >= 0, z'' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + s5) + s26 :|: s26 >= 0, s26 <= 0, s5 >= 0, s5 <= z'' - 1 + 1, z'' - 1 >= 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + s12 :|: s12 >= 0, s12 <= 0, z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + s25 :|: s25 >= 0, s25 <= 0, z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + s11 :|: s11 >= 0, s11 <= 0, z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(1, z, 0, 0) + s24 :|: s24 >= 0, s24 <= 0, z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + s'') + s10 :|: s10 >= 0, s10 <= 0, s'' >= 0, s'' <= z'' - 1 + 1, z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(1, z, 0, 1 + s4) + s23 :|: s23 >= 0, s23 <= 0, s4 >= 0, s4 <= z'' - 1 + 1, z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + s22 :|: s22 >= 0, s22 <= 0, z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + s9 :|: s9 >= 0, s9 <= 0, z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 0) + s20 :|: s20 >= 0, s20 <= 0, z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(0, z, z', 0) + s33 :|: s33 >= 0, s33 <= 0, z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 1 + s3) + s19 :|: s19 >= 0, s19 <= 0, s3 >= 0, s3 <= z'' - 1 + 1, z'' - 1 >= 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(0, z, z', 1 + s7) + s32 :|: s32 >= 0, s32 <= 0, s7 >= 0, s7 <= z'' - 1 + 1, z' >= 0, z >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 1 + 0) + s18 :|: s18 >= 0, s18 <= 0, z'' = 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + s31 :|: s31 >= 0, s31 <= 0, z'' = 0, z' >= 0, z >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(s, 1 + (z'' - 1), z3) + MINUS(1 + (z' - 1), 1 + (z'' - 1)) :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z'' - 1 >= 0, z = 1, z3 >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(0, 1 + (z'' - 1), z3) + MINUS(z', 1 + (z'' - 1)) :|: z'' - 1 >= 0, z = 1, z' >= 0, z3 >= 0 INC(z) -{ z }-> 1 + s34 :|: s34 >= 0, s34 <= 0, z - 1 >= 0 LT(z, z') -{ z' }-> 1 + s21 :|: s21 >= 0, s21 <= 0, z' - 1 >= 0, z - 1 >= 0 MINUS(z, z') -{ 1 }-> 1 + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 inc(z) -{ 0 }-> 0 :|: z >= 0 inc(z) -{ 0 }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1 + 1, z - 1 >= 0 inc(z) -{ 0 }-> 1 + 0 :|: z = 0 lt(z, z') -{ 0 }-> lt(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 lt(z, z') -{ 0 }-> 2 :|: z' - 1 >= 0, z = 0 lt(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0 lt(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 minus(z, z') -{ 0 }-> s' :|: s' >= 0, s' <= z - 1, z' - 1 >= 0, z - 1 >= 0 minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 Function symbols to be analyzed: {MINUS}, {IF,DIV} Previous analysis results are: minus: runtime: O(1) [0], size: O(n^1) [z] inc: runtime: O(1) [0], size: O(n^1) [1 + z] LT: runtime: O(n^1) [z'], size: O(1) [0] INC: runtime: O(n^1) [z], size: O(1) [0] lt: runtime: O(1) [0], size: O(1) [2] ---------------------------------------- (53) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (54) Obligation: Complexity RNTS consisting of the following rules: DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(s35, 1 + (z - 1), 1 + (z' - 1), 1 + 0) + s15 :|: s35 >= 0, s35 <= 2, s15 >= 0, s15 <= 0, z'' = 0, z' - 1 >= 0, z - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(s36, 1 + (z - 1), 1 + (z' - 1), 1 + s2) + s16 :|: s36 >= 0, s36 <= 2, s16 >= 0, s16 <= 0, s2 >= 0, s2 <= z'' - 1 + 1, z' - 1 >= 0, z - 1 >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(s37, 1 + (z - 1), 1 + (z' - 1), 0) + s17 :|: s37 >= 0, s37 <= 2, s17 >= 0, s17 <= 0, z' - 1 >= 0, z - 1 >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(s38, 1 + (z - 1), 1 + (z' - 1), 1 + 0) + s28 :|: s38 >= 0, s38 <= 2, s28 >= 0, s28 <= 0, z'' = 0, z - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(s39, 1 + (z - 1), 1 + (z' - 1), 1 + s6) + s29 :|: s39 >= 0, s39 <= 2, s29 >= 0, s29 <= 0, s6 >= 0, s6 <= z'' - 1 + 1, z - 1 >= 0, z'' - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(s40, 1 + (z - 1), 1 + (z' - 1), 0) + s30 :|: s40 >= 0, s40 <= 2, s30 >= 0, s30 <= 0, z - 1 >= 0, z'' >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + s14 :|: s14 >= 0, s14 <= 0, z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + s27 :|: s27 >= 0, s27 <= 0, z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + s1) + s13 :|: s13 >= 0, s13 <= 0, s1 >= 0, s1 <= z'' - 1 + 1, z' - 1 >= 0, z'' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + s5) + s26 :|: s26 >= 0, s26 <= 0, s5 >= 0, s5 <= z'' - 1 + 1, z'' - 1 >= 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + s12 :|: s12 >= 0, s12 <= 0, z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + s25 :|: s25 >= 0, s25 <= 0, z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + s11 :|: s11 >= 0, s11 <= 0, z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(1, z, 0, 0) + s24 :|: s24 >= 0, s24 <= 0, z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + s'') + s10 :|: s10 >= 0, s10 <= 0, s'' >= 0, s'' <= z'' - 1 + 1, z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(1, z, 0, 1 + s4) + s23 :|: s23 >= 0, s23 <= 0, s4 >= 0, s4 <= z'' - 1 + 1, z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + s22 :|: s22 >= 0, s22 <= 0, z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + s9 :|: s9 >= 0, s9 <= 0, z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 0) + s20 :|: s20 >= 0, s20 <= 0, z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(0, z, z', 0) + s33 :|: s33 >= 0, s33 <= 0, z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 1 + s3) + s19 :|: s19 >= 0, s19 <= 0, s3 >= 0, s3 <= z'' - 1 + 1, z'' - 1 >= 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(0, z, z', 1 + s7) + s32 :|: s32 >= 0, s32 <= 0, s7 >= 0, s7 <= z'' - 1 + 1, z' >= 0, z >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 1 + 0) + s18 :|: s18 >= 0, s18 <= 0, z'' = 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + s31 :|: s31 >= 0, s31 <= 0, z'' = 0, z' >= 0, z >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(s, 1 + (z'' - 1), z3) + MINUS(1 + (z' - 1), 1 + (z'' - 1)) :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z'' - 1 >= 0, z = 1, z3 >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(0, 1 + (z'' - 1), z3) + MINUS(z', 1 + (z'' - 1)) :|: z'' - 1 >= 0, z = 1, z' >= 0, z3 >= 0 INC(z) -{ z }-> 1 + s34 :|: s34 >= 0, s34 <= 0, z - 1 >= 0 LT(z, z') -{ z' }-> 1 + s21 :|: s21 >= 0, s21 <= 0, z' - 1 >= 0, z - 1 >= 0 MINUS(z, z') -{ 1 }-> 1 + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 inc(z) -{ 0 }-> 0 :|: z >= 0 inc(z) -{ 0 }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1 + 1, z - 1 >= 0 inc(z) -{ 0 }-> 1 + 0 :|: z = 0 lt(z, z') -{ 0 }-> s41 :|: s41 >= 0, s41 <= 2, z' - 1 >= 0, z - 1 >= 0 lt(z, z') -{ 0 }-> 2 :|: z' - 1 >= 0, z = 0 lt(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0 lt(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 minus(z, z') -{ 0 }-> s' :|: s' >= 0, s' <= z - 1, z' - 1 >= 0, z - 1 >= 0 minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 Function symbols to be analyzed: {MINUS}, {IF,DIV} Previous analysis results are: minus: runtime: O(1) [0], size: O(n^1) [z] inc: runtime: O(1) [0], size: O(n^1) [1 + z] LT: runtime: O(n^1) [z'], size: O(1) [0] INC: runtime: O(n^1) [z], size: O(1) [0] lt: runtime: O(1) [0], size: O(1) [2] ---------------------------------------- (55) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: MINUS after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 0 ---------------------------------------- (56) Obligation: Complexity RNTS consisting of the following rules: DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(s35, 1 + (z - 1), 1 + (z' - 1), 1 + 0) + s15 :|: s35 >= 0, s35 <= 2, s15 >= 0, s15 <= 0, z'' = 0, z' - 1 >= 0, z - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(s36, 1 + (z - 1), 1 + (z' - 1), 1 + s2) + s16 :|: s36 >= 0, s36 <= 2, s16 >= 0, s16 <= 0, s2 >= 0, s2 <= z'' - 1 + 1, z' - 1 >= 0, z - 1 >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(s37, 1 + (z - 1), 1 + (z' - 1), 0) + s17 :|: s37 >= 0, s37 <= 2, s17 >= 0, s17 <= 0, z' - 1 >= 0, z - 1 >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(s38, 1 + (z - 1), 1 + (z' - 1), 1 + 0) + s28 :|: s38 >= 0, s38 <= 2, s28 >= 0, s28 <= 0, z'' = 0, z - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(s39, 1 + (z - 1), 1 + (z' - 1), 1 + s6) + s29 :|: s39 >= 0, s39 <= 2, s29 >= 0, s29 <= 0, s6 >= 0, s6 <= z'' - 1 + 1, z - 1 >= 0, z'' - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(s40, 1 + (z - 1), 1 + (z' - 1), 0) + s30 :|: s40 >= 0, s40 <= 2, s30 >= 0, s30 <= 0, z - 1 >= 0, z'' >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + s14 :|: s14 >= 0, s14 <= 0, z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + s27 :|: s27 >= 0, s27 <= 0, z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + s1) + s13 :|: s13 >= 0, s13 <= 0, s1 >= 0, s1 <= z'' - 1 + 1, z' - 1 >= 0, z'' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + s5) + s26 :|: s26 >= 0, s26 <= 0, s5 >= 0, s5 <= z'' - 1 + 1, z'' - 1 >= 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + s12 :|: s12 >= 0, s12 <= 0, z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + s25 :|: s25 >= 0, s25 <= 0, z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + s11 :|: s11 >= 0, s11 <= 0, z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(1, z, 0, 0) + s24 :|: s24 >= 0, s24 <= 0, z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + s'') + s10 :|: s10 >= 0, s10 <= 0, s'' >= 0, s'' <= z'' - 1 + 1, z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(1, z, 0, 1 + s4) + s23 :|: s23 >= 0, s23 <= 0, s4 >= 0, s4 <= z'' - 1 + 1, z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + s22 :|: s22 >= 0, s22 <= 0, z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + s9 :|: s9 >= 0, s9 <= 0, z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 0) + s20 :|: s20 >= 0, s20 <= 0, z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(0, z, z', 0) + s33 :|: s33 >= 0, s33 <= 0, z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 1 + s3) + s19 :|: s19 >= 0, s19 <= 0, s3 >= 0, s3 <= z'' - 1 + 1, z'' - 1 >= 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(0, z, z', 1 + s7) + s32 :|: s32 >= 0, s32 <= 0, s7 >= 0, s7 <= z'' - 1 + 1, z' >= 0, z >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 1 + 0) + s18 :|: s18 >= 0, s18 <= 0, z'' = 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + s31 :|: s31 >= 0, s31 <= 0, z'' = 0, z' >= 0, z >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(s, 1 + (z'' - 1), z3) + MINUS(1 + (z' - 1), 1 + (z'' - 1)) :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z'' - 1 >= 0, z = 1, z3 >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(0, 1 + (z'' - 1), z3) + MINUS(z', 1 + (z'' - 1)) :|: z'' - 1 >= 0, z = 1, z' >= 0, z3 >= 0 INC(z) -{ z }-> 1 + s34 :|: s34 >= 0, s34 <= 0, z - 1 >= 0 LT(z, z') -{ z' }-> 1 + s21 :|: s21 >= 0, s21 <= 0, z' - 1 >= 0, z - 1 >= 0 MINUS(z, z') -{ 1 }-> 1 + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 inc(z) -{ 0 }-> 0 :|: z >= 0 inc(z) -{ 0 }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1 + 1, z - 1 >= 0 inc(z) -{ 0 }-> 1 + 0 :|: z = 0 lt(z, z') -{ 0 }-> s41 :|: s41 >= 0, s41 <= 2, z' - 1 >= 0, z - 1 >= 0 lt(z, z') -{ 0 }-> 2 :|: z' - 1 >= 0, z = 0 lt(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0 lt(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 minus(z, z') -{ 0 }-> s' :|: s' >= 0, s' <= z - 1, z' - 1 >= 0, z - 1 >= 0 minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 Function symbols to be analyzed: {MINUS}, {IF,DIV} Previous analysis results are: minus: runtime: O(1) [0], size: O(n^1) [z] inc: runtime: O(1) [0], size: O(n^1) [1 + z] LT: runtime: O(n^1) [z'], size: O(1) [0] INC: runtime: O(n^1) [z], size: O(1) [0] lt: runtime: O(1) [0], size: O(1) [2] MINUS: runtime: ?, size: O(1) [0] ---------------------------------------- (57) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: MINUS after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: z' ---------------------------------------- (58) Obligation: Complexity RNTS consisting of the following rules: DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(s35, 1 + (z - 1), 1 + (z' - 1), 1 + 0) + s15 :|: s35 >= 0, s35 <= 2, s15 >= 0, s15 <= 0, z'' = 0, z' - 1 >= 0, z - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(s36, 1 + (z - 1), 1 + (z' - 1), 1 + s2) + s16 :|: s36 >= 0, s36 <= 2, s16 >= 0, s16 <= 0, s2 >= 0, s2 <= z'' - 1 + 1, z' - 1 >= 0, z - 1 >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(s37, 1 + (z - 1), 1 + (z' - 1), 0) + s17 :|: s37 >= 0, s37 <= 2, s17 >= 0, s17 <= 0, z' - 1 >= 0, z - 1 >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(s38, 1 + (z - 1), 1 + (z' - 1), 1 + 0) + s28 :|: s38 >= 0, s38 <= 2, s28 >= 0, s28 <= 0, z'' = 0, z - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(s39, 1 + (z - 1), 1 + (z' - 1), 1 + s6) + s29 :|: s39 >= 0, s39 <= 2, s29 >= 0, s29 <= 0, s6 >= 0, s6 <= z'' - 1 + 1, z - 1 >= 0, z'' - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(s40, 1 + (z - 1), 1 + (z' - 1), 0) + s30 :|: s40 >= 0, s40 <= 2, s30 >= 0, s30 <= 0, z - 1 >= 0, z'' >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + s14 :|: s14 >= 0, s14 <= 0, z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + s27 :|: s27 >= 0, s27 <= 0, z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + s1) + s13 :|: s13 >= 0, s13 <= 0, s1 >= 0, s1 <= z'' - 1 + 1, z' - 1 >= 0, z'' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + s5) + s26 :|: s26 >= 0, s26 <= 0, s5 >= 0, s5 <= z'' - 1 + 1, z'' - 1 >= 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + s12 :|: s12 >= 0, s12 <= 0, z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + s25 :|: s25 >= 0, s25 <= 0, z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + s11 :|: s11 >= 0, s11 <= 0, z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(1, z, 0, 0) + s24 :|: s24 >= 0, s24 <= 0, z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + s'') + s10 :|: s10 >= 0, s10 <= 0, s'' >= 0, s'' <= z'' - 1 + 1, z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(1, z, 0, 1 + s4) + s23 :|: s23 >= 0, s23 <= 0, s4 >= 0, s4 <= z'' - 1 + 1, z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + s22 :|: s22 >= 0, s22 <= 0, z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + s9 :|: s9 >= 0, s9 <= 0, z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 0) + s20 :|: s20 >= 0, s20 <= 0, z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(0, z, z', 0) + s33 :|: s33 >= 0, s33 <= 0, z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 1 + s3) + s19 :|: s19 >= 0, s19 <= 0, s3 >= 0, s3 <= z'' - 1 + 1, z'' - 1 >= 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(0, z, z', 1 + s7) + s32 :|: s32 >= 0, s32 <= 0, s7 >= 0, s7 <= z'' - 1 + 1, z' >= 0, z >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 1 + 0) + s18 :|: s18 >= 0, s18 <= 0, z'' = 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + s31 :|: s31 >= 0, s31 <= 0, z'' = 0, z' >= 0, z >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(s, 1 + (z'' - 1), z3) + MINUS(1 + (z' - 1), 1 + (z'' - 1)) :|: s >= 0, s <= z' - 1, z' - 1 >= 0, z'' - 1 >= 0, z = 1, z3 >= 0 IF(z, z', z'', z3) -{ 1 }-> 1 + DIV(0, 1 + (z'' - 1), z3) + MINUS(z', 1 + (z'' - 1)) :|: z'' - 1 >= 0, z = 1, z' >= 0, z3 >= 0 INC(z) -{ z }-> 1 + s34 :|: s34 >= 0, s34 <= 0, z - 1 >= 0 LT(z, z') -{ z' }-> 1 + s21 :|: s21 >= 0, s21 <= 0, z' - 1 >= 0, z - 1 >= 0 MINUS(z, z') -{ 1 }-> 1 + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 inc(z) -{ 0 }-> 0 :|: z >= 0 inc(z) -{ 0 }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1 + 1, z - 1 >= 0 inc(z) -{ 0 }-> 1 + 0 :|: z = 0 lt(z, z') -{ 0 }-> s41 :|: s41 >= 0, s41 <= 2, z' - 1 >= 0, z - 1 >= 0 lt(z, z') -{ 0 }-> 2 :|: z' - 1 >= 0, z = 0 lt(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0 lt(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 minus(z, z') -{ 0 }-> s' :|: s' >= 0, s' <= z - 1, z' - 1 >= 0, z - 1 >= 0 minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 Function symbols to be analyzed: {IF,DIV} Previous analysis results are: minus: runtime: O(1) [0], size: O(n^1) [z] inc: runtime: O(1) [0], size: O(n^1) [1 + z] LT: runtime: O(n^1) [z'], size: O(1) [0] INC: runtime: O(n^1) [z], size: O(1) [0] lt: runtime: O(1) [0], size: O(1) [2] MINUS: runtime: O(n^1) [z'], size: O(1) [0] ---------------------------------------- (59) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (60) Obligation: Complexity RNTS consisting of the following rules: DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(s35, 1 + (z - 1), 1 + (z' - 1), 1 + 0) + s15 :|: s35 >= 0, s35 <= 2, s15 >= 0, s15 <= 0, z'' = 0, z' - 1 >= 0, z - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(s36, 1 + (z - 1), 1 + (z' - 1), 1 + s2) + s16 :|: s36 >= 0, s36 <= 2, s16 >= 0, s16 <= 0, s2 >= 0, s2 <= z'' - 1 + 1, z' - 1 >= 0, z - 1 >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(s37, 1 + (z - 1), 1 + (z' - 1), 0) + s17 :|: s37 >= 0, s37 <= 2, s17 >= 0, s17 <= 0, z' - 1 >= 0, z - 1 >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(s38, 1 + (z - 1), 1 + (z' - 1), 1 + 0) + s28 :|: s38 >= 0, s38 <= 2, s28 >= 0, s28 <= 0, z'' = 0, z - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(s39, 1 + (z - 1), 1 + (z' - 1), 1 + s6) + s29 :|: s39 >= 0, s39 <= 2, s29 >= 0, s29 <= 0, s6 >= 0, s6 <= z'' - 1 + 1, z - 1 >= 0, z'' - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(s40, 1 + (z - 1), 1 + (z' - 1), 0) + s30 :|: s40 >= 0, s40 <= 2, s30 >= 0, s30 <= 0, z - 1 >= 0, z'' >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + s14 :|: s14 >= 0, s14 <= 0, z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + s27 :|: s27 >= 0, s27 <= 0, z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + s1) + s13 :|: s13 >= 0, s13 <= 0, s1 >= 0, s1 <= z'' - 1 + 1, z' - 1 >= 0, z'' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + s5) + s26 :|: s26 >= 0, s26 <= 0, s5 >= 0, s5 <= z'' - 1 + 1, z'' - 1 >= 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + s12 :|: s12 >= 0, s12 <= 0, z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + s25 :|: s25 >= 0, s25 <= 0, z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + s11 :|: s11 >= 0, s11 <= 0, z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(1, z, 0, 0) + s24 :|: s24 >= 0, s24 <= 0, z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + s'') + s10 :|: s10 >= 0, s10 <= 0, s'' >= 0, s'' <= z'' - 1 + 1, z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(1, z, 0, 1 + s4) + s23 :|: s23 >= 0, s23 <= 0, s4 >= 0, s4 <= z'' - 1 + 1, z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + s22 :|: s22 >= 0, s22 <= 0, z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + s9 :|: s9 >= 0, s9 <= 0, z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 0) + s20 :|: s20 >= 0, s20 <= 0, z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(0, z, z', 0) + s33 :|: s33 >= 0, s33 <= 0, z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 1 + s3) + s19 :|: s19 >= 0, s19 <= 0, s3 >= 0, s3 <= z'' - 1 + 1, z'' - 1 >= 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(0, z, z', 1 + s7) + s32 :|: s32 >= 0, s32 <= 0, s7 >= 0, s7 <= z'' - 1 + 1, z' >= 0, z >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 1 + 0) + s18 :|: s18 >= 0, s18 <= 0, z'' = 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + s31 :|: s31 >= 0, s31 <= 0, z'' = 0, z' >= 0, z >= 0 IF(z, z', z'', z3) -{ 1 + z'' }-> 1 + DIV(s, 1 + (z'' - 1), z3) + s42 :|: s42 >= 0, s42 <= 0, s >= 0, s <= z' - 1, z' - 1 >= 0, z'' - 1 >= 0, z = 1, z3 >= 0 IF(z, z', z'', z3) -{ 1 + z'' }-> 1 + DIV(0, 1 + (z'' - 1), z3) + s43 :|: s43 >= 0, s43 <= 0, z'' - 1 >= 0, z = 1, z' >= 0, z3 >= 0 INC(z) -{ z }-> 1 + s34 :|: s34 >= 0, s34 <= 0, z - 1 >= 0 LT(z, z') -{ z' }-> 1 + s21 :|: s21 >= 0, s21 <= 0, z' - 1 >= 0, z - 1 >= 0 MINUS(z, z') -{ z' }-> 1 + s44 :|: s44 >= 0, s44 <= 0, z' - 1 >= 0, z - 1 >= 0 inc(z) -{ 0 }-> 0 :|: z >= 0 inc(z) -{ 0 }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1 + 1, z - 1 >= 0 inc(z) -{ 0 }-> 1 + 0 :|: z = 0 lt(z, z') -{ 0 }-> s41 :|: s41 >= 0, s41 <= 2, z' - 1 >= 0, z - 1 >= 0 lt(z, z') -{ 0 }-> 2 :|: z' - 1 >= 0, z = 0 lt(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0 lt(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 minus(z, z') -{ 0 }-> s' :|: s' >= 0, s' <= z - 1, z' - 1 >= 0, z - 1 >= 0 minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 Function symbols to be analyzed: {IF,DIV} Previous analysis results are: minus: runtime: O(1) [0], size: O(n^1) [z] inc: runtime: O(1) [0], size: O(n^1) [1 + z] LT: runtime: O(n^1) [z'], size: O(1) [0] INC: runtime: O(n^1) [z], size: O(1) [0] lt: runtime: O(1) [0], size: O(1) [2] MINUS: runtime: O(n^1) [z'], size: O(1) [0] ---------------------------------------- (61) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: IF after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 0 Computed SIZE bound using CoFloCo for: DIV after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 1 ---------------------------------------- (62) Obligation: Complexity RNTS consisting of the following rules: DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(s35, 1 + (z - 1), 1 + (z' - 1), 1 + 0) + s15 :|: s35 >= 0, s35 <= 2, s15 >= 0, s15 <= 0, z'' = 0, z' - 1 >= 0, z - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(s36, 1 + (z - 1), 1 + (z' - 1), 1 + s2) + s16 :|: s36 >= 0, s36 <= 2, s16 >= 0, s16 <= 0, s2 >= 0, s2 <= z'' - 1 + 1, z' - 1 >= 0, z - 1 >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(s37, 1 + (z - 1), 1 + (z' - 1), 0) + s17 :|: s37 >= 0, s37 <= 2, s17 >= 0, s17 <= 0, z' - 1 >= 0, z - 1 >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(s38, 1 + (z - 1), 1 + (z' - 1), 1 + 0) + s28 :|: s38 >= 0, s38 <= 2, s28 >= 0, s28 <= 0, z'' = 0, z - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(s39, 1 + (z - 1), 1 + (z' - 1), 1 + s6) + s29 :|: s39 >= 0, s39 <= 2, s29 >= 0, s29 <= 0, s6 >= 0, s6 <= z'' - 1 + 1, z - 1 >= 0, z'' - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(s40, 1 + (z - 1), 1 + (z' - 1), 0) + s30 :|: s40 >= 0, s40 <= 2, s30 >= 0, s30 <= 0, z - 1 >= 0, z'' >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + s14 :|: s14 >= 0, s14 <= 0, z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + s27 :|: s27 >= 0, s27 <= 0, z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + s1) + s13 :|: s13 >= 0, s13 <= 0, s1 >= 0, s1 <= z'' - 1 + 1, z' - 1 >= 0, z'' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + s5) + s26 :|: s26 >= 0, s26 <= 0, s5 >= 0, s5 <= z'' - 1 + 1, z'' - 1 >= 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + s12 :|: s12 >= 0, s12 <= 0, z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + s25 :|: s25 >= 0, s25 <= 0, z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + s11 :|: s11 >= 0, s11 <= 0, z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(1, z, 0, 0) + s24 :|: s24 >= 0, s24 <= 0, z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + s'') + s10 :|: s10 >= 0, s10 <= 0, s'' >= 0, s'' <= z'' - 1 + 1, z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(1, z, 0, 1 + s4) + s23 :|: s23 >= 0, s23 <= 0, s4 >= 0, s4 <= z'' - 1 + 1, z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + s22 :|: s22 >= 0, s22 <= 0, z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + s9 :|: s9 >= 0, s9 <= 0, z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 0) + s20 :|: s20 >= 0, s20 <= 0, z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(0, z, z', 0) + s33 :|: s33 >= 0, s33 <= 0, z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 1 + s3) + s19 :|: s19 >= 0, s19 <= 0, s3 >= 0, s3 <= z'' - 1 + 1, z'' - 1 >= 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(0, z, z', 1 + s7) + s32 :|: s32 >= 0, s32 <= 0, s7 >= 0, s7 <= z'' - 1 + 1, z' >= 0, z >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 1 + 0) + s18 :|: s18 >= 0, s18 <= 0, z'' = 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + s31 :|: s31 >= 0, s31 <= 0, z'' = 0, z' >= 0, z >= 0 IF(z, z', z'', z3) -{ 1 + z'' }-> 1 + DIV(s, 1 + (z'' - 1), z3) + s42 :|: s42 >= 0, s42 <= 0, s >= 0, s <= z' - 1, z' - 1 >= 0, z'' - 1 >= 0, z = 1, z3 >= 0 IF(z, z', z'', z3) -{ 1 + z'' }-> 1 + DIV(0, 1 + (z'' - 1), z3) + s43 :|: s43 >= 0, s43 <= 0, z'' - 1 >= 0, z = 1, z' >= 0, z3 >= 0 INC(z) -{ z }-> 1 + s34 :|: s34 >= 0, s34 <= 0, z - 1 >= 0 LT(z, z') -{ z' }-> 1 + s21 :|: s21 >= 0, s21 <= 0, z' - 1 >= 0, z - 1 >= 0 MINUS(z, z') -{ z' }-> 1 + s44 :|: s44 >= 0, s44 <= 0, z' - 1 >= 0, z - 1 >= 0 inc(z) -{ 0 }-> 0 :|: z >= 0 inc(z) -{ 0 }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1 + 1, z - 1 >= 0 inc(z) -{ 0 }-> 1 + 0 :|: z = 0 lt(z, z') -{ 0 }-> s41 :|: s41 >= 0, s41 <= 2, z' - 1 >= 0, z - 1 >= 0 lt(z, z') -{ 0 }-> 2 :|: z' - 1 >= 0, z = 0 lt(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0 lt(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 minus(z, z') -{ 0 }-> s' :|: s' >= 0, s' <= z - 1, z' - 1 >= 0, z - 1 >= 0 minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 Function symbols to be analyzed: {IF,DIV} Previous analysis results are: minus: runtime: O(1) [0], size: O(n^1) [z] inc: runtime: O(1) [0], size: O(n^1) [1 + z] LT: runtime: O(n^1) [z'], size: O(1) [0] INC: runtime: O(n^1) [z], size: O(1) [0] lt: runtime: O(1) [0], size: O(1) [2] MINUS: runtime: O(n^1) [z'], size: O(1) [0] IF: runtime: ?, size: O(1) [0] DIV: runtime: ?, size: O(1) [1] ---------------------------------------- (63) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using KoAT for: IF after applying outer abstraction to obtain an ITS, resulting in: O(n^2) with polynomial bound: 133 + 967*z' + 52*z'*z'' + 90*z'*z3 + 90*z'^2 + 7*z'' + 12*z3 Computed RUNTIME bound using KoAT for: DIV after applying outer abstraction to obtain an ITS, resulting in: O(n^2) with polynomial bound: 3408 + 18486*z + 624*z*z' + 540*z*z'' + 1620*z^2 + 135*z' + 104*z'' ---------------------------------------- (64) Obligation: Complexity RNTS consisting of the following rules: DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(s35, 1 + (z - 1), 1 + (z' - 1), 1 + 0) + s15 :|: s35 >= 0, s35 <= 2, s15 >= 0, s15 <= 0, z'' = 0, z' - 1 >= 0, z - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(s36, 1 + (z - 1), 1 + (z' - 1), 1 + s2) + s16 :|: s36 >= 0, s36 <= 2, s16 >= 0, s16 <= 0, s2 >= 0, s2 <= z'' - 1 + 1, z' - 1 >= 0, z - 1 >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(s37, 1 + (z - 1), 1 + (z' - 1), 0) + s17 :|: s37 >= 0, s37 <= 2, s17 >= 0, s17 <= 0, z' - 1 >= 0, z - 1 >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(s38, 1 + (z - 1), 1 + (z' - 1), 1 + 0) + s28 :|: s38 >= 0, s38 <= 2, s28 >= 0, s28 <= 0, z'' = 0, z - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(s39, 1 + (z - 1), 1 + (z' - 1), 1 + s6) + s29 :|: s39 >= 0, s39 <= 2, s29 >= 0, s29 <= 0, s6 >= 0, s6 <= z'' - 1 + 1, z - 1 >= 0, z'' - 1 >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(s40, 1 + (z - 1), 1 + (z' - 1), 0) + s30 :|: s40 >= 0, s40 <= 2, s30 >= 0, s30 <= 0, z - 1 >= 0, z'' >= 0, z' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + s14 :|: s14 >= 0, s14 <= 0, z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(2, 0, 1 + (z' - 1), 0) + s27 :|: s27 >= 0, s27 <= 0, z' - 1 >= 0, z = 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + s1) + s13 :|: s13 >= 0, s13 <= 0, s1 >= 0, s1 <= z'' - 1 + 1, z' - 1 >= 0, z'' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + s5) + s26 :|: s26 >= 0, s26 <= 0, s5 >= 0, s5 <= z'' - 1 + 1, z'' - 1 >= 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + s12 :|: s12 >= 0, s12 <= 0, z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(2, 0, 1 + (z' - 1), 1 + 0) + s25 :|: s25 >= 0, s25 <= 0, z'' = 0, z' - 1 >= 0, z = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 0) + s11 :|: s11 >= 0, s11 <= 0, z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(1, z, 0, 0) + s24 :|: s24 >= 0, s24 <= 0, z >= 0, z'' >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + s'') + s10 :|: s10 >= 0, s10 <= 0, s'' >= 0, s'' <= z'' - 1 + 1, z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(1, z, 0, 1 + s4) + s23 :|: s23 >= 0, s23 <= 0, s4 >= 0, s4 <= z'' - 1 + 1, z'' - 1 >= 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + s22 :|: s22 >= 0, s22 <= 0, z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(1, z, 0, 1 + 0) + s9 :|: s9 >= 0, s9 <= 0, z'' = 0, z >= 0, z' = 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 0) + s20 :|: s20 >= 0, s20 <= 0, z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(0, z, z', 0) + s33 :|: s33 >= 0, s33 <= 0, z' >= 0, z >= 0, z'' >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 1 + s3) + s19 :|: s19 >= 0, s19 <= 0, s3 >= 0, s3 <= z'' - 1 + 1, z'' - 1 >= 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 + z'' }-> 1 + IF(0, z, z', 1 + s7) + s32 :|: s32 >= 0, s32 <= 0, s7 >= 0, s7 <= z'' - 1 + 1, z' >= 0, z >= 0, z'' - 1 >= 0 DIV(z, z', z'') -{ 1 + z' }-> 1 + IF(0, z, z', 1 + 0) + s18 :|: s18 >= 0, s18 <= 0, z'' = 0, z' >= 0, z >= 0 DIV(z, z', z'') -{ 1 }-> 1 + IF(0, z, z', 1 + 0) + s31 :|: s31 >= 0, s31 <= 0, z'' = 0, z' >= 0, z >= 0 IF(z, z', z'', z3) -{ 1 + z'' }-> 1 + DIV(s, 1 + (z'' - 1), z3) + s42 :|: s42 >= 0, s42 <= 0, s >= 0, s <= z' - 1, z' - 1 >= 0, z'' - 1 >= 0, z = 1, z3 >= 0 IF(z, z', z'', z3) -{ 1 + z'' }-> 1 + DIV(0, 1 + (z'' - 1), z3) + s43 :|: s43 >= 0, s43 <= 0, z'' - 1 >= 0, z = 1, z' >= 0, z3 >= 0 INC(z) -{ z }-> 1 + s34 :|: s34 >= 0, s34 <= 0, z - 1 >= 0 LT(z, z') -{ z' }-> 1 + s21 :|: s21 >= 0, s21 <= 0, z' - 1 >= 0, z - 1 >= 0 MINUS(z, z') -{ z' }-> 1 + s44 :|: s44 >= 0, s44 <= 0, z' - 1 >= 0, z - 1 >= 0 inc(z) -{ 0 }-> 0 :|: z >= 0 inc(z) -{ 0 }-> 1 + s8 :|: s8 >= 0, s8 <= z - 1 + 1, z - 1 >= 0 inc(z) -{ 0 }-> 1 + 0 :|: z = 0 lt(z, z') -{ 0 }-> s41 :|: s41 >= 0, s41 <= 2, z' - 1 >= 0, z - 1 >= 0 lt(z, z') -{ 0 }-> 2 :|: z' - 1 >= 0, z = 0 lt(z, z') -{ 0 }-> 1 :|: z >= 0, z' = 0 lt(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 minus(z, z') -{ 0 }-> s' :|: s' >= 0, s' <= z - 1, z' - 1 >= 0, z - 1 >= 0 minus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 Function symbols to be analyzed: Previous analysis results are: minus: runtime: O(1) [0], size: O(n^1) [z] inc: runtime: O(1) [0], size: O(n^1) [1 + z] LT: runtime: O(n^1) [z'], size: O(1) [0] INC: runtime: O(n^1) [z], size: O(1) [0] lt: runtime: O(1) [0], size: O(1) [2] MINUS: runtime: O(n^1) [z'], size: O(1) [0] IF: runtime: O(n^2) [133 + 967*z' + 52*z'*z'' + 90*z'*z3 + 90*z'^2 + 7*z'' + 12*z3], size: O(1) [0] DIV: runtime: O(n^2) [3408 + 18486*z + 624*z*z' + 540*z*z'' + 1620*z^2 + 135*z' + 104*z''], size: O(1) [1] ---------------------------------------- (65) FinalProof (FINISHED) Computed overall runtime complexity ---------------------------------------- (66) BOUNDS(1, n^2) ---------------------------------------- (67) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (68) Obligation: Complexity Dependency Tuples Problem Rules: division(z0, z1) -> div(z0, z1, 0) div(z0, z1, z2) -> if(lt(z0, z1), z0, z1, inc(z2)) if(true, z0, z1, z2) -> z2 if(false, z0, s(z1), z2) -> div(minus(z0, s(z1)), s(z1), z2) minus(z0, 0) -> z0 minus(s(z0), s(z1)) -> minus(z0, z1) lt(z0, 0) -> false lt(0, s(z0)) -> true lt(s(z0), s(z1)) -> lt(z0, z1) inc(0) -> s(0) inc(s(z0)) -> s(inc(z0)) Tuples: DIVISION(z0, z1) -> c(DIV(z0, z1, 0)) DIV(z0, z1, z2) -> c1(IF(lt(z0, z1), z0, z1, inc(z2)), LT(z0, z1)) DIV(z0, z1, z2) -> c2(IF(lt(z0, z1), z0, z1, inc(z2)), INC(z2)) IF(true, z0, z1, z2) -> c3 IF(false, z0, s(z1), z2) -> c4(DIV(minus(z0, s(z1)), s(z1), z2), MINUS(z0, s(z1))) MINUS(z0, 0) -> c5 MINUS(s(z0), s(z1)) -> c6(MINUS(z0, z1)) LT(z0, 0) -> c7 LT(0, s(z0)) -> c8 LT(s(z0), s(z1)) -> c9(LT(z0, z1)) INC(0) -> c10 INC(s(z0)) -> c11(INC(z0)) S tuples: DIVISION(z0, z1) -> c(DIV(z0, z1, 0)) DIV(z0, z1, z2) -> c1(IF(lt(z0, z1), z0, z1, inc(z2)), LT(z0, z1)) DIV(z0, z1, z2) -> c2(IF(lt(z0, z1), z0, z1, inc(z2)), INC(z2)) IF(true, z0, z1, z2) -> c3 IF(false, z0, s(z1), z2) -> c4(DIV(minus(z0, s(z1)), s(z1), z2), MINUS(z0, s(z1))) MINUS(z0, 0) -> c5 MINUS(s(z0), s(z1)) -> c6(MINUS(z0, z1)) LT(z0, 0) -> c7 LT(0, s(z0)) -> c8 LT(s(z0), s(z1)) -> c9(LT(z0, z1)) INC(0) -> c10 INC(s(z0)) -> c11(INC(z0)) K tuples:none Defined Rule Symbols: division_2, div_3, if_4, minus_2, lt_2, inc_1 Defined Pair Symbols: DIVISION_2, DIV_3, IF_4, MINUS_2, LT_2, INC_1 Compound Symbols: c_1, c1_2, c2_2, c3, c4_2, c5, c6_1, c7, c8, c9_1, c10, c11_1 ---------------------------------------- (69) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID)) Converted S to standard rules, and D \ S as well as R to relative rules. ---------------------------------------- (70) 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: DIVISION(z0, z1) -> c(DIV(z0, z1, 0)) DIV(z0, z1, z2) -> c1(IF(lt(z0, z1), z0, z1, inc(z2)), LT(z0, z1)) DIV(z0, z1, z2) -> c2(IF(lt(z0, z1), z0, z1, inc(z2)), INC(z2)) IF(true, z0, z1, z2) -> c3 IF(false, z0, s(z1), z2) -> c4(DIV(minus(z0, s(z1)), s(z1), z2), MINUS(z0, s(z1))) MINUS(z0, 0) -> c5 MINUS(s(z0), s(z1)) -> c6(MINUS(z0, z1)) LT(z0, 0) -> c7 LT(0, s(z0)) -> c8 LT(s(z0), s(z1)) -> c9(LT(z0, z1)) INC(0) -> c10 INC(s(z0)) -> c11(INC(z0)) The (relative) TRS S consists of the following rules: division(z0, z1) -> div(z0, z1, 0) div(z0, z1, z2) -> if(lt(z0, z1), z0, z1, inc(z2)) if(true, z0, z1, z2) -> z2 if(false, z0, s(z1), z2) -> div(minus(z0, s(z1)), s(z1), z2) minus(z0, 0) -> z0 minus(s(z0), s(z1)) -> minus(z0, z1) lt(z0, 0) -> false lt(0, s(z0)) -> true lt(s(z0), s(z1)) -> lt(z0, z1) inc(0) -> s(0) inc(s(z0)) -> s(inc(z0)) Rewrite Strategy: INNERMOST ---------------------------------------- (71) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (72) 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: DIVISION(z0, z1) -> c(DIV(z0, z1, 0')) DIV(z0, z1, z2) -> c1(IF(lt(z0, z1), z0, z1, inc(z2)), LT(z0, z1)) DIV(z0, z1, z2) -> c2(IF(lt(z0, z1), z0, z1, inc(z2)), INC(z2)) IF(true, z0, z1, z2) -> c3 IF(false, z0, s(z1), z2) -> c4(DIV(minus(z0, s(z1)), s(z1), z2), MINUS(z0, s(z1))) MINUS(z0, 0') -> c5 MINUS(s(z0), s(z1)) -> c6(MINUS(z0, z1)) LT(z0, 0') -> c7 LT(0', s(z0)) -> c8 LT(s(z0), s(z1)) -> c9(LT(z0, z1)) INC(0') -> c10 INC(s(z0)) -> c11(INC(z0)) The (relative) TRS S consists of the following rules: division(z0, z1) -> div(z0, z1, 0') div(z0, z1, z2) -> if(lt(z0, z1), z0, z1, inc(z2)) if(true, z0, z1, z2) -> z2 if(false, z0, s(z1), z2) -> div(minus(z0, s(z1)), s(z1), z2) minus(z0, 0') -> z0 minus(s(z0), s(z1)) -> minus(z0, z1) lt(z0, 0') -> false lt(0', s(z0)) -> true lt(s(z0), s(z1)) -> lt(z0, z1) inc(0') -> s(0') inc(s(z0)) -> s(inc(z0)) Rewrite Strategy: INNERMOST ---------------------------------------- (73) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Inferred types. ---------------------------------------- (74) Obligation: Innermost TRS: Rules: DIVISION(z0, z1) -> c(DIV(z0, z1, 0')) DIV(z0, z1, z2) -> c1(IF(lt(z0, z1), z0, z1, inc(z2)), LT(z0, z1)) DIV(z0, z1, z2) -> c2(IF(lt(z0, z1), z0, z1, inc(z2)), INC(z2)) IF(true, z0, z1, z2) -> c3 IF(false, z0, s(z1), z2) -> c4(DIV(minus(z0, s(z1)), s(z1), z2), MINUS(z0, s(z1))) MINUS(z0, 0') -> c5 MINUS(s(z0), s(z1)) -> c6(MINUS(z0, z1)) LT(z0, 0') -> c7 LT(0', s(z0)) -> c8 LT(s(z0), s(z1)) -> c9(LT(z0, z1)) INC(0') -> c10 INC(s(z0)) -> c11(INC(z0)) division(z0, z1) -> div(z0, z1, 0') div(z0, z1, z2) -> if(lt(z0, z1), z0, z1, inc(z2)) if(true, z0, z1, z2) -> z2 if(false, z0, s(z1), z2) -> div(minus(z0, s(z1)), s(z1), z2) minus(z0, 0') -> z0 minus(s(z0), s(z1)) -> minus(z0, z1) lt(z0, 0') -> false lt(0', s(z0)) -> true lt(s(z0), s(z1)) -> lt(z0, z1) inc(0') -> s(0') inc(s(z0)) -> s(inc(z0)) Types: DIVISION :: 0':s -> 0':s -> c c :: c1:c2 -> c DIV :: 0':s -> 0':s -> 0':s -> c1:c2 0' :: 0':s c1 :: c3:c4 -> c7:c8:c9 -> c1:c2 IF :: true:false -> 0':s -> 0':s -> 0':s -> c3:c4 lt :: 0':s -> 0':s -> true:false inc :: 0':s -> 0':s LT :: 0':s -> 0':s -> c7:c8:c9 c2 :: c3:c4 -> c10:c11 -> c1:c2 INC :: 0':s -> c10:c11 true :: true:false c3 :: c3:c4 false :: true:false s :: 0':s -> 0':s c4 :: c1:c2 -> c5:c6 -> c3:c4 minus :: 0':s -> 0':s -> 0':s MINUS :: 0':s -> 0':s -> c5:c6 c5 :: c5:c6 c6 :: c5:c6 -> c5:c6 c7 :: c7:c8:c9 c8 :: c7:c8:c9 c9 :: c7:c8:c9 -> c7:c8:c9 c10 :: c10:c11 c11 :: c10:c11 -> c10:c11 division :: 0':s -> 0':s -> 0':s div :: 0':s -> 0':s -> 0':s -> 0':s if :: true:false -> 0':s -> 0':s -> 0':s -> 0':s hole_c1_12 :: c hole_0':s2_12 :: 0':s hole_c1:c23_12 :: c1:c2 hole_c3:c44_12 :: c3:c4 hole_c7:c8:c95_12 :: c7:c8:c9 hole_true:false6_12 :: true:false hole_c10:c117_12 :: c10:c11 hole_c5:c68_12 :: c5:c6 gen_0':s9_12 :: Nat -> 0':s gen_c7:c8:c910_12 :: Nat -> c7:c8:c9 gen_c10:c1111_12 :: Nat -> c10:c11 gen_c5:c612_12 :: Nat -> c5:c6 ---------------------------------------- (75) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: DIV, lt, inc, LT, INC, minus, MINUS, div They will be analysed ascendingly in the following order: lt < DIV inc < DIV LT < DIV INC < DIV minus < DIV MINUS < DIV lt < div inc < div minus < div ---------------------------------------- (76) Obligation: Innermost TRS: Rules: DIVISION(z0, z1) -> c(DIV(z0, z1, 0')) DIV(z0, z1, z2) -> c1(IF(lt(z0, z1), z0, z1, inc(z2)), LT(z0, z1)) DIV(z0, z1, z2) -> c2(IF(lt(z0, z1), z0, z1, inc(z2)), INC(z2)) IF(true, z0, z1, z2) -> c3 IF(false, z0, s(z1), z2) -> c4(DIV(minus(z0, s(z1)), s(z1), z2), MINUS(z0, s(z1))) MINUS(z0, 0') -> c5 MINUS(s(z0), s(z1)) -> c6(MINUS(z0, z1)) LT(z0, 0') -> c7 LT(0', s(z0)) -> c8 LT(s(z0), s(z1)) -> c9(LT(z0, z1)) INC(0') -> c10 INC(s(z0)) -> c11(INC(z0)) division(z0, z1) -> div(z0, z1, 0') div(z0, z1, z2) -> if(lt(z0, z1), z0, z1, inc(z2)) if(true, z0, z1, z2) -> z2 if(false, z0, s(z1), z2) -> div(minus(z0, s(z1)), s(z1), z2) minus(z0, 0') -> z0 minus(s(z0), s(z1)) -> minus(z0, z1) lt(z0, 0') -> false lt(0', s(z0)) -> true lt(s(z0), s(z1)) -> lt(z0, z1) inc(0') -> s(0') inc(s(z0)) -> s(inc(z0)) Types: DIVISION :: 0':s -> 0':s -> c c :: c1:c2 -> c DIV :: 0':s -> 0':s -> 0':s -> c1:c2 0' :: 0':s c1 :: c3:c4 -> c7:c8:c9 -> c1:c2 IF :: true:false -> 0':s -> 0':s -> 0':s -> c3:c4 lt :: 0':s -> 0':s -> true:false inc :: 0':s -> 0':s LT :: 0':s -> 0':s -> c7:c8:c9 c2 :: c3:c4 -> c10:c11 -> c1:c2 INC :: 0':s -> c10:c11 true :: true:false c3 :: c3:c4 false :: true:false s :: 0':s -> 0':s c4 :: c1:c2 -> c5:c6 -> c3:c4 minus :: 0':s -> 0':s -> 0':s MINUS :: 0':s -> 0':s -> c5:c6 c5 :: c5:c6 c6 :: c5:c6 -> c5:c6 c7 :: c7:c8:c9 c8 :: c7:c8:c9 c9 :: c7:c8:c9 -> c7:c8:c9 c10 :: c10:c11 c11 :: c10:c11 -> c10:c11 division :: 0':s -> 0':s -> 0':s div :: 0':s -> 0':s -> 0':s -> 0':s if :: true:false -> 0':s -> 0':s -> 0':s -> 0':s hole_c1_12 :: c hole_0':s2_12 :: 0':s hole_c1:c23_12 :: c1:c2 hole_c3:c44_12 :: c3:c4 hole_c7:c8:c95_12 :: c7:c8:c9 hole_true:false6_12 :: true:false hole_c10:c117_12 :: c10:c11 hole_c5:c68_12 :: c5:c6 gen_0':s9_12 :: Nat -> 0':s gen_c7:c8:c910_12 :: Nat -> c7:c8:c9 gen_c10:c1111_12 :: Nat -> c10:c11 gen_c5:c612_12 :: Nat -> c5:c6 Generator Equations: gen_0':s9_12(0) <=> 0' gen_0':s9_12(+(x, 1)) <=> s(gen_0':s9_12(x)) gen_c7:c8:c910_12(0) <=> c7 gen_c7:c8:c910_12(+(x, 1)) <=> c9(gen_c7:c8:c910_12(x)) gen_c10:c1111_12(0) <=> c10 gen_c10:c1111_12(+(x, 1)) <=> c11(gen_c10:c1111_12(x)) gen_c5:c612_12(0) <=> c5 gen_c5:c612_12(+(x, 1)) <=> c6(gen_c5:c612_12(x)) The following defined symbols remain to be analysed: lt, DIV, inc, LT, INC, minus, MINUS, div They will be analysed ascendingly in the following order: lt < DIV inc < DIV LT < DIV INC < DIV minus < DIV MINUS < DIV lt < div inc < div minus < div ---------------------------------------- (77) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: lt(gen_0':s9_12(n14_12), gen_0':s9_12(n14_12)) -> false, rt in Omega(0) Induction Base: lt(gen_0':s9_12(0), gen_0':s9_12(0)) ->_R^Omega(0) false Induction Step: lt(gen_0':s9_12(+(n14_12, 1)), gen_0':s9_12(+(n14_12, 1))) ->_R^Omega(0) lt(gen_0':s9_12(n14_12), gen_0':s9_12(n14_12)) ->_IH false We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (78) Obligation: Innermost TRS: Rules: DIVISION(z0, z1) -> c(DIV(z0, z1, 0')) DIV(z0, z1, z2) -> c1(IF(lt(z0, z1), z0, z1, inc(z2)), LT(z0, z1)) DIV(z0, z1, z2) -> c2(IF(lt(z0, z1), z0, z1, inc(z2)), INC(z2)) IF(true, z0, z1, z2) -> c3 IF(false, z0, s(z1), z2) -> c4(DIV(minus(z0, s(z1)), s(z1), z2), MINUS(z0, s(z1))) MINUS(z0, 0') -> c5 MINUS(s(z0), s(z1)) -> c6(MINUS(z0, z1)) LT(z0, 0') -> c7 LT(0', s(z0)) -> c8 LT(s(z0), s(z1)) -> c9(LT(z0, z1)) INC(0') -> c10 INC(s(z0)) -> c11(INC(z0)) division(z0, z1) -> div(z0, z1, 0') div(z0, z1, z2) -> if(lt(z0, z1), z0, z1, inc(z2)) if(true, z0, z1, z2) -> z2 if(false, z0, s(z1), z2) -> div(minus(z0, s(z1)), s(z1), z2) minus(z0, 0') -> z0 minus(s(z0), s(z1)) -> minus(z0, z1) lt(z0, 0') -> false lt(0', s(z0)) -> true lt(s(z0), s(z1)) -> lt(z0, z1) inc(0') -> s(0') inc(s(z0)) -> s(inc(z0)) Types: DIVISION :: 0':s -> 0':s -> c c :: c1:c2 -> c DIV :: 0':s -> 0':s -> 0':s -> c1:c2 0' :: 0':s c1 :: c3:c4 -> c7:c8:c9 -> c1:c2 IF :: true:false -> 0':s -> 0':s -> 0':s -> c3:c4 lt :: 0':s -> 0':s -> true:false inc :: 0':s -> 0':s LT :: 0':s -> 0':s -> c7:c8:c9 c2 :: c3:c4 -> c10:c11 -> c1:c2 INC :: 0':s -> c10:c11 true :: true:false c3 :: c3:c4 false :: true:false s :: 0':s -> 0':s c4 :: c1:c2 -> c5:c6 -> c3:c4 minus :: 0':s -> 0':s -> 0':s MINUS :: 0':s -> 0':s -> c5:c6 c5 :: c5:c6 c6 :: c5:c6 -> c5:c6 c7 :: c7:c8:c9 c8 :: c7:c8:c9 c9 :: c7:c8:c9 -> c7:c8:c9 c10 :: c10:c11 c11 :: c10:c11 -> c10:c11 division :: 0':s -> 0':s -> 0':s div :: 0':s -> 0':s -> 0':s -> 0':s if :: true:false -> 0':s -> 0':s -> 0':s -> 0':s hole_c1_12 :: c hole_0':s2_12 :: 0':s hole_c1:c23_12 :: c1:c2 hole_c3:c44_12 :: c3:c4 hole_c7:c8:c95_12 :: c7:c8:c9 hole_true:false6_12 :: true:false hole_c10:c117_12 :: c10:c11 hole_c5:c68_12 :: c5:c6 gen_0':s9_12 :: Nat -> 0':s gen_c7:c8:c910_12 :: Nat -> c7:c8:c9 gen_c10:c1111_12 :: Nat -> c10:c11 gen_c5:c612_12 :: Nat -> c5:c6 Lemmas: lt(gen_0':s9_12(n14_12), gen_0':s9_12(n14_12)) -> false, rt in Omega(0) Generator Equations: gen_0':s9_12(0) <=> 0' gen_0':s9_12(+(x, 1)) <=> s(gen_0':s9_12(x)) gen_c7:c8:c910_12(0) <=> c7 gen_c7:c8:c910_12(+(x, 1)) <=> c9(gen_c7:c8:c910_12(x)) gen_c10:c1111_12(0) <=> c10 gen_c10:c1111_12(+(x, 1)) <=> c11(gen_c10:c1111_12(x)) gen_c5:c612_12(0) <=> c5 gen_c5:c612_12(+(x, 1)) <=> c6(gen_c5:c612_12(x)) The following defined symbols remain to be analysed: inc, DIV, LT, INC, minus, MINUS, div They will be analysed ascendingly in the following order: inc < DIV LT < DIV INC < DIV minus < DIV MINUS < DIV inc < div minus < div ---------------------------------------- (79) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: inc(gen_0':s9_12(n398_12)) -> gen_0':s9_12(+(1, n398_12)), rt in Omega(0) Induction Base: inc(gen_0':s9_12(0)) ->_R^Omega(0) s(0') Induction Step: inc(gen_0':s9_12(+(n398_12, 1))) ->_R^Omega(0) s(inc(gen_0':s9_12(n398_12))) ->_IH s(gen_0':s9_12(+(1, c399_12))) We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (80) Obligation: Innermost TRS: Rules: DIVISION(z0, z1) -> c(DIV(z0, z1, 0')) DIV(z0, z1, z2) -> c1(IF(lt(z0, z1), z0, z1, inc(z2)), LT(z0, z1)) DIV(z0, z1, z2) -> c2(IF(lt(z0, z1), z0, z1, inc(z2)), INC(z2)) IF(true, z0, z1, z2) -> c3 IF(false, z0, s(z1), z2) -> c4(DIV(minus(z0, s(z1)), s(z1), z2), MINUS(z0, s(z1))) MINUS(z0, 0') -> c5 MINUS(s(z0), s(z1)) -> c6(MINUS(z0, z1)) LT(z0, 0') -> c7 LT(0', s(z0)) -> c8 LT(s(z0), s(z1)) -> c9(LT(z0, z1)) INC(0') -> c10 INC(s(z0)) -> c11(INC(z0)) division(z0, z1) -> div(z0, z1, 0') div(z0, z1, z2) -> if(lt(z0, z1), z0, z1, inc(z2)) if(true, z0, z1, z2) -> z2 if(false, z0, s(z1), z2) -> div(minus(z0, s(z1)), s(z1), z2) minus(z0, 0') -> z0 minus(s(z0), s(z1)) -> minus(z0, z1) lt(z0, 0') -> false lt(0', s(z0)) -> true lt(s(z0), s(z1)) -> lt(z0, z1) inc(0') -> s(0') inc(s(z0)) -> s(inc(z0)) Types: DIVISION :: 0':s -> 0':s -> c c :: c1:c2 -> c DIV :: 0':s -> 0':s -> 0':s -> c1:c2 0' :: 0':s c1 :: c3:c4 -> c7:c8:c9 -> c1:c2 IF :: true:false -> 0':s -> 0':s -> 0':s -> c3:c4 lt :: 0':s -> 0':s -> true:false inc :: 0':s -> 0':s LT :: 0':s -> 0':s -> c7:c8:c9 c2 :: c3:c4 -> c10:c11 -> c1:c2 INC :: 0':s -> c10:c11 true :: true:false c3 :: c3:c4 false :: true:false s :: 0':s -> 0':s c4 :: c1:c2 -> c5:c6 -> c3:c4 minus :: 0':s -> 0':s -> 0':s MINUS :: 0':s -> 0':s -> c5:c6 c5 :: c5:c6 c6 :: c5:c6 -> c5:c6 c7 :: c7:c8:c9 c8 :: c7:c8:c9 c9 :: c7:c8:c9 -> c7:c8:c9 c10 :: c10:c11 c11 :: c10:c11 -> c10:c11 division :: 0':s -> 0':s -> 0':s div :: 0':s -> 0':s -> 0':s -> 0':s if :: true:false -> 0':s -> 0':s -> 0':s -> 0':s hole_c1_12 :: c hole_0':s2_12 :: 0':s hole_c1:c23_12 :: c1:c2 hole_c3:c44_12 :: c3:c4 hole_c7:c8:c95_12 :: c7:c8:c9 hole_true:false6_12 :: true:false hole_c10:c117_12 :: c10:c11 hole_c5:c68_12 :: c5:c6 gen_0':s9_12 :: Nat -> 0':s gen_c7:c8:c910_12 :: Nat -> c7:c8:c9 gen_c10:c1111_12 :: Nat -> c10:c11 gen_c5:c612_12 :: Nat -> c5:c6 Lemmas: lt(gen_0':s9_12(n14_12), gen_0':s9_12(n14_12)) -> false, rt in Omega(0) inc(gen_0':s9_12(n398_12)) -> gen_0':s9_12(+(1, n398_12)), rt in Omega(0) Generator Equations: gen_0':s9_12(0) <=> 0' gen_0':s9_12(+(x, 1)) <=> s(gen_0':s9_12(x)) gen_c7:c8:c910_12(0) <=> c7 gen_c7:c8:c910_12(+(x, 1)) <=> c9(gen_c7:c8:c910_12(x)) gen_c10:c1111_12(0) <=> c10 gen_c10:c1111_12(+(x, 1)) <=> c11(gen_c10:c1111_12(x)) gen_c5:c612_12(0) <=> c5 gen_c5:c612_12(+(x, 1)) <=> c6(gen_c5:c612_12(x)) The following defined symbols remain to be analysed: LT, DIV, INC, minus, MINUS, div They will be analysed ascendingly in the following order: LT < DIV INC < DIV minus < DIV MINUS < DIV minus < div ---------------------------------------- (81) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: LT(gen_0':s9_12(n694_12), gen_0':s9_12(n694_12)) -> gen_c7:c8:c910_12(n694_12), rt in Omega(1 + n694_12) Induction Base: LT(gen_0':s9_12(0), gen_0':s9_12(0)) ->_R^Omega(1) c7 Induction Step: LT(gen_0':s9_12(+(n694_12, 1)), gen_0':s9_12(+(n694_12, 1))) ->_R^Omega(1) c9(LT(gen_0':s9_12(n694_12), gen_0':s9_12(n694_12))) ->_IH c9(gen_c7:c8:c910_12(c695_12)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (82) Complex Obligation (BEST) ---------------------------------------- (83) Obligation: Proved the lower bound n^1 for the following obligation: Innermost TRS: Rules: DIVISION(z0, z1) -> c(DIV(z0, z1, 0')) DIV(z0, z1, z2) -> c1(IF(lt(z0, z1), z0, z1, inc(z2)), LT(z0, z1)) DIV(z0, z1, z2) -> c2(IF(lt(z0, z1), z0, z1, inc(z2)), INC(z2)) IF(true, z0, z1, z2) -> c3 IF(false, z0, s(z1), z2) -> c4(DIV(minus(z0, s(z1)), s(z1), z2), MINUS(z0, s(z1))) MINUS(z0, 0') -> c5 MINUS(s(z0), s(z1)) -> c6(MINUS(z0, z1)) LT(z0, 0') -> c7 LT(0', s(z0)) -> c8 LT(s(z0), s(z1)) -> c9(LT(z0, z1)) INC(0') -> c10 INC(s(z0)) -> c11(INC(z0)) division(z0, z1) -> div(z0, z1, 0') div(z0, z1, z2) -> if(lt(z0, z1), z0, z1, inc(z2)) if(true, z0, z1, z2) -> z2 if(false, z0, s(z1), z2) -> div(minus(z0, s(z1)), s(z1), z2) minus(z0, 0') -> z0 minus(s(z0), s(z1)) -> minus(z0, z1) lt(z0, 0') -> false lt(0', s(z0)) -> true lt(s(z0), s(z1)) -> lt(z0, z1) inc(0') -> s(0') inc(s(z0)) -> s(inc(z0)) Types: DIVISION :: 0':s -> 0':s -> c c :: c1:c2 -> c DIV :: 0':s -> 0':s -> 0':s -> c1:c2 0' :: 0':s c1 :: c3:c4 -> c7:c8:c9 -> c1:c2 IF :: true:false -> 0':s -> 0':s -> 0':s -> c3:c4 lt :: 0':s -> 0':s -> true:false inc :: 0':s -> 0':s LT :: 0':s -> 0':s -> c7:c8:c9 c2 :: c3:c4 -> c10:c11 -> c1:c2 INC :: 0':s -> c10:c11 true :: true:false c3 :: c3:c4 false :: true:false s :: 0':s -> 0':s c4 :: c1:c2 -> c5:c6 -> c3:c4 minus :: 0':s -> 0':s -> 0':s MINUS :: 0':s -> 0':s -> c5:c6 c5 :: c5:c6 c6 :: c5:c6 -> c5:c6 c7 :: c7:c8:c9 c8 :: c7:c8:c9 c9 :: c7:c8:c9 -> c7:c8:c9 c10 :: c10:c11 c11 :: c10:c11 -> c10:c11 division :: 0':s -> 0':s -> 0':s div :: 0':s -> 0':s -> 0':s -> 0':s if :: true:false -> 0':s -> 0':s -> 0':s -> 0':s hole_c1_12 :: c hole_0':s2_12 :: 0':s hole_c1:c23_12 :: c1:c2 hole_c3:c44_12 :: c3:c4 hole_c7:c8:c95_12 :: c7:c8:c9 hole_true:false6_12 :: true:false hole_c10:c117_12 :: c10:c11 hole_c5:c68_12 :: c5:c6 gen_0':s9_12 :: Nat -> 0':s gen_c7:c8:c910_12 :: Nat -> c7:c8:c9 gen_c10:c1111_12 :: Nat -> c10:c11 gen_c5:c612_12 :: Nat -> c5:c6 Lemmas: lt(gen_0':s9_12(n14_12), gen_0':s9_12(n14_12)) -> false, rt in Omega(0) inc(gen_0':s9_12(n398_12)) -> gen_0':s9_12(+(1, n398_12)), rt in Omega(0) Generator Equations: gen_0':s9_12(0) <=> 0' gen_0':s9_12(+(x, 1)) <=> s(gen_0':s9_12(x)) gen_c7:c8:c910_12(0) <=> c7 gen_c7:c8:c910_12(+(x, 1)) <=> c9(gen_c7:c8:c910_12(x)) gen_c10:c1111_12(0) <=> c10 gen_c10:c1111_12(+(x, 1)) <=> c11(gen_c10:c1111_12(x)) gen_c5:c612_12(0) <=> c5 gen_c5:c612_12(+(x, 1)) <=> c6(gen_c5:c612_12(x)) The following defined symbols remain to be analysed: LT, DIV, INC, minus, MINUS, div They will be analysed ascendingly in the following order: LT < DIV INC < DIV minus < DIV MINUS < DIV minus < div ---------------------------------------- (84) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (85) BOUNDS(n^1, INF) ---------------------------------------- (86) Obligation: Innermost TRS: Rules: DIVISION(z0, z1) -> c(DIV(z0, z1, 0')) DIV(z0, z1, z2) -> c1(IF(lt(z0, z1), z0, z1, inc(z2)), LT(z0, z1)) DIV(z0, z1, z2) -> c2(IF(lt(z0, z1), z0, z1, inc(z2)), INC(z2)) IF(true, z0, z1, z2) -> c3 IF(false, z0, s(z1), z2) -> c4(DIV(minus(z0, s(z1)), s(z1), z2), MINUS(z0, s(z1))) MINUS(z0, 0') -> c5 MINUS(s(z0), s(z1)) -> c6(MINUS(z0, z1)) LT(z0, 0') -> c7 LT(0', s(z0)) -> c8 LT(s(z0), s(z1)) -> c9(LT(z0, z1)) INC(0') -> c10 INC(s(z0)) -> c11(INC(z0)) division(z0, z1) -> div(z0, z1, 0') div(z0, z1, z2) -> if(lt(z0, z1), z0, z1, inc(z2)) if(true, z0, z1, z2) -> z2 if(false, z0, s(z1), z2) -> div(minus(z0, s(z1)), s(z1), z2) minus(z0, 0') -> z0 minus(s(z0), s(z1)) -> minus(z0, z1) lt(z0, 0') -> false lt(0', s(z0)) -> true lt(s(z0), s(z1)) -> lt(z0, z1) inc(0') -> s(0') inc(s(z0)) -> s(inc(z0)) Types: DIVISION :: 0':s -> 0':s -> c c :: c1:c2 -> c DIV :: 0':s -> 0':s -> 0':s -> c1:c2 0' :: 0':s c1 :: c3:c4 -> c7:c8:c9 -> c1:c2 IF :: true:false -> 0':s -> 0':s -> 0':s -> c3:c4 lt :: 0':s -> 0':s -> true:false inc :: 0':s -> 0':s LT :: 0':s -> 0':s -> c7:c8:c9 c2 :: c3:c4 -> c10:c11 -> c1:c2 INC :: 0':s -> c10:c11 true :: true:false c3 :: c3:c4 false :: true:false s :: 0':s -> 0':s c4 :: c1:c2 -> c5:c6 -> c3:c4 minus :: 0':s -> 0':s -> 0':s MINUS :: 0':s -> 0':s -> c5:c6 c5 :: c5:c6 c6 :: c5:c6 -> c5:c6 c7 :: c7:c8:c9 c8 :: c7:c8:c9 c9 :: c7:c8:c9 -> c7:c8:c9 c10 :: c10:c11 c11 :: c10:c11 -> c10:c11 division :: 0':s -> 0':s -> 0':s div :: 0':s -> 0':s -> 0':s -> 0':s if :: true:false -> 0':s -> 0':s -> 0':s -> 0':s hole_c1_12 :: c hole_0':s2_12 :: 0':s hole_c1:c23_12 :: c1:c2 hole_c3:c44_12 :: c3:c4 hole_c7:c8:c95_12 :: c7:c8:c9 hole_true:false6_12 :: true:false hole_c10:c117_12 :: c10:c11 hole_c5:c68_12 :: c5:c6 gen_0':s9_12 :: Nat -> 0':s gen_c7:c8:c910_12 :: Nat -> c7:c8:c9 gen_c10:c1111_12 :: Nat -> c10:c11 gen_c5:c612_12 :: Nat -> c5:c6 Lemmas: lt(gen_0':s9_12(n14_12), gen_0':s9_12(n14_12)) -> false, rt in Omega(0) inc(gen_0':s9_12(n398_12)) -> gen_0':s9_12(+(1, n398_12)), rt in Omega(0) LT(gen_0':s9_12(n694_12), gen_0':s9_12(n694_12)) -> gen_c7:c8:c910_12(n694_12), rt in Omega(1 + n694_12) Generator Equations: gen_0':s9_12(0) <=> 0' gen_0':s9_12(+(x, 1)) <=> s(gen_0':s9_12(x)) gen_c7:c8:c910_12(0) <=> c7 gen_c7:c8:c910_12(+(x, 1)) <=> c9(gen_c7:c8:c910_12(x)) gen_c10:c1111_12(0) <=> c10 gen_c10:c1111_12(+(x, 1)) <=> c11(gen_c10:c1111_12(x)) gen_c5:c612_12(0) <=> c5 gen_c5:c612_12(+(x, 1)) <=> c6(gen_c5:c612_12(x)) The following defined symbols remain to be analysed: INC, DIV, minus, MINUS, div They will be analysed ascendingly in the following order: INC < DIV minus < DIV MINUS < DIV minus < div ---------------------------------------- (87) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: INC(gen_0':s9_12(n1356_12)) -> gen_c10:c1111_12(n1356_12), rt in Omega(1 + n1356_12) Induction Base: INC(gen_0':s9_12(0)) ->_R^Omega(1) c10 Induction Step: INC(gen_0':s9_12(+(n1356_12, 1))) ->_R^Omega(1) c11(INC(gen_0':s9_12(n1356_12))) ->_IH c11(gen_c10:c1111_12(c1357_12)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (88) Obligation: Innermost TRS: Rules: DIVISION(z0, z1) -> c(DIV(z0, z1, 0')) DIV(z0, z1, z2) -> c1(IF(lt(z0, z1), z0, z1, inc(z2)), LT(z0, z1)) DIV(z0, z1, z2) -> c2(IF(lt(z0, z1), z0, z1, inc(z2)), INC(z2)) IF(true, z0, z1, z2) -> c3 IF(false, z0, s(z1), z2) -> c4(DIV(minus(z0, s(z1)), s(z1), z2), MINUS(z0, s(z1))) MINUS(z0, 0') -> c5 MINUS(s(z0), s(z1)) -> c6(MINUS(z0, z1)) LT(z0, 0') -> c7 LT(0', s(z0)) -> c8 LT(s(z0), s(z1)) -> c9(LT(z0, z1)) INC(0') -> c10 INC(s(z0)) -> c11(INC(z0)) division(z0, z1) -> div(z0, z1, 0') div(z0, z1, z2) -> if(lt(z0, z1), z0, z1, inc(z2)) if(true, z0, z1, z2) -> z2 if(false, z0, s(z1), z2) -> div(minus(z0, s(z1)), s(z1), z2) minus(z0, 0') -> z0 minus(s(z0), s(z1)) -> minus(z0, z1) lt(z0, 0') -> false lt(0', s(z0)) -> true lt(s(z0), s(z1)) -> lt(z0, z1) inc(0') -> s(0') inc(s(z0)) -> s(inc(z0)) Types: DIVISION :: 0':s -> 0':s -> c c :: c1:c2 -> c DIV :: 0':s -> 0':s -> 0':s -> c1:c2 0' :: 0':s c1 :: c3:c4 -> c7:c8:c9 -> c1:c2 IF :: true:false -> 0':s -> 0':s -> 0':s -> c3:c4 lt :: 0':s -> 0':s -> true:false inc :: 0':s -> 0':s LT :: 0':s -> 0':s -> c7:c8:c9 c2 :: c3:c4 -> c10:c11 -> c1:c2 INC :: 0':s -> c10:c11 true :: true:false c3 :: c3:c4 false :: true:false s :: 0':s -> 0':s c4 :: c1:c2 -> c5:c6 -> c3:c4 minus :: 0':s -> 0':s -> 0':s MINUS :: 0':s -> 0':s -> c5:c6 c5 :: c5:c6 c6 :: c5:c6 -> c5:c6 c7 :: c7:c8:c9 c8 :: c7:c8:c9 c9 :: c7:c8:c9 -> c7:c8:c9 c10 :: c10:c11 c11 :: c10:c11 -> c10:c11 division :: 0':s -> 0':s -> 0':s div :: 0':s -> 0':s -> 0':s -> 0':s if :: true:false -> 0':s -> 0':s -> 0':s -> 0':s hole_c1_12 :: c hole_0':s2_12 :: 0':s hole_c1:c23_12 :: c1:c2 hole_c3:c44_12 :: c3:c4 hole_c7:c8:c95_12 :: c7:c8:c9 hole_true:false6_12 :: true:false hole_c10:c117_12 :: c10:c11 hole_c5:c68_12 :: c5:c6 gen_0':s9_12 :: Nat -> 0':s gen_c7:c8:c910_12 :: Nat -> c7:c8:c9 gen_c10:c1111_12 :: Nat -> c10:c11 gen_c5:c612_12 :: Nat -> c5:c6 Lemmas: lt(gen_0':s9_12(n14_12), gen_0':s9_12(n14_12)) -> false, rt in Omega(0) inc(gen_0':s9_12(n398_12)) -> gen_0':s9_12(+(1, n398_12)), rt in Omega(0) LT(gen_0':s9_12(n694_12), gen_0':s9_12(n694_12)) -> gen_c7:c8:c910_12(n694_12), rt in Omega(1 + n694_12) INC(gen_0':s9_12(n1356_12)) -> gen_c10:c1111_12(n1356_12), rt in Omega(1 + n1356_12) Generator Equations: gen_0':s9_12(0) <=> 0' gen_0':s9_12(+(x, 1)) <=> s(gen_0':s9_12(x)) gen_c7:c8:c910_12(0) <=> c7 gen_c7:c8:c910_12(+(x, 1)) <=> c9(gen_c7:c8:c910_12(x)) gen_c10:c1111_12(0) <=> c10 gen_c10:c1111_12(+(x, 1)) <=> c11(gen_c10:c1111_12(x)) gen_c5:c612_12(0) <=> c5 gen_c5:c612_12(+(x, 1)) <=> c6(gen_c5:c612_12(x)) The following defined symbols remain to be analysed: minus, DIV, MINUS, div They will be analysed ascendingly in the following order: minus < DIV MINUS < DIV minus < div ---------------------------------------- (89) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: minus(gen_0':s9_12(n1724_12), gen_0':s9_12(n1724_12)) -> gen_0':s9_12(0), rt in Omega(0) Induction Base: minus(gen_0':s9_12(0), gen_0':s9_12(0)) ->_R^Omega(0) gen_0':s9_12(0) Induction Step: minus(gen_0':s9_12(+(n1724_12, 1)), gen_0':s9_12(+(n1724_12, 1))) ->_R^Omega(0) minus(gen_0':s9_12(n1724_12), gen_0':s9_12(n1724_12)) ->_IH gen_0':s9_12(0) We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (90) Obligation: Innermost TRS: Rules: DIVISION(z0, z1) -> c(DIV(z0, z1, 0')) DIV(z0, z1, z2) -> c1(IF(lt(z0, z1), z0, z1, inc(z2)), LT(z0, z1)) DIV(z0, z1, z2) -> c2(IF(lt(z0, z1), z0, z1, inc(z2)), INC(z2)) IF(true, z0, z1, z2) -> c3 IF(false, z0, s(z1), z2) -> c4(DIV(minus(z0, s(z1)), s(z1), z2), MINUS(z0, s(z1))) MINUS(z0, 0') -> c5 MINUS(s(z0), s(z1)) -> c6(MINUS(z0, z1)) LT(z0, 0') -> c7 LT(0', s(z0)) -> c8 LT(s(z0), s(z1)) -> c9(LT(z0, z1)) INC(0') -> c10 INC(s(z0)) -> c11(INC(z0)) division(z0, z1) -> div(z0, z1, 0') div(z0, z1, z2) -> if(lt(z0, z1), z0, z1, inc(z2)) if(true, z0, z1, z2) -> z2 if(false, z0, s(z1), z2) -> div(minus(z0, s(z1)), s(z1), z2) minus(z0, 0') -> z0 minus(s(z0), s(z1)) -> minus(z0, z1) lt(z0, 0') -> false lt(0', s(z0)) -> true lt(s(z0), s(z1)) -> lt(z0, z1) inc(0') -> s(0') inc(s(z0)) -> s(inc(z0)) Types: DIVISION :: 0':s -> 0':s -> c c :: c1:c2 -> c DIV :: 0':s -> 0':s -> 0':s -> c1:c2 0' :: 0':s c1 :: c3:c4 -> c7:c8:c9 -> c1:c2 IF :: true:false -> 0':s -> 0':s -> 0':s -> c3:c4 lt :: 0':s -> 0':s -> true:false inc :: 0':s -> 0':s LT :: 0':s -> 0':s -> c7:c8:c9 c2 :: c3:c4 -> c10:c11 -> c1:c2 INC :: 0':s -> c10:c11 true :: true:false c3 :: c3:c4 false :: true:false s :: 0':s -> 0':s c4 :: c1:c2 -> c5:c6 -> c3:c4 minus :: 0':s -> 0':s -> 0':s MINUS :: 0':s -> 0':s -> c5:c6 c5 :: c5:c6 c6 :: c5:c6 -> c5:c6 c7 :: c7:c8:c9 c8 :: c7:c8:c9 c9 :: c7:c8:c9 -> c7:c8:c9 c10 :: c10:c11 c11 :: c10:c11 -> c10:c11 division :: 0':s -> 0':s -> 0':s div :: 0':s -> 0':s -> 0':s -> 0':s if :: true:false -> 0':s -> 0':s -> 0':s -> 0':s hole_c1_12 :: c hole_0':s2_12 :: 0':s hole_c1:c23_12 :: c1:c2 hole_c3:c44_12 :: c3:c4 hole_c7:c8:c95_12 :: c7:c8:c9 hole_true:false6_12 :: true:false hole_c10:c117_12 :: c10:c11 hole_c5:c68_12 :: c5:c6 gen_0':s9_12 :: Nat -> 0':s gen_c7:c8:c910_12 :: Nat -> c7:c8:c9 gen_c10:c1111_12 :: Nat -> c10:c11 gen_c5:c612_12 :: Nat -> c5:c6 Lemmas: lt(gen_0':s9_12(n14_12), gen_0':s9_12(n14_12)) -> false, rt in Omega(0) inc(gen_0':s9_12(n398_12)) -> gen_0':s9_12(+(1, n398_12)), rt in Omega(0) LT(gen_0':s9_12(n694_12), gen_0':s9_12(n694_12)) -> gen_c7:c8:c910_12(n694_12), rt in Omega(1 + n694_12) INC(gen_0':s9_12(n1356_12)) -> gen_c10:c1111_12(n1356_12), rt in Omega(1 + n1356_12) minus(gen_0':s9_12(n1724_12), gen_0':s9_12(n1724_12)) -> gen_0':s9_12(0), rt in Omega(0) Generator Equations: gen_0':s9_12(0) <=> 0' gen_0':s9_12(+(x, 1)) <=> s(gen_0':s9_12(x)) gen_c7:c8:c910_12(0) <=> c7 gen_c7:c8:c910_12(+(x, 1)) <=> c9(gen_c7:c8:c910_12(x)) gen_c10:c1111_12(0) <=> c10 gen_c10:c1111_12(+(x, 1)) <=> c11(gen_c10:c1111_12(x)) gen_c5:c612_12(0) <=> c5 gen_c5:c612_12(+(x, 1)) <=> c6(gen_c5:c612_12(x)) The following defined symbols remain to be analysed: MINUS, DIV, div They will be analysed ascendingly in the following order: MINUS < DIV ---------------------------------------- (91) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: MINUS(gen_0':s9_12(n2396_12), gen_0':s9_12(n2396_12)) -> gen_c5:c612_12(n2396_12), rt in Omega(1 + n2396_12) Induction Base: MINUS(gen_0':s9_12(0), gen_0':s9_12(0)) ->_R^Omega(1) c5 Induction Step: MINUS(gen_0':s9_12(+(n2396_12, 1)), gen_0':s9_12(+(n2396_12, 1))) ->_R^Omega(1) c6(MINUS(gen_0':s9_12(n2396_12), gen_0':s9_12(n2396_12))) ->_IH c6(gen_c5:c612_12(c2397_12)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (92) Obligation: Innermost TRS: Rules: DIVISION(z0, z1) -> c(DIV(z0, z1, 0')) DIV(z0, z1, z2) -> c1(IF(lt(z0, z1), z0, z1, inc(z2)), LT(z0, z1)) DIV(z0, z1, z2) -> c2(IF(lt(z0, z1), z0, z1, inc(z2)), INC(z2)) IF(true, z0, z1, z2) -> c3 IF(false, z0, s(z1), z2) -> c4(DIV(minus(z0, s(z1)), s(z1), z2), MINUS(z0, s(z1))) MINUS(z0, 0') -> c5 MINUS(s(z0), s(z1)) -> c6(MINUS(z0, z1)) LT(z0, 0') -> c7 LT(0', s(z0)) -> c8 LT(s(z0), s(z1)) -> c9(LT(z0, z1)) INC(0') -> c10 INC(s(z0)) -> c11(INC(z0)) division(z0, z1) -> div(z0, z1, 0') div(z0, z1, z2) -> if(lt(z0, z1), z0, z1, inc(z2)) if(true, z0, z1, z2) -> z2 if(false, z0, s(z1), z2) -> div(minus(z0, s(z1)), s(z1), z2) minus(z0, 0') -> z0 minus(s(z0), s(z1)) -> minus(z0, z1) lt(z0, 0') -> false lt(0', s(z0)) -> true lt(s(z0), s(z1)) -> lt(z0, z1) inc(0') -> s(0') inc(s(z0)) -> s(inc(z0)) Types: DIVISION :: 0':s -> 0':s -> c c :: c1:c2 -> c DIV :: 0':s -> 0':s -> 0':s -> c1:c2 0' :: 0':s c1 :: c3:c4 -> c7:c8:c9 -> c1:c2 IF :: true:false -> 0':s -> 0':s -> 0':s -> c3:c4 lt :: 0':s -> 0':s -> true:false inc :: 0':s -> 0':s LT :: 0':s -> 0':s -> c7:c8:c9 c2 :: c3:c4 -> c10:c11 -> c1:c2 INC :: 0':s -> c10:c11 true :: true:false c3 :: c3:c4 false :: true:false s :: 0':s -> 0':s c4 :: c1:c2 -> c5:c6 -> c3:c4 minus :: 0':s -> 0':s -> 0':s MINUS :: 0':s -> 0':s -> c5:c6 c5 :: c5:c6 c6 :: c5:c6 -> c5:c6 c7 :: c7:c8:c9 c8 :: c7:c8:c9 c9 :: c7:c8:c9 -> c7:c8:c9 c10 :: c10:c11 c11 :: c10:c11 -> c10:c11 division :: 0':s -> 0':s -> 0':s div :: 0':s -> 0':s -> 0':s -> 0':s if :: true:false -> 0':s -> 0':s -> 0':s -> 0':s hole_c1_12 :: c hole_0':s2_12 :: 0':s hole_c1:c23_12 :: c1:c2 hole_c3:c44_12 :: c3:c4 hole_c7:c8:c95_12 :: c7:c8:c9 hole_true:false6_12 :: true:false hole_c10:c117_12 :: c10:c11 hole_c5:c68_12 :: c5:c6 gen_0':s9_12 :: Nat -> 0':s gen_c7:c8:c910_12 :: Nat -> c7:c8:c9 gen_c10:c1111_12 :: Nat -> c10:c11 gen_c5:c612_12 :: Nat -> c5:c6 Lemmas: lt(gen_0':s9_12(n14_12), gen_0':s9_12(n14_12)) -> false, rt in Omega(0) inc(gen_0':s9_12(n398_12)) -> gen_0':s9_12(+(1, n398_12)), rt in Omega(0) LT(gen_0':s9_12(n694_12), gen_0':s9_12(n694_12)) -> gen_c7:c8:c910_12(n694_12), rt in Omega(1 + n694_12) INC(gen_0':s9_12(n1356_12)) -> gen_c10:c1111_12(n1356_12), rt in Omega(1 + n1356_12) minus(gen_0':s9_12(n1724_12), gen_0':s9_12(n1724_12)) -> gen_0':s9_12(0), rt in Omega(0) MINUS(gen_0':s9_12(n2396_12), gen_0':s9_12(n2396_12)) -> gen_c5:c612_12(n2396_12), rt in Omega(1 + n2396_12) Generator Equations: gen_0':s9_12(0) <=> 0' gen_0':s9_12(+(x, 1)) <=> s(gen_0':s9_12(x)) gen_c7:c8:c910_12(0) <=> c7 gen_c7:c8:c910_12(+(x, 1)) <=> c9(gen_c7:c8:c910_12(x)) gen_c10:c1111_12(0) <=> c10 gen_c10:c1111_12(+(x, 1)) <=> c11(gen_c10:c1111_12(x)) gen_c5:c612_12(0) <=> c5 gen_c5:c612_12(+(x, 1)) <=> c6(gen_c5:c612_12(x)) The following defined symbols remain to be analysed: DIV, div