WORST_CASE(Omega(n^1),O(n^1)) proof of /export/starexec/sandbox/benchmark/theBenchmark.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 843 ms] (2) CpxRelTRS (3) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (4) CpxWeightedTrs (5) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CpxTypedWeightedTrs (7) CompletionProof [UPPER BOUND(ID), 0 ms] (8) CpxTypedWeightedCompleteTrs (9) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (10) CpxTypedWeightedCompleteTrs (11) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 17 ms] (12) CpxRNTS (13) InliningProof [UPPER BOUND(ID), 693 ms] (14) CpxRNTS (15) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms] (16) CpxRNTS (17) CpxRntsAnalysisOrderProof [BOTH BOUNDS(ID, ID), 0 ms] (18) CpxRNTS (19) ResultPropagationProof [UPPER BOUND(ID), 3 ms] (20) CpxRNTS (21) IntTrsBoundProof [UPPER BOUND(ID), 92 ms] (22) CpxRNTS (23) IntTrsBoundProof [UPPER BOUND(ID), 37 ms] (24) CpxRNTS (25) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (26) CpxRNTS (27) IntTrsBoundProof [UPPER BOUND(ID), 376 ms] (28) CpxRNTS (29) IntTrsBoundProof [UPPER BOUND(ID), 146 ms] (30) CpxRNTS (31) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (32) CpxRNTS (33) IntTrsBoundProof [UPPER BOUND(ID), 281 ms] (34) CpxRNTS (35) IntTrsBoundProof [UPPER BOUND(ID), 16 ms] (36) CpxRNTS (37) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (38) CpxRNTS (39) IntTrsBoundProof [UPPER BOUND(ID), 5579 ms] (40) CpxRNTS (41) IntTrsBoundProof [UPPER BOUND(ID), 3369 ms] (42) CpxRNTS (43) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (44) CpxRNTS (45) IntTrsBoundProof [UPPER BOUND(ID), 122 ms] (46) CpxRNTS (47) IntTrsBoundProof [UPPER BOUND(ID), 4 ms] (48) CpxRNTS (49) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (50) CpxRNTS (51) IntTrsBoundProof [UPPER BOUND(ID), 7543 ms] (52) CpxRNTS (53) IntTrsBoundProof [UPPER BOUND(ID), 3815 ms] (54) CpxRNTS (55) FinalProof [FINISHED, 0 ms] (56) BOUNDS(1, n^1) (57) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (58) TRS for Loop Detection (59) DecreasingLoopProof [LOWER BOUND(ID), 0 ms] (60) BEST (61) proven lower bound (62) LowerBoundPropagationProof [FINISHED, 0 ms] (63) BOUNDS(n^1, INF) (64) TRS for Loop Detection ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: COND1(true, z0, z1) -> c(COND2(gr(z1, 0), z0, z1), GR(z1, 0)) COND2(true, z0, z1) -> c1(COND2(gr(z1, 0), z0, p(z1)), GR(z1, 0)) COND2(true, z0, z1) -> c2(COND2(gr(z1, 0), z0, p(z1)), P(z1)) COND2(false, z0, z1) -> c3(COND1(gr(z0, 0), p(z0), z1), GR(z0, 0)) COND2(false, z0, z1) -> c4(COND1(gr(z0, 0), p(z0), z1), P(z0)) GR(0, z0) -> c5 GR(s(z0), 0) -> c6 GR(s(z0), s(z1)) -> c7(GR(z0, z1)) P(0) -> c8 P(s(z0)) -> c9 The (relative) TRS S consists of the following rules: cond1(true, z0, z1) -> cond2(gr(z1, 0), z0, z1) cond2(true, z0, z1) -> cond2(gr(z1, 0), z0, p(z1)) cond2(false, z0, z1) -> cond1(gr(z0, 0), p(z0), z1) gr(0, z0) -> false gr(s(z0), 0) -> true gr(s(z0), s(z1)) -> gr(z0, z1) p(0) -> 0 p(s(z0)) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID)) proved innermost termination of relative rules ---------------------------------------- (2) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: COND1(true, z0, z1) -> c(COND2(gr(z1, 0), z0, z1), GR(z1, 0)) COND2(true, z0, z1) -> c1(COND2(gr(z1, 0), z0, p(z1)), GR(z1, 0)) COND2(true, z0, z1) -> c2(COND2(gr(z1, 0), z0, p(z1)), P(z1)) COND2(false, z0, z1) -> c3(COND1(gr(z0, 0), p(z0), z1), GR(z0, 0)) COND2(false, z0, z1) -> c4(COND1(gr(z0, 0), p(z0), z1), P(z0)) GR(0, z0) -> c5 GR(s(z0), 0) -> c6 GR(s(z0), s(z1)) -> c7(GR(z0, z1)) P(0) -> c8 P(s(z0)) -> c9 The (relative) TRS S consists of the following rules: cond1(true, z0, z1) -> cond2(gr(z1, 0), z0, z1) cond2(true, z0, z1) -> cond2(gr(z1, 0), z0, p(z1)) cond2(false, z0, z1) -> cond1(gr(z0, 0), p(z0), z1) gr(0, z0) -> false gr(s(z0), 0) -> true gr(s(z0), s(z1)) -> gr(z0, z1) p(0) -> 0 p(s(z0)) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (3) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID)) Transformed relative TRS to weighted TRS ---------------------------------------- (4) Obligation: The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1). The TRS R consists of the following rules: COND1(true, z0, z1) -> c(COND2(gr(z1, 0), z0, z1), GR(z1, 0)) [1] COND2(true, z0, z1) -> c1(COND2(gr(z1, 0), z0, p(z1)), GR(z1, 0)) [1] COND2(true, z0, z1) -> c2(COND2(gr(z1, 0), z0, p(z1)), P(z1)) [1] COND2(false, z0, z1) -> c3(COND1(gr(z0, 0), p(z0), z1), GR(z0, 0)) [1] COND2(false, z0, z1) -> c4(COND1(gr(z0, 0), p(z0), z1), P(z0)) [1] GR(0, z0) -> c5 [1] GR(s(z0), 0) -> c6 [1] GR(s(z0), s(z1)) -> c7(GR(z0, z1)) [1] P(0) -> c8 [1] P(s(z0)) -> c9 [1] cond1(true, z0, z1) -> cond2(gr(z1, 0), z0, z1) [0] cond2(true, z0, z1) -> cond2(gr(z1, 0), z0, p(z1)) [0] cond2(false, z0, z1) -> cond1(gr(z0, 0), p(z0), z1) [0] gr(0, z0) -> false [0] gr(s(z0), 0) -> true [0] gr(s(z0), s(z1)) -> gr(z0, z1) [0] p(0) -> 0 [0] p(s(z0)) -> z0 [0] Rewrite Strategy: INNERMOST ---------------------------------------- (5) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (6) Obligation: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: COND1(true, z0, z1) -> c(COND2(gr(z1, 0), z0, z1), GR(z1, 0)) [1] COND2(true, z0, z1) -> c1(COND2(gr(z1, 0), z0, p(z1)), GR(z1, 0)) [1] COND2(true, z0, z1) -> c2(COND2(gr(z1, 0), z0, p(z1)), P(z1)) [1] COND2(false, z0, z1) -> c3(COND1(gr(z0, 0), p(z0), z1), GR(z0, 0)) [1] COND2(false, z0, z1) -> c4(COND1(gr(z0, 0), p(z0), z1), P(z0)) [1] GR(0, z0) -> c5 [1] GR(s(z0), 0) -> c6 [1] GR(s(z0), s(z1)) -> c7(GR(z0, z1)) [1] P(0) -> c8 [1] P(s(z0)) -> c9 [1] cond1(true, z0, z1) -> cond2(gr(z1, 0), z0, z1) [0] cond2(true, z0, z1) -> cond2(gr(z1, 0), z0, p(z1)) [0] cond2(false, z0, z1) -> cond1(gr(z0, 0), p(z0), z1) [0] gr(0, z0) -> false [0] gr(s(z0), 0) -> true [0] gr(s(z0), s(z1)) -> gr(z0, z1) [0] p(0) -> 0 [0] p(s(z0)) -> z0 [0] The TRS has the following type information: COND1 :: true:false -> 0:s -> 0:s -> c true :: true:false c :: c1:c2:c3:c4 -> c5:c6:c7 -> c COND2 :: true:false -> 0:s -> 0:s -> c1:c2:c3:c4 gr :: 0:s -> 0:s -> true:false 0 :: 0:s GR :: 0:s -> 0:s -> c5:c6:c7 c1 :: c1:c2:c3:c4 -> c5:c6:c7 -> c1:c2:c3:c4 p :: 0:s -> 0:s c2 :: c1:c2:c3:c4 -> c8:c9 -> c1:c2:c3:c4 P :: 0:s -> c8:c9 false :: true:false c3 :: c -> c5:c6:c7 -> c1:c2:c3:c4 c4 :: c -> c8:c9 -> c1:c2:c3:c4 c5 :: c5:c6:c7 s :: 0:s -> 0:s c6 :: c5:c6:c7 c7 :: c5:c6:c7 -> c5:c6:c7 c8 :: c8:c9 c9 :: c8:c9 cond1 :: true:false -> 0:s -> 0:s -> cond1:cond2 cond2 :: true:false -> 0:s -> 0:s -> cond1:cond2 Rewrite Strategy: INNERMOST ---------------------------------------- (7) 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: COND1_3 COND2_3 GR_2 P_1 (c) The following functions are completely defined: cond1_3 cond2_3 gr_2 p_1 Due to the following rules being added: cond1(v0, v1, v2) -> const2 [0] cond2(v0, v1, v2) -> const2 [0] gr(v0, v1) -> null_gr [0] p(v0) -> 0 [0] And the following fresh constants: const2, null_gr, const, const1 ---------------------------------------- (8) 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: COND1(true, z0, z1) -> c(COND2(gr(z1, 0), z0, z1), GR(z1, 0)) [1] COND2(true, z0, z1) -> c1(COND2(gr(z1, 0), z0, p(z1)), GR(z1, 0)) [1] COND2(true, z0, z1) -> c2(COND2(gr(z1, 0), z0, p(z1)), P(z1)) [1] COND2(false, z0, z1) -> c3(COND1(gr(z0, 0), p(z0), z1), GR(z0, 0)) [1] COND2(false, z0, z1) -> c4(COND1(gr(z0, 0), p(z0), z1), P(z0)) [1] GR(0, z0) -> c5 [1] GR(s(z0), 0) -> c6 [1] GR(s(z0), s(z1)) -> c7(GR(z0, z1)) [1] P(0) -> c8 [1] P(s(z0)) -> c9 [1] cond1(true, z0, z1) -> cond2(gr(z1, 0), z0, z1) [0] cond2(true, z0, z1) -> cond2(gr(z1, 0), z0, p(z1)) [0] cond2(false, z0, z1) -> cond1(gr(z0, 0), p(z0), z1) [0] gr(0, z0) -> false [0] gr(s(z0), 0) -> true [0] gr(s(z0), s(z1)) -> gr(z0, z1) [0] p(0) -> 0 [0] p(s(z0)) -> z0 [0] cond1(v0, v1, v2) -> const2 [0] cond2(v0, v1, v2) -> const2 [0] gr(v0, v1) -> null_gr [0] p(v0) -> 0 [0] The TRS has the following type information: COND1 :: true:false:null_gr -> 0:s -> 0:s -> c true :: true:false:null_gr c :: c1:c2:c3:c4 -> c5:c6:c7 -> c COND2 :: true:false:null_gr -> 0:s -> 0:s -> c1:c2:c3:c4 gr :: 0:s -> 0:s -> true:false:null_gr 0 :: 0:s GR :: 0:s -> 0:s -> c5:c6:c7 c1 :: c1:c2:c3:c4 -> c5:c6:c7 -> c1:c2:c3:c4 p :: 0:s -> 0:s c2 :: c1:c2:c3:c4 -> c8:c9 -> c1:c2:c3:c4 P :: 0:s -> c8:c9 false :: true:false:null_gr c3 :: c -> c5:c6:c7 -> c1:c2:c3:c4 c4 :: c -> c8:c9 -> c1:c2:c3:c4 c5 :: c5:c6:c7 s :: 0:s -> 0:s c6 :: c5:c6:c7 c7 :: c5:c6:c7 -> c5:c6:c7 c8 :: c8:c9 c9 :: c8:c9 cond1 :: true:false:null_gr -> 0:s -> 0:s -> const2 cond2 :: true:false:null_gr -> 0:s -> 0:s -> const2 const2 :: const2 null_gr :: true:false:null_gr const :: c const1 :: c1:c2:c3:c4 Rewrite Strategy: INNERMOST ---------------------------------------- (9) NarrowingProof (BOTH BOUNDS(ID, ID)) Narrowed the inner basic terms of all right-hand sides by a single narrowing step. ---------------------------------------- (10) 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: COND1(true, z0, 0) -> c(COND2(false, z0, 0), GR(0, 0)) [1] COND1(true, z0, s(z0')) -> c(COND2(true, z0, s(z0')), GR(s(z0'), 0)) [1] COND1(true, z0, z1) -> c(COND2(null_gr, z0, z1), GR(z1, 0)) [1] COND2(true, z0, 0) -> c1(COND2(false, z0, 0), GR(0, 0)) [1] COND2(true, z0, 0) -> c1(COND2(false, z0, 0), GR(0, 0)) [1] COND2(true, z0, s(z0'')) -> c1(COND2(true, z0, z0''), GR(s(z0''), 0)) [1] COND2(true, z0, s(z0'')) -> c1(COND2(true, z0, 0), GR(s(z0''), 0)) [1] COND2(true, z0, 0) -> c1(COND2(null_gr, z0, 0), GR(0, 0)) [1] COND2(true, z0, s(z01)) -> c1(COND2(null_gr, z0, z01), GR(s(z01), 0)) [1] COND2(true, z0, z1) -> c1(COND2(null_gr, z0, 0), GR(z1, 0)) [1] COND2(true, z0, 0) -> c2(COND2(false, z0, 0), P(0)) [1] COND2(true, z0, 0) -> c2(COND2(false, z0, 0), P(0)) [1] COND2(true, z0, s(z02)) -> c2(COND2(true, z0, z02), P(s(z02))) [1] COND2(true, z0, s(z02)) -> c2(COND2(true, z0, 0), P(s(z02))) [1] COND2(true, z0, 0) -> c2(COND2(null_gr, z0, 0), P(0)) [1] COND2(true, z0, s(z03)) -> c2(COND2(null_gr, z0, z03), P(s(z03))) [1] COND2(true, z0, z1) -> c2(COND2(null_gr, z0, 0), P(z1)) [1] COND2(false, 0, z1) -> c3(COND1(false, 0, z1), GR(0, 0)) [1] COND2(false, 0, z1) -> c3(COND1(false, 0, z1), GR(0, 0)) [1] COND2(false, s(z04), z1) -> c3(COND1(true, z04, z1), GR(s(z04), 0)) [1] COND2(false, s(z04), z1) -> c3(COND1(true, 0, z1), GR(s(z04), 0)) [1] COND2(false, 0, z1) -> c3(COND1(null_gr, 0, z1), GR(0, 0)) [1] COND2(false, s(z05), z1) -> c3(COND1(null_gr, z05, z1), GR(s(z05), 0)) [1] COND2(false, z0, z1) -> c3(COND1(null_gr, 0, z1), GR(z0, 0)) [1] COND2(false, 0, z1) -> c4(COND1(false, 0, z1), P(0)) [1] COND2(false, 0, z1) -> c4(COND1(false, 0, z1), P(0)) [1] COND2(false, s(z06), z1) -> c4(COND1(true, z06, z1), P(s(z06))) [1] COND2(false, s(z06), z1) -> c4(COND1(true, 0, z1), P(s(z06))) [1] COND2(false, 0, z1) -> c4(COND1(null_gr, 0, z1), P(0)) [1] COND2(false, s(z07), z1) -> c4(COND1(null_gr, z07, z1), P(s(z07))) [1] COND2(false, z0, z1) -> c4(COND1(null_gr, 0, z1), P(z0)) [1] GR(0, z0) -> c5 [1] GR(s(z0), 0) -> c6 [1] GR(s(z0), s(z1)) -> c7(GR(z0, z1)) [1] P(0) -> c8 [1] P(s(z0)) -> c9 [1] cond1(true, z0, 0) -> cond2(false, z0, 0) [0] cond1(true, z0, s(z08)) -> cond2(true, z0, s(z08)) [0] cond1(true, z0, z1) -> cond2(null_gr, z0, z1) [0] cond2(true, z0, 0) -> cond2(false, z0, 0) [0] cond2(true, z0, 0) -> cond2(false, z0, 0) [0] cond2(true, z0, s(z09)) -> cond2(true, z0, z09) [0] cond2(true, z0, s(z09)) -> cond2(true, z0, 0) [0] cond2(true, z0, 0) -> cond2(null_gr, z0, 0) [0] cond2(true, z0, s(z010)) -> cond2(null_gr, z0, z010) [0] cond2(true, z0, z1) -> cond2(null_gr, z0, 0) [0] cond2(false, 0, z1) -> cond1(false, 0, z1) [0] cond2(false, 0, z1) -> cond1(false, 0, z1) [0] cond2(false, s(z011), z1) -> cond1(true, z011, z1) [0] cond2(false, s(z011), z1) -> cond1(true, 0, z1) [0] cond2(false, 0, z1) -> cond1(null_gr, 0, z1) [0] cond2(false, s(z012), z1) -> cond1(null_gr, z012, z1) [0] cond2(false, z0, z1) -> cond1(null_gr, 0, z1) [0] gr(0, z0) -> false [0] gr(s(z0), 0) -> true [0] gr(s(z0), s(z1)) -> gr(z0, z1) [0] p(0) -> 0 [0] p(s(z0)) -> z0 [0] cond1(v0, v1, v2) -> const2 [0] cond2(v0, v1, v2) -> const2 [0] gr(v0, v1) -> null_gr [0] p(v0) -> 0 [0] The TRS has the following type information: COND1 :: true:false:null_gr -> 0:s -> 0:s -> c true :: true:false:null_gr c :: c1:c2:c3:c4 -> c5:c6:c7 -> c COND2 :: true:false:null_gr -> 0:s -> 0:s -> c1:c2:c3:c4 gr :: 0:s -> 0:s -> true:false:null_gr 0 :: 0:s GR :: 0:s -> 0:s -> c5:c6:c7 c1 :: c1:c2:c3:c4 -> c5:c6:c7 -> c1:c2:c3:c4 p :: 0:s -> 0:s c2 :: c1:c2:c3:c4 -> c8:c9 -> c1:c2:c3:c4 P :: 0:s -> c8:c9 false :: true:false:null_gr c3 :: c -> c5:c6:c7 -> c1:c2:c3:c4 c4 :: c -> c8:c9 -> c1:c2:c3:c4 c5 :: c5:c6:c7 s :: 0:s -> 0:s c6 :: c5:c6:c7 c7 :: c5:c6:c7 -> c5:c6:c7 c8 :: c8:c9 c9 :: c8:c9 cond1 :: true:false:null_gr -> 0:s -> 0:s -> const2 cond2 :: true:false:null_gr -> 0:s -> 0:s -> const2 const2 :: const2 null_gr :: true:false:null_gr const :: c const1 :: c1:c2:c3:c4 Rewrite Strategy: INNERMOST ---------------------------------------- (11) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: true => 2 0 => 0 false => 1 c5 => 0 c6 => 1 c8 => 0 c9 => 1 const2 => 0 null_gr => 0 const => 0 const1 => 0 ---------------------------------------- (12) Obligation: Complexity RNTS consisting of the following rules: COND1(z, z', z'') -{ 1 }-> 1 + COND2(2, z0, 1 + z0') + GR(1 + z0', 0) :|: z = 2, z0' >= 0, z0 >= 0, z'' = 1 + z0', z' = z0 COND1(z, z', z'') -{ 1 }-> 1 + COND2(1, z0, 0) + GR(0, 0) :|: z = 2, z'' = 0, z0 >= 0, z' = z0 COND1(z, z', z'') -{ 1 }-> 1 + COND2(0, z0, z1) + GR(z1, 0) :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1 COND2(z, z', z'') -{ 1 }-> 1 + COND2(2, z0, z0'') + GR(1 + z0'', 0) :|: z = 2, z'' = 1 + z0'', z0 >= 0, z0'' >= 0, z' = z0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(2, z0, z02) + P(1 + z02) :|: z = 2, z02 >= 0, z0 >= 0, z' = z0, z'' = 1 + z02 COND2(z, z', z'') -{ 1 }-> 1 + COND2(2, z0, 0) + P(1 + z02) :|: z = 2, z02 >= 0, z0 >= 0, z' = z0, z'' = 1 + z02 COND2(z, z', z'') -{ 1 }-> 1 + COND2(2, z0, 0) + GR(1 + z0'', 0) :|: z = 2, z'' = 1 + z0'', z0 >= 0, z0'' >= 0, z' = z0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(1, z0, 0) + P(0) :|: z = 2, z'' = 0, z0 >= 0, z' = z0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(1, z0, 0) + GR(0, 0) :|: z = 2, z'' = 0, z0 >= 0, z' = z0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z0, z01) + GR(1 + z01, 0) :|: z = 2, z01 >= 0, z0 >= 0, z' = z0, z'' = 1 + z01 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z0, z03) + P(1 + z03) :|: z = 2, z'' = 1 + z03, z0 >= 0, z03 >= 0, z' = z0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z0, 0) + P(z1) :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z0, 0) + P(0) :|: z = 2, z'' = 0, z0 >= 0, z' = z0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z0, 0) + GR(z1, 0) :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z0, 0) + GR(0, 0) :|: z = 2, z'' = 0, z0 >= 0, z' = z0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(2, z04, z1) + GR(1 + z04, 0) :|: z04 >= 0, z1 >= 0, z = 1, z' = 1 + z04, z'' = z1 COND2(z, z', z'') -{ 1 }-> 1 + COND1(2, z06, z1) + P(1 + z06) :|: z1 >= 0, z = 1, z06 >= 0, z' = 1 + z06, z'' = z1 COND2(z, z', z'') -{ 1 }-> 1 + COND1(2, 0, z1) + P(1 + z06) :|: z1 >= 0, z = 1, z06 >= 0, z' = 1 + z06, z'' = z1 COND2(z, z', z'') -{ 1 }-> 1 + COND1(2, 0, z1) + GR(1 + z04, 0) :|: z04 >= 0, z1 >= 0, z = 1, z' = 1 + z04, z'' = z1 COND2(z, z', z'') -{ 1 }-> 1 + COND1(1, 0, z1) + P(0) :|: z1 >= 0, z = 1, z' = 0, z'' = z1 COND2(z, z', z'') -{ 1 }-> 1 + COND1(1, 0, z1) + GR(0, 0) :|: z1 >= 0, z = 1, z' = 0, z'' = z1 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, z05, z1) + GR(1 + z05, 0) :|: z1 >= 0, z = 1, z05 >= 0, z' = 1 + z05, z'' = z1 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, z07, z1) + P(1 + z07) :|: z1 >= 0, z07 >= 0, z = 1, z' = 1 + z07, z'' = z1 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, 0, z1) + P(z0) :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, 0, z1) + P(0) :|: z1 >= 0, z = 1, z' = 0, z'' = z1 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, 0, z1) + GR(z0, 0) :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, 0, z1) + GR(0, 0) :|: z1 >= 0, z = 1, z' = 0, z'' = z1 GR(z, z') -{ 1 }-> 1 :|: z = 1 + z0, z0 >= 0, z' = 0 GR(z, z') -{ 1 }-> 0 :|: z0 >= 0, z = 0, z' = z0 GR(z, z') -{ 1 }-> 1 + GR(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1 P(z) -{ 1 }-> 1 :|: z = 1 + z0, z0 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond1(z, z', z'') -{ 0 }-> cond2(2, z0, 1 + z08) :|: z = 2, z08 >= 0, z'' = 1 + z08, z0 >= 0, z' = z0 cond1(z, z', z'') -{ 0 }-> cond2(1, z0, 0) :|: z = 2, z'' = 0, z0 >= 0, z' = z0 cond1(z, z', z'') -{ 0 }-> cond2(0, z0, z1) :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1 cond1(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(2, z0, z09) :|: z = 2, z'' = 1 + z09, z0 >= 0, z09 >= 0, z' = z0 cond2(z, z', z'') -{ 0 }-> cond2(2, z0, 0) :|: z = 2, z'' = 1 + z09, z0 >= 0, z09 >= 0, z' = z0 cond2(z, z', z'') -{ 0 }-> cond2(1, z0, 0) :|: z = 2, z'' = 0, z0 >= 0, z' = z0 cond2(z, z', z'') -{ 0 }-> cond2(0, z0, z010) :|: z = 2, z'' = 1 + z010, z0 >= 0, z' = z0, z010 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z0, 0) :|: z = 2, z'' = 0, z0 >= 0, z' = z0 cond2(z, z', z'') -{ 0 }-> cond2(0, z0, 0) :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1 cond2(z, z', z'') -{ 0 }-> cond1(2, z011, z1) :|: z011 >= 0, z1 >= 0, z = 1, z' = 1 + z011, z'' = z1 cond2(z, z', z'') -{ 0 }-> cond1(2, 0, z1) :|: z011 >= 0, z1 >= 0, z = 1, z' = 1 + z011, z'' = z1 cond2(z, z', z'') -{ 0 }-> cond1(1, 0, z1) :|: z1 >= 0, z = 1, z' = 0, z'' = z1 cond2(z, z', z'') -{ 0 }-> cond1(0, z012, z1) :|: z1 >= 0, z = 1, z' = 1 + z012, z012 >= 0, z'' = z1 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z1) :|: z1 >= 0, z = 1, z' = 0, z'' = z1 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z1) :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1 cond2(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0 gr(z, z') -{ 0 }-> gr(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1 gr(z, z') -{ 0 }-> 2 :|: z = 1 + z0, z0 >= 0, z' = 0 gr(z, z') -{ 0 }-> 1 :|: z0 >= 0, z = 0, z' = z0 gr(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 p(z) -{ 0 }-> z0 :|: z = 1 + z0, z0 >= 0 p(z) -{ 0 }-> 0 :|: z = 0 p(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 ---------------------------------------- (13) InliningProof (UPPER BOUND(ID)) Inlined the following terminating rules on right-hand sides where appropriate: P(z) -{ 1 }-> 1 :|: z = 1 + z0, z0 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 ---------------------------------------- (14) Obligation: Complexity RNTS consisting of the following rules: COND1(z, z', z'') -{ 1 }-> 1 + COND2(2, z0, 1 + z0') + GR(1 + z0', 0) :|: z = 2, z0' >= 0, z0 >= 0, z'' = 1 + z0', z' = z0 COND1(z, z', z'') -{ 1 }-> 1 + COND2(1, z0, 0) + GR(0, 0) :|: z = 2, z'' = 0, z0 >= 0, z' = z0 COND1(z, z', z'') -{ 1 }-> 1 + COND2(0, z0, z1) + GR(z1, 0) :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1 COND2(z, z', z'') -{ 1 }-> 1 + COND2(2, z0, z0'') + GR(1 + z0'', 0) :|: z = 2, z'' = 1 + z0'', z0 >= 0, z0'' >= 0, z' = z0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z0, z02) + 1 :|: z = 2, z02 >= 0, z0 >= 0, z' = z0, z'' = 1 + z02, 1 + z02 = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(2, z0, 0) + GR(1 + z0'', 0) :|: z = 2, z'' = 1 + z0'', z0 >= 0, z0'' >= 0, z' = z0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z0, 0) + 1 :|: z = 2, z02 >= 0, z0 >= 0, z' = z0, z'' = 1 + z02, 1 + z02 = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(1, z0, 0) + GR(0, 0) :|: z = 2, z'' = 0, z0 >= 0, z' = z0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(1, z0, 0) + 0 :|: z = 2, z'' = 0, z0 >= 0, z' = z0, 0 = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z0, z01) + GR(1 + z01, 0) :|: z = 2, z01 >= 0, z0 >= 0, z' = z0, z'' = 1 + z01 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z0, z03) + 1 :|: z = 2, z'' = 1 + z03, z0 >= 0, z03 >= 0, z' = z0, 1 + z03 = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z0, 0) + GR(z1, 0) :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z0, 0) + GR(0, 0) :|: z = 2, z'' = 0, z0 >= 0, z' = z0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z0, 0) + 1 :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1, z1 = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z0, 0) + 0 :|: z = 2, z'' = 0, z0 >= 0, z' = z0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z0, 0) + 0 :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1, z1 = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(2, z04, z1) + GR(1 + z04, 0) :|: z04 >= 0, z1 >= 0, z = 1, z' = 1 + z04, z'' = z1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, z06, z1) + 1 :|: z1 >= 0, z = 1, z06 >= 0, z' = 1 + z06, z'' = z1, 1 + z06 = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(2, 0, z1) + GR(1 + z04, 0) :|: z04 >= 0, z1 >= 0, z = 1, z' = 1 + z04, z'' = z1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, 0, z1) + 1 :|: z1 >= 0, z = 1, z06 >= 0, z' = 1 + z06, z'' = z1, 1 + z06 = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(1, 0, z1) + GR(0, 0) :|: z1 >= 0, z = 1, z' = 0, z'' = z1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(1, 0, z1) + 0 :|: z1 >= 0, z = 1, z' = 0, z'' = z1, 0 = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, z05, z1) + GR(1 + z05, 0) :|: z1 >= 0, z = 1, z05 >= 0, z' = 1 + z05, z'' = z1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, z07, z1) + 1 :|: z1 >= 0, z07 >= 0, z = 1, z' = 1 + z07, z'' = z1, 1 + z07 = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, 0, z1) + GR(z0, 0) :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, 0, z1) + GR(0, 0) :|: z1 >= 0, z = 1, z' = 0, z'' = z1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z1) + 1 :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1, z0 = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z1) + 0 :|: z1 >= 0, z = 1, z' = 0, z'' = z1, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z1) + 0 :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1, z0 = 0 GR(z, z') -{ 1 }-> 1 :|: z = 1 + z0, z0 >= 0, z' = 0 GR(z, z') -{ 1 }-> 0 :|: z0 >= 0, z = 0, z' = z0 GR(z, z') -{ 1 }-> 1 + GR(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1 P(z) -{ 1 }-> 1 :|: z = 1 + z0, z0 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond1(z, z', z'') -{ 0 }-> cond2(2, z0, 1 + z08) :|: z = 2, z08 >= 0, z'' = 1 + z08, z0 >= 0, z' = z0 cond1(z, z', z'') -{ 0 }-> cond2(1, z0, 0) :|: z = 2, z'' = 0, z0 >= 0, z' = z0 cond1(z, z', z'') -{ 0 }-> cond2(0, z0, z1) :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1 cond1(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(2, z0, z09) :|: z = 2, z'' = 1 + z09, z0 >= 0, z09 >= 0, z' = z0 cond2(z, z', z'') -{ 0 }-> cond2(2, z0, 0) :|: z = 2, z'' = 1 + z09, z0 >= 0, z09 >= 0, z' = z0 cond2(z, z', z'') -{ 0 }-> cond2(1, z0, 0) :|: z = 2, z'' = 0, z0 >= 0, z' = z0 cond2(z, z', z'') -{ 0 }-> cond2(0, z0, z010) :|: z = 2, z'' = 1 + z010, z0 >= 0, z' = z0, z010 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z0, 0) :|: z = 2, z'' = 0, z0 >= 0, z' = z0 cond2(z, z', z'') -{ 0 }-> cond2(0, z0, 0) :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1 cond2(z, z', z'') -{ 0 }-> cond1(2, z011, z1) :|: z011 >= 0, z1 >= 0, z = 1, z' = 1 + z011, z'' = z1 cond2(z, z', z'') -{ 0 }-> cond1(2, 0, z1) :|: z011 >= 0, z1 >= 0, z = 1, z' = 1 + z011, z'' = z1 cond2(z, z', z'') -{ 0 }-> cond1(1, 0, z1) :|: z1 >= 0, z = 1, z' = 0, z'' = z1 cond2(z, z', z'') -{ 0 }-> cond1(0, z012, z1) :|: z1 >= 0, z = 1, z' = 1 + z012, z012 >= 0, z'' = z1 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z1) :|: z1 >= 0, z = 1, z' = 0, z'' = z1 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z1) :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1 cond2(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0 gr(z, z') -{ 0 }-> gr(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1 gr(z, z') -{ 0 }-> 2 :|: z = 1 + z0, z0 >= 0, z' = 0 gr(z, z') -{ 0 }-> 1 :|: z0 >= 0, z = 0, z' = z0 gr(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 p(z) -{ 0 }-> z0 :|: z = 1 + z0, z0 >= 0 p(z) -{ 0 }-> 0 :|: z = 0 p(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 ---------------------------------------- (15) SimplificationProof (BOTH BOUNDS(ID, ID)) Simplified the RNTS by moving equalities from the constraints into the right-hand sides. ---------------------------------------- (16) Obligation: Complexity RNTS consisting of the following rules: COND1(z, z', z'') -{ 1 }-> 1 + COND2(2, z', 1 + (z'' - 1)) + GR(1 + (z'' - 1), 0) :|: z = 2, z'' - 1 >= 0, z' >= 0 COND1(z, z', z'') -{ 1 }-> 1 + COND2(1, z', 0) + GR(0, 0) :|: z = 2, z'' = 0, z' >= 0 COND1(z, z', z'') -{ 1 }-> 1 + COND2(0, z', z'') + GR(z'', 0) :|: z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(2, z', 0) + GR(1 + (z'' - 1), 0) :|: z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', 0) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(2, z', z'' - 1) + GR(1 + (z'' - 1), 0) :|: z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', z'' - 1) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(1, z', 0) + GR(0, 0) :|: z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(1, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z', 0) + GR(z'', 0) :|: z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z', 0) + GR(0, 0) :|: z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 1 :|: z = 2, z'' >= 0, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' >= 0, z' >= 0, z'' = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z', z'' - 1) + GR(1 + (z'' - 1), 0) :|: z = 2, z'' - 1 >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', z'' - 1) + 1 :|: z = 2, z' >= 0, z'' - 1 >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(2, 0, z'') + GR(1 + (z' - 1), 0) :|: z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, 0, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(2, z' - 1, z'') + GR(1 + (z' - 1), 0) :|: z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, z' - 1, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(1, 0, z'') + GR(0, 0) :|: z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(1, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, 0, z'') + GR(z', 0) :|: z'' >= 0, z = 1, z' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, 0, z'') + GR(0, 0) :|: z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 1 :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' >= 0, z' = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, z' - 1, z'') + GR(1 + (z' - 1), 0) :|: z'' >= 0, z = 1, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, z' - 1, z'') + 1 :|: z'' >= 0, z' - 1 >= 0, z = 1, 1 + (z' - 1) = 1 + z0, z0 >= 0 GR(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0 GR(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 GR(z, z') -{ 1 }-> 1 + GR(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond1(z, z', z'') -{ 0 }-> cond2(2, z', 1 + (z'' - 1)) :|: z = 2, z'' - 1 >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> cond2(1, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> cond2(0, z', z'') :|: z = 2, z'' >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(2, z', 0) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(2, z', z'' - 1) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(1, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', 0) :|: z = 2, z'' >= 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', z'' - 1) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond1(2, 0, z'') :|: z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> cond1(2, z' - 1, z'') :|: z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> cond1(1, 0, z'') :|: z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z'') :|: z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z'') :|: z'' >= 0, z = 1, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond1(0, z' - 1, z'') :|: z'' >= 0, z = 1, z' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 gr(z, z') -{ 0 }-> gr(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 gr(z, z') -{ 0 }-> 2 :|: z - 1 >= 0, z' = 0 gr(z, z') -{ 0 }-> 1 :|: z' >= 0, z = 0 gr(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 p(z) -{ 0 }-> 0 :|: z = 0 p(z) -{ 0 }-> 0 :|: z >= 0 p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0 ---------------------------------------- (17) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID)) Found the following analysis order by SCC decomposition: { P } { GR } { gr } { cond2, cond1 } { p } { COND2, COND1 } ---------------------------------------- (18) Obligation: Complexity RNTS consisting of the following rules: COND1(z, z', z'') -{ 1 }-> 1 + COND2(2, z', 1 + (z'' - 1)) + GR(1 + (z'' - 1), 0) :|: z = 2, z'' - 1 >= 0, z' >= 0 COND1(z, z', z'') -{ 1 }-> 1 + COND2(1, z', 0) + GR(0, 0) :|: z = 2, z'' = 0, z' >= 0 COND1(z, z', z'') -{ 1 }-> 1 + COND2(0, z', z'') + GR(z'', 0) :|: z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(2, z', 0) + GR(1 + (z'' - 1), 0) :|: z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', 0) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(2, z', z'' - 1) + GR(1 + (z'' - 1), 0) :|: z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', z'' - 1) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(1, z', 0) + GR(0, 0) :|: z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(1, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z', 0) + GR(z'', 0) :|: z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z', 0) + GR(0, 0) :|: z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 1 :|: z = 2, z'' >= 0, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' >= 0, z' >= 0, z'' = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z', z'' - 1) + GR(1 + (z'' - 1), 0) :|: z = 2, z'' - 1 >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', z'' - 1) + 1 :|: z = 2, z' >= 0, z'' - 1 >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(2, 0, z'') + GR(1 + (z' - 1), 0) :|: z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, 0, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(2, z' - 1, z'') + GR(1 + (z' - 1), 0) :|: z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, z' - 1, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(1, 0, z'') + GR(0, 0) :|: z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(1, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, 0, z'') + GR(z', 0) :|: z'' >= 0, z = 1, z' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, 0, z'') + GR(0, 0) :|: z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 1 :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' >= 0, z' = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, z' - 1, z'') + GR(1 + (z' - 1), 0) :|: z'' >= 0, z = 1, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, z' - 1, z'') + 1 :|: z'' >= 0, z' - 1 >= 0, z = 1, 1 + (z' - 1) = 1 + z0, z0 >= 0 GR(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0 GR(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 GR(z, z') -{ 1 }-> 1 + GR(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond1(z, z', z'') -{ 0 }-> cond2(2, z', 1 + (z'' - 1)) :|: z = 2, z'' - 1 >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> cond2(1, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> cond2(0, z', z'') :|: z = 2, z'' >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(2, z', 0) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(2, z', z'' - 1) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(1, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', 0) :|: z = 2, z'' >= 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', z'' - 1) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond1(2, 0, z'') :|: z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> cond1(2, z' - 1, z'') :|: z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> cond1(1, 0, z'') :|: z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z'') :|: z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z'') :|: z'' >= 0, z = 1, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond1(0, z' - 1, z'') :|: z'' >= 0, z = 1, z' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 gr(z, z') -{ 0 }-> gr(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 gr(z, z') -{ 0 }-> 2 :|: z - 1 >= 0, z' = 0 gr(z, z') -{ 0 }-> 1 :|: z' >= 0, z = 0 gr(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 p(z) -{ 0 }-> 0 :|: z = 0 p(z) -{ 0 }-> 0 :|: z >= 0 p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0 Function symbols to be analyzed: {P}, {GR}, {gr}, {cond2,cond1}, {p}, {COND2,COND1} ---------------------------------------- (19) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (20) Obligation: Complexity RNTS consisting of the following rules: COND1(z, z', z'') -{ 1 }-> 1 + COND2(2, z', 1 + (z'' - 1)) + GR(1 + (z'' - 1), 0) :|: z = 2, z'' - 1 >= 0, z' >= 0 COND1(z, z', z'') -{ 1 }-> 1 + COND2(1, z', 0) + GR(0, 0) :|: z = 2, z'' = 0, z' >= 0 COND1(z, z', z'') -{ 1 }-> 1 + COND2(0, z', z'') + GR(z'', 0) :|: z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(2, z', 0) + GR(1 + (z'' - 1), 0) :|: z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', 0) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(2, z', z'' - 1) + GR(1 + (z'' - 1), 0) :|: z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', z'' - 1) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(1, z', 0) + GR(0, 0) :|: z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(1, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z', 0) + GR(z'', 0) :|: z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z', 0) + GR(0, 0) :|: z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 1 :|: z = 2, z'' >= 0, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' >= 0, z' >= 0, z'' = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z', z'' - 1) + GR(1 + (z'' - 1), 0) :|: z = 2, z'' - 1 >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', z'' - 1) + 1 :|: z = 2, z' >= 0, z'' - 1 >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(2, 0, z'') + GR(1 + (z' - 1), 0) :|: z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, 0, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(2, z' - 1, z'') + GR(1 + (z' - 1), 0) :|: z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, z' - 1, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(1, 0, z'') + GR(0, 0) :|: z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(1, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, 0, z'') + GR(z', 0) :|: z'' >= 0, z = 1, z' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, 0, z'') + GR(0, 0) :|: z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 1 :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' >= 0, z' = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, z' - 1, z'') + GR(1 + (z' - 1), 0) :|: z'' >= 0, z = 1, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, z' - 1, z'') + 1 :|: z'' >= 0, z' - 1 >= 0, z = 1, 1 + (z' - 1) = 1 + z0, z0 >= 0 GR(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0 GR(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 GR(z, z') -{ 1 }-> 1 + GR(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond1(z, z', z'') -{ 0 }-> cond2(2, z', 1 + (z'' - 1)) :|: z = 2, z'' - 1 >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> cond2(1, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> cond2(0, z', z'') :|: z = 2, z'' >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(2, z', 0) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(2, z', z'' - 1) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(1, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', 0) :|: z = 2, z'' >= 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', z'' - 1) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond1(2, 0, z'') :|: z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> cond1(2, z' - 1, z'') :|: z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> cond1(1, 0, z'') :|: z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z'') :|: z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z'') :|: z'' >= 0, z = 1, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond1(0, z' - 1, z'') :|: z'' >= 0, z = 1, z' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 gr(z, z') -{ 0 }-> gr(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 gr(z, z') -{ 0 }-> 2 :|: z - 1 >= 0, z' = 0 gr(z, z') -{ 0 }-> 1 :|: z' >= 0, z = 0 gr(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 p(z) -{ 0 }-> 0 :|: z = 0 p(z) -{ 0 }-> 0 :|: z >= 0 p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0 Function symbols to be analyzed: {P}, {GR}, {gr}, {cond2,cond1}, {p}, {COND2,COND1} ---------------------------------------- (21) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: P after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 1 ---------------------------------------- (22) Obligation: Complexity RNTS consisting of the following rules: COND1(z, z', z'') -{ 1 }-> 1 + COND2(2, z', 1 + (z'' - 1)) + GR(1 + (z'' - 1), 0) :|: z = 2, z'' - 1 >= 0, z' >= 0 COND1(z, z', z'') -{ 1 }-> 1 + COND2(1, z', 0) + GR(0, 0) :|: z = 2, z'' = 0, z' >= 0 COND1(z, z', z'') -{ 1 }-> 1 + COND2(0, z', z'') + GR(z'', 0) :|: z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(2, z', 0) + GR(1 + (z'' - 1), 0) :|: z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', 0) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(2, z', z'' - 1) + GR(1 + (z'' - 1), 0) :|: z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', z'' - 1) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(1, z', 0) + GR(0, 0) :|: z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(1, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z', 0) + GR(z'', 0) :|: z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z', 0) + GR(0, 0) :|: z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 1 :|: z = 2, z'' >= 0, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' >= 0, z' >= 0, z'' = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z', z'' - 1) + GR(1 + (z'' - 1), 0) :|: z = 2, z'' - 1 >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', z'' - 1) + 1 :|: z = 2, z' >= 0, z'' - 1 >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(2, 0, z'') + GR(1 + (z' - 1), 0) :|: z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, 0, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(2, z' - 1, z'') + GR(1 + (z' - 1), 0) :|: z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, z' - 1, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(1, 0, z'') + GR(0, 0) :|: z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(1, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, 0, z'') + GR(z', 0) :|: z'' >= 0, z = 1, z' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, 0, z'') + GR(0, 0) :|: z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 1 :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' >= 0, z' = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, z' - 1, z'') + GR(1 + (z' - 1), 0) :|: z'' >= 0, z = 1, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, z' - 1, z'') + 1 :|: z'' >= 0, z' - 1 >= 0, z = 1, 1 + (z' - 1) = 1 + z0, z0 >= 0 GR(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0 GR(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 GR(z, z') -{ 1 }-> 1 + GR(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond1(z, z', z'') -{ 0 }-> cond2(2, z', 1 + (z'' - 1)) :|: z = 2, z'' - 1 >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> cond2(1, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> cond2(0, z', z'') :|: z = 2, z'' >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(2, z', 0) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(2, z', z'' - 1) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(1, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', 0) :|: z = 2, z'' >= 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', z'' - 1) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond1(2, 0, z'') :|: z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> cond1(2, z' - 1, z'') :|: z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> cond1(1, 0, z'') :|: z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z'') :|: z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z'') :|: z'' >= 0, z = 1, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond1(0, z' - 1, z'') :|: z'' >= 0, z = 1, z' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 gr(z, z') -{ 0 }-> gr(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 gr(z, z') -{ 0 }-> 2 :|: z - 1 >= 0, z' = 0 gr(z, z') -{ 0 }-> 1 :|: z' >= 0, z = 0 gr(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 p(z) -{ 0 }-> 0 :|: z = 0 p(z) -{ 0 }-> 0 :|: z >= 0 p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0 Function symbols to be analyzed: {P}, {GR}, {gr}, {cond2,cond1}, {p}, {COND2,COND1} Previous analysis results are: P: runtime: ?, size: O(1) [1] ---------------------------------------- (23) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: P after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 1 ---------------------------------------- (24) Obligation: Complexity RNTS consisting of the following rules: COND1(z, z', z'') -{ 1 }-> 1 + COND2(2, z', 1 + (z'' - 1)) + GR(1 + (z'' - 1), 0) :|: z = 2, z'' - 1 >= 0, z' >= 0 COND1(z, z', z'') -{ 1 }-> 1 + COND2(1, z', 0) + GR(0, 0) :|: z = 2, z'' = 0, z' >= 0 COND1(z, z', z'') -{ 1 }-> 1 + COND2(0, z', z'') + GR(z'', 0) :|: z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(2, z', 0) + GR(1 + (z'' - 1), 0) :|: z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', 0) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(2, z', z'' - 1) + GR(1 + (z'' - 1), 0) :|: z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', z'' - 1) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(1, z', 0) + GR(0, 0) :|: z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(1, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z', 0) + GR(z'', 0) :|: z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z', 0) + GR(0, 0) :|: z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 1 :|: z = 2, z'' >= 0, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' >= 0, z' >= 0, z'' = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z', z'' - 1) + GR(1 + (z'' - 1), 0) :|: z = 2, z'' - 1 >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', z'' - 1) + 1 :|: z = 2, z' >= 0, z'' - 1 >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(2, 0, z'') + GR(1 + (z' - 1), 0) :|: z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, 0, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(2, z' - 1, z'') + GR(1 + (z' - 1), 0) :|: z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, z' - 1, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(1, 0, z'') + GR(0, 0) :|: z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(1, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, 0, z'') + GR(z', 0) :|: z'' >= 0, z = 1, z' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, 0, z'') + GR(0, 0) :|: z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 1 :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' >= 0, z' = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, z' - 1, z'') + GR(1 + (z' - 1), 0) :|: z'' >= 0, z = 1, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, z' - 1, z'') + 1 :|: z'' >= 0, z' - 1 >= 0, z = 1, 1 + (z' - 1) = 1 + z0, z0 >= 0 GR(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0 GR(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 GR(z, z') -{ 1 }-> 1 + GR(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond1(z, z', z'') -{ 0 }-> cond2(2, z', 1 + (z'' - 1)) :|: z = 2, z'' - 1 >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> cond2(1, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> cond2(0, z', z'') :|: z = 2, z'' >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(2, z', 0) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(2, z', z'' - 1) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(1, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', 0) :|: z = 2, z'' >= 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', z'' - 1) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond1(2, 0, z'') :|: z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> cond1(2, z' - 1, z'') :|: z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> cond1(1, 0, z'') :|: z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z'') :|: z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z'') :|: z'' >= 0, z = 1, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond1(0, z' - 1, z'') :|: z'' >= 0, z = 1, z' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 gr(z, z') -{ 0 }-> gr(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 gr(z, z') -{ 0 }-> 2 :|: z - 1 >= 0, z' = 0 gr(z, z') -{ 0 }-> 1 :|: z' >= 0, z = 0 gr(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 p(z) -{ 0 }-> 0 :|: z = 0 p(z) -{ 0 }-> 0 :|: z >= 0 p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0 Function symbols to be analyzed: {GR}, {gr}, {cond2,cond1}, {p}, {COND2,COND1} Previous analysis results are: P: runtime: O(1) [1], size: O(1) [1] ---------------------------------------- (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: COND1(z, z', z'') -{ 1 }-> 1 + COND2(2, z', 1 + (z'' - 1)) + GR(1 + (z'' - 1), 0) :|: z = 2, z'' - 1 >= 0, z' >= 0 COND1(z, z', z'') -{ 1 }-> 1 + COND2(1, z', 0) + GR(0, 0) :|: z = 2, z'' = 0, z' >= 0 COND1(z, z', z'') -{ 1 }-> 1 + COND2(0, z', z'') + GR(z'', 0) :|: z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(2, z', 0) + GR(1 + (z'' - 1), 0) :|: z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', 0) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(2, z', z'' - 1) + GR(1 + (z'' - 1), 0) :|: z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', z'' - 1) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(1, z', 0) + GR(0, 0) :|: z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(1, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z', 0) + GR(z'', 0) :|: z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z', 0) + GR(0, 0) :|: z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 1 :|: z = 2, z'' >= 0, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' >= 0, z' >= 0, z'' = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z', z'' - 1) + GR(1 + (z'' - 1), 0) :|: z = 2, z'' - 1 >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', z'' - 1) + 1 :|: z = 2, z' >= 0, z'' - 1 >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(2, 0, z'') + GR(1 + (z' - 1), 0) :|: z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, 0, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(2, z' - 1, z'') + GR(1 + (z' - 1), 0) :|: z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, z' - 1, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(1, 0, z'') + GR(0, 0) :|: z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(1, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, 0, z'') + GR(z', 0) :|: z'' >= 0, z = 1, z' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, 0, z'') + GR(0, 0) :|: z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 1 :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' >= 0, z' = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, z' - 1, z'') + GR(1 + (z' - 1), 0) :|: z'' >= 0, z = 1, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, z' - 1, z'') + 1 :|: z'' >= 0, z' - 1 >= 0, z = 1, 1 + (z' - 1) = 1 + z0, z0 >= 0 GR(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0 GR(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 GR(z, z') -{ 1 }-> 1 + GR(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond1(z, z', z'') -{ 0 }-> cond2(2, z', 1 + (z'' - 1)) :|: z = 2, z'' - 1 >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> cond2(1, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> cond2(0, z', z'') :|: z = 2, z'' >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(2, z', 0) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(2, z', z'' - 1) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(1, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', 0) :|: z = 2, z'' >= 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', z'' - 1) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond1(2, 0, z'') :|: z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> cond1(2, z' - 1, z'') :|: z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> cond1(1, 0, z'') :|: z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z'') :|: z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z'') :|: z'' >= 0, z = 1, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond1(0, z' - 1, z'') :|: z'' >= 0, z = 1, z' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 gr(z, z') -{ 0 }-> gr(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 gr(z, z') -{ 0 }-> 2 :|: z - 1 >= 0, z' = 0 gr(z, z') -{ 0 }-> 1 :|: z' >= 0, z = 0 gr(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 p(z) -{ 0 }-> 0 :|: z = 0 p(z) -{ 0 }-> 0 :|: z >= 0 p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0 Function symbols to be analyzed: {GR}, {gr}, {cond2,cond1}, {p}, {COND2,COND1} Previous analysis results are: P: runtime: O(1) [1], size: O(1) [1] ---------------------------------------- (27) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using KoAT for: GR after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: z ---------------------------------------- (28) Obligation: Complexity RNTS consisting of the following rules: COND1(z, z', z'') -{ 1 }-> 1 + COND2(2, z', 1 + (z'' - 1)) + GR(1 + (z'' - 1), 0) :|: z = 2, z'' - 1 >= 0, z' >= 0 COND1(z, z', z'') -{ 1 }-> 1 + COND2(1, z', 0) + GR(0, 0) :|: z = 2, z'' = 0, z' >= 0 COND1(z, z', z'') -{ 1 }-> 1 + COND2(0, z', z'') + GR(z'', 0) :|: z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(2, z', 0) + GR(1 + (z'' - 1), 0) :|: z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', 0) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(2, z', z'' - 1) + GR(1 + (z'' - 1), 0) :|: z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', z'' - 1) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(1, z', 0) + GR(0, 0) :|: z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(1, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z', 0) + GR(z'', 0) :|: z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z', 0) + GR(0, 0) :|: z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 1 :|: z = 2, z'' >= 0, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' >= 0, z' >= 0, z'' = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z', z'' - 1) + GR(1 + (z'' - 1), 0) :|: z = 2, z'' - 1 >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', z'' - 1) + 1 :|: z = 2, z' >= 0, z'' - 1 >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(2, 0, z'') + GR(1 + (z' - 1), 0) :|: z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, 0, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(2, z' - 1, z'') + GR(1 + (z' - 1), 0) :|: z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, z' - 1, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(1, 0, z'') + GR(0, 0) :|: z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(1, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, 0, z'') + GR(z', 0) :|: z'' >= 0, z = 1, z' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, 0, z'') + GR(0, 0) :|: z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 1 :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' >= 0, z' = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, z' - 1, z'') + GR(1 + (z' - 1), 0) :|: z'' >= 0, z = 1, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, z' - 1, z'') + 1 :|: z'' >= 0, z' - 1 >= 0, z = 1, 1 + (z' - 1) = 1 + z0, z0 >= 0 GR(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0 GR(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 GR(z, z') -{ 1 }-> 1 + GR(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond1(z, z', z'') -{ 0 }-> cond2(2, z', 1 + (z'' - 1)) :|: z = 2, z'' - 1 >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> cond2(1, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> cond2(0, z', z'') :|: z = 2, z'' >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(2, z', 0) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(2, z', z'' - 1) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(1, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', 0) :|: z = 2, z'' >= 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', z'' - 1) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond1(2, 0, z'') :|: z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> cond1(2, z' - 1, z'') :|: z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> cond1(1, 0, z'') :|: z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z'') :|: z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z'') :|: z'' >= 0, z = 1, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond1(0, z' - 1, z'') :|: z'' >= 0, z = 1, z' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 gr(z, z') -{ 0 }-> gr(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 gr(z, z') -{ 0 }-> 2 :|: z - 1 >= 0, z' = 0 gr(z, z') -{ 0 }-> 1 :|: z' >= 0, z = 0 gr(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 p(z) -{ 0 }-> 0 :|: z = 0 p(z) -{ 0 }-> 0 :|: z >= 0 p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0 Function symbols to be analyzed: {GR}, {gr}, {cond2,cond1}, {p}, {COND2,COND1} Previous analysis results are: P: runtime: O(1) [1], size: O(1) [1] GR: runtime: ?, size: O(n^1) [z] ---------------------------------------- (29) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using KoAT for: GR after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: 2 + z' ---------------------------------------- (30) Obligation: Complexity RNTS consisting of the following rules: COND1(z, z', z'') -{ 1 }-> 1 + COND2(2, z', 1 + (z'' - 1)) + GR(1 + (z'' - 1), 0) :|: z = 2, z'' - 1 >= 0, z' >= 0 COND1(z, z', z'') -{ 1 }-> 1 + COND2(1, z', 0) + GR(0, 0) :|: z = 2, z'' = 0, z' >= 0 COND1(z, z', z'') -{ 1 }-> 1 + COND2(0, z', z'') + GR(z'', 0) :|: z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(2, z', 0) + GR(1 + (z'' - 1), 0) :|: z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', 0) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(2, z', z'' - 1) + GR(1 + (z'' - 1), 0) :|: z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', z'' - 1) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(1, z', 0) + GR(0, 0) :|: z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(1, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z', 0) + GR(z'', 0) :|: z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z', 0) + GR(0, 0) :|: z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 1 :|: z = 2, z'' >= 0, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' >= 0, z' >= 0, z'' = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND2(0, z', z'' - 1) + GR(1 + (z'' - 1), 0) :|: z = 2, z'' - 1 >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', z'' - 1) + 1 :|: z = 2, z' >= 0, z'' - 1 >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(2, 0, z'') + GR(1 + (z' - 1), 0) :|: z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, 0, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(2, z' - 1, z'') + GR(1 + (z' - 1), 0) :|: z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, z' - 1, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(1, 0, z'') + GR(0, 0) :|: z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(1, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, 0, z'') + GR(z', 0) :|: z'' >= 0, z = 1, z' >= 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, 0, z'') + GR(0, 0) :|: z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 1 :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' >= 0, z' = 0 COND2(z, z', z'') -{ 1 }-> 1 + COND1(0, z' - 1, z'') + GR(1 + (z' - 1), 0) :|: z'' >= 0, z = 1, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, z' - 1, z'') + 1 :|: z'' >= 0, z' - 1 >= 0, z = 1, 1 + (z' - 1) = 1 + z0, z0 >= 0 GR(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0 GR(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 GR(z, z') -{ 1 }-> 1 + GR(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond1(z, z', z'') -{ 0 }-> cond2(2, z', 1 + (z'' - 1)) :|: z = 2, z'' - 1 >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> cond2(1, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> cond2(0, z', z'') :|: z = 2, z'' >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(2, z', 0) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(2, z', z'' - 1) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(1, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', 0) :|: z = 2, z'' >= 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', z'' - 1) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond1(2, 0, z'') :|: z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> cond1(2, z' - 1, z'') :|: z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> cond1(1, 0, z'') :|: z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z'') :|: z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z'') :|: z'' >= 0, z = 1, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond1(0, z' - 1, z'') :|: z'' >= 0, z = 1, z' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 gr(z, z') -{ 0 }-> gr(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 gr(z, z') -{ 0 }-> 2 :|: z - 1 >= 0, z' = 0 gr(z, z') -{ 0 }-> 1 :|: z' >= 0, z = 0 gr(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 p(z) -{ 0 }-> 0 :|: z = 0 p(z) -{ 0 }-> 0 :|: z >= 0 p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0 Function symbols to be analyzed: {gr}, {cond2,cond1}, {p}, {COND2,COND1} Previous analysis results are: P: runtime: O(1) [1], size: O(1) [1] GR: runtime: O(n^1) [2 + z'], size: O(n^1) [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: COND1(z, z', z'') -{ 3 }-> 1 + COND2(2, z', 1 + (z'' - 1)) + s' :|: s' >= 0, s' <= 1 + (z'' - 1), z = 2, z'' - 1 >= 0, z' >= 0 COND1(z, z', z'') -{ 3 }-> 1 + COND2(1, z', 0) + s :|: s >= 0, s <= 0, z = 2, z'' = 0, z' >= 0 COND1(z, z', z'') -{ 3 }-> 1 + COND2(0, z', z'') + s'' :|: s'' >= 0, s'' <= z'', z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(2, z', 0) + s3 :|: s3 >= 0, s3 <= 1 + (z'' - 1), z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', 0) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(2, z', z'' - 1) + s2 :|: s2 >= 0, s2 <= 1 + (z'' - 1), z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', z'' - 1) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(1, z', 0) + s1 :|: s1 >= 0, s1 <= 0, z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(1, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', 0) + s4 :|: s4 >= 0, s4 <= 0, z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', 0) + s6 :|: s6 >= 0, s6 <= z'', z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 1 :|: z = 2, z'' >= 0, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' >= 0, z' >= 0, z'' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', z'' - 1) + s5 :|: s5 >= 0, s5 <= 1 + (z'' - 1), z = 2, z'' - 1 >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', z'' - 1) + 1 :|: z = 2, z' >= 0, z'' - 1 >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(2, 0, z'') + s9 :|: s9 >= 0, s9 <= 1 + (z' - 1), z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, 0, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(2, z' - 1, z'') + s8 :|: s8 >= 0, s8 <= 1 + (z' - 1), z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, z' - 1, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(1, 0, z'') + s7 :|: s7 >= 0, s7 <= 0, z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(1, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, 0, z'') + s10 :|: s10 >= 0, s10 <= 0, z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, 0, z'') + s12 :|: s12 >= 0, s12 <= z', z'' >= 0, z = 1, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 1 :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' >= 0, z' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, z' - 1, z'') + s11 :|: s11 >= 0, s11 <= 1 + (z' - 1), z'' >= 0, z = 1, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, z' - 1, z'') + 1 :|: z'' >= 0, z' - 1 >= 0, z = 1, 1 + (z' - 1) = 1 + z0, z0 >= 0 GR(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0 GR(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 GR(z, z') -{ 2 + z' }-> 1 + s13 :|: s13 >= 0, s13 <= z - 1, z' - 1 >= 0, z - 1 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond1(z, z', z'') -{ 0 }-> cond2(2, z', 1 + (z'' - 1)) :|: z = 2, z'' - 1 >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> cond2(1, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> cond2(0, z', z'') :|: z = 2, z'' >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(2, z', 0) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(2, z', z'' - 1) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(1, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', 0) :|: z = 2, z'' >= 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', z'' - 1) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond1(2, 0, z'') :|: z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> cond1(2, z' - 1, z'') :|: z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> cond1(1, 0, z'') :|: z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z'') :|: z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z'') :|: z'' >= 0, z = 1, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond1(0, z' - 1, z'') :|: z'' >= 0, z = 1, z' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 gr(z, z') -{ 0 }-> gr(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 gr(z, z') -{ 0 }-> 2 :|: z - 1 >= 0, z' = 0 gr(z, z') -{ 0 }-> 1 :|: z' >= 0, z = 0 gr(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 p(z) -{ 0 }-> 0 :|: z = 0 p(z) -{ 0 }-> 0 :|: z >= 0 p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0 Function symbols to be analyzed: {gr}, {cond2,cond1}, {p}, {COND2,COND1} Previous analysis results are: P: runtime: O(1) [1], size: O(1) [1] GR: runtime: O(n^1) [2 + z'], size: O(n^1) [z] ---------------------------------------- (33) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: gr after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 2 ---------------------------------------- (34) Obligation: Complexity RNTS consisting of the following rules: COND1(z, z', z'') -{ 3 }-> 1 + COND2(2, z', 1 + (z'' - 1)) + s' :|: s' >= 0, s' <= 1 + (z'' - 1), z = 2, z'' - 1 >= 0, z' >= 0 COND1(z, z', z'') -{ 3 }-> 1 + COND2(1, z', 0) + s :|: s >= 0, s <= 0, z = 2, z'' = 0, z' >= 0 COND1(z, z', z'') -{ 3 }-> 1 + COND2(0, z', z'') + s'' :|: s'' >= 0, s'' <= z'', z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(2, z', 0) + s3 :|: s3 >= 0, s3 <= 1 + (z'' - 1), z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', 0) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(2, z', z'' - 1) + s2 :|: s2 >= 0, s2 <= 1 + (z'' - 1), z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', z'' - 1) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(1, z', 0) + s1 :|: s1 >= 0, s1 <= 0, z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(1, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', 0) + s4 :|: s4 >= 0, s4 <= 0, z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', 0) + s6 :|: s6 >= 0, s6 <= z'', z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 1 :|: z = 2, z'' >= 0, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' >= 0, z' >= 0, z'' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', z'' - 1) + s5 :|: s5 >= 0, s5 <= 1 + (z'' - 1), z = 2, z'' - 1 >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', z'' - 1) + 1 :|: z = 2, z' >= 0, z'' - 1 >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(2, 0, z'') + s9 :|: s9 >= 0, s9 <= 1 + (z' - 1), z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, 0, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(2, z' - 1, z'') + s8 :|: s8 >= 0, s8 <= 1 + (z' - 1), z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, z' - 1, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(1, 0, z'') + s7 :|: s7 >= 0, s7 <= 0, z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(1, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, 0, z'') + s10 :|: s10 >= 0, s10 <= 0, z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, 0, z'') + s12 :|: s12 >= 0, s12 <= z', z'' >= 0, z = 1, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 1 :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' >= 0, z' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, z' - 1, z'') + s11 :|: s11 >= 0, s11 <= 1 + (z' - 1), z'' >= 0, z = 1, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, z' - 1, z'') + 1 :|: z'' >= 0, z' - 1 >= 0, z = 1, 1 + (z' - 1) = 1 + z0, z0 >= 0 GR(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0 GR(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 GR(z, z') -{ 2 + z' }-> 1 + s13 :|: s13 >= 0, s13 <= z - 1, z' - 1 >= 0, z - 1 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond1(z, z', z'') -{ 0 }-> cond2(2, z', 1 + (z'' - 1)) :|: z = 2, z'' - 1 >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> cond2(1, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> cond2(0, z', z'') :|: z = 2, z'' >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(2, z', 0) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(2, z', z'' - 1) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(1, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', 0) :|: z = 2, z'' >= 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', z'' - 1) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond1(2, 0, z'') :|: z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> cond1(2, z' - 1, z'') :|: z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> cond1(1, 0, z'') :|: z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z'') :|: z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z'') :|: z'' >= 0, z = 1, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond1(0, z' - 1, z'') :|: z'' >= 0, z = 1, z' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 gr(z, z') -{ 0 }-> gr(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 gr(z, z') -{ 0 }-> 2 :|: z - 1 >= 0, z' = 0 gr(z, z') -{ 0 }-> 1 :|: z' >= 0, z = 0 gr(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 p(z) -{ 0 }-> 0 :|: z = 0 p(z) -{ 0 }-> 0 :|: z >= 0 p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0 Function symbols to be analyzed: {gr}, {cond2,cond1}, {p}, {COND2,COND1} Previous analysis results are: P: runtime: O(1) [1], size: O(1) [1] GR: runtime: O(n^1) [2 + z'], size: O(n^1) [z] gr: runtime: ?, size: O(1) [2] ---------------------------------------- (35) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: gr after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 0 ---------------------------------------- (36) Obligation: Complexity RNTS consisting of the following rules: COND1(z, z', z'') -{ 3 }-> 1 + COND2(2, z', 1 + (z'' - 1)) + s' :|: s' >= 0, s' <= 1 + (z'' - 1), z = 2, z'' - 1 >= 0, z' >= 0 COND1(z, z', z'') -{ 3 }-> 1 + COND2(1, z', 0) + s :|: s >= 0, s <= 0, z = 2, z'' = 0, z' >= 0 COND1(z, z', z'') -{ 3 }-> 1 + COND2(0, z', z'') + s'' :|: s'' >= 0, s'' <= z'', z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(2, z', 0) + s3 :|: s3 >= 0, s3 <= 1 + (z'' - 1), z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', 0) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(2, z', z'' - 1) + s2 :|: s2 >= 0, s2 <= 1 + (z'' - 1), z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', z'' - 1) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(1, z', 0) + s1 :|: s1 >= 0, s1 <= 0, z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(1, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', 0) + s4 :|: s4 >= 0, s4 <= 0, z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', 0) + s6 :|: s6 >= 0, s6 <= z'', z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 1 :|: z = 2, z'' >= 0, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' >= 0, z' >= 0, z'' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', z'' - 1) + s5 :|: s5 >= 0, s5 <= 1 + (z'' - 1), z = 2, z'' - 1 >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', z'' - 1) + 1 :|: z = 2, z' >= 0, z'' - 1 >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(2, 0, z'') + s9 :|: s9 >= 0, s9 <= 1 + (z' - 1), z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, 0, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(2, z' - 1, z'') + s8 :|: s8 >= 0, s8 <= 1 + (z' - 1), z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, z' - 1, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(1, 0, z'') + s7 :|: s7 >= 0, s7 <= 0, z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(1, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, 0, z'') + s10 :|: s10 >= 0, s10 <= 0, z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, 0, z'') + s12 :|: s12 >= 0, s12 <= z', z'' >= 0, z = 1, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 1 :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' >= 0, z' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, z' - 1, z'') + s11 :|: s11 >= 0, s11 <= 1 + (z' - 1), z'' >= 0, z = 1, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, z' - 1, z'') + 1 :|: z'' >= 0, z' - 1 >= 0, z = 1, 1 + (z' - 1) = 1 + z0, z0 >= 0 GR(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0 GR(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 GR(z, z') -{ 2 + z' }-> 1 + s13 :|: s13 >= 0, s13 <= z - 1, z' - 1 >= 0, z - 1 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond1(z, z', z'') -{ 0 }-> cond2(2, z', 1 + (z'' - 1)) :|: z = 2, z'' - 1 >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> cond2(1, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> cond2(0, z', z'') :|: z = 2, z'' >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(2, z', 0) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(2, z', z'' - 1) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(1, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', 0) :|: z = 2, z'' >= 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', z'' - 1) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond1(2, 0, z'') :|: z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> cond1(2, z' - 1, z'') :|: z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> cond1(1, 0, z'') :|: z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z'') :|: z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z'') :|: z'' >= 0, z = 1, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond1(0, z' - 1, z'') :|: z'' >= 0, z = 1, z' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 gr(z, z') -{ 0 }-> gr(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0 gr(z, z') -{ 0 }-> 2 :|: z - 1 >= 0, z' = 0 gr(z, z') -{ 0 }-> 1 :|: z' >= 0, z = 0 gr(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 p(z) -{ 0 }-> 0 :|: z = 0 p(z) -{ 0 }-> 0 :|: z >= 0 p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0 Function symbols to be analyzed: {cond2,cond1}, {p}, {COND2,COND1} Previous analysis results are: P: runtime: O(1) [1], size: O(1) [1] GR: runtime: O(n^1) [2 + z'], size: O(n^1) [z] gr: runtime: O(1) [0], size: O(1) [2] ---------------------------------------- (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: COND1(z, z', z'') -{ 3 }-> 1 + COND2(2, z', 1 + (z'' - 1)) + s' :|: s' >= 0, s' <= 1 + (z'' - 1), z = 2, z'' - 1 >= 0, z' >= 0 COND1(z, z', z'') -{ 3 }-> 1 + COND2(1, z', 0) + s :|: s >= 0, s <= 0, z = 2, z'' = 0, z' >= 0 COND1(z, z', z'') -{ 3 }-> 1 + COND2(0, z', z'') + s'' :|: s'' >= 0, s'' <= z'', z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(2, z', 0) + s3 :|: s3 >= 0, s3 <= 1 + (z'' - 1), z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', 0) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(2, z', z'' - 1) + s2 :|: s2 >= 0, s2 <= 1 + (z'' - 1), z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', z'' - 1) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(1, z', 0) + s1 :|: s1 >= 0, s1 <= 0, z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(1, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', 0) + s4 :|: s4 >= 0, s4 <= 0, z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', 0) + s6 :|: s6 >= 0, s6 <= z'', z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 1 :|: z = 2, z'' >= 0, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' >= 0, z' >= 0, z'' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', z'' - 1) + s5 :|: s5 >= 0, s5 <= 1 + (z'' - 1), z = 2, z'' - 1 >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', z'' - 1) + 1 :|: z = 2, z' >= 0, z'' - 1 >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(2, 0, z'') + s9 :|: s9 >= 0, s9 <= 1 + (z' - 1), z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, 0, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(2, z' - 1, z'') + s8 :|: s8 >= 0, s8 <= 1 + (z' - 1), z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, z' - 1, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(1, 0, z'') + s7 :|: s7 >= 0, s7 <= 0, z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(1, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, 0, z'') + s10 :|: s10 >= 0, s10 <= 0, z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, 0, z'') + s12 :|: s12 >= 0, s12 <= z', z'' >= 0, z = 1, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 1 :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' >= 0, z' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, z' - 1, z'') + s11 :|: s11 >= 0, s11 <= 1 + (z' - 1), z'' >= 0, z = 1, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, z' - 1, z'') + 1 :|: z'' >= 0, z' - 1 >= 0, z = 1, 1 + (z' - 1) = 1 + z0, z0 >= 0 GR(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0 GR(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 GR(z, z') -{ 2 + z' }-> 1 + s13 :|: s13 >= 0, s13 <= z - 1, z' - 1 >= 0, z - 1 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond1(z, z', z'') -{ 0 }-> cond2(2, z', 1 + (z'' - 1)) :|: z = 2, z'' - 1 >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> cond2(1, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> cond2(0, z', z'') :|: z = 2, z'' >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(2, z', 0) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(2, z', z'' - 1) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(1, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', 0) :|: z = 2, z'' >= 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', z'' - 1) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond1(2, 0, z'') :|: z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> cond1(2, z' - 1, z'') :|: z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> cond1(1, 0, z'') :|: z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z'') :|: z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z'') :|: z'' >= 0, z = 1, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond1(0, z' - 1, z'') :|: z'' >= 0, z = 1, z' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 gr(z, z') -{ 0 }-> s14 :|: s14 >= 0, s14 <= 2, z' - 1 >= 0, z - 1 >= 0 gr(z, z') -{ 0 }-> 2 :|: z - 1 >= 0, z' = 0 gr(z, z') -{ 0 }-> 1 :|: z' >= 0, z = 0 gr(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 p(z) -{ 0 }-> 0 :|: z = 0 p(z) -{ 0 }-> 0 :|: z >= 0 p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0 Function symbols to be analyzed: {cond2,cond1}, {p}, {COND2,COND1} Previous analysis results are: P: runtime: O(1) [1], size: O(1) [1] GR: runtime: O(n^1) [2 + z'], size: O(n^1) [z] gr: runtime: O(1) [0], size: O(1) [2] ---------------------------------------- (39) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using KoAT for: cond2 after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 0 Computed SIZE bound using CoFloCo for: cond1 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: COND1(z, z', z'') -{ 3 }-> 1 + COND2(2, z', 1 + (z'' - 1)) + s' :|: s' >= 0, s' <= 1 + (z'' - 1), z = 2, z'' - 1 >= 0, z' >= 0 COND1(z, z', z'') -{ 3 }-> 1 + COND2(1, z', 0) + s :|: s >= 0, s <= 0, z = 2, z'' = 0, z' >= 0 COND1(z, z', z'') -{ 3 }-> 1 + COND2(0, z', z'') + s'' :|: s'' >= 0, s'' <= z'', z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(2, z', 0) + s3 :|: s3 >= 0, s3 <= 1 + (z'' - 1), z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', 0) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(2, z', z'' - 1) + s2 :|: s2 >= 0, s2 <= 1 + (z'' - 1), z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', z'' - 1) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(1, z', 0) + s1 :|: s1 >= 0, s1 <= 0, z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(1, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', 0) + s4 :|: s4 >= 0, s4 <= 0, z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', 0) + s6 :|: s6 >= 0, s6 <= z'', z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 1 :|: z = 2, z'' >= 0, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' >= 0, z' >= 0, z'' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', z'' - 1) + s5 :|: s5 >= 0, s5 <= 1 + (z'' - 1), z = 2, z'' - 1 >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', z'' - 1) + 1 :|: z = 2, z' >= 0, z'' - 1 >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(2, 0, z'') + s9 :|: s9 >= 0, s9 <= 1 + (z' - 1), z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, 0, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(2, z' - 1, z'') + s8 :|: s8 >= 0, s8 <= 1 + (z' - 1), z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, z' - 1, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(1, 0, z'') + s7 :|: s7 >= 0, s7 <= 0, z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(1, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, 0, z'') + s10 :|: s10 >= 0, s10 <= 0, z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, 0, z'') + s12 :|: s12 >= 0, s12 <= z', z'' >= 0, z = 1, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 1 :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' >= 0, z' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, z' - 1, z'') + s11 :|: s11 >= 0, s11 <= 1 + (z' - 1), z'' >= 0, z = 1, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, z' - 1, z'') + 1 :|: z'' >= 0, z' - 1 >= 0, z = 1, 1 + (z' - 1) = 1 + z0, z0 >= 0 GR(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0 GR(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 GR(z, z') -{ 2 + z' }-> 1 + s13 :|: s13 >= 0, s13 <= z - 1, z' - 1 >= 0, z - 1 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond1(z, z', z'') -{ 0 }-> cond2(2, z', 1 + (z'' - 1)) :|: z = 2, z'' - 1 >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> cond2(1, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> cond2(0, z', z'') :|: z = 2, z'' >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(2, z', 0) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(2, z', z'' - 1) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(1, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', 0) :|: z = 2, z'' >= 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', z'' - 1) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond1(2, 0, z'') :|: z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> cond1(2, z' - 1, z'') :|: z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> cond1(1, 0, z'') :|: z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z'') :|: z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z'') :|: z'' >= 0, z = 1, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond1(0, z' - 1, z'') :|: z'' >= 0, z = 1, z' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 gr(z, z') -{ 0 }-> s14 :|: s14 >= 0, s14 <= 2, z' - 1 >= 0, z - 1 >= 0 gr(z, z') -{ 0 }-> 2 :|: z - 1 >= 0, z' = 0 gr(z, z') -{ 0 }-> 1 :|: z' >= 0, z = 0 gr(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 p(z) -{ 0 }-> 0 :|: z = 0 p(z) -{ 0 }-> 0 :|: z >= 0 p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0 Function symbols to be analyzed: {cond2,cond1}, {p}, {COND2,COND1} Previous analysis results are: P: runtime: O(1) [1], size: O(1) [1] GR: runtime: O(n^1) [2 + z'], size: O(n^1) [z] gr: runtime: O(1) [0], size: O(1) [2] cond2: runtime: ?, size: O(1) [0] cond1: runtime: ?, size: O(1) [0] ---------------------------------------- (41) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: cond2 after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 0 Computed RUNTIME bound using CoFloCo for: cond1 after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 0 ---------------------------------------- (42) Obligation: Complexity RNTS consisting of the following rules: COND1(z, z', z'') -{ 3 }-> 1 + COND2(2, z', 1 + (z'' - 1)) + s' :|: s' >= 0, s' <= 1 + (z'' - 1), z = 2, z'' - 1 >= 0, z' >= 0 COND1(z, z', z'') -{ 3 }-> 1 + COND2(1, z', 0) + s :|: s >= 0, s <= 0, z = 2, z'' = 0, z' >= 0 COND1(z, z', z'') -{ 3 }-> 1 + COND2(0, z', z'') + s'' :|: s'' >= 0, s'' <= z'', z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(2, z', 0) + s3 :|: s3 >= 0, s3 <= 1 + (z'' - 1), z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', 0) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(2, z', z'' - 1) + s2 :|: s2 >= 0, s2 <= 1 + (z'' - 1), z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', z'' - 1) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(1, z', 0) + s1 :|: s1 >= 0, s1 <= 0, z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(1, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', 0) + s4 :|: s4 >= 0, s4 <= 0, z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', 0) + s6 :|: s6 >= 0, s6 <= z'', z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 1 :|: z = 2, z'' >= 0, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' >= 0, z' >= 0, z'' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', z'' - 1) + s5 :|: s5 >= 0, s5 <= 1 + (z'' - 1), z = 2, z'' - 1 >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', z'' - 1) + 1 :|: z = 2, z' >= 0, z'' - 1 >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(2, 0, z'') + s9 :|: s9 >= 0, s9 <= 1 + (z' - 1), z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, 0, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(2, z' - 1, z'') + s8 :|: s8 >= 0, s8 <= 1 + (z' - 1), z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, z' - 1, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(1, 0, z'') + s7 :|: s7 >= 0, s7 <= 0, z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(1, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, 0, z'') + s10 :|: s10 >= 0, s10 <= 0, z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, 0, z'') + s12 :|: s12 >= 0, s12 <= z', z'' >= 0, z = 1, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 1 :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' >= 0, z' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, z' - 1, z'') + s11 :|: s11 >= 0, s11 <= 1 + (z' - 1), z'' >= 0, z = 1, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, z' - 1, z'') + 1 :|: z'' >= 0, z' - 1 >= 0, z = 1, 1 + (z' - 1) = 1 + z0, z0 >= 0 GR(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0 GR(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 GR(z, z') -{ 2 + z' }-> 1 + s13 :|: s13 >= 0, s13 <= z - 1, z' - 1 >= 0, z - 1 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond1(z, z', z'') -{ 0 }-> cond2(2, z', 1 + (z'' - 1)) :|: z = 2, z'' - 1 >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> cond2(1, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> cond2(0, z', z'') :|: z = 2, z'' >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(2, z', 0) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(2, z', z'' - 1) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond2(1, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', 0) :|: z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', 0) :|: z = 2, z'' >= 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond2(0, z', z'' - 1) :|: z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> cond1(2, 0, z'') :|: z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> cond1(2, z' - 1, z'') :|: z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> cond1(1, 0, z'') :|: z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z'') :|: z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> cond1(0, 0, z'') :|: z'' >= 0, z = 1, z' >= 0 cond2(z, z', z'') -{ 0 }-> cond1(0, z' - 1, z'') :|: z'' >= 0, z = 1, z' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 gr(z, z') -{ 0 }-> s14 :|: s14 >= 0, s14 <= 2, z' - 1 >= 0, z - 1 >= 0 gr(z, z') -{ 0 }-> 2 :|: z - 1 >= 0, z' = 0 gr(z, z') -{ 0 }-> 1 :|: z' >= 0, z = 0 gr(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 p(z) -{ 0 }-> 0 :|: z = 0 p(z) -{ 0 }-> 0 :|: z >= 0 p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0 Function symbols to be analyzed: {p}, {COND2,COND1} Previous analysis results are: P: runtime: O(1) [1], size: O(1) [1] GR: runtime: O(n^1) [2 + z'], size: O(n^1) [z] gr: runtime: O(1) [0], size: O(1) [2] cond2: runtime: O(1) [0], size: O(1) [0] cond1: runtime: O(1) [0], 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: COND1(z, z', z'') -{ 3 }-> 1 + COND2(2, z', 1 + (z'' - 1)) + s' :|: s' >= 0, s' <= 1 + (z'' - 1), z = 2, z'' - 1 >= 0, z' >= 0 COND1(z, z', z'') -{ 3 }-> 1 + COND2(1, z', 0) + s :|: s >= 0, s <= 0, z = 2, z'' = 0, z' >= 0 COND1(z, z', z'') -{ 3 }-> 1 + COND2(0, z', z'') + s'' :|: s'' >= 0, s'' <= z'', z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(2, z', 0) + s3 :|: s3 >= 0, s3 <= 1 + (z'' - 1), z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', 0) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(2, z', z'' - 1) + s2 :|: s2 >= 0, s2 <= 1 + (z'' - 1), z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', z'' - 1) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(1, z', 0) + s1 :|: s1 >= 0, s1 <= 0, z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(1, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', 0) + s4 :|: s4 >= 0, s4 <= 0, z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', 0) + s6 :|: s6 >= 0, s6 <= z'', z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 1 :|: z = 2, z'' >= 0, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' >= 0, z' >= 0, z'' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', z'' - 1) + s5 :|: s5 >= 0, s5 <= 1 + (z'' - 1), z = 2, z'' - 1 >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', z'' - 1) + 1 :|: z = 2, z' >= 0, z'' - 1 >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(2, 0, z'') + s9 :|: s9 >= 0, s9 <= 1 + (z' - 1), z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, 0, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(2, z' - 1, z'') + s8 :|: s8 >= 0, s8 <= 1 + (z' - 1), z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, z' - 1, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(1, 0, z'') + s7 :|: s7 >= 0, s7 <= 0, z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(1, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, 0, z'') + s10 :|: s10 >= 0, s10 <= 0, z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, 0, z'') + s12 :|: s12 >= 0, s12 <= z', z'' >= 0, z = 1, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 1 :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' >= 0, z' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, z' - 1, z'') + s11 :|: s11 >= 0, s11 <= 1 + (z' - 1), z'' >= 0, z = 1, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, z' - 1, z'') + 1 :|: z'' >= 0, z' - 1 >= 0, z = 1, 1 + (z' - 1) = 1 + z0, z0 >= 0 GR(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0 GR(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 GR(z, z') -{ 2 + z' }-> 1 + s13 :|: s13 >= 0, s13 <= z - 1, z' - 1 >= 0, z - 1 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond1(z, z', z'') -{ 0 }-> s15 :|: s15 >= 0, s15 <= 0, z = 2, z'' = 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> s16 :|: s16 >= 0, s16 <= 0, z = 2, z'' - 1 >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> s17 :|: s17 >= 0, s17 <= 0, z = 2, z'' >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 cond2(z, z', z'') -{ 0 }-> s18 :|: s18 >= 0, s18 <= 0, z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> s19 :|: s19 >= 0, s19 <= 0, z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> s20 :|: s20 >= 0, s20 <= 0, z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> s21 :|: s21 >= 0, s21 <= 0, z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> s22 :|: s22 >= 0, s22 <= 0, z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> s23 :|: s23 >= 0, s23 <= 0, z = 2, z'' >= 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> s24 :|: s24 >= 0, s24 <= 0, z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> s25 :|: s25 >= 0, s25 <= 0, z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> s26 :|: s26 >= 0, s26 <= 0, z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> s27 :|: s27 >= 0, s27 <= 0, z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> s28 :|: s28 >= 0, s28 <= 0, z'' >= 0, z = 1, z' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> s29 :|: s29 >= 0, s29 <= 0, z'' >= 0, z = 1, z' >= 0 cond2(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 gr(z, z') -{ 0 }-> s14 :|: s14 >= 0, s14 <= 2, z' - 1 >= 0, z - 1 >= 0 gr(z, z') -{ 0 }-> 2 :|: z - 1 >= 0, z' = 0 gr(z, z') -{ 0 }-> 1 :|: z' >= 0, z = 0 gr(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 p(z) -{ 0 }-> 0 :|: z = 0 p(z) -{ 0 }-> 0 :|: z >= 0 p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0 Function symbols to be analyzed: {p}, {COND2,COND1} Previous analysis results are: P: runtime: O(1) [1], size: O(1) [1] GR: runtime: O(n^1) [2 + z'], size: O(n^1) [z] gr: runtime: O(1) [0], size: O(1) [2] cond2: runtime: O(1) [0], size: O(1) [0] cond1: runtime: O(1) [0], size: O(1) [0] ---------------------------------------- (45) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using KoAT for: p after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: z ---------------------------------------- (46) Obligation: Complexity RNTS consisting of the following rules: COND1(z, z', z'') -{ 3 }-> 1 + COND2(2, z', 1 + (z'' - 1)) + s' :|: s' >= 0, s' <= 1 + (z'' - 1), z = 2, z'' - 1 >= 0, z' >= 0 COND1(z, z', z'') -{ 3 }-> 1 + COND2(1, z', 0) + s :|: s >= 0, s <= 0, z = 2, z'' = 0, z' >= 0 COND1(z, z', z'') -{ 3 }-> 1 + COND2(0, z', z'') + s'' :|: s'' >= 0, s'' <= z'', z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(2, z', 0) + s3 :|: s3 >= 0, s3 <= 1 + (z'' - 1), z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', 0) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(2, z', z'' - 1) + s2 :|: s2 >= 0, s2 <= 1 + (z'' - 1), z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', z'' - 1) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(1, z', 0) + s1 :|: s1 >= 0, s1 <= 0, z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(1, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', 0) + s4 :|: s4 >= 0, s4 <= 0, z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', 0) + s6 :|: s6 >= 0, s6 <= z'', z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 1 :|: z = 2, z'' >= 0, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' >= 0, z' >= 0, z'' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', z'' - 1) + s5 :|: s5 >= 0, s5 <= 1 + (z'' - 1), z = 2, z'' - 1 >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', z'' - 1) + 1 :|: z = 2, z' >= 0, z'' - 1 >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(2, 0, z'') + s9 :|: s9 >= 0, s9 <= 1 + (z' - 1), z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, 0, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(2, z' - 1, z'') + s8 :|: s8 >= 0, s8 <= 1 + (z' - 1), z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, z' - 1, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(1, 0, z'') + s7 :|: s7 >= 0, s7 <= 0, z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(1, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, 0, z'') + s10 :|: s10 >= 0, s10 <= 0, z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, 0, z'') + s12 :|: s12 >= 0, s12 <= z', z'' >= 0, z = 1, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 1 :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' >= 0, z' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, z' - 1, z'') + s11 :|: s11 >= 0, s11 <= 1 + (z' - 1), z'' >= 0, z = 1, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, z' - 1, z'') + 1 :|: z'' >= 0, z' - 1 >= 0, z = 1, 1 + (z' - 1) = 1 + z0, z0 >= 0 GR(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0 GR(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 GR(z, z') -{ 2 + z' }-> 1 + s13 :|: s13 >= 0, s13 <= z - 1, z' - 1 >= 0, z - 1 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond1(z, z', z'') -{ 0 }-> s15 :|: s15 >= 0, s15 <= 0, z = 2, z'' = 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> s16 :|: s16 >= 0, s16 <= 0, z = 2, z'' - 1 >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> s17 :|: s17 >= 0, s17 <= 0, z = 2, z'' >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 cond2(z, z', z'') -{ 0 }-> s18 :|: s18 >= 0, s18 <= 0, z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> s19 :|: s19 >= 0, s19 <= 0, z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> s20 :|: s20 >= 0, s20 <= 0, z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> s21 :|: s21 >= 0, s21 <= 0, z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> s22 :|: s22 >= 0, s22 <= 0, z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> s23 :|: s23 >= 0, s23 <= 0, z = 2, z'' >= 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> s24 :|: s24 >= 0, s24 <= 0, z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> s25 :|: s25 >= 0, s25 <= 0, z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> s26 :|: s26 >= 0, s26 <= 0, z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> s27 :|: s27 >= 0, s27 <= 0, z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> s28 :|: s28 >= 0, s28 <= 0, z'' >= 0, z = 1, z' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> s29 :|: s29 >= 0, s29 <= 0, z'' >= 0, z = 1, z' >= 0 cond2(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 gr(z, z') -{ 0 }-> s14 :|: s14 >= 0, s14 <= 2, z' - 1 >= 0, z - 1 >= 0 gr(z, z') -{ 0 }-> 2 :|: z - 1 >= 0, z' = 0 gr(z, z') -{ 0 }-> 1 :|: z' >= 0, z = 0 gr(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 p(z) -{ 0 }-> 0 :|: z = 0 p(z) -{ 0 }-> 0 :|: z >= 0 p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0 Function symbols to be analyzed: {p}, {COND2,COND1} Previous analysis results are: P: runtime: O(1) [1], size: O(1) [1] GR: runtime: O(n^1) [2 + z'], size: O(n^1) [z] gr: runtime: O(1) [0], size: O(1) [2] cond2: runtime: O(1) [0], size: O(1) [0] cond1: runtime: O(1) [0], size: O(1) [0] p: runtime: ?, size: O(n^1) [z] ---------------------------------------- (47) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: p 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: COND1(z, z', z'') -{ 3 }-> 1 + COND2(2, z', 1 + (z'' - 1)) + s' :|: s' >= 0, s' <= 1 + (z'' - 1), z = 2, z'' - 1 >= 0, z' >= 0 COND1(z, z', z'') -{ 3 }-> 1 + COND2(1, z', 0) + s :|: s >= 0, s <= 0, z = 2, z'' = 0, z' >= 0 COND1(z, z', z'') -{ 3 }-> 1 + COND2(0, z', z'') + s'' :|: s'' >= 0, s'' <= z'', z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(2, z', 0) + s3 :|: s3 >= 0, s3 <= 1 + (z'' - 1), z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', 0) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(2, z', z'' - 1) + s2 :|: s2 >= 0, s2 <= 1 + (z'' - 1), z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', z'' - 1) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(1, z', 0) + s1 :|: s1 >= 0, s1 <= 0, z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(1, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', 0) + s4 :|: s4 >= 0, s4 <= 0, z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', 0) + s6 :|: s6 >= 0, s6 <= z'', z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 1 :|: z = 2, z'' >= 0, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' >= 0, z' >= 0, z'' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', z'' - 1) + s5 :|: s5 >= 0, s5 <= 1 + (z'' - 1), z = 2, z'' - 1 >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', z'' - 1) + 1 :|: z = 2, z' >= 0, z'' - 1 >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(2, 0, z'') + s9 :|: s9 >= 0, s9 <= 1 + (z' - 1), z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, 0, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(2, z' - 1, z'') + s8 :|: s8 >= 0, s8 <= 1 + (z' - 1), z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, z' - 1, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(1, 0, z'') + s7 :|: s7 >= 0, s7 <= 0, z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(1, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, 0, z'') + s10 :|: s10 >= 0, s10 <= 0, z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, 0, z'') + s12 :|: s12 >= 0, s12 <= z', z'' >= 0, z = 1, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 1 :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' >= 0, z' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, z' - 1, z'') + s11 :|: s11 >= 0, s11 <= 1 + (z' - 1), z'' >= 0, z = 1, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, z' - 1, z'') + 1 :|: z'' >= 0, z' - 1 >= 0, z = 1, 1 + (z' - 1) = 1 + z0, z0 >= 0 GR(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0 GR(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 GR(z, z') -{ 2 + z' }-> 1 + s13 :|: s13 >= 0, s13 <= z - 1, z' - 1 >= 0, z - 1 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond1(z, z', z'') -{ 0 }-> s15 :|: s15 >= 0, s15 <= 0, z = 2, z'' = 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> s16 :|: s16 >= 0, s16 <= 0, z = 2, z'' - 1 >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> s17 :|: s17 >= 0, s17 <= 0, z = 2, z'' >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 cond2(z, z', z'') -{ 0 }-> s18 :|: s18 >= 0, s18 <= 0, z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> s19 :|: s19 >= 0, s19 <= 0, z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> s20 :|: s20 >= 0, s20 <= 0, z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> s21 :|: s21 >= 0, s21 <= 0, z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> s22 :|: s22 >= 0, s22 <= 0, z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> s23 :|: s23 >= 0, s23 <= 0, z = 2, z'' >= 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> s24 :|: s24 >= 0, s24 <= 0, z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> s25 :|: s25 >= 0, s25 <= 0, z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> s26 :|: s26 >= 0, s26 <= 0, z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> s27 :|: s27 >= 0, s27 <= 0, z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> s28 :|: s28 >= 0, s28 <= 0, z'' >= 0, z = 1, z' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> s29 :|: s29 >= 0, s29 <= 0, z'' >= 0, z = 1, z' >= 0 cond2(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 gr(z, z') -{ 0 }-> s14 :|: s14 >= 0, s14 <= 2, z' - 1 >= 0, z - 1 >= 0 gr(z, z') -{ 0 }-> 2 :|: z - 1 >= 0, z' = 0 gr(z, z') -{ 0 }-> 1 :|: z' >= 0, z = 0 gr(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 p(z) -{ 0 }-> 0 :|: z = 0 p(z) -{ 0 }-> 0 :|: z >= 0 p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0 Function symbols to be analyzed: {COND2,COND1} Previous analysis results are: P: runtime: O(1) [1], size: O(1) [1] GR: runtime: O(n^1) [2 + z'], size: O(n^1) [z] gr: runtime: O(1) [0], size: O(1) [2] cond2: runtime: O(1) [0], size: O(1) [0] cond1: runtime: O(1) [0], size: O(1) [0] p: runtime: O(1) [0], size: O(n^1) [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: COND1(z, z', z'') -{ 3 }-> 1 + COND2(2, z', 1 + (z'' - 1)) + s' :|: s' >= 0, s' <= 1 + (z'' - 1), z = 2, z'' - 1 >= 0, z' >= 0 COND1(z, z', z'') -{ 3 }-> 1 + COND2(1, z', 0) + s :|: s >= 0, s <= 0, z = 2, z'' = 0, z' >= 0 COND1(z, z', z'') -{ 3 }-> 1 + COND2(0, z', z'') + s'' :|: s'' >= 0, s'' <= z'', z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(2, z', 0) + s3 :|: s3 >= 0, s3 <= 1 + (z'' - 1), z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', 0) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(2, z', z'' - 1) + s2 :|: s2 >= 0, s2 <= 1 + (z'' - 1), z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', z'' - 1) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(1, z', 0) + s1 :|: s1 >= 0, s1 <= 0, z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(1, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', 0) + s4 :|: s4 >= 0, s4 <= 0, z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', 0) + s6 :|: s6 >= 0, s6 <= z'', z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 1 :|: z = 2, z'' >= 0, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' >= 0, z' >= 0, z'' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', z'' - 1) + s5 :|: s5 >= 0, s5 <= 1 + (z'' - 1), z = 2, z'' - 1 >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', z'' - 1) + 1 :|: z = 2, z' >= 0, z'' - 1 >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(2, 0, z'') + s9 :|: s9 >= 0, s9 <= 1 + (z' - 1), z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, 0, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(2, z' - 1, z'') + s8 :|: s8 >= 0, s8 <= 1 + (z' - 1), z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, z' - 1, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(1, 0, z'') + s7 :|: s7 >= 0, s7 <= 0, z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(1, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, 0, z'') + s10 :|: s10 >= 0, s10 <= 0, z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, 0, z'') + s12 :|: s12 >= 0, s12 <= z', z'' >= 0, z = 1, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 1 :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' >= 0, z' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, z' - 1, z'') + s11 :|: s11 >= 0, s11 <= 1 + (z' - 1), z'' >= 0, z = 1, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, z' - 1, z'') + 1 :|: z'' >= 0, z' - 1 >= 0, z = 1, 1 + (z' - 1) = 1 + z0, z0 >= 0 GR(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0 GR(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 GR(z, z') -{ 2 + z' }-> 1 + s13 :|: s13 >= 0, s13 <= z - 1, z' - 1 >= 0, z - 1 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond1(z, z', z'') -{ 0 }-> s15 :|: s15 >= 0, s15 <= 0, z = 2, z'' = 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> s16 :|: s16 >= 0, s16 <= 0, z = 2, z'' - 1 >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> s17 :|: s17 >= 0, s17 <= 0, z = 2, z'' >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 cond2(z, z', z'') -{ 0 }-> s18 :|: s18 >= 0, s18 <= 0, z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> s19 :|: s19 >= 0, s19 <= 0, z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> s20 :|: s20 >= 0, s20 <= 0, z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> s21 :|: s21 >= 0, s21 <= 0, z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> s22 :|: s22 >= 0, s22 <= 0, z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> s23 :|: s23 >= 0, s23 <= 0, z = 2, z'' >= 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> s24 :|: s24 >= 0, s24 <= 0, z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> s25 :|: s25 >= 0, s25 <= 0, z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> s26 :|: s26 >= 0, s26 <= 0, z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> s27 :|: s27 >= 0, s27 <= 0, z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> s28 :|: s28 >= 0, s28 <= 0, z'' >= 0, z = 1, z' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> s29 :|: s29 >= 0, s29 <= 0, z'' >= 0, z = 1, z' >= 0 cond2(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 gr(z, z') -{ 0 }-> s14 :|: s14 >= 0, s14 <= 2, z' - 1 >= 0, z - 1 >= 0 gr(z, z') -{ 0 }-> 2 :|: z - 1 >= 0, z' = 0 gr(z, z') -{ 0 }-> 1 :|: z' >= 0, z = 0 gr(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 p(z) -{ 0 }-> 0 :|: z = 0 p(z) -{ 0 }-> 0 :|: z >= 0 p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0 Function symbols to be analyzed: {COND2,COND1} Previous analysis results are: P: runtime: O(1) [1], size: O(1) [1] GR: runtime: O(n^1) [2 + z'], size: O(n^1) [z] gr: runtime: O(1) [0], size: O(1) [2] cond2: runtime: O(1) [0], size: O(1) [0] cond1: runtime: O(1) [0], size: O(1) [0] p: runtime: O(1) [0], size: O(n^1) [z] ---------------------------------------- (51) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: COND2 after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 0 Computed SIZE bound using CoFloCo for: COND1 after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: 1 + z'' ---------------------------------------- (52) Obligation: Complexity RNTS consisting of the following rules: COND1(z, z', z'') -{ 3 }-> 1 + COND2(2, z', 1 + (z'' - 1)) + s' :|: s' >= 0, s' <= 1 + (z'' - 1), z = 2, z'' - 1 >= 0, z' >= 0 COND1(z, z', z'') -{ 3 }-> 1 + COND2(1, z', 0) + s :|: s >= 0, s <= 0, z = 2, z'' = 0, z' >= 0 COND1(z, z', z'') -{ 3 }-> 1 + COND2(0, z', z'') + s'' :|: s'' >= 0, s'' <= z'', z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(2, z', 0) + s3 :|: s3 >= 0, s3 <= 1 + (z'' - 1), z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', 0) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(2, z', z'' - 1) + s2 :|: s2 >= 0, s2 <= 1 + (z'' - 1), z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', z'' - 1) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(1, z', 0) + s1 :|: s1 >= 0, s1 <= 0, z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(1, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', 0) + s4 :|: s4 >= 0, s4 <= 0, z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', 0) + s6 :|: s6 >= 0, s6 <= z'', z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 1 :|: z = 2, z'' >= 0, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' >= 0, z' >= 0, z'' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', z'' - 1) + s5 :|: s5 >= 0, s5 <= 1 + (z'' - 1), z = 2, z'' - 1 >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', z'' - 1) + 1 :|: z = 2, z' >= 0, z'' - 1 >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(2, 0, z'') + s9 :|: s9 >= 0, s9 <= 1 + (z' - 1), z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, 0, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(2, z' - 1, z'') + s8 :|: s8 >= 0, s8 <= 1 + (z' - 1), z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, z' - 1, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(1, 0, z'') + s7 :|: s7 >= 0, s7 <= 0, z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(1, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, 0, z'') + s10 :|: s10 >= 0, s10 <= 0, z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, 0, z'') + s12 :|: s12 >= 0, s12 <= z', z'' >= 0, z = 1, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 1 :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' >= 0, z' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, z' - 1, z'') + s11 :|: s11 >= 0, s11 <= 1 + (z' - 1), z'' >= 0, z = 1, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, z' - 1, z'') + 1 :|: z'' >= 0, z' - 1 >= 0, z = 1, 1 + (z' - 1) = 1 + z0, z0 >= 0 GR(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0 GR(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 GR(z, z') -{ 2 + z' }-> 1 + s13 :|: s13 >= 0, s13 <= z - 1, z' - 1 >= 0, z - 1 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond1(z, z', z'') -{ 0 }-> s15 :|: s15 >= 0, s15 <= 0, z = 2, z'' = 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> s16 :|: s16 >= 0, s16 <= 0, z = 2, z'' - 1 >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> s17 :|: s17 >= 0, s17 <= 0, z = 2, z'' >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 cond2(z, z', z'') -{ 0 }-> s18 :|: s18 >= 0, s18 <= 0, z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> s19 :|: s19 >= 0, s19 <= 0, z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> s20 :|: s20 >= 0, s20 <= 0, z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> s21 :|: s21 >= 0, s21 <= 0, z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> s22 :|: s22 >= 0, s22 <= 0, z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> s23 :|: s23 >= 0, s23 <= 0, z = 2, z'' >= 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> s24 :|: s24 >= 0, s24 <= 0, z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> s25 :|: s25 >= 0, s25 <= 0, z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> s26 :|: s26 >= 0, s26 <= 0, z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> s27 :|: s27 >= 0, s27 <= 0, z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> s28 :|: s28 >= 0, s28 <= 0, z'' >= 0, z = 1, z' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> s29 :|: s29 >= 0, s29 <= 0, z'' >= 0, z = 1, z' >= 0 cond2(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 gr(z, z') -{ 0 }-> s14 :|: s14 >= 0, s14 <= 2, z' - 1 >= 0, z - 1 >= 0 gr(z, z') -{ 0 }-> 2 :|: z - 1 >= 0, z' = 0 gr(z, z') -{ 0 }-> 1 :|: z' >= 0, z = 0 gr(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 p(z) -{ 0 }-> 0 :|: z = 0 p(z) -{ 0 }-> 0 :|: z >= 0 p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0 Function symbols to be analyzed: {COND2,COND1} Previous analysis results are: P: runtime: O(1) [1], size: O(1) [1] GR: runtime: O(n^1) [2 + z'], size: O(n^1) [z] gr: runtime: O(1) [0], size: O(1) [2] cond2: runtime: O(1) [0], size: O(1) [0] cond1: runtime: O(1) [0], size: O(1) [0] p: runtime: O(1) [0], size: O(n^1) [z] COND2: runtime: ?, size: O(1) [0] COND1: runtime: ?, size: O(n^1) [1 + z''] ---------------------------------------- (53) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using KoAT for: COND2 after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: 73*z + 219*z' + 73*z'' Computed RUNTIME bound using CoFloCo for: COND1 after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: 149 + 219*z' + 73*z'' ---------------------------------------- (54) Obligation: Complexity RNTS consisting of the following rules: COND1(z, z', z'') -{ 3 }-> 1 + COND2(2, z', 1 + (z'' - 1)) + s' :|: s' >= 0, s' <= 1 + (z'' - 1), z = 2, z'' - 1 >= 0, z' >= 0 COND1(z, z', z'') -{ 3 }-> 1 + COND2(1, z', 0) + s :|: s >= 0, s <= 0, z = 2, z'' = 0, z' >= 0 COND1(z, z', z'') -{ 3 }-> 1 + COND2(0, z', z'') + s'' :|: s'' >= 0, s'' <= z'', z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(2, z', 0) + s3 :|: s3 >= 0, s3 <= 1 + (z'' - 1), z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', 0) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(2, z', z'' - 1) + s2 :|: s2 >= 0, s2 <= 1 + (z'' - 1), z = 2, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(2, z', z'' - 1) + 1 :|: z = 2, z'' - 1 >= 0, z' >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(1, z', 0) + s1 :|: s1 >= 0, s1 <= 0, z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(1, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', 0) + s4 :|: s4 >= 0, s4 <= 0, z = 2, z'' = 0, z' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', 0) + s6 :|: s6 >= 0, s6 <= z'', z = 2, z'' >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 1 :|: z = 2, z'' >= 0, z' >= 0, z'' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' = 0, z' >= 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', 0) + 0 :|: z = 2, z'' >= 0, z' >= 0, z'' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND2(0, z', z'' - 1) + s5 :|: s5 >= 0, s5 <= 1 + (z'' - 1), z = 2, z'' - 1 >= 0, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND2(0, z', z'' - 1) + 1 :|: z = 2, z' >= 0, z'' - 1 >= 0, 1 + (z'' - 1) = 1 + z0', z0' >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(2, 0, z'') + s9 :|: s9 >= 0, s9 <= 1 + (z' - 1), z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, 0, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(2, z' - 1, z'') + s8 :|: s8 >= 0, s8 <= 1 + (z' - 1), z' - 1 >= 0, z'' >= 0, z = 1 COND2(z, z', z'') -{ 2 }-> 1 + COND1(2, z' - 1, z'') + 1 :|: z'' >= 0, z = 1, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(1, 0, z'') + s7 :|: s7 >= 0, s7 <= 0, z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(1, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, 0, z'') + s10 :|: s10 >= 0, s10 <= 0, z'' >= 0, z = 1, z' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, 0, z'') + s12 :|: s12 >= 0, s12 <= z', z'' >= 0, z = 1, z' >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 1 :|: z'' >= 0, z = 1, z' >= 0, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' = 0, 0 = 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, 0, z'') + 0 :|: z'' >= 0, z = 1, z' >= 0, z' = 0 COND2(z, z', z'') -{ 3 }-> 1 + COND1(0, z' - 1, z'') + s11 :|: s11 >= 0, s11 <= 1 + (z' - 1), z'' >= 0, z = 1, z' - 1 >= 0 COND2(z, z', z'') -{ 2 }-> 1 + COND1(0, z' - 1, z'') + 1 :|: z'' >= 0, z' - 1 >= 0, z = 1, 1 + (z' - 1) = 1 + z0, z0 >= 0 GR(z, z') -{ 1 }-> 1 :|: z - 1 >= 0, z' = 0 GR(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 GR(z, z') -{ 2 + z' }-> 1 + s13 :|: s13 >= 0, s13 <= z - 1, z' - 1 >= 0, z - 1 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond1(z, z', z'') -{ 0 }-> s15 :|: s15 >= 0, s15 <= 0, z = 2, z'' = 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> s16 :|: s16 >= 0, s16 <= 0, z = 2, z'' - 1 >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> s17 :|: s17 >= 0, s17 <= 0, z = 2, z'' >= 0, z' >= 0 cond1(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 cond2(z, z', z'') -{ 0 }-> s18 :|: s18 >= 0, s18 <= 0, z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> s19 :|: s19 >= 0, s19 <= 0, z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> s20 :|: s20 >= 0, s20 <= 0, z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> s21 :|: s21 >= 0, s21 <= 0, z = 2, z'' = 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> s22 :|: s22 >= 0, s22 <= 0, z = 2, z' >= 0, z'' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> s23 :|: s23 >= 0, s23 <= 0, z = 2, z'' >= 0, z' >= 0 cond2(z, z', z'') -{ 0 }-> s24 :|: s24 >= 0, s24 <= 0, z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> s25 :|: s25 >= 0, s25 <= 0, z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> s26 :|: s26 >= 0, s26 <= 0, z' - 1 >= 0, z'' >= 0, z = 1 cond2(z, z', z'') -{ 0 }-> s27 :|: s27 >= 0, s27 <= 0, z'' >= 0, z = 1, z' = 0 cond2(z, z', z'') -{ 0 }-> s28 :|: s28 >= 0, s28 <= 0, z'' >= 0, z = 1, z' - 1 >= 0 cond2(z, z', z'') -{ 0 }-> s29 :|: s29 >= 0, s29 <= 0, z'' >= 0, z = 1, z' >= 0 cond2(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 gr(z, z') -{ 0 }-> s14 :|: s14 >= 0, s14 <= 2, z' - 1 >= 0, z - 1 >= 0 gr(z, z') -{ 0 }-> 2 :|: z - 1 >= 0, z' = 0 gr(z, z') -{ 0 }-> 1 :|: z' >= 0, z = 0 gr(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 p(z) -{ 0 }-> 0 :|: z = 0 p(z) -{ 0 }-> 0 :|: z >= 0 p(z) -{ 0 }-> z - 1 :|: z - 1 >= 0 Function symbols to be analyzed: Previous analysis results are: P: runtime: O(1) [1], size: O(1) [1] GR: runtime: O(n^1) [2 + z'], size: O(n^1) [z] gr: runtime: O(1) [0], size: O(1) [2] cond2: runtime: O(1) [0], size: O(1) [0] cond1: runtime: O(1) [0], size: O(1) [0] p: runtime: O(1) [0], size: O(n^1) [z] COND2: runtime: O(n^1) [73*z + 219*z' + 73*z''], size: O(1) [0] COND1: runtime: O(n^1) [149 + 219*z' + 73*z''], size: O(n^1) [1 + z''] ---------------------------------------- (55) FinalProof (FINISHED) Computed overall runtime complexity ---------------------------------------- (56) BOUNDS(1, n^1) ---------------------------------------- (57) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (58) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: COND1(true, z0, z1) -> c(COND2(gr(z1, 0), z0, z1), GR(z1, 0)) COND2(true, z0, z1) -> c1(COND2(gr(z1, 0), z0, p(z1)), GR(z1, 0)) COND2(true, z0, z1) -> c2(COND2(gr(z1, 0), z0, p(z1)), P(z1)) COND2(false, z0, z1) -> c3(COND1(gr(z0, 0), p(z0), z1), GR(z0, 0)) COND2(false, z0, z1) -> c4(COND1(gr(z0, 0), p(z0), z1), P(z0)) GR(0, z0) -> c5 GR(s(z0), 0) -> c6 GR(s(z0), s(z1)) -> c7(GR(z0, z1)) P(0) -> c8 P(s(z0)) -> c9 The (relative) TRS S consists of the following rules: cond1(true, z0, z1) -> cond2(gr(z1, 0), z0, z1) cond2(true, z0, z1) -> cond2(gr(z1, 0), z0, p(z1)) cond2(false, z0, z1) -> cond1(gr(z0, 0), p(z0), z1) gr(0, z0) -> false gr(s(z0), 0) -> true gr(s(z0), s(z1)) -> gr(z0, z1) p(0) -> 0 p(s(z0)) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (59) DecreasingLoopProof (LOWER BOUND(ID)) The following loop(s) give(s) rise to the lower bound Omega(n^1): The rewrite sequence GR(s(z0), s(z1)) ->^+ c7(GR(z0, z1)) gives rise to a decreasing loop by considering the right hand sides subterm at position [0]. The pumping substitution is [z0 / s(z0), z1 / s(z1)]. The result substitution is [ ]. ---------------------------------------- (60) Complex Obligation (BEST) ---------------------------------------- (61) Obligation: Proved the lower bound n^1 for the following obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: COND1(true, z0, z1) -> c(COND2(gr(z1, 0), z0, z1), GR(z1, 0)) COND2(true, z0, z1) -> c1(COND2(gr(z1, 0), z0, p(z1)), GR(z1, 0)) COND2(true, z0, z1) -> c2(COND2(gr(z1, 0), z0, p(z1)), P(z1)) COND2(false, z0, z1) -> c3(COND1(gr(z0, 0), p(z0), z1), GR(z0, 0)) COND2(false, z0, z1) -> c4(COND1(gr(z0, 0), p(z0), z1), P(z0)) GR(0, z0) -> c5 GR(s(z0), 0) -> c6 GR(s(z0), s(z1)) -> c7(GR(z0, z1)) P(0) -> c8 P(s(z0)) -> c9 The (relative) TRS S consists of the following rules: cond1(true, z0, z1) -> cond2(gr(z1, 0), z0, z1) cond2(true, z0, z1) -> cond2(gr(z1, 0), z0, p(z1)) cond2(false, z0, z1) -> cond1(gr(z0, 0), p(z0), z1) gr(0, z0) -> false gr(s(z0), 0) -> true gr(s(z0), s(z1)) -> gr(z0, z1) p(0) -> 0 p(s(z0)) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (62) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (63) BOUNDS(n^1, INF) ---------------------------------------- (64) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: COND1(true, z0, z1) -> c(COND2(gr(z1, 0), z0, z1), GR(z1, 0)) COND2(true, z0, z1) -> c1(COND2(gr(z1, 0), z0, p(z1)), GR(z1, 0)) COND2(true, z0, z1) -> c2(COND2(gr(z1, 0), z0, p(z1)), P(z1)) COND2(false, z0, z1) -> c3(COND1(gr(z0, 0), p(z0), z1), GR(z0, 0)) COND2(false, z0, z1) -> c4(COND1(gr(z0, 0), p(z0), z1), P(z0)) GR(0, z0) -> c5 GR(s(z0), 0) -> c6 GR(s(z0), s(z1)) -> c7(GR(z0, z1)) P(0) -> c8 P(s(z0)) -> c9 The (relative) TRS S consists of the following rules: cond1(true, z0, z1) -> cond2(gr(z1, 0), z0, z1) cond2(true, z0, z1) -> cond2(gr(z1, 0), z0, p(z1)) cond2(false, z0, z1) -> cond1(gr(z0, 0), p(z0), z1) gr(0, z0) -> false gr(s(z0), 0) -> true gr(s(z0), s(z1)) -> gr(z0, z1) p(0) -> 0 p(s(z0)) -> z0 Rewrite Strategy: INNERMOST