WORST_CASE(Omega(n^1),O(n^1)) 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^1). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 285 ms] (2) CpxRelTRS (3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (4) CdtProblem (5) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms] (6) CdtProblem (7) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CdtProblem (9) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (10) CdtProblem (11) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 15 ms] (12) CdtProblem (13) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms] (14) BOUNDS(1, 1) (15) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (16) TRS for Loop Detection (17) DecreasingLoopProof [LOWER BOUND(ID), 0 ms] (18) BEST (19) proven lower bound (20) LowerBoundPropagationProof [FINISHED, 0 ms] (21) BOUNDS(n^1, INF) (22) 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: PRIME(0) -> c PRIME(s(0)) -> c1 PRIME(s(s(z0))) -> c2(PRIME1(s(s(z0)), s(z0))) PRIME1(z0, 0) -> c3 PRIME1(z0, s(0)) -> c4 PRIME1(z0, s(s(z1))) -> c5(DIVP(s(s(z1)), z0)) PRIME1(z0, s(s(z1))) -> c6(PRIME1(z0, s(z1))) DIVP(z0, z1) -> c7 The (relative) TRS S consists of the following rules: prime(0) -> false prime(s(0)) -> false prime(s(s(z0))) -> prime1(s(s(z0)), s(z0)) prime1(z0, 0) -> false prime1(z0, s(0)) -> true prime1(z0, s(s(z1))) -> and(not(divp(s(s(z1)), z0)), prime1(z0, s(z1))) divp(z0, z1) -> =(rem(z0, z1), 0) 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: PRIME(0) -> c PRIME(s(0)) -> c1 PRIME(s(s(z0))) -> c2(PRIME1(s(s(z0)), s(z0))) PRIME1(z0, 0) -> c3 PRIME1(z0, s(0)) -> c4 PRIME1(z0, s(s(z1))) -> c5(DIVP(s(s(z1)), z0)) PRIME1(z0, s(s(z1))) -> c6(PRIME1(z0, s(z1))) DIVP(z0, z1) -> c7 The (relative) TRS S consists of the following rules: prime(0) -> false prime(s(0)) -> false prime(s(s(z0))) -> prime1(s(s(z0)), s(z0)) prime1(z0, 0) -> false prime1(z0, s(0)) -> true prime1(z0, s(s(z1))) -> and(not(divp(s(s(z1)), z0)), prime1(z0, s(z1))) divp(z0, z1) -> =(rem(z0, z1), 0) Rewrite Strategy: INNERMOST ---------------------------------------- (3) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS to CDT ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: prime(0) -> false prime(s(0)) -> false prime(s(s(z0))) -> prime1(s(s(z0)), s(z0)) prime1(z0, 0) -> false prime1(z0, s(0)) -> true prime1(z0, s(s(z1))) -> and(not(divp(s(s(z1)), z0)), prime1(z0, s(z1))) divp(z0, z1) -> =(rem(z0, z1), 0) PRIME(0) -> c PRIME(s(0)) -> c1 PRIME(s(s(z0))) -> c2(PRIME1(s(s(z0)), s(z0))) PRIME1(z0, 0) -> c3 PRIME1(z0, s(0)) -> c4 PRIME1(z0, s(s(z1))) -> c5(DIVP(s(s(z1)), z0)) PRIME1(z0, s(s(z1))) -> c6(PRIME1(z0, s(z1))) DIVP(z0, z1) -> c7 Tuples: PRIME'(0) -> c8 PRIME'(s(0)) -> c9 PRIME'(s(s(z0))) -> c10(PRIME1'(s(s(z0)), s(z0))) PRIME1'(z0, 0) -> c11 PRIME1'(z0, s(0)) -> c12 PRIME1'(z0, s(s(z1))) -> c13(DIVP'(s(s(z1)), z0), PRIME1'(z0, s(z1))) DIVP'(z0, z1) -> c14 PRIME''(0) -> c15 PRIME''(s(0)) -> c16 PRIME''(s(s(z0))) -> c17(PRIME1''(s(s(z0)), s(z0))) PRIME1''(z0, 0) -> c18 PRIME1''(z0, s(0)) -> c19 PRIME1''(z0, s(s(z1))) -> c20(DIVP''(s(s(z1)), z0)) PRIME1''(z0, s(s(z1))) -> c21(PRIME1''(z0, s(z1))) DIVP''(z0, z1) -> c22 S tuples: PRIME''(0) -> c15 PRIME''(s(0)) -> c16 PRIME''(s(s(z0))) -> c17(PRIME1''(s(s(z0)), s(z0))) PRIME1''(z0, 0) -> c18 PRIME1''(z0, s(0)) -> c19 PRIME1''(z0, s(s(z1))) -> c20(DIVP''(s(s(z1)), z0)) PRIME1''(z0, s(s(z1))) -> c21(PRIME1''(z0, s(z1))) DIVP''(z0, z1) -> c22 K tuples:none Defined Rule Symbols: PRIME_1, PRIME1_2, DIVP_2, prime_1, prime1_2, divp_2 Defined Pair Symbols: PRIME'_1, PRIME1'_2, DIVP'_2, PRIME''_1, PRIME1''_2, DIVP''_2 Compound Symbols: c8, c9, c10_1, c11, c12, c13_2, c14, c15, c16, c17_1, c18, c19, c20_1, c21_1, c22 ---------------------------------------- (5) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 2 leading nodes: PRIME'(s(s(z0))) -> c10(PRIME1'(s(s(z0)), s(z0))) PRIME''(s(s(z0))) -> c17(PRIME1''(s(s(z0)), s(z0))) Removed 11 trailing nodes: DIVP'(z0, z1) -> c14 PRIME1''(z0, s(0)) -> c19 PRIME'(s(0)) -> c9 DIVP''(z0, z1) -> c22 PRIME''(s(0)) -> c16 PRIME1'(z0, s(0)) -> c12 PRIME''(0) -> c15 PRIME1'(z0, 0) -> c11 PRIME1''(z0, s(s(z1))) -> c20(DIVP''(s(s(z1)), z0)) PRIME1''(z0, 0) -> c18 PRIME'(0) -> c8 ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: prime(0) -> false prime(s(0)) -> false prime(s(s(z0))) -> prime1(s(s(z0)), s(z0)) prime1(z0, 0) -> false prime1(z0, s(0)) -> true prime1(z0, s(s(z1))) -> and(not(divp(s(s(z1)), z0)), prime1(z0, s(z1))) divp(z0, z1) -> =(rem(z0, z1), 0) PRIME(0) -> c PRIME(s(0)) -> c1 PRIME(s(s(z0))) -> c2(PRIME1(s(s(z0)), s(z0))) PRIME1(z0, 0) -> c3 PRIME1(z0, s(0)) -> c4 PRIME1(z0, s(s(z1))) -> c5(DIVP(s(s(z1)), z0)) PRIME1(z0, s(s(z1))) -> c6(PRIME1(z0, s(z1))) DIVP(z0, z1) -> c7 Tuples: PRIME1'(z0, s(s(z1))) -> c13(DIVP'(s(s(z1)), z0), PRIME1'(z0, s(z1))) PRIME1''(z0, s(s(z1))) -> c21(PRIME1''(z0, s(z1))) S tuples: PRIME1''(z0, s(s(z1))) -> c21(PRIME1''(z0, s(z1))) K tuples:none Defined Rule Symbols: PRIME_1, PRIME1_2, DIVP_2, prime_1, prime1_2, divp_2 Defined Pair Symbols: PRIME1'_2, PRIME1''_2 Compound Symbols: c13_2, c21_1 ---------------------------------------- (7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing tuple parts ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules: prime(0) -> false prime(s(0)) -> false prime(s(s(z0))) -> prime1(s(s(z0)), s(z0)) prime1(z0, 0) -> false prime1(z0, s(0)) -> true prime1(z0, s(s(z1))) -> and(not(divp(s(s(z1)), z0)), prime1(z0, s(z1))) divp(z0, z1) -> =(rem(z0, z1), 0) PRIME(0) -> c PRIME(s(0)) -> c1 PRIME(s(s(z0))) -> c2(PRIME1(s(s(z0)), s(z0))) PRIME1(z0, 0) -> c3 PRIME1(z0, s(0)) -> c4 PRIME1(z0, s(s(z1))) -> c5(DIVP(s(s(z1)), z0)) PRIME1(z0, s(s(z1))) -> c6(PRIME1(z0, s(z1))) DIVP(z0, z1) -> c7 Tuples: PRIME1''(z0, s(s(z1))) -> c21(PRIME1''(z0, s(z1))) PRIME1'(z0, s(s(z1))) -> c13(PRIME1'(z0, s(z1))) S tuples: PRIME1''(z0, s(s(z1))) -> c21(PRIME1''(z0, s(z1))) K tuples:none Defined Rule Symbols: PRIME_1, PRIME1_2, DIVP_2, prime_1, prime1_2, divp_2 Defined Pair Symbols: PRIME1''_2, PRIME1'_2 Compound Symbols: c21_1, c13_1 ---------------------------------------- (9) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: prime(0) -> false prime(s(0)) -> false prime(s(s(z0))) -> prime1(s(s(z0)), s(z0)) prime1(z0, 0) -> false prime1(z0, s(0)) -> true prime1(z0, s(s(z1))) -> and(not(divp(s(s(z1)), z0)), prime1(z0, s(z1))) divp(z0, z1) -> =(rem(z0, z1), 0) PRIME(0) -> c PRIME(s(0)) -> c1 PRIME(s(s(z0))) -> c2(PRIME1(s(s(z0)), s(z0))) PRIME1(z0, 0) -> c3 PRIME1(z0, s(0)) -> c4 PRIME1(z0, s(s(z1))) -> c5(DIVP(s(s(z1)), z0)) PRIME1(z0, s(s(z1))) -> c6(PRIME1(z0, s(z1))) DIVP(z0, z1) -> c7 ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: PRIME1''(z0, s(s(z1))) -> c21(PRIME1''(z0, s(z1))) PRIME1'(z0, s(s(z1))) -> c13(PRIME1'(z0, s(z1))) S tuples: PRIME1''(z0, s(s(z1))) -> c21(PRIME1''(z0, s(z1))) K tuples:none Defined Rule Symbols:none Defined Pair Symbols: PRIME1''_2, PRIME1'_2 Compound Symbols: c21_1, c13_1 ---------------------------------------- (11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. PRIME1''(z0, s(s(z1))) -> c21(PRIME1''(z0, s(z1))) We considered the (Usable) Rules:none And the Tuples: PRIME1''(z0, s(s(z1))) -> c21(PRIME1''(z0, s(z1))) PRIME1'(z0, s(s(z1))) -> c13(PRIME1'(z0, s(z1))) The order we found is given by the following interpretation: Polynomial interpretation : POL(PRIME1'(x_1, x_2)) = 0 POL(PRIME1''(x_1, x_2)) = x_2 POL(c13(x_1)) = x_1 POL(c21(x_1)) = x_1 POL(s(x_1)) = [1] + x_1 ---------------------------------------- (12) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: PRIME1''(z0, s(s(z1))) -> c21(PRIME1''(z0, s(z1))) PRIME1'(z0, s(s(z1))) -> c13(PRIME1'(z0, s(z1))) S tuples:none K tuples: PRIME1''(z0, s(s(z1))) -> c21(PRIME1''(z0, s(z1))) Defined Rule Symbols:none Defined Pair Symbols: PRIME1''_2, PRIME1'_2 Compound Symbols: c21_1, c13_1 ---------------------------------------- (13) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (14) BOUNDS(1, 1) ---------------------------------------- (15) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (16) 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: PRIME(0) -> c PRIME(s(0)) -> c1 PRIME(s(s(z0))) -> c2(PRIME1(s(s(z0)), s(z0))) PRIME1(z0, 0) -> c3 PRIME1(z0, s(0)) -> c4 PRIME1(z0, s(s(z1))) -> c5(DIVP(s(s(z1)), z0)) PRIME1(z0, s(s(z1))) -> c6(PRIME1(z0, s(z1))) DIVP(z0, z1) -> c7 The (relative) TRS S consists of the following rules: prime(0) -> false prime(s(0)) -> false prime(s(s(z0))) -> prime1(s(s(z0)), s(z0)) prime1(z0, 0) -> false prime1(z0, s(0)) -> true prime1(z0, s(s(z1))) -> and(not(divp(s(s(z1)), z0)), prime1(z0, s(z1))) divp(z0, z1) -> =(rem(z0, z1), 0) Rewrite Strategy: INNERMOST ---------------------------------------- (17) DecreasingLoopProof (LOWER BOUND(ID)) The following loop(s) give(s) rise to the lower bound Omega(n^1): The rewrite sequence PRIME1(z0, s(s(z1))) ->^+ c6(PRIME1(z0, s(z1))) gives rise to a decreasing loop by considering the right hand sides subterm at position [0]. The pumping substitution is [z1 / s(z1)]. The result substitution is [ ]. ---------------------------------------- (18) Complex Obligation (BEST) ---------------------------------------- (19) 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: PRIME(0) -> c PRIME(s(0)) -> c1 PRIME(s(s(z0))) -> c2(PRIME1(s(s(z0)), s(z0))) PRIME1(z0, 0) -> c3 PRIME1(z0, s(0)) -> c4 PRIME1(z0, s(s(z1))) -> c5(DIVP(s(s(z1)), z0)) PRIME1(z0, s(s(z1))) -> c6(PRIME1(z0, s(z1))) DIVP(z0, z1) -> c7 The (relative) TRS S consists of the following rules: prime(0) -> false prime(s(0)) -> false prime(s(s(z0))) -> prime1(s(s(z0)), s(z0)) prime1(z0, 0) -> false prime1(z0, s(0)) -> true prime1(z0, s(s(z1))) -> and(not(divp(s(s(z1)), z0)), prime1(z0, s(z1))) divp(z0, z1) -> =(rem(z0, z1), 0) Rewrite Strategy: INNERMOST ---------------------------------------- (20) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (21) BOUNDS(n^1, INF) ---------------------------------------- (22) 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: PRIME(0) -> c PRIME(s(0)) -> c1 PRIME(s(s(z0))) -> c2(PRIME1(s(s(z0)), s(z0))) PRIME1(z0, 0) -> c3 PRIME1(z0, s(0)) -> c4 PRIME1(z0, s(s(z1))) -> c5(DIVP(s(s(z1)), z0)) PRIME1(z0, s(s(z1))) -> c6(PRIME1(z0, s(z1))) DIVP(z0, z1) -> c7 The (relative) TRS S consists of the following rules: prime(0) -> false prime(s(0)) -> false prime(s(s(z0))) -> prime1(s(s(z0)), s(z0)) prime1(z0, 0) -> false prime1(z0, s(0)) -> true prime1(z0, s(s(z1))) -> and(not(divp(s(s(z1)), z0)), prime1(z0, s(z1))) divp(z0, z1) -> =(rem(z0, z1), 0) Rewrite Strategy: INNERMOST