WORST_CASE(Omega(n^1),O(n^2)) proof of /export/starexec/sandbox/benchmark/theBenchmark.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, n^2). (0) CpxTRS (1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (2) CdtProblem (3) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (4) CdtProblem (5) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CdtProblem (7) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CdtProblem (9) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (10) CdtProblem (11) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (12) CdtProblem (13) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 35 ms] (14) CdtProblem (15) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 18 ms] (16) CdtProblem (17) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (18) CdtProblem (19) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (20) CdtProblem (21) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 0 ms] (22) CdtProblem (23) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 14 ms] (24) CdtProblem (25) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 2300 ms] (26) CdtProblem (27) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms] (28) BOUNDS(1, 1) (29) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (30) TRS for Loop Detection (31) DecreasingLoopProof [LOWER BOUND(ID), 0 ms] (32) BEST (33) proven lower bound (34) LowerBoundPropagationProof [FINISHED, 0 ms] (35) BOUNDS(n^1, INF) (36) TRS for Loop Detection ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, n^2). The TRS R consists of the following rules: -(x, 0) -> x -(s(x), s(y)) -> -(x, y) p(s(x)) -> x f(s(x), y) -> f(p(-(s(x), y)), p(-(y, s(x)))) f(x, s(y)) -> f(p(-(x, s(y))), p(-(s(y), x))) S is empty. Rewrite Strategy: INNERMOST ---------------------------------------- (1) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS to CDT ---------------------------------------- (2) Obligation: Complexity Dependency Tuples Problem Rules: -(z0, 0) -> z0 -(s(z0), s(z1)) -> -(z0, z1) p(s(z0)) -> z0 f(s(z0), z1) -> f(p(-(s(z0), z1)), p(-(z1, s(z0)))) f(z0, s(z1)) -> f(p(-(z0, s(z1))), p(-(s(z1), z0))) Tuples: -'(z0, 0) -> c -'(s(z0), s(z1)) -> c1(-'(z0, z1)) P(s(z0)) -> c2 F(s(z0), z1) -> c3(F(p(-(s(z0), z1)), p(-(z1, s(z0)))), P(-(s(z0), z1)), -'(s(z0), z1), P(-(z1, s(z0))), -'(z1, s(z0))) F(z0, s(z1)) -> c4(F(p(-(z0, s(z1))), p(-(s(z1), z0))), P(-(z0, s(z1))), -'(z0, s(z1)), P(-(s(z1), z0)), -'(s(z1), z0)) S tuples: -'(z0, 0) -> c -'(s(z0), s(z1)) -> c1(-'(z0, z1)) P(s(z0)) -> c2 F(s(z0), z1) -> c3(F(p(-(s(z0), z1)), p(-(z1, s(z0)))), P(-(s(z0), z1)), -'(s(z0), z1), P(-(z1, s(z0))), -'(z1, s(z0))) F(z0, s(z1)) -> c4(F(p(-(z0, s(z1))), p(-(s(z1), z0))), P(-(z0, s(z1))), -'(z0, s(z1)), P(-(s(z1), z0)), -'(s(z1), z0)) K tuples:none Defined Rule Symbols: -_2, p_1, f_2 Defined Pair Symbols: -'_2, P_1, F_2 Compound Symbols: c, c1_1, c2, c3_5, c4_5 ---------------------------------------- (3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 2 trailing nodes: P(s(z0)) -> c2 -'(z0, 0) -> c ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: -(z0, 0) -> z0 -(s(z0), s(z1)) -> -(z0, z1) p(s(z0)) -> z0 f(s(z0), z1) -> f(p(-(s(z0), z1)), p(-(z1, s(z0)))) f(z0, s(z1)) -> f(p(-(z0, s(z1))), p(-(s(z1), z0))) Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) F(s(z0), z1) -> c3(F(p(-(s(z0), z1)), p(-(z1, s(z0)))), P(-(s(z0), z1)), -'(s(z0), z1), P(-(z1, s(z0))), -'(z1, s(z0))) F(z0, s(z1)) -> c4(F(p(-(z0, s(z1))), p(-(s(z1), z0))), P(-(z0, s(z1))), -'(z0, s(z1)), P(-(s(z1), z0)), -'(s(z1), z0)) S tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) F(s(z0), z1) -> c3(F(p(-(s(z0), z1)), p(-(z1, s(z0)))), P(-(s(z0), z1)), -'(s(z0), z1), P(-(z1, s(z0))), -'(z1, s(z0))) F(z0, s(z1)) -> c4(F(p(-(z0, s(z1))), p(-(s(z1), z0))), P(-(z0, s(z1))), -'(z0, s(z1)), P(-(s(z1), z0)), -'(s(z1), z0)) K tuples:none Defined Rule Symbols: -_2, p_1, f_2 Defined Pair Symbols: -'_2, F_2 Compound Symbols: c1_1, c3_5, c4_5 ---------------------------------------- (5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 4 trailing tuple parts ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: -(z0, 0) -> z0 -(s(z0), s(z1)) -> -(z0, z1) p(s(z0)) -> z0 f(s(z0), z1) -> f(p(-(s(z0), z1)), p(-(z1, s(z0)))) f(z0, s(z1)) -> f(p(-(z0, s(z1))), p(-(s(z1), z0))) Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) F(s(z0), z1) -> c3(F(p(-(s(z0), z1)), p(-(z1, s(z0)))), -'(s(z0), z1), -'(z1, s(z0))) F(z0, s(z1)) -> c4(F(p(-(z0, s(z1))), p(-(s(z1), z0))), -'(z0, s(z1)), -'(s(z1), z0)) S tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) F(s(z0), z1) -> c3(F(p(-(s(z0), z1)), p(-(z1, s(z0)))), -'(s(z0), z1), -'(z1, s(z0))) F(z0, s(z1)) -> c4(F(p(-(z0, s(z1))), p(-(s(z1), z0))), -'(z0, s(z1)), -'(s(z1), z0)) K tuples:none Defined Rule Symbols: -_2, p_1, f_2 Defined Pair Symbols: -'_2, F_2 Compound Symbols: c1_1, c3_3, c4_3 ---------------------------------------- (7) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: f(s(z0), z1) -> f(p(-(s(z0), z1)), p(-(z1, s(z0)))) f(z0, s(z1)) -> f(p(-(z0, s(z1))), p(-(s(z1), z0))) ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules: p(s(z0)) -> z0 -(z0, 0) -> z0 -(s(z0), s(z1)) -> -(z0, z1) Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) F(s(z0), z1) -> c3(F(p(-(s(z0), z1)), p(-(z1, s(z0)))), -'(s(z0), z1), -'(z1, s(z0))) F(z0, s(z1)) -> c4(F(p(-(z0, s(z1))), p(-(s(z1), z0))), -'(z0, s(z1)), -'(s(z1), z0)) S tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) F(s(z0), z1) -> c3(F(p(-(s(z0), z1)), p(-(z1, s(z0)))), -'(s(z0), z1), -'(z1, s(z0))) F(z0, s(z1)) -> c4(F(p(-(z0, s(z1))), p(-(s(z1), z0))), -'(z0, s(z1)), -'(s(z1), z0)) K tuples:none Defined Rule Symbols: p_1, -_2 Defined Pair Symbols: -'_2, F_2 Compound Symbols: c1_1, c3_3, c4_3 ---------------------------------------- (9) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace F(s(z0), z1) -> c3(F(p(-(s(z0), z1)), p(-(z1, s(z0)))), -'(s(z0), z1), -'(z1, s(z0))) by F(s(z1), s(z0)) -> c3(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(s(x0), 0) -> c3(F(p(s(x0)), p(-(0, s(x0)))), -'(s(x0), 0), -'(0, s(x0))) F(s(z0), s(z1)) -> c3(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules: p(s(z0)) -> z0 -(z0, 0) -> z0 -(s(z0), s(z1)) -> -(z0, z1) Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) F(z0, s(z1)) -> c4(F(p(-(z0, s(z1))), p(-(s(z1), z0))), -'(z0, s(z1)), -'(s(z1), z0)) F(s(z1), s(z0)) -> c3(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(s(x0), 0) -> c3(F(p(s(x0)), p(-(0, s(x0)))), -'(s(x0), 0), -'(0, s(x0))) F(s(z0), s(z1)) -> c3(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) S tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) F(z0, s(z1)) -> c4(F(p(-(z0, s(z1))), p(-(s(z1), z0))), -'(z0, s(z1)), -'(s(z1), z0)) F(s(z1), s(z0)) -> c3(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(s(x0), 0) -> c3(F(p(s(x0)), p(-(0, s(x0)))), -'(s(x0), 0), -'(0, s(x0))) F(s(z0), s(z1)) -> c3(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) K tuples:none Defined Rule Symbols: p_1, -_2 Defined Pair Symbols: -'_2, F_2 Compound Symbols: c1_1, c4_3, c3_3 ---------------------------------------- (11) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing nodes: F(s(x0), 0) -> c3(F(p(s(x0)), p(-(0, s(x0)))), -'(s(x0), 0), -'(0, s(x0))) ---------------------------------------- (12) Obligation: Complexity Dependency Tuples Problem Rules: p(s(z0)) -> z0 -(z0, 0) -> z0 -(s(z0), s(z1)) -> -(z0, z1) Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) F(z0, s(z1)) -> c4(F(p(-(z0, s(z1))), p(-(s(z1), z0))), -'(z0, s(z1)), -'(s(z1), z0)) F(s(z1), s(z0)) -> c3(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(s(z0), s(z1)) -> c3(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) S tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) F(z0, s(z1)) -> c4(F(p(-(z0, s(z1))), p(-(s(z1), z0))), -'(z0, s(z1)), -'(s(z1), z0)) F(s(z1), s(z0)) -> c3(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(s(z0), s(z1)) -> c3(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) K tuples:none Defined Rule Symbols: p_1, -_2 Defined Pair Symbols: -'_2, F_2 Compound Symbols: c1_1, c4_3, c3_3 ---------------------------------------- (13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. F(s(z1), s(z0)) -> c3(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) We considered the (Usable) Rules: p(s(z0)) -> z0 -(s(z0), s(z1)) -> -(z0, z1) -(z0, 0) -> z0 And the Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) F(z0, s(z1)) -> c4(F(p(-(z0, s(z1))), p(-(s(z1), z0))), -'(z0, s(z1)), -'(s(z1), z0)) F(s(z1), s(z0)) -> c3(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(s(z0), s(z1)) -> c3(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) The order we found is given by the following interpretation: Polynomial interpretation : POL(-(x_1, x_2)) = x_1 POL(-'(x_1, x_2)) = 0 POL(0) = 0 POL(F(x_1, x_2)) = x_2 POL(c1(x_1)) = x_1 POL(c3(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c4(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(p(x_1)) = x_1 POL(s(x_1)) = [1] + x_1 ---------------------------------------- (14) Obligation: Complexity Dependency Tuples Problem Rules: p(s(z0)) -> z0 -(z0, 0) -> z0 -(s(z0), s(z1)) -> -(z0, z1) Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) F(z0, s(z1)) -> c4(F(p(-(z0, s(z1))), p(-(s(z1), z0))), -'(z0, s(z1)), -'(s(z1), z0)) F(s(z1), s(z0)) -> c3(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(s(z0), s(z1)) -> c3(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) S tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) F(z0, s(z1)) -> c4(F(p(-(z0, s(z1))), p(-(s(z1), z0))), -'(z0, s(z1)), -'(s(z1), z0)) F(s(z0), s(z1)) -> c3(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) K tuples: F(s(z1), s(z0)) -> c3(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) Defined Rule Symbols: p_1, -_2 Defined Pair Symbols: -'_2, F_2 Compound Symbols: c1_1, c4_3, c3_3 ---------------------------------------- (15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. F(s(z0), s(z1)) -> c3(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) We considered the (Usable) Rules: p(s(z0)) -> z0 -(s(z0), s(z1)) -> -(z0, z1) -(z0, 0) -> z0 And the Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) F(z0, s(z1)) -> c4(F(p(-(z0, s(z1))), p(-(s(z1), z0))), -'(z0, s(z1)), -'(s(z1), z0)) F(s(z1), s(z0)) -> c3(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(s(z0), s(z1)) -> c3(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) The order we found is given by the following interpretation: Polynomial interpretation : POL(-(x_1, x_2)) = x_1 POL(-'(x_1, x_2)) = 0 POL(0) = 0 POL(F(x_1, x_2)) = x_1 POL(c1(x_1)) = x_1 POL(c3(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c4(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(p(x_1)) = x_1 POL(s(x_1)) = [1] + x_1 ---------------------------------------- (16) Obligation: Complexity Dependency Tuples Problem Rules: p(s(z0)) -> z0 -(z0, 0) -> z0 -(s(z0), s(z1)) -> -(z0, z1) Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) F(z0, s(z1)) -> c4(F(p(-(z0, s(z1))), p(-(s(z1), z0))), -'(z0, s(z1)), -'(s(z1), z0)) F(s(z1), s(z0)) -> c3(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(s(z0), s(z1)) -> c3(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) S tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) F(z0, s(z1)) -> c4(F(p(-(z0, s(z1))), p(-(s(z1), z0))), -'(z0, s(z1)), -'(s(z1), z0)) K tuples: F(s(z1), s(z0)) -> c3(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(s(z0), s(z1)) -> c3(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) Defined Rule Symbols: p_1, -_2 Defined Pair Symbols: -'_2, F_2 Compound Symbols: c1_1, c4_3, c3_3 ---------------------------------------- (17) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace F(z0, s(z1)) -> c4(F(p(-(z0, s(z1))), p(-(s(z1), z0))), -'(z0, s(z1)), -'(s(z1), z0)) by F(s(z1), s(z0)) -> c4(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(0, s(x1)) -> c4(F(p(-(0, s(x1))), p(s(x1))), -'(0, s(x1)), -'(s(x1), 0)) F(s(z0), s(z1)) -> c4(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) ---------------------------------------- (18) Obligation: Complexity Dependency Tuples Problem Rules: p(s(z0)) -> z0 -(z0, 0) -> z0 -(s(z0), s(z1)) -> -(z0, z1) Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) F(s(z1), s(z0)) -> c3(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(s(z0), s(z1)) -> c3(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) F(s(z1), s(z0)) -> c4(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(0, s(x1)) -> c4(F(p(-(0, s(x1))), p(s(x1))), -'(0, s(x1)), -'(s(x1), 0)) F(s(z0), s(z1)) -> c4(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) S tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) F(s(z1), s(z0)) -> c4(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(0, s(x1)) -> c4(F(p(-(0, s(x1))), p(s(x1))), -'(0, s(x1)), -'(s(x1), 0)) F(s(z0), s(z1)) -> c4(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) K tuples: F(s(z1), s(z0)) -> c3(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(s(z0), s(z1)) -> c3(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) Defined Rule Symbols: p_1, -_2 Defined Pair Symbols: -'_2, F_2 Compound Symbols: c1_1, c3_3, c4_3 ---------------------------------------- (19) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing nodes: F(0, s(x1)) -> c4(F(p(-(0, s(x1))), p(s(x1))), -'(0, s(x1)), -'(s(x1), 0)) ---------------------------------------- (20) Obligation: Complexity Dependency Tuples Problem Rules: p(s(z0)) -> z0 -(z0, 0) -> z0 -(s(z0), s(z1)) -> -(z0, z1) Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) F(s(z1), s(z0)) -> c3(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(s(z0), s(z1)) -> c3(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) F(s(z1), s(z0)) -> c4(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(s(z0), s(z1)) -> c4(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) S tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) F(s(z1), s(z0)) -> c4(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(s(z0), s(z1)) -> c4(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) K tuples: F(s(z1), s(z0)) -> c3(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(s(z0), s(z1)) -> c3(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) Defined Rule Symbols: p_1, -_2 Defined Pair Symbols: -'_2, F_2 Compound Symbols: c1_1, c3_3, c4_3 ---------------------------------------- (21) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. F(s(z0), s(z1)) -> c4(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) We considered the (Usable) Rules: p(s(z0)) -> z0 -(s(z0), s(z1)) -> -(z0, z1) -(z0, 0) -> z0 And the Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) F(s(z1), s(z0)) -> c3(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(s(z0), s(z1)) -> c3(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) F(s(z1), s(z0)) -> c4(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(s(z0), s(z1)) -> c4(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) The order we found is given by the following interpretation: Polynomial interpretation : POL(-(x_1, x_2)) = x_1 POL(-'(x_1, x_2)) = 0 POL(0) = 0 POL(F(x_1, x_2)) = x_1 POL(c1(x_1)) = x_1 POL(c3(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c4(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(p(x_1)) = x_1 POL(s(x_1)) = [1] + x_1 ---------------------------------------- (22) Obligation: Complexity Dependency Tuples Problem Rules: p(s(z0)) -> z0 -(z0, 0) -> z0 -(s(z0), s(z1)) -> -(z0, z1) Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) F(s(z1), s(z0)) -> c3(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(s(z0), s(z1)) -> c3(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) F(s(z1), s(z0)) -> c4(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(s(z0), s(z1)) -> c4(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) S tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) F(s(z1), s(z0)) -> c4(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) K tuples: F(s(z1), s(z0)) -> c3(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(s(z0), s(z1)) -> c3(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) F(s(z0), s(z1)) -> c4(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) Defined Rule Symbols: p_1, -_2 Defined Pair Symbols: -'_2, F_2 Compound Symbols: c1_1, c3_3, c4_3 ---------------------------------------- (23) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. F(s(z1), s(z0)) -> c4(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) We considered the (Usable) Rules: p(s(z0)) -> z0 -(s(z0), s(z1)) -> -(z0, z1) -(z0, 0) -> z0 And the Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) F(s(z1), s(z0)) -> c3(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(s(z0), s(z1)) -> c3(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) F(s(z1), s(z0)) -> c4(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(s(z0), s(z1)) -> c4(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) The order we found is given by the following interpretation: Polynomial interpretation : POL(-(x_1, x_2)) = x_1 POL(-'(x_1, x_2)) = 0 POL(0) = 0 POL(F(x_1, x_2)) = x_2 POL(c1(x_1)) = x_1 POL(c3(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c4(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(p(x_1)) = x_1 POL(s(x_1)) = [1] + x_1 ---------------------------------------- (24) Obligation: Complexity Dependency Tuples Problem Rules: p(s(z0)) -> z0 -(z0, 0) -> z0 -(s(z0), s(z1)) -> -(z0, z1) Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) F(s(z1), s(z0)) -> c3(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(s(z0), s(z1)) -> c3(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) F(s(z1), s(z0)) -> c4(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(s(z0), s(z1)) -> c4(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) S tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) K tuples: F(s(z1), s(z0)) -> c3(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(s(z0), s(z1)) -> c3(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) F(s(z0), s(z1)) -> c4(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) F(s(z1), s(z0)) -> c4(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) Defined Rule Symbols: p_1, -_2 Defined Pair Symbols: -'_2, F_2 Compound Symbols: c1_1, c3_3, c4_3 ---------------------------------------- (25) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. -'(s(z0), s(z1)) -> c1(-'(z0, z1)) We considered the (Usable) Rules: p(s(z0)) -> z0 -(s(z0), s(z1)) -> -(z0, z1) -(z0, 0) -> z0 And the Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) F(s(z1), s(z0)) -> c3(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(s(z0), s(z1)) -> c3(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) F(s(z1), s(z0)) -> c4(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(s(z0), s(z1)) -> c4(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) The order we found is given by the following interpretation: Polynomial interpretation : POL(-(x_1, x_2)) = x_1 POL(-'(x_1, x_2)) = x_1 + x_2 POL(0) = [2] POL(F(x_1, x_2)) = x_2^2 + x_1*x_2 + [2]x_1^2 POL(c1(x_1)) = x_1 POL(c3(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c4(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(p(x_1)) = x_1 POL(s(x_1)) = [2] + x_1 ---------------------------------------- (26) Obligation: Complexity Dependency Tuples Problem Rules: p(s(z0)) -> z0 -(z0, 0) -> z0 -(s(z0), s(z1)) -> -(z0, z1) Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) F(s(z1), s(z0)) -> c3(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(s(z0), s(z1)) -> c3(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) F(s(z1), s(z0)) -> c4(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(s(z0), s(z1)) -> c4(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) S tuples:none K tuples: F(s(z1), s(z0)) -> c3(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) F(s(z0), s(z1)) -> c3(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) F(s(z0), s(z1)) -> c4(F(p(-(z0, z1)), p(-(s(z1), s(z0)))), -'(s(z0), s(z1)), -'(s(z1), s(z0))) F(s(z1), s(z0)) -> c4(F(p(-(s(z1), s(z0))), p(-(z0, z1))), -'(s(z1), s(z0)), -'(s(z0), s(z1))) -'(s(z0), s(z1)) -> c1(-'(z0, z1)) Defined Rule Symbols: p_1, -_2 Defined Pair Symbols: -'_2, F_2 Compound Symbols: c1_1, c3_3, c4_3 ---------------------------------------- (27) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (28) BOUNDS(1, 1) ---------------------------------------- (29) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (30) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, n^2). The TRS R consists of the following rules: -(x, 0) -> x -(s(x), s(y)) -> -(x, y) p(s(x)) -> x f(s(x), y) -> f(p(-(s(x), y)), p(-(y, s(x)))) f(x, s(y)) -> f(p(-(x, s(y))), p(-(s(y), x))) S is empty. Rewrite Strategy: INNERMOST ---------------------------------------- (31) DecreasingLoopProof (LOWER BOUND(ID)) The following loop(s) give(s) rise to the lower bound Omega(n^1): The rewrite sequence -(s(x), s(y)) ->^+ -(x, y) gives rise to a decreasing loop by considering the right hand sides subterm at position []. The pumping substitution is [x / s(x), y / s(y)]. The result substitution is [ ]. ---------------------------------------- (32) Complex Obligation (BEST) ---------------------------------------- (33) Obligation: Proved the lower bound n^1 for the following obligation: The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, n^2). The TRS R consists of the following rules: -(x, 0) -> x -(s(x), s(y)) -> -(x, y) p(s(x)) -> x f(s(x), y) -> f(p(-(s(x), y)), p(-(y, s(x)))) f(x, s(y)) -> f(p(-(x, s(y))), p(-(s(y), x))) S is empty. Rewrite Strategy: INNERMOST ---------------------------------------- (34) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (35) BOUNDS(n^1, INF) ---------------------------------------- (36) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, n^2). The TRS R consists of the following rules: -(x, 0) -> x -(s(x), s(y)) -> -(x, y) p(s(x)) -> x f(s(x), y) -> f(p(-(s(x), y)), p(-(y, s(x)))) f(x, s(y)) -> f(p(-(x, s(y))), p(-(s(y), x))) S is empty. Rewrite Strategy: INNERMOST