WORST_CASE(?,O(n^2)) proof of input_VjAlc02pIe.trs # AProVE Commit ID: 5b976082cb74a395683ed8cc7acf94bd611ab29f fuhs 20230524 unpublished The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2). (0) CpxTRS (1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (2) CdtProblem (3) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (4) CdtProblem (5) CdtGraphSplitRhsProof [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) CpxWeightedTrsRenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (12) CpxWeightedTrs (13) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (14) CpxTypedWeightedTrs (15) CompletionProof [UPPER BOUND(ID), 0 ms] (16) CpxTypedWeightedCompleteTrs (17) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (18) CpxTypedWeightedCompleteTrs (19) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (20) CpxRNTS (21) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms] (22) CpxRNTS (23) CpxRntsAnalysisOrderProof [BOTH BOUNDS(ID, ID), 0 ms] (24) CpxRNTS (25) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (26) CpxRNTS (27) IntTrsBoundProof [UPPER BOUND(ID), 200 ms] (28) CpxRNTS (29) IntTrsBoundProof [UPPER BOUND(ID), 24 ms] (30) CpxRNTS (31) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (32) CpxRNTS (33) IntTrsBoundProof [UPPER BOUND(ID), 116 ms] (34) CpxRNTS (35) IntTrsBoundProof [UPPER BOUND(ID), 32 ms] (36) CpxRNTS (37) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (38) CpxRNTS (39) IntTrsBoundProof [UPPER BOUND(ID), 88 ms] (40) CpxRNTS (41) IntTrsBoundProof [UPPER BOUND(ID), 62 ms] (42) CpxRNTS (43) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (44) CpxRNTS (45) IntTrsBoundProof [UPPER BOUND(ID), 331 ms] (46) CpxRNTS (47) IntTrsBoundProof [UPPER BOUND(ID), 73 ms] (48) CpxRNTS (49) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (50) CpxRNTS (51) IntTrsBoundProof [UPPER BOUND(ID), 2041 ms] (52) CpxRNTS (53) IntTrsBoundProof [UPPER BOUND(ID), 265 ms] (54) CpxRNTS (55) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (56) CpxRNTS (57) IntTrsBoundProof [UPPER BOUND(ID), 2896 ms] (58) CpxRNTS (59) IntTrsBoundProof [UPPER BOUND(ID), 1232 ms] (60) CpxRNTS (61) FinalProof [FINISHED, 0 ms] (62) BOUNDS(1, n^2) ---------------------------------------- (0) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2). The TRS R consists of the following rules: sqr(0) -> 0 sqr(s(x)) -> +(sqr(x), s(double(x))) double(0) -> 0 double(s(x)) -> s(s(double(x))) +(x, 0) -> x +(x, s(y)) -> s(+(x, y)) sqr(s(x)) -> s(+(sqr(x), double(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: sqr(0) -> 0 sqr(s(z0)) -> +(sqr(z0), s(double(z0))) sqr(s(z0)) -> s(+(sqr(z0), double(z0))) double(0) -> 0 double(s(z0)) -> s(s(double(z0))) +(z0, 0) -> z0 +(z0, s(z1)) -> s(+(z0, z1)) Tuples: SQR(0) -> c SQR(s(z0)) -> c1(+'(sqr(z0), s(double(z0))), SQR(z0)) SQR(s(z0)) -> c2(+'(sqr(z0), s(double(z0))), DOUBLE(z0)) SQR(s(z0)) -> c3(+'(sqr(z0), double(z0)), SQR(z0)) SQR(s(z0)) -> c4(+'(sqr(z0), double(z0)), DOUBLE(z0)) DOUBLE(0) -> c5 DOUBLE(s(z0)) -> c6(DOUBLE(z0)) +'(z0, 0) -> c7 +'(z0, s(z1)) -> c8(+'(z0, z1)) S tuples: SQR(0) -> c SQR(s(z0)) -> c1(+'(sqr(z0), s(double(z0))), SQR(z0)) SQR(s(z0)) -> c2(+'(sqr(z0), s(double(z0))), DOUBLE(z0)) SQR(s(z0)) -> c3(+'(sqr(z0), double(z0)), SQR(z0)) SQR(s(z0)) -> c4(+'(sqr(z0), double(z0)), DOUBLE(z0)) DOUBLE(0) -> c5 DOUBLE(s(z0)) -> c6(DOUBLE(z0)) +'(z0, 0) -> c7 +'(z0, s(z1)) -> c8(+'(z0, z1)) K tuples:none Defined Rule Symbols: sqr_1, double_1, +_2 Defined Pair Symbols: SQR_1, DOUBLE_1, +'_2 Compound Symbols: c, c1_2, c2_2, c3_2, c4_2, c5, c6_1, c7, c8_1 ---------------------------------------- (3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 3 trailing nodes: +'(z0, 0) -> c7 SQR(0) -> c DOUBLE(0) -> c5 ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: sqr(0) -> 0 sqr(s(z0)) -> +(sqr(z0), s(double(z0))) sqr(s(z0)) -> s(+(sqr(z0), double(z0))) double(0) -> 0 double(s(z0)) -> s(s(double(z0))) +(z0, 0) -> z0 +(z0, s(z1)) -> s(+(z0, z1)) Tuples: SQR(s(z0)) -> c1(+'(sqr(z0), s(double(z0))), SQR(z0)) SQR(s(z0)) -> c2(+'(sqr(z0), s(double(z0))), DOUBLE(z0)) SQR(s(z0)) -> c3(+'(sqr(z0), double(z0)), SQR(z0)) SQR(s(z0)) -> c4(+'(sqr(z0), double(z0)), DOUBLE(z0)) DOUBLE(s(z0)) -> c6(DOUBLE(z0)) +'(z0, s(z1)) -> c8(+'(z0, z1)) S tuples: SQR(s(z0)) -> c1(+'(sqr(z0), s(double(z0))), SQR(z0)) SQR(s(z0)) -> c2(+'(sqr(z0), s(double(z0))), DOUBLE(z0)) SQR(s(z0)) -> c3(+'(sqr(z0), double(z0)), SQR(z0)) SQR(s(z0)) -> c4(+'(sqr(z0), double(z0)), DOUBLE(z0)) DOUBLE(s(z0)) -> c6(DOUBLE(z0)) +'(z0, s(z1)) -> c8(+'(z0, z1)) K tuples:none Defined Rule Symbols: sqr_1, double_1, +_2 Defined Pair Symbols: SQR_1, DOUBLE_1, +'_2 Compound Symbols: c1_2, c2_2, c3_2, c4_2, c6_1, c8_1 ---------------------------------------- (5) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID)) Split RHS of tuples not part of any SCC ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: sqr(0) -> 0 sqr(s(z0)) -> +(sqr(z0), s(double(z0))) sqr(s(z0)) -> s(+(sqr(z0), double(z0))) double(0) -> 0 double(s(z0)) -> s(s(double(z0))) +(z0, 0) -> z0 +(z0, s(z1)) -> s(+(z0, z1)) Tuples: SQR(s(z0)) -> c1(+'(sqr(z0), s(double(z0))), SQR(z0)) SQR(s(z0)) -> c3(+'(sqr(z0), double(z0)), SQR(z0)) DOUBLE(s(z0)) -> c6(DOUBLE(z0)) +'(z0, s(z1)) -> c8(+'(z0, z1)) SQR(s(z0)) -> c(+'(sqr(z0), s(double(z0)))) SQR(s(z0)) -> c(DOUBLE(z0)) SQR(s(z0)) -> c(+'(sqr(z0), double(z0))) S tuples: SQR(s(z0)) -> c1(+'(sqr(z0), s(double(z0))), SQR(z0)) SQR(s(z0)) -> c3(+'(sqr(z0), double(z0)), SQR(z0)) DOUBLE(s(z0)) -> c6(DOUBLE(z0)) +'(z0, s(z1)) -> c8(+'(z0, z1)) SQR(s(z0)) -> c(+'(sqr(z0), s(double(z0)))) SQR(s(z0)) -> c(DOUBLE(z0)) SQR(s(z0)) -> c(+'(sqr(z0), double(z0))) K tuples:none Defined Rule Symbols: sqr_1, double_1, +_2 Defined Pair Symbols: SQR_1, DOUBLE_1, +'_2 Compound Symbols: c1_2, c3_2, c6_1, c8_1, c_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: SQR(s(z0)) -> c1(+'(sqr(z0), s(double(z0))), SQR(z0)) SQR(s(z0)) -> c3(+'(sqr(z0), double(z0)), SQR(z0)) DOUBLE(s(z0)) -> c6(DOUBLE(z0)) +'(z0, s(z1)) -> c8(+'(z0, z1)) SQR(s(z0)) -> c(+'(sqr(z0), s(double(z0)))) SQR(s(z0)) -> c(DOUBLE(z0)) SQR(s(z0)) -> c(+'(sqr(z0), double(z0))) The (relative) TRS S consists of the following rules: sqr(0) -> 0 sqr(s(z0)) -> +(sqr(z0), s(double(z0))) sqr(s(z0)) -> s(+(sqr(z0), double(z0))) double(0) -> 0 double(s(z0)) -> s(s(double(z0))) +(z0, 0) -> z0 +(z0, s(z1)) -> s(+(z0, z1)) 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: SQR(s(z0)) -> c1(+'(sqr(z0), s(double(z0))), SQR(z0)) [1] SQR(s(z0)) -> c3(+'(sqr(z0), double(z0)), SQR(z0)) [1] DOUBLE(s(z0)) -> c6(DOUBLE(z0)) [1] +'(z0, s(z1)) -> c8(+'(z0, z1)) [1] SQR(s(z0)) -> c(+'(sqr(z0), s(double(z0)))) [1] SQR(s(z0)) -> c(DOUBLE(z0)) [1] SQR(s(z0)) -> c(+'(sqr(z0), double(z0))) [1] sqr(0) -> 0 [0] sqr(s(z0)) -> +(sqr(z0), s(double(z0))) [0] sqr(s(z0)) -> s(+(sqr(z0), double(z0))) [0] double(0) -> 0 [0] double(s(z0)) -> s(s(double(z0))) [0] +(z0, 0) -> z0 [0] +(z0, s(z1)) -> s(+(z0, z1)) [0] Rewrite Strategy: INNERMOST ---------------------------------------- (11) CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID)) Renamed defined symbols to avoid conflicts with arithmetic symbols: + => plus ---------------------------------------- (12) 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: SQR(s(z0)) -> c1(+'(sqr(z0), s(double(z0))), SQR(z0)) [1] SQR(s(z0)) -> c3(+'(sqr(z0), double(z0)), SQR(z0)) [1] DOUBLE(s(z0)) -> c6(DOUBLE(z0)) [1] +'(z0, s(z1)) -> c8(+'(z0, z1)) [1] SQR(s(z0)) -> c(+'(sqr(z0), s(double(z0)))) [1] SQR(s(z0)) -> c(DOUBLE(z0)) [1] SQR(s(z0)) -> c(+'(sqr(z0), double(z0))) [1] sqr(0) -> 0 [0] sqr(s(z0)) -> plus(sqr(z0), s(double(z0))) [0] sqr(s(z0)) -> s(plus(sqr(z0), double(z0))) [0] double(0) -> 0 [0] double(s(z0)) -> s(s(double(z0))) [0] plus(z0, 0) -> z0 [0] plus(z0, s(z1)) -> s(plus(z0, z1)) [0] Rewrite Strategy: INNERMOST ---------------------------------------- (13) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (14) Obligation: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: SQR(s(z0)) -> c1(+'(sqr(z0), s(double(z0))), SQR(z0)) [1] SQR(s(z0)) -> c3(+'(sqr(z0), double(z0)), SQR(z0)) [1] DOUBLE(s(z0)) -> c6(DOUBLE(z0)) [1] +'(z0, s(z1)) -> c8(+'(z0, z1)) [1] SQR(s(z0)) -> c(+'(sqr(z0), s(double(z0)))) [1] SQR(s(z0)) -> c(DOUBLE(z0)) [1] SQR(s(z0)) -> c(+'(sqr(z0), double(z0))) [1] sqr(0) -> 0 [0] sqr(s(z0)) -> plus(sqr(z0), s(double(z0))) [0] sqr(s(z0)) -> s(plus(sqr(z0), double(z0))) [0] double(0) -> 0 [0] double(s(z0)) -> s(s(double(z0))) [0] plus(z0, 0) -> z0 [0] plus(z0, s(z1)) -> s(plus(z0, z1)) [0] The TRS has the following type information: SQR :: s:0 -> c1:c3:c s :: s:0 -> s:0 c1 :: c6:c8 -> c1:c3:c -> c1:c3:c +' :: s:0 -> s:0 -> c6:c8 sqr :: s:0 -> s:0 double :: s:0 -> s:0 c3 :: c6:c8 -> c1:c3:c -> c1:c3:c DOUBLE :: s:0 -> c6:c8 c6 :: c6:c8 -> c6:c8 c8 :: c6:c8 -> c6:c8 c :: c6:c8 -> c1:c3:c 0 :: s:0 plus :: s:0 -> s:0 -> s:0 Rewrite Strategy: INNERMOST ---------------------------------------- (15) 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: SQR_1 DOUBLE_1 +'_2 (c) The following functions are completely defined: sqr_1 double_1 plus_2 Due to the following rules being added: sqr(v0) -> 0 [0] double(v0) -> 0 [0] plus(v0, v1) -> 0 [0] And the following fresh constants: const, const1 ---------------------------------------- (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: SQR(s(z0)) -> c1(+'(sqr(z0), s(double(z0))), SQR(z0)) [1] SQR(s(z0)) -> c3(+'(sqr(z0), double(z0)), SQR(z0)) [1] DOUBLE(s(z0)) -> c6(DOUBLE(z0)) [1] +'(z0, s(z1)) -> c8(+'(z0, z1)) [1] SQR(s(z0)) -> c(+'(sqr(z0), s(double(z0)))) [1] SQR(s(z0)) -> c(DOUBLE(z0)) [1] SQR(s(z0)) -> c(+'(sqr(z0), double(z0))) [1] sqr(0) -> 0 [0] sqr(s(z0)) -> plus(sqr(z0), s(double(z0))) [0] sqr(s(z0)) -> s(plus(sqr(z0), double(z0))) [0] double(0) -> 0 [0] double(s(z0)) -> s(s(double(z0))) [0] plus(z0, 0) -> z0 [0] plus(z0, s(z1)) -> s(plus(z0, z1)) [0] sqr(v0) -> 0 [0] double(v0) -> 0 [0] plus(v0, v1) -> 0 [0] The TRS has the following type information: SQR :: s:0 -> c1:c3:c s :: s:0 -> s:0 c1 :: c6:c8 -> c1:c3:c -> c1:c3:c +' :: s:0 -> s:0 -> c6:c8 sqr :: s:0 -> s:0 double :: s:0 -> s:0 c3 :: c6:c8 -> c1:c3:c -> c1:c3:c DOUBLE :: s:0 -> c6:c8 c6 :: c6:c8 -> c6:c8 c8 :: c6:c8 -> c6:c8 c :: c6:c8 -> c1:c3:c 0 :: s:0 plus :: s:0 -> s:0 -> s:0 const :: c1:c3:c const1 :: c6:c8 Rewrite Strategy: INNERMOST ---------------------------------------- (17) NarrowingProof (BOTH BOUNDS(ID, ID)) Narrowed the inner basic terms of all right-hand sides by a single narrowing step. ---------------------------------------- (18) 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: SQR(s(0)) -> c1(+'(0, s(0)), SQR(0)) [1] SQR(s(0)) -> c1(+'(0, s(0)), SQR(0)) [1] SQR(s(s(z0'))) -> c1(+'(plus(sqr(z0'), s(double(z0'))), s(s(s(double(z0'))))), SQR(s(z0'))) [1] SQR(s(s(z0'))) -> c1(+'(plus(sqr(z0'), s(double(z0'))), s(0)), SQR(s(z0'))) [1] SQR(s(s(z0''))) -> c1(+'(s(plus(sqr(z0''), double(z0''))), s(s(s(double(z0''))))), SQR(s(z0''))) [1] SQR(s(s(z0''))) -> c1(+'(s(plus(sqr(z0''), double(z0''))), s(0)), SQR(s(z0''))) [1] SQR(s(0)) -> c1(+'(0, s(0)), SQR(0)) [1] SQR(s(s(z01))) -> c1(+'(0, s(s(s(double(z01))))), SQR(s(z01))) [1] SQR(s(z0)) -> c1(+'(0, s(0)), SQR(z0)) [1] SQR(s(0)) -> c3(+'(0, 0), SQR(0)) [1] SQR(s(0)) -> c3(+'(0, 0), SQR(0)) [1] SQR(s(s(z02))) -> c3(+'(plus(sqr(z02), s(double(z02))), s(s(double(z02)))), SQR(s(z02))) [1] SQR(s(s(z02))) -> c3(+'(plus(sqr(z02), s(double(z02))), 0), SQR(s(z02))) [1] SQR(s(s(z03))) -> c3(+'(s(plus(sqr(z03), double(z03))), s(s(double(z03)))), SQR(s(z03))) [1] SQR(s(s(z03))) -> c3(+'(s(plus(sqr(z03), double(z03))), 0), SQR(s(z03))) [1] SQR(s(0)) -> c3(+'(0, 0), SQR(0)) [1] SQR(s(s(z04))) -> c3(+'(0, s(s(double(z04)))), SQR(s(z04))) [1] SQR(s(z0)) -> c3(+'(0, 0), SQR(z0)) [1] DOUBLE(s(z0)) -> c6(DOUBLE(z0)) [1] +'(z0, s(z1)) -> c8(+'(z0, z1)) [1] SQR(s(0)) -> c(+'(0, s(0))) [1] SQR(s(0)) -> c(+'(0, s(0))) [1] SQR(s(s(z05))) -> c(+'(plus(sqr(z05), s(double(z05))), s(s(s(double(z05)))))) [1] SQR(s(s(z05))) -> c(+'(plus(sqr(z05), s(double(z05))), s(0))) [1] SQR(s(s(z06))) -> c(+'(s(plus(sqr(z06), double(z06))), s(s(s(double(z06)))))) [1] SQR(s(s(z06))) -> c(+'(s(plus(sqr(z06), double(z06))), s(0))) [1] SQR(s(0)) -> c(+'(0, s(0))) [1] SQR(s(s(z07))) -> c(+'(0, s(s(s(double(z07)))))) [1] SQR(s(z0)) -> c(+'(0, s(0))) [1] SQR(s(z0)) -> c(DOUBLE(z0)) [1] SQR(s(0)) -> c(+'(0, 0)) [1] SQR(s(0)) -> c(+'(0, 0)) [1] SQR(s(s(z08))) -> c(+'(plus(sqr(z08), s(double(z08))), s(s(double(z08))))) [1] SQR(s(s(z08))) -> c(+'(plus(sqr(z08), s(double(z08))), 0)) [1] SQR(s(s(z09))) -> c(+'(s(plus(sqr(z09), double(z09))), s(s(double(z09))))) [1] SQR(s(s(z09))) -> c(+'(s(plus(sqr(z09), double(z09))), 0)) [1] SQR(s(0)) -> c(+'(0, 0)) [1] SQR(s(s(z010))) -> c(+'(0, s(s(double(z010))))) [1] SQR(s(z0)) -> c(+'(0, 0)) [1] sqr(0) -> 0 [0] sqr(s(0)) -> plus(0, s(0)) [0] sqr(s(0)) -> plus(0, s(0)) [0] sqr(s(s(z011))) -> plus(plus(sqr(z011), s(double(z011))), s(s(s(double(z011))))) [0] sqr(s(s(z011))) -> plus(plus(sqr(z011), s(double(z011))), s(0)) [0] sqr(s(s(z012))) -> plus(s(plus(sqr(z012), double(z012))), s(s(s(double(z012))))) [0] sqr(s(s(z012))) -> plus(s(plus(sqr(z012), double(z012))), s(0)) [0] sqr(s(0)) -> plus(0, s(0)) [0] sqr(s(s(z013))) -> plus(0, s(s(s(double(z013))))) [0] sqr(s(z0)) -> plus(0, s(0)) [0] sqr(s(0)) -> s(plus(0, 0)) [0] sqr(s(0)) -> s(plus(0, 0)) [0] sqr(s(s(z014))) -> s(plus(plus(sqr(z014), s(double(z014))), s(s(double(z014))))) [0] sqr(s(s(z014))) -> s(plus(plus(sqr(z014), s(double(z014))), 0)) [0] sqr(s(s(z015))) -> s(plus(s(plus(sqr(z015), double(z015))), s(s(double(z015))))) [0] sqr(s(s(z015))) -> s(plus(s(plus(sqr(z015), double(z015))), 0)) [0] sqr(s(0)) -> s(plus(0, 0)) [0] sqr(s(s(z016))) -> s(plus(0, s(s(double(z016))))) [0] sqr(s(z0)) -> s(plus(0, 0)) [0] double(0) -> 0 [0] double(s(z0)) -> s(s(double(z0))) [0] plus(z0, 0) -> z0 [0] plus(z0, s(z1)) -> s(plus(z0, z1)) [0] sqr(v0) -> 0 [0] double(v0) -> 0 [0] plus(v0, v1) -> 0 [0] The TRS has the following type information: SQR :: s:0 -> c1:c3:c s :: s:0 -> s:0 c1 :: c6:c8 -> c1:c3:c -> c1:c3:c +' :: s:0 -> s:0 -> c6:c8 sqr :: s:0 -> s:0 double :: s:0 -> s:0 c3 :: c6:c8 -> c1:c3:c -> c1:c3:c DOUBLE :: s:0 -> c6:c8 c6 :: c6:c8 -> c6:c8 c8 :: c6:c8 -> c6:c8 c :: c6:c8 -> c1:c3:c 0 :: s:0 plus :: s:0 -> s:0 -> s:0 const :: c1:c3:c const1 :: c6:c8 Rewrite Strategy: INNERMOST ---------------------------------------- (19) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: 0 => 0 const => 0 const1 => 0 ---------------------------------------- (20) Obligation: Complexity RNTS consisting of the following rules: +'(z, z') -{ 1 }-> 1 + +'(z0, z1) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1 DOUBLE(z) -{ 1 }-> 1 + DOUBLE(z0) :|: z = 1 + z0, z0 >= 0 SQR(z) -{ 1 }-> 1 + DOUBLE(z0) :|: z = 1 + z0, z0 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z05), 1 + double(z05)), 1 + 0) :|: z05 >= 0, z = 1 + (1 + z05) SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z05), 1 + double(z05)), 1 + (1 + (1 + double(z05)))) :|: z05 >= 0, z = 1 + (1 + z05) SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z08), 1 + double(z08)), 0) :|: z08 >= 0, z = 1 + (1 + z08) SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z08), 1 + double(z08)), 1 + (1 + double(z08))) :|: z08 >= 0, z = 1 + (1 + z08) SQR(z) -{ 1 }-> 1 + +'(0, 0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) :|: z = 1 + z0, z0 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) :|: z = 1 + z0, z0 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + double(z010))) :|: z = 1 + (1 + z010), z010 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + (1 + double(z07)))) :|: z = 1 + (1 + z07), z07 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z06), double(z06)), 1 + 0) :|: z06 >= 0, z = 1 + (1 + z06) SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z06), double(z06)), 1 + (1 + (1 + double(z06)))) :|: z06 >= 0, z = 1 + (1 + z06) SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z09), double(z09)), 0) :|: z = 1 + (1 + z09), z09 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z09), double(z09)), 1 + (1 + double(z09))) :|: z = 1 + (1 + z09), z09 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z0'), 1 + double(z0')), 1 + 0) + SQR(1 + z0') :|: z = 1 + (1 + z0'), z0' >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z0'), 1 + double(z0')), 1 + (1 + (1 + double(z0')))) + SQR(1 + z0') :|: z = 1 + (1 + z0'), z0' >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z02), 1 + double(z02)), 0) + SQR(1 + z02) :|: z = 1 + (1 + z02), z02 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z02), 1 + double(z02)), 1 + (1 + double(z02))) + SQR(1 + z02) :|: z = 1 + (1 + z02), z02 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) + SQR(z0) :|: z = 1 + z0, z0 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) + SQR(0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) + SQR(z0) :|: z = 1 + z0, z0 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) + SQR(0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + double(z04))) + SQR(1 + z04) :|: z04 >= 0, z = 1 + (1 + z04) SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + (1 + double(z01)))) + SQR(1 + z01) :|: z = 1 + (1 + z01), z01 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z0''), double(z0'')), 1 + 0) + SQR(1 + z0'') :|: z = 1 + (1 + z0''), z0'' >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z0''), double(z0'')), 1 + (1 + (1 + double(z0'')))) + SQR(1 + z0'') :|: z = 1 + (1 + z0''), z0'' >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z03), double(z03)), 0) + SQR(1 + z03) :|: z = 1 + (1 + z03), z03 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z03), double(z03)), 1 + (1 + double(z03))) + SQR(1 + z03) :|: z = 1 + (1 + z03), z03 >= 0 double(z) -{ 0 }-> 0 :|: z = 0 double(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 double(z) -{ 0 }-> 1 + (1 + double(z0)) :|: z = 1 + z0, z0 >= 0 plus(z, z') -{ 0 }-> z0 :|: z = z0, z0 >= 0, z' = 0 plus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 plus(z, z') -{ 0 }-> 1 + plus(z0, z1) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1 sqr(z) -{ 0 }-> plus(plus(sqr(z011), 1 + double(z011)), 1 + 0) :|: z = 1 + (1 + z011), z011 >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z011), 1 + double(z011)), 1 + (1 + (1 + double(z011)))) :|: z = 1 + (1 + z011), z011 >= 0 sqr(z) -{ 0 }-> plus(0, 1 + 0) :|: z = 1 + 0 sqr(z) -{ 0 }-> plus(0, 1 + 0) :|: z = 1 + z0, z0 >= 0 sqr(z) -{ 0 }-> plus(0, 1 + (1 + (1 + double(z013)))) :|: z013 >= 0, z = 1 + (1 + z013) sqr(z) -{ 0 }-> plus(1 + plus(sqr(z012), double(z012)), 1 + 0) :|: z012 >= 0, z = 1 + (1 + z012) sqr(z) -{ 0 }-> plus(1 + plus(sqr(z012), double(z012)), 1 + (1 + (1 + double(z012)))) :|: z012 >= 0, z = 1 + (1 + z012) sqr(z) -{ 0 }-> 0 :|: z = 0 sqr(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z014), 1 + double(z014)), 0) :|: z = 1 + (1 + z014), z014 >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z014), 1 + double(z014)), 1 + (1 + double(z014))) :|: z = 1 + (1 + z014), z014 >= 0 sqr(z) -{ 0 }-> 1 + plus(0, 0) :|: z = 1 + 0 sqr(z) -{ 0 }-> 1 + plus(0, 0) :|: z = 1 + z0, z0 >= 0 sqr(z) -{ 0 }-> 1 + plus(0, 1 + (1 + double(z016))) :|: z016 >= 0, z = 1 + (1 + z016) sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z015), double(z015)), 0) :|: z015 >= 0, z = 1 + (1 + z015) sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z015), double(z015)), 1 + (1 + double(z015))) :|: z015 >= 0, z = 1 + (1 + z015) ---------------------------------------- (21) SimplificationProof (BOTH BOUNDS(ID, ID)) Simplified the RNTS by moving equalities from the constraints into the right-hand sides. ---------------------------------------- (22) Obligation: Complexity RNTS consisting of the following rules: +'(z, z') -{ 1 }-> 1 + +'(z, z' - 1) :|: z' - 1 >= 0, z >= 0 DOUBLE(z) -{ 1 }-> 1 + DOUBLE(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + DOUBLE(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 0) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 1 + 0) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 1 + (1 + double(z - 2))) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 1 + (1 + (1 + double(z - 2)))) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + double(z - 2))) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + (1 + double(z - 2)))) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 0) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 1 + 0) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 1 + (1 + double(z - 2))) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 1 + (1 + (1 + double(z - 2)))) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 0) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 1 + 0) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 1 + (1 + double(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 1 + (1 + (1 + double(z - 2)))) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) + SQR(0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) + SQR(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) + SQR(0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) + SQR(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + double(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + (1 + double(z - 2)))) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 0) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 1 + 0) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 1 + (1 + double(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 1 + (1 + (1 + double(z - 2)))) + SQR(1 + (z - 2)) :|: z - 2 >= 0 double(z) -{ 0 }-> 0 :|: z = 0 double(z) -{ 0 }-> 0 :|: z >= 0 double(z) -{ 0 }-> 1 + (1 + double(z - 1)) :|: z - 1 >= 0 plus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 plus(z, z') -{ 0 }-> 1 + plus(z, z' - 1) :|: z' - 1 >= 0, z >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + double(z - 2)), 1 + 0) :|: z - 2 >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + double(z - 2)), 1 + (1 + (1 + double(z - 2)))) :|: z - 2 >= 0 sqr(z) -{ 0 }-> plus(0, 1 + 0) :|: z = 1 + 0 sqr(z) -{ 0 }-> plus(0, 1 + 0) :|: z - 1 >= 0 sqr(z) -{ 0 }-> plus(0, 1 + (1 + (1 + double(z - 2)))) :|: z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), double(z - 2)), 1 + 0) :|: z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), double(z - 2)), 1 + (1 + (1 + double(z - 2)))) :|: z - 2 >= 0 sqr(z) -{ 0 }-> 0 :|: z = 0 sqr(z) -{ 0 }-> 0 :|: z >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + double(z - 2)), 0) :|: z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + double(z - 2)), 1 + (1 + double(z - 2))) :|: z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(0, 0) :|: z = 1 + 0 sqr(z) -{ 0 }-> 1 + plus(0, 0) :|: z - 1 >= 0 sqr(z) -{ 0 }-> 1 + plus(0, 1 + (1 + double(z - 2))) :|: z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), double(z - 2)), 0) :|: z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), double(z - 2)), 1 + (1 + double(z - 2))) :|: z - 2 >= 0 ---------------------------------------- (23) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID)) Found the following analysis order by SCC decomposition: { double } { DOUBLE } { +' } { plus } { sqr } { SQR } ---------------------------------------- (24) Obligation: Complexity RNTS consisting of the following rules: +'(z, z') -{ 1 }-> 1 + +'(z, z' - 1) :|: z' - 1 >= 0, z >= 0 DOUBLE(z) -{ 1 }-> 1 + DOUBLE(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + DOUBLE(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 0) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 1 + 0) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 1 + (1 + double(z - 2))) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 1 + (1 + (1 + double(z - 2)))) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + double(z - 2))) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + (1 + double(z - 2)))) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 0) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 1 + 0) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 1 + (1 + double(z - 2))) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 1 + (1 + (1 + double(z - 2)))) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 0) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 1 + 0) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 1 + (1 + double(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 1 + (1 + (1 + double(z - 2)))) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) + SQR(0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) + SQR(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) + SQR(0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) + SQR(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + double(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + (1 + double(z - 2)))) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 0) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 1 + 0) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 1 + (1 + double(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 1 + (1 + (1 + double(z - 2)))) + SQR(1 + (z - 2)) :|: z - 2 >= 0 double(z) -{ 0 }-> 0 :|: z = 0 double(z) -{ 0 }-> 0 :|: z >= 0 double(z) -{ 0 }-> 1 + (1 + double(z - 1)) :|: z - 1 >= 0 plus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 plus(z, z') -{ 0 }-> 1 + plus(z, z' - 1) :|: z' - 1 >= 0, z >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + double(z - 2)), 1 + 0) :|: z - 2 >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + double(z - 2)), 1 + (1 + (1 + double(z - 2)))) :|: z - 2 >= 0 sqr(z) -{ 0 }-> plus(0, 1 + 0) :|: z = 1 + 0 sqr(z) -{ 0 }-> plus(0, 1 + 0) :|: z - 1 >= 0 sqr(z) -{ 0 }-> plus(0, 1 + (1 + (1 + double(z - 2)))) :|: z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), double(z - 2)), 1 + 0) :|: z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), double(z - 2)), 1 + (1 + (1 + double(z - 2)))) :|: z - 2 >= 0 sqr(z) -{ 0 }-> 0 :|: z = 0 sqr(z) -{ 0 }-> 0 :|: z >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + double(z - 2)), 0) :|: z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + double(z - 2)), 1 + (1 + double(z - 2))) :|: z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(0, 0) :|: z = 1 + 0 sqr(z) -{ 0 }-> 1 + plus(0, 0) :|: z - 1 >= 0 sqr(z) -{ 0 }-> 1 + plus(0, 1 + (1 + double(z - 2))) :|: z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), double(z - 2)), 0) :|: z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), double(z - 2)), 1 + (1 + double(z - 2))) :|: z - 2 >= 0 Function symbols to be analyzed: {double}, {DOUBLE}, {+'}, {plus}, {sqr}, {SQR} ---------------------------------------- (25) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (26) Obligation: Complexity RNTS consisting of the following rules: +'(z, z') -{ 1 }-> 1 + +'(z, z' - 1) :|: z' - 1 >= 0, z >= 0 DOUBLE(z) -{ 1 }-> 1 + DOUBLE(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + DOUBLE(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 0) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 1 + 0) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 1 + (1 + double(z - 2))) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 1 + (1 + (1 + double(z - 2)))) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + double(z - 2))) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + (1 + double(z - 2)))) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 0) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 1 + 0) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 1 + (1 + double(z - 2))) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 1 + (1 + (1 + double(z - 2)))) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 0) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 1 + 0) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 1 + (1 + double(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 1 + (1 + (1 + double(z - 2)))) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) + SQR(0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) + SQR(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) + SQR(0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) + SQR(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + double(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + (1 + double(z - 2)))) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 0) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 1 + 0) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 1 + (1 + double(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 1 + (1 + (1 + double(z - 2)))) + SQR(1 + (z - 2)) :|: z - 2 >= 0 double(z) -{ 0 }-> 0 :|: z = 0 double(z) -{ 0 }-> 0 :|: z >= 0 double(z) -{ 0 }-> 1 + (1 + double(z - 1)) :|: z - 1 >= 0 plus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 plus(z, z') -{ 0 }-> 1 + plus(z, z' - 1) :|: z' - 1 >= 0, z >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + double(z - 2)), 1 + 0) :|: z - 2 >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + double(z - 2)), 1 + (1 + (1 + double(z - 2)))) :|: z - 2 >= 0 sqr(z) -{ 0 }-> plus(0, 1 + 0) :|: z = 1 + 0 sqr(z) -{ 0 }-> plus(0, 1 + 0) :|: z - 1 >= 0 sqr(z) -{ 0 }-> plus(0, 1 + (1 + (1 + double(z - 2)))) :|: z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), double(z - 2)), 1 + 0) :|: z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), double(z - 2)), 1 + (1 + (1 + double(z - 2)))) :|: z - 2 >= 0 sqr(z) -{ 0 }-> 0 :|: z = 0 sqr(z) -{ 0 }-> 0 :|: z >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + double(z - 2)), 0) :|: z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + double(z - 2)), 1 + (1 + double(z - 2))) :|: z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(0, 0) :|: z = 1 + 0 sqr(z) -{ 0 }-> 1 + plus(0, 0) :|: z - 1 >= 0 sqr(z) -{ 0 }-> 1 + plus(0, 1 + (1 + double(z - 2))) :|: z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), double(z - 2)), 0) :|: z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), double(z - 2)), 1 + (1 + double(z - 2))) :|: z - 2 >= 0 Function symbols to be analyzed: {double}, {DOUBLE}, {+'}, {plus}, {sqr}, {SQR} ---------------------------------------- (27) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: double after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: 2*z ---------------------------------------- (28) Obligation: Complexity RNTS consisting of the following rules: +'(z, z') -{ 1 }-> 1 + +'(z, z' - 1) :|: z' - 1 >= 0, z >= 0 DOUBLE(z) -{ 1 }-> 1 + DOUBLE(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + DOUBLE(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 0) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 1 + 0) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 1 + (1 + double(z - 2))) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 1 + (1 + (1 + double(z - 2)))) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + double(z - 2))) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + (1 + double(z - 2)))) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 0) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 1 + 0) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 1 + (1 + double(z - 2))) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 1 + (1 + (1 + double(z - 2)))) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 0) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 1 + 0) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 1 + (1 + double(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 1 + (1 + (1 + double(z - 2)))) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) + SQR(0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) + SQR(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) + SQR(0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) + SQR(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + double(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + (1 + double(z - 2)))) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 0) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 1 + 0) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 1 + (1 + double(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 1 + (1 + (1 + double(z - 2)))) + SQR(1 + (z - 2)) :|: z - 2 >= 0 double(z) -{ 0 }-> 0 :|: z = 0 double(z) -{ 0 }-> 0 :|: z >= 0 double(z) -{ 0 }-> 1 + (1 + double(z - 1)) :|: z - 1 >= 0 plus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 plus(z, z') -{ 0 }-> 1 + plus(z, z' - 1) :|: z' - 1 >= 0, z >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + double(z - 2)), 1 + 0) :|: z - 2 >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + double(z - 2)), 1 + (1 + (1 + double(z - 2)))) :|: z - 2 >= 0 sqr(z) -{ 0 }-> plus(0, 1 + 0) :|: z = 1 + 0 sqr(z) -{ 0 }-> plus(0, 1 + 0) :|: z - 1 >= 0 sqr(z) -{ 0 }-> plus(0, 1 + (1 + (1 + double(z - 2)))) :|: z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), double(z - 2)), 1 + 0) :|: z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), double(z - 2)), 1 + (1 + (1 + double(z - 2)))) :|: z - 2 >= 0 sqr(z) -{ 0 }-> 0 :|: z = 0 sqr(z) -{ 0 }-> 0 :|: z >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + double(z - 2)), 0) :|: z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + double(z - 2)), 1 + (1 + double(z - 2))) :|: z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(0, 0) :|: z = 1 + 0 sqr(z) -{ 0 }-> 1 + plus(0, 0) :|: z - 1 >= 0 sqr(z) -{ 0 }-> 1 + plus(0, 1 + (1 + double(z - 2))) :|: z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), double(z - 2)), 0) :|: z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), double(z - 2)), 1 + (1 + double(z - 2))) :|: z - 2 >= 0 Function symbols to be analyzed: {double}, {DOUBLE}, {+'}, {plus}, {sqr}, {SQR} Previous analysis results are: double: runtime: ?, size: O(n^1) [2*z] ---------------------------------------- (29) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: double after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 0 ---------------------------------------- (30) Obligation: Complexity RNTS consisting of the following rules: +'(z, z') -{ 1 }-> 1 + +'(z, z' - 1) :|: z' - 1 >= 0, z >= 0 DOUBLE(z) -{ 1 }-> 1 + DOUBLE(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + DOUBLE(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 0) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 1 + 0) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 1 + (1 + double(z - 2))) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 1 + (1 + (1 + double(z - 2)))) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + double(z - 2))) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + (1 + double(z - 2)))) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 0) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 1 + 0) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 1 + (1 + double(z - 2))) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 1 + (1 + (1 + double(z - 2)))) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 0) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 1 + 0) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 1 + (1 + double(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + double(z - 2)), 1 + (1 + (1 + double(z - 2)))) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) + SQR(0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) + SQR(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) + SQR(0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) + SQR(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + double(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + (1 + double(z - 2)))) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 0) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 1 + 0) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 1 + (1 + double(z - 2))) + SQR(1 + (z - 2)) :|: z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), double(z - 2)), 1 + (1 + (1 + double(z - 2)))) + SQR(1 + (z - 2)) :|: z - 2 >= 0 double(z) -{ 0 }-> 0 :|: z = 0 double(z) -{ 0 }-> 0 :|: z >= 0 double(z) -{ 0 }-> 1 + (1 + double(z - 1)) :|: z - 1 >= 0 plus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 plus(z, z') -{ 0 }-> 1 + plus(z, z' - 1) :|: z' - 1 >= 0, z >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + double(z - 2)), 1 + 0) :|: z - 2 >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + double(z - 2)), 1 + (1 + (1 + double(z - 2)))) :|: z - 2 >= 0 sqr(z) -{ 0 }-> plus(0, 1 + 0) :|: z = 1 + 0 sqr(z) -{ 0 }-> plus(0, 1 + 0) :|: z - 1 >= 0 sqr(z) -{ 0 }-> plus(0, 1 + (1 + (1 + double(z - 2)))) :|: z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), double(z - 2)), 1 + 0) :|: z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), double(z - 2)), 1 + (1 + (1 + double(z - 2)))) :|: z - 2 >= 0 sqr(z) -{ 0 }-> 0 :|: z = 0 sqr(z) -{ 0 }-> 0 :|: z >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + double(z - 2)), 0) :|: z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + double(z - 2)), 1 + (1 + double(z - 2))) :|: z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(0, 0) :|: z = 1 + 0 sqr(z) -{ 0 }-> 1 + plus(0, 0) :|: z - 1 >= 0 sqr(z) -{ 0 }-> 1 + plus(0, 1 + (1 + double(z - 2))) :|: z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), double(z - 2)), 0) :|: z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), double(z - 2)), 1 + (1 + double(z - 2))) :|: z - 2 >= 0 Function symbols to be analyzed: {DOUBLE}, {+'}, {plus}, {sqr}, {SQR} Previous analysis results are: double: runtime: O(1) [0], size: O(n^1) [2*z] ---------------------------------------- (31) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (32) Obligation: Complexity RNTS consisting of the following rules: +'(z, z') -{ 1 }-> 1 + +'(z, z' - 1) :|: z' - 1 >= 0, z >= 0 DOUBLE(z) -{ 1 }-> 1 + DOUBLE(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + DOUBLE(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s12), 1 + (1 + (1 + s13))) :|: s12 >= 0, s12 <= 2 * (z - 2), s13 >= 0, s13 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s14), 1 + 0) :|: s14 >= 0, s14 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s19), 1 + (1 + s20)) :|: s19 >= 0, s19 <= 2 * (z - 2), s20 >= 0, s20 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s21), 0) :|: s21 >= 0, s21 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + s25)) :|: s25 >= 0, s25 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + (1 + s18))) :|: s18 >= 0, s18 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s15), 1 + (1 + (1 + s16))) :|: s15 >= 0, s15 <= 2 * (z - 2), s16 >= 0, s16 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s17), 1 + 0) :|: s17 >= 0, s17 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s22), 1 + (1 + s23)) :|: s22 >= 0, s22 <= 2 * (z - 2), s23 >= 0, s23 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s24), 0) :|: s24 >= 0, s24 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s), 1 + (1 + (1 + s'))) + SQR(1 + (z - 2)) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s''), 1 + 0) + SQR(1 + (z - 2)) :|: s'' >= 0, s'' <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s5), 1 + (1 + s6)) + SQR(1 + (z - 2)) :|: s5 >= 0, s5 <= 2 * (z - 2), s6 >= 0, s6 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s7), 0) + SQR(1 + (z - 2)) :|: s7 >= 0, s7 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) + SQR(0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) + SQR(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) + SQR(0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) + SQR(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + s11)) + SQR(1 + (z - 2)) :|: s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + (1 + s4))) + SQR(1 + (z - 2)) :|: s4 >= 0, s4 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s1), 1 + (1 + (1 + s2))) + SQR(1 + (z - 2)) :|: s1 >= 0, s1 <= 2 * (z - 2), s2 >= 0, s2 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s10), 0) + SQR(1 + (z - 2)) :|: s10 >= 0, s10 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s3), 1 + 0) + SQR(1 + (z - 2)) :|: s3 >= 0, s3 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s8), 1 + (1 + s9)) + SQR(1 + (z - 2)) :|: s8 >= 0, s8 <= 2 * (z - 2), s9 >= 0, s9 <= 2 * (z - 2), z - 2 >= 0 double(z) -{ 0 }-> 0 :|: z = 0 double(z) -{ 0 }-> 0 :|: z >= 0 double(z) -{ 0 }-> 1 + (1 + s40) :|: s40 >= 0, s40 <= 2 * (z - 1), z - 1 >= 0 plus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 plus(z, z') -{ 0 }-> 1 + plus(z, z' - 1) :|: z' - 1 >= 0, z >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + s26), 1 + (1 + (1 + s27))) :|: s26 >= 0, s26 <= 2 * (z - 2), s27 >= 0, s27 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + s28), 1 + 0) :|: s28 >= 0, s28 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(0, 1 + 0) :|: z = 1 + 0 sqr(z) -{ 0 }-> plus(0, 1 + 0) :|: z - 1 >= 0 sqr(z) -{ 0 }-> plus(0, 1 + (1 + (1 + s32))) :|: s32 >= 0, s32 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), s29), 1 + (1 + (1 + s30))) :|: s29 >= 0, s29 <= 2 * (z - 2), s30 >= 0, s30 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), s31), 1 + 0) :|: s31 >= 0, s31 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 0 :|: z = 0 sqr(z) -{ 0 }-> 0 :|: z >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + s33), 1 + (1 + s34)) :|: s33 >= 0, s33 <= 2 * (z - 2), s34 >= 0, s34 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + s35), 0) :|: s35 >= 0, s35 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(0, 0) :|: z = 1 + 0 sqr(z) -{ 0 }-> 1 + plus(0, 0) :|: z - 1 >= 0 sqr(z) -{ 0 }-> 1 + plus(0, 1 + (1 + s39)) :|: s39 >= 0, s39 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), s36), 1 + (1 + s37)) :|: s36 >= 0, s36 <= 2 * (z - 2), s37 >= 0, s37 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), s38), 0) :|: s38 >= 0, s38 <= 2 * (z - 2), z - 2 >= 0 Function symbols to be analyzed: {DOUBLE}, {+'}, {plus}, {sqr}, {SQR} Previous analysis results are: double: runtime: O(1) [0], size: O(n^1) [2*z] ---------------------------------------- (33) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: DOUBLE 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: +'(z, z') -{ 1 }-> 1 + +'(z, z' - 1) :|: z' - 1 >= 0, z >= 0 DOUBLE(z) -{ 1 }-> 1 + DOUBLE(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + DOUBLE(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s12), 1 + (1 + (1 + s13))) :|: s12 >= 0, s12 <= 2 * (z - 2), s13 >= 0, s13 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s14), 1 + 0) :|: s14 >= 0, s14 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s19), 1 + (1 + s20)) :|: s19 >= 0, s19 <= 2 * (z - 2), s20 >= 0, s20 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s21), 0) :|: s21 >= 0, s21 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + s25)) :|: s25 >= 0, s25 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + (1 + s18))) :|: s18 >= 0, s18 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s15), 1 + (1 + (1 + s16))) :|: s15 >= 0, s15 <= 2 * (z - 2), s16 >= 0, s16 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s17), 1 + 0) :|: s17 >= 0, s17 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s22), 1 + (1 + s23)) :|: s22 >= 0, s22 <= 2 * (z - 2), s23 >= 0, s23 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s24), 0) :|: s24 >= 0, s24 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s), 1 + (1 + (1 + s'))) + SQR(1 + (z - 2)) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s''), 1 + 0) + SQR(1 + (z - 2)) :|: s'' >= 0, s'' <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s5), 1 + (1 + s6)) + SQR(1 + (z - 2)) :|: s5 >= 0, s5 <= 2 * (z - 2), s6 >= 0, s6 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s7), 0) + SQR(1 + (z - 2)) :|: s7 >= 0, s7 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) + SQR(0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) + SQR(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) + SQR(0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) + SQR(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + s11)) + SQR(1 + (z - 2)) :|: s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + (1 + s4))) + SQR(1 + (z - 2)) :|: s4 >= 0, s4 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s1), 1 + (1 + (1 + s2))) + SQR(1 + (z - 2)) :|: s1 >= 0, s1 <= 2 * (z - 2), s2 >= 0, s2 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s10), 0) + SQR(1 + (z - 2)) :|: s10 >= 0, s10 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s3), 1 + 0) + SQR(1 + (z - 2)) :|: s3 >= 0, s3 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s8), 1 + (1 + s9)) + SQR(1 + (z - 2)) :|: s8 >= 0, s8 <= 2 * (z - 2), s9 >= 0, s9 <= 2 * (z - 2), z - 2 >= 0 double(z) -{ 0 }-> 0 :|: z = 0 double(z) -{ 0 }-> 0 :|: z >= 0 double(z) -{ 0 }-> 1 + (1 + s40) :|: s40 >= 0, s40 <= 2 * (z - 1), z - 1 >= 0 plus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 plus(z, z') -{ 0 }-> 1 + plus(z, z' - 1) :|: z' - 1 >= 0, z >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + s26), 1 + (1 + (1 + s27))) :|: s26 >= 0, s26 <= 2 * (z - 2), s27 >= 0, s27 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + s28), 1 + 0) :|: s28 >= 0, s28 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(0, 1 + 0) :|: z = 1 + 0 sqr(z) -{ 0 }-> plus(0, 1 + 0) :|: z - 1 >= 0 sqr(z) -{ 0 }-> plus(0, 1 + (1 + (1 + s32))) :|: s32 >= 0, s32 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), s29), 1 + (1 + (1 + s30))) :|: s29 >= 0, s29 <= 2 * (z - 2), s30 >= 0, s30 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), s31), 1 + 0) :|: s31 >= 0, s31 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 0 :|: z = 0 sqr(z) -{ 0 }-> 0 :|: z >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + s33), 1 + (1 + s34)) :|: s33 >= 0, s33 <= 2 * (z - 2), s34 >= 0, s34 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + s35), 0) :|: s35 >= 0, s35 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(0, 0) :|: z = 1 + 0 sqr(z) -{ 0 }-> 1 + plus(0, 0) :|: z - 1 >= 0 sqr(z) -{ 0 }-> 1 + plus(0, 1 + (1 + s39)) :|: s39 >= 0, s39 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), s36), 1 + (1 + s37)) :|: s36 >= 0, s36 <= 2 * (z - 2), s37 >= 0, s37 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), s38), 0) :|: s38 >= 0, s38 <= 2 * (z - 2), z - 2 >= 0 Function symbols to be analyzed: {DOUBLE}, {+'}, {plus}, {sqr}, {SQR} Previous analysis results are: double: runtime: O(1) [0], size: O(n^1) [2*z] DOUBLE: runtime: ?, size: O(1) [0] ---------------------------------------- (35) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: DOUBLE after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: z ---------------------------------------- (36) Obligation: Complexity RNTS consisting of the following rules: +'(z, z') -{ 1 }-> 1 + +'(z, z' - 1) :|: z' - 1 >= 0, z >= 0 DOUBLE(z) -{ 1 }-> 1 + DOUBLE(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + DOUBLE(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s12), 1 + (1 + (1 + s13))) :|: s12 >= 0, s12 <= 2 * (z - 2), s13 >= 0, s13 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s14), 1 + 0) :|: s14 >= 0, s14 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s19), 1 + (1 + s20)) :|: s19 >= 0, s19 <= 2 * (z - 2), s20 >= 0, s20 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s21), 0) :|: s21 >= 0, s21 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + s25)) :|: s25 >= 0, s25 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + (1 + s18))) :|: s18 >= 0, s18 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s15), 1 + (1 + (1 + s16))) :|: s15 >= 0, s15 <= 2 * (z - 2), s16 >= 0, s16 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s17), 1 + 0) :|: s17 >= 0, s17 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s22), 1 + (1 + s23)) :|: s22 >= 0, s22 <= 2 * (z - 2), s23 >= 0, s23 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s24), 0) :|: s24 >= 0, s24 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s), 1 + (1 + (1 + s'))) + SQR(1 + (z - 2)) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s''), 1 + 0) + SQR(1 + (z - 2)) :|: s'' >= 0, s'' <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s5), 1 + (1 + s6)) + SQR(1 + (z - 2)) :|: s5 >= 0, s5 <= 2 * (z - 2), s6 >= 0, s6 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s7), 0) + SQR(1 + (z - 2)) :|: s7 >= 0, s7 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) + SQR(0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) + SQR(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) + SQR(0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) + SQR(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + s11)) + SQR(1 + (z - 2)) :|: s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + (1 + s4))) + SQR(1 + (z - 2)) :|: s4 >= 0, s4 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s1), 1 + (1 + (1 + s2))) + SQR(1 + (z - 2)) :|: s1 >= 0, s1 <= 2 * (z - 2), s2 >= 0, s2 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s10), 0) + SQR(1 + (z - 2)) :|: s10 >= 0, s10 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s3), 1 + 0) + SQR(1 + (z - 2)) :|: s3 >= 0, s3 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s8), 1 + (1 + s9)) + SQR(1 + (z - 2)) :|: s8 >= 0, s8 <= 2 * (z - 2), s9 >= 0, s9 <= 2 * (z - 2), z - 2 >= 0 double(z) -{ 0 }-> 0 :|: z = 0 double(z) -{ 0 }-> 0 :|: z >= 0 double(z) -{ 0 }-> 1 + (1 + s40) :|: s40 >= 0, s40 <= 2 * (z - 1), z - 1 >= 0 plus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 plus(z, z') -{ 0 }-> 1 + plus(z, z' - 1) :|: z' - 1 >= 0, z >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + s26), 1 + (1 + (1 + s27))) :|: s26 >= 0, s26 <= 2 * (z - 2), s27 >= 0, s27 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + s28), 1 + 0) :|: s28 >= 0, s28 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(0, 1 + 0) :|: z = 1 + 0 sqr(z) -{ 0 }-> plus(0, 1 + 0) :|: z - 1 >= 0 sqr(z) -{ 0 }-> plus(0, 1 + (1 + (1 + s32))) :|: s32 >= 0, s32 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), s29), 1 + (1 + (1 + s30))) :|: s29 >= 0, s29 <= 2 * (z - 2), s30 >= 0, s30 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), s31), 1 + 0) :|: s31 >= 0, s31 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 0 :|: z = 0 sqr(z) -{ 0 }-> 0 :|: z >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + s33), 1 + (1 + s34)) :|: s33 >= 0, s33 <= 2 * (z - 2), s34 >= 0, s34 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + s35), 0) :|: s35 >= 0, s35 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(0, 0) :|: z = 1 + 0 sqr(z) -{ 0 }-> 1 + plus(0, 0) :|: z - 1 >= 0 sqr(z) -{ 0 }-> 1 + plus(0, 1 + (1 + s39)) :|: s39 >= 0, s39 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), s36), 1 + (1 + s37)) :|: s36 >= 0, s36 <= 2 * (z - 2), s37 >= 0, s37 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), s38), 0) :|: s38 >= 0, s38 <= 2 * (z - 2), z - 2 >= 0 Function symbols to be analyzed: {+'}, {plus}, {sqr}, {SQR} Previous analysis results are: double: runtime: O(1) [0], size: O(n^1) [2*z] DOUBLE: runtime: O(n^1) [z], size: O(1) [0] ---------------------------------------- (37) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (38) Obligation: Complexity RNTS consisting of the following rules: +'(z, z') -{ 1 }-> 1 + +'(z, z' - 1) :|: z' - 1 >= 0, z >= 0 DOUBLE(z) -{ z }-> 1 + s41 :|: s41 >= 0, s41 <= 0, z - 1 >= 0 SQR(z) -{ z }-> 1 + s42 :|: s42 >= 0, s42 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s12), 1 + (1 + (1 + s13))) :|: s12 >= 0, s12 <= 2 * (z - 2), s13 >= 0, s13 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s14), 1 + 0) :|: s14 >= 0, s14 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s19), 1 + (1 + s20)) :|: s19 >= 0, s19 <= 2 * (z - 2), s20 >= 0, s20 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s21), 0) :|: s21 >= 0, s21 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + s25)) :|: s25 >= 0, s25 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + (1 + s18))) :|: s18 >= 0, s18 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s15), 1 + (1 + (1 + s16))) :|: s15 >= 0, s15 <= 2 * (z - 2), s16 >= 0, s16 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s17), 1 + 0) :|: s17 >= 0, s17 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s22), 1 + (1 + s23)) :|: s22 >= 0, s22 <= 2 * (z - 2), s23 >= 0, s23 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s24), 0) :|: s24 >= 0, s24 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s), 1 + (1 + (1 + s'))) + SQR(1 + (z - 2)) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s''), 1 + 0) + SQR(1 + (z - 2)) :|: s'' >= 0, s'' <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s5), 1 + (1 + s6)) + SQR(1 + (z - 2)) :|: s5 >= 0, s5 <= 2 * (z - 2), s6 >= 0, s6 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s7), 0) + SQR(1 + (z - 2)) :|: s7 >= 0, s7 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) + SQR(0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) + SQR(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) + SQR(0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) + SQR(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + s11)) + SQR(1 + (z - 2)) :|: s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + (1 + s4))) + SQR(1 + (z - 2)) :|: s4 >= 0, s4 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s1), 1 + (1 + (1 + s2))) + SQR(1 + (z - 2)) :|: s1 >= 0, s1 <= 2 * (z - 2), s2 >= 0, s2 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s10), 0) + SQR(1 + (z - 2)) :|: s10 >= 0, s10 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s3), 1 + 0) + SQR(1 + (z - 2)) :|: s3 >= 0, s3 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s8), 1 + (1 + s9)) + SQR(1 + (z - 2)) :|: s8 >= 0, s8 <= 2 * (z - 2), s9 >= 0, s9 <= 2 * (z - 2), z - 2 >= 0 double(z) -{ 0 }-> 0 :|: z = 0 double(z) -{ 0 }-> 0 :|: z >= 0 double(z) -{ 0 }-> 1 + (1 + s40) :|: s40 >= 0, s40 <= 2 * (z - 1), z - 1 >= 0 plus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 plus(z, z') -{ 0 }-> 1 + plus(z, z' - 1) :|: z' - 1 >= 0, z >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + s26), 1 + (1 + (1 + s27))) :|: s26 >= 0, s26 <= 2 * (z - 2), s27 >= 0, s27 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + s28), 1 + 0) :|: s28 >= 0, s28 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(0, 1 + 0) :|: z = 1 + 0 sqr(z) -{ 0 }-> plus(0, 1 + 0) :|: z - 1 >= 0 sqr(z) -{ 0 }-> plus(0, 1 + (1 + (1 + s32))) :|: s32 >= 0, s32 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), s29), 1 + (1 + (1 + s30))) :|: s29 >= 0, s29 <= 2 * (z - 2), s30 >= 0, s30 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), s31), 1 + 0) :|: s31 >= 0, s31 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 0 :|: z = 0 sqr(z) -{ 0 }-> 0 :|: z >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + s33), 1 + (1 + s34)) :|: s33 >= 0, s33 <= 2 * (z - 2), s34 >= 0, s34 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + s35), 0) :|: s35 >= 0, s35 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(0, 0) :|: z = 1 + 0 sqr(z) -{ 0 }-> 1 + plus(0, 0) :|: z - 1 >= 0 sqr(z) -{ 0 }-> 1 + plus(0, 1 + (1 + s39)) :|: s39 >= 0, s39 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), s36), 1 + (1 + s37)) :|: s36 >= 0, s36 <= 2 * (z - 2), s37 >= 0, s37 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), s38), 0) :|: s38 >= 0, s38 <= 2 * (z - 2), z - 2 >= 0 Function symbols to be analyzed: {+'}, {plus}, {sqr}, {SQR} Previous analysis results are: double: runtime: O(1) [0], size: O(n^1) [2*z] DOUBLE: runtime: O(n^1) [z], size: O(1) [0] ---------------------------------------- (39) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: +' after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 0 ---------------------------------------- (40) Obligation: Complexity RNTS consisting of the following rules: +'(z, z') -{ 1 }-> 1 + +'(z, z' - 1) :|: z' - 1 >= 0, z >= 0 DOUBLE(z) -{ z }-> 1 + s41 :|: s41 >= 0, s41 <= 0, z - 1 >= 0 SQR(z) -{ z }-> 1 + s42 :|: s42 >= 0, s42 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s12), 1 + (1 + (1 + s13))) :|: s12 >= 0, s12 <= 2 * (z - 2), s13 >= 0, s13 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s14), 1 + 0) :|: s14 >= 0, s14 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s19), 1 + (1 + s20)) :|: s19 >= 0, s19 <= 2 * (z - 2), s20 >= 0, s20 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s21), 0) :|: s21 >= 0, s21 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + s25)) :|: s25 >= 0, s25 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + (1 + s18))) :|: s18 >= 0, s18 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s15), 1 + (1 + (1 + s16))) :|: s15 >= 0, s15 <= 2 * (z - 2), s16 >= 0, s16 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s17), 1 + 0) :|: s17 >= 0, s17 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s22), 1 + (1 + s23)) :|: s22 >= 0, s22 <= 2 * (z - 2), s23 >= 0, s23 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s24), 0) :|: s24 >= 0, s24 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s), 1 + (1 + (1 + s'))) + SQR(1 + (z - 2)) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s''), 1 + 0) + SQR(1 + (z - 2)) :|: s'' >= 0, s'' <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s5), 1 + (1 + s6)) + SQR(1 + (z - 2)) :|: s5 >= 0, s5 <= 2 * (z - 2), s6 >= 0, s6 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s7), 0) + SQR(1 + (z - 2)) :|: s7 >= 0, s7 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) + SQR(0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) + SQR(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) + SQR(0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) + SQR(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + s11)) + SQR(1 + (z - 2)) :|: s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + (1 + s4))) + SQR(1 + (z - 2)) :|: s4 >= 0, s4 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s1), 1 + (1 + (1 + s2))) + SQR(1 + (z - 2)) :|: s1 >= 0, s1 <= 2 * (z - 2), s2 >= 0, s2 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s10), 0) + SQR(1 + (z - 2)) :|: s10 >= 0, s10 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s3), 1 + 0) + SQR(1 + (z - 2)) :|: s3 >= 0, s3 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s8), 1 + (1 + s9)) + SQR(1 + (z - 2)) :|: s8 >= 0, s8 <= 2 * (z - 2), s9 >= 0, s9 <= 2 * (z - 2), z - 2 >= 0 double(z) -{ 0 }-> 0 :|: z = 0 double(z) -{ 0 }-> 0 :|: z >= 0 double(z) -{ 0 }-> 1 + (1 + s40) :|: s40 >= 0, s40 <= 2 * (z - 1), z - 1 >= 0 plus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 plus(z, z') -{ 0 }-> 1 + plus(z, z' - 1) :|: z' - 1 >= 0, z >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + s26), 1 + (1 + (1 + s27))) :|: s26 >= 0, s26 <= 2 * (z - 2), s27 >= 0, s27 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + s28), 1 + 0) :|: s28 >= 0, s28 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(0, 1 + 0) :|: z = 1 + 0 sqr(z) -{ 0 }-> plus(0, 1 + 0) :|: z - 1 >= 0 sqr(z) -{ 0 }-> plus(0, 1 + (1 + (1 + s32))) :|: s32 >= 0, s32 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), s29), 1 + (1 + (1 + s30))) :|: s29 >= 0, s29 <= 2 * (z - 2), s30 >= 0, s30 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), s31), 1 + 0) :|: s31 >= 0, s31 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 0 :|: z = 0 sqr(z) -{ 0 }-> 0 :|: z >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + s33), 1 + (1 + s34)) :|: s33 >= 0, s33 <= 2 * (z - 2), s34 >= 0, s34 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + s35), 0) :|: s35 >= 0, s35 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(0, 0) :|: z = 1 + 0 sqr(z) -{ 0 }-> 1 + plus(0, 0) :|: z - 1 >= 0 sqr(z) -{ 0 }-> 1 + plus(0, 1 + (1 + s39)) :|: s39 >= 0, s39 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), s36), 1 + (1 + s37)) :|: s36 >= 0, s36 <= 2 * (z - 2), s37 >= 0, s37 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), s38), 0) :|: s38 >= 0, s38 <= 2 * (z - 2), z - 2 >= 0 Function symbols to be analyzed: {+'}, {plus}, {sqr}, {SQR} Previous analysis results are: double: runtime: O(1) [0], size: O(n^1) [2*z] DOUBLE: runtime: O(n^1) [z], size: O(1) [0] +': runtime: ?, size: O(1) [0] ---------------------------------------- (41) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: +' after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: z' ---------------------------------------- (42) Obligation: Complexity RNTS consisting of the following rules: +'(z, z') -{ 1 }-> 1 + +'(z, z' - 1) :|: z' - 1 >= 0, z >= 0 DOUBLE(z) -{ z }-> 1 + s41 :|: s41 >= 0, s41 <= 0, z - 1 >= 0 SQR(z) -{ z }-> 1 + s42 :|: s42 >= 0, s42 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s12), 1 + (1 + (1 + s13))) :|: s12 >= 0, s12 <= 2 * (z - 2), s13 >= 0, s13 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s14), 1 + 0) :|: s14 >= 0, s14 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s19), 1 + (1 + s20)) :|: s19 >= 0, s19 <= 2 * (z - 2), s20 >= 0, s20 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s21), 0) :|: s21 >= 0, s21 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + s25)) :|: s25 >= 0, s25 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + (1 + s18))) :|: s18 >= 0, s18 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s15), 1 + (1 + (1 + s16))) :|: s15 >= 0, s15 <= 2 * (z - 2), s16 >= 0, s16 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s17), 1 + 0) :|: s17 >= 0, s17 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s22), 1 + (1 + s23)) :|: s22 >= 0, s22 <= 2 * (z - 2), s23 >= 0, s23 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s24), 0) :|: s24 >= 0, s24 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s), 1 + (1 + (1 + s'))) + SQR(1 + (z - 2)) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s''), 1 + 0) + SQR(1 + (z - 2)) :|: s'' >= 0, s'' <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s5), 1 + (1 + s6)) + SQR(1 + (z - 2)) :|: s5 >= 0, s5 <= 2 * (z - 2), s6 >= 0, s6 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s7), 0) + SQR(1 + (z - 2)) :|: s7 >= 0, s7 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) + SQR(0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 0) + SQR(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) + SQR(0) :|: z = 1 + 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + 0) + SQR(z - 1) :|: z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + s11)) + SQR(1 + (z - 2)) :|: s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(0, 1 + (1 + (1 + s4))) + SQR(1 + (z - 2)) :|: s4 >= 0, s4 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s1), 1 + (1 + (1 + s2))) + SQR(1 + (z - 2)) :|: s1 >= 0, s1 <= 2 * (z - 2), s2 >= 0, s2 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s10), 0) + SQR(1 + (z - 2)) :|: s10 >= 0, s10 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s3), 1 + 0) + SQR(1 + (z - 2)) :|: s3 >= 0, s3 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s8), 1 + (1 + s9)) + SQR(1 + (z - 2)) :|: s8 >= 0, s8 <= 2 * (z - 2), s9 >= 0, s9 <= 2 * (z - 2), z - 2 >= 0 double(z) -{ 0 }-> 0 :|: z = 0 double(z) -{ 0 }-> 0 :|: z >= 0 double(z) -{ 0 }-> 1 + (1 + s40) :|: s40 >= 0, s40 <= 2 * (z - 1), z - 1 >= 0 plus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 plus(z, z') -{ 0 }-> 1 + plus(z, z' - 1) :|: z' - 1 >= 0, z >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + s26), 1 + (1 + (1 + s27))) :|: s26 >= 0, s26 <= 2 * (z - 2), s27 >= 0, s27 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + s28), 1 + 0) :|: s28 >= 0, s28 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(0, 1 + 0) :|: z = 1 + 0 sqr(z) -{ 0 }-> plus(0, 1 + 0) :|: z - 1 >= 0 sqr(z) -{ 0 }-> plus(0, 1 + (1 + (1 + s32))) :|: s32 >= 0, s32 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), s29), 1 + (1 + (1 + s30))) :|: s29 >= 0, s29 <= 2 * (z - 2), s30 >= 0, s30 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), s31), 1 + 0) :|: s31 >= 0, s31 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 0 :|: z = 0 sqr(z) -{ 0 }-> 0 :|: z >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + s33), 1 + (1 + s34)) :|: s33 >= 0, s33 <= 2 * (z - 2), s34 >= 0, s34 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + s35), 0) :|: s35 >= 0, s35 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(0, 0) :|: z = 1 + 0 sqr(z) -{ 0 }-> 1 + plus(0, 0) :|: z - 1 >= 0 sqr(z) -{ 0 }-> 1 + plus(0, 1 + (1 + s39)) :|: s39 >= 0, s39 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), s36), 1 + (1 + s37)) :|: s36 >= 0, s36 <= 2 * (z - 2), s37 >= 0, s37 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), s38), 0) :|: s38 >= 0, s38 <= 2 * (z - 2), z - 2 >= 0 Function symbols to be analyzed: {plus}, {sqr}, {SQR} Previous analysis results are: double: runtime: O(1) [0], size: O(n^1) [2*z] DOUBLE: runtime: O(n^1) [z], size: O(1) [0] +': runtime: O(n^1) [z'], size: O(1) [0] ---------------------------------------- (43) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (44) Obligation: Complexity RNTS consisting of the following rules: +'(z, z') -{ z' }-> 1 + s49 :|: s49 >= 0, s49 <= 0, z' - 1 >= 0, z >= 0 DOUBLE(z) -{ z }-> 1 + s41 :|: s41 >= 0, s41 <= 0, z - 1 >= 0 SQR(z) -{ z }-> 1 + s42 :|: s42 >= 0, s42 <= 0, z - 1 >= 0 SQR(z) -{ 2 }-> 1 + s50 :|: s50 >= 0, s50 <= 0, z = 1 + 0 SQR(z) -{ 4 + s18 }-> 1 + s51 :|: s51 >= 0, s51 <= 0, s18 >= 0, s18 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s52 :|: s52 >= 0, s52 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + s53 :|: s53 >= 0, s53 <= 0, z = 1 + 0 SQR(z) -{ 3 + s25 }-> 1 + s54 :|: s54 >= 0, s54 <= 0, s25 >= 0, s25 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + s55 :|: s55 >= 0, s55 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s12), 1 + (1 + (1 + s13))) :|: s12 >= 0, s12 <= 2 * (z - 2), s13 >= 0, s13 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s14), 1 + 0) :|: s14 >= 0, s14 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s19), 1 + (1 + s20)) :|: s19 >= 0, s19 <= 2 * (z - 2), s20 >= 0, s20 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s21), 0) :|: s21 >= 0, s21 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s15), 1 + (1 + (1 + s16))) :|: s15 >= 0, s15 <= 2 * (z - 2), s16 >= 0, s16 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s17), 1 + 0) :|: s17 >= 0, s17 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s22), 1 + (1 + s23)) :|: s22 >= 0, s22 <= 2 * (z - 2), s23 >= 0, s23 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s24), 0) :|: s24 >= 0, s24 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s43 + SQR(0) :|: s43 >= 0, s43 <= 0, z = 1 + 0 SQR(z) -{ 4 + s4 }-> 1 + s44 + SQR(1 + (z - 2)) :|: s44 >= 0, s44 <= 0, s4 >= 0, s4 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s45 + SQR(z - 1) :|: s45 >= 0, s45 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + s46 + SQR(0) :|: s46 >= 0, s46 <= 0, z = 1 + 0 SQR(z) -{ 3 + s11 }-> 1 + s47 + SQR(1 + (z - 2)) :|: s47 >= 0, s47 <= 0, s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + s48 + SQR(z - 1) :|: s48 >= 0, s48 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s), 1 + (1 + (1 + s'))) + SQR(1 + (z - 2)) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s''), 1 + 0) + SQR(1 + (z - 2)) :|: s'' >= 0, s'' <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s5), 1 + (1 + s6)) + SQR(1 + (z - 2)) :|: s5 >= 0, s5 <= 2 * (z - 2), s6 >= 0, s6 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s7), 0) + SQR(1 + (z - 2)) :|: s7 >= 0, s7 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s1), 1 + (1 + (1 + s2))) + SQR(1 + (z - 2)) :|: s1 >= 0, s1 <= 2 * (z - 2), s2 >= 0, s2 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s10), 0) + SQR(1 + (z - 2)) :|: s10 >= 0, s10 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s3), 1 + 0) + SQR(1 + (z - 2)) :|: s3 >= 0, s3 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s8), 1 + (1 + s9)) + SQR(1 + (z - 2)) :|: s8 >= 0, s8 <= 2 * (z - 2), s9 >= 0, s9 <= 2 * (z - 2), z - 2 >= 0 double(z) -{ 0 }-> 0 :|: z = 0 double(z) -{ 0 }-> 0 :|: z >= 0 double(z) -{ 0 }-> 1 + (1 + s40) :|: s40 >= 0, s40 <= 2 * (z - 1), z - 1 >= 0 plus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 plus(z, z') -{ 0 }-> 1 + plus(z, z' - 1) :|: z' - 1 >= 0, z >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + s26), 1 + (1 + (1 + s27))) :|: s26 >= 0, s26 <= 2 * (z - 2), s27 >= 0, s27 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + s28), 1 + 0) :|: s28 >= 0, s28 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(0, 1 + 0) :|: z = 1 + 0 sqr(z) -{ 0 }-> plus(0, 1 + 0) :|: z - 1 >= 0 sqr(z) -{ 0 }-> plus(0, 1 + (1 + (1 + s32))) :|: s32 >= 0, s32 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), s29), 1 + (1 + (1 + s30))) :|: s29 >= 0, s29 <= 2 * (z - 2), s30 >= 0, s30 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), s31), 1 + 0) :|: s31 >= 0, s31 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 0 :|: z = 0 sqr(z) -{ 0 }-> 0 :|: z >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + s33), 1 + (1 + s34)) :|: s33 >= 0, s33 <= 2 * (z - 2), s34 >= 0, s34 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + s35), 0) :|: s35 >= 0, s35 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(0, 0) :|: z = 1 + 0 sqr(z) -{ 0 }-> 1 + plus(0, 0) :|: z - 1 >= 0 sqr(z) -{ 0 }-> 1 + plus(0, 1 + (1 + s39)) :|: s39 >= 0, s39 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), s36), 1 + (1 + s37)) :|: s36 >= 0, s36 <= 2 * (z - 2), s37 >= 0, s37 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), s38), 0) :|: s38 >= 0, s38 <= 2 * (z - 2), z - 2 >= 0 Function symbols to be analyzed: {plus}, {sqr}, {SQR} Previous analysis results are: double: runtime: O(1) [0], size: O(n^1) [2*z] DOUBLE: runtime: O(n^1) [z], size: O(1) [0] +': runtime: O(n^1) [z'], size: O(1) [0] ---------------------------------------- (45) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: plus after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: z + z' ---------------------------------------- (46) Obligation: Complexity RNTS consisting of the following rules: +'(z, z') -{ z' }-> 1 + s49 :|: s49 >= 0, s49 <= 0, z' - 1 >= 0, z >= 0 DOUBLE(z) -{ z }-> 1 + s41 :|: s41 >= 0, s41 <= 0, z - 1 >= 0 SQR(z) -{ z }-> 1 + s42 :|: s42 >= 0, s42 <= 0, z - 1 >= 0 SQR(z) -{ 2 }-> 1 + s50 :|: s50 >= 0, s50 <= 0, z = 1 + 0 SQR(z) -{ 4 + s18 }-> 1 + s51 :|: s51 >= 0, s51 <= 0, s18 >= 0, s18 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s52 :|: s52 >= 0, s52 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + s53 :|: s53 >= 0, s53 <= 0, z = 1 + 0 SQR(z) -{ 3 + s25 }-> 1 + s54 :|: s54 >= 0, s54 <= 0, s25 >= 0, s25 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + s55 :|: s55 >= 0, s55 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s12), 1 + (1 + (1 + s13))) :|: s12 >= 0, s12 <= 2 * (z - 2), s13 >= 0, s13 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s14), 1 + 0) :|: s14 >= 0, s14 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s19), 1 + (1 + s20)) :|: s19 >= 0, s19 <= 2 * (z - 2), s20 >= 0, s20 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s21), 0) :|: s21 >= 0, s21 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s15), 1 + (1 + (1 + s16))) :|: s15 >= 0, s15 <= 2 * (z - 2), s16 >= 0, s16 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s17), 1 + 0) :|: s17 >= 0, s17 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s22), 1 + (1 + s23)) :|: s22 >= 0, s22 <= 2 * (z - 2), s23 >= 0, s23 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s24), 0) :|: s24 >= 0, s24 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s43 + SQR(0) :|: s43 >= 0, s43 <= 0, z = 1 + 0 SQR(z) -{ 4 + s4 }-> 1 + s44 + SQR(1 + (z - 2)) :|: s44 >= 0, s44 <= 0, s4 >= 0, s4 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s45 + SQR(z - 1) :|: s45 >= 0, s45 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + s46 + SQR(0) :|: s46 >= 0, s46 <= 0, z = 1 + 0 SQR(z) -{ 3 + s11 }-> 1 + s47 + SQR(1 + (z - 2)) :|: s47 >= 0, s47 <= 0, s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + s48 + SQR(z - 1) :|: s48 >= 0, s48 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s), 1 + (1 + (1 + s'))) + SQR(1 + (z - 2)) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s''), 1 + 0) + SQR(1 + (z - 2)) :|: s'' >= 0, s'' <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s5), 1 + (1 + s6)) + SQR(1 + (z - 2)) :|: s5 >= 0, s5 <= 2 * (z - 2), s6 >= 0, s6 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s7), 0) + SQR(1 + (z - 2)) :|: s7 >= 0, s7 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s1), 1 + (1 + (1 + s2))) + SQR(1 + (z - 2)) :|: s1 >= 0, s1 <= 2 * (z - 2), s2 >= 0, s2 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s10), 0) + SQR(1 + (z - 2)) :|: s10 >= 0, s10 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s3), 1 + 0) + SQR(1 + (z - 2)) :|: s3 >= 0, s3 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s8), 1 + (1 + s9)) + SQR(1 + (z - 2)) :|: s8 >= 0, s8 <= 2 * (z - 2), s9 >= 0, s9 <= 2 * (z - 2), z - 2 >= 0 double(z) -{ 0 }-> 0 :|: z = 0 double(z) -{ 0 }-> 0 :|: z >= 0 double(z) -{ 0 }-> 1 + (1 + s40) :|: s40 >= 0, s40 <= 2 * (z - 1), z - 1 >= 0 plus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 plus(z, z') -{ 0 }-> 1 + plus(z, z' - 1) :|: z' - 1 >= 0, z >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + s26), 1 + (1 + (1 + s27))) :|: s26 >= 0, s26 <= 2 * (z - 2), s27 >= 0, s27 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + s28), 1 + 0) :|: s28 >= 0, s28 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(0, 1 + 0) :|: z = 1 + 0 sqr(z) -{ 0 }-> plus(0, 1 + 0) :|: z - 1 >= 0 sqr(z) -{ 0 }-> plus(0, 1 + (1 + (1 + s32))) :|: s32 >= 0, s32 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), s29), 1 + (1 + (1 + s30))) :|: s29 >= 0, s29 <= 2 * (z - 2), s30 >= 0, s30 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), s31), 1 + 0) :|: s31 >= 0, s31 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 0 :|: z = 0 sqr(z) -{ 0 }-> 0 :|: z >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + s33), 1 + (1 + s34)) :|: s33 >= 0, s33 <= 2 * (z - 2), s34 >= 0, s34 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + s35), 0) :|: s35 >= 0, s35 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(0, 0) :|: z = 1 + 0 sqr(z) -{ 0 }-> 1 + plus(0, 0) :|: z - 1 >= 0 sqr(z) -{ 0 }-> 1 + plus(0, 1 + (1 + s39)) :|: s39 >= 0, s39 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), s36), 1 + (1 + s37)) :|: s36 >= 0, s36 <= 2 * (z - 2), s37 >= 0, s37 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), s38), 0) :|: s38 >= 0, s38 <= 2 * (z - 2), z - 2 >= 0 Function symbols to be analyzed: {plus}, {sqr}, {SQR} Previous analysis results are: double: runtime: O(1) [0], size: O(n^1) [2*z] DOUBLE: runtime: O(n^1) [z], size: O(1) [0] +': runtime: O(n^1) [z'], size: O(1) [0] plus: runtime: ?, size: O(n^1) [z + z'] ---------------------------------------- (47) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: plus after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 0 ---------------------------------------- (48) Obligation: Complexity RNTS consisting of the following rules: +'(z, z') -{ z' }-> 1 + s49 :|: s49 >= 0, s49 <= 0, z' - 1 >= 0, z >= 0 DOUBLE(z) -{ z }-> 1 + s41 :|: s41 >= 0, s41 <= 0, z - 1 >= 0 SQR(z) -{ z }-> 1 + s42 :|: s42 >= 0, s42 <= 0, z - 1 >= 0 SQR(z) -{ 2 }-> 1 + s50 :|: s50 >= 0, s50 <= 0, z = 1 + 0 SQR(z) -{ 4 + s18 }-> 1 + s51 :|: s51 >= 0, s51 <= 0, s18 >= 0, s18 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s52 :|: s52 >= 0, s52 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + s53 :|: s53 >= 0, s53 <= 0, z = 1 + 0 SQR(z) -{ 3 + s25 }-> 1 + s54 :|: s54 >= 0, s54 <= 0, s25 >= 0, s25 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + s55 :|: s55 >= 0, s55 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s12), 1 + (1 + (1 + s13))) :|: s12 >= 0, s12 <= 2 * (z - 2), s13 >= 0, s13 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s14), 1 + 0) :|: s14 >= 0, s14 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s19), 1 + (1 + s20)) :|: s19 >= 0, s19 <= 2 * (z - 2), s20 >= 0, s20 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s21), 0) :|: s21 >= 0, s21 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s15), 1 + (1 + (1 + s16))) :|: s15 >= 0, s15 <= 2 * (z - 2), s16 >= 0, s16 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s17), 1 + 0) :|: s17 >= 0, s17 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s22), 1 + (1 + s23)) :|: s22 >= 0, s22 <= 2 * (z - 2), s23 >= 0, s23 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s24), 0) :|: s24 >= 0, s24 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s43 + SQR(0) :|: s43 >= 0, s43 <= 0, z = 1 + 0 SQR(z) -{ 4 + s4 }-> 1 + s44 + SQR(1 + (z - 2)) :|: s44 >= 0, s44 <= 0, s4 >= 0, s4 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s45 + SQR(z - 1) :|: s45 >= 0, s45 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + s46 + SQR(0) :|: s46 >= 0, s46 <= 0, z = 1 + 0 SQR(z) -{ 3 + s11 }-> 1 + s47 + SQR(1 + (z - 2)) :|: s47 >= 0, s47 <= 0, s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + s48 + SQR(z - 1) :|: s48 >= 0, s48 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s), 1 + (1 + (1 + s'))) + SQR(1 + (z - 2)) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s''), 1 + 0) + SQR(1 + (z - 2)) :|: s'' >= 0, s'' <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s5), 1 + (1 + s6)) + SQR(1 + (z - 2)) :|: s5 >= 0, s5 <= 2 * (z - 2), s6 >= 0, s6 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s7), 0) + SQR(1 + (z - 2)) :|: s7 >= 0, s7 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s1), 1 + (1 + (1 + s2))) + SQR(1 + (z - 2)) :|: s1 >= 0, s1 <= 2 * (z - 2), s2 >= 0, s2 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s10), 0) + SQR(1 + (z - 2)) :|: s10 >= 0, s10 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s3), 1 + 0) + SQR(1 + (z - 2)) :|: s3 >= 0, s3 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s8), 1 + (1 + s9)) + SQR(1 + (z - 2)) :|: s8 >= 0, s8 <= 2 * (z - 2), s9 >= 0, s9 <= 2 * (z - 2), z - 2 >= 0 double(z) -{ 0 }-> 0 :|: z = 0 double(z) -{ 0 }-> 0 :|: z >= 0 double(z) -{ 0 }-> 1 + (1 + s40) :|: s40 >= 0, s40 <= 2 * (z - 1), z - 1 >= 0 plus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 plus(z, z') -{ 0 }-> 1 + plus(z, z' - 1) :|: z' - 1 >= 0, z >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + s26), 1 + (1 + (1 + s27))) :|: s26 >= 0, s26 <= 2 * (z - 2), s27 >= 0, s27 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + s28), 1 + 0) :|: s28 >= 0, s28 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(0, 1 + 0) :|: z = 1 + 0 sqr(z) -{ 0 }-> plus(0, 1 + 0) :|: z - 1 >= 0 sqr(z) -{ 0 }-> plus(0, 1 + (1 + (1 + s32))) :|: s32 >= 0, s32 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), s29), 1 + (1 + (1 + s30))) :|: s29 >= 0, s29 <= 2 * (z - 2), s30 >= 0, s30 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), s31), 1 + 0) :|: s31 >= 0, s31 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 0 :|: z = 0 sqr(z) -{ 0 }-> 0 :|: z >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + s33), 1 + (1 + s34)) :|: s33 >= 0, s33 <= 2 * (z - 2), s34 >= 0, s34 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + s35), 0) :|: s35 >= 0, s35 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(0, 0) :|: z = 1 + 0 sqr(z) -{ 0 }-> 1 + plus(0, 0) :|: z - 1 >= 0 sqr(z) -{ 0 }-> 1 + plus(0, 1 + (1 + s39)) :|: s39 >= 0, s39 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), s36), 1 + (1 + s37)) :|: s36 >= 0, s36 <= 2 * (z - 2), s37 >= 0, s37 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), s38), 0) :|: s38 >= 0, s38 <= 2 * (z - 2), z - 2 >= 0 Function symbols to be analyzed: {sqr}, {SQR} Previous analysis results are: double: runtime: O(1) [0], size: O(n^1) [2*z] DOUBLE: runtime: O(n^1) [z], size: O(1) [0] +': runtime: O(n^1) [z'], size: O(1) [0] plus: runtime: O(1) [0], size: O(n^1) [z + z'] ---------------------------------------- (49) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (50) Obligation: Complexity RNTS consisting of the following rules: +'(z, z') -{ z' }-> 1 + s49 :|: s49 >= 0, s49 <= 0, z' - 1 >= 0, z >= 0 DOUBLE(z) -{ z }-> 1 + s41 :|: s41 >= 0, s41 <= 0, z - 1 >= 0 SQR(z) -{ z }-> 1 + s42 :|: s42 >= 0, s42 <= 0, z - 1 >= 0 SQR(z) -{ 2 }-> 1 + s50 :|: s50 >= 0, s50 <= 0, z = 1 + 0 SQR(z) -{ 4 + s18 }-> 1 + s51 :|: s51 >= 0, s51 <= 0, s18 >= 0, s18 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s52 :|: s52 >= 0, s52 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + s53 :|: s53 >= 0, s53 <= 0, z = 1 + 0 SQR(z) -{ 3 + s25 }-> 1 + s54 :|: s54 >= 0, s54 <= 0, s25 >= 0, s25 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + s55 :|: s55 >= 0, s55 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s12), 1 + (1 + (1 + s13))) :|: s12 >= 0, s12 <= 2 * (z - 2), s13 >= 0, s13 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s14), 1 + 0) :|: s14 >= 0, s14 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s19), 1 + (1 + s20)) :|: s19 >= 0, s19 <= 2 * (z - 2), s20 >= 0, s20 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s21), 0) :|: s21 >= 0, s21 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s15), 1 + (1 + (1 + s16))) :|: s15 >= 0, s15 <= 2 * (z - 2), s16 >= 0, s16 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s17), 1 + 0) :|: s17 >= 0, s17 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s22), 1 + (1 + s23)) :|: s22 >= 0, s22 <= 2 * (z - 2), s23 >= 0, s23 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s24), 0) :|: s24 >= 0, s24 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s43 + SQR(0) :|: s43 >= 0, s43 <= 0, z = 1 + 0 SQR(z) -{ 4 + s4 }-> 1 + s44 + SQR(1 + (z - 2)) :|: s44 >= 0, s44 <= 0, s4 >= 0, s4 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s45 + SQR(z - 1) :|: s45 >= 0, s45 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + s46 + SQR(0) :|: s46 >= 0, s46 <= 0, z = 1 + 0 SQR(z) -{ 3 + s11 }-> 1 + s47 + SQR(1 + (z - 2)) :|: s47 >= 0, s47 <= 0, s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + s48 + SQR(z - 1) :|: s48 >= 0, s48 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s), 1 + (1 + (1 + s'))) + SQR(1 + (z - 2)) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s''), 1 + 0) + SQR(1 + (z - 2)) :|: s'' >= 0, s'' <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s5), 1 + (1 + s6)) + SQR(1 + (z - 2)) :|: s5 >= 0, s5 <= 2 * (z - 2), s6 >= 0, s6 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s7), 0) + SQR(1 + (z - 2)) :|: s7 >= 0, s7 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s1), 1 + (1 + (1 + s2))) + SQR(1 + (z - 2)) :|: s1 >= 0, s1 <= 2 * (z - 2), s2 >= 0, s2 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s10), 0) + SQR(1 + (z - 2)) :|: s10 >= 0, s10 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s3), 1 + 0) + SQR(1 + (z - 2)) :|: s3 >= 0, s3 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s8), 1 + (1 + s9)) + SQR(1 + (z - 2)) :|: s8 >= 0, s8 <= 2 * (z - 2), s9 >= 0, s9 <= 2 * (z - 2), z - 2 >= 0 double(z) -{ 0 }-> 0 :|: z = 0 double(z) -{ 0 }-> 0 :|: z >= 0 double(z) -{ 0 }-> 1 + (1 + s40) :|: s40 >= 0, s40 <= 2 * (z - 1), z - 1 >= 0 plus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 plus(z, z') -{ 0 }-> 1 + s62 :|: s62 >= 0, s62 <= z + (z' - 1), z' - 1 >= 0, z >= 0 sqr(z) -{ 0 }-> s56 :|: s56 >= 0, s56 <= 0 + (1 + 0), z = 1 + 0 sqr(z) -{ 0 }-> s57 :|: s57 >= 0, s57 <= 0 + (1 + (1 + (1 + s32))), s32 >= 0, s32 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> s58 :|: s58 >= 0, s58 <= 0 + (1 + 0), z - 1 >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + s26), 1 + (1 + (1 + s27))) :|: s26 >= 0, s26 <= 2 * (z - 2), s27 >= 0, s27 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + s28), 1 + 0) :|: s28 >= 0, s28 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), s29), 1 + (1 + (1 + s30))) :|: s29 >= 0, s29 <= 2 * (z - 2), s30 >= 0, s30 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), s31), 1 + 0) :|: s31 >= 0, s31 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 0 :|: z = 0 sqr(z) -{ 0 }-> 0 :|: z >= 0 sqr(z) -{ 0 }-> 1 + s59 :|: s59 >= 0, s59 <= 0 + 0, z = 1 + 0 sqr(z) -{ 0 }-> 1 + s60 :|: s60 >= 0, s60 <= 0 + (1 + (1 + s39)), s39 >= 0, s39 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + s61 :|: s61 >= 0, s61 <= 0 + 0, z - 1 >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + s33), 1 + (1 + s34)) :|: s33 >= 0, s33 <= 2 * (z - 2), s34 >= 0, s34 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + s35), 0) :|: s35 >= 0, s35 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), s36), 1 + (1 + s37)) :|: s36 >= 0, s36 <= 2 * (z - 2), s37 >= 0, s37 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), s38), 0) :|: s38 >= 0, s38 <= 2 * (z - 2), z - 2 >= 0 Function symbols to be analyzed: {sqr}, {SQR} Previous analysis results are: double: runtime: O(1) [0], size: O(n^1) [2*z] DOUBLE: runtime: O(n^1) [z], size: O(1) [0] +': runtime: O(n^1) [z'], size: O(1) [0] plus: runtime: O(1) [0], size: O(n^1) [z + z'] ---------------------------------------- (51) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: sqr after applying outer abstraction to obtain an ITS, resulting in: O(n^2) with polynomial bound: 5 + 12*z + 8*z^2 ---------------------------------------- (52) Obligation: Complexity RNTS consisting of the following rules: +'(z, z') -{ z' }-> 1 + s49 :|: s49 >= 0, s49 <= 0, z' - 1 >= 0, z >= 0 DOUBLE(z) -{ z }-> 1 + s41 :|: s41 >= 0, s41 <= 0, z - 1 >= 0 SQR(z) -{ z }-> 1 + s42 :|: s42 >= 0, s42 <= 0, z - 1 >= 0 SQR(z) -{ 2 }-> 1 + s50 :|: s50 >= 0, s50 <= 0, z = 1 + 0 SQR(z) -{ 4 + s18 }-> 1 + s51 :|: s51 >= 0, s51 <= 0, s18 >= 0, s18 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s52 :|: s52 >= 0, s52 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + s53 :|: s53 >= 0, s53 <= 0, z = 1 + 0 SQR(z) -{ 3 + s25 }-> 1 + s54 :|: s54 >= 0, s54 <= 0, s25 >= 0, s25 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + s55 :|: s55 >= 0, s55 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s12), 1 + (1 + (1 + s13))) :|: s12 >= 0, s12 <= 2 * (z - 2), s13 >= 0, s13 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s14), 1 + 0) :|: s14 >= 0, s14 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s19), 1 + (1 + s20)) :|: s19 >= 0, s19 <= 2 * (z - 2), s20 >= 0, s20 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s21), 0) :|: s21 >= 0, s21 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s15), 1 + (1 + (1 + s16))) :|: s15 >= 0, s15 <= 2 * (z - 2), s16 >= 0, s16 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s17), 1 + 0) :|: s17 >= 0, s17 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s22), 1 + (1 + s23)) :|: s22 >= 0, s22 <= 2 * (z - 2), s23 >= 0, s23 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s24), 0) :|: s24 >= 0, s24 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s43 + SQR(0) :|: s43 >= 0, s43 <= 0, z = 1 + 0 SQR(z) -{ 4 + s4 }-> 1 + s44 + SQR(1 + (z - 2)) :|: s44 >= 0, s44 <= 0, s4 >= 0, s4 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s45 + SQR(z - 1) :|: s45 >= 0, s45 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + s46 + SQR(0) :|: s46 >= 0, s46 <= 0, z = 1 + 0 SQR(z) -{ 3 + s11 }-> 1 + s47 + SQR(1 + (z - 2)) :|: s47 >= 0, s47 <= 0, s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + s48 + SQR(z - 1) :|: s48 >= 0, s48 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s), 1 + (1 + (1 + s'))) + SQR(1 + (z - 2)) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s''), 1 + 0) + SQR(1 + (z - 2)) :|: s'' >= 0, s'' <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s5), 1 + (1 + s6)) + SQR(1 + (z - 2)) :|: s5 >= 0, s5 <= 2 * (z - 2), s6 >= 0, s6 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s7), 0) + SQR(1 + (z - 2)) :|: s7 >= 0, s7 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s1), 1 + (1 + (1 + s2))) + SQR(1 + (z - 2)) :|: s1 >= 0, s1 <= 2 * (z - 2), s2 >= 0, s2 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s10), 0) + SQR(1 + (z - 2)) :|: s10 >= 0, s10 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s3), 1 + 0) + SQR(1 + (z - 2)) :|: s3 >= 0, s3 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s8), 1 + (1 + s9)) + SQR(1 + (z - 2)) :|: s8 >= 0, s8 <= 2 * (z - 2), s9 >= 0, s9 <= 2 * (z - 2), z - 2 >= 0 double(z) -{ 0 }-> 0 :|: z = 0 double(z) -{ 0 }-> 0 :|: z >= 0 double(z) -{ 0 }-> 1 + (1 + s40) :|: s40 >= 0, s40 <= 2 * (z - 1), z - 1 >= 0 plus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 plus(z, z') -{ 0 }-> 1 + s62 :|: s62 >= 0, s62 <= z + (z' - 1), z' - 1 >= 0, z >= 0 sqr(z) -{ 0 }-> s56 :|: s56 >= 0, s56 <= 0 + (1 + 0), z = 1 + 0 sqr(z) -{ 0 }-> s57 :|: s57 >= 0, s57 <= 0 + (1 + (1 + (1 + s32))), s32 >= 0, s32 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> s58 :|: s58 >= 0, s58 <= 0 + (1 + 0), z - 1 >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + s26), 1 + (1 + (1 + s27))) :|: s26 >= 0, s26 <= 2 * (z - 2), s27 >= 0, s27 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + s28), 1 + 0) :|: s28 >= 0, s28 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), s29), 1 + (1 + (1 + s30))) :|: s29 >= 0, s29 <= 2 * (z - 2), s30 >= 0, s30 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), s31), 1 + 0) :|: s31 >= 0, s31 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 0 :|: z = 0 sqr(z) -{ 0 }-> 0 :|: z >= 0 sqr(z) -{ 0 }-> 1 + s59 :|: s59 >= 0, s59 <= 0 + 0, z = 1 + 0 sqr(z) -{ 0 }-> 1 + s60 :|: s60 >= 0, s60 <= 0 + (1 + (1 + s39)), s39 >= 0, s39 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + s61 :|: s61 >= 0, s61 <= 0 + 0, z - 1 >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + s33), 1 + (1 + s34)) :|: s33 >= 0, s33 <= 2 * (z - 2), s34 >= 0, s34 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + s35), 0) :|: s35 >= 0, s35 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), s36), 1 + (1 + s37)) :|: s36 >= 0, s36 <= 2 * (z - 2), s37 >= 0, s37 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), s38), 0) :|: s38 >= 0, s38 <= 2 * (z - 2), z - 2 >= 0 Function symbols to be analyzed: {sqr}, {SQR} Previous analysis results are: double: runtime: O(1) [0], size: O(n^1) [2*z] DOUBLE: runtime: O(n^1) [z], size: O(1) [0] +': runtime: O(n^1) [z'], size: O(1) [0] plus: runtime: O(1) [0], size: O(n^1) [z + z'] sqr: runtime: ?, size: O(n^2) [5 + 12*z + 8*z^2] ---------------------------------------- (53) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: sqr after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 0 ---------------------------------------- (54) Obligation: Complexity RNTS consisting of the following rules: +'(z, z') -{ z' }-> 1 + s49 :|: s49 >= 0, s49 <= 0, z' - 1 >= 0, z >= 0 DOUBLE(z) -{ z }-> 1 + s41 :|: s41 >= 0, s41 <= 0, z - 1 >= 0 SQR(z) -{ z }-> 1 + s42 :|: s42 >= 0, s42 <= 0, z - 1 >= 0 SQR(z) -{ 2 }-> 1 + s50 :|: s50 >= 0, s50 <= 0, z = 1 + 0 SQR(z) -{ 4 + s18 }-> 1 + s51 :|: s51 >= 0, s51 <= 0, s18 >= 0, s18 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s52 :|: s52 >= 0, s52 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + s53 :|: s53 >= 0, s53 <= 0, z = 1 + 0 SQR(z) -{ 3 + s25 }-> 1 + s54 :|: s54 >= 0, s54 <= 0, s25 >= 0, s25 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + s55 :|: s55 >= 0, s55 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s12), 1 + (1 + (1 + s13))) :|: s12 >= 0, s12 <= 2 * (z - 2), s13 >= 0, s13 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s14), 1 + 0) :|: s14 >= 0, s14 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s19), 1 + (1 + s20)) :|: s19 >= 0, s19 <= 2 * (z - 2), s20 >= 0, s20 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s21), 0) :|: s21 >= 0, s21 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s15), 1 + (1 + (1 + s16))) :|: s15 >= 0, s15 <= 2 * (z - 2), s16 >= 0, s16 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s17), 1 + 0) :|: s17 >= 0, s17 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s22), 1 + (1 + s23)) :|: s22 >= 0, s22 <= 2 * (z - 2), s23 >= 0, s23 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s24), 0) :|: s24 >= 0, s24 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s43 + SQR(0) :|: s43 >= 0, s43 <= 0, z = 1 + 0 SQR(z) -{ 4 + s4 }-> 1 + s44 + SQR(1 + (z - 2)) :|: s44 >= 0, s44 <= 0, s4 >= 0, s4 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s45 + SQR(z - 1) :|: s45 >= 0, s45 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + s46 + SQR(0) :|: s46 >= 0, s46 <= 0, z = 1 + 0 SQR(z) -{ 3 + s11 }-> 1 + s47 + SQR(1 + (z - 2)) :|: s47 >= 0, s47 <= 0, s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + s48 + SQR(z - 1) :|: s48 >= 0, s48 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s), 1 + (1 + (1 + s'))) + SQR(1 + (z - 2)) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s''), 1 + 0) + SQR(1 + (z - 2)) :|: s'' >= 0, s'' <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s5), 1 + (1 + s6)) + SQR(1 + (z - 2)) :|: s5 >= 0, s5 <= 2 * (z - 2), s6 >= 0, s6 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(plus(sqr(z - 2), 1 + s7), 0) + SQR(1 + (z - 2)) :|: s7 >= 0, s7 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s1), 1 + (1 + (1 + s2))) + SQR(1 + (z - 2)) :|: s1 >= 0, s1 <= 2 * (z - 2), s2 >= 0, s2 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s10), 0) + SQR(1 + (z - 2)) :|: s10 >= 0, s10 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s3), 1 + 0) + SQR(1 + (z - 2)) :|: s3 >= 0, s3 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + +'(1 + plus(sqr(z - 2), s8), 1 + (1 + s9)) + SQR(1 + (z - 2)) :|: s8 >= 0, s8 <= 2 * (z - 2), s9 >= 0, s9 <= 2 * (z - 2), z - 2 >= 0 double(z) -{ 0 }-> 0 :|: z = 0 double(z) -{ 0 }-> 0 :|: z >= 0 double(z) -{ 0 }-> 1 + (1 + s40) :|: s40 >= 0, s40 <= 2 * (z - 1), z - 1 >= 0 plus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 plus(z, z') -{ 0 }-> 1 + s62 :|: s62 >= 0, s62 <= z + (z' - 1), z' - 1 >= 0, z >= 0 sqr(z) -{ 0 }-> s56 :|: s56 >= 0, s56 <= 0 + (1 + 0), z = 1 + 0 sqr(z) -{ 0 }-> s57 :|: s57 >= 0, s57 <= 0 + (1 + (1 + (1 + s32))), s32 >= 0, s32 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> s58 :|: s58 >= 0, s58 <= 0 + (1 + 0), z - 1 >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + s26), 1 + (1 + (1 + s27))) :|: s26 >= 0, s26 <= 2 * (z - 2), s27 >= 0, s27 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(plus(sqr(z - 2), 1 + s28), 1 + 0) :|: s28 >= 0, s28 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), s29), 1 + (1 + (1 + s30))) :|: s29 >= 0, s29 <= 2 * (z - 2), s30 >= 0, s30 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> plus(1 + plus(sqr(z - 2), s31), 1 + 0) :|: s31 >= 0, s31 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 0 :|: z = 0 sqr(z) -{ 0 }-> 0 :|: z >= 0 sqr(z) -{ 0 }-> 1 + s59 :|: s59 >= 0, s59 <= 0 + 0, z = 1 + 0 sqr(z) -{ 0 }-> 1 + s60 :|: s60 >= 0, s60 <= 0 + (1 + (1 + s39)), s39 >= 0, s39 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + s61 :|: s61 >= 0, s61 <= 0 + 0, z - 1 >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + s33), 1 + (1 + s34)) :|: s33 >= 0, s33 <= 2 * (z - 2), s34 >= 0, s34 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(plus(sqr(z - 2), 1 + s35), 0) :|: s35 >= 0, s35 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), s36), 1 + (1 + s37)) :|: s36 >= 0, s36 <= 2 * (z - 2), s37 >= 0, s37 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + plus(1 + plus(sqr(z - 2), s38), 0) :|: s38 >= 0, s38 <= 2 * (z - 2), z - 2 >= 0 Function symbols to be analyzed: {SQR} Previous analysis results are: double: runtime: O(1) [0], size: O(n^1) [2*z] DOUBLE: runtime: O(n^1) [z], size: O(1) [0] +': runtime: O(n^1) [z'], size: O(1) [0] plus: runtime: O(1) [0], size: O(n^1) [z + z'] sqr: runtime: O(1) [0], size: O(n^2) [5 + 12*z + 8*z^2] ---------------------------------------- (55) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (56) Obligation: Complexity RNTS consisting of the following rules: +'(z, z') -{ z' }-> 1 + s49 :|: s49 >= 0, s49 <= 0, z' - 1 >= 0, z >= 0 DOUBLE(z) -{ z }-> 1 + s41 :|: s41 >= 0, s41 <= 0, z - 1 >= 0 SQR(z) -{ 3 + s20 }-> 1 + s101 :|: s99 >= 0, s99 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s100 >= 0, s100 <= s99 + (1 + s19), s101 >= 0, s101 <= 0, s19 >= 0, s19 <= 2 * (z - 2), s20 >= 0, s20 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + s104 :|: s102 >= 0, s102 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s103 >= 0, s103 <= s102 + (1 + s21), s104 >= 0, s104 <= 0, s21 >= 0, s21 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 3 + s23 }-> 1 + s107 :|: s105 >= 0, s105 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s106 >= 0, s106 <= s105 + s22, s107 >= 0, s107 <= 0, s22 >= 0, s22 <= 2 * (z - 2), s23 >= 0, s23 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + s110 :|: s108 >= 0, s108 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s109 >= 0, s109 <= s108 + s24, s110 >= 0, s110 <= 0, s24 >= 0, s24 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ z }-> 1 + s42 :|: s42 >= 0, s42 <= 0, z - 1 >= 0 SQR(z) -{ 2 }-> 1 + s50 :|: s50 >= 0, s50 <= 0, z = 1 + 0 SQR(z) -{ 4 + s18 }-> 1 + s51 :|: s51 >= 0, s51 <= 0, s18 >= 0, s18 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s52 :|: s52 >= 0, s52 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + s53 :|: s53 >= 0, s53 <= 0, z = 1 + 0 SQR(z) -{ 3 + s25 }-> 1 + s54 :|: s54 >= 0, s54 <= 0, s25 >= 0, s25 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + s55 :|: s55 >= 0, s55 <= 0, z - 1 >= 0 SQR(z) -{ 4 + s13 }-> 1 + s89 :|: s87 >= 0, s87 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s88 >= 0, s88 <= s87 + (1 + s12), s89 >= 0, s89 <= 0, s12 >= 0, s12 <= 2 * (z - 2), s13 >= 0, s13 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s92 :|: s90 >= 0, s90 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s91 >= 0, s91 <= s90 + (1 + s14), s92 >= 0, s92 <= 0, s14 >= 0, s14 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 4 + s16 }-> 1 + s95 :|: s93 >= 0, s93 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s94 >= 0, s94 <= s93 + s15, s95 >= 0, s95 <= 0, s15 >= 0, s15 <= 2 * (z - 2), s16 >= 0, s16 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s98 :|: s96 >= 0, s96 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s97 >= 0, s97 <= s96 + s17, s98 >= 0, s98 <= 0, s17 >= 0, s17 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s43 + SQR(0) :|: s43 >= 0, s43 <= 0, z = 1 + 0 SQR(z) -{ 4 + s4 }-> 1 + s44 + SQR(1 + (z - 2)) :|: s44 >= 0, s44 <= 0, s4 >= 0, s4 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s45 + SQR(z - 1) :|: s45 >= 0, s45 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + s46 + SQR(0) :|: s46 >= 0, s46 <= 0, z = 1 + 0 SQR(z) -{ 3 + s11 }-> 1 + s47 + SQR(1 + (z - 2)) :|: s47 >= 0, s47 <= 0, s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + s48 + SQR(z - 1) :|: s48 >= 0, s48 <= 0, z - 1 >= 0 SQR(z) -{ 4 + s' }-> 1 + s65 + SQR(1 + (z - 2)) :|: s63 >= 0, s63 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s64 >= 0, s64 <= s63 + (1 + s), s65 >= 0, s65 <= 0, s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s68 + SQR(1 + (z - 2)) :|: s66 >= 0, s66 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s67 >= 0, s67 <= s66 + (1 + s''), s68 >= 0, s68 <= 0, s'' >= 0, s'' <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 4 + s2 }-> 1 + s71 + SQR(1 + (z - 2)) :|: s69 >= 0, s69 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s70 >= 0, s70 <= s69 + s1, s71 >= 0, s71 <= 0, s1 >= 0, s1 <= 2 * (z - 2), s2 >= 0, s2 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s74 + SQR(1 + (z - 2)) :|: s72 >= 0, s72 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s73 >= 0, s73 <= s72 + s3, s74 >= 0, s74 <= 0, s3 >= 0, s3 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 3 + s6 }-> 1 + s77 + SQR(1 + (z - 2)) :|: s75 >= 0, s75 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s76 >= 0, s76 <= s75 + (1 + s5), s77 >= 0, s77 <= 0, s5 >= 0, s5 <= 2 * (z - 2), s6 >= 0, s6 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + s80 + SQR(1 + (z - 2)) :|: s78 >= 0, s78 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s79 >= 0, s79 <= s78 + (1 + s7), s80 >= 0, s80 <= 0, s7 >= 0, s7 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 3 + s9 }-> 1 + s83 + SQR(1 + (z - 2)) :|: s81 >= 0, s81 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s82 >= 0, s82 <= s81 + s8, s83 >= 0, s83 <= 0, s8 >= 0, s8 <= 2 * (z - 2), s9 >= 0, s9 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + s86 + SQR(1 + (z - 2)) :|: s84 >= 0, s84 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s85 >= 0, s85 <= s84 + s10, s86 >= 0, s86 <= 0, s10 >= 0, s10 <= 2 * (z - 2), z - 2 >= 0 double(z) -{ 0 }-> 0 :|: z = 0 double(z) -{ 0 }-> 0 :|: z >= 0 double(z) -{ 0 }-> 1 + (1 + s40) :|: s40 >= 0, s40 <= 2 * (z - 1), z - 1 >= 0 plus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 plus(z, z') -{ 0 }-> 1 + s62 :|: s62 >= 0, s62 <= z + (z' - 1), z' - 1 >= 0, z >= 0 sqr(z) -{ 0 }-> s113 :|: s111 >= 0, s111 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s112 >= 0, s112 <= s111 + (1 + s26), s113 >= 0, s113 <= s112 + (1 + (1 + (1 + s27))), s26 >= 0, s26 <= 2 * (z - 2), s27 >= 0, s27 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> s116 :|: s114 >= 0, s114 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s115 >= 0, s115 <= s114 + (1 + s28), s116 >= 0, s116 <= s115 + (1 + 0), s28 >= 0, s28 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> s119 :|: s117 >= 0, s117 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s118 >= 0, s118 <= s117 + s29, s119 >= 0, s119 <= 1 + s118 + (1 + (1 + (1 + s30))), s29 >= 0, s29 <= 2 * (z - 2), s30 >= 0, s30 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> s122 :|: s120 >= 0, s120 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s121 >= 0, s121 <= s120 + s31, s122 >= 0, s122 <= 1 + s121 + (1 + 0), s31 >= 0, s31 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> s56 :|: s56 >= 0, s56 <= 0 + (1 + 0), z = 1 + 0 sqr(z) -{ 0 }-> s57 :|: s57 >= 0, s57 <= 0 + (1 + (1 + (1 + s32))), s32 >= 0, s32 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> s58 :|: s58 >= 0, s58 <= 0 + (1 + 0), z - 1 >= 0 sqr(z) -{ 0 }-> 0 :|: z = 0 sqr(z) -{ 0 }-> 0 :|: z >= 0 sqr(z) -{ 0 }-> 1 + s125 :|: s123 >= 0, s123 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s124 >= 0, s124 <= s123 + (1 + s33), s125 >= 0, s125 <= s124 + (1 + (1 + s34)), s33 >= 0, s33 <= 2 * (z - 2), s34 >= 0, s34 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + s128 :|: s126 >= 0, s126 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s127 >= 0, s127 <= s126 + (1 + s35), s128 >= 0, s128 <= s127 + 0, s35 >= 0, s35 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + s131 :|: s129 >= 0, s129 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s130 >= 0, s130 <= s129 + s36, s131 >= 0, s131 <= 1 + s130 + (1 + (1 + s37)), s36 >= 0, s36 <= 2 * (z - 2), s37 >= 0, s37 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + s134 :|: s132 >= 0, s132 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s133 >= 0, s133 <= s132 + s38, s134 >= 0, s134 <= 1 + s133 + 0, s38 >= 0, s38 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + s59 :|: s59 >= 0, s59 <= 0 + 0, z = 1 + 0 sqr(z) -{ 0 }-> 1 + s60 :|: s60 >= 0, s60 <= 0 + (1 + (1 + s39)), s39 >= 0, s39 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + s61 :|: s61 >= 0, s61 <= 0 + 0, z - 1 >= 0 Function symbols to be analyzed: {SQR} Previous analysis results are: double: runtime: O(1) [0], size: O(n^1) [2*z] DOUBLE: runtime: O(n^1) [z], size: O(1) [0] +': runtime: O(n^1) [z'], size: O(1) [0] plus: runtime: O(1) [0], size: O(n^1) [z + z'] sqr: runtime: O(1) [0], size: O(n^2) [5 + 12*z + 8*z^2] ---------------------------------------- (57) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using KoAT for: SQR 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: +'(z, z') -{ z' }-> 1 + s49 :|: s49 >= 0, s49 <= 0, z' - 1 >= 0, z >= 0 DOUBLE(z) -{ z }-> 1 + s41 :|: s41 >= 0, s41 <= 0, z - 1 >= 0 SQR(z) -{ 3 + s20 }-> 1 + s101 :|: s99 >= 0, s99 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s100 >= 0, s100 <= s99 + (1 + s19), s101 >= 0, s101 <= 0, s19 >= 0, s19 <= 2 * (z - 2), s20 >= 0, s20 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + s104 :|: s102 >= 0, s102 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s103 >= 0, s103 <= s102 + (1 + s21), s104 >= 0, s104 <= 0, s21 >= 0, s21 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 3 + s23 }-> 1 + s107 :|: s105 >= 0, s105 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s106 >= 0, s106 <= s105 + s22, s107 >= 0, s107 <= 0, s22 >= 0, s22 <= 2 * (z - 2), s23 >= 0, s23 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + s110 :|: s108 >= 0, s108 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s109 >= 0, s109 <= s108 + s24, s110 >= 0, s110 <= 0, s24 >= 0, s24 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ z }-> 1 + s42 :|: s42 >= 0, s42 <= 0, z - 1 >= 0 SQR(z) -{ 2 }-> 1 + s50 :|: s50 >= 0, s50 <= 0, z = 1 + 0 SQR(z) -{ 4 + s18 }-> 1 + s51 :|: s51 >= 0, s51 <= 0, s18 >= 0, s18 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s52 :|: s52 >= 0, s52 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + s53 :|: s53 >= 0, s53 <= 0, z = 1 + 0 SQR(z) -{ 3 + s25 }-> 1 + s54 :|: s54 >= 0, s54 <= 0, s25 >= 0, s25 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + s55 :|: s55 >= 0, s55 <= 0, z - 1 >= 0 SQR(z) -{ 4 + s13 }-> 1 + s89 :|: s87 >= 0, s87 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s88 >= 0, s88 <= s87 + (1 + s12), s89 >= 0, s89 <= 0, s12 >= 0, s12 <= 2 * (z - 2), s13 >= 0, s13 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s92 :|: s90 >= 0, s90 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s91 >= 0, s91 <= s90 + (1 + s14), s92 >= 0, s92 <= 0, s14 >= 0, s14 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 4 + s16 }-> 1 + s95 :|: s93 >= 0, s93 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s94 >= 0, s94 <= s93 + s15, s95 >= 0, s95 <= 0, s15 >= 0, s15 <= 2 * (z - 2), s16 >= 0, s16 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s98 :|: s96 >= 0, s96 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s97 >= 0, s97 <= s96 + s17, s98 >= 0, s98 <= 0, s17 >= 0, s17 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s43 + SQR(0) :|: s43 >= 0, s43 <= 0, z = 1 + 0 SQR(z) -{ 4 + s4 }-> 1 + s44 + SQR(1 + (z - 2)) :|: s44 >= 0, s44 <= 0, s4 >= 0, s4 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s45 + SQR(z - 1) :|: s45 >= 0, s45 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + s46 + SQR(0) :|: s46 >= 0, s46 <= 0, z = 1 + 0 SQR(z) -{ 3 + s11 }-> 1 + s47 + SQR(1 + (z - 2)) :|: s47 >= 0, s47 <= 0, s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + s48 + SQR(z - 1) :|: s48 >= 0, s48 <= 0, z - 1 >= 0 SQR(z) -{ 4 + s' }-> 1 + s65 + SQR(1 + (z - 2)) :|: s63 >= 0, s63 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s64 >= 0, s64 <= s63 + (1 + s), s65 >= 0, s65 <= 0, s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s68 + SQR(1 + (z - 2)) :|: s66 >= 0, s66 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s67 >= 0, s67 <= s66 + (1 + s''), s68 >= 0, s68 <= 0, s'' >= 0, s'' <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 4 + s2 }-> 1 + s71 + SQR(1 + (z - 2)) :|: s69 >= 0, s69 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s70 >= 0, s70 <= s69 + s1, s71 >= 0, s71 <= 0, s1 >= 0, s1 <= 2 * (z - 2), s2 >= 0, s2 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s74 + SQR(1 + (z - 2)) :|: s72 >= 0, s72 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s73 >= 0, s73 <= s72 + s3, s74 >= 0, s74 <= 0, s3 >= 0, s3 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 3 + s6 }-> 1 + s77 + SQR(1 + (z - 2)) :|: s75 >= 0, s75 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s76 >= 0, s76 <= s75 + (1 + s5), s77 >= 0, s77 <= 0, s5 >= 0, s5 <= 2 * (z - 2), s6 >= 0, s6 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + s80 + SQR(1 + (z - 2)) :|: s78 >= 0, s78 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s79 >= 0, s79 <= s78 + (1 + s7), s80 >= 0, s80 <= 0, s7 >= 0, s7 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 3 + s9 }-> 1 + s83 + SQR(1 + (z - 2)) :|: s81 >= 0, s81 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s82 >= 0, s82 <= s81 + s8, s83 >= 0, s83 <= 0, s8 >= 0, s8 <= 2 * (z - 2), s9 >= 0, s9 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + s86 + SQR(1 + (z - 2)) :|: s84 >= 0, s84 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s85 >= 0, s85 <= s84 + s10, s86 >= 0, s86 <= 0, s10 >= 0, s10 <= 2 * (z - 2), z - 2 >= 0 double(z) -{ 0 }-> 0 :|: z = 0 double(z) -{ 0 }-> 0 :|: z >= 0 double(z) -{ 0 }-> 1 + (1 + s40) :|: s40 >= 0, s40 <= 2 * (z - 1), z - 1 >= 0 plus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 plus(z, z') -{ 0 }-> 1 + s62 :|: s62 >= 0, s62 <= z + (z' - 1), z' - 1 >= 0, z >= 0 sqr(z) -{ 0 }-> s113 :|: s111 >= 0, s111 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s112 >= 0, s112 <= s111 + (1 + s26), s113 >= 0, s113 <= s112 + (1 + (1 + (1 + s27))), s26 >= 0, s26 <= 2 * (z - 2), s27 >= 0, s27 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> s116 :|: s114 >= 0, s114 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s115 >= 0, s115 <= s114 + (1 + s28), s116 >= 0, s116 <= s115 + (1 + 0), s28 >= 0, s28 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> s119 :|: s117 >= 0, s117 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s118 >= 0, s118 <= s117 + s29, s119 >= 0, s119 <= 1 + s118 + (1 + (1 + (1 + s30))), s29 >= 0, s29 <= 2 * (z - 2), s30 >= 0, s30 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> s122 :|: s120 >= 0, s120 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s121 >= 0, s121 <= s120 + s31, s122 >= 0, s122 <= 1 + s121 + (1 + 0), s31 >= 0, s31 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> s56 :|: s56 >= 0, s56 <= 0 + (1 + 0), z = 1 + 0 sqr(z) -{ 0 }-> s57 :|: s57 >= 0, s57 <= 0 + (1 + (1 + (1 + s32))), s32 >= 0, s32 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> s58 :|: s58 >= 0, s58 <= 0 + (1 + 0), z - 1 >= 0 sqr(z) -{ 0 }-> 0 :|: z = 0 sqr(z) -{ 0 }-> 0 :|: z >= 0 sqr(z) -{ 0 }-> 1 + s125 :|: s123 >= 0, s123 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s124 >= 0, s124 <= s123 + (1 + s33), s125 >= 0, s125 <= s124 + (1 + (1 + s34)), s33 >= 0, s33 <= 2 * (z - 2), s34 >= 0, s34 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + s128 :|: s126 >= 0, s126 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s127 >= 0, s127 <= s126 + (1 + s35), s128 >= 0, s128 <= s127 + 0, s35 >= 0, s35 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + s131 :|: s129 >= 0, s129 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s130 >= 0, s130 <= s129 + s36, s131 >= 0, s131 <= 1 + s130 + (1 + (1 + s37)), s36 >= 0, s36 <= 2 * (z - 2), s37 >= 0, s37 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + s134 :|: s132 >= 0, s132 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s133 >= 0, s133 <= s132 + s38, s134 >= 0, s134 <= 1 + s133 + 0, s38 >= 0, s38 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + s59 :|: s59 >= 0, s59 <= 0 + 0, z = 1 + 0 sqr(z) -{ 0 }-> 1 + s60 :|: s60 >= 0, s60 <= 0 + (1 + (1 + s39)), s39 >= 0, s39 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + s61 :|: s61 >= 0, s61 <= 0 + 0, z - 1 >= 0 Function symbols to be analyzed: {SQR} Previous analysis results are: double: runtime: O(1) [0], size: O(n^1) [2*z] DOUBLE: runtime: O(n^1) [z], size: O(1) [0] +': runtime: O(n^1) [z'], size: O(1) [0] plus: runtime: O(1) [0], size: O(n^1) [z + z'] sqr: runtime: O(1) [0], size: O(n^2) [5 + 12*z + 8*z^2] SQR: runtime: ?, size: O(n^1) [z] ---------------------------------------- (59) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: SQR after applying outer abstraction to obtain an ITS, resulting in: O(n^2) with polynomial bound: 4 + 6*z + 4*z^2 ---------------------------------------- (60) Obligation: Complexity RNTS consisting of the following rules: +'(z, z') -{ z' }-> 1 + s49 :|: s49 >= 0, s49 <= 0, z' - 1 >= 0, z >= 0 DOUBLE(z) -{ z }-> 1 + s41 :|: s41 >= 0, s41 <= 0, z - 1 >= 0 SQR(z) -{ 3 + s20 }-> 1 + s101 :|: s99 >= 0, s99 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s100 >= 0, s100 <= s99 + (1 + s19), s101 >= 0, s101 <= 0, s19 >= 0, s19 <= 2 * (z - 2), s20 >= 0, s20 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + s104 :|: s102 >= 0, s102 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s103 >= 0, s103 <= s102 + (1 + s21), s104 >= 0, s104 <= 0, s21 >= 0, s21 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 3 + s23 }-> 1 + s107 :|: s105 >= 0, s105 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s106 >= 0, s106 <= s105 + s22, s107 >= 0, s107 <= 0, s22 >= 0, s22 <= 2 * (z - 2), s23 >= 0, s23 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + s110 :|: s108 >= 0, s108 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s109 >= 0, s109 <= s108 + s24, s110 >= 0, s110 <= 0, s24 >= 0, s24 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ z }-> 1 + s42 :|: s42 >= 0, s42 <= 0, z - 1 >= 0 SQR(z) -{ 2 }-> 1 + s50 :|: s50 >= 0, s50 <= 0, z = 1 + 0 SQR(z) -{ 4 + s18 }-> 1 + s51 :|: s51 >= 0, s51 <= 0, s18 >= 0, s18 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s52 :|: s52 >= 0, s52 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + s53 :|: s53 >= 0, s53 <= 0, z = 1 + 0 SQR(z) -{ 3 + s25 }-> 1 + s54 :|: s54 >= 0, s54 <= 0, s25 >= 0, s25 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + s55 :|: s55 >= 0, s55 <= 0, z - 1 >= 0 SQR(z) -{ 4 + s13 }-> 1 + s89 :|: s87 >= 0, s87 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s88 >= 0, s88 <= s87 + (1 + s12), s89 >= 0, s89 <= 0, s12 >= 0, s12 <= 2 * (z - 2), s13 >= 0, s13 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s92 :|: s90 >= 0, s90 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s91 >= 0, s91 <= s90 + (1 + s14), s92 >= 0, s92 <= 0, s14 >= 0, s14 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 4 + s16 }-> 1 + s95 :|: s93 >= 0, s93 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s94 >= 0, s94 <= s93 + s15, s95 >= 0, s95 <= 0, s15 >= 0, s15 <= 2 * (z - 2), s16 >= 0, s16 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s98 :|: s96 >= 0, s96 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s97 >= 0, s97 <= s96 + s17, s98 >= 0, s98 <= 0, s17 >= 0, s17 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s43 + SQR(0) :|: s43 >= 0, s43 <= 0, z = 1 + 0 SQR(z) -{ 4 + s4 }-> 1 + s44 + SQR(1 + (z - 2)) :|: s44 >= 0, s44 <= 0, s4 >= 0, s4 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s45 + SQR(z - 1) :|: s45 >= 0, s45 <= 0, z - 1 >= 0 SQR(z) -{ 1 }-> 1 + s46 + SQR(0) :|: s46 >= 0, s46 <= 0, z = 1 + 0 SQR(z) -{ 3 + s11 }-> 1 + s47 + SQR(1 + (z - 2)) :|: s47 >= 0, s47 <= 0, s11 >= 0, s11 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + s48 + SQR(z - 1) :|: s48 >= 0, s48 <= 0, z - 1 >= 0 SQR(z) -{ 4 + s' }-> 1 + s65 + SQR(1 + (z - 2)) :|: s63 >= 0, s63 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s64 >= 0, s64 <= s63 + (1 + s), s65 >= 0, s65 <= 0, s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s68 + SQR(1 + (z - 2)) :|: s66 >= 0, s66 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s67 >= 0, s67 <= s66 + (1 + s''), s68 >= 0, s68 <= 0, s'' >= 0, s'' <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 4 + s2 }-> 1 + s71 + SQR(1 + (z - 2)) :|: s69 >= 0, s69 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s70 >= 0, s70 <= s69 + s1, s71 >= 0, s71 <= 0, s1 >= 0, s1 <= 2 * (z - 2), s2 >= 0, s2 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 2 }-> 1 + s74 + SQR(1 + (z - 2)) :|: s72 >= 0, s72 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s73 >= 0, s73 <= s72 + s3, s74 >= 0, s74 <= 0, s3 >= 0, s3 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 3 + s6 }-> 1 + s77 + SQR(1 + (z - 2)) :|: s75 >= 0, s75 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s76 >= 0, s76 <= s75 + (1 + s5), s77 >= 0, s77 <= 0, s5 >= 0, s5 <= 2 * (z - 2), s6 >= 0, s6 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + s80 + SQR(1 + (z - 2)) :|: s78 >= 0, s78 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s79 >= 0, s79 <= s78 + (1 + s7), s80 >= 0, s80 <= 0, s7 >= 0, s7 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 3 + s9 }-> 1 + s83 + SQR(1 + (z - 2)) :|: s81 >= 0, s81 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s82 >= 0, s82 <= s81 + s8, s83 >= 0, s83 <= 0, s8 >= 0, s8 <= 2 * (z - 2), s9 >= 0, s9 <= 2 * (z - 2), z - 2 >= 0 SQR(z) -{ 1 }-> 1 + s86 + SQR(1 + (z - 2)) :|: s84 >= 0, s84 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s85 >= 0, s85 <= s84 + s10, s86 >= 0, s86 <= 0, s10 >= 0, s10 <= 2 * (z - 2), z - 2 >= 0 double(z) -{ 0 }-> 0 :|: z = 0 double(z) -{ 0 }-> 0 :|: z >= 0 double(z) -{ 0 }-> 1 + (1 + s40) :|: s40 >= 0, s40 <= 2 * (z - 1), z - 1 >= 0 plus(z, z') -{ 0 }-> z :|: z >= 0, z' = 0 plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 plus(z, z') -{ 0 }-> 1 + s62 :|: s62 >= 0, s62 <= z + (z' - 1), z' - 1 >= 0, z >= 0 sqr(z) -{ 0 }-> s113 :|: s111 >= 0, s111 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s112 >= 0, s112 <= s111 + (1 + s26), s113 >= 0, s113 <= s112 + (1 + (1 + (1 + s27))), s26 >= 0, s26 <= 2 * (z - 2), s27 >= 0, s27 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> s116 :|: s114 >= 0, s114 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s115 >= 0, s115 <= s114 + (1 + s28), s116 >= 0, s116 <= s115 + (1 + 0), s28 >= 0, s28 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> s119 :|: s117 >= 0, s117 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s118 >= 0, s118 <= s117 + s29, s119 >= 0, s119 <= 1 + s118 + (1 + (1 + (1 + s30))), s29 >= 0, s29 <= 2 * (z - 2), s30 >= 0, s30 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> s122 :|: s120 >= 0, s120 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s121 >= 0, s121 <= s120 + s31, s122 >= 0, s122 <= 1 + s121 + (1 + 0), s31 >= 0, s31 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> s56 :|: s56 >= 0, s56 <= 0 + (1 + 0), z = 1 + 0 sqr(z) -{ 0 }-> s57 :|: s57 >= 0, s57 <= 0 + (1 + (1 + (1 + s32))), s32 >= 0, s32 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> s58 :|: s58 >= 0, s58 <= 0 + (1 + 0), z - 1 >= 0 sqr(z) -{ 0 }-> 0 :|: z = 0 sqr(z) -{ 0 }-> 0 :|: z >= 0 sqr(z) -{ 0 }-> 1 + s125 :|: s123 >= 0, s123 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s124 >= 0, s124 <= s123 + (1 + s33), s125 >= 0, s125 <= s124 + (1 + (1 + s34)), s33 >= 0, s33 <= 2 * (z - 2), s34 >= 0, s34 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + s128 :|: s126 >= 0, s126 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s127 >= 0, s127 <= s126 + (1 + s35), s128 >= 0, s128 <= s127 + 0, s35 >= 0, s35 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + s131 :|: s129 >= 0, s129 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s130 >= 0, s130 <= s129 + s36, s131 >= 0, s131 <= 1 + s130 + (1 + (1 + s37)), s36 >= 0, s36 <= 2 * (z - 2), s37 >= 0, s37 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + s134 :|: s132 >= 0, s132 <= 5 + 12 * (z - 2) + 8 * ((z - 2) * (z - 2)), s133 >= 0, s133 <= s132 + s38, s134 >= 0, s134 <= 1 + s133 + 0, s38 >= 0, s38 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + s59 :|: s59 >= 0, s59 <= 0 + 0, z = 1 + 0 sqr(z) -{ 0 }-> 1 + s60 :|: s60 >= 0, s60 <= 0 + (1 + (1 + s39)), s39 >= 0, s39 <= 2 * (z - 2), z - 2 >= 0 sqr(z) -{ 0 }-> 1 + s61 :|: s61 >= 0, s61 <= 0 + 0, z - 1 >= 0 Function symbols to be analyzed: Previous analysis results are: double: runtime: O(1) [0], size: O(n^1) [2*z] DOUBLE: runtime: O(n^1) [z], size: O(1) [0] +': runtime: O(n^1) [z'], size: O(1) [0] plus: runtime: O(1) [0], size: O(n^1) [z + z'] sqr: runtime: O(1) [0], size: O(n^2) [5 + 12*z + 8*z^2] SQR: runtime: O(n^2) [4 + 6*z + 4*z^2], size: O(n^1) [z] ---------------------------------------- (61) FinalProof (FINISHED) Computed overall runtime complexity ---------------------------------------- (62) BOUNDS(1, n^2)