WORST_CASE(?,O(n^1)) proof of input_24nKBIUQN8.trs # AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1). (0) CpxTRS (1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (2) CdtProblem (3) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (4) CdtProblem (5) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CdtProblem (7) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 53 ms] (8) CdtProblem (9) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms] (10) BOUNDS(1, 1) ---------------------------------------- (0) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1). The TRS R consists of the following rules: bin(x, 0) -> s(0) bin(0, s(y)) -> 0 bin(s(x), s(y)) -> +(bin(x, s(y)), bin(x, y)) S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (1) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (2) Obligation: Complexity Dependency Tuples Problem Rules: bin(z0, 0) -> s(0) bin(0, s(z0)) -> 0 bin(s(z0), s(z1)) -> +(bin(z0, s(z1)), bin(z0, z1)) Tuples: 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)) S tuples: 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)) K tuples:none Defined Rule Symbols: bin_2 Defined Pair Symbols: BIN_2 Compound Symbols: c, c1, c2_1, c3_1 ---------------------------------------- (3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 2 trailing nodes: BIN(0, s(z0)) -> c1 BIN(z0, 0) -> c ---------------------------------------- (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)) Tuples: BIN(s(z0), s(z1)) -> c2(BIN(z0, s(z1))) BIN(s(z0), s(z1)) -> c3(BIN(z0, z1)) S tuples: BIN(s(z0), s(z1)) -> c2(BIN(z0, s(z1))) BIN(s(z0), s(z1)) -> c3(BIN(z0, z1)) K tuples:none Defined Rule Symbols: bin_2 Defined Pair Symbols: BIN_2 Compound Symbols: c2_1, c3_1 ---------------------------------------- (5) 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)) ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: BIN(s(z0), s(z1)) -> c2(BIN(z0, s(z1))) BIN(s(z0), s(z1)) -> c3(BIN(z0, z1)) S tuples: BIN(s(z0), s(z1)) -> c2(BIN(z0, s(z1))) BIN(s(z0), s(z1)) -> c3(BIN(z0, z1)) K tuples:none Defined Rule Symbols:none Defined Pair Symbols: BIN_2 Compound Symbols: c2_1, c3_1 ---------------------------------------- (7) 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)) -> c2(BIN(z0, s(z1))) BIN(s(z0), s(z1)) -> c3(BIN(z0, z1)) We considered the (Usable) Rules:none And the Tuples: BIN(s(z0), s(z1)) -> c2(BIN(z0, s(z1))) BIN(s(z0), s(z1)) -> c3(BIN(z0, z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(BIN(x_1, x_2)) = x_1 POL(c2(x_1)) = x_1 POL(c3(x_1)) = x_1 POL(s(x_1)) = [1] + x_1 ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: BIN(s(z0), s(z1)) -> c2(BIN(z0, s(z1))) BIN(s(z0), s(z1)) -> c3(BIN(z0, z1)) S tuples:none K tuples: BIN(s(z0), s(z1)) -> c2(BIN(z0, s(z1))) BIN(s(z0), s(z1)) -> c3(BIN(z0, z1)) Defined Rule Symbols:none Defined Pair Symbols: BIN_2 Compound Symbols: c2_1, c3_1 ---------------------------------------- (9) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (10) BOUNDS(1, 1)