WORST_CASE(Omega(n^1),O(n^2)) proof of /export/starexec/sandbox2/benchmark/theBenchmark.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 464 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), 0 ms] (12) CpxRNTS (13) InliningProof [UPPER BOUND(ID), 405 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), 0 ms] (20) CpxRNTS (21) IntTrsBoundProof [UPPER BOUND(ID), 160 ms] (22) CpxRNTS (23) IntTrsBoundProof [UPPER BOUND(ID), 55 ms] (24) CpxRNTS (25) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (26) CpxRNTS (27) IntTrsBoundProof [UPPER BOUND(ID), 273 ms] (28) CpxRNTS (29) IntTrsBoundProof [UPPER BOUND(ID), 96 ms] (30) CpxRNTS (31) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (32) CpxRNTS (33) IntTrsBoundProof [UPPER BOUND(ID), 301 ms] (34) CpxRNTS (35) IntTrsBoundProof [UPPER BOUND(ID), 6 ms] (36) CpxRNTS (37) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (38) CpxRNTS (39) IntTrsBoundProof [UPPER BOUND(ID), 129 ms] (40) CpxRNTS (41) IntTrsBoundProof [UPPER BOUND(ID), 52 ms] (42) CpxRNTS (43) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (44) CpxRNTS (45) IntTrsBoundProof [UPPER BOUND(ID), 2187 ms] (46) CpxRNTS (47) IntTrsBoundProof [UPPER BOUND(ID), 1339 ms] (48) CpxRNTS (49) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (50) CpxRNTS (51) IntTrsBoundProof [UPPER BOUND(ID), 1087 ms] (52) CpxRNTS (53) IntTrsBoundProof [UPPER BOUND(ID), 408 ms] (54) CpxRNTS (55) FinalProof [FINISHED, 0 ms] (56) BOUNDS(1, n^2) (57) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (58) CpxRelTRS (59) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (60) typed CpxTrs (61) OrderProof [LOWER BOUND(ID), 0 ms] (62) typed CpxTrs (63) RewriteLemmaProof [LOWER BOUND(ID), 269 ms] (64) typed CpxTrs (65) RewriteLemmaProof [LOWER BOUND(ID), 52 ms] (66) BEST (67) proven lower bound (68) LowerBoundPropagationProof [FINISHED, 0 ms] (69) BOUNDS(n^1, INF) (70) typed CpxTrs ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2). The TRS R consists of the following rules: COND(true, z0) -> c(COND(odd(z0), p(z0)), ODD(z0)) COND(true, z0) -> c1(COND(odd(z0), p(z0)), P(z0)) ODD(0) -> c2 ODD(s(0)) -> c3 ODD(s(s(z0))) -> c4(ODD(z0)) P(0) -> c5 P(s(z0)) -> c6 The (relative) TRS S consists of the following rules: cond(true, z0) -> cond(odd(z0), p(z0)) odd(0) -> false odd(s(0)) -> true odd(s(s(z0))) -> odd(z0) p(0) -> 0 p(s(z0)) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID)) proved innermost termination of relative rules ---------------------------------------- (2) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2). The TRS R consists of the following rules: COND(true, z0) -> c(COND(odd(z0), p(z0)), ODD(z0)) COND(true, z0) -> c1(COND(odd(z0), p(z0)), P(z0)) ODD(0) -> c2 ODD(s(0)) -> c3 ODD(s(s(z0))) -> c4(ODD(z0)) P(0) -> c5 P(s(z0)) -> c6 The (relative) TRS S consists of the following rules: cond(true, z0) -> cond(odd(z0), p(z0)) odd(0) -> false odd(s(0)) -> true odd(s(s(z0))) -> odd(z0) p(0) -> 0 p(s(z0)) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (3) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID)) Transformed relative TRS to weighted TRS ---------------------------------------- (4) Obligation: The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^2). The TRS R consists of the following rules: COND(true, z0) -> c(COND(odd(z0), p(z0)), ODD(z0)) [1] COND(true, z0) -> c1(COND(odd(z0), p(z0)), P(z0)) [1] ODD(0) -> c2 [1] ODD(s(0)) -> c3 [1] ODD(s(s(z0))) -> c4(ODD(z0)) [1] P(0) -> c5 [1] P(s(z0)) -> c6 [1] cond(true, z0) -> cond(odd(z0), p(z0)) [0] odd(0) -> false [0] odd(s(0)) -> true [0] odd(s(s(z0))) -> odd(z0) [0] p(0) -> 0 [0] p(s(z0)) -> z0 [0] Rewrite Strategy: INNERMOST ---------------------------------------- (5) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (6) Obligation: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: COND(true, z0) -> c(COND(odd(z0), p(z0)), ODD(z0)) [1] COND(true, z0) -> c1(COND(odd(z0), p(z0)), P(z0)) [1] ODD(0) -> c2 [1] ODD(s(0)) -> c3 [1] ODD(s(s(z0))) -> c4(ODD(z0)) [1] P(0) -> c5 [1] P(s(z0)) -> c6 [1] cond(true, z0) -> cond(odd(z0), p(z0)) [0] odd(0) -> false [0] odd(s(0)) -> true [0] odd(s(s(z0))) -> odd(z0) [0] p(0) -> 0 [0] p(s(z0)) -> z0 [0] The TRS has the following type information: COND :: true:false -> 0:s -> c:c1 true :: true:false c :: c:c1 -> c2:c3:c4 -> c:c1 odd :: 0:s -> true:false p :: 0:s -> 0:s ODD :: 0:s -> c2:c3:c4 c1 :: c:c1 -> c5:c6 -> c:c1 P :: 0:s -> c5:c6 0 :: 0:s c2 :: c2:c3:c4 s :: 0:s -> 0:s c3 :: c2:c3:c4 c4 :: c2:c3:c4 -> c2:c3:c4 c5 :: c5:c6 c6 :: c5:c6 cond :: true:false -> 0:s -> cond false :: true:false 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: COND_2 ODD_1 P_1 (c) The following functions are completely defined: cond_2 odd_1 p_1 Due to the following rules being added: cond(v0, v1) -> const1 [0] odd(v0) -> null_odd [0] p(v0) -> 0 [0] And the following fresh constants: const1, null_odd, const ---------------------------------------- (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: COND(true, z0) -> c(COND(odd(z0), p(z0)), ODD(z0)) [1] COND(true, z0) -> c1(COND(odd(z0), p(z0)), P(z0)) [1] ODD(0) -> c2 [1] ODD(s(0)) -> c3 [1] ODD(s(s(z0))) -> c4(ODD(z0)) [1] P(0) -> c5 [1] P(s(z0)) -> c6 [1] cond(true, z0) -> cond(odd(z0), p(z0)) [0] odd(0) -> false [0] odd(s(0)) -> true [0] odd(s(s(z0))) -> odd(z0) [0] p(0) -> 0 [0] p(s(z0)) -> z0 [0] cond(v0, v1) -> const1 [0] odd(v0) -> null_odd [0] p(v0) -> 0 [0] The TRS has the following type information: COND :: true:false:null_odd -> 0:s -> c:c1 true :: true:false:null_odd c :: c:c1 -> c2:c3:c4 -> c:c1 odd :: 0:s -> true:false:null_odd p :: 0:s -> 0:s ODD :: 0:s -> c2:c3:c4 c1 :: c:c1 -> c5:c6 -> c:c1 P :: 0:s -> c5:c6 0 :: 0:s c2 :: c2:c3:c4 s :: 0:s -> 0:s c3 :: c2:c3:c4 c4 :: c2:c3:c4 -> c2:c3:c4 c5 :: c5:c6 c6 :: c5:c6 cond :: true:false:null_odd -> 0:s -> const1 false :: true:false:null_odd const1 :: const1 null_odd :: true:false:null_odd const :: c:c1 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: COND(true, 0) -> c(COND(false, 0), ODD(0)) [1] COND(true, 0) -> c(COND(false, 0), ODD(0)) [1] COND(true, s(0)) -> c(COND(true, 0), ODD(s(0))) [1] COND(true, s(0)) -> c(COND(true, 0), ODD(s(0))) [1] COND(true, s(s(z0'))) -> c(COND(odd(z0'), s(z0')), ODD(s(s(z0')))) [1] COND(true, s(s(z0'))) -> c(COND(odd(z0'), 0), ODD(s(s(z0')))) [1] COND(true, 0) -> c(COND(null_odd, 0), ODD(0)) [1] COND(true, s(z0'')) -> c(COND(null_odd, z0''), ODD(s(z0''))) [1] COND(true, z0) -> c(COND(null_odd, 0), ODD(z0)) [1] COND(true, 0) -> c1(COND(false, 0), P(0)) [1] COND(true, 0) -> c1(COND(false, 0), P(0)) [1] COND(true, s(0)) -> c1(COND(true, 0), P(s(0))) [1] COND(true, s(0)) -> c1(COND(true, 0), P(s(0))) [1] COND(true, s(s(z01))) -> c1(COND(odd(z01), s(z01)), P(s(s(z01)))) [1] COND(true, s(s(z01))) -> c1(COND(odd(z01), 0), P(s(s(z01)))) [1] COND(true, 0) -> c1(COND(null_odd, 0), P(0)) [1] COND(true, s(z02)) -> c1(COND(null_odd, z02), P(s(z02))) [1] COND(true, z0) -> c1(COND(null_odd, 0), P(z0)) [1] ODD(0) -> c2 [1] ODD(s(0)) -> c3 [1] ODD(s(s(z0))) -> c4(ODD(z0)) [1] P(0) -> c5 [1] P(s(z0)) -> c6 [1] cond(true, 0) -> cond(false, 0) [0] cond(true, 0) -> cond(false, 0) [0] cond(true, s(0)) -> cond(true, 0) [0] cond(true, s(0)) -> cond(true, 0) [0] cond(true, s(s(z03))) -> cond(odd(z03), s(z03)) [0] cond(true, s(s(z03))) -> cond(odd(z03), 0) [0] cond(true, 0) -> cond(null_odd, 0) [0] cond(true, s(z04)) -> cond(null_odd, z04) [0] cond(true, z0) -> cond(null_odd, 0) [0] odd(0) -> false [0] odd(s(0)) -> true [0] odd(s(s(z0))) -> odd(z0) [0] p(0) -> 0 [0] p(s(z0)) -> z0 [0] cond(v0, v1) -> const1 [0] odd(v0) -> null_odd [0] p(v0) -> 0 [0] The TRS has the following type information: COND :: true:false:null_odd -> 0:s -> c:c1 true :: true:false:null_odd c :: c:c1 -> c2:c3:c4 -> c:c1 odd :: 0:s -> true:false:null_odd p :: 0:s -> 0:s ODD :: 0:s -> c2:c3:c4 c1 :: c:c1 -> c5:c6 -> c:c1 P :: 0:s -> c5:c6 0 :: 0:s c2 :: c2:c3:c4 s :: 0:s -> 0:s c3 :: c2:c3:c4 c4 :: c2:c3:c4 -> c2:c3:c4 c5 :: c5:c6 c6 :: c5:c6 cond :: true:false:null_odd -> 0:s -> const1 false :: true:false:null_odd const1 :: const1 null_odd :: true:false:null_odd const :: c:c1 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 c2 => 0 c3 => 1 c5 => 0 c6 => 1 false => 1 const1 => 0 null_odd => 0 const => 0 ---------------------------------------- (12) Obligation: Complexity RNTS consisting of the following rules: COND(z, z') -{ 1 }-> 1 + COND(odd(z0'), 0) + ODD(1 + (1 + z0')) :|: z = 2, z' = 1 + (1 + z0'), z0' >= 0 COND(z, z') -{ 1 }-> 1 + COND(odd(z0'), 1 + z0') + ODD(1 + (1 + z0')) :|: z = 2, z' = 1 + (1 + z0'), z0' >= 0 COND(z, z') -{ 1 }-> 1 + COND(odd(z01), 0) + P(1 + (1 + z01)) :|: z = 2, z01 >= 0, z' = 1 + (1 + z01) COND(z, z') -{ 1 }-> 1 + COND(odd(z01), 1 + z01) + P(1 + (1 + z01)) :|: z = 2, z01 >= 0, z' = 1 + (1 + z01) COND(z, z') -{ 1 }-> 1 + COND(2, 0) + P(1 + 0) :|: z = 2, z' = 1 + 0 COND(z, z') -{ 1 }-> 1 + COND(2, 0) + ODD(1 + 0) :|: z = 2, z' = 1 + 0 COND(z, z') -{ 1 }-> 1 + COND(1, 0) + P(0) :|: z = 2, z' = 0 COND(z, z') -{ 1 }-> 1 + COND(1, 0) + ODD(0) :|: z = 2, z' = 0 COND(z, z') -{ 1 }-> 1 + COND(0, z0'') + ODD(1 + z0'') :|: z = 2, z' = 1 + z0'', z0'' >= 0 COND(z, z') -{ 1 }-> 1 + COND(0, z02) + P(1 + z02) :|: z = 2, z02 >= 0, z' = 1 + z02 COND(z, z') -{ 1 }-> 1 + COND(0, 0) + P(z0) :|: z = 2, z0 >= 0, z' = z0 COND(z, z') -{ 1 }-> 1 + COND(0, 0) + P(0) :|: z = 2, z' = 0 COND(z, z') -{ 1 }-> 1 + COND(0, 0) + ODD(z0) :|: z = 2, z0 >= 0, z' = z0 COND(z, z') -{ 1 }-> 1 + COND(0, 0) + ODD(0) :|: z = 2, z' = 0 ODD(z) -{ 1 }-> 1 :|: z = 1 + 0 ODD(z) -{ 1 }-> 0 :|: z = 0 ODD(z) -{ 1 }-> 1 + ODD(z0) :|: z0 >= 0, z = 1 + (1 + z0) P(z) -{ 1 }-> 1 :|: z = 1 + z0, z0 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond(z, z') -{ 0 }-> cond(odd(z03), 0) :|: z = 2, z' = 1 + (1 + z03), z03 >= 0 cond(z, z') -{ 0 }-> cond(odd(z03), 1 + z03) :|: z = 2, z' = 1 + (1 + z03), z03 >= 0 cond(z, z') -{ 0 }-> cond(2, 0) :|: z = 2, z' = 1 + 0 cond(z, z') -{ 0 }-> cond(1, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, z04) :|: z = 2, z04 >= 0, z' = 1 + z04 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z0 >= 0, z' = z0 cond(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 odd(z) -{ 0 }-> odd(z0) :|: z0 >= 0, z = 1 + (1 + z0) odd(z) -{ 0 }-> 2 :|: z = 1 + 0 odd(z) -{ 0 }-> 1 :|: z = 0 odd(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 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: COND(z, z') -{ 1 }-> 1 + COND(odd(z0'), 0) + ODD(1 + (1 + z0')) :|: z = 2, z' = 1 + (1 + z0'), z0' >= 0 COND(z, z') -{ 1 }-> 1 + COND(odd(z0'), 1 + z0') + ODD(1 + (1 + z0')) :|: z = 2, z' = 1 + (1 + z0'), z0' >= 0 COND(z, z') -{ 2 }-> 1 + COND(odd(z01), 0) + 1 :|: z = 2, z01 >= 0, z' = 1 + (1 + z01), 1 + (1 + z01) = 1 + z0, z0 >= 0 COND(z, z') -{ 2 }-> 1 + COND(odd(z01), 1 + z01) + 1 :|: z = 2, z01 >= 0, z' = 1 + (1 + z01), 1 + (1 + z01) = 1 + z0, z0 >= 0 COND(z, z') -{ 1 }-> 1 + COND(2, 0) + ODD(1 + 0) :|: z = 2, z' = 1 + 0 COND(z, z') -{ 2 }-> 1 + COND(2, 0) + 1 :|: z = 2, z' = 1 + 0, 1 + 0 = 1 + z0, z0 >= 0 COND(z, z') -{ 1 }-> 1 + COND(1, 0) + ODD(0) :|: z = 2, z' = 0 COND(z, z') -{ 2 }-> 1 + COND(1, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 1 }-> 1 + COND(0, z0'') + ODD(1 + z0'') :|: z = 2, z' = 1 + z0'', z0'' >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, z02) + 1 :|: z = 2, z02 >= 0, z' = 1 + z02, 1 + z02 = 1 + z0, z0 >= 0 COND(z, z') -{ 1 }-> 1 + COND(0, 0) + ODD(z0) :|: z = 2, z0 >= 0, z' = z0 COND(z, z') -{ 1 }-> 1 + COND(0, 0) + ODD(0) :|: z = 2, z' = 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 1 :|: z = 2, z0 >= 0, z' = z0, z0 = 1 + z0', z0' >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z0 >= 0, z' = z0, z0 = 0 ODD(z) -{ 1 }-> 1 :|: z = 1 + 0 ODD(z) -{ 1 }-> 0 :|: z = 0 ODD(z) -{ 1 }-> 1 + ODD(z0) :|: z0 >= 0, z = 1 + (1 + z0) P(z) -{ 1 }-> 1 :|: z = 1 + z0, z0 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond(z, z') -{ 0 }-> cond(odd(z03), 0) :|: z = 2, z' = 1 + (1 + z03), z03 >= 0 cond(z, z') -{ 0 }-> cond(odd(z03), 1 + z03) :|: z = 2, z' = 1 + (1 + z03), z03 >= 0 cond(z, z') -{ 0 }-> cond(2, 0) :|: z = 2, z' = 1 + 0 cond(z, z') -{ 0 }-> cond(1, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, z04) :|: z = 2, z04 >= 0, z' = 1 + z04 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z0 >= 0, z' = z0 cond(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 odd(z) -{ 0 }-> odd(z0) :|: z0 >= 0, z = 1 + (1 + z0) odd(z) -{ 0 }-> 2 :|: z = 1 + 0 odd(z) -{ 0 }-> 1 :|: z = 0 odd(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 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: COND(z, z') -{ 1 }-> 1 + COND(odd(z' - 2), 0) + ODD(1 + (1 + (z' - 2))) :|: z = 2, z' - 2 >= 0 COND(z, z') -{ 2 }-> 1 + COND(odd(z' - 2), 0) + 1 :|: z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 1 }-> 1 + COND(odd(z' - 2), 1 + (z' - 2)) + ODD(1 + (1 + (z' - 2))) :|: z = 2, z' - 2 >= 0 COND(z, z') -{ 2 }-> 1 + COND(odd(z' - 2), 1 + (z' - 2)) + 1 :|: z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 1 }-> 1 + COND(2, 0) + ODD(1 + 0) :|: z = 2, z' = 1 + 0 COND(z, z') -{ 2 }-> 1 + COND(2, 0) + 1 :|: z = 2, z' = 1 + 0, 1 + 0 = 1 + z0, z0 >= 0 COND(z, z') -{ 1 }-> 1 + COND(1, 0) + ODD(0) :|: z = 2, z' = 0 COND(z, z') -{ 2 }-> 1 + COND(1, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 1 }-> 1 + COND(0, 0) + ODD(z') :|: z = 2, z' >= 0 COND(z, z') -{ 1 }-> 1 + COND(0, 0) + ODD(0) :|: z = 2, z' = 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 1 :|: z = 2, z' >= 0, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' >= 0, z' = 0 COND(z, z') -{ 1 }-> 1 + COND(0, z' - 1) + ODD(1 + (z' - 1)) :|: z = 2, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, z' - 1) + 1 :|: z = 2, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 ODD(z) -{ 1 }-> 1 :|: z = 1 + 0 ODD(z) -{ 1 }-> 0 :|: z = 0 ODD(z) -{ 1 }-> 1 + ODD(z - 2) :|: z - 2 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond(z, z') -{ 0 }-> cond(odd(z' - 2), 0) :|: z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(odd(z' - 2), 1 + (z' - 2)) :|: z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(2, 0) :|: z = 2, z' = 1 + 0 cond(z, z') -{ 0 }-> cond(1, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' >= 0 cond(z, z') -{ 0 }-> cond(0, z' - 1) :|: z = 2, z' - 1 >= 0 cond(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 odd(z) -{ 0 }-> odd(z - 2) :|: z - 2 >= 0 odd(z) -{ 0 }-> 2 :|: z = 1 + 0 odd(z) -{ 0 }-> 1 :|: z = 0 odd(z) -{ 0 }-> 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 } { ODD } { odd } { p } { COND } { cond } ---------------------------------------- (18) Obligation: Complexity RNTS consisting of the following rules: COND(z, z') -{ 1 }-> 1 + COND(odd(z' - 2), 0) + ODD(1 + (1 + (z' - 2))) :|: z = 2, z' - 2 >= 0 COND(z, z') -{ 2 }-> 1 + COND(odd(z' - 2), 0) + 1 :|: z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 1 }-> 1 + COND(odd(z' - 2), 1 + (z' - 2)) + ODD(1 + (1 + (z' - 2))) :|: z = 2, z' - 2 >= 0 COND(z, z') -{ 2 }-> 1 + COND(odd(z' - 2), 1 + (z' - 2)) + 1 :|: z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 1 }-> 1 + COND(2, 0) + ODD(1 + 0) :|: z = 2, z' = 1 + 0 COND(z, z') -{ 2 }-> 1 + COND(2, 0) + 1 :|: z = 2, z' = 1 + 0, 1 + 0 = 1 + z0, z0 >= 0 COND(z, z') -{ 1 }-> 1 + COND(1, 0) + ODD(0) :|: z = 2, z' = 0 COND(z, z') -{ 2 }-> 1 + COND(1, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 1 }-> 1 + COND(0, 0) + ODD(z') :|: z = 2, z' >= 0 COND(z, z') -{ 1 }-> 1 + COND(0, 0) + ODD(0) :|: z = 2, z' = 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 1 :|: z = 2, z' >= 0, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' >= 0, z' = 0 COND(z, z') -{ 1 }-> 1 + COND(0, z' - 1) + ODD(1 + (z' - 1)) :|: z = 2, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, z' - 1) + 1 :|: z = 2, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 ODD(z) -{ 1 }-> 1 :|: z = 1 + 0 ODD(z) -{ 1 }-> 0 :|: z = 0 ODD(z) -{ 1 }-> 1 + ODD(z - 2) :|: z - 2 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond(z, z') -{ 0 }-> cond(odd(z' - 2), 0) :|: z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(odd(z' - 2), 1 + (z' - 2)) :|: z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(2, 0) :|: z = 2, z' = 1 + 0 cond(z, z') -{ 0 }-> cond(1, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' >= 0 cond(z, z') -{ 0 }-> cond(0, z' - 1) :|: z = 2, z' - 1 >= 0 cond(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 odd(z) -{ 0 }-> odd(z - 2) :|: z - 2 >= 0 odd(z) -{ 0 }-> 2 :|: z = 1 + 0 odd(z) -{ 0 }-> 1 :|: z = 0 odd(z) -{ 0 }-> 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}, {ODD}, {odd}, {p}, {COND}, {cond} ---------------------------------------- (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: COND(z, z') -{ 1 }-> 1 + COND(odd(z' - 2), 0) + ODD(1 + (1 + (z' - 2))) :|: z = 2, z' - 2 >= 0 COND(z, z') -{ 2 }-> 1 + COND(odd(z' - 2), 0) + 1 :|: z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 1 }-> 1 + COND(odd(z' - 2), 1 + (z' - 2)) + ODD(1 + (1 + (z' - 2))) :|: z = 2, z' - 2 >= 0 COND(z, z') -{ 2 }-> 1 + COND(odd(z' - 2), 1 + (z' - 2)) + 1 :|: z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 1 }-> 1 + COND(2, 0) + ODD(1 + 0) :|: z = 2, z' = 1 + 0 COND(z, z') -{ 2 }-> 1 + COND(2, 0) + 1 :|: z = 2, z' = 1 + 0, 1 + 0 = 1 + z0, z0 >= 0 COND(z, z') -{ 1 }-> 1 + COND(1, 0) + ODD(0) :|: z = 2, z' = 0 COND(z, z') -{ 2 }-> 1 + COND(1, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 1 }-> 1 + COND(0, 0) + ODD(z') :|: z = 2, z' >= 0 COND(z, z') -{ 1 }-> 1 + COND(0, 0) + ODD(0) :|: z = 2, z' = 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 1 :|: z = 2, z' >= 0, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' >= 0, z' = 0 COND(z, z') -{ 1 }-> 1 + COND(0, z' - 1) + ODD(1 + (z' - 1)) :|: z = 2, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, z' - 1) + 1 :|: z = 2, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 ODD(z) -{ 1 }-> 1 :|: z = 1 + 0 ODD(z) -{ 1 }-> 0 :|: z = 0 ODD(z) -{ 1 }-> 1 + ODD(z - 2) :|: z - 2 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond(z, z') -{ 0 }-> cond(odd(z' - 2), 0) :|: z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(odd(z' - 2), 1 + (z' - 2)) :|: z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(2, 0) :|: z = 2, z' = 1 + 0 cond(z, z') -{ 0 }-> cond(1, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' >= 0 cond(z, z') -{ 0 }-> cond(0, z' - 1) :|: z = 2, z' - 1 >= 0 cond(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 odd(z) -{ 0 }-> odd(z - 2) :|: z - 2 >= 0 odd(z) -{ 0 }-> 2 :|: z = 1 + 0 odd(z) -{ 0 }-> 1 :|: z = 0 odd(z) -{ 0 }-> 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}, {ODD}, {odd}, {p}, {COND}, {cond} ---------------------------------------- (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: COND(z, z') -{ 1 }-> 1 + COND(odd(z' - 2), 0) + ODD(1 + (1 + (z' - 2))) :|: z = 2, z' - 2 >= 0 COND(z, z') -{ 2 }-> 1 + COND(odd(z' - 2), 0) + 1 :|: z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 1 }-> 1 + COND(odd(z' - 2), 1 + (z' - 2)) + ODD(1 + (1 + (z' - 2))) :|: z = 2, z' - 2 >= 0 COND(z, z') -{ 2 }-> 1 + COND(odd(z' - 2), 1 + (z' - 2)) + 1 :|: z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 1 }-> 1 + COND(2, 0) + ODD(1 + 0) :|: z = 2, z' = 1 + 0 COND(z, z') -{ 2 }-> 1 + COND(2, 0) + 1 :|: z = 2, z' = 1 + 0, 1 + 0 = 1 + z0, z0 >= 0 COND(z, z') -{ 1 }-> 1 + COND(1, 0) + ODD(0) :|: z = 2, z' = 0 COND(z, z') -{ 2 }-> 1 + COND(1, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 1 }-> 1 + COND(0, 0) + ODD(z') :|: z = 2, z' >= 0 COND(z, z') -{ 1 }-> 1 + COND(0, 0) + ODD(0) :|: z = 2, z' = 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 1 :|: z = 2, z' >= 0, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' >= 0, z' = 0 COND(z, z') -{ 1 }-> 1 + COND(0, z' - 1) + ODD(1 + (z' - 1)) :|: z = 2, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, z' - 1) + 1 :|: z = 2, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 ODD(z) -{ 1 }-> 1 :|: z = 1 + 0 ODD(z) -{ 1 }-> 0 :|: z = 0 ODD(z) -{ 1 }-> 1 + ODD(z - 2) :|: z - 2 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond(z, z') -{ 0 }-> cond(odd(z' - 2), 0) :|: z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(odd(z' - 2), 1 + (z' - 2)) :|: z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(2, 0) :|: z = 2, z' = 1 + 0 cond(z, z') -{ 0 }-> cond(1, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' >= 0 cond(z, z') -{ 0 }-> cond(0, z' - 1) :|: z = 2, z' - 1 >= 0 cond(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 odd(z) -{ 0 }-> odd(z - 2) :|: z - 2 >= 0 odd(z) -{ 0 }-> 2 :|: z = 1 + 0 odd(z) -{ 0 }-> 1 :|: z = 0 odd(z) -{ 0 }-> 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}, {ODD}, {odd}, {p}, {COND}, {cond} 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: COND(z, z') -{ 1 }-> 1 + COND(odd(z' - 2), 0) + ODD(1 + (1 + (z' - 2))) :|: z = 2, z' - 2 >= 0 COND(z, z') -{ 2 }-> 1 + COND(odd(z' - 2), 0) + 1 :|: z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 1 }-> 1 + COND(odd(z' - 2), 1 + (z' - 2)) + ODD(1 + (1 + (z' - 2))) :|: z = 2, z' - 2 >= 0 COND(z, z') -{ 2 }-> 1 + COND(odd(z' - 2), 1 + (z' - 2)) + 1 :|: z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 1 }-> 1 + COND(2, 0) + ODD(1 + 0) :|: z = 2, z' = 1 + 0 COND(z, z') -{ 2 }-> 1 + COND(2, 0) + 1 :|: z = 2, z' = 1 + 0, 1 + 0 = 1 + z0, z0 >= 0 COND(z, z') -{ 1 }-> 1 + COND(1, 0) + ODD(0) :|: z = 2, z' = 0 COND(z, z') -{ 2 }-> 1 + COND(1, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 1 }-> 1 + COND(0, 0) + ODD(z') :|: z = 2, z' >= 0 COND(z, z') -{ 1 }-> 1 + COND(0, 0) + ODD(0) :|: z = 2, z' = 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 1 :|: z = 2, z' >= 0, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' >= 0, z' = 0 COND(z, z') -{ 1 }-> 1 + COND(0, z' - 1) + ODD(1 + (z' - 1)) :|: z = 2, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, z' - 1) + 1 :|: z = 2, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 ODD(z) -{ 1 }-> 1 :|: z = 1 + 0 ODD(z) -{ 1 }-> 0 :|: z = 0 ODD(z) -{ 1 }-> 1 + ODD(z - 2) :|: z - 2 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond(z, z') -{ 0 }-> cond(odd(z' - 2), 0) :|: z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(odd(z' - 2), 1 + (z' - 2)) :|: z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(2, 0) :|: z = 2, z' = 1 + 0 cond(z, z') -{ 0 }-> cond(1, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' >= 0 cond(z, z') -{ 0 }-> cond(0, z' - 1) :|: z = 2, z' - 1 >= 0 cond(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 odd(z) -{ 0 }-> odd(z - 2) :|: z - 2 >= 0 odd(z) -{ 0 }-> 2 :|: z = 1 + 0 odd(z) -{ 0 }-> 1 :|: z = 0 odd(z) -{ 0 }-> 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: {ODD}, {odd}, {p}, {COND}, {cond} 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: COND(z, z') -{ 1 }-> 1 + COND(odd(z' - 2), 0) + ODD(1 + (1 + (z' - 2))) :|: z = 2, z' - 2 >= 0 COND(z, z') -{ 2 }-> 1 + COND(odd(z' - 2), 0) + 1 :|: z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 1 }-> 1 + COND(odd(z' - 2), 1 + (z' - 2)) + ODD(1 + (1 + (z' - 2))) :|: z = 2, z' - 2 >= 0 COND(z, z') -{ 2 }-> 1 + COND(odd(z' - 2), 1 + (z' - 2)) + 1 :|: z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 1 }-> 1 + COND(2, 0) + ODD(1 + 0) :|: z = 2, z' = 1 + 0 COND(z, z') -{ 2 }-> 1 + COND(2, 0) + 1 :|: z = 2, z' = 1 + 0, 1 + 0 = 1 + z0, z0 >= 0 COND(z, z') -{ 1 }-> 1 + COND(1, 0) + ODD(0) :|: z = 2, z' = 0 COND(z, z') -{ 2 }-> 1 + COND(1, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 1 }-> 1 + COND(0, 0) + ODD(z') :|: z = 2, z' >= 0 COND(z, z') -{ 1 }-> 1 + COND(0, 0) + ODD(0) :|: z = 2, z' = 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 1 :|: z = 2, z' >= 0, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' >= 0, z' = 0 COND(z, z') -{ 1 }-> 1 + COND(0, z' - 1) + ODD(1 + (z' - 1)) :|: z = 2, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, z' - 1) + 1 :|: z = 2, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 ODD(z) -{ 1 }-> 1 :|: z = 1 + 0 ODD(z) -{ 1 }-> 0 :|: z = 0 ODD(z) -{ 1 }-> 1 + ODD(z - 2) :|: z - 2 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond(z, z') -{ 0 }-> cond(odd(z' - 2), 0) :|: z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(odd(z' - 2), 1 + (z' - 2)) :|: z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(2, 0) :|: z = 2, z' = 1 + 0 cond(z, z') -{ 0 }-> cond(1, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' >= 0 cond(z, z') -{ 0 }-> cond(0, z' - 1) :|: z = 2, z' - 1 >= 0 cond(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 odd(z) -{ 0 }-> odd(z - 2) :|: z - 2 >= 0 odd(z) -{ 0 }-> 2 :|: z = 1 + 0 odd(z) -{ 0 }-> 1 :|: z = 0 odd(z) -{ 0 }-> 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: {ODD}, {odd}, {p}, {COND}, {cond} Previous analysis results are: P: runtime: O(1) [1], size: O(1) [1] ---------------------------------------- (27) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using KoAT for: ODD 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: COND(z, z') -{ 1 }-> 1 + COND(odd(z' - 2), 0) + ODD(1 + (1 + (z' - 2))) :|: z = 2, z' - 2 >= 0 COND(z, z') -{ 2 }-> 1 + COND(odd(z' - 2), 0) + 1 :|: z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 1 }-> 1 + COND(odd(z' - 2), 1 + (z' - 2)) + ODD(1 + (1 + (z' - 2))) :|: z = 2, z' - 2 >= 0 COND(z, z') -{ 2 }-> 1 + COND(odd(z' - 2), 1 + (z' - 2)) + 1 :|: z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 1 }-> 1 + COND(2, 0) + ODD(1 + 0) :|: z = 2, z' = 1 + 0 COND(z, z') -{ 2 }-> 1 + COND(2, 0) + 1 :|: z = 2, z' = 1 + 0, 1 + 0 = 1 + z0, z0 >= 0 COND(z, z') -{ 1 }-> 1 + COND(1, 0) + ODD(0) :|: z = 2, z' = 0 COND(z, z') -{ 2 }-> 1 + COND(1, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 1 }-> 1 + COND(0, 0) + ODD(z') :|: z = 2, z' >= 0 COND(z, z') -{ 1 }-> 1 + COND(0, 0) + ODD(0) :|: z = 2, z' = 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 1 :|: z = 2, z' >= 0, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' >= 0, z' = 0 COND(z, z') -{ 1 }-> 1 + COND(0, z' - 1) + ODD(1 + (z' - 1)) :|: z = 2, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, z' - 1) + 1 :|: z = 2, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 ODD(z) -{ 1 }-> 1 :|: z = 1 + 0 ODD(z) -{ 1 }-> 0 :|: z = 0 ODD(z) -{ 1 }-> 1 + ODD(z - 2) :|: z - 2 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond(z, z') -{ 0 }-> cond(odd(z' - 2), 0) :|: z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(odd(z' - 2), 1 + (z' - 2)) :|: z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(2, 0) :|: z = 2, z' = 1 + 0 cond(z, z') -{ 0 }-> cond(1, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' >= 0 cond(z, z') -{ 0 }-> cond(0, z' - 1) :|: z = 2, z' - 1 >= 0 cond(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 odd(z) -{ 0 }-> odd(z - 2) :|: z - 2 >= 0 odd(z) -{ 0 }-> 2 :|: z = 1 + 0 odd(z) -{ 0 }-> 1 :|: z = 0 odd(z) -{ 0 }-> 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: {ODD}, {odd}, {p}, {COND}, {cond} Previous analysis results are: P: runtime: O(1) [1], size: O(1) [1] ODD: runtime: ?, size: O(n^1) [z] ---------------------------------------- (29) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: ODD 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: COND(z, z') -{ 1 }-> 1 + COND(odd(z' - 2), 0) + ODD(1 + (1 + (z' - 2))) :|: z = 2, z' - 2 >= 0 COND(z, z') -{ 2 }-> 1 + COND(odd(z' - 2), 0) + 1 :|: z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 1 }-> 1 + COND(odd(z' - 2), 1 + (z' - 2)) + ODD(1 + (1 + (z' - 2))) :|: z = 2, z' - 2 >= 0 COND(z, z') -{ 2 }-> 1 + COND(odd(z' - 2), 1 + (z' - 2)) + 1 :|: z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 1 }-> 1 + COND(2, 0) + ODD(1 + 0) :|: z = 2, z' = 1 + 0 COND(z, z') -{ 2 }-> 1 + COND(2, 0) + 1 :|: z = 2, z' = 1 + 0, 1 + 0 = 1 + z0, z0 >= 0 COND(z, z') -{ 1 }-> 1 + COND(1, 0) + ODD(0) :|: z = 2, z' = 0 COND(z, z') -{ 2 }-> 1 + COND(1, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 1 }-> 1 + COND(0, 0) + ODD(z') :|: z = 2, z' >= 0 COND(z, z') -{ 1 }-> 1 + COND(0, 0) + ODD(0) :|: z = 2, z' = 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 1 :|: z = 2, z' >= 0, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' >= 0, z' = 0 COND(z, z') -{ 1 }-> 1 + COND(0, z' - 1) + ODD(1 + (z' - 1)) :|: z = 2, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, z' - 1) + 1 :|: z = 2, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 ODD(z) -{ 1 }-> 1 :|: z = 1 + 0 ODD(z) -{ 1 }-> 0 :|: z = 0 ODD(z) -{ 1 }-> 1 + ODD(z - 2) :|: z - 2 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond(z, z') -{ 0 }-> cond(odd(z' - 2), 0) :|: z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(odd(z' - 2), 1 + (z' - 2)) :|: z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(2, 0) :|: z = 2, z' = 1 + 0 cond(z, z') -{ 0 }-> cond(1, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' >= 0 cond(z, z') -{ 0 }-> cond(0, z' - 1) :|: z = 2, z' - 1 >= 0 cond(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 odd(z) -{ 0 }-> odd(z - 2) :|: z - 2 >= 0 odd(z) -{ 0 }-> 2 :|: z = 1 + 0 odd(z) -{ 0 }-> 1 :|: z = 0 odd(z) -{ 0 }-> 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: {odd}, {p}, {COND}, {cond} Previous analysis results are: P: runtime: O(1) [1], size: O(1) [1] ODD: 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: COND(z, z') -{ 3 + z' }-> 1 + COND(odd(z' - 2), 0) + s1 :|: s1 >= 0, s1 <= 1 + (1 + (z' - 2)), z = 2, z' - 2 >= 0 COND(z, z') -{ 2 }-> 1 + COND(odd(z' - 2), 0) + 1 :|: z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 3 + z' }-> 1 + COND(odd(z' - 2), 1 + (z' - 2)) + s'' :|: s'' >= 0, s'' <= 1 + (1 + (z' - 2)), z = 2, z' - 2 >= 0 COND(z, z') -{ 2 }-> 1 + COND(odd(z' - 2), 1 + (z' - 2)) + 1 :|: z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 4 }-> 1 + COND(2, 0) + s' :|: s' >= 0, s' <= 1 + 0, z = 2, z' = 1 + 0 COND(z, z') -{ 2 }-> 1 + COND(2, 0) + 1 :|: z = 2, z' = 1 + 0, 1 + 0 = 1 + z0, z0 >= 0 COND(z, z') -{ 3 }-> 1 + COND(1, 0) + s :|: s >= 0, s <= 0, z = 2, z' = 0 COND(z, z') -{ 2 }-> 1 + COND(1, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 3 }-> 1 + COND(0, 0) + s2 :|: s2 >= 0, s2 <= 0, z = 2, z' = 0 COND(z, z') -{ 3 + z' }-> 1 + COND(0, 0) + s4 :|: s4 >= 0, s4 <= z', z = 2, z' >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 1 :|: z = 2, z' >= 0, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' >= 0, z' = 0 COND(z, z') -{ 3 + z' }-> 1 + COND(0, z' - 1) + s3 :|: s3 >= 0, s3 <= 1 + (z' - 1), z = 2, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, z' - 1) + 1 :|: z = 2, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 ODD(z) -{ 1 }-> 1 :|: z = 1 + 0 ODD(z) -{ 1 }-> 0 :|: z = 0 ODD(z) -{ 1 + z }-> 1 + s5 :|: s5 >= 0, s5 <= z - 2, z - 2 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond(z, z') -{ 0 }-> cond(odd(z' - 2), 0) :|: z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(odd(z' - 2), 1 + (z' - 2)) :|: z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(2, 0) :|: z = 2, z' = 1 + 0 cond(z, z') -{ 0 }-> cond(1, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' >= 0 cond(z, z') -{ 0 }-> cond(0, z' - 1) :|: z = 2, z' - 1 >= 0 cond(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 odd(z) -{ 0 }-> odd(z - 2) :|: z - 2 >= 0 odd(z) -{ 0 }-> 2 :|: z = 1 + 0 odd(z) -{ 0 }-> 1 :|: z = 0 odd(z) -{ 0 }-> 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: {odd}, {p}, {COND}, {cond} Previous analysis results are: P: runtime: O(1) [1], size: O(1) [1] ODD: runtime: O(n^1) [2 + z], size: O(n^1) [z] ---------------------------------------- (33) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: odd 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: COND(z, z') -{ 3 + z' }-> 1 + COND(odd(z' - 2), 0) + s1 :|: s1 >= 0, s1 <= 1 + (1 + (z' - 2)), z = 2, z' - 2 >= 0 COND(z, z') -{ 2 }-> 1 + COND(odd(z' - 2), 0) + 1 :|: z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 3 + z' }-> 1 + COND(odd(z' - 2), 1 + (z' - 2)) + s'' :|: s'' >= 0, s'' <= 1 + (1 + (z' - 2)), z = 2, z' - 2 >= 0 COND(z, z') -{ 2 }-> 1 + COND(odd(z' - 2), 1 + (z' - 2)) + 1 :|: z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 4 }-> 1 + COND(2, 0) + s' :|: s' >= 0, s' <= 1 + 0, z = 2, z' = 1 + 0 COND(z, z') -{ 2 }-> 1 + COND(2, 0) + 1 :|: z = 2, z' = 1 + 0, 1 + 0 = 1 + z0, z0 >= 0 COND(z, z') -{ 3 }-> 1 + COND(1, 0) + s :|: s >= 0, s <= 0, z = 2, z' = 0 COND(z, z') -{ 2 }-> 1 + COND(1, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 3 }-> 1 + COND(0, 0) + s2 :|: s2 >= 0, s2 <= 0, z = 2, z' = 0 COND(z, z') -{ 3 + z' }-> 1 + COND(0, 0) + s4 :|: s4 >= 0, s4 <= z', z = 2, z' >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 1 :|: z = 2, z' >= 0, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' >= 0, z' = 0 COND(z, z') -{ 3 + z' }-> 1 + COND(0, z' - 1) + s3 :|: s3 >= 0, s3 <= 1 + (z' - 1), z = 2, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, z' - 1) + 1 :|: z = 2, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 ODD(z) -{ 1 }-> 1 :|: z = 1 + 0 ODD(z) -{ 1 }-> 0 :|: z = 0 ODD(z) -{ 1 + z }-> 1 + s5 :|: s5 >= 0, s5 <= z - 2, z - 2 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond(z, z') -{ 0 }-> cond(odd(z' - 2), 0) :|: z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(odd(z' - 2), 1 + (z' - 2)) :|: z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(2, 0) :|: z = 2, z' = 1 + 0 cond(z, z') -{ 0 }-> cond(1, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' >= 0 cond(z, z') -{ 0 }-> cond(0, z' - 1) :|: z = 2, z' - 1 >= 0 cond(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 odd(z) -{ 0 }-> odd(z - 2) :|: z - 2 >= 0 odd(z) -{ 0 }-> 2 :|: z = 1 + 0 odd(z) -{ 0 }-> 1 :|: z = 0 odd(z) -{ 0 }-> 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: {odd}, {p}, {COND}, {cond} Previous analysis results are: P: runtime: O(1) [1], size: O(1) [1] ODD: runtime: O(n^1) [2 + z], size: O(n^1) [z] odd: runtime: ?, size: O(1) [2] ---------------------------------------- (35) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: odd 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: COND(z, z') -{ 3 + z' }-> 1 + COND(odd(z' - 2), 0) + s1 :|: s1 >= 0, s1 <= 1 + (1 + (z' - 2)), z = 2, z' - 2 >= 0 COND(z, z') -{ 2 }-> 1 + COND(odd(z' - 2), 0) + 1 :|: z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 3 + z' }-> 1 + COND(odd(z' - 2), 1 + (z' - 2)) + s'' :|: s'' >= 0, s'' <= 1 + (1 + (z' - 2)), z = 2, z' - 2 >= 0 COND(z, z') -{ 2 }-> 1 + COND(odd(z' - 2), 1 + (z' - 2)) + 1 :|: z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 4 }-> 1 + COND(2, 0) + s' :|: s' >= 0, s' <= 1 + 0, z = 2, z' = 1 + 0 COND(z, z') -{ 2 }-> 1 + COND(2, 0) + 1 :|: z = 2, z' = 1 + 0, 1 + 0 = 1 + z0, z0 >= 0 COND(z, z') -{ 3 }-> 1 + COND(1, 0) + s :|: s >= 0, s <= 0, z = 2, z' = 0 COND(z, z') -{ 2 }-> 1 + COND(1, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 3 }-> 1 + COND(0, 0) + s2 :|: s2 >= 0, s2 <= 0, z = 2, z' = 0 COND(z, z') -{ 3 + z' }-> 1 + COND(0, 0) + s4 :|: s4 >= 0, s4 <= z', z = 2, z' >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 1 :|: z = 2, z' >= 0, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' >= 0, z' = 0 COND(z, z') -{ 3 + z' }-> 1 + COND(0, z' - 1) + s3 :|: s3 >= 0, s3 <= 1 + (z' - 1), z = 2, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, z' - 1) + 1 :|: z = 2, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 ODD(z) -{ 1 }-> 1 :|: z = 1 + 0 ODD(z) -{ 1 }-> 0 :|: z = 0 ODD(z) -{ 1 + z }-> 1 + s5 :|: s5 >= 0, s5 <= z - 2, z - 2 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond(z, z') -{ 0 }-> cond(odd(z' - 2), 0) :|: z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(odd(z' - 2), 1 + (z' - 2)) :|: z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(2, 0) :|: z = 2, z' = 1 + 0 cond(z, z') -{ 0 }-> cond(1, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' >= 0 cond(z, z') -{ 0 }-> cond(0, z' - 1) :|: z = 2, z' - 1 >= 0 cond(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 odd(z) -{ 0 }-> odd(z - 2) :|: z - 2 >= 0 odd(z) -{ 0 }-> 2 :|: z = 1 + 0 odd(z) -{ 0 }-> 1 :|: z = 0 odd(z) -{ 0 }-> 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}, {COND}, {cond} Previous analysis results are: P: runtime: O(1) [1], size: O(1) [1] ODD: runtime: O(n^1) [2 + z], size: O(n^1) [z] odd: 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: COND(z, z') -{ 2 }-> 1 + COND(s11, 1 + (z' - 2)) + 1 :|: s11 >= 0, s11 <= 2, z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 2 }-> 1 + COND(s12, 0) + 1 :|: s12 >= 0, s12 <= 2, z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 3 + z' }-> 1 + COND(s6, 1 + (z' - 2)) + s'' :|: s6 >= 0, s6 <= 2, s'' >= 0, s'' <= 1 + (1 + (z' - 2)), z = 2, z' - 2 >= 0 COND(z, z') -{ 3 + z' }-> 1 + COND(s7, 0) + s1 :|: s7 >= 0, s7 <= 2, s1 >= 0, s1 <= 1 + (1 + (z' - 2)), z = 2, z' - 2 >= 0 COND(z, z') -{ 4 }-> 1 + COND(2, 0) + s' :|: s' >= 0, s' <= 1 + 0, z = 2, z' = 1 + 0 COND(z, z') -{ 2 }-> 1 + COND(2, 0) + 1 :|: z = 2, z' = 1 + 0, 1 + 0 = 1 + z0, z0 >= 0 COND(z, z') -{ 3 }-> 1 + COND(1, 0) + s :|: s >= 0, s <= 0, z = 2, z' = 0 COND(z, z') -{ 2 }-> 1 + COND(1, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 3 }-> 1 + COND(0, 0) + s2 :|: s2 >= 0, s2 <= 0, z = 2, z' = 0 COND(z, z') -{ 3 + z' }-> 1 + COND(0, 0) + s4 :|: s4 >= 0, s4 <= z', z = 2, z' >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 1 :|: z = 2, z' >= 0, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' >= 0, z' = 0 COND(z, z') -{ 3 + z' }-> 1 + COND(0, z' - 1) + s3 :|: s3 >= 0, s3 <= 1 + (z' - 1), z = 2, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, z' - 1) + 1 :|: z = 2, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 ODD(z) -{ 1 }-> 1 :|: z = 1 + 0 ODD(z) -{ 1 }-> 0 :|: z = 0 ODD(z) -{ 1 + z }-> 1 + s5 :|: s5 >= 0, s5 <= z - 2, z - 2 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond(z, z') -{ 0 }-> cond(s8, 1 + (z' - 2)) :|: s8 >= 0, s8 <= 2, z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(s9, 0) :|: s9 >= 0, s9 <= 2, z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(2, 0) :|: z = 2, z' = 1 + 0 cond(z, z') -{ 0 }-> cond(1, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' >= 0 cond(z, z') -{ 0 }-> cond(0, z' - 1) :|: z = 2, z' - 1 >= 0 cond(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 odd(z) -{ 0 }-> s10 :|: s10 >= 0, s10 <= 2, z - 2 >= 0 odd(z) -{ 0 }-> 2 :|: z = 1 + 0 odd(z) -{ 0 }-> 1 :|: z = 0 odd(z) -{ 0 }-> 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}, {COND}, {cond} Previous analysis results are: P: runtime: O(1) [1], size: O(1) [1] ODD: runtime: O(n^1) [2 + z], size: O(n^1) [z] odd: runtime: O(1) [0], size: O(1) [2] ---------------------------------------- (39) 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 ---------------------------------------- (40) Obligation: Complexity RNTS consisting of the following rules: COND(z, z') -{ 2 }-> 1 + COND(s11, 1 + (z' - 2)) + 1 :|: s11 >= 0, s11 <= 2, z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 2 }-> 1 + COND(s12, 0) + 1 :|: s12 >= 0, s12 <= 2, z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 3 + z' }-> 1 + COND(s6, 1 + (z' - 2)) + s'' :|: s6 >= 0, s6 <= 2, s'' >= 0, s'' <= 1 + (1 + (z' - 2)), z = 2, z' - 2 >= 0 COND(z, z') -{ 3 + z' }-> 1 + COND(s7, 0) + s1 :|: s7 >= 0, s7 <= 2, s1 >= 0, s1 <= 1 + (1 + (z' - 2)), z = 2, z' - 2 >= 0 COND(z, z') -{ 4 }-> 1 + COND(2, 0) + s' :|: s' >= 0, s' <= 1 + 0, z = 2, z' = 1 + 0 COND(z, z') -{ 2 }-> 1 + COND(2, 0) + 1 :|: z = 2, z' = 1 + 0, 1 + 0 = 1 + z0, z0 >= 0 COND(z, z') -{ 3 }-> 1 + COND(1, 0) + s :|: s >= 0, s <= 0, z = 2, z' = 0 COND(z, z') -{ 2 }-> 1 + COND(1, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 3 }-> 1 + COND(0, 0) + s2 :|: s2 >= 0, s2 <= 0, z = 2, z' = 0 COND(z, z') -{ 3 + z' }-> 1 + COND(0, 0) + s4 :|: s4 >= 0, s4 <= z', z = 2, z' >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 1 :|: z = 2, z' >= 0, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' >= 0, z' = 0 COND(z, z') -{ 3 + z' }-> 1 + COND(0, z' - 1) + s3 :|: s3 >= 0, s3 <= 1 + (z' - 1), z = 2, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, z' - 1) + 1 :|: z = 2, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 ODD(z) -{ 1 }-> 1 :|: z = 1 + 0 ODD(z) -{ 1 }-> 0 :|: z = 0 ODD(z) -{ 1 + z }-> 1 + s5 :|: s5 >= 0, s5 <= z - 2, z - 2 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond(z, z') -{ 0 }-> cond(s8, 1 + (z' - 2)) :|: s8 >= 0, s8 <= 2, z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(s9, 0) :|: s9 >= 0, s9 <= 2, z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(2, 0) :|: z = 2, z' = 1 + 0 cond(z, z') -{ 0 }-> cond(1, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' >= 0 cond(z, z') -{ 0 }-> cond(0, z' - 1) :|: z = 2, z' - 1 >= 0 cond(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 odd(z) -{ 0 }-> s10 :|: s10 >= 0, s10 <= 2, z - 2 >= 0 odd(z) -{ 0 }-> 2 :|: z = 1 + 0 odd(z) -{ 0 }-> 1 :|: z = 0 odd(z) -{ 0 }-> 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}, {COND}, {cond} Previous analysis results are: P: runtime: O(1) [1], size: O(1) [1] ODD: runtime: O(n^1) [2 + z], size: O(n^1) [z] odd: runtime: O(1) [0], size: O(1) [2] p: runtime: ?, size: O(n^1) [z] ---------------------------------------- (41) 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 ---------------------------------------- (42) Obligation: Complexity RNTS consisting of the following rules: COND(z, z') -{ 2 }-> 1 + COND(s11, 1 + (z' - 2)) + 1 :|: s11 >= 0, s11 <= 2, z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 2 }-> 1 + COND(s12, 0) + 1 :|: s12 >= 0, s12 <= 2, z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 3 + z' }-> 1 + COND(s6, 1 + (z' - 2)) + s'' :|: s6 >= 0, s6 <= 2, s'' >= 0, s'' <= 1 + (1 + (z' - 2)), z = 2, z' - 2 >= 0 COND(z, z') -{ 3 + z' }-> 1 + COND(s7, 0) + s1 :|: s7 >= 0, s7 <= 2, s1 >= 0, s1 <= 1 + (1 + (z' - 2)), z = 2, z' - 2 >= 0 COND(z, z') -{ 4 }-> 1 + COND(2, 0) + s' :|: s' >= 0, s' <= 1 + 0, z = 2, z' = 1 + 0 COND(z, z') -{ 2 }-> 1 + COND(2, 0) + 1 :|: z = 2, z' = 1 + 0, 1 + 0 = 1 + z0, z0 >= 0 COND(z, z') -{ 3 }-> 1 + COND(1, 0) + s :|: s >= 0, s <= 0, z = 2, z' = 0 COND(z, z') -{ 2 }-> 1 + COND(1, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 3 }-> 1 + COND(0, 0) + s2 :|: s2 >= 0, s2 <= 0, z = 2, z' = 0 COND(z, z') -{ 3 + z' }-> 1 + COND(0, 0) + s4 :|: s4 >= 0, s4 <= z', z = 2, z' >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 1 :|: z = 2, z' >= 0, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' >= 0, z' = 0 COND(z, z') -{ 3 + z' }-> 1 + COND(0, z' - 1) + s3 :|: s3 >= 0, s3 <= 1 + (z' - 1), z = 2, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, z' - 1) + 1 :|: z = 2, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 ODD(z) -{ 1 }-> 1 :|: z = 1 + 0 ODD(z) -{ 1 }-> 0 :|: z = 0 ODD(z) -{ 1 + z }-> 1 + s5 :|: s5 >= 0, s5 <= z - 2, z - 2 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond(z, z') -{ 0 }-> cond(s8, 1 + (z' - 2)) :|: s8 >= 0, s8 <= 2, z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(s9, 0) :|: s9 >= 0, s9 <= 2, z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(2, 0) :|: z = 2, z' = 1 + 0 cond(z, z') -{ 0 }-> cond(1, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' >= 0 cond(z, z') -{ 0 }-> cond(0, z' - 1) :|: z = 2, z' - 1 >= 0 cond(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 odd(z) -{ 0 }-> s10 :|: s10 >= 0, s10 <= 2, z - 2 >= 0 odd(z) -{ 0 }-> 2 :|: z = 1 + 0 odd(z) -{ 0 }-> 1 :|: z = 0 odd(z) -{ 0 }-> 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: {COND}, {cond} Previous analysis results are: P: runtime: O(1) [1], size: O(1) [1] ODD: runtime: O(n^1) [2 + z], size: O(n^1) [z] odd: runtime: O(1) [0], size: O(1) [2] p: runtime: O(1) [0], size: O(n^1) [z] ---------------------------------------- (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: COND(z, z') -{ 2 }-> 1 + COND(s11, 1 + (z' - 2)) + 1 :|: s11 >= 0, s11 <= 2, z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 2 }-> 1 + COND(s12, 0) + 1 :|: s12 >= 0, s12 <= 2, z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 3 + z' }-> 1 + COND(s6, 1 + (z' - 2)) + s'' :|: s6 >= 0, s6 <= 2, s'' >= 0, s'' <= 1 + (1 + (z' - 2)), z = 2, z' - 2 >= 0 COND(z, z') -{ 3 + z' }-> 1 + COND(s7, 0) + s1 :|: s7 >= 0, s7 <= 2, s1 >= 0, s1 <= 1 + (1 + (z' - 2)), z = 2, z' - 2 >= 0 COND(z, z') -{ 4 }-> 1 + COND(2, 0) + s' :|: s' >= 0, s' <= 1 + 0, z = 2, z' = 1 + 0 COND(z, z') -{ 2 }-> 1 + COND(2, 0) + 1 :|: z = 2, z' = 1 + 0, 1 + 0 = 1 + z0, z0 >= 0 COND(z, z') -{ 3 }-> 1 + COND(1, 0) + s :|: s >= 0, s <= 0, z = 2, z' = 0 COND(z, z') -{ 2 }-> 1 + COND(1, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 3 }-> 1 + COND(0, 0) + s2 :|: s2 >= 0, s2 <= 0, z = 2, z' = 0 COND(z, z') -{ 3 + z' }-> 1 + COND(0, 0) + s4 :|: s4 >= 0, s4 <= z', z = 2, z' >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 1 :|: z = 2, z' >= 0, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' >= 0, z' = 0 COND(z, z') -{ 3 + z' }-> 1 + COND(0, z' - 1) + s3 :|: s3 >= 0, s3 <= 1 + (z' - 1), z = 2, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, z' - 1) + 1 :|: z = 2, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 ODD(z) -{ 1 }-> 1 :|: z = 1 + 0 ODD(z) -{ 1 }-> 0 :|: z = 0 ODD(z) -{ 1 + z }-> 1 + s5 :|: s5 >= 0, s5 <= z - 2, z - 2 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond(z, z') -{ 0 }-> cond(s8, 1 + (z' - 2)) :|: s8 >= 0, s8 <= 2, z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(s9, 0) :|: s9 >= 0, s9 <= 2, z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(2, 0) :|: z = 2, z' = 1 + 0 cond(z, z') -{ 0 }-> cond(1, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' >= 0 cond(z, z') -{ 0 }-> cond(0, z' - 1) :|: z = 2, z' - 1 >= 0 cond(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 odd(z) -{ 0 }-> s10 :|: s10 >= 0, s10 <= 2, z - 2 >= 0 odd(z) -{ 0 }-> 2 :|: z = 1 + 0 odd(z) -{ 0 }-> 1 :|: z = 0 odd(z) -{ 0 }-> 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: {COND}, {cond} Previous analysis results are: P: runtime: O(1) [1], size: O(1) [1] ODD: runtime: O(n^1) [2 + z], size: O(n^1) [z] odd: runtime: O(1) [0], size: O(1) [2] p: runtime: O(1) [0], size: O(n^1) [z] ---------------------------------------- (45) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: COND after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 0 ---------------------------------------- (46) Obligation: Complexity RNTS consisting of the following rules: COND(z, z') -{ 2 }-> 1 + COND(s11, 1 + (z' - 2)) + 1 :|: s11 >= 0, s11 <= 2, z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 2 }-> 1 + COND(s12, 0) + 1 :|: s12 >= 0, s12 <= 2, z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 3 + z' }-> 1 + COND(s6, 1 + (z' - 2)) + s'' :|: s6 >= 0, s6 <= 2, s'' >= 0, s'' <= 1 + (1 + (z' - 2)), z = 2, z' - 2 >= 0 COND(z, z') -{ 3 + z' }-> 1 + COND(s7, 0) + s1 :|: s7 >= 0, s7 <= 2, s1 >= 0, s1 <= 1 + (1 + (z' - 2)), z = 2, z' - 2 >= 0 COND(z, z') -{ 4 }-> 1 + COND(2, 0) + s' :|: s' >= 0, s' <= 1 + 0, z = 2, z' = 1 + 0 COND(z, z') -{ 2 }-> 1 + COND(2, 0) + 1 :|: z = 2, z' = 1 + 0, 1 + 0 = 1 + z0, z0 >= 0 COND(z, z') -{ 3 }-> 1 + COND(1, 0) + s :|: s >= 0, s <= 0, z = 2, z' = 0 COND(z, z') -{ 2 }-> 1 + COND(1, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 3 }-> 1 + COND(0, 0) + s2 :|: s2 >= 0, s2 <= 0, z = 2, z' = 0 COND(z, z') -{ 3 + z' }-> 1 + COND(0, 0) + s4 :|: s4 >= 0, s4 <= z', z = 2, z' >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 1 :|: z = 2, z' >= 0, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' >= 0, z' = 0 COND(z, z') -{ 3 + z' }-> 1 + COND(0, z' - 1) + s3 :|: s3 >= 0, s3 <= 1 + (z' - 1), z = 2, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, z' - 1) + 1 :|: z = 2, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 ODD(z) -{ 1 }-> 1 :|: z = 1 + 0 ODD(z) -{ 1 }-> 0 :|: z = 0 ODD(z) -{ 1 + z }-> 1 + s5 :|: s5 >= 0, s5 <= z - 2, z - 2 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond(z, z') -{ 0 }-> cond(s8, 1 + (z' - 2)) :|: s8 >= 0, s8 <= 2, z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(s9, 0) :|: s9 >= 0, s9 <= 2, z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(2, 0) :|: z = 2, z' = 1 + 0 cond(z, z') -{ 0 }-> cond(1, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' >= 0 cond(z, z') -{ 0 }-> cond(0, z' - 1) :|: z = 2, z' - 1 >= 0 cond(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 odd(z) -{ 0 }-> s10 :|: s10 >= 0, s10 <= 2, z - 2 >= 0 odd(z) -{ 0 }-> 2 :|: z = 1 + 0 odd(z) -{ 0 }-> 1 :|: z = 0 odd(z) -{ 0 }-> 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: {COND}, {cond} Previous analysis results are: P: runtime: O(1) [1], size: O(1) [1] ODD: runtime: O(n^1) [2 + z], size: O(n^1) [z] odd: runtime: O(1) [0], size: O(1) [2] p: runtime: O(1) [0], size: O(n^1) [z] COND: runtime: ?, size: O(1) [0] ---------------------------------------- (47) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: COND after applying outer abstraction to obtain an ITS, resulting in: O(n^2) with polynomial bound: 12 + 6*z' + z'^2 ---------------------------------------- (48) Obligation: Complexity RNTS consisting of the following rules: COND(z, z') -{ 2 }-> 1 + COND(s11, 1 + (z' - 2)) + 1 :|: s11 >= 0, s11 <= 2, z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 2 }-> 1 + COND(s12, 0) + 1 :|: s12 >= 0, s12 <= 2, z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 3 + z' }-> 1 + COND(s6, 1 + (z' - 2)) + s'' :|: s6 >= 0, s6 <= 2, s'' >= 0, s'' <= 1 + (1 + (z' - 2)), z = 2, z' - 2 >= 0 COND(z, z') -{ 3 + z' }-> 1 + COND(s7, 0) + s1 :|: s7 >= 0, s7 <= 2, s1 >= 0, s1 <= 1 + (1 + (z' - 2)), z = 2, z' - 2 >= 0 COND(z, z') -{ 4 }-> 1 + COND(2, 0) + s' :|: s' >= 0, s' <= 1 + 0, z = 2, z' = 1 + 0 COND(z, z') -{ 2 }-> 1 + COND(2, 0) + 1 :|: z = 2, z' = 1 + 0, 1 + 0 = 1 + z0, z0 >= 0 COND(z, z') -{ 3 }-> 1 + COND(1, 0) + s :|: s >= 0, s <= 0, z = 2, z' = 0 COND(z, z') -{ 2 }-> 1 + COND(1, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 3 }-> 1 + COND(0, 0) + s2 :|: s2 >= 0, s2 <= 0, z = 2, z' = 0 COND(z, z') -{ 3 + z' }-> 1 + COND(0, 0) + s4 :|: s4 >= 0, s4 <= z', z = 2, z' >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 1 :|: z = 2, z' >= 0, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' = 0, 0 = 0 COND(z, z') -{ 2 }-> 1 + COND(0, 0) + 0 :|: z = 2, z' >= 0, z' = 0 COND(z, z') -{ 3 + z' }-> 1 + COND(0, z' - 1) + s3 :|: s3 >= 0, s3 <= 1 + (z' - 1), z = 2, z' - 1 >= 0 COND(z, z') -{ 2 }-> 1 + COND(0, z' - 1) + 1 :|: z = 2, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 ODD(z) -{ 1 }-> 1 :|: z = 1 + 0 ODD(z) -{ 1 }-> 0 :|: z = 0 ODD(z) -{ 1 + z }-> 1 + s5 :|: s5 >= 0, s5 <= z - 2, z - 2 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond(z, z') -{ 0 }-> cond(s8, 1 + (z' - 2)) :|: s8 >= 0, s8 <= 2, z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(s9, 0) :|: s9 >= 0, s9 <= 2, z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(2, 0) :|: z = 2, z' = 1 + 0 cond(z, z') -{ 0 }-> cond(1, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' >= 0 cond(z, z') -{ 0 }-> cond(0, z' - 1) :|: z = 2, z' - 1 >= 0 cond(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 odd(z) -{ 0 }-> s10 :|: s10 >= 0, s10 <= 2, z - 2 >= 0 odd(z) -{ 0 }-> 2 :|: z = 1 + 0 odd(z) -{ 0 }-> 1 :|: z = 0 odd(z) -{ 0 }-> 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: {cond} Previous analysis results are: P: runtime: O(1) [1], size: O(1) [1] ODD: runtime: O(n^1) [2 + z], size: O(n^1) [z] odd: runtime: O(1) [0], size: O(1) [2] p: runtime: O(1) [0], size: O(n^1) [z] COND: runtime: O(n^2) [12 + 6*z' + z'^2], size: O(1) [0] ---------------------------------------- (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: COND(z, z') -{ 15 }-> 1 + s13 + s :|: s13 >= 0, s13 <= 0, s >= 0, s <= 0, z = 2, z' = 0 COND(z, z') -{ 16 }-> 1 + s14 + s' :|: s14 >= 0, s14 <= 0, s' >= 0, s' <= 1 + 0, z = 2, z' = 1 + 0 COND(z, z') -{ 10 + 5*z' + z'^2 }-> 1 + s15 + s'' :|: s15 >= 0, s15 <= 0, s6 >= 0, s6 <= 2, s'' >= 0, s'' <= 1 + (1 + (z' - 2)), z = 2, z' - 2 >= 0 COND(z, z') -{ 15 + z' }-> 1 + s16 + s1 :|: s16 >= 0, s16 <= 0, s7 >= 0, s7 <= 2, s1 >= 0, s1 <= 1 + (1 + (z' - 2)), z = 2, z' - 2 >= 0 COND(z, z') -{ 15 }-> 1 + s17 + s2 :|: s17 >= 0, s17 <= 0, s2 >= 0, s2 <= 0, z = 2, z' = 0 COND(z, z') -{ 10 + 5*z' + z'^2 }-> 1 + s18 + s3 :|: s18 >= 0, s18 <= 0, s3 >= 0, s3 <= 1 + (z' - 1), z = 2, z' - 1 >= 0 COND(z, z') -{ 15 + z' }-> 1 + s19 + s4 :|: s19 >= 0, s19 <= 0, s4 >= 0, s4 <= z', z = 2, z' >= 0 COND(z, z') -{ 14 }-> 1 + s20 + 0 :|: s20 >= 0, s20 <= 0, z = 2, z' = 0, 0 = 0 COND(z, z') -{ 14 }-> 1 + s21 + 1 :|: s21 >= 0, s21 <= 0, z = 2, z' = 1 + 0, 1 + 0 = 1 + z0, z0 >= 0 COND(z, z') -{ 9 + 4*z' + z'^2 }-> 1 + s22 + 1 :|: s22 >= 0, s22 <= 0, s11 >= 0, s11 <= 2, z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 14 }-> 1 + s23 + 1 :|: s23 >= 0, s23 <= 0, s12 >= 0, s12 <= 2, z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 14 }-> 1 + s24 + 0 :|: s24 >= 0, s24 <= 0, z = 2, z' = 0, 0 = 0 COND(z, z') -{ 9 + 4*z' + z'^2 }-> 1 + s25 + 1 :|: s25 >= 0, s25 <= 0, z = 2, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND(z, z') -{ 14 }-> 1 + s26 + 1 :|: s26 >= 0, s26 <= 0, z = 2, z' >= 0, z' - 1 >= 0 COND(z, z') -{ 14 }-> 1 + s27 + 0 :|: s27 >= 0, s27 <= 0, z = 2, z' >= 0, z' = 0 ODD(z) -{ 1 }-> 1 :|: z = 1 + 0 ODD(z) -{ 1 }-> 0 :|: z = 0 ODD(z) -{ 1 + z }-> 1 + s5 :|: s5 >= 0, s5 <= z - 2, z - 2 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond(z, z') -{ 0 }-> cond(s8, 1 + (z' - 2)) :|: s8 >= 0, s8 <= 2, z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(s9, 0) :|: s9 >= 0, s9 <= 2, z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(2, 0) :|: z = 2, z' = 1 + 0 cond(z, z') -{ 0 }-> cond(1, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' >= 0 cond(z, z') -{ 0 }-> cond(0, z' - 1) :|: z = 2, z' - 1 >= 0 cond(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 odd(z) -{ 0 }-> s10 :|: s10 >= 0, s10 <= 2, z - 2 >= 0 odd(z) -{ 0 }-> 2 :|: z = 1 + 0 odd(z) -{ 0 }-> 1 :|: z = 0 odd(z) -{ 0 }-> 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: {cond} Previous analysis results are: P: runtime: O(1) [1], size: O(1) [1] ODD: runtime: O(n^1) [2 + z], size: O(n^1) [z] odd: runtime: O(1) [0], size: O(1) [2] p: runtime: O(1) [0], size: O(n^1) [z] COND: runtime: O(n^2) [12 + 6*z' + z'^2], size: O(1) [0] ---------------------------------------- (51) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: cond after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 0 ---------------------------------------- (52) Obligation: Complexity RNTS consisting of the following rules: COND(z, z') -{ 15 }-> 1 + s13 + s :|: s13 >= 0, s13 <= 0, s >= 0, s <= 0, z = 2, z' = 0 COND(z, z') -{ 16 }-> 1 + s14 + s' :|: s14 >= 0, s14 <= 0, s' >= 0, s' <= 1 + 0, z = 2, z' = 1 + 0 COND(z, z') -{ 10 + 5*z' + z'^2 }-> 1 + s15 + s'' :|: s15 >= 0, s15 <= 0, s6 >= 0, s6 <= 2, s'' >= 0, s'' <= 1 + (1 + (z' - 2)), z = 2, z' - 2 >= 0 COND(z, z') -{ 15 + z' }-> 1 + s16 + s1 :|: s16 >= 0, s16 <= 0, s7 >= 0, s7 <= 2, s1 >= 0, s1 <= 1 + (1 + (z' - 2)), z = 2, z' - 2 >= 0 COND(z, z') -{ 15 }-> 1 + s17 + s2 :|: s17 >= 0, s17 <= 0, s2 >= 0, s2 <= 0, z = 2, z' = 0 COND(z, z') -{ 10 + 5*z' + z'^2 }-> 1 + s18 + s3 :|: s18 >= 0, s18 <= 0, s3 >= 0, s3 <= 1 + (z' - 1), z = 2, z' - 1 >= 0 COND(z, z') -{ 15 + z' }-> 1 + s19 + s4 :|: s19 >= 0, s19 <= 0, s4 >= 0, s4 <= z', z = 2, z' >= 0 COND(z, z') -{ 14 }-> 1 + s20 + 0 :|: s20 >= 0, s20 <= 0, z = 2, z' = 0, 0 = 0 COND(z, z') -{ 14 }-> 1 + s21 + 1 :|: s21 >= 0, s21 <= 0, z = 2, z' = 1 + 0, 1 + 0 = 1 + z0, z0 >= 0 COND(z, z') -{ 9 + 4*z' + z'^2 }-> 1 + s22 + 1 :|: s22 >= 0, s22 <= 0, s11 >= 0, s11 <= 2, z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 14 }-> 1 + s23 + 1 :|: s23 >= 0, s23 <= 0, s12 >= 0, s12 <= 2, z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 14 }-> 1 + s24 + 0 :|: s24 >= 0, s24 <= 0, z = 2, z' = 0, 0 = 0 COND(z, z') -{ 9 + 4*z' + z'^2 }-> 1 + s25 + 1 :|: s25 >= 0, s25 <= 0, z = 2, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND(z, z') -{ 14 }-> 1 + s26 + 1 :|: s26 >= 0, s26 <= 0, z = 2, z' >= 0, z' - 1 >= 0 COND(z, z') -{ 14 }-> 1 + s27 + 0 :|: s27 >= 0, s27 <= 0, z = 2, z' >= 0, z' = 0 ODD(z) -{ 1 }-> 1 :|: z = 1 + 0 ODD(z) -{ 1 }-> 0 :|: z = 0 ODD(z) -{ 1 + z }-> 1 + s5 :|: s5 >= 0, s5 <= z - 2, z - 2 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond(z, z') -{ 0 }-> cond(s8, 1 + (z' - 2)) :|: s8 >= 0, s8 <= 2, z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(s9, 0) :|: s9 >= 0, s9 <= 2, z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(2, 0) :|: z = 2, z' = 1 + 0 cond(z, z') -{ 0 }-> cond(1, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' >= 0 cond(z, z') -{ 0 }-> cond(0, z' - 1) :|: z = 2, z' - 1 >= 0 cond(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 odd(z) -{ 0 }-> s10 :|: s10 >= 0, s10 <= 2, z - 2 >= 0 odd(z) -{ 0 }-> 2 :|: z = 1 + 0 odd(z) -{ 0 }-> 1 :|: z = 0 odd(z) -{ 0 }-> 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: {cond} Previous analysis results are: P: runtime: O(1) [1], size: O(1) [1] ODD: runtime: O(n^1) [2 + z], size: O(n^1) [z] odd: runtime: O(1) [0], size: O(1) [2] p: runtime: O(1) [0], size: O(n^1) [z] COND: runtime: O(n^2) [12 + 6*z' + z'^2], size: O(1) [0] cond: runtime: ?, size: O(1) [0] ---------------------------------------- (53) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: cond after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 0 ---------------------------------------- (54) Obligation: Complexity RNTS consisting of the following rules: COND(z, z') -{ 15 }-> 1 + s13 + s :|: s13 >= 0, s13 <= 0, s >= 0, s <= 0, z = 2, z' = 0 COND(z, z') -{ 16 }-> 1 + s14 + s' :|: s14 >= 0, s14 <= 0, s' >= 0, s' <= 1 + 0, z = 2, z' = 1 + 0 COND(z, z') -{ 10 + 5*z' + z'^2 }-> 1 + s15 + s'' :|: s15 >= 0, s15 <= 0, s6 >= 0, s6 <= 2, s'' >= 0, s'' <= 1 + (1 + (z' - 2)), z = 2, z' - 2 >= 0 COND(z, z') -{ 15 + z' }-> 1 + s16 + s1 :|: s16 >= 0, s16 <= 0, s7 >= 0, s7 <= 2, s1 >= 0, s1 <= 1 + (1 + (z' - 2)), z = 2, z' - 2 >= 0 COND(z, z') -{ 15 }-> 1 + s17 + s2 :|: s17 >= 0, s17 <= 0, s2 >= 0, s2 <= 0, z = 2, z' = 0 COND(z, z') -{ 10 + 5*z' + z'^2 }-> 1 + s18 + s3 :|: s18 >= 0, s18 <= 0, s3 >= 0, s3 <= 1 + (z' - 1), z = 2, z' - 1 >= 0 COND(z, z') -{ 15 + z' }-> 1 + s19 + s4 :|: s19 >= 0, s19 <= 0, s4 >= 0, s4 <= z', z = 2, z' >= 0 COND(z, z') -{ 14 }-> 1 + s20 + 0 :|: s20 >= 0, s20 <= 0, z = 2, z' = 0, 0 = 0 COND(z, z') -{ 14 }-> 1 + s21 + 1 :|: s21 >= 0, s21 <= 0, z = 2, z' = 1 + 0, 1 + 0 = 1 + z0, z0 >= 0 COND(z, z') -{ 9 + 4*z' + z'^2 }-> 1 + s22 + 1 :|: s22 >= 0, s22 <= 0, s11 >= 0, s11 <= 2, z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 14 }-> 1 + s23 + 1 :|: s23 >= 0, s23 <= 0, s12 >= 0, s12 <= 2, z = 2, z' - 2 >= 0, 1 + (1 + (z' - 2)) = 1 + z0, z0 >= 0 COND(z, z') -{ 14 }-> 1 + s24 + 0 :|: s24 >= 0, s24 <= 0, z = 2, z' = 0, 0 = 0 COND(z, z') -{ 9 + 4*z' + z'^2 }-> 1 + s25 + 1 :|: s25 >= 0, s25 <= 0, z = 2, z' - 1 >= 0, 1 + (z' - 1) = 1 + z0, z0 >= 0 COND(z, z') -{ 14 }-> 1 + s26 + 1 :|: s26 >= 0, s26 <= 0, z = 2, z' >= 0, z' - 1 >= 0 COND(z, z') -{ 14 }-> 1 + s27 + 0 :|: s27 >= 0, s27 <= 0, z = 2, z' >= 0, z' = 0 ODD(z) -{ 1 }-> 1 :|: z = 1 + 0 ODD(z) -{ 1 }-> 0 :|: z = 0 ODD(z) -{ 1 + z }-> 1 + s5 :|: s5 >= 0, s5 <= z - 2, z - 2 >= 0 P(z) -{ 1 }-> 1 :|: z - 1 >= 0 P(z) -{ 1 }-> 0 :|: z = 0 cond(z, z') -{ 0 }-> cond(s8, 1 + (z' - 2)) :|: s8 >= 0, s8 <= 2, z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(s9, 0) :|: s9 >= 0, s9 <= 2, z = 2, z' - 2 >= 0 cond(z, z') -{ 0 }-> cond(2, 0) :|: z = 2, z' = 1 + 0 cond(z, z') -{ 0 }-> cond(1, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' = 0 cond(z, z') -{ 0 }-> cond(0, 0) :|: z = 2, z' >= 0 cond(z, z') -{ 0 }-> cond(0, z' - 1) :|: z = 2, z' - 1 >= 0 cond(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 odd(z) -{ 0 }-> s10 :|: s10 >= 0, s10 <= 2, z - 2 >= 0 odd(z) -{ 0 }-> 2 :|: z = 1 + 0 odd(z) -{ 0 }-> 1 :|: z = 0 odd(z) -{ 0 }-> 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] ODD: runtime: O(n^1) [2 + z], size: O(n^1) [z] odd: runtime: O(1) [0], size: O(1) [2] p: runtime: O(1) [0], size: O(n^1) [z] COND: runtime: O(n^2) [12 + 6*z' + z'^2], size: O(1) [0] cond: runtime: O(1) [0], size: O(1) [0] ---------------------------------------- (55) FinalProof (FINISHED) Computed overall runtime complexity ---------------------------------------- (56) BOUNDS(1, n^2) ---------------------------------------- (57) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (58) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: COND(true, z0) -> c(COND(odd(z0), p(z0)), ODD(z0)) COND(true, z0) -> c1(COND(odd(z0), p(z0)), P(z0)) ODD(0') -> c2 ODD(s(0')) -> c3 ODD(s(s(z0))) -> c4(ODD(z0)) P(0') -> c5 P(s(z0)) -> c6 The (relative) TRS S consists of the following rules: cond(true, z0) -> cond(odd(z0), p(z0)) odd(0') -> false odd(s(0')) -> true odd(s(s(z0))) -> odd(z0) p(0') -> 0' p(s(z0)) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (59) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (60) Obligation: Innermost TRS: Rules: COND(true, z0) -> c(COND(odd(z0), p(z0)), ODD(z0)) COND(true, z0) -> c1(COND(odd(z0), p(z0)), P(z0)) ODD(0') -> c2 ODD(s(0')) -> c3 ODD(s(s(z0))) -> c4(ODD(z0)) P(0') -> c5 P(s(z0)) -> c6 cond(true, z0) -> cond(odd(z0), p(z0)) odd(0') -> false odd(s(0')) -> true odd(s(s(z0))) -> odd(z0) p(0') -> 0' p(s(z0)) -> z0 Types: COND :: true:false -> 0':s -> c:c1 true :: true:false c :: c:c1 -> c2:c3:c4 -> c:c1 odd :: 0':s -> true:false p :: 0':s -> 0':s ODD :: 0':s -> c2:c3:c4 c1 :: c:c1 -> c5:c6 -> c:c1 P :: 0':s -> c5:c6 0' :: 0':s c2 :: c2:c3:c4 s :: 0':s -> 0':s c3 :: c2:c3:c4 c4 :: c2:c3:c4 -> c2:c3:c4 c5 :: c5:c6 c6 :: c5:c6 cond :: true:false -> 0':s -> cond false :: true:false hole_c:c11_7 :: c:c1 hole_true:false2_7 :: true:false hole_0':s3_7 :: 0':s hole_c2:c3:c44_7 :: c2:c3:c4 hole_c5:c65_7 :: c5:c6 hole_cond6_7 :: cond gen_c:c17_7 :: Nat -> c:c1 gen_0':s8_7 :: Nat -> 0':s gen_c2:c3:c49_7 :: Nat -> c2:c3:c4 ---------------------------------------- (61) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: COND, odd, ODD, cond They will be analysed ascendingly in the following order: odd < COND ODD < COND odd < cond ---------------------------------------- (62) Obligation: Innermost TRS: Rules: COND(true, z0) -> c(COND(odd(z0), p(z0)), ODD(z0)) COND(true, z0) -> c1(COND(odd(z0), p(z0)), P(z0)) ODD(0') -> c2 ODD(s(0')) -> c3 ODD(s(s(z0))) -> c4(ODD(z0)) P(0') -> c5 P(s(z0)) -> c6 cond(true, z0) -> cond(odd(z0), p(z0)) odd(0') -> false odd(s(0')) -> true odd(s(s(z0))) -> odd(z0) p(0') -> 0' p(s(z0)) -> z0 Types: COND :: true:false -> 0':s -> c:c1 true :: true:false c :: c:c1 -> c2:c3:c4 -> c:c1 odd :: 0':s -> true:false p :: 0':s -> 0':s ODD :: 0':s -> c2:c3:c4 c1 :: c:c1 -> c5:c6 -> c:c1 P :: 0':s -> c5:c6 0' :: 0':s c2 :: c2:c3:c4 s :: 0':s -> 0':s c3 :: c2:c3:c4 c4 :: c2:c3:c4 -> c2:c3:c4 c5 :: c5:c6 c6 :: c5:c6 cond :: true:false -> 0':s -> cond false :: true:false hole_c:c11_7 :: c:c1 hole_true:false2_7 :: true:false hole_0':s3_7 :: 0':s hole_c2:c3:c44_7 :: c2:c3:c4 hole_c5:c65_7 :: c5:c6 hole_cond6_7 :: cond gen_c:c17_7 :: Nat -> c:c1 gen_0':s8_7 :: Nat -> 0':s gen_c2:c3:c49_7 :: Nat -> c2:c3:c4 Generator Equations: gen_c:c17_7(0) <=> hole_c:c11_7 gen_c:c17_7(+(x, 1)) <=> c(gen_c:c17_7(x), c2) gen_0':s8_7(0) <=> 0' gen_0':s8_7(+(x, 1)) <=> s(gen_0':s8_7(x)) gen_c2:c3:c49_7(0) <=> c2 gen_c2:c3:c49_7(+(x, 1)) <=> c4(gen_c2:c3:c49_7(x)) The following defined symbols remain to be analysed: odd, COND, ODD, cond They will be analysed ascendingly in the following order: odd < COND ODD < COND odd < cond ---------------------------------------- (63) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: odd(gen_0':s8_7(*(2, n11_7))) -> false, rt in Omega(0) Induction Base: odd(gen_0':s8_7(*(2, 0))) ->_R^Omega(0) false Induction Step: odd(gen_0':s8_7(*(2, +(n11_7, 1)))) ->_R^Omega(0) odd(gen_0':s8_7(*(2, n11_7))) ->_IH false We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (64) Obligation: Innermost TRS: Rules: COND(true, z0) -> c(COND(odd(z0), p(z0)), ODD(z0)) COND(true, z0) -> c1(COND(odd(z0), p(z0)), P(z0)) ODD(0') -> c2 ODD(s(0')) -> c3 ODD(s(s(z0))) -> c4(ODD(z0)) P(0') -> c5 P(s(z0)) -> c6 cond(true, z0) -> cond(odd(z0), p(z0)) odd(0') -> false odd(s(0')) -> true odd(s(s(z0))) -> odd(z0) p(0') -> 0' p(s(z0)) -> z0 Types: COND :: true:false -> 0':s -> c:c1 true :: true:false c :: c:c1 -> c2:c3:c4 -> c:c1 odd :: 0':s -> true:false p :: 0':s -> 0':s ODD :: 0':s -> c2:c3:c4 c1 :: c:c1 -> c5:c6 -> c:c1 P :: 0':s -> c5:c6 0' :: 0':s c2 :: c2:c3:c4 s :: 0':s -> 0':s c3 :: c2:c3:c4 c4 :: c2:c3:c4 -> c2:c3:c4 c5 :: c5:c6 c6 :: c5:c6 cond :: true:false -> 0':s -> cond false :: true:false hole_c:c11_7 :: c:c1 hole_true:false2_7 :: true:false hole_0':s3_7 :: 0':s hole_c2:c3:c44_7 :: c2:c3:c4 hole_c5:c65_7 :: c5:c6 hole_cond6_7 :: cond gen_c:c17_7 :: Nat -> c:c1 gen_0':s8_7 :: Nat -> 0':s gen_c2:c3:c49_7 :: Nat -> c2:c3:c4 Lemmas: odd(gen_0':s8_7(*(2, n11_7))) -> false, rt in Omega(0) Generator Equations: gen_c:c17_7(0) <=> hole_c:c11_7 gen_c:c17_7(+(x, 1)) <=> c(gen_c:c17_7(x), c2) gen_0':s8_7(0) <=> 0' gen_0':s8_7(+(x, 1)) <=> s(gen_0':s8_7(x)) gen_c2:c3:c49_7(0) <=> c2 gen_c2:c3:c49_7(+(x, 1)) <=> c4(gen_c2:c3:c49_7(x)) The following defined symbols remain to be analysed: ODD, COND, cond They will be analysed ascendingly in the following order: ODD < COND ---------------------------------------- (65) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: ODD(gen_0':s8_7(*(2, n171_7))) -> gen_c2:c3:c49_7(n171_7), rt in Omega(1 + n171_7) Induction Base: ODD(gen_0':s8_7(*(2, 0))) ->_R^Omega(1) c2 Induction Step: ODD(gen_0':s8_7(*(2, +(n171_7, 1)))) ->_R^Omega(1) c4(ODD(gen_0':s8_7(*(2, n171_7)))) ->_IH c4(gen_c2:c3:c49_7(c172_7)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (66) Complex Obligation (BEST) ---------------------------------------- (67) Obligation: Proved the lower bound n^1 for the following obligation: Innermost TRS: Rules: COND(true, z0) -> c(COND(odd(z0), p(z0)), ODD(z0)) COND(true, z0) -> c1(COND(odd(z0), p(z0)), P(z0)) ODD(0') -> c2 ODD(s(0')) -> c3 ODD(s(s(z0))) -> c4(ODD(z0)) P(0') -> c5 P(s(z0)) -> c6 cond(true, z0) -> cond(odd(z0), p(z0)) odd(0') -> false odd(s(0')) -> true odd(s(s(z0))) -> odd(z0) p(0') -> 0' p(s(z0)) -> z0 Types: COND :: true:false -> 0':s -> c:c1 true :: true:false c :: c:c1 -> c2:c3:c4 -> c:c1 odd :: 0':s -> true:false p :: 0':s -> 0':s ODD :: 0':s -> c2:c3:c4 c1 :: c:c1 -> c5:c6 -> c:c1 P :: 0':s -> c5:c6 0' :: 0':s c2 :: c2:c3:c4 s :: 0':s -> 0':s c3 :: c2:c3:c4 c4 :: c2:c3:c4 -> c2:c3:c4 c5 :: c5:c6 c6 :: c5:c6 cond :: true:false -> 0':s -> cond false :: true:false hole_c:c11_7 :: c:c1 hole_true:false2_7 :: true:false hole_0':s3_7 :: 0':s hole_c2:c3:c44_7 :: c2:c3:c4 hole_c5:c65_7 :: c5:c6 hole_cond6_7 :: cond gen_c:c17_7 :: Nat -> c:c1 gen_0':s8_7 :: Nat -> 0':s gen_c2:c3:c49_7 :: Nat -> c2:c3:c4 Lemmas: odd(gen_0':s8_7(*(2, n11_7))) -> false, rt in Omega(0) Generator Equations: gen_c:c17_7(0) <=> hole_c:c11_7 gen_c:c17_7(+(x, 1)) <=> c(gen_c:c17_7(x), c2) gen_0':s8_7(0) <=> 0' gen_0':s8_7(+(x, 1)) <=> s(gen_0':s8_7(x)) gen_c2:c3:c49_7(0) <=> c2 gen_c2:c3:c49_7(+(x, 1)) <=> c4(gen_c2:c3:c49_7(x)) The following defined symbols remain to be analysed: ODD, COND, cond They will be analysed ascendingly in the following order: ODD < COND ---------------------------------------- (68) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (69) BOUNDS(n^1, INF) ---------------------------------------- (70) Obligation: Innermost TRS: Rules: COND(true, z0) -> c(COND(odd(z0), p(z0)), ODD(z0)) COND(true, z0) -> c1(COND(odd(z0), p(z0)), P(z0)) ODD(0') -> c2 ODD(s(0')) -> c3 ODD(s(s(z0))) -> c4(ODD(z0)) P(0') -> c5 P(s(z0)) -> c6 cond(true, z0) -> cond(odd(z0), p(z0)) odd(0') -> false odd(s(0')) -> true odd(s(s(z0))) -> odd(z0) p(0') -> 0' p(s(z0)) -> z0 Types: COND :: true:false -> 0':s -> c:c1 true :: true:false c :: c:c1 -> c2:c3:c4 -> c:c1 odd :: 0':s -> true:false p :: 0':s -> 0':s ODD :: 0':s -> c2:c3:c4 c1 :: c:c1 -> c5:c6 -> c:c1 P :: 0':s -> c5:c6 0' :: 0':s c2 :: c2:c3:c4 s :: 0':s -> 0':s c3 :: c2:c3:c4 c4 :: c2:c3:c4 -> c2:c3:c4 c5 :: c5:c6 c6 :: c5:c6 cond :: true:false -> 0':s -> cond false :: true:false hole_c:c11_7 :: c:c1 hole_true:false2_7 :: true:false hole_0':s3_7 :: 0':s hole_c2:c3:c44_7 :: c2:c3:c4 hole_c5:c65_7 :: c5:c6 hole_cond6_7 :: cond gen_c:c17_7 :: Nat -> c:c1 gen_0':s8_7 :: Nat -> 0':s gen_c2:c3:c49_7 :: Nat -> c2:c3:c4 Lemmas: odd(gen_0':s8_7(*(2, n11_7))) -> false, rt in Omega(0) ODD(gen_0':s8_7(*(2, n171_7))) -> gen_c2:c3:c49_7(n171_7), rt in Omega(1 + n171_7) Generator Equations: gen_c:c17_7(0) <=> hole_c:c11_7 gen_c:c17_7(+(x, 1)) <=> c(gen_c:c17_7(x), c2) gen_0':s8_7(0) <=> 0' gen_0':s8_7(+(x, 1)) <=> s(gen_0':s8_7(x)) gen_c2:c3:c49_7(0) <=> c2 gen_c2:c3:c49_7(+(x, 1)) <=> c4(gen_c2:c3:c49_7(x)) The following defined symbols remain to be analysed: COND, cond