WORST_CASE(?,O(n^3)) proof of input_U6acDrFo5o.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^3). (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^3)), 166 ms] (8) CdtProblem (9) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (10) CdtProblem (11) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 37 ms] (12) CdtProblem (13) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (14) CdtProblem (15) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 48 ms] (16) CdtProblem (17) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (18) CdtProblem (19) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 39 ms] (20) CdtProblem (21) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (22) CdtProblem (23) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 35 ms] (24) CdtProblem (25) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (26) CdtProblem (27) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 13 ms] (28) CdtProblem (29) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 12 ms] (30) CdtProblem (31) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 13 ms] (32) CdtProblem (33) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 15 ms] (34) CdtProblem (35) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms] (36) BOUNDS(1, 1) ---------------------------------------- (0) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^3). 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)) f_6(x) -> g_6(x, x) g_6(s(x), y) -> b(f_5(y), g_6(x, y)) f_7(x) -> g_7(x, x) g_7(s(x), y) -> b(f_6(y), g_7(x, y)) f_8(x) -> g_8(x, x) g_8(s(x), y) -> b(f_7(y), g_8(x, y)) f_9(x) -> g_9(x, x) g_9(s(x), y) -> b(f_8(y), g_9(x, y)) f_10(x) -> g_10(x, x) g_10(s(x), y) -> b(f_9(y), g_10(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)) f_6(z0) -> g_6(z0, z0) g_6(s(z0), z1) -> b(f_5(z1), g_6(z0, z1)) f_7(z0) -> g_7(z0, z0) g_7(s(z0), z1) -> b(f_6(z1), g_7(z0, z1)) f_8(z0) -> g_8(z0, z0) g_8(s(z0), z1) -> b(f_7(z1), g_8(z0, z1)) f_9(z0) -> g_9(z0, z0) g_9(s(z0), z1) -> b(f_8(z1), g_9(z0, z1)) f_10(z0) -> g_10(z0, z0) g_10(s(z0), z1) -> b(f_9(z1), g_10(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)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) F_10(z0) -> c28(G_10(z0, z0)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(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)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) F_10(z0) -> c28(G_10(z0, z0)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(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, f_6_1, g_6_2, f_7_1, g_7_2, f_8_1, g_8_2, f_9_1, g_9_2, f_10_1, g_10_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, F_6_1, G_6_2, F_7_1, G_7_2, F_8_1, G_8_2, F_9_1, G_9_2, F_10_1, G_10_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, c16_1, c17_1, c18_1, c19_1, c20_1, c21_1, c22_1, c23_1, c24_1, c25_1, c26_1, c27_1, c28_1, c29_1, c30_1 ---------------------------------------- (3) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 1 leading nodes: F_10(z0) -> c28(G_10(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)) f_6(z0) -> g_6(z0, z0) g_6(s(z0), z1) -> b(f_5(z1), g_6(z0, z1)) f_7(z0) -> g_7(z0, z0) g_7(s(z0), z1) -> b(f_6(z1), g_7(z0, z1)) f_8(z0) -> g_8(z0, z0) g_8(s(z0), z1) -> b(f_7(z1), g_8(z0, z1)) f_9(z0) -> g_9(z0, z0) g_9(s(z0), z1) -> b(f_8(z1), g_9(z0, z1)) f_10(z0) -> g_10(z0, z0) g_10(s(z0), z1) -> b(f_9(z1), g_10(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)) 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)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(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)) 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)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(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, f_6_1, g_6_2, f_7_1, g_7_2, f_8_1, g_8_2, f_9_1, g_9_2, f_10_1, g_10_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, F_5_1, G_5_2, F_6_1, G_6_2, F_7_1, G_7_2, F_8_1, G_8_2, F_9_1, G_9_2, G_10_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, c13_1, c14_1, c15_1, c16_1, c17_1, c18_1, c19_1, c20_1, c21_1, c22_1, c23_1, c24_1, c25_1, c26_1, c27_1, c29_1, c30_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)) f_6(z0) -> g_6(z0, z0) g_6(s(z0), z1) -> b(f_5(z1), g_6(z0, z1)) f_7(z0) -> g_7(z0, z0) g_7(s(z0), z1) -> b(f_6(z1), g_7(z0, z1)) f_8(z0) -> g_8(z0, z0) g_8(s(z0), z1) -> b(f_7(z1), g_8(z0, z1)) f_9(z0) -> g_9(z0, z0) g_9(s(z0), z1) -> b(f_8(z1), g_9(z0, z1)) f_10(z0) -> g_10(z0, z0) g_10(s(z0), z1) -> b(f_9(z1), g_10(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)) 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)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(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)) 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)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(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, F_5_1, G_5_2, F_6_1, G_6_2, F_7_1, G_7_2, F_8_1, G_8_2, F_9_1, G_9_2, G_10_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, c13_1, c14_1, c15_1, c16_1, c17_1, c18_1, c19_1, c20_1, c21_1, c22_1, c23_1, c24_1, c25_1, c26_1, c27_1, c29_1, c30_1 ---------------------------------------- (7) CdtRuleRemovalProof (UPPER BOUND(ADD(n^3))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(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)) 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)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(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)) = 0 POL(F_3(x_1)) = 0 POL(F_4(x_1)) = 0 POL(F_5(x_1)) = 0 POL(F_6(x_1)) = 0 POL(F_7(x_1)) = 0 POL(F_8(x_1)) = x_1 + x_1^2 POL(F_9(x_1)) = [1] + x_1 + x_1^2 + x_1^3 POL(G_1(x_1, x_2)) = 0 POL(G_10(x_1, x_2)) = x_1 + x_1*x_2 + x_1^2 + x_1^3 + x_1^2*x_2 + x_1*x_2^2 + x_2^3 POL(G_2(x_1, x_2)) = 0 POL(G_3(x_1, x_2)) = 0 POL(G_4(x_1, x_2)) = 0 POL(G_5(x_1, x_2)) = 0 POL(G_6(x_1, x_2)) = 0 POL(G_7(x_1, x_2)) = 0 POL(G_8(x_1, x_2)) = 0 POL(G_9(x_1, x_2)) = x_2 + x_2^2 + x_1^3 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(c13(x_1)) = x_1 POL(c14(x_1)) = x_1 POL(c15(x_1)) = x_1 POL(c16(x_1)) = x_1 POL(c17(x_1)) = x_1 POL(c18(x_1)) = x_1 POL(c19(x_1)) = x_1 POL(c20(x_1)) = x_1 POL(c21(x_1)) = x_1 POL(c22(x_1)) = x_1 POL(c23(x_1)) = x_1 POL(c24(x_1)) = x_1 POL(c25(x_1)) = x_1 POL(c26(x_1)) = x_1 POL(c27(x_1)) = x_1 POL(c29(x_1)) = x_1 POL(c3(x_1)) = x_1 POL(c30(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)) 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)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(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)) 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)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) K tuples: F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(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, F_5_1, G_5_2, F_6_1, G_6_2, F_7_1, G_7_2, F_8_1, G_8_2, F_9_1, G_9_2, G_10_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, c13_1, c14_1, c15_1, c16_1, c17_1, c18_1, c19_1, c20_1, c21_1, c22_1, c23_1, c24_1, c25_1, c26_1, c27_1, c29_1, c30_1 ---------------------------------------- (9) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: F_8(z0) -> c22(G_8(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)) 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)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(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)) 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)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) K tuples: F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(z0, z1)) F_8(z0) -> c22(G_8(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, F_5_1, G_5_2, F_6_1, G_6_2, F_7_1, G_7_2, F_8_1, G_8_2, F_9_1, G_9_2, G_10_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, c13_1, c14_1, c15_1, c16_1, c17_1, c18_1, c19_1, c20_1, c21_1, c22_1, c23_1, c24_1, c25_1, c26_1, c27_1, c29_1, c30_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_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(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)) 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)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(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)) = 0 POL(F_3(x_1)) = 0 POL(F_4(x_1)) = 0 POL(F_5(x_1)) = 0 POL(F_6(x_1)) = [2] POL(F_7(x_1)) = [2] + x_1 POL(F_8(x_1)) = [3] + [3]x_1 POL(F_9(x_1)) = [3] + [3]x_1 POL(G_1(x_1, x_2)) = 0 POL(G_10(x_1, x_2)) = [3] + [3]x_1 + [3]x_2 POL(G_2(x_1, x_2)) = 0 POL(G_3(x_1, x_2)) = 0 POL(G_4(x_1, x_2)) = 0 POL(G_5(x_1, x_2)) = 0 POL(G_6(x_1, x_2)) = [1] POL(G_7(x_1, x_2)) = [2] + x_1 POL(G_8(x_1, x_2)) = [1] + [2]x_1 + x_2 POL(G_9(x_1, x_2)) = [3] + [3]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(c13(x_1)) = x_1 POL(c14(x_1)) = x_1 POL(c15(x_1)) = x_1 POL(c16(x_1)) = x_1 POL(c17(x_1)) = x_1 POL(c18(x_1)) = x_1 POL(c19(x_1)) = x_1 POL(c20(x_1)) = x_1 POL(c21(x_1)) = x_1 POL(c22(x_1)) = x_1 POL(c23(x_1)) = x_1 POL(c24(x_1)) = x_1 POL(c25(x_1)) = x_1 POL(c26(x_1)) = x_1 POL(c27(x_1)) = x_1 POL(c29(x_1)) = x_1 POL(c3(x_1)) = x_1 POL(c30(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)) = [2] + 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)) 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)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(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)) 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)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) K tuples: F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(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, F_5_1, G_5_2, F_6_1, G_6_2, F_7_1, G_7_2, F_8_1, G_8_2, F_9_1, G_9_2, G_10_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, c13_1, c14_1, c15_1, c16_1, c17_1, c18_1, c19_1, c20_1, c21_1, c22_1, c23_1, c24_1, c25_1, c26_1, c27_1, c29_1, c30_1 ---------------------------------------- (13) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: F_5(z0) -> c13(G_5(z0, z0)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) ---------------------------------------- (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)) 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)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(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)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) K tuples: F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_5(z0) -> c13(G_5(z0, z0)) F_7(z0) -> c19(G_7(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, F_5_1, G_5_2, F_6_1, G_6_2, F_7_1, G_7_2, F_8_1, G_8_2, F_9_1, G_9_2, G_10_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, c13_1, c14_1, c15_1, c16_1, c17_1, c18_1, c19_1, c20_1, c21_1, c22_1, c23_1, c24_1, c25_1, c26_1, c27_1, c29_1, c30_1 ---------------------------------------- (15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. 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)) 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)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(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)) = 0 POL(F_3(x_1)) = 0 POL(F_4(x_1)) = 0 POL(F_5(x_1)) = x_1 POL(F_6(x_1)) = x_1 POL(F_7(x_1)) = x_1 POL(F_8(x_1)) = x_1 POL(F_9(x_1)) = [2]x_1 + [2]x_1^2 POL(G_1(x_1, x_2)) = 0 POL(G_10(x_1, x_2)) = [2]x_2 + [2]x_2^2 + [2]x_1*x_2 POL(G_2(x_1, x_2)) = 0 POL(G_3(x_1, x_2)) = 0 POL(G_4(x_1, x_2)) = 0 POL(G_5(x_1, x_2)) = x_1 POL(G_6(x_1, x_2)) = x_2 POL(G_7(x_1, x_2)) = x_2 POL(G_8(x_1, x_2)) = x_2 POL(G_9(x_1, x_2)) = 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(c13(x_1)) = x_1 POL(c14(x_1)) = x_1 POL(c15(x_1)) = x_1 POL(c16(x_1)) = x_1 POL(c17(x_1)) = x_1 POL(c18(x_1)) = x_1 POL(c19(x_1)) = x_1 POL(c20(x_1)) = x_1 POL(c21(x_1)) = x_1 POL(c22(x_1)) = x_1 POL(c23(x_1)) = x_1 POL(c24(x_1)) = x_1 POL(c25(x_1)) = x_1 POL(c26(x_1)) = x_1 POL(c27(x_1)) = x_1 POL(c29(x_1)) = x_1 POL(c3(x_1)) = x_1 POL(c30(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)) 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)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(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_6(s(z0), z1) -> c18(G_6(z0, z1)) K tuples: F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_5(z0) -> c13(G_5(z0, z0)) F_7(z0) -> c19(G_7(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, F_5_1, G_5_2, F_6_1, G_6_2, F_7_1, G_7_2, F_8_1, G_8_2, F_9_1, G_9_2, G_10_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, c13_1, c14_1, c15_1, c16_1, c17_1, c18_1, c19_1, c20_1, c21_1, c22_1, c23_1, c24_1, c25_1, c26_1, c27_1, c29_1, c30_1 ---------------------------------------- (17) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: F_4(z0) -> c10(G_4(z0, z0)) ---------------------------------------- (18) 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)) 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)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(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)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) K tuples: F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_5(z0) -> c13(G_5(z0, z0)) F_7(z0) -> c19(G_7(z0, z0)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) 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, F_5_1, G_5_2, F_6_1, G_6_2, F_7_1, G_7_2, F_8_1, G_8_2, F_9_1, G_9_2, G_10_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, c13_1, c14_1, c15_1, c16_1, c17_1, c18_1, c19_1, c20_1, c21_1, c22_1, c23_1, c24_1, c25_1, c26_1, c27_1, c29_1, c30_1 ---------------------------------------- (19) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2))) 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)) 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)) 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)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(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)) = x_1 POL(F_3(x_1)) = x_1 POL(F_4(x_1)) = x_1 POL(F_5(x_1)) = x_1 POL(F_6(x_1)) = x_1 POL(F_7(x_1)) = x_1 POL(F_8(x_1)) = x_1 POL(F_9(x_1)) = [2]x_1 + [2]x_1^2 POL(G_1(x_1, x_2)) = [1] POL(G_10(x_1, x_2)) = [2]x_2 + [2]x_2^2 + x_1*x_2 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)) = x_2 POL(G_5(x_1, x_2)) = x_2 POL(G_6(x_1, x_2)) = x_2 POL(G_7(x_1, x_2)) = x_2 POL(G_8(x_1, x_2)) = x_2 POL(G_9(x_1, x_2)) = 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(c13(x_1)) = x_1 POL(c14(x_1)) = x_1 POL(c15(x_1)) = x_1 POL(c16(x_1)) = x_1 POL(c17(x_1)) = x_1 POL(c18(x_1)) = x_1 POL(c19(x_1)) = x_1 POL(c20(x_1)) = x_1 POL(c21(x_1)) = x_1 POL(c22(x_1)) = x_1 POL(c23(x_1)) = x_1 POL(c24(x_1)) = x_1 POL(c25(x_1)) = x_1 POL(c26(x_1)) = x_1 POL(c27(x_1)) = x_1 POL(c29(x_1)) = x_1 POL(c3(x_1)) = x_1 POL(c30(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)) = [2] + x_1 ---------------------------------------- (20) 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)) 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)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(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)) 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)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) K tuples: F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_5(z0) -> c13(G_5(z0, z0)) F_7(z0) -> c19(G_7(z0, z0)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(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, F_5_1, G_5_2, F_6_1, G_6_2, F_7_1, G_7_2, F_8_1, G_8_2, F_9_1, G_9_2, G_10_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, c13_1, c14_1, c15_1, c16_1, c17_1, c18_1, c19_1, c20_1, c21_1, c22_1, c23_1, c24_1, c25_1, c26_1, c27_1, c29_1, c30_1 ---------------------------------------- (21) 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)) ---------------------------------------- (22) 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)) 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)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(z0, z1)) S tuples: G_1(s(z0), z1) -> c3(G_1(z0, z1)) F_2(z0) -> c4(G_2(z0, z0)) 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)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) K tuples: F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_5(z0) -> c13(G_5(z0, z0)) F_7(z0) -> c19(G_7(z0, z0)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_1(z0) -> c1(G_1(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, F_5_1, G_5_2, F_6_1, G_6_2, F_7_1, G_7_2, F_8_1, G_8_2, F_9_1, G_9_2, G_10_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, c13_1, c14_1, c15_1, c16_1, c17_1, c18_1, c19_1, c20_1, c21_1, c22_1, c23_1, c24_1, c25_1, c26_1, c27_1, c29_1, c30_1 ---------------------------------------- (23) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. G_4(s(z0), z1) -> c11(F_3(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)) 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)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(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)) = 0 POL(F_3(x_1)) = 0 POL(F_4(x_1)) = [1] POL(F_5(x_1)) = [1] POL(F_6(x_1)) = [1] POL(F_7(x_1)) = [1] POL(F_8(x_1)) = [2] POL(F_9(x_1)) = [2] + [2]x_1^2 POL(G_1(x_1, x_2)) = 0 POL(G_10(x_1, x_2)) = [2] + [2]x_1 + x_2 + [2]x_2^2 + [2]x_1*x_2 + x_1^2 POL(G_2(x_1, x_2)) = 0 POL(G_3(x_1, x_2)) = 0 POL(G_4(x_1, x_2)) = [1] POL(G_5(x_1, x_2)) = [1] POL(G_6(x_1, x_2)) = [1] POL(G_7(x_1, x_2)) = [1] POL(G_8(x_1, x_2)) = [1] POL(G_9(x_1, x_2)) = [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(c13(x_1)) = x_1 POL(c14(x_1)) = x_1 POL(c15(x_1)) = x_1 POL(c16(x_1)) = x_1 POL(c17(x_1)) = x_1 POL(c18(x_1)) = x_1 POL(c19(x_1)) = x_1 POL(c20(x_1)) = x_1 POL(c21(x_1)) = x_1 POL(c22(x_1)) = x_1 POL(c23(x_1)) = x_1 POL(c24(x_1)) = x_1 POL(c25(x_1)) = x_1 POL(c26(x_1)) = x_1 POL(c27(x_1)) = x_1 POL(c29(x_1)) = x_1 POL(c3(x_1)) = x_1 POL(c30(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)) = x_1 ---------------------------------------- (24) 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)) 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)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(z0, z1)) S tuples: G_1(s(z0), z1) -> c3(G_1(z0, z1)) F_2(z0) -> c4(G_2(z0, z0)) 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)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) K tuples: F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_5(z0) -> c13(G_5(z0, z0)) F_7(z0) -> c19(G_7(z0, z0)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_1(z0) -> c1(G_1(z0, z0)) G_4(s(z0), z1) -> c11(F_3(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, F_5_1, G_5_2, F_6_1, G_6_2, F_7_1, G_7_2, F_8_1, G_8_2, F_9_1, G_9_2, G_10_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, c13_1, c14_1, c15_1, c16_1, c17_1, c18_1, c19_1, c20_1, c21_1, c22_1, c23_1, c24_1, c25_1, c26_1, c27_1, c29_1, c30_1 ---------------------------------------- (25) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: F_3(z0) -> c7(G_3(z0, z0)) ---------------------------------------- (26) 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)) 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)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(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) -> c12(G_4(z0, z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) K tuples: F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_5(z0) -> c13(G_5(z0, z0)) F_7(z0) -> c19(G_7(z0, z0)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_1(z0) -> c1(G_1(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) F_3(z0) -> c7(G_3(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, F_5_1, G_5_2, F_6_1, G_6_2, F_7_1, G_7_2, F_8_1, G_8_2, F_9_1, G_9_2, G_10_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, c13_1, c14_1, c15_1, c16_1, c17_1, c18_1, c19_1, c20_1, c21_1, c22_1, c23_1, c24_1, c25_1, c26_1, c27_1, c29_1, c30_1 ---------------------------------------- (27) 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_6(s(z0), z1) -> c18(G_6(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)) 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)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(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] POL(F_5(x_1)) = [1] POL(F_6(x_1)) = [1] + x_1 POL(F_7(x_1)) = [1] + x_1 POL(F_8(x_1)) = [1] + x_1 POL(F_9(x_1)) = [1] + x_1 POL(G_1(x_1, x_2)) = 0 POL(G_10(x_1, x_2)) = [1] + x_2 POL(G_2(x_1, x_2)) = 0 POL(G_3(x_1, x_2)) = [1] POL(G_4(x_1, x_2)) = [1] POL(G_5(x_1, x_2)) = [1] POL(G_6(x_1, x_2)) = x_1 POL(G_7(x_1, x_2)) = [1] + x_2 POL(G_8(x_1, x_2)) = [1] + x_2 POL(G_9(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(c13(x_1)) = x_1 POL(c14(x_1)) = x_1 POL(c15(x_1)) = x_1 POL(c16(x_1)) = x_1 POL(c17(x_1)) = x_1 POL(c18(x_1)) = x_1 POL(c19(x_1)) = x_1 POL(c20(x_1)) = x_1 POL(c21(x_1)) = x_1 POL(c22(x_1)) = x_1 POL(c23(x_1)) = x_1 POL(c24(x_1)) = x_1 POL(c25(x_1)) = x_1 POL(c26(x_1)) = x_1 POL(c27(x_1)) = x_1 POL(c29(x_1)) = x_1 POL(c3(x_1)) = x_1 POL(c30(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 ---------------------------------------- (28) 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)) 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)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(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)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) K tuples: F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_5(z0) -> c13(G_5(z0, z0)) F_7(z0) -> c19(G_7(z0, z0)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_1(z0) -> c1(G_1(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) F_3(z0) -> c7(G_3(z0, z0)) F_2(z0) -> c4(G_2(z0, z0)) G_6(s(z0), z1) -> c18(G_6(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, F_5_1, G_5_2, F_6_1, G_6_2, F_7_1, G_7_2, F_8_1, G_8_2, F_9_1, G_9_2, G_10_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, c13_1, c14_1, c15_1, c16_1, c17_1, c18_1, c19_1, c20_1, c21_1, c22_1, c23_1, c24_1, c25_1, c26_1, c27_1, c29_1, c30_1 ---------------------------------------- (29) 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_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)) 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)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(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)) = 0 POL(F_3(x_1)) = [1] POL(F_4(x_1)) = [1] + x_1 POL(F_5(x_1)) = [1] + x_1 POL(F_6(x_1)) = [1] + x_1 POL(F_7(x_1)) = [1] + x_1 POL(F_8(x_1)) = [1] + x_1 POL(F_9(x_1)) = [1] + x_1 POL(G_1(x_1, x_2)) = 0 POL(G_10(x_1, x_2)) = x_1 + x_2 POL(G_2(x_1, x_2)) = 0 POL(G_3(x_1, x_2)) = [1] POL(G_4(x_1, x_2)) = x_1 POL(G_5(x_1, x_2)) = [1] + x_2 POL(G_6(x_1, x_2)) = [1] + x_2 POL(G_7(x_1, x_2)) = [1] + x_2 POL(G_8(x_1, x_2)) = [1] + x_2 POL(G_9(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(c13(x_1)) = x_1 POL(c14(x_1)) = x_1 POL(c15(x_1)) = x_1 POL(c16(x_1)) = x_1 POL(c17(x_1)) = x_1 POL(c18(x_1)) = x_1 POL(c19(x_1)) = x_1 POL(c20(x_1)) = x_1 POL(c21(x_1)) = x_1 POL(c22(x_1)) = x_1 POL(c23(x_1)) = x_1 POL(c24(x_1)) = x_1 POL(c25(x_1)) = x_1 POL(c26(x_1)) = x_1 POL(c27(x_1)) = x_1 POL(c29(x_1)) = x_1 POL(c3(x_1)) = x_1 POL(c30(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 ---------------------------------------- (30) 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)) 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)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(z0, z1)) S tuples: G_1(s(z0), z1) -> c3(G_1(z0, z1)) G_3(s(z0), z1) -> c9(G_3(z0, z1)) K tuples: F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_5(z0) -> c13(G_5(z0, z0)) F_7(z0) -> c19(G_7(z0, z0)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_1(z0) -> c1(G_1(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) F_3(z0) -> c7(G_3(z0, z0)) F_2(z0) -> c4(G_2(z0, z0)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) G_3(s(z0), z1) -> c8(F_2(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, F_5_1, G_5_2, F_6_1, G_6_2, F_7_1, G_7_2, F_8_1, G_8_2, F_9_1, G_9_2, G_10_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, c13_1, c14_1, c15_1, c16_1, c17_1, c18_1, c19_1, c20_1, c21_1, c22_1, c23_1, c24_1, c25_1, c26_1, c27_1, c29_1, c30_1 ---------------------------------------- (31) 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)) 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)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(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(F_5(x_1)) = [1] + x_1 POL(F_6(x_1)) = [1] + x_1 POL(F_7(x_1)) = [1] + x_1 POL(F_8(x_1)) = [1] + x_1 POL(F_9(x_1)) = [1] + x_1 POL(G_1(x_1, x_2)) = [1] + x_1 POL(G_10(x_1, x_2)) = [1] + x_2 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(G_6(x_1, x_2)) = [1] + x_2 POL(G_7(x_1, x_2)) = [1] + x_2 POL(G_8(x_1, x_2)) = [1] + x_2 POL(G_9(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(c13(x_1)) = x_1 POL(c14(x_1)) = x_1 POL(c15(x_1)) = x_1 POL(c16(x_1)) = x_1 POL(c17(x_1)) = x_1 POL(c18(x_1)) = x_1 POL(c19(x_1)) = x_1 POL(c20(x_1)) = x_1 POL(c21(x_1)) = x_1 POL(c22(x_1)) = x_1 POL(c23(x_1)) = x_1 POL(c24(x_1)) = x_1 POL(c25(x_1)) = x_1 POL(c26(x_1)) = x_1 POL(c27(x_1)) = x_1 POL(c29(x_1)) = x_1 POL(c3(x_1)) = x_1 POL(c30(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 ---------------------------------------- (32) 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)) 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)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(z0, z1)) S tuples: G_3(s(z0), z1) -> c9(G_3(z0, z1)) K tuples: F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_5(z0) -> c13(G_5(z0, z0)) F_7(z0) -> c19(G_7(z0, z0)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_1(z0) -> c1(G_1(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) F_3(z0) -> c7(G_3(z0, z0)) F_2(z0) -> c4(G_2(z0, z0)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) G_3(s(z0), z1) -> c8(F_2(z1)) G_4(s(z0), z1) -> c12(G_4(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, F_5_1, G_5_2, F_6_1, G_6_2, F_7_1, G_7_2, F_8_1, G_8_2, F_9_1, G_9_2, G_10_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, c13_1, c14_1, c15_1, c16_1, c17_1, c18_1, c19_1, c20_1, c21_1, c22_1, c23_1, c24_1, c25_1, c26_1, c27_1, c29_1, c30_1 ---------------------------------------- (33) 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) -> 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)) 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)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(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)) = 0 POL(F_3(x_1)) = [1] + x_1 POL(F_4(x_1)) = [1] + x_1 POL(F_5(x_1)) = [1] + x_1 POL(F_6(x_1)) = [1] + x_1 POL(F_7(x_1)) = [1] + x_1 POL(F_8(x_1)) = [1] + x_1 POL(F_9(x_1)) = [1] + x_1 POL(G_1(x_1, x_2)) = 0 POL(G_10(x_1, x_2)) = x_1 + x_2 POL(G_2(x_1, x_2)) = 0 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(G_6(x_1, x_2)) = [1] + x_2 POL(G_7(x_1, x_2)) = [1] + x_2 POL(G_8(x_1, x_2)) = [1] + x_2 POL(G_9(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(c13(x_1)) = x_1 POL(c14(x_1)) = x_1 POL(c15(x_1)) = x_1 POL(c16(x_1)) = x_1 POL(c17(x_1)) = x_1 POL(c18(x_1)) = x_1 POL(c19(x_1)) = x_1 POL(c20(x_1)) = x_1 POL(c21(x_1)) = x_1 POL(c22(x_1)) = x_1 POL(c23(x_1)) = x_1 POL(c24(x_1)) = x_1 POL(c25(x_1)) = x_1 POL(c26(x_1)) = x_1 POL(c27(x_1)) = x_1 POL(c29(x_1)) = x_1 POL(c3(x_1)) = x_1 POL(c30(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 ---------------------------------------- (34) 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)) 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)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(z0, z1)) S tuples:none K tuples: F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_5(z0) -> c13(G_5(z0, z0)) F_7(z0) -> c19(G_7(z0, z0)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_1(z0) -> c1(G_1(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) F_3(z0) -> c7(G_3(z0, z0)) F_2(z0) -> c4(G_2(z0, z0)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) G_3(s(z0), z1) -> c8(F_2(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) G_1(s(z0), z1) -> c3(G_1(z0, 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, F_5_1, G_5_2, F_6_1, G_6_2, F_7_1, G_7_2, F_8_1, G_8_2, F_9_1, G_9_2, G_10_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, c13_1, c14_1, c15_1, c16_1, c17_1, c18_1, c19_1, c20_1, c21_1, c22_1, c23_1, c24_1, c25_1, c26_1, c27_1, c29_1, c30_1 ---------------------------------------- (35) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (36) BOUNDS(1, 1)