WORST_CASE(?,O(n^1)) proof of input_QCitfDOhpv.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)), 97 ms] (8) CdtProblem (9) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (10) CdtProblem (11) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 4 ms] (12) CdtProblem (13) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 15 ms] (14) CdtProblem (15) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 0 ms] (16) CdtProblem (17) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms] (18) 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: f_0(x) -> a f_1(x) -> g_1(x, x) g_1(s(x), y) -> b(f_0(y), g_1(x, y)) f_2(x) -> g_2(x, x) g_2(s(x), y) -> b(f_1(y), g_2(x, y)) f_3(x) -> g_3(x, x) g_3(s(x), y) -> b(f_2(y), g_3(x, y)) f_4(x) -> g_4(x, x) g_4(s(x), y) -> b(f_3(y), g_4(x, y)) f_5(x) -> g_5(x, x) g_5(s(x), y) -> b(f_4(y), g_5(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: f_0(z0) -> a f_1(z0) -> g_1(z0, z0) g_1(s(z0), z1) -> b(f_0(z1), g_1(z0, z1)) f_2(z0) -> g_2(z0, z0) g_2(s(z0), z1) -> b(f_1(z1), g_2(z0, z1)) f_3(z0) -> g_3(z0, z0) g_3(s(z0), z1) -> b(f_2(z1), g_3(z0, z1)) f_4(z0) -> g_4(z0, z0) g_4(s(z0), z1) -> b(f_3(z1), g_4(z0, z1)) f_5(z0) -> g_5(z0, z0) g_5(s(z0), z1) -> b(f_4(z1), g_5(z0, z1)) Tuples: F_0(z0) -> c F_1(z0) -> c1(G_1(z0, z0)) G_1(s(z0), z1) -> c2(F_0(z1)) G_1(s(z0), z1) -> c3(G_1(z0, z1)) F_2(z0) -> c4(G_2(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_3(z0) -> c7(G_3(z0, z0)) G_3(s(z0), z1) -> c8(F_2(z1)) G_3(s(z0), z1) -> c9(G_3(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) F_5(z0) -> c13(G_5(z0, z0)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) S tuples: F_0(z0) -> c F_1(z0) -> c1(G_1(z0, z0)) G_1(s(z0), z1) -> c2(F_0(z1)) G_1(s(z0), z1) -> c3(G_1(z0, z1)) F_2(z0) -> c4(G_2(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_3(z0) -> c7(G_3(z0, z0)) G_3(s(z0), z1) -> c8(F_2(z1)) G_3(s(z0), z1) -> c9(G_3(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) F_5(z0) -> c13(G_5(z0, z0)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) K tuples:none Defined Rule Symbols: f_0_1, f_1_1, g_1_2, f_2_1, g_2_2, f_3_1, g_3_2, f_4_1, g_4_2, f_5_1, g_5_2 Defined Pair Symbols: F_0_1, F_1_1, G_1_2, F_2_1, G_2_2, F_3_1, G_3_2, F_4_1, G_4_2, F_5_1, G_5_2 Compound Symbols: c, c1_1, c2_1, c3_1, c4_1, c5_1, c6_1, c7_1, c8_1, c9_1, c10_1, c11_1, c12_1, c13_1, c14_1, c15_1 ---------------------------------------- (3) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 1 leading nodes: F_5(z0) -> c13(G_5(z0, z0)) Removed 2 trailing nodes: G_1(s(z0), z1) -> c2(F_0(z1)) F_0(z0) -> c ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: f_0(z0) -> a f_1(z0) -> g_1(z0, z0) g_1(s(z0), z1) -> b(f_0(z1), g_1(z0, z1)) f_2(z0) -> g_2(z0, z0) g_2(s(z0), z1) -> b(f_1(z1), g_2(z0, z1)) f_3(z0) -> g_3(z0, z0) g_3(s(z0), z1) -> b(f_2(z1), g_3(z0, z1)) f_4(z0) -> g_4(z0, z0) g_4(s(z0), z1) -> b(f_3(z1), g_4(z0, z1)) f_5(z0) -> g_5(z0, z0) g_5(s(z0), z1) -> b(f_4(z1), g_5(z0, z1)) Tuples: F_1(z0) -> c1(G_1(z0, z0)) G_1(s(z0), z1) -> c3(G_1(z0, z1)) F_2(z0) -> c4(G_2(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_3(z0) -> c7(G_3(z0, z0)) G_3(s(z0), z1) -> c8(F_2(z1)) G_3(s(z0), z1) -> c9(G_3(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) S tuples: F_1(z0) -> c1(G_1(z0, z0)) G_1(s(z0), z1) -> c3(G_1(z0, z1)) F_2(z0) -> c4(G_2(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_3(z0) -> c7(G_3(z0, z0)) G_3(s(z0), z1) -> c8(F_2(z1)) G_3(s(z0), z1) -> c9(G_3(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) K tuples:none Defined Rule Symbols: f_0_1, f_1_1, g_1_2, f_2_1, g_2_2, f_3_1, g_3_2, f_4_1, g_4_2, f_5_1, g_5_2 Defined Pair Symbols: F_1_1, G_1_2, F_2_1, G_2_2, F_3_1, G_3_2, F_4_1, G_4_2, G_5_2 Compound Symbols: c1_1, c3_1, c4_1, c5_1, c6_1, c7_1, c8_1, c9_1, c10_1, c11_1, c12_1, c14_1, c15_1 ---------------------------------------- (5) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: f_0(z0) -> a f_1(z0) -> g_1(z0, z0) g_1(s(z0), z1) -> b(f_0(z1), g_1(z0, z1)) f_2(z0) -> g_2(z0, z0) g_2(s(z0), z1) -> b(f_1(z1), g_2(z0, z1)) f_3(z0) -> g_3(z0, z0) g_3(s(z0), z1) -> b(f_2(z1), g_3(z0, z1)) f_4(z0) -> g_4(z0, z0) g_4(s(z0), z1) -> b(f_3(z1), g_4(z0, z1)) f_5(z0) -> g_5(z0, z0) g_5(s(z0), z1) -> b(f_4(z1), g_5(z0, z1)) ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: F_1(z0) -> c1(G_1(z0, z0)) G_1(s(z0), z1) -> c3(G_1(z0, z1)) F_2(z0) -> c4(G_2(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_3(z0) -> c7(G_3(z0, z0)) G_3(s(z0), z1) -> c8(F_2(z1)) G_3(s(z0), z1) -> c9(G_3(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) S tuples: F_1(z0) -> c1(G_1(z0, z0)) G_1(s(z0), z1) -> c3(G_1(z0, z1)) F_2(z0) -> c4(G_2(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_3(z0) -> c7(G_3(z0, z0)) G_3(s(z0), z1) -> c8(F_2(z1)) G_3(s(z0), z1) -> c9(G_3(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) K tuples:none Defined Rule Symbols:none Defined Pair Symbols: F_1_1, G_1_2, F_2_1, G_2_2, F_3_1, G_3_2, F_4_1, G_4_2, G_5_2 Compound Symbols: c1_1, c3_1, c4_1, c5_1, c6_1, c7_1, c8_1, c9_1, c10_1, c11_1, c12_1, c14_1, c15_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. G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_3(z0) -> c7(G_3(z0, z0)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) We considered the (Usable) Rules:none And the Tuples: F_1(z0) -> c1(G_1(z0, z0)) G_1(s(z0), z1) -> c3(G_1(z0, z1)) F_2(z0) -> c4(G_2(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_3(z0) -> c7(G_3(z0, z0)) G_3(s(z0), z1) -> c8(F_2(z1)) G_3(s(z0), z1) -> c9(G_3(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(F_1(x_1)) = 0 POL(F_2(x_1)) = x_1 POL(F_3(x_1)) = [1] + x_1 POL(F_4(x_1)) = [1] + x_1 POL(G_1(x_1, x_2)) = 0 POL(G_2(x_1, x_2)) = x_1 POL(G_3(x_1, x_2)) = x_2 POL(G_4(x_1, x_2)) = [1] + x_2 POL(G_5(x_1, x_2)) = [1] + x_1 + x_2 POL(c1(x_1)) = x_1 POL(c10(x_1)) = x_1 POL(c11(x_1)) = x_1 POL(c12(x_1)) = x_1 POL(c14(x_1)) = x_1 POL(c15(x_1)) = x_1 POL(c3(x_1)) = x_1 POL(c4(x_1)) = x_1 POL(c5(x_1)) = x_1 POL(c6(x_1)) = x_1 POL(c7(x_1)) = x_1 POL(c8(x_1)) = x_1 POL(c9(x_1)) = x_1 POL(s(x_1)) = [1] + x_1 ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: F_1(z0) -> c1(G_1(z0, z0)) G_1(s(z0), z1) -> c3(G_1(z0, z1)) F_2(z0) -> c4(G_2(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_3(z0) -> c7(G_3(z0, z0)) G_3(s(z0), z1) -> c8(F_2(z1)) G_3(s(z0), z1) -> c9(G_3(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) S tuples: F_1(z0) -> c1(G_1(z0, z0)) G_1(s(z0), z1) -> c3(G_1(z0, z1)) F_2(z0) -> c4(G_2(z0, z0)) G_3(s(z0), z1) -> c8(F_2(z1)) G_3(s(z0), z1) -> c9(G_3(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) K tuples: G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_3(z0) -> c7(G_3(z0, z0)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) Defined Rule Symbols:none Defined Pair Symbols: F_1_1, G_1_2, F_2_1, G_2_2, F_3_1, G_3_2, F_4_1, G_4_2, G_5_2 Compound Symbols: c1_1, c3_1, c4_1, c5_1, c6_1, c7_1, c8_1, c9_1, c10_1, c11_1, c12_1, c14_1, c15_1 ---------------------------------------- (9) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: F_1(z0) -> c1(G_1(z0, z0)) F_4(z0) -> c10(G_4(z0, z0)) ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: F_1(z0) -> c1(G_1(z0, z0)) G_1(s(z0), z1) -> c3(G_1(z0, z1)) F_2(z0) -> c4(G_2(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_3(z0) -> c7(G_3(z0, z0)) G_3(s(z0), z1) -> c8(F_2(z1)) G_3(s(z0), z1) -> c9(G_3(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) S tuples: G_1(s(z0), z1) -> c3(G_1(z0, z1)) F_2(z0) -> c4(G_2(z0, z0)) G_3(s(z0), z1) -> c8(F_2(z1)) G_3(s(z0), z1) -> c9(G_3(z0, z1)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) K tuples: G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_3(z0) -> c7(G_3(z0, z0)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) F_1(z0) -> c1(G_1(z0, z0)) F_4(z0) -> c10(G_4(z0, z0)) Defined Rule Symbols:none Defined Pair Symbols: F_1_1, G_1_2, F_2_1, G_2_2, F_3_1, G_3_2, F_4_1, G_4_2, G_5_2 Compound Symbols: c1_1, c3_1, c4_1, c5_1, c6_1, c7_1, c8_1, c9_1, c10_1, c11_1, c12_1, c14_1, c15_1 ---------------------------------------- (11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. F_2(z0) -> c4(G_2(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) We considered the (Usable) Rules:none And the Tuples: F_1(z0) -> c1(G_1(z0, z0)) G_1(s(z0), z1) -> c3(G_1(z0, z1)) F_2(z0) -> c4(G_2(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_3(z0) -> c7(G_3(z0, z0)) G_3(s(z0), z1) -> c8(F_2(z1)) G_3(s(z0), z1) -> c9(G_3(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(F_1(x_1)) = 0 POL(F_2(x_1)) = [1] POL(F_3(x_1)) = [1] POL(F_4(x_1)) = [1] + x_1 POL(G_1(x_1, x_2)) = 0 POL(G_2(x_1, x_2)) = 0 POL(G_3(x_1, x_2)) = [1] POL(G_4(x_1, x_2)) = [1] + x_1 POL(G_5(x_1, x_2)) = x_1 + x_2 POL(c1(x_1)) = x_1 POL(c10(x_1)) = x_1 POL(c11(x_1)) = x_1 POL(c12(x_1)) = x_1 POL(c14(x_1)) = x_1 POL(c15(x_1)) = x_1 POL(c3(x_1)) = x_1 POL(c4(x_1)) = x_1 POL(c5(x_1)) = x_1 POL(c6(x_1)) = x_1 POL(c7(x_1)) = x_1 POL(c8(x_1)) = x_1 POL(c9(x_1)) = x_1 POL(s(x_1)) = [1] + x_1 ---------------------------------------- (12) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: F_1(z0) -> c1(G_1(z0, z0)) G_1(s(z0), z1) -> c3(G_1(z0, z1)) F_2(z0) -> c4(G_2(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_3(z0) -> c7(G_3(z0, z0)) G_3(s(z0), z1) -> c8(F_2(z1)) G_3(s(z0), z1) -> c9(G_3(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) S tuples: G_1(s(z0), z1) -> c3(G_1(z0, z1)) G_3(s(z0), z1) -> c8(F_2(z1)) G_3(s(z0), z1) -> c9(G_3(z0, z1)) K tuples: G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_3(z0) -> c7(G_3(z0, z0)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) F_1(z0) -> c1(G_1(z0, z0)) F_4(z0) -> c10(G_4(z0, z0)) F_2(z0) -> c4(G_2(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) Defined Rule Symbols:none Defined Pair Symbols: F_1_1, G_1_2, F_2_1, G_2_2, F_3_1, G_3_2, F_4_1, G_4_2, G_5_2 Compound Symbols: c1_1, c3_1, c4_1, c5_1, c6_1, c7_1, c8_1, c9_1, c10_1, c11_1, c12_1, c14_1, c15_1 ---------------------------------------- (13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. G_3(s(z0), z1) -> c8(F_2(z1)) G_3(s(z0), z1) -> c9(G_3(z0, z1)) We considered the (Usable) Rules:none And the Tuples: F_1(z0) -> c1(G_1(z0, z0)) G_1(s(z0), z1) -> c3(G_1(z0, z1)) F_2(z0) -> c4(G_2(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_3(z0) -> c7(G_3(z0, z0)) G_3(s(z0), z1) -> c8(F_2(z1)) G_3(s(z0), z1) -> c9(G_3(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(F_1(x_1)) = [1] POL(F_2(x_1)) = [1] POL(F_3(x_1)) = [1] + x_1 POL(F_4(x_1)) = [1] + x_1 POL(G_1(x_1, x_2)) = [1] POL(G_2(x_1, x_2)) = [1] POL(G_3(x_1, x_2)) = [1] + x_1 POL(G_4(x_1, x_2)) = [1] + x_2 POL(G_5(x_1, x_2)) = [1] + x_2 POL(c1(x_1)) = x_1 POL(c10(x_1)) = x_1 POL(c11(x_1)) = x_1 POL(c12(x_1)) = x_1 POL(c14(x_1)) = x_1 POL(c15(x_1)) = x_1 POL(c3(x_1)) = x_1 POL(c4(x_1)) = x_1 POL(c5(x_1)) = x_1 POL(c6(x_1)) = x_1 POL(c7(x_1)) = x_1 POL(c8(x_1)) = x_1 POL(c9(x_1)) = x_1 POL(s(x_1)) = [1] + x_1 ---------------------------------------- (14) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: F_1(z0) -> c1(G_1(z0, z0)) G_1(s(z0), z1) -> c3(G_1(z0, z1)) F_2(z0) -> c4(G_2(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_3(z0) -> c7(G_3(z0, z0)) G_3(s(z0), z1) -> c8(F_2(z1)) G_3(s(z0), z1) -> c9(G_3(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) S tuples: G_1(s(z0), z1) -> c3(G_1(z0, z1)) K tuples: G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_3(z0) -> c7(G_3(z0, z0)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) F_1(z0) -> c1(G_1(z0, z0)) F_4(z0) -> c10(G_4(z0, z0)) F_2(z0) -> c4(G_2(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) G_3(s(z0), z1) -> c8(F_2(z1)) G_3(s(z0), z1) -> c9(G_3(z0, z1)) Defined Rule Symbols:none Defined Pair Symbols: F_1_1, G_1_2, F_2_1, G_2_2, F_3_1, G_3_2, F_4_1, G_4_2, G_5_2 Compound Symbols: c1_1, c3_1, c4_1, c5_1, c6_1, c7_1, c8_1, c9_1, c10_1, c11_1, c12_1, c14_1, c15_1 ---------------------------------------- (15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. G_1(s(z0), z1) -> c3(G_1(z0, z1)) We considered the (Usable) Rules:none And the Tuples: F_1(z0) -> c1(G_1(z0, z0)) G_1(s(z0), z1) -> c3(G_1(z0, z1)) F_2(z0) -> c4(G_2(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_3(z0) -> c7(G_3(z0, z0)) G_3(s(z0), z1) -> c8(F_2(z1)) G_3(s(z0), z1) -> c9(G_3(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(F_1(x_1)) = [1] + x_1 POL(F_2(x_1)) = [1] + x_1 POL(F_3(x_1)) = [1] + x_1 POL(F_4(x_1)) = [1] + x_1 POL(G_1(x_1, x_2)) = [1] + x_1 POL(G_2(x_1, x_2)) = [1] + x_2 POL(G_3(x_1, x_2)) = [1] + x_2 POL(G_4(x_1, x_2)) = [1] + x_2 POL(G_5(x_1, x_2)) = [1] + x_2 POL(c1(x_1)) = x_1 POL(c10(x_1)) = x_1 POL(c11(x_1)) = x_1 POL(c12(x_1)) = x_1 POL(c14(x_1)) = x_1 POL(c15(x_1)) = x_1 POL(c3(x_1)) = x_1 POL(c4(x_1)) = x_1 POL(c5(x_1)) = x_1 POL(c6(x_1)) = x_1 POL(c7(x_1)) = x_1 POL(c8(x_1)) = x_1 POL(c9(x_1)) = x_1 POL(s(x_1)) = [1] + x_1 ---------------------------------------- (16) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: F_1(z0) -> c1(G_1(z0, z0)) G_1(s(z0), z1) -> c3(G_1(z0, z1)) F_2(z0) -> c4(G_2(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_3(z0) -> c7(G_3(z0, z0)) G_3(s(z0), z1) -> c8(F_2(z1)) G_3(s(z0), z1) -> c9(G_3(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) S tuples:none K tuples: G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_3(z0) -> c7(G_3(z0, z0)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) F_1(z0) -> c1(G_1(z0, z0)) F_4(z0) -> c10(G_4(z0, z0)) F_2(z0) -> c4(G_2(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) G_3(s(z0), z1) -> c8(F_2(z1)) G_3(s(z0), z1) -> c9(G_3(z0, z1)) G_1(s(z0), z1) -> c3(G_1(z0, z1)) Defined Rule Symbols:none Defined Pair Symbols: F_1_1, G_1_2, F_2_1, G_2_2, F_3_1, G_3_2, F_4_1, G_4_2, G_5_2 Compound Symbols: c1_1, c3_1, c4_1, c5_1, c6_1, c7_1, c8_1, c9_1, c10_1, c11_1, c12_1, c14_1, c15_1 ---------------------------------------- (17) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (18) BOUNDS(1, 1)