WORST_CASE(?,O(n^2)) proof of input_SXdjFkPouG.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^2). (0) CpxTRS (1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (2) CdtProblem (3) CdtLeafRemovalProof [ComplexityIfPolyImplication, 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) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 151 ms] (10) CdtProblem (11) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (12) CdtProblem (13) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (14) CdtProblem (15) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 29 ms] (16) CdtProblem (17) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 24 ms] (18) CdtProblem (19) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 26 ms] (20) CdtProblem (21) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (22) CdtProblem (23) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (24) CdtProblem (25) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 23 ms] (26) CdtProblem (27) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 17 ms] (28) CdtProblem (29) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (30) CdtProblem (31) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (32) CdtProblem (33) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (34) CdtProblem (35) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (36) CdtProblem (37) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 5 ms] (38) CdtProblem (39) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (40) CdtProblem (41) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (42) CdtProblem (43) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 34 ms] (44) CdtProblem (45) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 307 ms] (46) CdtProblem (47) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms] (48) BOUNDS(1, 1) ---------------------------------------- (0) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2). The TRS R consists of the following rules: -(x, 0) -> x -(s(x), s(y)) -> -(x, y) *(x, 0) -> 0 *(x, s(y)) -> +(*(x, y), x) if(true, x, y) -> x if(false, x, y) -> y odd(0) -> false odd(s(0)) -> true odd(s(s(x))) -> odd(x) half(0) -> 0 half(s(0)) -> 0 half(s(s(x))) -> s(half(x)) if(true, x, y) -> true if(false, x, y) -> false pow(x, y) -> f(x, y, s(0)) f(x, 0, z) -> z f(x, s(y), z) -> if(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z)) S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (1) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (2) Obligation: Complexity Dependency Tuples Problem Rules: -(z0, 0) -> z0 -(s(z0), s(z1)) -> -(z0, z1) *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) if(true, z0, z1) -> z0 if(false, z0, z1) -> z1 if(true, z0, z1) -> true if(false, z0, z1) -> false odd(0) -> false odd(s(0)) -> true odd(s(s(z0))) -> odd(z0) half(0) -> 0 half(s(0)) -> 0 half(s(s(z0))) -> s(half(z0)) pow(z0, z1) -> f(z0, z1, s(0)) f(z0, 0, z1) -> z1 f(z0, s(z1), z2) -> if(odd(s(z1)), f(z0, z1, *(z0, z2)), f(*(z0, z0), half(s(z1)), z2)) Tuples: -'(z0, 0) -> c -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, 0) -> c2 *'(z0, s(z1)) -> c3(*'(z0, z1)) IF(true, z0, z1) -> c4 IF(false, z0, z1) -> c5 IF(true, z0, z1) -> c6 IF(false, z0, z1) -> c7 ODD(0) -> c8 ODD(s(0)) -> c9 ODD(s(s(z0))) -> c10(ODD(z0)) HALF(0) -> c11 HALF(s(0)) -> c12 HALF(s(s(z0))) -> c13(HALF(z0)) POW(z0, z1) -> c14(F(z0, z1, s(0))) F(z0, 0, z1) -> c15 F(z0, s(z1), z2) -> c16(IF(odd(s(z1)), f(z0, z1, *(z0, z2)), f(*(z0, z0), half(s(z1)), z2)), ODD(s(z1))) F(z0, s(z1), z2) -> c17(IF(odd(s(z1)), f(z0, z1, *(z0, z2)), f(*(z0, z0), half(s(z1)), z2)), F(z0, z1, *(z0, z2)), *'(z0, z2)) F(z0, s(z1), z2) -> c18(IF(odd(s(z1)), f(z0, z1, *(z0, z2)), f(*(z0, z0), half(s(z1)), z2)), F(*(z0, z0), half(s(z1)), z2), *'(z0, z0)) F(z0, s(z1), z2) -> c19(IF(odd(s(z1)), f(z0, z1, *(z0, z2)), f(*(z0, z0), half(s(z1)), z2)), F(*(z0, z0), half(s(z1)), z2), HALF(s(z1))) S tuples: -'(z0, 0) -> c -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, 0) -> c2 *'(z0, s(z1)) -> c3(*'(z0, z1)) IF(true, z0, z1) -> c4 IF(false, z0, z1) -> c5 IF(true, z0, z1) -> c6 IF(false, z0, z1) -> c7 ODD(0) -> c8 ODD(s(0)) -> c9 ODD(s(s(z0))) -> c10(ODD(z0)) HALF(0) -> c11 HALF(s(0)) -> c12 HALF(s(s(z0))) -> c13(HALF(z0)) POW(z0, z1) -> c14(F(z0, z1, s(0))) F(z0, 0, z1) -> c15 F(z0, s(z1), z2) -> c16(IF(odd(s(z1)), f(z0, z1, *(z0, z2)), f(*(z0, z0), half(s(z1)), z2)), ODD(s(z1))) F(z0, s(z1), z2) -> c17(IF(odd(s(z1)), f(z0, z1, *(z0, z2)), f(*(z0, z0), half(s(z1)), z2)), F(z0, z1, *(z0, z2)), *'(z0, z2)) F(z0, s(z1), z2) -> c18(IF(odd(s(z1)), f(z0, z1, *(z0, z2)), f(*(z0, z0), half(s(z1)), z2)), F(*(z0, z0), half(s(z1)), z2), *'(z0, z0)) F(z0, s(z1), z2) -> c19(IF(odd(s(z1)), f(z0, z1, *(z0, z2)), f(*(z0, z0), half(s(z1)), z2)), F(*(z0, z0), half(s(z1)), z2), HALF(s(z1))) K tuples:none Defined Rule Symbols: -_2, *_2, if_3, odd_1, half_1, pow_2, f_3 Defined Pair Symbols: -'_2, *'_2, IF_3, ODD_1, HALF_1, POW_2, F_3 Compound Symbols: c, c1_1, c2, c3_1, c4, c5, c6, c7, c8, c9, c10_1, c11, c12, c13_1, c14_1, c15, c16_2, c17_3, c18_3, c19_3 ---------------------------------------- (3) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 1 leading nodes: POW(z0, z1) -> c14(F(z0, z1, s(0))) Removed 11 trailing nodes: HALF(s(0)) -> c12 ODD(0) -> c8 F(z0, 0, z1) -> c15 IF(true, z0, z1) -> c6 IF(false, z0, z1) -> c7 *'(z0, 0) -> c2 HALF(0) -> c11 -'(z0, 0) -> c IF(true, z0, z1) -> c4 ODD(s(0)) -> c9 IF(false, z0, z1) -> c5 ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: -(z0, 0) -> z0 -(s(z0), s(z1)) -> -(z0, z1) *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) if(true, z0, z1) -> z0 if(false, z0, z1) -> z1 if(true, z0, z1) -> true if(false, z0, z1) -> false odd(0) -> false odd(s(0)) -> true odd(s(s(z0))) -> odd(z0) half(0) -> 0 half(s(0)) -> 0 half(s(s(z0))) -> s(half(z0)) pow(z0, z1) -> f(z0, z1, s(0)) f(z0, 0, z1) -> z1 f(z0, s(z1), z2) -> if(odd(s(z1)), f(z0, z1, *(z0, z2)), f(*(z0, z0), half(s(z1)), z2)) Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(IF(odd(s(z1)), f(z0, z1, *(z0, z2)), f(*(z0, z0), half(s(z1)), z2)), ODD(s(z1))) F(z0, s(z1), z2) -> c17(IF(odd(s(z1)), f(z0, z1, *(z0, z2)), f(*(z0, z0), half(s(z1)), z2)), F(z0, z1, *(z0, z2)), *'(z0, z2)) F(z0, s(z1), z2) -> c18(IF(odd(s(z1)), f(z0, z1, *(z0, z2)), f(*(z0, z0), half(s(z1)), z2)), F(*(z0, z0), half(s(z1)), z2), *'(z0, z0)) F(z0, s(z1), z2) -> c19(IF(odd(s(z1)), f(z0, z1, *(z0, z2)), f(*(z0, z0), half(s(z1)), z2)), F(*(z0, z0), half(s(z1)), z2), HALF(s(z1))) S tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(IF(odd(s(z1)), f(z0, z1, *(z0, z2)), f(*(z0, z0), half(s(z1)), z2)), ODD(s(z1))) F(z0, s(z1), z2) -> c17(IF(odd(s(z1)), f(z0, z1, *(z0, z2)), f(*(z0, z0), half(s(z1)), z2)), F(z0, z1, *(z0, z2)), *'(z0, z2)) F(z0, s(z1), z2) -> c18(IF(odd(s(z1)), f(z0, z1, *(z0, z2)), f(*(z0, z0), half(s(z1)), z2)), F(*(z0, z0), half(s(z1)), z2), *'(z0, z0)) F(z0, s(z1), z2) -> c19(IF(odd(s(z1)), f(z0, z1, *(z0, z2)), f(*(z0, z0), half(s(z1)), z2)), F(*(z0, z0), half(s(z1)), z2), HALF(s(z1))) K tuples:none Defined Rule Symbols: -_2, *_2, if_3, odd_1, half_1, pow_2, f_3 Defined Pair Symbols: -'_2, *'_2, ODD_1, HALF_1, F_3 Compound Symbols: c1_1, c3_1, c10_1, c13_1, c16_2, c17_3, c18_3, c19_3 ---------------------------------------- (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) *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) if(true, z0, z1) -> z0 if(false, z0, z1) -> z1 if(true, z0, z1) -> true if(false, z0, z1) -> false odd(0) -> false odd(s(0)) -> true odd(s(s(z0))) -> odd(z0) half(0) -> 0 half(s(0)) -> 0 half(s(s(z0))) -> s(half(z0)) pow(z0, z1) -> f(z0, z1, s(0)) f(z0, 0, z1) -> z1 f(z0, s(z1), z2) -> if(odd(s(z1)), f(z0, z1, *(z0, z2)), f(*(z0, z0), half(s(z1)), z2)) Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(z0, s(z1), z2) -> c18(F(*(z0, z0), half(s(z1)), z2), *'(z0, z0)) F(z0, s(z1), z2) -> c19(F(*(z0, z0), half(s(z1)), z2), HALF(s(z1))) S tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(z0, s(z1), z2) -> c18(F(*(z0, z0), half(s(z1)), z2), *'(z0, z0)) F(z0, s(z1), z2) -> c19(F(*(z0, z0), half(s(z1)), z2), HALF(s(z1))) K tuples:none Defined Rule Symbols: -_2, *_2, if_3, odd_1, half_1, pow_2, f_3 Defined Pair Symbols: -'_2, *'_2, ODD_1, HALF_1, F_3 Compound Symbols: c1_1, c3_1, c10_1, c13_1, c16_1, c17_2, c18_2, c19_2 ---------------------------------------- (7) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: -(z0, 0) -> z0 -(s(z0), s(z1)) -> -(z0, z1) if(true, z0, z1) -> z0 if(false, z0, z1) -> z1 if(true, z0, z1) -> true if(false, z0, z1) -> false odd(0) -> false odd(s(0)) -> true odd(s(s(z0))) -> odd(z0) pow(z0, z1) -> f(z0, z1, s(0)) f(z0, 0, z1) -> z1 f(z0, s(z1), z2) -> if(odd(s(z1)), f(z0, z1, *(z0, z2)), f(*(z0, z0), half(s(z1)), z2)) ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules: *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) half(s(0)) -> 0 half(s(s(z0))) -> s(half(z0)) half(0) -> 0 Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(z0, s(z1), z2) -> c18(F(*(z0, z0), half(s(z1)), z2), *'(z0, z0)) F(z0, s(z1), z2) -> c19(F(*(z0, z0), half(s(z1)), z2), HALF(s(z1))) S tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(z0, s(z1), z2) -> c18(F(*(z0, z0), half(s(z1)), z2), *'(z0, z0)) F(z0, s(z1), z2) -> c19(F(*(z0, z0), half(s(z1)), z2), HALF(s(z1))) K tuples:none Defined Rule Symbols: *_2, half_1 Defined Pair Symbols: -'_2, *'_2, ODD_1, HALF_1, F_3 Compound Symbols: c1_1, c3_1, c10_1, c13_1, c16_1, c17_2, c18_2, c19_2 ---------------------------------------- (9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) We considered the (Usable) Rules: half(s(0)) -> 0 half(s(s(z0))) -> s(half(z0)) half(0) -> 0 *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) And the Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(z0, s(z1), z2) -> c18(F(*(z0, z0), half(s(z1)), z2), *'(z0, z0)) F(z0, s(z1), z2) -> c19(F(*(z0, z0), half(s(z1)), z2), HALF(s(z1))) The order we found is given by the following interpretation: Polynomial interpretation : POL(*(x_1, x_2)) = 0 POL(*'(x_1, x_2)) = x_2 POL(+(x_1, x_2)) = x_1 POL(-'(x_1, x_2)) = x_1 + x_2 POL(0) = 0 POL(F(x_1, x_2, x_3)) = [1] + x_1 + x_2 + x_3 POL(HALF(x_1)) = 0 POL(ODD(x_1)) = x_1 POL(c1(x_1)) = x_1 POL(c10(x_1)) = x_1 POL(c13(x_1)) = x_1 POL(c16(x_1)) = x_1 POL(c17(x_1, x_2)) = x_1 + x_2 POL(c18(x_1, x_2)) = x_1 + x_2 POL(c19(x_1, x_2)) = x_1 + x_2 POL(c3(x_1)) = x_1 POL(half(x_1)) = x_1 POL(s(x_1)) = [1] + x_1 ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules: *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) half(s(0)) -> 0 half(s(s(z0))) -> s(half(z0)) half(0) -> 0 Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(z0, s(z1), z2) -> c18(F(*(z0, z0), half(s(z1)), z2), *'(z0, z0)) F(z0, s(z1), z2) -> c19(F(*(z0, z0), half(s(z1)), z2), HALF(s(z1))) S tuples: HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c18(F(*(z0, z0), half(s(z1)), z2), *'(z0, z0)) F(z0, s(z1), z2) -> c19(F(*(z0, z0), half(s(z1)), z2), HALF(s(z1))) K tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) Defined Rule Symbols: *_2, half_1 Defined Pair Symbols: -'_2, *'_2, ODD_1, HALF_1, F_3 Compound Symbols: c1_1, c3_1, c10_1, c13_1, c16_1, c17_2, c18_2, c19_2 ---------------------------------------- (11) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace F(z0, s(z1), z2) -> c18(F(*(z0, z0), half(s(z1)), z2), *'(z0, z0)) by F(x0, s(0), x2) -> c18(F(*(x0, x0), 0, x2), *'(x0, x0)) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(0, s(x1), x2) -> c18(F(0, half(s(x1)), x2), *'(0, 0)) F(s(z1), s(x1), x2) -> c18(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), *'(s(z1), s(z1))) ---------------------------------------- (12) Obligation: Complexity Dependency Tuples Problem Rules: *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) half(s(0)) -> 0 half(s(s(z0))) -> s(half(z0)) half(0) -> 0 Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(z0, s(z1), z2) -> c19(F(*(z0, z0), half(s(z1)), z2), HALF(s(z1))) F(x0, s(0), x2) -> c18(F(*(x0, x0), 0, x2), *'(x0, x0)) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(0, s(x1), x2) -> c18(F(0, half(s(x1)), x2), *'(0, 0)) F(s(z1), s(x1), x2) -> c18(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), *'(s(z1), s(z1))) S tuples: HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c19(F(*(z0, z0), half(s(z1)), z2), HALF(s(z1))) F(x0, s(0), x2) -> c18(F(*(x0, x0), 0, x2), *'(x0, x0)) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(0, s(x1), x2) -> c18(F(0, half(s(x1)), x2), *'(0, 0)) F(s(z1), s(x1), x2) -> c18(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), *'(s(z1), s(z1))) K tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) Defined Rule Symbols: *_2, half_1 Defined Pair Symbols: -'_2, *'_2, ODD_1, HALF_1, F_3 Compound Symbols: c1_1, c3_1, c10_1, c13_1, c16_1, c17_2, c19_2, c18_2 ---------------------------------------- (13) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 2 trailing tuple parts ---------------------------------------- (14) Obligation: Complexity Dependency Tuples Problem Rules: *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) half(s(0)) -> 0 half(s(s(z0))) -> s(half(z0)) half(0) -> 0 Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(z0, s(z1), z2) -> c19(F(*(z0, z0), half(s(z1)), z2), HALF(s(z1))) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(s(z1), s(x1), x2) -> c18(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), *'(s(z1), s(z1))) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(0, s(x1), x2) -> c18(F(0, half(s(x1)), x2)) S tuples: HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c19(F(*(z0, z0), half(s(z1)), z2), HALF(s(z1))) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(s(z1), s(x1), x2) -> c18(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), *'(s(z1), s(z1))) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(0, s(x1), x2) -> c18(F(0, half(s(x1)), x2)) K tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) Defined Rule Symbols: *_2, half_1 Defined Pair Symbols: -'_2, *'_2, ODD_1, HALF_1, F_3 Compound Symbols: c1_1, c3_1, c10_1, c13_1, c16_1, c17_2, c19_2, c18_2, c18_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. F(x0, s(0), x2) -> c18(*'(x0, x0)) We considered the (Usable) Rules:none And the Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(z0, s(z1), z2) -> c19(F(*(z0, z0), half(s(z1)), z2), HALF(s(z1))) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(s(z1), s(x1), x2) -> c18(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), *'(s(z1), s(z1))) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(0, s(x1), x2) -> c18(F(0, half(s(x1)), x2)) The order we found is given by the following interpretation: Polynomial interpretation : POL(*(x_1, x_2)) = [1] + x_1 POL(*'(x_1, x_2)) = 0 POL(+(x_1, x_2)) = [1] + x_2 POL(-'(x_1, x_2)) = 0 POL(0) = 0 POL(F(x_1, x_2, x_3)) = [1] POL(HALF(x_1)) = 0 POL(ODD(x_1)) = [1] POL(c1(x_1)) = x_1 POL(c10(x_1)) = x_1 POL(c13(x_1)) = x_1 POL(c16(x_1)) = x_1 POL(c17(x_1, x_2)) = x_1 + x_2 POL(c18(x_1)) = x_1 POL(c18(x_1, x_2)) = x_1 + x_2 POL(c19(x_1, x_2)) = x_1 + x_2 POL(c3(x_1)) = x_1 POL(half(x_1)) = x_1 POL(s(x_1)) = 0 ---------------------------------------- (16) Obligation: Complexity Dependency Tuples Problem Rules: *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) half(s(0)) -> 0 half(s(s(z0))) -> s(half(z0)) half(0) -> 0 Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(z0, s(z1), z2) -> c19(F(*(z0, z0), half(s(z1)), z2), HALF(s(z1))) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(s(z1), s(x1), x2) -> c18(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), *'(s(z1), s(z1))) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(0, s(x1), x2) -> c18(F(0, half(s(x1)), x2)) S tuples: HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c19(F(*(z0, z0), half(s(z1)), z2), HALF(s(z1))) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(s(z1), s(x1), x2) -> c18(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), *'(s(z1), s(z1))) F(0, s(x1), x2) -> c18(F(0, half(s(x1)), x2)) K tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(0), x2) -> c18(*'(x0, x0)) Defined Rule Symbols: *_2, half_1 Defined Pair Symbols: -'_2, *'_2, ODD_1, HALF_1, F_3 Compound Symbols: c1_1, c3_1, c10_1, c13_1, c16_1, c17_2, c19_2, c18_2, c18_1 ---------------------------------------- (17) 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(x1), x2) -> c18(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), *'(s(z1), s(z1))) We considered the (Usable) Rules: *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) And the Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(z0, s(z1), z2) -> c19(F(*(z0, z0), half(s(z1)), z2), HALF(s(z1))) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(s(z1), s(x1), x2) -> c18(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), *'(s(z1), s(z1))) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(0, s(x1), x2) -> c18(F(0, half(s(x1)), x2)) The order we found is given by the following interpretation: Polynomial interpretation : POL(*(x_1, x_2)) = 0 POL(*'(x_1, x_2)) = 0 POL(+(x_1, x_2)) = 0 POL(-'(x_1, x_2)) = 0 POL(0) = 0 POL(F(x_1, x_2, x_3)) = [1] + x_1 + x_3 POL(HALF(x_1)) = 0 POL(ODD(x_1)) = 0 POL(c1(x_1)) = x_1 POL(c10(x_1)) = x_1 POL(c13(x_1)) = x_1 POL(c16(x_1)) = x_1 POL(c17(x_1, x_2)) = x_1 + x_2 POL(c18(x_1)) = x_1 POL(c18(x_1, x_2)) = x_1 + x_2 POL(c19(x_1, x_2)) = x_1 + x_2 POL(c3(x_1)) = x_1 POL(half(x_1)) = x_1 POL(s(x_1)) = [1] ---------------------------------------- (18) Obligation: Complexity Dependency Tuples Problem Rules: *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) half(s(0)) -> 0 half(s(s(z0))) -> s(half(z0)) half(0) -> 0 Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(z0, s(z1), z2) -> c19(F(*(z0, z0), half(s(z1)), z2), HALF(s(z1))) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(s(z1), s(x1), x2) -> c18(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), *'(s(z1), s(z1))) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(0, s(x1), x2) -> c18(F(0, half(s(x1)), x2)) S tuples: HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c19(F(*(z0, z0), half(s(z1)), z2), HALF(s(z1))) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(0, s(x1), x2) -> c18(F(0, half(s(x1)), x2)) K tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(s(z1), s(x1), x2) -> c18(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), *'(s(z1), s(z1))) Defined Rule Symbols: *_2, half_1 Defined Pair Symbols: -'_2, *'_2, ODD_1, HALF_1, F_3 Compound Symbols: c1_1, c3_1, c10_1, c13_1, c16_1, c17_2, c19_2, c18_2, c18_1 ---------------------------------------- (19) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) We considered the (Usable) Rules: half(s(0)) -> 0 half(s(s(z0))) -> s(half(z0)) half(0) -> 0 *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) And the Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(z0, s(z1), z2) -> c19(F(*(z0, z0), half(s(z1)), z2), HALF(s(z1))) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(s(z1), s(x1), x2) -> c18(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), *'(s(z1), s(z1))) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(0, s(x1), x2) -> c18(F(0, half(s(x1)), x2)) The order we found is given by the following interpretation: Polynomial interpretation : POL(*(x_1, x_2)) = x_2 POL(*'(x_1, x_2)) = 0 POL(+(x_1, x_2)) = [1] POL(-'(x_1, x_2)) = x_1 + x_2 POL(0) = [1] POL(F(x_1, x_2, x_3)) = [1] + x_1 + x_2 + x_3 POL(HALF(x_1)) = 0 POL(ODD(x_1)) = [1] + x_1 POL(c1(x_1)) = x_1 POL(c10(x_1)) = x_1 POL(c13(x_1)) = x_1 POL(c16(x_1)) = x_1 POL(c17(x_1, x_2)) = x_1 + x_2 POL(c18(x_1)) = x_1 POL(c18(x_1, x_2)) = x_1 + x_2 POL(c19(x_1, x_2)) = x_1 + x_2 POL(c3(x_1)) = x_1 POL(half(x_1)) = x_1 POL(s(x_1)) = [1] + x_1 ---------------------------------------- (20) Obligation: Complexity Dependency Tuples Problem Rules: *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) half(s(0)) -> 0 half(s(s(z0))) -> s(half(z0)) half(0) -> 0 Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(z0, s(z1), z2) -> c19(F(*(z0, z0), half(s(z1)), z2), HALF(s(z1))) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(s(z1), s(x1), x2) -> c18(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), *'(s(z1), s(z1))) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(0, s(x1), x2) -> c18(F(0, half(s(x1)), x2)) S tuples: HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c19(F(*(z0, z0), half(s(z1)), z2), HALF(s(z1))) F(0, s(x1), x2) -> c18(F(0, half(s(x1)), x2)) K tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(s(z1), s(x1), x2) -> c18(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), *'(s(z1), s(z1))) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) Defined Rule Symbols: *_2, half_1 Defined Pair Symbols: -'_2, *'_2, ODD_1, HALF_1, F_3 Compound Symbols: c1_1, c3_1, c10_1, c13_1, c16_1, c17_2, c19_2, c18_2, c18_1 ---------------------------------------- (21) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace F(z0, s(z1), z2) -> c19(F(*(z0, z0), half(s(z1)), z2), HALF(s(z1))) by F(x0, s(0), x2) -> c19(F(*(x0, x0), 0, x2), HALF(s(0))) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) F(0, s(x1), x2) -> c19(F(0, half(s(x1)), x2), HALF(s(x1))) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) ---------------------------------------- (22) Obligation: Complexity Dependency Tuples Problem Rules: *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) half(s(0)) -> 0 half(s(s(z0))) -> s(half(z0)) half(0) -> 0 Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(s(z1), s(x1), x2) -> c18(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), *'(s(z1), s(z1))) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(0, s(x1), x2) -> c18(F(0, half(s(x1)), x2)) F(x0, s(0), x2) -> c19(F(*(x0, x0), 0, x2), HALF(s(0))) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) F(0, s(x1), x2) -> c19(F(0, half(s(x1)), x2), HALF(s(x1))) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) S tuples: HALF(s(s(z0))) -> c13(HALF(z0)) F(0, s(x1), x2) -> c18(F(0, half(s(x1)), x2)) F(x0, s(0), x2) -> c19(F(*(x0, x0), 0, x2), HALF(s(0))) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) F(0, s(x1), x2) -> c19(F(0, half(s(x1)), x2), HALF(s(x1))) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) K tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(s(z1), s(x1), x2) -> c18(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), *'(s(z1), s(z1))) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) Defined Rule Symbols: *_2, half_1 Defined Pair Symbols: -'_2, *'_2, ODD_1, HALF_1, F_3 Compound Symbols: c1_1, c3_1, c10_1, c13_1, c16_1, c17_2, c18_2, c18_1, c19_2 ---------------------------------------- (23) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing nodes: F(x0, s(0), x2) -> c19(F(*(x0, x0), 0, x2), HALF(s(0))) ---------------------------------------- (24) Obligation: Complexity Dependency Tuples Problem Rules: *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) half(s(0)) -> 0 half(s(s(z0))) -> s(half(z0)) half(0) -> 0 Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(s(z1), s(x1), x2) -> c18(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), *'(s(z1), s(z1))) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(0, s(x1), x2) -> c18(F(0, half(s(x1)), x2)) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) F(0, s(x1), x2) -> c19(F(0, half(s(x1)), x2), HALF(s(x1))) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) S tuples: HALF(s(s(z0))) -> c13(HALF(z0)) F(0, s(x1), x2) -> c18(F(0, half(s(x1)), x2)) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) F(0, s(x1), x2) -> c19(F(0, half(s(x1)), x2), HALF(s(x1))) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) K tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(s(z1), s(x1), x2) -> c18(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), *'(s(z1), s(z1))) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) Defined Rule Symbols: *_2, half_1 Defined Pair Symbols: -'_2, *'_2, ODD_1, HALF_1, F_3 Compound Symbols: c1_1, c3_1, c10_1, c13_1, c16_1, c17_2, c18_2, c18_1, c19_2 ---------------------------------------- (25) 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(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) We considered the (Usable) Rules: *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) And the Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(s(z1), s(x1), x2) -> c18(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), *'(s(z1), s(z1))) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(0, s(x1), x2) -> c18(F(0, half(s(x1)), x2)) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) F(0, s(x1), x2) -> c19(F(0, half(s(x1)), x2), HALF(s(x1))) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) The order we found is given by the following interpretation: Polynomial interpretation : POL(*(x_1, x_2)) = 0 POL(*'(x_1, x_2)) = 0 POL(+(x_1, x_2)) = 0 POL(-'(x_1, x_2)) = 0 POL(0) = 0 POL(F(x_1, x_2, x_3)) = [1] + x_1 + x_3 POL(HALF(x_1)) = 0 POL(ODD(x_1)) = [1] POL(c1(x_1)) = x_1 POL(c10(x_1)) = x_1 POL(c13(x_1)) = x_1 POL(c16(x_1)) = x_1 POL(c17(x_1, x_2)) = x_1 + x_2 POL(c18(x_1)) = x_1 POL(c18(x_1, x_2)) = x_1 + x_2 POL(c19(x_1, x_2)) = x_1 + x_2 POL(c3(x_1)) = x_1 POL(half(x_1)) = [1] POL(s(x_1)) = [1] ---------------------------------------- (26) Obligation: Complexity Dependency Tuples Problem Rules: *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) half(s(0)) -> 0 half(s(s(z0))) -> s(half(z0)) half(0) -> 0 Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(s(z1), s(x1), x2) -> c18(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), *'(s(z1), s(z1))) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(0, s(x1), x2) -> c18(F(0, half(s(x1)), x2)) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) F(0, s(x1), x2) -> c19(F(0, half(s(x1)), x2), HALF(s(x1))) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) S tuples: HALF(s(s(z0))) -> c13(HALF(z0)) F(0, s(x1), x2) -> c18(F(0, half(s(x1)), x2)) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) F(0, s(x1), x2) -> c19(F(0, half(s(x1)), x2), HALF(s(x1))) K tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(s(z1), s(x1), x2) -> c18(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), *'(s(z1), s(z1))) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) Defined Rule Symbols: *_2, half_1 Defined Pair Symbols: -'_2, *'_2, ODD_1, HALF_1, F_3 Compound Symbols: c1_1, c3_1, c10_1, c13_1, c16_1, c17_2, c18_2, c18_1, c19_2 ---------------------------------------- (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(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) We considered the (Usable) Rules: half(s(0)) -> 0 half(s(s(z0))) -> s(half(z0)) half(0) -> 0 And the Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(s(z1), s(x1), x2) -> c18(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), *'(s(z1), s(z1))) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(0, s(x1), x2) -> c18(F(0, half(s(x1)), x2)) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) F(0, s(x1), x2) -> c19(F(0, half(s(x1)), x2), HALF(s(x1))) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) The order we found is given by the following interpretation: Polynomial interpretation : POL(*(x_1, x_2)) = [1] + x_1 POL(*'(x_1, x_2)) = 0 POL(+(x_1, x_2)) = [1] + x_2 POL(-'(x_1, x_2)) = x_1 + x_2 POL(0) = [1] POL(F(x_1, x_2, x_3)) = [1] + x_2 POL(HALF(x_1)) = 0 POL(ODD(x_1)) = [1] + x_1 POL(c1(x_1)) = x_1 POL(c10(x_1)) = x_1 POL(c13(x_1)) = x_1 POL(c16(x_1)) = x_1 POL(c17(x_1, x_2)) = x_1 + x_2 POL(c18(x_1)) = x_1 POL(c18(x_1, x_2)) = x_1 + x_2 POL(c19(x_1, x_2)) = x_1 + x_2 POL(c3(x_1)) = x_1 POL(half(x_1)) = x_1 POL(s(x_1)) = [1] + x_1 ---------------------------------------- (28) Obligation: Complexity Dependency Tuples Problem Rules: *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) half(s(0)) -> 0 half(s(s(z0))) -> s(half(z0)) half(0) -> 0 Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(s(z1), s(x1), x2) -> c18(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), *'(s(z1), s(z1))) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(0, s(x1), x2) -> c18(F(0, half(s(x1)), x2)) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) F(0, s(x1), x2) -> c19(F(0, half(s(x1)), x2), HALF(s(x1))) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) S tuples: HALF(s(s(z0))) -> c13(HALF(z0)) F(0, s(x1), x2) -> c18(F(0, half(s(x1)), x2)) F(0, s(x1), x2) -> c19(F(0, half(s(x1)), x2), HALF(s(x1))) K tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(s(z1), s(x1), x2) -> c18(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), *'(s(z1), s(z1))) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) Defined Rule Symbols: *_2, half_1 Defined Pair Symbols: -'_2, *'_2, ODD_1, HALF_1, F_3 Compound Symbols: c1_1, c3_1, c10_1, c13_1, c16_1, c17_2, c18_2, c18_1, c19_2 ---------------------------------------- (29) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace F(s(z1), s(x1), x2) -> c18(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), *'(s(z1), s(z1))) by F(s(x0), s(0), x2) -> c18(F(+(*(s(x0), x0), s(x0)), 0, x2), *'(s(x0), s(x0))) F(s(x0), s(s(z0)), x2) -> c18(F(+(*(s(x0), x0), s(x0)), s(half(z0)), x2), *'(s(x0), s(x0))) F(s(0), s(x1), x2) -> c18(F(+(0, s(0)), half(s(x1)), x2), *'(s(0), s(0))) F(s(s(z1)), s(x1), x2) -> c18(F(+(+(*(s(s(z1)), z1), s(s(z1))), s(s(z1))), half(s(x1)), x2), *'(s(s(z1)), s(s(z1)))) F(s(x0), s(x1), x2) -> c18(*'(s(x0), s(x0))) ---------------------------------------- (30) Obligation: Complexity Dependency Tuples Problem Rules: *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) half(s(0)) -> 0 half(s(s(z0))) -> s(half(z0)) half(0) -> 0 Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(0, s(x1), x2) -> c18(F(0, half(s(x1)), x2)) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) F(0, s(x1), x2) -> c19(F(0, half(s(x1)), x2), HALF(s(x1))) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) F(s(x0), s(0), x2) -> c18(F(+(*(s(x0), x0), s(x0)), 0, x2), *'(s(x0), s(x0))) F(s(x0), s(s(z0)), x2) -> c18(F(+(*(s(x0), x0), s(x0)), s(half(z0)), x2), *'(s(x0), s(x0))) F(s(0), s(x1), x2) -> c18(F(+(0, s(0)), half(s(x1)), x2), *'(s(0), s(0))) F(s(s(z1)), s(x1), x2) -> c18(F(+(+(*(s(s(z1)), z1), s(s(z1))), s(s(z1))), half(s(x1)), x2), *'(s(s(z1)), s(s(z1)))) F(s(x0), s(x1), x2) -> c18(*'(s(x0), s(x0))) S tuples: HALF(s(s(z0))) -> c13(HALF(z0)) F(0, s(x1), x2) -> c18(F(0, half(s(x1)), x2)) F(0, s(x1), x2) -> c19(F(0, half(s(x1)), x2), HALF(s(x1))) K tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(s(z1), s(x1), x2) -> c18(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), *'(s(z1), s(z1))) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) Defined Rule Symbols: *_2, half_1 Defined Pair Symbols: -'_2, *'_2, ODD_1, HALF_1, F_3 Compound Symbols: c1_1, c3_1, c10_1, c13_1, c16_1, c17_2, c18_2, c18_1, c19_2 ---------------------------------------- (31) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing tuple parts ---------------------------------------- (32) Obligation: Complexity Dependency Tuples Problem Rules: *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) half(s(0)) -> 0 half(s(s(z0))) -> s(half(z0)) half(0) -> 0 Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(0, s(x1), x2) -> c18(F(0, half(s(x1)), x2)) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) F(0, s(x1), x2) -> c19(F(0, half(s(x1)), x2), HALF(s(x1))) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) F(s(x0), s(s(z0)), x2) -> c18(F(+(*(s(x0), x0), s(x0)), s(half(z0)), x2), *'(s(x0), s(x0))) F(s(0), s(x1), x2) -> c18(F(+(0, s(0)), half(s(x1)), x2), *'(s(0), s(0))) F(s(s(z1)), s(x1), x2) -> c18(F(+(+(*(s(s(z1)), z1), s(s(z1))), s(s(z1))), half(s(x1)), x2), *'(s(s(z1)), s(s(z1)))) F(s(x0), s(x1), x2) -> c18(*'(s(x0), s(x0))) F(s(x0), s(0), x2) -> c18(*'(s(x0), s(x0))) S tuples: HALF(s(s(z0))) -> c13(HALF(z0)) F(0, s(x1), x2) -> c18(F(0, half(s(x1)), x2)) F(0, s(x1), x2) -> c19(F(0, half(s(x1)), x2), HALF(s(x1))) K tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(s(z1), s(x1), x2) -> c18(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), *'(s(z1), s(z1))) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) Defined Rule Symbols: *_2, half_1 Defined Pair Symbols: -'_2, *'_2, ODD_1, HALF_1, F_3 Compound Symbols: c1_1, c3_1, c10_1, c13_1, c16_1, c17_2, c18_2, c18_1, c19_2 ---------------------------------------- (33) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace F(0, s(x1), x2) -> c18(F(0, half(s(x1)), x2)) by F(0, s(0), x1) -> c18(F(0, 0, x1)) F(0, s(s(z0)), x1) -> c18(F(0, s(half(z0)), x1)) ---------------------------------------- (34) Obligation: Complexity Dependency Tuples Problem Rules: *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) half(s(0)) -> 0 half(s(s(z0))) -> s(half(z0)) half(0) -> 0 Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) F(0, s(x1), x2) -> c19(F(0, half(s(x1)), x2), HALF(s(x1))) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) F(s(x0), s(s(z0)), x2) -> c18(F(+(*(s(x0), x0), s(x0)), s(half(z0)), x2), *'(s(x0), s(x0))) F(s(0), s(x1), x2) -> c18(F(+(0, s(0)), half(s(x1)), x2), *'(s(0), s(0))) F(s(s(z1)), s(x1), x2) -> c18(F(+(+(*(s(s(z1)), z1), s(s(z1))), s(s(z1))), half(s(x1)), x2), *'(s(s(z1)), s(s(z1)))) F(s(x0), s(x1), x2) -> c18(*'(s(x0), s(x0))) F(s(x0), s(0), x2) -> c18(*'(s(x0), s(x0))) F(0, s(0), x1) -> c18(F(0, 0, x1)) F(0, s(s(z0)), x1) -> c18(F(0, s(half(z0)), x1)) S tuples: HALF(s(s(z0))) -> c13(HALF(z0)) F(0, s(x1), x2) -> c19(F(0, half(s(x1)), x2), HALF(s(x1))) F(0, s(0), x1) -> c18(F(0, 0, x1)) F(0, s(s(z0)), x1) -> c18(F(0, s(half(z0)), x1)) K tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(s(z1), s(x1), x2) -> c18(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), *'(s(z1), s(z1))) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) Defined Rule Symbols: *_2, half_1 Defined Pair Symbols: -'_2, *'_2, ODD_1, HALF_1, F_3 Compound Symbols: c1_1, c3_1, c10_1, c13_1, c16_1, c17_2, c18_2, c18_1, c19_2 ---------------------------------------- (35) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing nodes: F(0, s(0), x1) -> c18(F(0, 0, x1)) ---------------------------------------- (36) Obligation: Complexity Dependency Tuples Problem Rules: *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) half(s(0)) -> 0 half(s(s(z0))) -> s(half(z0)) half(0) -> 0 Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) F(0, s(x1), x2) -> c19(F(0, half(s(x1)), x2), HALF(s(x1))) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) F(s(x0), s(s(z0)), x2) -> c18(F(+(*(s(x0), x0), s(x0)), s(half(z0)), x2), *'(s(x0), s(x0))) F(s(0), s(x1), x2) -> c18(F(+(0, s(0)), half(s(x1)), x2), *'(s(0), s(0))) F(s(s(z1)), s(x1), x2) -> c18(F(+(+(*(s(s(z1)), z1), s(s(z1))), s(s(z1))), half(s(x1)), x2), *'(s(s(z1)), s(s(z1)))) F(s(x0), s(x1), x2) -> c18(*'(s(x0), s(x0))) F(s(x0), s(0), x2) -> c18(*'(s(x0), s(x0))) F(0, s(s(z0)), x1) -> c18(F(0, s(half(z0)), x1)) S tuples: HALF(s(s(z0))) -> c13(HALF(z0)) F(0, s(x1), x2) -> c19(F(0, half(s(x1)), x2), HALF(s(x1))) F(0, s(s(z0)), x1) -> c18(F(0, s(half(z0)), x1)) K tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) Defined Rule Symbols: *_2, half_1 Defined Pair Symbols: -'_2, *'_2, ODD_1, HALF_1, F_3 Compound Symbols: c1_1, c3_1, c10_1, c13_1, c16_1, c17_2, c18_2, c18_1, c19_2 ---------------------------------------- (37) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. F(0, s(s(z0)), x1) -> c18(F(0, s(half(z0)), x1)) We considered the (Usable) Rules: half(s(0)) -> 0 half(s(s(z0))) -> s(half(z0)) half(0) -> 0 *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) And the Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) F(0, s(x1), x2) -> c19(F(0, half(s(x1)), x2), HALF(s(x1))) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) F(s(x0), s(s(z0)), x2) -> c18(F(+(*(s(x0), x0), s(x0)), s(half(z0)), x2), *'(s(x0), s(x0))) F(s(0), s(x1), x2) -> c18(F(+(0, s(0)), half(s(x1)), x2), *'(s(0), s(0))) F(s(s(z1)), s(x1), x2) -> c18(F(+(+(*(s(s(z1)), z1), s(s(z1))), s(s(z1))), half(s(x1)), x2), *'(s(s(z1)), s(s(z1)))) F(s(x0), s(x1), x2) -> c18(*'(s(x0), s(x0))) F(s(x0), s(0), x2) -> c18(*'(s(x0), s(x0))) F(0, s(s(z0)), x1) -> c18(F(0, s(half(z0)), x1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(*(x_1, x_2)) = [1] POL(*'(x_1, x_2)) = 0 POL(+(x_1, x_2)) = x_1 POL(-'(x_1, x_2)) = x_1 + x_2 POL(0) = 0 POL(F(x_1, x_2, x_3)) = [1] + x_1 + x_2 + x_3 POL(HALF(x_1)) = 0 POL(ODD(x_1)) = [1] + x_1 POL(c1(x_1)) = x_1 POL(c10(x_1)) = x_1 POL(c13(x_1)) = x_1 POL(c16(x_1)) = x_1 POL(c17(x_1, x_2)) = x_1 + x_2 POL(c18(x_1)) = x_1 POL(c18(x_1, x_2)) = x_1 + x_2 POL(c19(x_1, x_2)) = x_1 + x_2 POL(c3(x_1)) = x_1 POL(half(x_1)) = x_1 POL(s(x_1)) = [1] + x_1 ---------------------------------------- (38) Obligation: Complexity Dependency Tuples Problem Rules: *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) half(s(0)) -> 0 half(s(s(z0))) -> s(half(z0)) half(0) -> 0 Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) F(0, s(x1), x2) -> c19(F(0, half(s(x1)), x2), HALF(s(x1))) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) F(s(x0), s(s(z0)), x2) -> c18(F(+(*(s(x0), x0), s(x0)), s(half(z0)), x2), *'(s(x0), s(x0))) F(s(0), s(x1), x2) -> c18(F(+(0, s(0)), half(s(x1)), x2), *'(s(0), s(0))) F(s(s(z1)), s(x1), x2) -> c18(F(+(+(*(s(s(z1)), z1), s(s(z1))), s(s(z1))), half(s(x1)), x2), *'(s(s(z1)), s(s(z1)))) F(s(x0), s(x1), x2) -> c18(*'(s(x0), s(x0))) F(s(x0), s(0), x2) -> c18(*'(s(x0), s(x0))) F(0, s(s(z0)), x1) -> c18(F(0, s(half(z0)), x1)) S tuples: HALF(s(s(z0))) -> c13(HALF(z0)) F(0, s(x1), x2) -> c19(F(0, half(s(x1)), x2), HALF(s(x1))) K tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) F(0, s(s(z0)), x1) -> c18(F(0, s(half(z0)), x1)) Defined Rule Symbols: *_2, half_1 Defined Pair Symbols: -'_2, *'_2, ODD_1, HALF_1, F_3 Compound Symbols: c1_1, c3_1, c10_1, c13_1, c16_1, c17_2, c18_2, c18_1, c19_2 ---------------------------------------- (39) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace F(0, s(x1), x2) -> c19(F(0, half(s(x1)), x2), HALF(s(x1))) by F(0, s(0), x1) -> c19(F(0, 0, x1), HALF(s(0))) F(0, s(s(z0)), x1) -> c19(F(0, s(half(z0)), x1), HALF(s(s(z0)))) ---------------------------------------- (40) Obligation: Complexity Dependency Tuples Problem Rules: *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) half(s(0)) -> 0 half(s(s(z0))) -> s(half(z0)) half(0) -> 0 Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) F(s(x0), s(s(z0)), x2) -> c18(F(+(*(s(x0), x0), s(x0)), s(half(z0)), x2), *'(s(x0), s(x0))) F(s(0), s(x1), x2) -> c18(F(+(0, s(0)), half(s(x1)), x2), *'(s(0), s(0))) F(s(s(z1)), s(x1), x2) -> c18(F(+(+(*(s(s(z1)), z1), s(s(z1))), s(s(z1))), half(s(x1)), x2), *'(s(s(z1)), s(s(z1)))) F(s(x0), s(x1), x2) -> c18(*'(s(x0), s(x0))) F(s(x0), s(0), x2) -> c18(*'(s(x0), s(x0))) F(0, s(s(z0)), x1) -> c18(F(0, s(half(z0)), x1)) F(0, s(0), x1) -> c19(F(0, 0, x1), HALF(s(0))) F(0, s(s(z0)), x1) -> c19(F(0, s(half(z0)), x1), HALF(s(s(z0)))) S tuples: HALF(s(s(z0))) -> c13(HALF(z0)) F(0, s(0), x1) -> c19(F(0, 0, x1), HALF(s(0))) F(0, s(s(z0)), x1) -> c19(F(0, s(half(z0)), x1), HALF(s(s(z0)))) K tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) F(0, s(s(z0)), x1) -> c18(F(0, s(half(z0)), x1)) Defined Rule Symbols: *_2, half_1 Defined Pair Symbols: -'_2, *'_2, ODD_1, HALF_1, F_3 Compound Symbols: c1_1, c3_1, c10_1, c13_1, c16_1, c17_2, c18_2, c18_1, c19_2 ---------------------------------------- (41) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing nodes: F(0, s(0), x1) -> c19(F(0, 0, x1), HALF(s(0))) ---------------------------------------- (42) Obligation: Complexity Dependency Tuples Problem Rules: *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) half(s(0)) -> 0 half(s(s(z0))) -> s(half(z0)) half(0) -> 0 Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) F(s(x0), s(s(z0)), x2) -> c18(F(+(*(s(x0), x0), s(x0)), s(half(z0)), x2), *'(s(x0), s(x0))) F(s(0), s(x1), x2) -> c18(F(+(0, s(0)), half(s(x1)), x2), *'(s(0), s(0))) F(s(s(z1)), s(x1), x2) -> c18(F(+(+(*(s(s(z1)), z1), s(s(z1))), s(s(z1))), half(s(x1)), x2), *'(s(s(z1)), s(s(z1)))) F(s(x0), s(x1), x2) -> c18(*'(s(x0), s(x0))) F(s(x0), s(0), x2) -> c18(*'(s(x0), s(x0))) F(0, s(s(z0)), x1) -> c18(F(0, s(half(z0)), x1)) F(0, s(s(z0)), x1) -> c19(F(0, s(half(z0)), x1), HALF(s(s(z0)))) S tuples: HALF(s(s(z0))) -> c13(HALF(z0)) F(0, s(s(z0)), x1) -> c19(F(0, s(half(z0)), x1), HALF(s(s(z0)))) K tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) F(0, s(s(z0)), x1) -> c18(F(0, s(half(z0)), x1)) Defined Rule Symbols: *_2, half_1 Defined Pair Symbols: -'_2, *'_2, ODD_1, HALF_1, F_3 Compound Symbols: c1_1, c3_1, c10_1, c13_1, c16_1, c17_2, c18_2, c18_1, c19_2 ---------------------------------------- (43) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. F(0, s(s(z0)), x1) -> c19(F(0, s(half(z0)), x1), HALF(s(s(z0)))) We considered the (Usable) Rules: half(s(0)) -> 0 half(s(s(z0))) -> s(half(z0)) half(0) -> 0 *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) And the Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) F(s(x0), s(s(z0)), x2) -> c18(F(+(*(s(x0), x0), s(x0)), s(half(z0)), x2), *'(s(x0), s(x0))) F(s(0), s(x1), x2) -> c18(F(+(0, s(0)), half(s(x1)), x2), *'(s(0), s(0))) F(s(s(z1)), s(x1), x2) -> c18(F(+(+(*(s(s(z1)), z1), s(s(z1))), s(s(z1))), half(s(x1)), x2), *'(s(s(z1)), s(s(z1)))) F(s(x0), s(x1), x2) -> c18(*'(s(x0), s(x0))) F(s(x0), s(0), x2) -> c18(*'(s(x0), s(x0))) F(0, s(s(z0)), x1) -> c18(F(0, s(half(z0)), x1)) F(0, s(s(z0)), x1) -> c19(F(0, s(half(z0)), x1), HALF(s(s(z0)))) The order we found is given by the following interpretation: Polynomial interpretation : POL(*(x_1, x_2)) = x_2 POL(*'(x_1, x_2)) = [1] POL(+(x_1, x_2)) = [1] POL(-'(x_1, x_2)) = [3]x_1 + [3]x_2 POL(0) = [2] POL(F(x_1, x_2, x_3)) = x_1 + x_2 POL(HALF(x_1)) = 0 POL(ODD(x_1)) = [2] POL(c1(x_1)) = x_1 POL(c10(x_1)) = x_1 POL(c13(x_1)) = x_1 POL(c16(x_1)) = x_1 POL(c17(x_1, x_2)) = x_1 + x_2 POL(c18(x_1)) = x_1 POL(c18(x_1, x_2)) = x_1 + x_2 POL(c19(x_1, x_2)) = x_1 + x_2 POL(c3(x_1)) = x_1 POL(half(x_1)) = [1] + x_1 POL(s(x_1)) = [2] + x_1 ---------------------------------------- (44) Obligation: Complexity Dependency Tuples Problem Rules: *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) half(s(0)) -> 0 half(s(s(z0))) -> s(half(z0)) half(0) -> 0 Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) F(s(x0), s(s(z0)), x2) -> c18(F(+(*(s(x0), x0), s(x0)), s(half(z0)), x2), *'(s(x0), s(x0))) F(s(0), s(x1), x2) -> c18(F(+(0, s(0)), half(s(x1)), x2), *'(s(0), s(0))) F(s(s(z1)), s(x1), x2) -> c18(F(+(+(*(s(s(z1)), z1), s(s(z1))), s(s(z1))), half(s(x1)), x2), *'(s(s(z1)), s(s(z1)))) F(s(x0), s(x1), x2) -> c18(*'(s(x0), s(x0))) F(s(x0), s(0), x2) -> c18(*'(s(x0), s(x0))) F(0, s(s(z0)), x1) -> c18(F(0, s(half(z0)), x1)) F(0, s(s(z0)), x1) -> c19(F(0, s(half(z0)), x1), HALF(s(s(z0)))) S tuples: HALF(s(s(z0))) -> c13(HALF(z0)) K tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) F(0, s(s(z0)), x1) -> c18(F(0, s(half(z0)), x1)) F(0, s(s(z0)), x1) -> c19(F(0, s(half(z0)), x1), HALF(s(s(z0)))) Defined Rule Symbols: *_2, half_1 Defined Pair Symbols: -'_2, *'_2, ODD_1, HALF_1, F_3 Compound Symbols: c1_1, c3_1, c10_1, c13_1, c16_1, c17_2, c18_2, c18_1, c19_2 ---------------------------------------- (45) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. HALF(s(s(z0))) -> c13(HALF(z0)) We considered the (Usable) Rules: half(s(0)) -> 0 half(s(s(z0))) -> s(half(z0)) half(0) -> 0 *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) And the Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) F(s(x0), s(s(z0)), x2) -> c18(F(+(*(s(x0), x0), s(x0)), s(half(z0)), x2), *'(s(x0), s(x0))) F(s(0), s(x1), x2) -> c18(F(+(0, s(0)), half(s(x1)), x2), *'(s(0), s(0))) F(s(s(z1)), s(x1), x2) -> c18(F(+(+(*(s(s(z1)), z1), s(s(z1))), s(s(z1))), half(s(x1)), x2), *'(s(s(z1)), s(s(z1)))) F(s(x0), s(x1), x2) -> c18(*'(s(x0), s(x0))) F(s(x0), s(0), x2) -> c18(*'(s(x0), s(x0))) F(0, s(s(z0)), x1) -> c18(F(0, s(half(z0)), x1)) F(0, s(s(z0)), x1) -> c19(F(0, s(half(z0)), x1), HALF(s(s(z0)))) The order we found is given by the following interpretation: Polynomial interpretation : POL(*(x_1, x_2)) = [1] POL(*'(x_1, x_2)) = 0 POL(+(x_1, x_2)) = 0 POL(-'(x_1, x_2)) = x_1 + x_2 POL(0) = 0 POL(F(x_1, x_2, x_3)) = [2] + [2]x_1*x_2 + [2]x_2^2 POL(HALF(x_1)) = [2]x_1 POL(ODD(x_1)) = 0 POL(c1(x_1)) = x_1 POL(c10(x_1)) = x_1 POL(c13(x_1)) = x_1 POL(c16(x_1)) = x_1 POL(c17(x_1, x_2)) = x_1 + x_2 POL(c18(x_1)) = x_1 POL(c18(x_1, x_2)) = x_1 + x_2 POL(c19(x_1, x_2)) = x_1 + x_2 POL(c3(x_1)) = x_1 POL(half(x_1)) = x_1 POL(s(x_1)) = [1] + x_1 ---------------------------------------- (46) Obligation: Complexity Dependency Tuples Problem Rules: *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) half(s(0)) -> 0 half(s(s(z0))) -> s(half(z0)) half(0) -> 0 Tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) HALF(s(s(z0))) -> c13(HALF(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) F(s(x0), s(s(z0)), x2) -> c18(F(+(*(s(x0), x0), s(x0)), s(half(z0)), x2), *'(s(x0), s(x0))) F(s(0), s(x1), x2) -> c18(F(+(0, s(0)), half(s(x1)), x2), *'(s(0), s(0))) F(s(s(z1)), s(x1), x2) -> c18(F(+(+(*(s(s(z1)), z1), s(s(z1))), s(s(z1))), half(s(x1)), x2), *'(s(s(z1)), s(s(z1)))) F(s(x0), s(x1), x2) -> c18(*'(s(x0), s(x0))) F(s(x0), s(0), x2) -> c18(*'(s(x0), s(x0))) F(0, s(s(z0)), x1) -> c18(F(0, s(half(z0)), x1)) F(0, s(s(z0)), x1) -> c19(F(0, s(half(z0)), x1), HALF(s(s(z0)))) S tuples:none K tuples: -'(s(z0), s(z1)) -> c1(-'(z0, z1)) *'(z0, s(z1)) -> c3(*'(z0, z1)) ODD(s(s(z0))) -> c10(ODD(z0)) F(z0, s(z1), z2) -> c16(ODD(s(z1))) F(z0, s(z1), z2) -> c17(F(z0, z1, *(z0, z2)), *'(z0, z2)) F(x0, s(0), x2) -> c18(*'(x0, x0)) F(x0, s(s(z0)), x2) -> c18(F(*(x0, x0), s(half(z0)), x2), *'(x0, x0)) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) F(x0, s(s(z0)), x2) -> c19(F(*(x0, x0), s(half(z0)), x2), HALF(s(s(z0)))) F(0, s(s(z0)), x1) -> c18(F(0, s(half(z0)), x1)) F(0, s(s(z0)), x1) -> c19(F(0, s(half(z0)), x1), HALF(s(s(z0)))) HALF(s(s(z0))) -> c13(HALF(z0)) Defined Rule Symbols: *_2, half_1 Defined Pair Symbols: -'_2, *'_2, ODD_1, HALF_1, F_3 Compound Symbols: c1_1, c3_1, c10_1, c13_1, c16_1, c17_2, c18_2, c18_1, c19_2 ---------------------------------------- (47) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (48) BOUNDS(1, 1)