WORST_CASE(Omega(n^1),O(n^2)) proof of input_hnxWtEQbn6.trs # AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, n^2). (0) CpxTRS (1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (2) CdtProblem (3) CdtLeafRemovalProof [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)), 100 ms] (10) CdtProblem (11) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 27 ms] (12) CdtProblem (13) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (14) CdtProblem (15) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (16) CdtProblem (17) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 23 ms] (18) CdtProblem (19) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 14 ms] (20) CdtProblem (21) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 15 ms] (22) CdtProblem (23) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (24) CdtProblem (25) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (26) CdtProblem (27) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 24 ms] (28) CdtProblem (29) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 20 ms] (30) CdtProblem (31) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (32) CdtProblem (33) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (34) CdtProblem (35) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (36) CdtProblem (37) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (38) CdtProblem (39) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 6 ms] (40) CdtProblem (41) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (42) CdtProblem (43) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (44) CdtProblem (45) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 21 ms] (46) CdtProblem (47) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 358 ms] (48) CdtProblem (49) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms] (50) BOUNDS(1, 1) (51) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms] (52) CdtProblem (53) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (54) CpxRelTRS (55) RenamingProof [BOTH BOUNDS(ID, ID), 2 ms] (56) CpxRelTRS (57) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (58) typed CpxTrs (59) OrderProof [LOWER BOUND(ID), 0 ms] (60) typed CpxTrs (61) RewriteLemmaProof [LOWER BOUND(ID), 296 ms] (62) BEST (63) proven lower bound (64) LowerBoundPropagationProof [FINISHED, 0 ms] (65) BOUNDS(n^1, INF) (66) typed CpxTrs (67) RewriteLemmaProof [LOWER BOUND(ID), 2037 ms] (68) typed CpxTrs (69) RewriteLemmaProof [LOWER BOUND(ID), 76 ms] (70) typed CpxTrs (71) RewriteLemmaProof [LOWER BOUND(ID), 75 ms] (72) typed CpxTrs (73) RewriteLemmaProof [LOWER BOUND(ID), 8 ms] (74) typed CpxTrs (75) RewriteLemmaProof [LOWER BOUND(ID), 79 ms] (76) typed CpxTrs (77) RewriteLemmaProof [LOWER BOUND(ID), 612 ms] (78) BOUNDS(1, INF) ---------------------------------------- (0) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, n^2). The TRS R consists of the following rules: -(x, 0) -> x -(s(x), s(y)) -> -(x, y) *(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: IF(true, z0, z1) -> c6 F(z0, 0, z1) -> c15 -'(z0, 0) -> c HALF(s(0)) -> c12 HALF(0) -> c11 ODD(s(0)) -> c9 *'(z0, 0) -> c2 IF(false, z0, z1) -> c5 ODD(0) -> c8 IF(true, z0, z1) -> c4 IF(false, z0, z1) -> c7 ---------------------------------------- (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. F(z0, s(z1), z2) -> c16(ODD(s(z1))) 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) -> 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)) = [2] + [3]x_1 + [2]x_2 POL(*'(x_1, x_2)) = 0 POL(+(x_1, x_2)) = x_2 POL(-'(x_1, x_2)) = 0 POL(0) = [1] POL(F(x_1, x_2, x_3)) = [2] 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_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)) = 0 POL(s(x_1)) = [2] ---------------------------------------- (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: -'(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) -> 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: F(z0, s(z1), z2) -> c16(ODD(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, c18_2, c19_2 ---------------------------------------- (11) 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) -> 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)) = [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 ---------------------------------------- (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) -> 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: F(z0, s(z1), z2) -> c16(ODD(s(z1))) -'(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) -> 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 ---------------------------------------- (13) 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))) ---------------------------------------- (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(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: F(z0, s(z1), z2) -> c16(ODD(s(z1))) -'(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) -> 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 ---------------------------------------- (15) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 2 trailing tuple parts ---------------------------------------- (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(x0, s(0), x2) -> c18(*'(x0, x0)) F(0, s(x1), x2) -> c18(F(0, half(s(x1)), x2)) K tuples: F(z0, s(z1), z2) -> c16(ODD(s(z1))) -'(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) -> 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 ---------------------------------------- (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(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 ---------------------------------------- (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(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: F(z0, s(z1), z2) -> c16(ODD(s(z1))) -'(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) -> 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 ---------------------------------------- (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(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] ---------------------------------------- (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(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: F(z0, s(z1), z2) -> c16(ODD(s(z1))) -'(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) -> 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 ---------------------------------------- (21) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. F(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 ---------------------------------------- (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(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: F(z0, s(z1), z2) -> c16(ODD(s(z1))) -'(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) -> 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 ---------------------------------------- (23) 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))) ---------------------------------------- (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(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: F(z0, s(z1), z2) -> c16(ODD(s(z1))) -'(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) -> 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) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing nodes: F(x0, s(0), x2) -> c19(F(*(x0, x0), 0, x2), HALF(s(0))) ---------------------------------------- (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))) F(s(z1), s(x1), x2) -> c19(F(+(*(s(z1), z1), s(z1)), half(s(x1)), x2), HALF(s(x1))) K tuples: F(z0, s(z1), z2) -> c16(ODD(s(z1))) -'(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) -> 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 ---------------------------------------- (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(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] ---------------------------------------- (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(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: F(z0, s(z1), z2) -> c16(ODD(s(z1))) -'(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) -> 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 ---------------------------------------- (29) 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 ---------------------------------------- (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(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: F(z0, s(z1), z2) -> c16(ODD(s(z1))) -'(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) -> 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) 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))) ---------------------------------------- (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(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: F(z0, s(z1), z2) -> c16(ODD(s(z1))) -'(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) -> 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) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing tuple parts ---------------------------------------- (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(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: F(z0, s(z1), z2) -> c16(ODD(s(z1))) -'(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) -> 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) 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)) ---------------------------------------- (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(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: F(z0, s(z1), z2) -> c16(ODD(s(z1))) -'(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) -> 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 ---------------------------------------- (37) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing nodes: F(0, s(0), x1) -> c18(F(0, 0, x1)) ---------------------------------------- (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))) F(0, s(s(z0)), x1) -> c18(F(0, s(half(z0)), x1)) K tuples: F(z0, s(z1), z2) -> c16(ODD(s(z1))) -'(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) -> 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 ---------------------------------------- (39) 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 ---------------------------------------- (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(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: F(z0, s(z1), z2) -> c16(ODD(s(z1))) -'(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) -> 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) 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)))) ---------------------------------------- (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(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: F(z0, s(z1), z2) -> c16(ODD(s(z1))) -'(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) -> 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) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing nodes: F(0, s(0), x1) -> c19(F(0, 0, x1), HALF(s(0))) ---------------------------------------- (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)) F(0, s(s(z0)), x1) -> c19(F(0, s(half(z0)), x1), HALF(s(s(z0)))) K tuples: F(z0, s(z1), z2) -> c16(ODD(s(z1))) -'(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) -> 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 ---------------------------------------- (45) 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 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] + x_1 POL(*'(x_1, x_2)) = 0 POL(+(x_1, x_2)) = [1] POL(-'(x_1, x_2)) = x_1 + x_2 POL(0) = 0 POL(F(x_1, x_2, x_3)) = x_2 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] + 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: HALF(s(s(z0))) -> c13(HALF(z0)) K tuples: F(z0, s(z1), z2) -> c16(ODD(s(z1))) -'(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) -> 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 ---------------------------------------- (47) 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 ---------------------------------------- (48) 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: F(z0, s(z1), z2) -> c16(ODD(s(z1))) -'(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) -> 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 ---------------------------------------- (49) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (50) BOUNDS(1, 1) ---------------------------------------- (51) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (52) 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 ---------------------------------------- (53) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID)) Converted S to standard rules, and D \ S as well as R to relative rules. ---------------------------------------- (54) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: -'(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))) The (relative) TRS S consists of the following 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)) Rewrite Strategy: INNERMOST ---------------------------------------- (55) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (56) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: -'(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))) The (relative) TRS S consists of the following 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)) Rewrite Strategy: INNERMOST ---------------------------------------- (57) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Inferred types. ---------------------------------------- (58) Obligation: Innermost TRS: Rules: -'(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))) -(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)) Types: -' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c:c1 0' :: 0':s:c2:c3:true:false:+' c :: c:c1 s :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' c1 :: c:c1 -> c:c1 *' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' c2 :: 0':s:c2:c3:true:false:+' c3 :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' IF :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c4:c5:c6:c7 true :: 0':s:c2:c3:true:false:+' c4 :: c4:c5:c6:c7 false :: 0':s:c2:c3:true:false:+' c5 :: c4:c5:c6:c7 c6 :: c4:c5:c6:c7 c7 :: c4:c5:c6:c7 ODD :: 0':s:c2:c3:true:false:+' -> c8:c9:c10 c8 :: c8:c9:c10 c9 :: c8:c9:c10 c10 :: c8:c9:c10 -> c8:c9:c10 HALF :: 0':s:c2:c3:true:false:+' -> c11:c12:c13 c11 :: c11:c12:c13 c12 :: c11:c12:c13 c13 :: c11:c12:c13 -> c11:c12:c13 POW :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c14 c14 :: c15:c16:c17:c18:c19 -> c14 F :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19 c15 :: c15:c16:c17:c18:c19 c16 :: c4:c5:c6:c7 -> c8:c9:c10 -> c15:c16:c17:c18:c19 odd :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' f :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' half :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' c17 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19 c18 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19 c19 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> c11:c12:c13 -> c15:c16:c17:c18:c19 - :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' +' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' if :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' pow :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' hole_c:c11_20 :: c:c1 hole_0':s:c2:c3:true:false:+'2_20 :: 0':s:c2:c3:true:false:+' hole_c4:c5:c6:c73_20 :: c4:c5:c6:c7 hole_c8:c9:c104_20 :: c8:c9:c10 hole_c11:c12:c135_20 :: c11:c12:c13 hole_c146_20 :: c14 hole_c15:c16:c17:c18:c197_20 :: c15:c16:c17:c18:c19 gen_c:c18_20 :: Nat -> c:c1 gen_0':s:c2:c3:true:false:+'9_20 :: Nat -> 0':s:c2:c3:true:false:+' gen_c8:c9:c1010_20 :: Nat -> c8:c9:c10 gen_c11:c12:c1311_20 :: Nat -> c11:c12:c13 gen_c15:c16:c17:c18:c1912_20 :: Nat -> c15:c16:c17:c18:c19 ---------------------------------------- (59) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: -', *', ODD, HALF, F, odd, f, half, - They will be analysed ascendingly in the following order: *' < F *' < f ODD < F HALF < F odd < F f < F half < F odd < f half < f ---------------------------------------- (60) Obligation: Innermost TRS: Rules: -'(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))) -(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)) Types: -' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c:c1 0' :: 0':s:c2:c3:true:false:+' c :: c:c1 s :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' c1 :: c:c1 -> c:c1 *' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' c2 :: 0':s:c2:c3:true:false:+' c3 :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' IF :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c4:c5:c6:c7 true :: 0':s:c2:c3:true:false:+' c4 :: c4:c5:c6:c7 false :: 0':s:c2:c3:true:false:+' c5 :: c4:c5:c6:c7 c6 :: c4:c5:c6:c7 c7 :: c4:c5:c6:c7 ODD :: 0':s:c2:c3:true:false:+' -> c8:c9:c10 c8 :: c8:c9:c10 c9 :: c8:c9:c10 c10 :: c8:c9:c10 -> c8:c9:c10 HALF :: 0':s:c2:c3:true:false:+' -> c11:c12:c13 c11 :: c11:c12:c13 c12 :: c11:c12:c13 c13 :: c11:c12:c13 -> c11:c12:c13 POW :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c14 c14 :: c15:c16:c17:c18:c19 -> c14 F :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19 c15 :: c15:c16:c17:c18:c19 c16 :: c4:c5:c6:c7 -> c8:c9:c10 -> c15:c16:c17:c18:c19 odd :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' f :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' half :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' c17 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19 c18 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19 c19 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> c11:c12:c13 -> c15:c16:c17:c18:c19 - :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' +' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' if :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' pow :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' hole_c:c11_20 :: c:c1 hole_0':s:c2:c3:true:false:+'2_20 :: 0':s:c2:c3:true:false:+' hole_c4:c5:c6:c73_20 :: c4:c5:c6:c7 hole_c8:c9:c104_20 :: c8:c9:c10 hole_c11:c12:c135_20 :: c11:c12:c13 hole_c146_20 :: c14 hole_c15:c16:c17:c18:c197_20 :: c15:c16:c17:c18:c19 gen_c:c18_20 :: Nat -> c:c1 gen_0':s:c2:c3:true:false:+'9_20 :: Nat -> 0':s:c2:c3:true:false:+' gen_c8:c9:c1010_20 :: Nat -> c8:c9:c10 gen_c11:c12:c1311_20 :: Nat -> c11:c12:c13 gen_c15:c16:c17:c18:c1912_20 :: Nat -> c15:c16:c17:c18:c19 Generator Equations: gen_c:c18_20(0) <=> c gen_c:c18_20(+(x, 1)) <=> c1(gen_c:c18_20(x)) gen_0':s:c2:c3:true:false:+'9_20(0) <=> 0' gen_0':s:c2:c3:true:false:+'9_20(+(x, 1)) <=> s(gen_0':s:c2:c3:true:false:+'9_20(x)) gen_c8:c9:c1010_20(0) <=> c8 gen_c8:c9:c1010_20(+(x, 1)) <=> c10(gen_c8:c9:c1010_20(x)) gen_c11:c12:c1311_20(0) <=> c11 gen_c11:c12:c1311_20(+(x, 1)) <=> c13(gen_c11:c12:c1311_20(x)) gen_c15:c16:c17:c18:c1912_20(0) <=> c15 gen_c15:c16:c17:c18:c1912_20(+(x, 1)) <=> c17(c4, gen_c15:c16:c17:c18:c1912_20(x), 0') The following defined symbols remain to be analysed: -', *', ODD, HALF, F, odd, f, half, - They will be analysed ascendingly in the following order: *' < F *' < f ODD < F HALF < F odd < F f < F half < F odd < f half < f ---------------------------------------- (61) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: -'(gen_0':s:c2:c3:true:false:+'9_20(n14_20), gen_0':s:c2:c3:true:false:+'9_20(n14_20)) -> gen_c:c18_20(n14_20), rt in Omega(1 + n14_20) Induction Base: -'(gen_0':s:c2:c3:true:false:+'9_20(0), gen_0':s:c2:c3:true:false:+'9_20(0)) ->_R^Omega(1) c Induction Step: -'(gen_0':s:c2:c3:true:false:+'9_20(+(n14_20, 1)), gen_0':s:c2:c3:true:false:+'9_20(+(n14_20, 1))) ->_R^Omega(1) c1(-'(gen_0':s:c2:c3:true:false:+'9_20(n14_20), gen_0':s:c2:c3:true:false:+'9_20(n14_20))) ->_IH c1(gen_c:c18_20(c15_20)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (62) Complex Obligation (BEST) ---------------------------------------- (63) Obligation: Proved the lower bound n^1 for the following obligation: Innermost TRS: Rules: -'(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))) -(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)) Types: -' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c:c1 0' :: 0':s:c2:c3:true:false:+' c :: c:c1 s :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' c1 :: c:c1 -> c:c1 *' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' c2 :: 0':s:c2:c3:true:false:+' c3 :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' IF :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c4:c5:c6:c7 true :: 0':s:c2:c3:true:false:+' c4 :: c4:c5:c6:c7 false :: 0':s:c2:c3:true:false:+' c5 :: c4:c5:c6:c7 c6 :: c4:c5:c6:c7 c7 :: c4:c5:c6:c7 ODD :: 0':s:c2:c3:true:false:+' -> c8:c9:c10 c8 :: c8:c9:c10 c9 :: c8:c9:c10 c10 :: c8:c9:c10 -> c8:c9:c10 HALF :: 0':s:c2:c3:true:false:+' -> c11:c12:c13 c11 :: c11:c12:c13 c12 :: c11:c12:c13 c13 :: c11:c12:c13 -> c11:c12:c13 POW :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c14 c14 :: c15:c16:c17:c18:c19 -> c14 F :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19 c15 :: c15:c16:c17:c18:c19 c16 :: c4:c5:c6:c7 -> c8:c9:c10 -> c15:c16:c17:c18:c19 odd :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' f :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' half :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' c17 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19 c18 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19 c19 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> c11:c12:c13 -> c15:c16:c17:c18:c19 - :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' +' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' if :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' pow :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' hole_c:c11_20 :: c:c1 hole_0':s:c2:c3:true:false:+'2_20 :: 0':s:c2:c3:true:false:+' hole_c4:c5:c6:c73_20 :: c4:c5:c6:c7 hole_c8:c9:c104_20 :: c8:c9:c10 hole_c11:c12:c135_20 :: c11:c12:c13 hole_c146_20 :: c14 hole_c15:c16:c17:c18:c197_20 :: c15:c16:c17:c18:c19 gen_c:c18_20 :: Nat -> c:c1 gen_0':s:c2:c3:true:false:+'9_20 :: Nat -> 0':s:c2:c3:true:false:+' gen_c8:c9:c1010_20 :: Nat -> c8:c9:c10 gen_c11:c12:c1311_20 :: Nat -> c11:c12:c13 gen_c15:c16:c17:c18:c1912_20 :: Nat -> c15:c16:c17:c18:c19 Generator Equations: gen_c:c18_20(0) <=> c gen_c:c18_20(+(x, 1)) <=> c1(gen_c:c18_20(x)) gen_0':s:c2:c3:true:false:+'9_20(0) <=> 0' gen_0':s:c2:c3:true:false:+'9_20(+(x, 1)) <=> s(gen_0':s:c2:c3:true:false:+'9_20(x)) gen_c8:c9:c1010_20(0) <=> c8 gen_c8:c9:c1010_20(+(x, 1)) <=> c10(gen_c8:c9:c1010_20(x)) gen_c11:c12:c1311_20(0) <=> c11 gen_c11:c12:c1311_20(+(x, 1)) <=> c13(gen_c11:c12:c1311_20(x)) gen_c15:c16:c17:c18:c1912_20(0) <=> c15 gen_c15:c16:c17:c18:c1912_20(+(x, 1)) <=> c17(c4, gen_c15:c16:c17:c18:c1912_20(x), 0') The following defined symbols remain to be analysed: -', *', ODD, HALF, F, odd, f, half, - They will be analysed ascendingly in the following order: *' < F *' < f ODD < F HALF < F odd < F f < F half < F odd < f half < f ---------------------------------------- (64) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (65) BOUNDS(n^1, INF) ---------------------------------------- (66) Obligation: Innermost TRS: Rules: -'(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))) -(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)) Types: -' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c:c1 0' :: 0':s:c2:c3:true:false:+' c :: c:c1 s :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' c1 :: c:c1 -> c:c1 *' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' c2 :: 0':s:c2:c3:true:false:+' c3 :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' IF :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c4:c5:c6:c7 true :: 0':s:c2:c3:true:false:+' c4 :: c4:c5:c6:c7 false :: 0':s:c2:c3:true:false:+' c5 :: c4:c5:c6:c7 c6 :: c4:c5:c6:c7 c7 :: c4:c5:c6:c7 ODD :: 0':s:c2:c3:true:false:+' -> c8:c9:c10 c8 :: c8:c9:c10 c9 :: c8:c9:c10 c10 :: c8:c9:c10 -> c8:c9:c10 HALF :: 0':s:c2:c3:true:false:+' -> c11:c12:c13 c11 :: c11:c12:c13 c12 :: c11:c12:c13 c13 :: c11:c12:c13 -> c11:c12:c13 POW :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c14 c14 :: c15:c16:c17:c18:c19 -> c14 F :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19 c15 :: c15:c16:c17:c18:c19 c16 :: c4:c5:c6:c7 -> c8:c9:c10 -> c15:c16:c17:c18:c19 odd :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' f :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' half :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' c17 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19 c18 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19 c19 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> c11:c12:c13 -> c15:c16:c17:c18:c19 - :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' +' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' if :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' pow :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' hole_c:c11_20 :: c:c1 hole_0':s:c2:c3:true:false:+'2_20 :: 0':s:c2:c3:true:false:+' hole_c4:c5:c6:c73_20 :: c4:c5:c6:c7 hole_c8:c9:c104_20 :: c8:c9:c10 hole_c11:c12:c135_20 :: c11:c12:c13 hole_c146_20 :: c14 hole_c15:c16:c17:c18:c197_20 :: c15:c16:c17:c18:c19 gen_c:c18_20 :: Nat -> c:c1 gen_0':s:c2:c3:true:false:+'9_20 :: Nat -> 0':s:c2:c3:true:false:+' gen_c8:c9:c1010_20 :: Nat -> c8:c9:c10 gen_c11:c12:c1311_20 :: Nat -> c11:c12:c13 gen_c15:c16:c17:c18:c1912_20 :: Nat -> c15:c16:c17:c18:c19 Lemmas: -'(gen_0':s:c2:c3:true:false:+'9_20(n14_20), gen_0':s:c2:c3:true:false:+'9_20(n14_20)) -> gen_c:c18_20(n14_20), rt in Omega(1 + n14_20) Generator Equations: gen_c:c18_20(0) <=> c gen_c:c18_20(+(x, 1)) <=> c1(gen_c:c18_20(x)) gen_0':s:c2:c3:true:false:+'9_20(0) <=> 0' gen_0':s:c2:c3:true:false:+'9_20(+(x, 1)) <=> s(gen_0':s:c2:c3:true:false:+'9_20(x)) gen_c8:c9:c1010_20(0) <=> c8 gen_c8:c9:c1010_20(+(x, 1)) <=> c10(gen_c8:c9:c1010_20(x)) gen_c11:c12:c1311_20(0) <=> c11 gen_c11:c12:c1311_20(+(x, 1)) <=> c13(gen_c11:c12:c1311_20(x)) gen_c15:c16:c17:c18:c1912_20(0) <=> c15 gen_c15:c16:c17:c18:c1912_20(+(x, 1)) <=> c17(c4, gen_c15:c16:c17:c18:c1912_20(x), 0') The following defined symbols remain to be analysed: *', ODD, HALF, F, odd, f, half, - They will be analysed ascendingly in the following order: *' < F *' < f ODD < F HALF < F odd < F f < F half < F odd < f half < f ---------------------------------------- (67) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: *'(gen_0':s:c2:c3:true:false:+'9_20(a), gen_0':s:c2:c3:true:false:+'9_20(+(1, n618_20))) -> *13_20, rt in Omega(n618_20) Induction Base: *'(gen_0':s:c2:c3:true:false:+'9_20(a), gen_0':s:c2:c3:true:false:+'9_20(+(1, 0))) Induction Step: *'(gen_0':s:c2:c3:true:false:+'9_20(a), gen_0':s:c2:c3:true:false:+'9_20(+(1, +(n618_20, 1)))) ->_R^Omega(1) c3(*'(gen_0':s:c2:c3:true:false:+'9_20(a), gen_0':s:c2:c3:true:false:+'9_20(+(1, n618_20)))) ->_IH c3(*13_20) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (68) Obligation: Innermost TRS: Rules: -'(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))) -(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)) Types: -' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c:c1 0' :: 0':s:c2:c3:true:false:+' c :: c:c1 s :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' c1 :: c:c1 -> c:c1 *' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' c2 :: 0':s:c2:c3:true:false:+' c3 :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' IF :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c4:c5:c6:c7 true :: 0':s:c2:c3:true:false:+' c4 :: c4:c5:c6:c7 false :: 0':s:c2:c3:true:false:+' c5 :: c4:c5:c6:c7 c6 :: c4:c5:c6:c7 c7 :: c4:c5:c6:c7 ODD :: 0':s:c2:c3:true:false:+' -> c8:c9:c10 c8 :: c8:c9:c10 c9 :: c8:c9:c10 c10 :: c8:c9:c10 -> c8:c9:c10 HALF :: 0':s:c2:c3:true:false:+' -> c11:c12:c13 c11 :: c11:c12:c13 c12 :: c11:c12:c13 c13 :: c11:c12:c13 -> c11:c12:c13 POW :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c14 c14 :: c15:c16:c17:c18:c19 -> c14 F :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19 c15 :: c15:c16:c17:c18:c19 c16 :: c4:c5:c6:c7 -> c8:c9:c10 -> c15:c16:c17:c18:c19 odd :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' f :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' half :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' c17 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19 c18 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19 c19 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> c11:c12:c13 -> c15:c16:c17:c18:c19 - :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' +' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' if :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' pow :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' hole_c:c11_20 :: c:c1 hole_0':s:c2:c3:true:false:+'2_20 :: 0':s:c2:c3:true:false:+' hole_c4:c5:c6:c73_20 :: c4:c5:c6:c7 hole_c8:c9:c104_20 :: c8:c9:c10 hole_c11:c12:c135_20 :: c11:c12:c13 hole_c146_20 :: c14 hole_c15:c16:c17:c18:c197_20 :: c15:c16:c17:c18:c19 gen_c:c18_20 :: Nat -> c:c1 gen_0':s:c2:c3:true:false:+'9_20 :: Nat -> 0':s:c2:c3:true:false:+' gen_c8:c9:c1010_20 :: Nat -> c8:c9:c10 gen_c11:c12:c1311_20 :: Nat -> c11:c12:c13 gen_c15:c16:c17:c18:c1912_20 :: Nat -> c15:c16:c17:c18:c19 Lemmas: -'(gen_0':s:c2:c3:true:false:+'9_20(n14_20), gen_0':s:c2:c3:true:false:+'9_20(n14_20)) -> gen_c:c18_20(n14_20), rt in Omega(1 + n14_20) *'(gen_0':s:c2:c3:true:false:+'9_20(a), gen_0':s:c2:c3:true:false:+'9_20(+(1, n618_20))) -> *13_20, rt in Omega(n618_20) Generator Equations: gen_c:c18_20(0) <=> c gen_c:c18_20(+(x, 1)) <=> c1(gen_c:c18_20(x)) gen_0':s:c2:c3:true:false:+'9_20(0) <=> 0' gen_0':s:c2:c3:true:false:+'9_20(+(x, 1)) <=> s(gen_0':s:c2:c3:true:false:+'9_20(x)) gen_c8:c9:c1010_20(0) <=> c8 gen_c8:c9:c1010_20(+(x, 1)) <=> c10(gen_c8:c9:c1010_20(x)) gen_c11:c12:c1311_20(0) <=> c11 gen_c11:c12:c1311_20(+(x, 1)) <=> c13(gen_c11:c12:c1311_20(x)) gen_c15:c16:c17:c18:c1912_20(0) <=> c15 gen_c15:c16:c17:c18:c1912_20(+(x, 1)) <=> c17(c4, gen_c15:c16:c17:c18:c1912_20(x), 0') The following defined symbols remain to be analysed: ODD, HALF, F, odd, f, half, - They will be analysed ascendingly in the following order: ODD < F HALF < F odd < F f < F half < F odd < f half < f ---------------------------------------- (69) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: ODD(gen_0':s:c2:c3:true:false:+'9_20(*(2, n3997_20))) -> gen_c8:c9:c1010_20(n3997_20), rt in Omega(1 + n3997_20) Induction Base: ODD(gen_0':s:c2:c3:true:false:+'9_20(*(2, 0))) ->_R^Omega(1) c8 Induction Step: ODD(gen_0':s:c2:c3:true:false:+'9_20(*(2, +(n3997_20, 1)))) ->_R^Omega(1) c10(ODD(gen_0':s:c2:c3:true:false:+'9_20(*(2, n3997_20)))) ->_IH c10(gen_c8:c9:c1010_20(c3998_20)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (70) Obligation: Innermost TRS: Rules: -'(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))) -(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)) Types: -' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c:c1 0' :: 0':s:c2:c3:true:false:+' c :: c:c1 s :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' c1 :: c:c1 -> c:c1 *' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' c2 :: 0':s:c2:c3:true:false:+' c3 :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' IF :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c4:c5:c6:c7 true :: 0':s:c2:c3:true:false:+' c4 :: c4:c5:c6:c7 false :: 0':s:c2:c3:true:false:+' c5 :: c4:c5:c6:c7 c6 :: c4:c5:c6:c7 c7 :: c4:c5:c6:c7 ODD :: 0':s:c2:c3:true:false:+' -> c8:c9:c10 c8 :: c8:c9:c10 c9 :: c8:c9:c10 c10 :: c8:c9:c10 -> c8:c9:c10 HALF :: 0':s:c2:c3:true:false:+' -> c11:c12:c13 c11 :: c11:c12:c13 c12 :: c11:c12:c13 c13 :: c11:c12:c13 -> c11:c12:c13 POW :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c14 c14 :: c15:c16:c17:c18:c19 -> c14 F :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19 c15 :: c15:c16:c17:c18:c19 c16 :: c4:c5:c6:c7 -> c8:c9:c10 -> c15:c16:c17:c18:c19 odd :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' f :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' half :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' c17 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19 c18 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19 c19 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> c11:c12:c13 -> c15:c16:c17:c18:c19 - :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' +' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' if :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' pow :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' hole_c:c11_20 :: c:c1 hole_0':s:c2:c3:true:false:+'2_20 :: 0':s:c2:c3:true:false:+' hole_c4:c5:c6:c73_20 :: c4:c5:c6:c7 hole_c8:c9:c104_20 :: c8:c9:c10 hole_c11:c12:c135_20 :: c11:c12:c13 hole_c146_20 :: c14 hole_c15:c16:c17:c18:c197_20 :: c15:c16:c17:c18:c19 gen_c:c18_20 :: Nat -> c:c1 gen_0':s:c2:c3:true:false:+'9_20 :: Nat -> 0':s:c2:c3:true:false:+' gen_c8:c9:c1010_20 :: Nat -> c8:c9:c10 gen_c11:c12:c1311_20 :: Nat -> c11:c12:c13 gen_c15:c16:c17:c18:c1912_20 :: Nat -> c15:c16:c17:c18:c19 Lemmas: -'(gen_0':s:c2:c3:true:false:+'9_20(n14_20), gen_0':s:c2:c3:true:false:+'9_20(n14_20)) -> gen_c:c18_20(n14_20), rt in Omega(1 + n14_20) *'(gen_0':s:c2:c3:true:false:+'9_20(a), gen_0':s:c2:c3:true:false:+'9_20(+(1, n618_20))) -> *13_20, rt in Omega(n618_20) ODD(gen_0':s:c2:c3:true:false:+'9_20(*(2, n3997_20))) -> gen_c8:c9:c1010_20(n3997_20), rt in Omega(1 + n3997_20) Generator Equations: gen_c:c18_20(0) <=> c gen_c:c18_20(+(x, 1)) <=> c1(gen_c:c18_20(x)) gen_0':s:c2:c3:true:false:+'9_20(0) <=> 0' gen_0':s:c2:c3:true:false:+'9_20(+(x, 1)) <=> s(gen_0':s:c2:c3:true:false:+'9_20(x)) gen_c8:c9:c1010_20(0) <=> c8 gen_c8:c9:c1010_20(+(x, 1)) <=> c10(gen_c8:c9:c1010_20(x)) gen_c11:c12:c1311_20(0) <=> c11 gen_c11:c12:c1311_20(+(x, 1)) <=> c13(gen_c11:c12:c1311_20(x)) gen_c15:c16:c17:c18:c1912_20(0) <=> c15 gen_c15:c16:c17:c18:c1912_20(+(x, 1)) <=> c17(c4, gen_c15:c16:c17:c18:c1912_20(x), 0') The following defined symbols remain to be analysed: HALF, F, odd, f, half, - They will be analysed ascendingly in the following order: HALF < F odd < F f < F half < F odd < f half < f ---------------------------------------- (71) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: HALF(gen_0':s:c2:c3:true:false:+'9_20(*(2, n4781_20))) -> gen_c11:c12:c1311_20(n4781_20), rt in Omega(1 + n4781_20) Induction Base: HALF(gen_0':s:c2:c3:true:false:+'9_20(*(2, 0))) ->_R^Omega(1) c11 Induction Step: HALF(gen_0':s:c2:c3:true:false:+'9_20(*(2, +(n4781_20, 1)))) ->_R^Omega(1) c13(HALF(gen_0':s:c2:c3:true:false:+'9_20(*(2, n4781_20)))) ->_IH c13(gen_c11:c12:c1311_20(c4782_20)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (72) Obligation: Innermost TRS: Rules: -'(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))) -(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)) Types: -' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c:c1 0' :: 0':s:c2:c3:true:false:+' c :: c:c1 s :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' c1 :: c:c1 -> c:c1 *' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' c2 :: 0':s:c2:c3:true:false:+' c3 :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' IF :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c4:c5:c6:c7 true :: 0':s:c2:c3:true:false:+' c4 :: c4:c5:c6:c7 false :: 0':s:c2:c3:true:false:+' c5 :: c4:c5:c6:c7 c6 :: c4:c5:c6:c7 c7 :: c4:c5:c6:c7 ODD :: 0':s:c2:c3:true:false:+' -> c8:c9:c10 c8 :: c8:c9:c10 c9 :: c8:c9:c10 c10 :: c8:c9:c10 -> c8:c9:c10 HALF :: 0':s:c2:c3:true:false:+' -> c11:c12:c13 c11 :: c11:c12:c13 c12 :: c11:c12:c13 c13 :: c11:c12:c13 -> c11:c12:c13 POW :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c14 c14 :: c15:c16:c17:c18:c19 -> c14 F :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19 c15 :: c15:c16:c17:c18:c19 c16 :: c4:c5:c6:c7 -> c8:c9:c10 -> c15:c16:c17:c18:c19 odd :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' f :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' half :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' c17 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19 c18 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19 c19 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> c11:c12:c13 -> c15:c16:c17:c18:c19 - :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' +' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' if :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' pow :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' hole_c:c11_20 :: c:c1 hole_0':s:c2:c3:true:false:+'2_20 :: 0':s:c2:c3:true:false:+' hole_c4:c5:c6:c73_20 :: c4:c5:c6:c7 hole_c8:c9:c104_20 :: c8:c9:c10 hole_c11:c12:c135_20 :: c11:c12:c13 hole_c146_20 :: c14 hole_c15:c16:c17:c18:c197_20 :: c15:c16:c17:c18:c19 gen_c:c18_20 :: Nat -> c:c1 gen_0':s:c2:c3:true:false:+'9_20 :: Nat -> 0':s:c2:c3:true:false:+' gen_c8:c9:c1010_20 :: Nat -> c8:c9:c10 gen_c11:c12:c1311_20 :: Nat -> c11:c12:c13 gen_c15:c16:c17:c18:c1912_20 :: Nat -> c15:c16:c17:c18:c19 Lemmas: -'(gen_0':s:c2:c3:true:false:+'9_20(n14_20), gen_0':s:c2:c3:true:false:+'9_20(n14_20)) -> gen_c:c18_20(n14_20), rt in Omega(1 + n14_20) *'(gen_0':s:c2:c3:true:false:+'9_20(a), gen_0':s:c2:c3:true:false:+'9_20(+(1, n618_20))) -> *13_20, rt in Omega(n618_20) ODD(gen_0':s:c2:c3:true:false:+'9_20(*(2, n3997_20))) -> gen_c8:c9:c1010_20(n3997_20), rt in Omega(1 + n3997_20) HALF(gen_0':s:c2:c3:true:false:+'9_20(*(2, n4781_20))) -> gen_c11:c12:c1311_20(n4781_20), rt in Omega(1 + n4781_20) Generator Equations: gen_c:c18_20(0) <=> c gen_c:c18_20(+(x, 1)) <=> c1(gen_c:c18_20(x)) gen_0':s:c2:c3:true:false:+'9_20(0) <=> 0' gen_0':s:c2:c3:true:false:+'9_20(+(x, 1)) <=> s(gen_0':s:c2:c3:true:false:+'9_20(x)) gen_c8:c9:c1010_20(0) <=> c8 gen_c8:c9:c1010_20(+(x, 1)) <=> c10(gen_c8:c9:c1010_20(x)) gen_c11:c12:c1311_20(0) <=> c11 gen_c11:c12:c1311_20(+(x, 1)) <=> c13(gen_c11:c12:c1311_20(x)) gen_c15:c16:c17:c18:c1912_20(0) <=> c15 gen_c15:c16:c17:c18:c1912_20(+(x, 1)) <=> c17(c4, gen_c15:c16:c17:c18:c1912_20(x), 0') The following defined symbols remain to be analysed: odd, F, f, half, - They will be analysed ascendingly in the following order: odd < F f < F half < F odd < f half < f ---------------------------------------- (73) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: odd(gen_0':s:c2:c3:true:false:+'9_20(*(2, n5603_20))) -> false, rt in Omega(0) Induction Base: odd(gen_0':s:c2:c3:true:false:+'9_20(*(2, 0))) ->_R^Omega(0) false Induction Step: odd(gen_0':s:c2:c3:true:false:+'9_20(*(2, +(n5603_20, 1)))) ->_R^Omega(0) odd(gen_0':s:c2:c3:true:false:+'9_20(*(2, n5603_20))) ->_IH false We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (74) Obligation: Innermost TRS: Rules: -'(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))) -(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)) Types: -' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c:c1 0' :: 0':s:c2:c3:true:false:+' c :: c:c1 s :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' c1 :: c:c1 -> c:c1 *' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' c2 :: 0':s:c2:c3:true:false:+' c3 :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' IF :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c4:c5:c6:c7 true :: 0':s:c2:c3:true:false:+' c4 :: c4:c5:c6:c7 false :: 0':s:c2:c3:true:false:+' c5 :: c4:c5:c6:c7 c6 :: c4:c5:c6:c7 c7 :: c4:c5:c6:c7 ODD :: 0':s:c2:c3:true:false:+' -> c8:c9:c10 c8 :: c8:c9:c10 c9 :: c8:c9:c10 c10 :: c8:c9:c10 -> c8:c9:c10 HALF :: 0':s:c2:c3:true:false:+' -> c11:c12:c13 c11 :: c11:c12:c13 c12 :: c11:c12:c13 c13 :: c11:c12:c13 -> c11:c12:c13 POW :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c14 c14 :: c15:c16:c17:c18:c19 -> c14 F :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19 c15 :: c15:c16:c17:c18:c19 c16 :: c4:c5:c6:c7 -> c8:c9:c10 -> c15:c16:c17:c18:c19 odd :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' f :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' half :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' c17 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19 c18 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19 c19 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> c11:c12:c13 -> c15:c16:c17:c18:c19 - :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' +' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' if :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' pow :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' hole_c:c11_20 :: c:c1 hole_0':s:c2:c3:true:false:+'2_20 :: 0':s:c2:c3:true:false:+' hole_c4:c5:c6:c73_20 :: c4:c5:c6:c7 hole_c8:c9:c104_20 :: c8:c9:c10 hole_c11:c12:c135_20 :: c11:c12:c13 hole_c146_20 :: c14 hole_c15:c16:c17:c18:c197_20 :: c15:c16:c17:c18:c19 gen_c:c18_20 :: Nat -> c:c1 gen_0':s:c2:c3:true:false:+'9_20 :: Nat -> 0':s:c2:c3:true:false:+' gen_c8:c9:c1010_20 :: Nat -> c8:c9:c10 gen_c11:c12:c1311_20 :: Nat -> c11:c12:c13 gen_c15:c16:c17:c18:c1912_20 :: Nat -> c15:c16:c17:c18:c19 Lemmas: -'(gen_0':s:c2:c3:true:false:+'9_20(n14_20), gen_0':s:c2:c3:true:false:+'9_20(n14_20)) -> gen_c:c18_20(n14_20), rt in Omega(1 + n14_20) *'(gen_0':s:c2:c3:true:false:+'9_20(a), gen_0':s:c2:c3:true:false:+'9_20(+(1, n618_20))) -> *13_20, rt in Omega(n618_20) ODD(gen_0':s:c2:c3:true:false:+'9_20(*(2, n3997_20))) -> gen_c8:c9:c1010_20(n3997_20), rt in Omega(1 + n3997_20) HALF(gen_0':s:c2:c3:true:false:+'9_20(*(2, n4781_20))) -> gen_c11:c12:c1311_20(n4781_20), rt in Omega(1 + n4781_20) odd(gen_0':s:c2:c3:true:false:+'9_20(*(2, n5603_20))) -> false, rt in Omega(0) Generator Equations: gen_c:c18_20(0) <=> c gen_c:c18_20(+(x, 1)) <=> c1(gen_c:c18_20(x)) gen_0':s:c2:c3:true:false:+'9_20(0) <=> 0' gen_0':s:c2:c3:true:false:+'9_20(+(x, 1)) <=> s(gen_0':s:c2:c3:true:false:+'9_20(x)) gen_c8:c9:c1010_20(0) <=> c8 gen_c8:c9:c1010_20(+(x, 1)) <=> c10(gen_c8:c9:c1010_20(x)) gen_c11:c12:c1311_20(0) <=> c11 gen_c11:c12:c1311_20(+(x, 1)) <=> c13(gen_c11:c12:c1311_20(x)) gen_c15:c16:c17:c18:c1912_20(0) <=> c15 gen_c15:c16:c17:c18:c1912_20(+(x, 1)) <=> c17(c4, gen_c15:c16:c17:c18:c1912_20(x), 0') The following defined symbols remain to be analysed: half, F, f, - They will be analysed ascendingly in the following order: f < F half < F half < f ---------------------------------------- (75) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: half(gen_0':s:c2:c3:true:false:+'9_20(*(2, n5961_20))) -> gen_0':s:c2:c3:true:false:+'9_20(n5961_20), rt in Omega(0) Induction Base: half(gen_0':s:c2:c3:true:false:+'9_20(*(2, 0))) ->_R^Omega(0) 0' Induction Step: half(gen_0':s:c2:c3:true:false:+'9_20(*(2, +(n5961_20, 1)))) ->_R^Omega(0) s(half(gen_0':s:c2:c3:true:false:+'9_20(*(2, n5961_20)))) ->_IH s(gen_0':s:c2:c3:true:false:+'9_20(c5962_20)) We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (76) Obligation: Innermost TRS: Rules: -'(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))) -(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)) Types: -' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c:c1 0' :: 0':s:c2:c3:true:false:+' c :: c:c1 s :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' c1 :: c:c1 -> c:c1 *' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' c2 :: 0':s:c2:c3:true:false:+' c3 :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' IF :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c4:c5:c6:c7 true :: 0':s:c2:c3:true:false:+' c4 :: c4:c5:c6:c7 false :: 0':s:c2:c3:true:false:+' c5 :: c4:c5:c6:c7 c6 :: c4:c5:c6:c7 c7 :: c4:c5:c6:c7 ODD :: 0':s:c2:c3:true:false:+' -> c8:c9:c10 c8 :: c8:c9:c10 c9 :: c8:c9:c10 c10 :: c8:c9:c10 -> c8:c9:c10 HALF :: 0':s:c2:c3:true:false:+' -> c11:c12:c13 c11 :: c11:c12:c13 c12 :: c11:c12:c13 c13 :: c11:c12:c13 -> c11:c12:c13 POW :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c14 c14 :: c15:c16:c17:c18:c19 -> c14 F :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19 c15 :: c15:c16:c17:c18:c19 c16 :: c4:c5:c6:c7 -> c8:c9:c10 -> c15:c16:c17:c18:c19 odd :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' f :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' half :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' c17 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19 c18 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19 c19 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> c11:c12:c13 -> c15:c16:c17:c18:c19 - :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' +' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' if :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' pow :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' hole_c:c11_20 :: c:c1 hole_0':s:c2:c3:true:false:+'2_20 :: 0':s:c2:c3:true:false:+' hole_c4:c5:c6:c73_20 :: c4:c5:c6:c7 hole_c8:c9:c104_20 :: c8:c9:c10 hole_c11:c12:c135_20 :: c11:c12:c13 hole_c146_20 :: c14 hole_c15:c16:c17:c18:c197_20 :: c15:c16:c17:c18:c19 gen_c:c18_20 :: Nat -> c:c1 gen_0':s:c2:c3:true:false:+'9_20 :: Nat -> 0':s:c2:c3:true:false:+' gen_c8:c9:c1010_20 :: Nat -> c8:c9:c10 gen_c11:c12:c1311_20 :: Nat -> c11:c12:c13 gen_c15:c16:c17:c18:c1912_20 :: Nat -> c15:c16:c17:c18:c19 Lemmas: -'(gen_0':s:c2:c3:true:false:+'9_20(n14_20), gen_0':s:c2:c3:true:false:+'9_20(n14_20)) -> gen_c:c18_20(n14_20), rt in Omega(1 + n14_20) *'(gen_0':s:c2:c3:true:false:+'9_20(a), gen_0':s:c2:c3:true:false:+'9_20(+(1, n618_20))) -> *13_20, rt in Omega(n618_20) ODD(gen_0':s:c2:c3:true:false:+'9_20(*(2, n3997_20))) -> gen_c8:c9:c1010_20(n3997_20), rt in Omega(1 + n3997_20) HALF(gen_0':s:c2:c3:true:false:+'9_20(*(2, n4781_20))) -> gen_c11:c12:c1311_20(n4781_20), rt in Omega(1 + n4781_20) odd(gen_0':s:c2:c3:true:false:+'9_20(*(2, n5603_20))) -> false, rt in Omega(0) half(gen_0':s:c2:c3:true:false:+'9_20(*(2, n5961_20))) -> gen_0':s:c2:c3:true:false:+'9_20(n5961_20), rt in Omega(0) Generator Equations: gen_c:c18_20(0) <=> c gen_c:c18_20(+(x, 1)) <=> c1(gen_c:c18_20(x)) gen_0':s:c2:c3:true:false:+'9_20(0) <=> 0' gen_0':s:c2:c3:true:false:+'9_20(+(x, 1)) <=> s(gen_0':s:c2:c3:true:false:+'9_20(x)) gen_c8:c9:c1010_20(0) <=> c8 gen_c8:c9:c1010_20(+(x, 1)) <=> c10(gen_c8:c9:c1010_20(x)) gen_c11:c12:c1311_20(0) <=> c11 gen_c11:c12:c1311_20(+(x, 1)) <=> c13(gen_c11:c12:c1311_20(x)) gen_c15:c16:c17:c18:c1912_20(0) <=> c15 gen_c15:c16:c17:c18:c1912_20(+(x, 1)) <=> c17(c4, gen_c15:c16:c17:c18:c1912_20(x), 0') The following defined symbols remain to be analysed: f, F, - They will be analysed ascendingly in the following order: f < F ---------------------------------------- (77) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: -(gen_0':s:c2:c3:true:false:+'9_20(n24373_20), gen_0':s:c2:c3:true:false:+'9_20(n24373_20)) -> gen_0':s:c2:c3:true:false:+'9_20(0), rt in Omega(0) Induction Base: -(gen_0':s:c2:c3:true:false:+'9_20(0), gen_0':s:c2:c3:true:false:+'9_20(0)) ->_R^Omega(0) gen_0':s:c2:c3:true:false:+'9_20(0) Induction Step: -(gen_0':s:c2:c3:true:false:+'9_20(+(n24373_20, 1)), gen_0':s:c2:c3:true:false:+'9_20(+(n24373_20, 1))) ->_R^Omega(0) -(gen_0':s:c2:c3:true:false:+'9_20(n24373_20), gen_0':s:c2:c3:true:false:+'9_20(n24373_20)) ->_IH gen_0':s:c2:c3:true:false:+'9_20(0) We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (78) BOUNDS(1, INF)