WORST_CASE(?,O(n^1)) proof of input_CNq0TWYTPa.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 [ComplexityIfPolyImplication, 0 ms] (4) CdtProblem (5) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CdtProblem (7) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 48 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: plus_x#1(0, x8) -> x8 plus_x#1(S(x12), x14) -> S(plus_x#1(x12, x14)) map#2(plus_x(x2), Nil) -> Nil map#2(plus_x(x6), Cons(x4, x2)) -> Cons(plus_x#1(x6, x4), map#2(plus_x(x6), x2)) main(x5, x12) -> map#2(plus_x(x12), x5) 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: plus_x#1(0, z0) -> z0 plus_x#1(S(z0), z1) -> S(plus_x#1(z0, z1)) map#2(plus_x(z0), Nil) -> Nil map#2(plus_x(z0), Cons(z1, z2)) -> Cons(plus_x#1(z0, z1), map#2(plus_x(z0), z2)) main(z0, z1) -> map#2(plus_x(z1), z0) Tuples: PLUS_X#1(0, z0) -> c PLUS_X#1(S(z0), z1) -> c1(PLUS_X#1(z0, z1)) MAP#2(plus_x(z0), Nil) -> c2 MAP#2(plus_x(z0), Cons(z1, z2)) -> c3(PLUS_X#1(z0, z1)) MAP#2(plus_x(z0), Cons(z1, z2)) -> c4(MAP#2(plus_x(z0), z2)) MAIN(z0, z1) -> c5(MAP#2(plus_x(z1), z0)) S tuples: PLUS_X#1(0, z0) -> c PLUS_X#1(S(z0), z1) -> c1(PLUS_X#1(z0, z1)) MAP#2(plus_x(z0), Nil) -> c2 MAP#2(plus_x(z0), Cons(z1, z2)) -> c3(PLUS_X#1(z0, z1)) MAP#2(plus_x(z0), Cons(z1, z2)) -> c4(MAP#2(plus_x(z0), z2)) MAIN(z0, z1) -> c5(MAP#2(plus_x(z1), z0)) K tuples:none Defined Rule Symbols: plus_x#1_2, map#2_2, main_2 Defined Pair Symbols: PLUS_X#1_2, MAP#2_2, MAIN_2 Compound Symbols: c, c1_1, c2, c3_1, c4_1, c5_1 ---------------------------------------- (3) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 1 leading nodes: MAIN(z0, z1) -> c5(MAP#2(plus_x(z1), z0)) Removed 2 trailing nodes: MAP#2(plus_x(z0), Nil) -> c2 PLUS_X#1(0, z0) -> c ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: plus_x#1(0, z0) -> z0 plus_x#1(S(z0), z1) -> S(plus_x#1(z0, z1)) map#2(plus_x(z0), Nil) -> Nil map#2(plus_x(z0), Cons(z1, z2)) -> Cons(plus_x#1(z0, z1), map#2(plus_x(z0), z2)) main(z0, z1) -> map#2(plus_x(z1), z0) Tuples: PLUS_X#1(S(z0), z1) -> c1(PLUS_X#1(z0, z1)) MAP#2(plus_x(z0), Cons(z1, z2)) -> c3(PLUS_X#1(z0, z1)) MAP#2(plus_x(z0), Cons(z1, z2)) -> c4(MAP#2(plus_x(z0), z2)) S tuples: PLUS_X#1(S(z0), z1) -> c1(PLUS_X#1(z0, z1)) MAP#2(plus_x(z0), Cons(z1, z2)) -> c3(PLUS_X#1(z0, z1)) MAP#2(plus_x(z0), Cons(z1, z2)) -> c4(MAP#2(plus_x(z0), z2)) K tuples:none Defined Rule Symbols: plus_x#1_2, map#2_2, main_2 Defined Pair Symbols: PLUS_X#1_2, MAP#2_2 Compound Symbols: c1_1, c3_1, c4_1 ---------------------------------------- (5) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: plus_x#1(0, z0) -> z0 plus_x#1(S(z0), z1) -> S(plus_x#1(z0, z1)) map#2(plus_x(z0), Nil) -> Nil map#2(plus_x(z0), Cons(z1, z2)) -> Cons(plus_x#1(z0, z1), map#2(plus_x(z0), z2)) main(z0, z1) -> map#2(plus_x(z1), z0) ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: PLUS_X#1(S(z0), z1) -> c1(PLUS_X#1(z0, z1)) MAP#2(plus_x(z0), Cons(z1, z2)) -> c3(PLUS_X#1(z0, z1)) MAP#2(plus_x(z0), Cons(z1, z2)) -> c4(MAP#2(plus_x(z0), z2)) S tuples: PLUS_X#1(S(z0), z1) -> c1(PLUS_X#1(z0, z1)) MAP#2(plus_x(z0), Cons(z1, z2)) -> c3(PLUS_X#1(z0, z1)) MAP#2(plus_x(z0), Cons(z1, z2)) -> c4(MAP#2(plus_x(z0), z2)) K tuples:none Defined Rule Symbols:none Defined Pair Symbols: PLUS_X#1_2, MAP#2_2 Compound Symbols: c1_1, c3_1, c4_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. PLUS_X#1(S(z0), z1) -> c1(PLUS_X#1(z0, z1)) MAP#2(plus_x(z0), Cons(z1, z2)) -> c3(PLUS_X#1(z0, z1)) MAP#2(plus_x(z0), Cons(z1, z2)) -> c4(MAP#2(plus_x(z0), z2)) We considered the (Usable) Rules:none And the Tuples: PLUS_X#1(S(z0), z1) -> c1(PLUS_X#1(z0, z1)) MAP#2(plus_x(z0), Cons(z1, z2)) -> c3(PLUS_X#1(z0, z1)) MAP#2(plus_x(z0), Cons(z1, z2)) -> c4(MAP#2(plus_x(z0), z2)) The order we found is given by the following interpretation: Polynomial interpretation : POL(Cons(x_1, x_2)) = [3] + x_1 + x_2 POL(MAP#2(x_1, x_2)) = [3] + [2]x_1 + [3]x_2 POL(PLUS_X#1(x_1, x_2)) = [2]x_1 + [3]x_2 POL(S(x_1)) = [3] + x_1 POL(c1(x_1)) = x_1 POL(c3(x_1)) = x_1 POL(c4(x_1)) = x_1 POL(plus_x(x_1)) = [3] + x_1 ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: PLUS_X#1(S(z0), z1) -> c1(PLUS_X#1(z0, z1)) MAP#2(plus_x(z0), Cons(z1, z2)) -> c3(PLUS_X#1(z0, z1)) MAP#2(plus_x(z0), Cons(z1, z2)) -> c4(MAP#2(plus_x(z0), z2)) S tuples:none K tuples: PLUS_X#1(S(z0), z1) -> c1(PLUS_X#1(z0, z1)) MAP#2(plus_x(z0), Cons(z1, z2)) -> c3(PLUS_X#1(z0, z1)) MAP#2(plus_x(z0), Cons(z1, z2)) -> c4(MAP#2(plus_x(z0), z2)) Defined Rule Symbols:none Defined Pair Symbols: PLUS_X#1_2, MAP#2_2 Compound Symbols: c1_1, c3_1, c4_1 ---------------------------------------- (9) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (10) BOUNDS(1, 1)