WORST_CASE(?,O(n^1)) proof of input_q0Z8g6J9g0.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)), 56 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: *(x, +(y, z)) -> +(*(x, y), *(x, z)) *(+(x, y), z) -> +(*(x, z), *(y, z)) *(x, 1) -> x *(1, y) -> 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: *(z0, +(z1, z2)) -> +(*(z0, z1), *(z0, z2)) *(+(z0, z1), z2) -> +(*(z0, z2), *(z1, z2)) *(z0, 1) -> z0 *(1, z0) -> z0 Tuples: *'(z0, +(z1, z2)) -> c(*'(z0, z1)) *'(z0, +(z1, z2)) -> c1(*'(z0, z2)) *'(+(z0, z1), z2) -> c2(*'(z0, z2)) *'(+(z0, z1), z2) -> c3(*'(z1, z2)) *'(z0, 1) -> c4 *'(1, z0) -> c5 S tuples: *'(z0, +(z1, z2)) -> c(*'(z0, z1)) *'(z0, +(z1, z2)) -> c1(*'(z0, z2)) *'(+(z0, z1), z2) -> c2(*'(z0, z2)) *'(+(z0, z1), z2) -> c3(*'(z1, z2)) *'(z0, 1) -> c4 *'(1, z0) -> c5 K tuples:none Defined Rule Symbols: *_2 Defined Pair Symbols: *'_2 Compound Symbols: c_1, c1_1, c2_1, c3_1, c4, c5 ---------------------------------------- (3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 2 trailing nodes: *'(z0, 1) -> c4 *'(1, z0) -> c5 ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: *(z0, +(z1, z2)) -> +(*(z0, z1), *(z0, z2)) *(+(z0, z1), z2) -> +(*(z0, z2), *(z1, z2)) *(z0, 1) -> z0 *(1, z0) -> z0 Tuples: *'(z0, +(z1, z2)) -> c(*'(z0, z1)) *'(z0, +(z1, z2)) -> c1(*'(z0, z2)) *'(+(z0, z1), z2) -> c2(*'(z0, z2)) *'(+(z0, z1), z2) -> c3(*'(z1, z2)) S tuples: *'(z0, +(z1, z2)) -> c(*'(z0, z1)) *'(z0, +(z1, z2)) -> c1(*'(z0, z2)) *'(+(z0, z1), z2) -> c2(*'(z0, z2)) *'(+(z0, z1), z2) -> c3(*'(z1, z2)) K tuples:none Defined Rule Symbols: *_2 Defined Pair Symbols: *'_2 Compound Symbols: c_1, c1_1, c2_1, c3_1 ---------------------------------------- (5) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: *(z0, +(z1, z2)) -> +(*(z0, z1), *(z0, z2)) *(+(z0, z1), z2) -> +(*(z0, z2), *(z1, z2)) *(z0, 1) -> z0 *(1, z0) -> z0 ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: *'(z0, +(z1, z2)) -> c(*'(z0, z1)) *'(z0, +(z1, z2)) -> c1(*'(z0, z2)) *'(+(z0, z1), z2) -> c2(*'(z0, z2)) *'(+(z0, z1), z2) -> c3(*'(z1, z2)) S tuples: *'(z0, +(z1, z2)) -> c(*'(z0, z1)) *'(z0, +(z1, z2)) -> c1(*'(z0, z2)) *'(+(z0, z1), z2) -> c2(*'(z0, z2)) *'(+(z0, z1), z2) -> c3(*'(z1, z2)) K tuples:none Defined Rule Symbols:none Defined Pair Symbols: *'_2 Compound Symbols: c_1, c1_1, 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. *'(z0, +(z1, z2)) -> c(*'(z0, z1)) *'(z0, +(z1, z2)) -> c1(*'(z0, z2)) *'(+(z0, z1), z2) -> c2(*'(z0, z2)) *'(+(z0, z1), z2) -> c3(*'(z1, z2)) We considered the (Usable) Rules:none And the Tuples: *'(z0, +(z1, z2)) -> c(*'(z0, z1)) *'(z0, +(z1, z2)) -> c1(*'(z0, z2)) *'(+(z0, z1), z2) -> c2(*'(z0, z2)) *'(+(z0, z1), z2) -> c3(*'(z1, z2)) The order we found is given by the following interpretation: Polynomial interpretation : POL(*'(x_1, x_2)) = x_1 + x_2 POL(+(x_1, x_2)) = [1] + x_1 + x_2 POL(c(x_1)) = x_1 POL(c1(x_1)) = x_1 POL(c2(x_1)) = x_1 POL(c3(x_1)) = x_1 ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: *'(z0, +(z1, z2)) -> c(*'(z0, z1)) *'(z0, +(z1, z2)) -> c1(*'(z0, z2)) *'(+(z0, z1), z2) -> c2(*'(z0, z2)) *'(+(z0, z1), z2) -> c3(*'(z1, z2)) S tuples:none K tuples: *'(z0, +(z1, z2)) -> c(*'(z0, z1)) *'(z0, +(z1, z2)) -> c1(*'(z0, z2)) *'(+(z0, z1), z2) -> c2(*'(z0, z2)) *'(+(z0, z1), z2) -> c3(*'(z1, z2)) Defined Rule Symbols:none Defined Pair Symbols: *'_2 Compound Symbols: c_1, c1_1, c2_1, c3_1 ---------------------------------------- (9) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (10) BOUNDS(1, 1)