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), 244 ms] (2) CpxRelTRS (3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (4) CdtProblem (5) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CdtProblem (7) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 1 ms] (8) CdtProblem (9) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 35 ms] (10) CdtProblem (11) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms] (12) BOUNDS(1, 1) (13) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (14) TRS for Loop Detection (15) DecreasingLoopProof [LOWER BOUND(ID), 0 ms] (16) BEST (17) proven lower bound (18) LowerBoundPropagationProof [FINISHED, 0 ms] (19) BOUNDS(n^1, INF) (20) 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: BIN(z0, 0) -> c BIN(0, s(z0)) -> c1 BIN(s(z0), s(z1)) -> c2(BIN(z0, s(z1))) BIN(s(z0), s(z1)) -> c3(BIN(z0, z1)) The (relative) TRS S consists of the following rules: bin(z0, 0) -> s(0) bin(0, s(z0)) -> 0 bin(s(z0), s(z1)) -> +(bin(z0, s(z1)), bin(z0, z1)) 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: BIN(z0, 0) -> c BIN(0, s(z0)) -> c1 BIN(s(z0), s(z1)) -> c2(BIN(z0, s(z1))) BIN(s(z0), s(z1)) -> c3(BIN(z0, z1)) The (relative) TRS S consists of the following rules: bin(z0, 0) -> s(0) bin(0, s(z0)) -> 0 bin(s(z0), s(z1)) -> +(bin(z0, s(z1)), bin(z0, z1)) Rewrite Strategy: INNERMOST ---------------------------------------- (3) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS to CDT ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: bin(z0, 0) -> s(0) bin(0, s(z0)) -> 0 bin(s(z0), s(z1)) -> +(bin(z0, s(z1)), bin(z0, z1)) BIN(z0, 0) -> c BIN(0, s(z0)) -> c1 BIN(s(z0), s(z1)) -> c2(BIN(z0, s(z1))) BIN(s(z0), s(z1)) -> c3(BIN(z0, z1)) Tuples: BIN'(z0, 0) -> c4 BIN'(0, s(z0)) -> c5 BIN'(s(z0), s(z1)) -> c6(BIN'(z0, s(z1)), BIN'(z0, z1)) BIN''(z0, 0) -> c7 BIN''(0, s(z0)) -> c8 BIN''(s(z0), s(z1)) -> c9(BIN''(z0, s(z1))) BIN''(s(z0), s(z1)) -> c10(BIN''(z0, z1)) S tuples: BIN''(z0, 0) -> c7 BIN''(0, s(z0)) -> c8 BIN''(s(z0), s(z1)) -> c9(BIN''(z0, s(z1))) BIN''(s(z0), s(z1)) -> c10(BIN''(z0, z1)) K tuples:none Defined Rule Symbols: BIN_2, bin_2 Defined Pair Symbols: BIN'_2, BIN''_2 Compound Symbols: c4, c5, c6_2, c7, c8, c9_1, c10_1 ---------------------------------------- (5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 4 trailing nodes: BIN''(0, s(z0)) -> c8 BIN''(z0, 0) -> c7 BIN'(0, s(z0)) -> c5 BIN'(z0, 0) -> c4 ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: bin(z0, 0) -> s(0) bin(0, s(z0)) -> 0 bin(s(z0), s(z1)) -> +(bin(z0, s(z1)), bin(z0, z1)) BIN(z0, 0) -> c BIN(0, s(z0)) -> c1 BIN(s(z0), s(z1)) -> c2(BIN(z0, s(z1))) BIN(s(z0), s(z1)) -> c3(BIN(z0, z1)) Tuples: BIN'(s(z0), s(z1)) -> c6(BIN'(z0, s(z1)), BIN'(z0, z1)) BIN''(s(z0), s(z1)) -> c9(BIN''(z0, s(z1))) BIN''(s(z0), s(z1)) -> c10(BIN''(z0, z1)) S tuples: BIN''(s(z0), s(z1)) -> c9(BIN''(z0, s(z1))) BIN''(s(z0), s(z1)) -> c10(BIN''(z0, z1)) K tuples:none Defined Rule Symbols: BIN_2, bin_2 Defined Pair Symbols: BIN'_2, BIN''_2 Compound Symbols: c6_2, c9_1, c10_1 ---------------------------------------- (7) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: bin(z0, 0) -> s(0) bin(0, s(z0)) -> 0 bin(s(z0), s(z1)) -> +(bin(z0, s(z1)), bin(z0, z1)) BIN(z0, 0) -> c BIN(0, s(z0)) -> c1 BIN(s(z0), s(z1)) -> c2(BIN(z0, s(z1))) BIN(s(z0), s(z1)) -> c3(BIN(z0, z1)) ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: BIN'(s(z0), s(z1)) -> c6(BIN'(z0, s(z1)), BIN'(z0, z1)) BIN''(s(z0), s(z1)) -> c9(BIN''(z0, s(z1))) BIN''(s(z0), s(z1)) -> c10(BIN''(z0, z1)) S tuples: BIN''(s(z0), s(z1)) -> c9(BIN''(z0, s(z1))) BIN''(s(z0), s(z1)) -> c10(BIN''(z0, z1)) K tuples:none Defined Rule Symbols:none Defined Pair Symbols: BIN'_2, BIN''_2 Compound Symbols: c6_2, c9_1, c10_1 ---------------------------------------- (9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. BIN''(s(z0), s(z1)) -> c9(BIN''(z0, s(z1))) BIN''(s(z0), s(z1)) -> c10(BIN''(z0, z1)) We considered the (Usable) Rules:none And the Tuples: BIN'(s(z0), s(z1)) -> c6(BIN'(z0, s(z1)), BIN'(z0, z1)) BIN''(s(z0), s(z1)) -> c9(BIN''(z0, s(z1))) BIN''(s(z0), s(z1)) -> c10(BIN''(z0, z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(BIN'(x_1, x_2)) = 0 POL(BIN''(x_1, x_2)) = x_1 POL(c10(x_1)) = x_1 POL(c6(x_1, x_2)) = x_1 + x_2 POL(c9(x_1)) = x_1 POL(s(x_1)) = [1] + x_1 ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: BIN'(s(z0), s(z1)) -> c6(BIN'(z0, s(z1)), BIN'(z0, z1)) BIN''(s(z0), s(z1)) -> c9(BIN''(z0, s(z1))) BIN''(s(z0), s(z1)) -> c10(BIN''(z0, z1)) S tuples:none K tuples: BIN''(s(z0), s(z1)) -> c9(BIN''(z0, s(z1))) BIN''(s(z0), s(z1)) -> c10(BIN''(z0, z1)) Defined Rule Symbols:none Defined Pair Symbols: BIN'_2, BIN''_2 Compound Symbols: c6_2, c9_1, c10_1 ---------------------------------------- (11) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (12) BOUNDS(1, 1) ---------------------------------------- (13) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (14) 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: BIN(z0, 0) -> c BIN(0, s(z0)) -> c1 BIN(s(z0), s(z1)) -> c2(BIN(z0, s(z1))) BIN(s(z0), s(z1)) -> c3(BIN(z0, z1)) The (relative) TRS S consists of the following rules: bin(z0, 0) -> s(0) bin(0, s(z0)) -> 0 bin(s(z0), s(z1)) -> +(bin(z0, s(z1)), bin(z0, z1)) Rewrite Strategy: INNERMOST ---------------------------------------- (15) DecreasingLoopProof (LOWER BOUND(ID)) The following loop(s) give(s) rise to the lower bound Omega(n^1): The rewrite sequence BIN(s(z0), s(z1)) ->^+ c2(BIN(z0, s(z1))) gives rise to a decreasing loop by considering the right hand sides subterm at position [0]. The pumping substitution is [z0 / s(z0)]. The result substitution is [ ]. ---------------------------------------- (16) Complex Obligation (BEST) ---------------------------------------- (17) 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: BIN(z0, 0) -> c BIN(0, s(z0)) -> c1 BIN(s(z0), s(z1)) -> c2(BIN(z0, s(z1))) BIN(s(z0), s(z1)) -> c3(BIN(z0, z1)) The (relative) TRS S consists of the following rules: bin(z0, 0) -> s(0) bin(0, s(z0)) -> 0 bin(s(z0), s(z1)) -> +(bin(z0, s(z1)), bin(z0, z1)) Rewrite Strategy: INNERMOST ---------------------------------------- (18) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (19) BOUNDS(n^1, INF) ---------------------------------------- (20) 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: BIN(z0, 0) -> c BIN(0, s(z0)) -> c1 BIN(s(z0), s(z1)) -> c2(BIN(z0, s(z1))) BIN(s(z0), s(z1)) -> c3(BIN(z0, z1)) The (relative) TRS S consists of the following rules: bin(z0, 0) -> s(0) bin(0, s(z0)) -> 0 bin(s(z0), s(z1)) -> +(bin(z0, s(z1)), bin(z0, z1)) Rewrite Strategy: INNERMOST