WORST_CASE(Omega(n^1),O(n^1)) proof of /export/starexec/sandbox/benchmark/theBenchmark.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 452 ms] (2) CpxRelTRS (3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (4) CdtProblem (5) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms] (6) CdtProblem (7) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CdtProblem (9) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (10) CdtProblem (11) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 137 ms] (12) CdtProblem (13) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (14) CdtProblem (15) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 56 ms] (16) CdtProblem (17) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (18) CdtProblem (19) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 51 ms] (20) CdtProblem (21) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (22) CdtProblem (23) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 51 ms] (24) CdtProblem (25) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 33 ms] (26) CdtProblem (27) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (28) CdtProblem (29) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 31 ms] (30) CdtProblem (31) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 27 ms] (32) CdtProblem (33) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (34) CdtProblem (35) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 26 ms] (36) CdtProblem (37) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 27 ms] (38) CdtProblem (39) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 33 ms] (40) CdtProblem (41) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms] (42) BOUNDS(1, 1) (43) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (44) TRS for Loop Detection (45) DecreasingLoopProof [LOWER BOUND(ID), 0 ms] (46) BEST (47) proven lower bound (48) LowerBoundPropagationProof [FINISHED, 0 ms] (49) BOUNDS(n^1, INF) (50) TRS for Loop Detection ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: F_0(z0) -> c F_1(z0) -> c1(G_1(z0, z0)) G_1(s(z0), z1) -> c2(F_0(z1)) G_1(s(z0), z1) -> c3(G_1(z0, z1)) F_2(z0) -> c4(G_2(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_3(z0) -> c7(G_3(z0, z0)) G_3(s(z0), z1) -> c8(F_2(z1)) G_3(s(z0), z1) -> c9(G_3(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) F_5(z0) -> c13(G_5(z0, z0)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) F_10(z0) -> c28(G_10(z0, z0)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(z0, z1)) The (relative) TRS S consists of the following rules: f_0(z0) -> a f_1(z0) -> g_1(z0, z0) g_1(s(z0), z1) -> b(f_0(z1), g_1(z0, z1)) f_2(z0) -> g_2(z0, z0) g_2(s(z0), z1) -> b(f_1(z1), g_2(z0, z1)) f_3(z0) -> g_3(z0, z0) g_3(s(z0), z1) -> b(f_2(z1), g_3(z0, z1)) f_4(z0) -> g_4(z0, z0) g_4(s(z0), z1) -> b(f_3(z1), g_4(z0, z1)) f_5(z0) -> g_5(z0, z0) g_5(s(z0), z1) -> b(f_4(z1), g_5(z0, z1)) f_6(z0) -> g_6(z0, z0) g_6(s(z0), z1) -> b(f_5(z1), g_6(z0, z1)) f_7(z0) -> g_7(z0, z0) g_7(s(z0), z1) -> b(f_6(z1), g_7(z0, z1)) f_8(z0) -> g_8(z0, z0) g_8(s(z0), z1) -> b(f_7(z1), g_8(z0, z1)) f_9(z0) -> g_9(z0, z0) g_9(s(z0), z1) -> b(f_8(z1), g_9(z0, z1)) f_10(z0) -> g_10(z0, z0) g_10(s(z0), z1) -> b(f_9(z1), g_10(z0, z1)) Rewrite Strategy: INNERMOST ---------------------------------------- (1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID)) proved innermost termination of relative rules ---------------------------------------- (2) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: F_0(z0) -> c F_1(z0) -> c1(G_1(z0, z0)) G_1(s(z0), z1) -> c2(F_0(z1)) G_1(s(z0), z1) -> c3(G_1(z0, z1)) F_2(z0) -> c4(G_2(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_3(z0) -> c7(G_3(z0, z0)) G_3(s(z0), z1) -> c8(F_2(z1)) G_3(s(z0), z1) -> c9(G_3(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) F_5(z0) -> c13(G_5(z0, z0)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) F_10(z0) -> c28(G_10(z0, z0)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(z0, z1)) The (relative) TRS S consists of the following rules: f_0(z0) -> a f_1(z0) -> g_1(z0, z0) g_1(s(z0), z1) -> b(f_0(z1), g_1(z0, z1)) f_2(z0) -> g_2(z0, z0) g_2(s(z0), z1) -> b(f_1(z1), g_2(z0, z1)) f_3(z0) -> g_3(z0, z0) g_3(s(z0), z1) -> b(f_2(z1), g_3(z0, z1)) f_4(z0) -> g_4(z0, z0) g_4(s(z0), z1) -> b(f_3(z1), g_4(z0, z1)) f_5(z0) -> g_5(z0, z0) g_5(s(z0), z1) -> b(f_4(z1), g_5(z0, z1)) f_6(z0) -> g_6(z0, z0) g_6(s(z0), z1) -> b(f_5(z1), g_6(z0, z1)) f_7(z0) -> g_7(z0, z0) g_7(s(z0), z1) -> b(f_6(z1), g_7(z0, z1)) f_8(z0) -> g_8(z0, z0) g_8(s(z0), z1) -> b(f_7(z1), g_8(z0, z1)) f_9(z0) -> g_9(z0, z0) g_9(s(z0), z1) -> b(f_8(z1), g_9(z0, z1)) f_10(z0) -> g_10(z0, z0) g_10(s(z0), z1) -> b(f_9(z1), g_10(z0, z1)) Rewrite Strategy: INNERMOST ---------------------------------------- (3) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS to CDT ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: f_0(z0) -> a f_1(z0) -> g_1(z0, z0) g_1(s(z0), z1) -> b(f_0(z1), g_1(z0, z1)) f_2(z0) -> g_2(z0, z0) g_2(s(z0), z1) -> b(f_1(z1), g_2(z0, z1)) f_3(z0) -> g_3(z0, z0) g_3(s(z0), z1) -> b(f_2(z1), g_3(z0, z1)) f_4(z0) -> g_4(z0, z0) g_4(s(z0), z1) -> b(f_3(z1), g_4(z0, z1)) f_5(z0) -> g_5(z0, z0) g_5(s(z0), z1) -> b(f_4(z1), g_5(z0, z1)) f_6(z0) -> g_6(z0, z0) g_6(s(z0), z1) -> b(f_5(z1), g_6(z0, z1)) f_7(z0) -> g_7(z0, z0) g_7(s(z0), z1) -> b(f_6(z1), g_7(z0, z1)) f_8(z0) -> g_8(z0, z0) g_8(s(z0), z1) -> b(f_7(z1), g_8(z0, z1)) f_9(z0) -> g_9(z0, z0) g_9(s(z0), z1) -> b(f_8(z1), g_9(z0, z1)) f_10(z0) -> g_10(z0, z0) g_10(s(z0), z1) -> b(f_9(z1), g_10(z0, z1)) F_0(z0) -> c F_1(z0) -> c1(G_1(z0, z0)) G_1(s(z0), z1) -> c2(F_0(z1)) G_1(s(z0), z1) -> c3(G_1(z0, z1)) F_2(z0) -> c4(G_2(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_3(z0) -> c7(G_3(z0, z0)) G_3(s(z0), z1) -> c8(F_2(z1)) G_3(s(z0), z1) -> c9(G_3(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) F_5(z0) -> c13(G_5(z0, z0)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) F_10(z0) -> c28(G_10(z0, z0)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(z0, z1)) Tuples: F_0'(z0) -> c31 F_1'(z0) -> c32(G_1'(z0, z0)) G_1'(s(z0), z1) -> c33(F_0'(z1), G_1'(z0, z1)) F_2'(z0) -> c34(G_2'(z0, z0)) G_2'(s(z0), z1) -> c35(F_1'(z1), G_2'(z0, z1)) F_3'(z0) -> c36(G_3'(z0, z0)) G_3'(s(z0), z1) -> c37(F_2'(z1), G_3'(z0, z1)) F_4'(z0) -> c38(G_4'(z0, z0)) G_4'(s(z0), z1) -> c39(F_3'(z1), G_4'(z0, z1)) F_5'(z0) -> c40(G_5'(z0, z0)) G_5'(s(z0), z1) -> c41(F_4'(z1), G_5'(z0, z1)) F_6'(z0) -> c42(G_6'(z0, z0)) G_6'(s(z0), z1) -> c43(F_5'(z1), G_6'(z0, z1)) F_7'(z0) -> c44(G_7'(z0, z0)) G_7'(s(z0), z1) -> c45(F_6'(z1), G_7'(z0, z1)) F_8'(z0) -> c46(G_8'(z0, z0)) G_8'(s(z0), z1) -> c47(F_7'(z1), G_8'(z0, z1)) F_9'(z0) -> c48(G_9'(z0, z0)) G_9'(s(z0), z1) -> c49(F_8'(z1), G_9'(z0, z1)) F_10'(z0) -> c50(G_10'(z0, z0)) G_10'(s(z0), z1) -> c51(F_9'(z1), G_10'(z0, z1)) F_0''(z0) -> c52 F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c54(F_0''(z1)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) F_10''(z0) -> c80(G_10''(z0, z0)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) S tuples: F_0''(z0) -> c52 F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c54(F_0''(z1)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) F_10''(z0) -> c80(G_10''(z0, z0)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) K tuples:none Defined Rule Symbols: F_0_1, F_1_1, G_1_2, F_2_1, G_2_2, F_3_1, G_3_2, F_4_1, G_4_2, F_5_1, G_5_2, F_6_1, G_6_2, F_7_1, G_7_2, F_8_1, G_8_2, F_9_1, G_9_2, F_10_1, G_10_2, f_0_1, f_1_1, g_1_2, f_2_1, g_2_2, f_3_1, g_3_2, f_4_1, g_4_2, f_5_1, g_5_2, f_6_1, g_6_2, f_7_1, g_7_2, f_8_1, g_8_2, f_9_1, g_9_2, f_10_1, g_10_2 Defined Pair Symbols: F_0'_1, F_1'_1, G_1'_2, F_2'_1, G_2'_2, F_3'_1, G_3'_2, F_4'_1, G_4'_2, F_5'_1, G_5'_2, F_6'_1, G_6'_2, F_7'_1, G_7'_2, F_8'_1, G_8'_2, F_9'_1, G_9'_2, F_10'_1, G_10'_2, F_0''_1, F_1''_1, G_1''_2, F_2''_1, G_2''_2, F_3''_1, G_3''_2, F_4''_1, G_4''_2, F_5''_1, G_5''_2, F_6''_1, G_6''_2, F_7''_1, G_7''_2, F_8''_1, G_8''_2, F_9''_1, G_9''_2, F_10''_1, G_10''_2 Compound Symbols: c31, c32_1, c33_2, c34_1, c35_2, c36_1, c37_2, c38_1, c39_2, c40_1, c41_2, c42_1, c43_2, c44_1, c45_2, c46_1, c47_2, c48_1, c49_2, c50_1, c51_2, c52, c53_1, c54_1, c55_1, c56_1, c57_1, c58_1, c59_1, c60_1, c61_1, c62_1, c63_1, c64_1, c65_1, c66_1, c67_1, c68_1, c69_1, c70_1, c71_1, c72_1, c73_1, c74_1, c75_1, c76_1, c77_1, c78_1, c79_1, c80_1, c81_1, c82_1 ---------------------------------------- (5) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 2 leading nodes: F_10'(z0) -> c50(G_10'(z0, z0)) F_10''(z0) -> c80(G_10''(z0, z0)) Removed 3 trailing nodes: G_1''(s(z0), z1) -> c54(F_0''(z1)) F_0'(z0) -> c31 F_0''(z0) -> c52 ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: f_0(z0) -> a f_1(z0) -> g_1(z0, z0) g_1(s(z0), z1) -> b(f_0(z1), g_1(z0, z1)) f_2(z0) -> g_2(z0, z0) g_2(s(z0), z1) -> b(f_1(z1), g_2(z0, z1)) f_3(z0) -> g_3(z0, z0) g_3(s(z0), z1) -> b(f_2(z1), g_3(z0, z1)) f_4(z0) -> g_4(z0, z0) g_4(s(z0), z1) -> b(f_3(z1), g_4(z0, z1)) f_5(z0) -> g_5(z0, z0) g_5(s(z0), z1) -> b(f_4(z1), g_5(z0, z1)) f_6(z0) -> g_6(z0, z0) g_6(s(z0), z1) -> b(f_5(z1), g_6(z0, z1)) f_7(z0) -> g_7(z0, z0) g_7(s(z0), z1) -> b(f_6(z1), g_7(z0, z1)) f_8(z0) -> g_8(z0, z0) g_8(s(z0), z1) -> b(f_7(z1), g_8(z0, z1)) f_9(z0) -> g_9(z0, z0) g_9(s(z0), z1) -> b(f_8(z1), g_9(z0, z1)) f_10(z0) -> g_10(z0, z0) g_10(s(z0), z1) -> b(f_9(z1), g_10(z0, z1)) F_0(z0) -> c F_1(z0) -> c1(G_1(z0, z0)) G_1(s(z0), z1) -> c2(F_0(z1)) G_1(s(z0), z1) -> c3(G_1(z0, z1)) F_2(z0) -> c4(G_2(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_3(z0) -> c7(G_3(z0, z0)) G_3(s(z0), z1) -> c8(F_2(z1)) G_3(s(z0), z1) -> c9(G_3(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) F_5(z0) -> c13(G_5(z0, z0)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) F_10(z0) -> c28(G_10(z0, z0)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(z0, z1)) Tuples: F_1'(z0) -> c32(G_1'(z0, z0)) G_1'(s(z0), z1) -> c33(F_0'(z1), G_1'(z0, z1)) F_2'(z0) -> c34(G_2'(z0, z0)) G_2'(s(z0), z1) -> c35(F_1'(z1), G_2'(z0, z1)) F_3'(z0) -> c36(G_3'(z0, z0)) G_3'(s(z0), z1) -> c37(F_2'(z1), G_3'(z0, z1)) F_4'(z0) -> c38(G_4'(z0, z0)) G_4'(s(z0), z1) -> c39(F_3'(z1), G_4'(z0, z1)) F_5'(z0) -> c40(G_5'(z0, z0)) G_5'(s(z0), z1) -> c41(F_4'(z1), G_5'(z0, z1)) F_6'(z0) -> c42(G_6'(z0, z0)) G_6'(s(z0), z1) -> c43(F_5'(z1), G_6'(z0, z1)) F_7'(z0) -> c44(G_7'(z0, z0)) G_7'(s(z0), z1) -> c45(F_6'(z1), G_7'(z0, z1)) F_8'(z0) -> c46(G_8'(z0, z0)) G_8'(s(z0), z1) -> c47(F_7'(z1), G_8'(z0, z1)) F_9'(z0) -> c48(G_9'(z0, z0)) G_9'(s(z0), z1) -> c49(F_8'(z1), G_9'(z0, z1)) G_10'(s(z0), z1) -> c51(F_9'(z1), G_10'(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) S tuples: F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) K tuples:none Defined Rule Symbols: F_0_1, F_1_1, G_1_2, F_2_1, G_2_2, F_3_1, G_3_2, F_4_1, G_4_2, F_5_1, G_5_2, F_6_1, G_6_2, F_7_1, G_7_2, F_8_1, G_8_2, F_9_1, G_9_2, F_10_1, G_10_2, f_0_1, f_1_1, g_1_2, f_2_1, g_2_2, f_3_1, g_3_2, f_4_1, g_4_2, f_5_1, g_5_2, f_6_1, g_6_2, f_7_1, g_7_2, f_8_1, g_8_2, f_9_1, g_9_2, f_10_1, g_10_2 Defined Pair Symbols: F_1'_1, G_1'_2, F_2'_1, G_2'_2, F_3'_1, G_3'_2, F_4'_1, G_4'_2, F_5'_1, G_5'_2, F_6'_1, G_6'_2, F_7'_1, G_7'_2, F_8'_1, G_8'_2, F_9'_1, G_9'_2, G_10'_2, F_1''_1, G_1''_2, F_2''_1, G_2''_2, F_3''_1, G_3''_2, F_4''_1, G_4''_2, F_5''_1, G_5''_2, F_6''_1, G_6''_2, F_7''_1, G_7''_2, F_8''_1, G_8''_2, F_9''_1, G_9''_2, G_10''_2 Compound Symbols: c32_1, c33_2, c34_1, c35_2, c36_1, c37_2, c38_1, c39_2, c40_1, c41_2, c42_1, c43_2, c44_1, c45_2, c46_1, c47_2, c48_1, c49_2, c51_2, c53_1, c55_1, c56_1, c57_1, c58_1, c59_1, c60_1, c61_1, c62_1, c63_1, c64_1, c65_1, c66_1, c67_1, c68_1, c69_1, c70_1, c71_1, c72_1, c73_1, c74_1, c75_1, c76_1, c77_1, c78_1, c79_1, c81_1, c82_1 ---------------------------------------- (7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing tuple parts ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules: f_0(z0) -> a f_1(z0) -> g_1(z0, z0) g_1(s(z0), z1) -> b(f_0(z1), g_1(z0, z1)) f_2(z0) -> g_2(z0, z0) g_2(s(z0), z1) -> b(f_1(z1), g_2(z0, z1)) f_3(z0) -> g_3(z0, z0) g_3(s(z0), z1) -> b(f_2(z1), g_3(z0, z1)) f_4(z0) -> g_4(z0, z0) g_4(s(z0), z1) -> b(f_3(z1), g_4(z0, z1)) f_5(z0) -> g_5(z0, z0) g_5(s(z0), z1) -> b(f_4(z1), g_5(z0, z1)) f_6(z0) -> g_6(z0, z0) g_6(s(z0), z1) -> b(f_5(z1), g_6(z0, z1)) f_7(z0) -> g_7(z0, z0) g_7(s(z0), z1) -> b(f_6(z1), g_7(z0, z1)) f_8(z0) -> g_8(z0, z0) g_8(s(z0), z1) -> b(f_7(z1), g_8(z0, z1)) f_9(z0) -> g_9(z0, z0) g_9(s(z0), z1) -> b(f_8(z1), g_9(z0, z1)) f_10(z0) -> g_10(z0, z0) g_10(s(z0), z1) -> b(f_9(z1), g_10(z0, z1)) F_0(z0) -> c F_1(z0) -> c1(G_1(z0, z0)) G_1(s(z0), z1) -> c2(F_0(z1)) G_1(s(z0), z1) -> c3(G_1(z0, z1)) F_2(z0) -> c4(G_2(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_3(z0) -> c7(G_3(z0, z0)) G_3(s(z0), z1) -> c8(F_2(z1)) G_3(s(z0), z1) -> c9(G_3(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) F_5(z0) -> c13(G_5(z0, z0)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) F_10(z0) -> c28(G_10(z0, z0)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(z0, z1)) Tuples: F_1'(z0) -> c32(G_1'(z0, z0)) F_2'(z0) -> c34(G_2'(z0, z0)) G_2'(s(z0), z1) -> c35(F_1'(z1), G_2'(z0, z1)) F_3'(z0) -> c36(G_3'(z0, z0)) G_3'(s(z0), z1) -> c37(F_2'(z1), G_3'(z0, z1)) F_4'(z0) -> c38(G_4'(z0, z0)) G_4'(s(z0), z1) -> c39(F_3'(z1), G_4'(z0, z1)) F_5'(z0) -> c40(G_5'(z0, z0)) G_5'(s(z0), z1) -> c41(F_4'(z1), G_5'(z0, z1)) F_6'(z0) -> c42(G_6'(z0, z0)) G_6'(s(z0), z1) -> c43(F_5'(z1), G_6'(z0, z1)) F_7'(z0) -> c44(G_7'(z0, z0)) G_7'(s(z0), z1) -> c45(F_6'(z1), G_7'(z0, z1)) F_8'(z0) -> c46(G_8'(z0, z0)) G_8'(s(z0), z1) -> c47(F_7'(z1), G_8'(z0, z1)) F_9'(z0) -> c48(G_9'(z0, z0)) G_9'(s(z0), z1) -> c49(F_8'(z1), G_9'(z0, z1)) G_10'(s(z0), z1) -> c51(F_9'(z1), G_10'(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) G_1'(s(z0), z1) -> c33(G_1'(z0, z1)) S tuples: F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) K tuples:none Defined Rule Symbols: F_0_1, F_1_1, G_1_2, F_2_1, G_2_2, F_3_1, G_3_2, F_4_1, G_4_2, F_5_1, G_5_2, F_6_1, G_6_2, F_7_1, G_7_2, F_8_1, G_8_2, F_9_1, G_9_2, F_10_1, G_10_2, f_0_1, f_1_1, g_1_2, f_2_1, g_2_2, f_3_1, g_3_2, f_4_1, g_4_2, f_5_1, g_5_2, f_6_1, g_6_2, f_7_1, g_7_2, f_8_1, g_8_2, f_9_1, g_9_2, f_10_1, g_10_2 Defined Pair Symbols: F_1'_1, F_2'_1, G_2'_2, F_3'_1, G_3'_2, F_4'_1, G_4'_2, F_5'_1, G_5'_2, F_6'_1, G_6'_2, F_7'_1, G_7'_2, F_8'_1, G_8'_2, F_9'_1, G_9'_2, G_10'_2, F_1''_1, G_1''_2, F_2''_1, G_2''_2, F_3''_1, G_3''_2, F_4''_1, G_4''_2, F_5''_1, G_5''_2, F_6''_1, G_6''_2, F_7''_1, G_7''_2, F_8''_1, G_8''_2, F_9''_1, G_9''_2, G_10''_2, G_1'_2 Compound Symbols: c32_1, c34_1, c35_2, c36_1, c37_2, c38_1, c39_2, c40_1, c41_2, c42_1, c43_2, c44_1, c45_2, c46_1, c47_2, c48_1, c49_2, c51_2, c53_1, c55_1, c56_1, c57_1, c58_1, c59_1, c60_1, c61_1, c62_1, c63_1, c64_1, c65_1, c66_1, c67_1, c68_1, c69_1, c70_1, c71_1, c72_1, c73_1, c74_1, c75_1, c76_1, c77_1, c78_1, c79_1, c81_1, c82_1, c33_1 ---------------------------------------- (9) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: f_0(z0) -> a f_1(z0) -> g_1(z0, z0) g_1(s(z0), z1) -> b(f_0(z1), g_1(z0, z1)) f_2(z0) -> g_2(z0, z0) g_2(s(z0), z1) -> b(f_1(z1), g_2(z0, z1)) f_3(z0) -> g_3(z0, z0) g_3(s(z0), z1) -> b(f_2(z1), g_3(z0, z1)) f_4(z0) -> g_4(z0, z0) g_4(s(z0), z1) -> b(f_3(z1), g_4(z0, z1)) f_5(z0) -> g_5(z0, z0) g_5(s(z0), z1) -> b(f_4(z1), g_5(z0, z1)) f_6(z0) -> g_6(z0, z0) g_6(s(z0), z1) -> b(f_5(z1), g_6(z0, z1)) f_7(z0) -> g_7(z0, z0) g_7(s(z0), z1) -> b(f_6(z1), g_7(z0, z1)) f_8(z0) -> g_8(z0, z0) g_8(s(z0), z1) -> b(f_7(z1), g_8(z0, z1)) f_9(z0) -> g_9(z0, z0) g_9(s(z0), z1) -> b(f_8(z1), g_9(z0, z1)) f_10(z0) -> g_10(z0, z0) g_10(s(z0), z1) -> b(f_9(z1), g_10(z0, z1)) F_0(z0) -> c F_1(z0) -> c1(G_1(z0, z0)) G_1(s(z0), z1) -> c2(F_0(z1)) G_1(s(z0), z1) -> c3(G_1(z0, z1)) F_2(z0) -> c4(G_2(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_3(z0) -> c7(G_3(z0, z0)) G_3(s(z0), z1) -> c8(F_2(z1)) G_3(s(z0), z1) -> c9(G_3(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) F_5(z0) -> c13(G_5(z0, z0)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) F_10(z0) -> c28(G_10(z0, z0)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(z0, z1)) ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: F_1'(z0) -> c32(G_1'(z0, z0)) F_2'(z0) -> c34(G_2'(z0, z0)) G_2'(s(z0), z1) -> c35(F_1'(z1), G_2'(z0, z1)) F_3'(z0) -> c36(G_3'(z0, z0)) G_3'(s(z0), z1) -> c37(F_2'(z1), G_3'(z0, z1)) F_4'(z0) -> c38(G_4'(z0, z0)) G_4'(s(z0), z1) -> c39(F_3'(z1), G_4'(z0, z1)) F_5'(z0) -> c40(G_5'(z0, z0)) G_5'(s(z0), z1) -> c41(F_4'(z1), G_5'(z0, z1)) F_6'(z0) -> c42(G_6'(z0, z0)) G_6'(s(z0), z1) -> c43(F_5'(z1), G_6'(z0, z1)) F_7'(z0) -> c44(G_7'(z0, z0)) G_7'(s(z0), z1) -> c45(F_6'(z1), G_7'(z0, z1)) F_8'(z0) -> c46(G_8'(z0, z0)) G_8'(s(z0), z1) -> c47(F_7'(z1), G_8'(z0, z1)) F_9'(z0) -> c48(G_9'(z0, z0)) G_9'(s(z0), z1) -> c49(F_8'(z1), G_9'(z0, z1)) G_10'(s(z0), z1) -> c51(F_9'(z1), G_10'(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) G_1'(s(z0), z1) -> c33(G_1'(z0, z1)) S tuples: F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) K tuples:none Defined Rule Symbols:none Defined Pair Symbols: F_1'_1, F_2'_1, G_2'_2, F_3'_1, G_3'_2, F_4'_1, G_4'_2, F_5'_1, G_5'_2, F_6'_1, G_6'_2, F_7'_1, G_7'_2, F_8'_1, G_8'_2, F_9'_1, G_9'_2, G_10'_2, F_1''_1, G_1''_2, F_2''_1, G_2''_2, F_3''_1, G_3''_2, F_4''_1, G_4''_2, F_5''_1, G_5''_2, F_6''_1, G_6''_2, F_7''_1, G_7''_2, F_8''_1, G_8''_2, F_9''_1, G_9''_2, G_10''_2, G_1'_2 Compound Symbols: c32_1, c34_1, c35_2, c36_1, c37_2, c38_1, c39_2, c40_1, c41_2, c42_1, c43_2, c44_1, c45_2, c46_1, c47_2, c48_1, c49_2, c51_2, c53_1, c55_1, c56_1, c57_1, c58_1, c59_1, c60_1, c61_1, c62_1, c63_1, c64_1, c65_1, c66_1, c67_1, c68_1, c69_1, c70_1, c71_1, c72_1, c73_1, c74_1, c75_1, c76_1, c77_1, c78_1, c79_1, c81_1, c82_1, c33_1 ---------------------------------------- (11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. G_9''(s(z0), z1) -> c78(F_8''(z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) We considered the (Usable) Rules:none And the Tuples: F_1'(z0) -> c32(G_1'(z0, z0)) F_2'(z0) -> c34(G_2'(z0, z0)) G_2'(s(z0), z1) -> c35(F_1'(z1), G_2'(z0, z1)) F_3'(z0) -> c36(G_3'(z0, z0)) G_3'(s(z0), z1) -> c37(F_2'(z1), G_3'(z0, z1)) F_4'(z0) -> c38(G_4'(z0, z0)) G_4'(s(z0), z1) -> c39(F_3'(z1), G_4'(z0, z1)) F_5'(z0) -> c40(G_5'(z0, z0)) G_5'(s(z0), z1) -> c41(F_4'(z1), G_5'(z0, z1)) F_6'(z0) -> c42(G_6'(z0, z0)) G_6'(s(z0), z1) -> c43(F_5'(z1), G_6'(z0, z1)) F_7'(z0) -> c44(G_7'(z0, z0)) G_7'(s(z0), z1) -> c45(F_6'(z1), G_7'(z0, z1)) F_8'(z0) -> c46(G_8'(z0, z0)) G_8'(s(z0), z1) -> c47(F_7'(z1), G_8'(z0, z1)) F_9'(z0) -> c48(G_9'(z0, z0)) G_9'(s(z0), z1) -> c49(F_8'(z1), G_9'(z0, z1)) G_10'(s(z0), z1) -> c51(F_9'(z1), G_10'(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) G_1'(s(z0), z1) -> c33(G_1'(z0, z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(F_1'(x_1)) = 0 POL(F_1''(x_1)) = 0 POL(F_2'(x_1)) = 0 POL(F_2''(x_1)) = 0 POL(F_3'(x_1)) = 0 POL(F_3''(x_1)) = 0 POL(F_4'(x_1)) = 0 POL(F_4''(x_1)) = 0 POL(F_5'(x_1)) = 0 POL(F_5''(x_1)) = 0 POL(F_6'(x_1)) = 0 POL(F_6''(x_1)) = 0 POL(F_7'(x_1)) = 0 POL(F_7''(x_1)) = x_1 POL(F_8'(x_1)) = 0 POL(F_8''(x_1)) = x_1 POL(F_9'(x_1)) = [1] POL(F_9''(x_1)) = [1] + x_1 POL(G_1'(x_1, x_2)) = 0 POL(G_1''(x_1, x_2)) = 0 POL(G_10'(x_1, x_2)) = x_1 POL(G_10''(x_1, x_2)) = [1] + x_1 + x_2 POL(G_2'(x_1, x_2)) = 0 POL(G_2''(x_1, x_2)) = 0 POL(G_3'(x_1, x_2)) = 0 POL(G_3''(x_1, x_2)) = 0 POL(G_4'(x_1, x_2)) = 0 POL(G_4''(x_1, x_2)) = 0 POL(G_5'(x_1, x_2)) = 0 POL(G_5''(x_1, x_2)) = 0 POL(G_6'(x_1, x_2)) = 0 POL(G_6''(x_1, x_2)) = 0 POL(G_7'(x_1, x_2)) = 0 POL(G_7''(x_1, x_2)) = 0 POL(G_8'(x_1, x_2)) = 0 POL(G_8''(x_1, x_2)) = x_2 POL(G_9'(x_1, x_2)) = [1] POL(G_9''(x_1, x_2)) = [1] + x_2 POL(c32(x_1)) = x_1 POL(c33(x_1)) = x_1 POL(c34(x_1)) = x_1 POL(c35(x_1, x_2)) = x_1 + x_2 POL(c36(x_1)) = x_1 POL(c37(x_1, x_2)) = x_1 + x_2 POL(c38(x_1)) = x_1 POL(c39(x_1, x_2)) = x_1 + x_2 POL(c40(x_1)) = x_1 POL(c41(x_1, x_2)) = x_1 + x_2 POL(c42(x_1)) = x_1 POL(c43(x_1, x_2)) = x_1 + x_2 POL(c44(x_1)) = x_1 POL(c45(x_1, x_2)) = x_1 + x_2 POL(c46(x_1)) = x_1 POL(c47(x_1, x_2)) = x_1 + x_2 POL(c48(x_1)) = x_1 POL(c49(x_1, x_2)) = x_1 + x_2 POL(c51(x_1, x_2)) = x_1 + x_2 POL(c53(x_1)) = x_1 POL(c55(x_1)) = x_1 POL(c56(x_1)) = x_1 POL(c57(x_1)) = x_1 POL(c58(x_1)) = x_1 POL(c59(x_1)) = x_1 POL(c60(x_1)) = x_1 POL(c61(x_1)) = x_1 POL(c62(x_1)) = x_1 POL(c63(x_1)) = x_1 POL(c64(x_1)) = x_1 POL(c65(x_1)) = x_1 POL(c66(x_1)) = x_1 POL(c67(x_1)) = x_1 POL(c68(x_1)) = x_1 POL(c69(x_1)) = x_1 POL(c70(x_1)) = x_1 POL(c71(x_1)) = x_1 POL(c72(x_1)) = x_1 POL(c73(x_1)) = x_1 POL(c74(x_1)) = x_1 POL(c75(x_1)) = x_1 POL(c76(x_1)) = x_1 POL(c77(x_1)) = x_1 POL(c78(x_1)) = x_1 POL(c79(x_1)) = x_1 POL(c81(x_1)) = x_1 POL(c82(x_1)) = x_1 POL(s(x_1)) = [1] + x_1 ---------------------------------------- (12) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: F_1'(z0) -> c32(G_1'(z0, z0)) F_2'(z0) -> c34(G_2'(z0, z0)) G_2'(s(z0), z1) -> c35(F_1'(z1), G_2'(z0, z1)) F_3'(z0) -> c36(G_3'(z0, z0)) G_3'(s(z0), z1) -> c37(F_2'(z1), G_3'(z0, z1)) F_4'(z0) -> c38(G_4'(z0, z0)) G_4'(s(z0), z1) -> c39(F_3'(z1), G_4'(z0, z1)) F_5'(z0) -> c40(G_5'(z0, z0)) G_5'(s(z0), z1) -> c41(F_4'(z1), G_5'(z0, z1)) F_6'(z0) -> c42(G_6'(z0, z0)) G_6'(s(z0), z1) -> c43(F_5'(z1), G_6'(z0, z1)) F_7'(z0) -> c44(G_7'(z0, z0)) G_7'(s(z0), z1) -> c45(F_6'(z1), G_7'(z0, z1)) F_8'(z0) -> c46(G_8'(z0, z0)) G_8'(s(z0), z1) -> c47(F_7'(z1), G_8'(z0, z1)) F_9'(z0) -> c48(G_9'(z0, z0)) G_9'(s(z0), z1) -> c49(F_8'(z1), G_9'(z0, z1)) G_10'(s(z0), z1) -> c51(F_9'(z1), G_10'(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) G_1'(s(z0), z1) -> c33(G_1'(z0, z1)) S tuples: F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) K tuples: G_9''(s(z0), z1) -> c78(F_8''(z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) Defined Rule Symbols:none Defined Pair Symbols: F_1'_1, F_2'_1, G_2'_2, F_3'_1, G_3'_2, F_4'_1, G_4'_2, F_5'_1, G_5'_2, F_6'_1, G_6'_2, F_7'_1, G_7'_2, F_8'_1, G_8'_2, F_9'_1, G_9'_2, G_10'_2, F_1''_1, G_1''_2, F_2''_1, G_2''_2, F_3''_1, G_3''_2, F_4''_1, G_4''_2, F_5''_1, G_5''_2, F_6''_1, G_6''_2, F_7''_1, G_7''_2, F_8''_1, G_8''_2, F_9''_1, G_9''_2, G_10''_2, G_1'_2 Compound Symbols: c32_1, c34_1, c35_2, c36_1, c37_2, c38_1, c39_2, c40_1, c41_2, c42_1, c43_2, c44_1, c45_2, c46_1, c47_2, c48_1, c49_2, c51_2, c53_1, c55_1, c56_1, c57_1, c58_1, c59_1, c60_1, c61_1, c62_1, c63_1, c64_1, c65_1, c66_1, c67_1, c68_1, c69_1, c70_1, c71_1, c72_1, c73_1, c74_1, c75_1, c76_1, c77_1, c78_1, c79_1, c81_1, c82_1, c33_1 ---------------------------------------- (13) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: F_8''(z0) -> c74(G_8''(z0, z0)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) ---------------------------------------- (14) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: F_1'(z0) -> c32(G_1'(z0, z0)) F_2'(z0) -> c34(G_2'(z0, z0)) G_2'(s(z0), z1) -> c35(F_1'(z1), G_2'(z0, z1)) F_3'(z0) -> c36(G_3'(z0, z0)) G_3'(s(z0), z1) -> c37(F_2'(z1), G_3'(z0, z1)) F_4'(z0) -> c38(G_4'(z0, z0)) G_4'(s(z0), z1) -> c39(F_3'(z1), G_4'(z0, z1)) F_5'(z0) -> c40(G_5'(z0, z0)) G_5'(s(z0), z1) -> c41(F_4'(z1), G_5'(z0, z1)) F_6'(z0) -> c42(G_6'(z0, z0)) G_6'(s(z0), z1) -> c43(F_5'(z1), G_6'(z0, z1)) F_7'(z0) -> c44(G_7'(z0, z0)) G_7'(s(z0), z1) -> c45(F_6'(z1), G_7'(z0, z1)) F_8'(z0) -> c46(G_8'(z0, z0)) G_8'(s(z0), z1) -> c47(F_7'(z1), G_8'(z0, z1)) F_9'(z0) -> c48(G_9'(z0, z0)) G_9'(s(z0), z1) -> c49(F_8'(z1), G_9'(z0, z1)) G_10'(s(z0), z1) -> c51(F_9'(z1), G_10'(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) G_1'(s(z0), z1) -> c33(G_1'(z0, z1)) S tuples: F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) K tuples: G_9''(s(z0), z1) -> c78(F_8''(z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) F_9''(z0) -> c77(G_9''(z0, z0)) Defined Rule Symbols:none Defined Pair Symbols: F_1'_1, F_2'_1, G_2'_2, F_3'_1, G_3'_2, F_4'_1, G_4'_2, F_5'_1, G_5'_2, F_6'_1, G_6'_2, F_7'_1, G_7'_2, F_8'_1, G_8'_2, F_9'_1, G_9'_2, G_10'_2, F_1''_1, G_1''_2, F_2''_1, G_2''_2, F_3''_1, G_3''_2, F_4''_1, G_4''_2, F_5''_1, G_5''_2, F_6''_1, G_6''_2, F_7''_1, G_7''_2, F_8''_1, G_8''_2, F_9''_1, G_9''_2, G_10''_2, G_1'_2 Compound Symbols: c32_1, c34_1, c35_2, c36_1, c37_2, c38_1, c39_2, c40_1, c41_2, c42_1, c43_2, c44_1, c45_2, c46_1, c47_2, c48_1, c49_2, c51_2, c53_1, c55_1, c56_1, c57_1, c58_1, c59_1, c60_1, c61_1, c62_1, c63_1, c64_1, c65_1, c66_1, c67_1, c68_1, c69_1, c70_1, c71_1, c72_1, c73_1, c74_1, c75_1, c76_1, c77_1, c78_1, c79_1, c81_1, c82_1, c33_1 ---------------------------------------- (15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) We considered the (Usable) Rules:none And the Tuples: F_1'(z0) -> c32(G_1'(z0, z0)) F_2'(z0) -> c34(G_2'(z0, z0)) G_2'(s(z0), z1) -> c35(F_1'(z1), G_2'(z0, z1)) F_3'(z0) -> c36(G_3'(z0, z0)) G_3'(s(z0), z1) -> c37(F_2'(z1), G_3'(z0, z1)) F_4'(z0) -> c38(G_4'(z0, z0)) G_4'(s(z0), z1) -> c39(F_3'(z1), G_4'(z0, z1)) F_5'(z0) -> c40(G_5'(z0, z0)) G_5'(s(z0), z1) -> c41(F_4'(z1), G_5'(z0, z1)) F_6'(z0) -> c42(G_6'(z0, z0)) G_6'(s(z0), z1) -> c43(F_5'(z1), G_6'(z0, z1)) F_7'(z0) -> c44(G_7'(z0, z0)) G_7'(s(z0), z1) -> c45(F_6'(z1), G_7'(z0, z1)) F_8'(z0) -> c46(G_8'(z0, z0)) G_8'(s(z0), z1) -> c47(F_7'(z1), G_8'(z0, z1)) F_9'(z0) -> c48(G_9'(z0, z0)) G_9'(s(z0), z1) -> c49(F_8'(z1), G_9'(z0, z1)) G_10'(s(z0), z1) -> c51(F_9'(z1), G_10'(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) G_1'(s(z0), z1) -> c33(G_1'(z0, z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(F_1'(x_1)) = 0 POL(F_1''(x_1)) = 0 POL(F_2'(x_1)) = 0 POL(F_2''(x_1)) = 0 POL(F_3'(x_1)) = 0 POL(F_3''(x_1)) = 0 POL(F_4'(x_1)) = 0 POL(F_4''(x_1)) = 0 POL(F_5'(x_1)) = 0 POL(F_5''(x_1)) = x_1 POL(F_6'(x_1)) = 0 POL(F_6''(x_1)) = x_1 POL(F_7'(x_1)) = 0 POL(F_7''(x_1)) = [1] + x_1 POL(F_8'(x_1)) = 0 POL(F_8''(x_1)) = [1] + x_1 POL(F_9'(x_1)) = [1] POL(F_9''(x_1)) = [1] + x_1 POL(G_1'(x_1, x_2)) = 0 POL(G_1''(x_1, x_2)) = 0 POL(G_10'(x_1, x_2)) = x_1 POL(G_10''(x_1, x_2)) = [1] + x_2 POL(G_2'(x_1, x_2)) = 0 POL(G_2''(x_1, x_2)) = 0 POL(G_3'(x_1, x_2)) = 0 POL(G_3''(x_1, x_2)) = 0 POL(G_4'(x_1, x_2)) = 0 POL(G_4''(x_1, x_2)) = 0 POL(G_5'(x_1, x_2)) = 0 POL(G_5''(x_1, x_2)) = x_1 POL(G_6'(x_1, x_2)) = 0 POL(G_6''(x_1, x_2)) = x_2 POL(G_7'(x_1, x_2)) = 0 POL(G_7''(x_1, x_2)) = x_2 POL(G_8'(x_1, x_2)) = 0 POL(G_8''(x_1, x_2)) = [1] + x_2 POL(G_9'(x_1, x_2)) = [1] POL(G_9''(x_1, x_2)) = [1] + x_2 POL(c32(x_1)) = x_1 POL(c33(x_1)) = x_1 POL(c34(x_1)) = x_1 POL(c35(x_1, x_2)) = x_1 + x_2 POL(c36(x_1)) = x_1 POL(c37(x_1, x_2)) = x_1 + x_2 POL(c38(x_1)) = x_1 POL(c39(x_1, x_2)) = x_1 + x_2 POL(c40(x_1)) = x_1 POL(c41(x_1, x_2)) = x_1 + x_2 POL(c42(x_1)) = x_1 POL(c43(x_1, x_2)) = x_1 + x_2 POL(c44(x_1)) = x_1 POL(c45(x_1, x_2)) = x_1 + x_2 POL(c46(x_1)) = x_1 POL(c47(x_1, x_2)) = x_1 + x_2 POL(c48(x_1)) = x_1 POL(c49(x_1, x_2)) = x_1 + x_2 POL(c51(x_1, x_2)) = x_1 + x_2 POL(c53(x_1)) = x_1 POL(c55(x_1)) = x_1 POL(c56(x_1)) = x_1 POL(c57(x_1)) = x_1 POL(c58(x_1)) = x_1 POL(c59(x_1)) = x_1 POL(c60(x_1)) = x_1 POL(c61(x_1)) = x_1 POL(c62(x_1)) = x_1 POL(c63(x_1)) = x_1 POL(c64(x_1)) = x_1 POL(c65(x_1)) = x_1 POL(c66(x_1)) = x_1 POL(c67(x_1)) = x_1 POL(c68(x_1)) = x_1 POL(c69(x_1)) = x_1 POL(c70(x_1)) = x_1 POL(c71(x_1)) = x_1 POL(c72(x_1)) = x_1 POL(c73(x_1)) = x_1 POL(c74(x_1)) = x_1 POL(c75(x_1)) = x_1 POL(c76(x_1)) = x_1 POL(c77(x_1)) = x_1 POL(c78(x_1)) = x_1 POL(c79(x_1)) = x_1 POL(c81(x_1)) = x_1 POL(c82(x_1)) = x_1 POL(s(x_1)) = [1] + x_1 ---------------------------------------- (16) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: F_1'(z0) -> c32(G_1'(z0, z0)) F_2'(z0) -> c34(G_2'(z0, z0)) G_2'(s(z0), z1) -> c35(F_1'(z1), G_2'(z0, z1)) F_3'(z0) -> c36(G_3'(z0, z0)) G_3'(s(z0), z1) -> c37(F_2'(z1), G_3'(z0, z1)) F_4'(z0) -> c38(G_4'(z0, z0)) G_4'(s(z0), z1) -> c39(F_3'(z1), G_4'(z0, z1)) F_5'(z0) -> c40(G_5'(z0, z0)) G_5'(s(z0), z1) -> c41(F_4'(z1), G_5'(z0, z1)) F_6'(z0) -> c42(G_6'(z0, z0)) G_6'(s(z0), z1) -> c43(F_5'(z1), G_6'(z0, z1)) F_7'(z0) -> c44(G_7'(z0, z0)) G_7'(s(z0), z1) -> c45(F_6'(z1), G_7'(z0, z1)) F_8'(z0) -> c46(G_8'(z0, z0)) G_8'(s(z0), z1) -> c47(F_7'(z1), G_8'(z0, z1)) F_9'(z0) -> c48(G_9'(z0, z0)) G_9'(s(z0), z1) -> c49(F_8'(z1), G_9'(z0, z1)) G_10'(s(z0), z1) -> c51(F_9'(z1), G_10'(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) G_1'(s(z0), z1) -> c33(G_1'(z0, z1)) S tuples: F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) K tuples: G_9''(s(z0), z1) -> c78(F_8''(z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) F_9''(z0) -> c77(G_9''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) Defined Rule Symbols:none Defined Pair Symbols: F_1'_1, F_2'_1, G_2'_2, F_3'_1, G_3'_2, F_4'_1, G_4'_2, F_5'_1, G_5'_2, F_6'_1, G_6'_2, F_7'_1, G_7'_2, F_8'_1, G_8'_2, F_9'_1, G_9'_2, G_10'_2, F_1''_1, G_1''_2, F_2''_1, G_2''_2, F_3''_1, G_3''_2, F_4''_1, G_4''_2, F_5''_1, G_5''_2, F_6''_1, G_6''_2, F_7''_1, G_7''_2, F_8''_1, G_8''_2, F_9''_1, G_9''_2, G_10''_2, G_1'_2 Compound Symbols: c32_1, c34_1, c35_2, c36_1, c37_2, c38_1, c39_2, c40_1, c41_2, c42_1, c43_2, c44_1, c45_2, c46_1, c47_2, c48_1, c49_2, c51_2, c53_1, c55_1, c56_1, c57_1, c58_1, c59_1, c60_1, c61_1, c62_1, c63_1, c64_1, c65_1, c66_1, c67_1, c68_1, c69_1, c70_1, c71_1, c72_1, c73_1, c74_1, c75_1, c76_1, c77_1, c78_1, c79_1, c81_1, c82_1, c33_1 ---------------------------------------- (17) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: F_4''(z0) -> c62(G_4''(z0, z0)) ---------------------------------------- (18) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: F_1'(z0) -> c32(G_1'(z0, z0)) F_2'(z0) -> c34(G_2'(z0, z0)) G_2'(s(z0), z1) -> c35(F_1'(z1), G_2'(z0, z1)) F_3'(z0) -> c36(G_3'(z0, z0)) G_3'(s(z0), z1) -> c37(F_2'(z1), G_3'(z0, z1)) F_4'(z0) -> c38(G_4'(z0, z0)) G_4'(s(z0), z1) -> c39(F_3'(z1), G_4'(z0, z1)) F_5'(z0) -> c40(G_5'(z0, z0)) G_5'(s(z0), z1) -> c41(F_4'(z1), G_5'(z0, z1)) F_6'(z0) -> c42(G_6'(z0, z0)) G_6'(s(z0), z1) -> c43(F_5'(z1), G_6'(z0, z1)) F_7'(z0) -> c44(G_7'(z0, z0)) G_7'(s(z0), z1) -> c45(F_6'(z1), G_7'(z0, z1)) F_8'(z0) -> c46(G_8'(z0, z0)) G_8'(s(z0), z1) -> c47(F_7'(z1), G_8'(z0, z1)) F_9'(z0) -> c48(G_9'(z0, z0)) G_9'(s(z0), z1) -> c49(F_8'(z1), G_9'(z0, z1)) G_10'(s(z0), z1) -> c51(F_9'(z1), G_10'(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) G_1'(s(z0), z1) -> c33(G_1'(z0, z1)) S tuples: F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) K tuples: G_9''(s(z0), z1) -> c78(F_8''(z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) F_9''(z0) -> c77(G_9''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) F_4''(z0) -> c62(G_4''(z0, z0)) Defined Rule Symbols:none Defined Pair Symbols: F_1'_1, F_2'_1, G_2'_2, F_3'_1, G_3'_2, F_4'_1, G_4'_2, F_5'_1, G_5'_2, F_6'_1, G_6'_2, F_7'_1, G_7'_2, F_8'_1, G_8'_2, F_9'_1, G_9'_2, G_10'_2, F_1''_1, G_1''_2, F_2''_1, G_2''_2, F_3''_1, G_3''_2, F_4''_1, G_4''_2, F_5''_1, G_5''_2, F_6''_1, G_6''_2, F_7''_1, G_7''_2, F_8''_1, G_8''_2, F_9''_1, G_9''_2, G_10''_2, G_1'_2 Compound Symbols: c32_1, c34_1, c35_2, c36_1, c37_2, c38_1, c39_2, c40_1, c41_2, c42_1, c43_2, c44_1, c45_2, c46_1, c47_2, c48_1, c49_2, c51_2, c53_1, c55_1, c56_1, c57_1, c58_1, c59_1, c60_1, c61_1, c62_1, c63_1, c64_1, c65_1, c66_1, c67_1, c68_1, c69_1, c70_1, c71_1, c72_1, c73_1, c74_1, c75_1, c76_1, c77_1, c78_1, c79_1, c81_1, c82_1, c33_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. G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) We considered the (Usable) Rules:none And the Tuples: F_1'(z0) -> c32(G_1'(z0, z0)) F_2'(z0) -> c34(G_2'(z0, z0)) G_2'(s(z0), z1) -> c35(F_1'(z1), G_2'(z0, z1)) F_3'(z0) -> c36(G_3'(z0, z0)) G_3'(s(z0), z1) -> c37(F_2'(z1), G_3'(z0, z1)) F_4'(z0) -> c38(G_4'(z0, z0)) G_4'(s(z0), z1) -> c39(F_3'(z1), G_4'(z0, z1)) F_5'(z0) -> c40(G_5'(z0, z0)) G_5'(s(z0), z1) -> c41(F_4'(z1), G_5'(z0, z1)) F_6'(z0) -> c42(G_6'(z0, z0)) G_6'(s(z0), z1) -> c43(F_5'(z1), G_6'(z0, z1)) F_7'(z0) -> c44(G_7'(z0, z0)) G_7'(s(z0), z1) -> c45(F_6'(z1), G_7'(z0, z1)) F_8'(z0) -> c46(G_8'(z0, z0)) G_8'(s(z0), z1) -> c47(F_7'(z1), G_8'(z0, z1)) F_9'(z0) -> c48(G_9'(z0, z0)) G_9'(s(z0), z1) -> c49(F_8'(z1), G_9'(z0, z1)) G_10'(s(z0), z1) -> c51(F_9'(z1), G_10'(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) G_1'(s(z0), z1) -> c33(G_1'(z0, z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(F_1'(x_1)) = 0 POL(F_1''(x_1)) = 0 POL(F_2'(x_1)) = 0 POL(F_2''(x_1)) = x_1 POL(F_3'(x_1)) = 0 POL(F_3''(x_1)) = x_1 POL(F_4'(x_1)) = 0 POL(F_4''(x_1)) = x_1 POL(F_5'(x_1)) = 0 POL(F_5''(x_1)) = x_1 POL(F_6'(x_1)) = 0 POL(F_6''(x_1)) = x_1 POL(F_7'(x_1)) = 0 POL(F_7''(x_1)) = x_1 POL(F_8'(x_1)) = 0 POL(F_8''(x_1)) = [3] + [2]x_1 POL(F_9'(x_1)) = [3] POL(F_9''(x_1)) = [3] + [3]x_1 POL(G_1'(x_1, x_2)) = 0 POL(G_1''(x_1, x_2)) = 0 POL(G_10'(x_1, x_2)) = [3]x_1 POL(G_10''(x_1, x_2)) = [3] + [3]x_1 + [3]x_2 POL(G_2'(x_1, x_2)) = 0 POL(G_2''(x_1, x_2)) = x_1 POL(G_3'(x_1, x_2)) = 0 POL(G_3''(x_1, x_2)) = x_2 POL(G_4'(x_1, x_2)) = 0 POL(G_4''(x_1, x_2)) = x_2 POL(G_5'(x_1, x_2)) = 0 POL(G_5''(x_1, x_2)) = x_2 POL(G_6'(x_1, x_2)) = 0 POL(G_6''(x_1, x_2)) = x_2 POL(G_7'(x_1, x_2)) = 0 POL(G_7''(x_1, x_2)) = x_2 POL(G_8'(x_1, x_2)) = 0 POL(G_8''(x_1, x_2)) = x_2 POL(G_9'(x_1, x_2)) = [3] POL(G_9''(x_1, x_2)) = [3] + [3]x_2 POL(c32(x_1)) = x_1 POL(c33(x_1)) = x_1 POL(c34(x_1)) = x_1 POL(c35(x_1, x_2)) = x_1 + x_2 POL(c36(x_1)) = x_1 POL(c37(x_1, x_2)) = x_1 + x_2 POL(c38(x_1)) = x_1 POL(c39(x_1, x_2)) = x_1 + x_2 POL(c40(x_1)) = x_1 POL(c41(x_1, x_2)) = x_1 + x_2 POL(c42(x_1)) = x_1 POL(c43(x_1, x_2)) = x_1 + x_2 POL(c44(x_1)) = x_1 POL(c45(x_1, x_2)) = x_1 + x_2 POL(c46(x_1)) = x_1 POL(c47(x_1, x_2)) = x_1 + x_2 POL(c48(x_1)) = x_1 POL(c49(x_1, x_2)) = x_1 + x_2 POL(c51(x_1, x_2)) = x_1 + x_2 POL(c53(x_1)) = x_1 POL(c55(x_1)) = x_1 POL(c56(x_1)) = x_1 POL(c57(x_1)) = x_1 POL(c58(x_1)) = x_1 POL(c59(x_1)) = x_1 POL(c60(x_1)) = x_1 POL(c61(x_1)) = x_1 POL(c62(x_1)) = x_1 POL(c63(x_1)) = x_1 POL(c64(x_1)) = x_1 POL(c65(x_1)) = x_1 POL(c66(x_1)) = x_1 POL(c67(x_1)) = x_1 POL(c68(x_1)) = x_1 POL(c69(x_1)) = x_1 POL(c70(x_1)) = x_1 POL(c71(x_1)) = x_1 POL(c72(x_1)) = x_1 POL(c73(x_1)) = x_1 POL(c74(x_1)) = x_1 POL(c75(x_1)) = x_1 POL(c76(x_1)) = x_1 POL(c77(x_1)) = x_1 POL(c78(x_1)) = x_1 POL(c79(x_1)) = x_1 POL(c81(x_1)) = x_1 POL(c82(x_1)) = x_1 POL(s(x_1)) = [1] + x_1 ---------------------------------------- (20) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: F_1'(z0) -> c32(G_1'(z0, z0)) F_2'(z0) -> c34(G_2'(z0, z0)) G_2'(s(z0), z1) -> c35(F_1'(z1), G_2'(z0, z1)) F_3'(z0) -> c36(G_3'(z0, z0)) G_3'(s(z0), z1) -> c37(F_2'(z1), G_3'(z0, z1)) F_4'(z0) -> c38(G_4'(z0, z0)) G_4'(s(z0), z1) -> c39(F_3'(z1), G_4'(z0, z1)) F_5'(z0) -> c40(G_5'(z0, z0)) G_5'(s(z0), z1) -> c41(F_4'(z1), G_5'(z0, z1)) F_6'(z0) -> c42(G_6'(z0, z0)) G_6'(s(z0), z1) -> c43(F_5'(z1), G_6'(z0, z1)) F_7'(z0) -> c44(G_7'(z0, z0)) G_7'(s(z0), z1) -> c45(F_6'(z1), G_7'(z0, z1)) F_8'(z0) -> c46(G_8'(z0, z0)) G_8'(s(z0), z1) -> c47(F_7'(z1), G_8'(z0, z1)) F_9'(z0) -> c48(G_9'(z0, z0)) G_9'(s(z0), z1) -> c49(F_8'(z1), G_9'(z0, z1)) G_10'(s(z0), z1) -> c51(F_9'(z1), G_10'(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) G_1'(s(z0), z1) -> c33(G_1'(z0, z1)) S tuples: F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) K tuples: G_9''(s(z0), z1) -> c78(F_8''(z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) F_9''(z0) -> c77(G_9''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) F_4''(z0) -> c62(G_4''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) Defined Rule Symbols:none Defined Pair Symbols: F_1'_1, F_2'_1, G_2'_2, F_3'_1, G_3'_2, F_4'_1, G_4'_2, F_5'_1, G_5'_2, F_6'_1, G_6'_2, F_7'_1, G_7'_2, F_8'_1, G_8'_2, F_9'_1, G_9'_2, G_10'_2, F_1''_1, G_1''_2, F_2''_1, G_2''_2, F_3''_1, G_3''_2, F_4''_1, G_4''_2, F_5''_1, G_5''_2, F_6''_1, G_6''_2, F_7''_1, G_7''_2, F_8''_1, G_8''_2, F_9''_1, G_9''_2, G_10''_2, G_1'_2 Compound Symbols: c32_1, c34_1, c35_2, c36_1, c37_2, c38_1, c39_2, c40_1, c41_2, c42_1, c43_2, c44_1, c45_2, c46_1, c47_2, c48_1, c49_2, c51_2, c53_1, c55_1, c56_1, c57_1, c58_1, c59_1, c60_1, c61_1, c62_1, c63_1, c64_1, c65_1, c66_1, c67_1, c68_1, c69_1, c70_1, c71_1, c72_1, c73_1, c74_1, c75_1, c76_1, c77_1, c78_1, c79_1, c81_1, c82_1, c33_1 ---------------------------------------- (21) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: F_1''(z0) -> c53(G_1''(z0, z0)) ---------------------------------------- (22) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: F_1'(z0) -> c32(G_1'(z0, z0)) F_2'(z0) -> c34(G_2'(z0, z0)) G_2'(s(z0), z1) -> c35(F_1'(z1), G_2'(z0, z1)) F_3'(z0) -> c36(G_3'(z0, z0)) G_3'(s(z0), z1) -> c37(F_2'(z1), G_3'(z0, z1)) F_4'(z0) -> c38(G_4'(z0, z0)) G_4'(s(z0), z1) -> c39(F_3'(z1), G_4'(z0, z1)) F_5'(z0) -> c40(G_5'(z0, z0)) G_5'(s(z0), z1) -> c41(F_4'(z1), G_5'(z0, z1)) F_6'(z0) -> c42(G_6'(z0, z0)) G_6'(s(z0), z1) -> c43(F_5'(z1), G_6'(z0, z1)) F_7'(z0) -> c44(G_7'(z0, z0)) G_7'(s(z0), z1) -> c45(F_6'(z1), G_7'(z0, z1)) F_8'(z0) -> c46(G_8'(z0, z0)) G_8'(s(z0), z1) -> c47(F_7'(z1), G_8'(z0, z1)) F_9'(z0) -> c48(G_9'(z0, z0)) G_9'(s(z0), z1) -> c49(F_8'(z1), G_9'(z0, z1)) G_10'(s(z0), z1) -> c51(F_9'(z1), G_10'(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) G_1'(s(z0), z1) -> c33(G_1'(z0, z1)) S tuples: G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) K tuples: G_9''(s(z0), z1) -> c78(F_8''(z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) F_9''(z0) -> c77(G_9''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) F_4''(z0) -> c62(G_4''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) Defined Rule Symbols:none Defined Pair Symbols: F_1'_1, F_2'_1, G_2'_2, F_3'_1, G_3'_2, F_4'_1, G_4'_2, F_5'_1, G_5'_2, F_6'_1, G_6'_2, F_7'_1, G_7'_2, F_8'_1, G_8'_2, F_9'_1, G_9'_2, G_10'_2, F_1''_1, G_1''_2, F_2''_1, G_2''_2, F_3''_1, G_3''_2, F_4''_1, G_4''_2, F_5''_1, G_5''_2, F_6''_1, G_6''_2, F_7''_1, G_7''_2, F_8''_1, G_8''_2, F_9''_1, G_9''_2, G_10''_2, G_1'_2 Compound Symbols: c32_1, c34_1, c35_2, c36_1, c37_2, c38_1, c39_2, c40_1, c41_2, c42_1, c43_2, c44_1, c45_2, c46_1, c47_2, c48_1, c49_2, c51_2, c53_1, c55_1, c56_1, c57_1, c58_1, c59_1, c60_1, c61_1, c62_1, c63_1, c64_1, c65_1, c66_1, c67_1, c68_1, c69_1, c70_1, c71_1, c72_1, c73_1, c74_1, c75_1, c76_1, c77_1, c78_1, c79_1, c81_1, c82_1, c33_1 ---------------------------------------- (23) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. F_3''(z0) -> c59(G_3''(z0, z0)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) We considered the (Usable) Rules:none And the Tuples: F_1'(z0) -> c32(G_1'(z0, z0)) F_2'(z0) -> c34(G_2'(z0, z0)) G_2'(s(z0), z1) -> c35(F_1'(z1), G_2'(z0, z1)) F_3'(z0) -> c36(G_3'(z0, z0)) G_3'(s(z0), z1) -> c37(F_2'(z1), G_3'(z0, z1)) F_4'(z0) -> c38(G_4'(z0, z0)) G_4'(s(z0), z1) -> c39(F_3'(z1), G_4'(z0, z1)) F_5'(z0) -> c40(G_5'(z0, z0)) G_5'(s(z0), z1) -> c41(F_4'(z1), G_5'(z0, z1)) F_6'(z0) -> c42(G_6'(z0, z0)) G_6'(s(z0), z1) -> c43(F_5'(z1), G_6'(z0, z1)) F_7'(z0) -> c44(G_7'(z0, z0)) G_7'(s(z0), z1) -> c45(F_6'(z1), G_7'(z0, z1)) F_8'(z0) -> c46(G_8'(z0, z0)) G_8'(s(z0), z1) -> c47(F_7'(z1), G_8'(z0, z1)) F_9'(z0) -> c48(G_9'(z0, z0)) G_9'(s(z0), z1) -> c49(F_8'(z1), G_9'(z0, z1)) G_10'(s(z0), z1) -> c51(F_9'(z1), G_10'(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) G_1'(s(z0), z1) -> c33(G_1'(z0, z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(F_1'(x_1)) = 0 POL(F_1''(x_1)) = 0 POL(F_2'(x_1)) = 0 POL(F_2''(x_1)) = 0 POL(F_3'(x_1)) = 0 POL(F_3''(x_1)) = [1] POL(F_4'(x_1)) = 0 POL(F_4''(x_1)) = [1] POL(F_5'(x_1)) = 0 POL(F_5''(x_1)) = [1] POL(F_6'(x_1)) = 0 POL(F_6''(x_1)) = [1] POL(F_7'(x_1)) = 0 POL(F_7''(x_1)) = [1] POL(F_8'(x_1)) = 0 POL(F_8''(x_1)) = [1] POL(F_9'(x_1)) = [1] POL(F_9''(x_1)) = [1] + x_1 POL(G_1'(x_1, x_2)) = 0 POL(G_1''(x_1, x_2)) = 0 POL(G_10'(x_1, x_2)) = x_1 POL(G_10''(x_1, x_2)) = x_1 + x_2 POL(G_2'(x_1, x_2)) = 0 POL(G_2''(x_1, x_2)) = 0 POL(G_3'(x_1, x_2)) = 0 POL(G_3''(x_1, x_2)) = 0 POL(G_4'(x_1, x_2)) = 0 POL(G_4''(x_1, x_2)) = [1] POL(G_5'(x_1, x_2)) = 0 POL(G_5''(x_1, x_2)) = [1] POL(G_6'(x_1, x_2)) = 0 POL(G_6''(x_1, x_2)) = [1] POL(G_7'(x_1, x_2)) = 0 POL(G_7''(x_1, x_2)) = [1] POL(G_8'(x_1, x_2)) = 0 POL(G_8''(x_1, x_2)) = [1] POL(G_9'(x_1, x_2)) = [1] POL(G_9''(x_1, x_2)) = x_1 POL(c32(x_1)) = x_1 POL(c33(x_1)) = x_1 POL(c34(x_1)) = x_1 POL(c35(x_1, x_2)) = x_1 + x_2 POL(c36(x_1)) = x_1 POL(c37(x_1, x_2)) = x_1 + x_2 POL(c38(x_1)) = x_1 POL(c39(x_1, x_2)) = x_1 + x_2 POL(c40(x_1)) = x_1 POL(c41(x_1, x_2)) = x_1 + x_2 POL(c42(x_1)) = x_1 POL(c43(x_1, x_2)) = x_1 + x_2 POL(c44(x_1)) = x_1 POL(c45(x_1, x_2)) = x_1 + x_2 POL(c46(x_1)) = x_1 POL(c47(x_1, x_2)) = x_1 + x_2 POL(c48(x_1)) = x_1 POL(c49(x_1, x_2)) = x_1 + x_2 POL(c51(x_1, x_2)) = x_1 + x_2 POL(c53(x_1)) = x_1 POL(c55(x_1)) = x_1 POL(c56(x_1)) = x_1 POL(c57(x_1)) = x_1 POL(c58(x_1)) = x_1 POL(c59(x_1)) = x_1 POL(c60(x_1)) = x_1 POL(c61(x_1)) = x_1 POL(c62(x_1)) = x_1 POL(c63(x_1)) = x_1 POL(c64(x_1)) = x_1 POL(c65(x_1)) = x_1 POL(c66(x_1)) = x_1 POL(c67(x_1)) = x_1 POL(c68(x_1)) = x_1 POL(c69(x_1)) = x_1 POL(c70(x_1)) = x_1 POL(c71(x_1)) = x_1 POL(c72(x_1)) = x_1 POL(c73(x_1)) = x_1 POL(c74(x_1)) = x_1 POL(c75(x_1)) = x_1 POL(c76(x_1)) = x_1 POL(c77(x_1)) = x_1 POL(c78(x_1)) = x_1 POL(c79(x_1)) = x_1 POL(c81(x_1)) = x_1 POL(c82(x_1)) = x_1 POL(s(x_1)) = [1] + x_1 ---------------------------------------- (24) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: F_1'(z0) -> c32(G_1'(z0, z0)) F_2'(z0) -> c34(G_2'(z0, z0)) G_2'(s(z0), z1) -> c35(F_1'(z1), G_2'(z0, z1)) F_3'(z0) -> c36(G_3'(z0, z0)) G_3'(s(z0), z1) -> c37(F_2'(z1), G_3'(z0, z1)) F_4'(z0) -> c38(G_4'(z0, z0)) G_4'(s(z0), z1) -> c39(F_3'(z1), G_4'(z0, z1)) F_5'(z0) -> c40(G_5'(z0, z0)) G_5'(s(z0), z1) -> c41(F_4'(z1), G_5'(z0, z1)) F_6'(z0) -> c42(G_6'(z0, z0)) G_6'(s(z0), z1) -> c43(F_5'(z1), G_6'(z0, z1)) F_7'(z0) -> c44(G_7'(z0, z0)) G_7'(s(z0), z1) -> c45(F_6'(z1), G_7'(z0, z1)) F_8'(z0) -> c46(G_8'(z0, z0)) G_8'(s(z0), z1) -> c47(F_7'(z1), G_8'(z0, z1)) F_9'(z0) -> c48(G_9'(z0, z0)) G_9'(s(z0), z1) -> c49(F_8'(z1), G_9'(z0, z1)) G_10'(s(z0), z1) -> c51(F_9'(z1), G_10'(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) G_1'(s(z0), z1) -> c33(G_1'(z0, z1)) S tuples: G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) K tuples: G_9''(s(z0), z1) -> c78(F_8''(z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) F_9''(z0) -> c77(G_9''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) F_4''(z0) -> c62(G_4''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) F_3''(z0) -> c59(G_3''(z0, z0)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) Defined Rule Symbols:none Defined Pair Symbols: F_1'_1, F_2'_1, G_2'_2, F_3'_1, G_3'_2, F_4'_1, G_4'_2, F_5'_1, G_5'_2, F_6'_1, G_6'_2, F_7'_1, G_7'_2, F_8'_1, G_8'_2, F_9'_1, G_9'_2, G_10'_2, F_1''_1, G_1''_2, F_2''_1, G_2''_2, F_3''_1, G_3''_2, F_4''_1, G_4''_2, F_5''_1, G_5''_2, F_6''_1, G_6''_2, F_7''_1, G_7''_2, F_8''_1, G_8''_2, F_9''_1, G_9''_2, G_10''_2, G_1'_2 Compound Symbols: c32_1, c34_1, c35_2, c36_1, c37_2, c38_1, c39_2, c40_1, c41_2, c42_1, c43_2, c44_1, c45_2, c46_1, c47_2, c48_1, c49_2, c51_2, c53_1, c55_1, c56_1, c57_1, c58_1, c59_1, c60_1, c61_1, c62_1, c63_1, c64_1, c65_1, c66_1, c67_1, c68_1, c69_1, c70_1, c71_1, c72_1, c73_1, c74_1, c75_1, c76_1, c77_1, c78_1, c79_1, c81_1, c82_1, c33_1 ---------------------------------------- (25) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) G_4''(s(z0), z1) -> c63(F_3''(z1)) We considered the (Usable) Rules:none And the Tuples: F_1'(z0) -> c32(G_1'(z0, z0)) F_2'(z0) -> c34(G_2'(z0, z0)) G_2'(s(z0), z1) -> c35(F_1'(z1), G_2'(z0, z1)) F_3'(z0) -> c36(G_3'(z0, z0)) G_3'(s(z0), z1) -> c37(F_2'(z1), G_3'(z0, z1)) F_4'(z0) -> c38(G_4'(z0, z0)) G_4'(s(z0), z1) -> c39(F_3'(z1), G_4'(z0, z1)) F_5'(z0) -> c40(G_5'(z0, z0)) G_5'(s(z0), z1) -> c41(F_4'(z1), G_5'(z0, z1)) F_6'(z0) -> c42(G_6'(z0, z0)) G_6'(s(z0), z1) -> c43(F_5'(z1), G_6'(z0, z1)) F_7'(z0) -> c44(G_7'(z0, z0)) G_7'(s(z0), z1) -> c45(F_6'(z1), G_7'(z0, z1)) F_8'(z0) -> c46(G_8'(z0, z0)) G_8'(s(z0), z1) -> c47(F_7'(z1), G_8'(z0, z1)) F_9'(z0) -> c48(G_9'(z0, z0)) G_9'(s(z0), z1) -> c49(F_8'(z1), G_9'(z0, z1)) G_10'(s(z0), z1) -> c51(F_9'(z1), G_10'(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) G_1'(s(z0), z1) -> c33(G_1'(z0, z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(F_1'(x_1)) = 0 POL(F_1''(x_1)) = [1] POL(F_2'(x_1)) = 0 POL(F_2''(x_1)) = [1] POL(F_3'(x_1)) = 0 POL(F_3''(x_1)) = x_1 POL(F_4'(x_1)) = 0 POL(F_4''(x_1)) = [1] + x_1 POL(F_5'(x_1)) = 0 POL(F_5''(x_1)) = [1] + x_1 POL(F_6'(x_1)) = 0 POL(F_6''(x_1)) = [1] + x_1 POL(F_7'(x_1)) = 0 POL(F_7''(x_1)) = [1] + x_1 POL(F_8'(x_1)) = 0 POL(F_8''(x_1)) = [1] + x_1 POL(F_9'(x_1)) = [1] POL(F_9''(x_1)) = [1] + x_1 POL(G_1'(x_1, x_2)) = 0 POL(G_1''(x_1, x_2)) = [1] POL(G_10'(x_1, x_2)) = x_1 POL(G_10''(x_1, x_2)) = x_1 + x_2 POL(G_2'(x_1, x_2)) = 0 POL(G_2''(x_1, x_2)) = [1] POL(G_3'(x_1, x_2)) = 0 POL(G_3''(x_1, x_2)) = x_1 POL(G_4'(x_1, x_2)) = 0 POL(G_4''(x_1, x_2)) = [1] + x_2 POL(G_5'(x_1, x_2)) = 0 POL(G_5''(x_1, x_2)) = [1] + x_2 POL(G_6'(x_1, x_2)) = 0 POL(G_6''(x_1, x_2)) = [1] + x_2 POL(G_7'(x_1, x_2)) = 0 POL(G_7''(x_1, x_2)) = [1] + x_2 POL(G_8'(x_1, x_2)) = 0 POL(G_8''(x_1, x_2)) = [1] + x_2 POL(G_9'(x_1, x_2)) = [1] POL(G_9''(x_1, x_2)) = [1] + x_2 POL(c32(x_1)) = x_1 POL(c33(x_1)) = x_1 POL(c34(x_1)) = x_1 POL(c35(x_1, x_2)) = x_1 + x_2 POL(c36(x_1)) = x_1 POL(c37(x_1, x_2)) = x_1 + x_2 POL(c38(x_1)) = x_1 POL(c39(x_1, x_2)) = x_1 + x_2 POL(c40(x_1)) = x_1 POL(c41(x_1, x_2)) = x_1 + x_2 POL(c42(x_1)) = x_1 POL(c43(x_1, x_2)) = x_1 + x_2 POL(c44(x_1)) = x_1 POL(c45(x_1, x_2)) = x_1 + x_2 POL(c46(x_1)) = x_1 POL(c47(x_1, x_2)) = x_1 + x_2 POL(c48(x_1)) = x_1 POL(c49(x_1, x_2)) = x_1 + x_2 POL(c51(x_1, x_2)) = x_1 + x_2 POL(c53(x_1)) = x_1 POL(c55(x_1)) = x_1 POL(c56(x_1)) = x_1 POL(c57(x_1)) = x_1 POL(c58(x_1)) = x_1 POL(c59(x_1)) = x_1 POL(c60(x_1)) = x_1 POL(c61(x_1)) = x_1 POL(c62(x_1)) = x_1 POL(c63(x_1)) = x_1 POL(c64(x_1)) = x_1 POL(c65(x_1)) = x_1 POL(c66(x_1)) = x_1 POL(c67(x_1)) = x_1 POL(c68(x_1)) = x_1 POL(c69(x_1)) = x_1 POL(c70(x_1)) = x_1 POL(c71(x_1)) = x_1 POL(c72(x_1)) = x_1 POL(c73(x_1)) = x_1 POL(c74(x_1)) = x_1 POL(c75(x_1)) = x_1 POL(c76(x_1)) = x_1 POL(c77(x_1)) = x_1 POL(c78(x_1)) = x_1 POL(c79(x_1)) = x_1 POL(c81(x_1)) = x_1 POL(c82(x_1)) = x_1 POL(s(x_1)) = [1] + x_1 ---------------------------------------- (26) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: F_1'(z0) -> c32(G_1'(z0, z0)) F_2'(z0) -> c34(G_2'(z0, z0)) G_2'(s(z0), z1) -> c35(F_1'(z1), G_2'(z0, z1)) F_3'(z0) -> c36(G_3'(z0, z0)) G_3'(s(z0), z1) -> c37(F_2'(z1), G_3'(z0, z1)) F_4'(z0) -> c38(G_4'(z0, z0)) G_4'(s(z0), z1) -> c39(F_3'(z1), G_4'(z0, z1)) F_5'(z0) -> c40(G_5'(z0, z0)) G_5'(s(z0), z1) -> c41(F_4'(z1), G_5'(z0, z1)) F_6'(z0) -> c42(G_6'(z0, z0)) G_6'(s(z0), z1) -> c43(F_5'(z1), G_6'(z0, z1)) F_7'(z0) -> c44(G_7'(z0, z0)) G_7'(s(z0), z1) -> c45(F_6'(z1), G_7'(z0, z1)) F_8'(z0) -> c46(G_8'(z0, z0)) G_8'(s(z0), z1) -> c47(F_7'(z1), G_8'(z0, z1)) F_9'(z0) -> c48(G_9'(z0, z0)) G_9'(s(z0), z1) -> c49(F_8'(z1), G_9'(z0, z1)) G_10'(s(z0), z1) -> c51(F_9'(z1), G_10'(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) G_1'(s(z0), z1) -> c33(G_1'(z0, z1)) S tuples: G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) K tuples: G_9''(s(z0), z1) -> c78(F_8''(z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) F_9''(z0) -> c77(G_9''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) F_4''(z0) -> c62(G_4''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) F_3''(z0) -> c59(G_3''(z0, z0)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) G_4''(s(z0), z1) -> c63(F_3''(z1)) Defined Rule Symbols:none Defined Pair Symbols: F_1'_1, F_2'_1, G_2'_2, F_3'_1, G_3'_2, F_4'_1, G_4'_2, F_5'_1, G_5'_2, F_6'_1, G_6'_2, F_7'_1, G_7'_2, F_8'_1, G_8'_2, F_9'_1, G_9'_2, G_10'_2, F_1''_1, G_1''_2, F_2''_1, G_2''_2, F_3''_1, G_3''_2, F_4''_1, G_4''_2, F_5''_1, G_5''_2, F_6''_1, G_6''_2, F_7''_1, G_7''_2, F_8''_1, G_8''_2, F_9''_1, G_9''_2, G_10''_2, G_1'_2 Compound Symbols: c32_1, c34_1, c35_2, c36_1, c37_2, c38_1, c39_2, c40_1, c41_2, c42_1, c43_2, c44_1, c45_2, c46_1, c47_2, c48_1, c49_2, c51_2, c53_1, c55_1, c56_1, c57_1, c58_1, c59_1, c60_1, c61_1, c62_1, c63_1, c64_1, c65_1, c66_1, c67_1, c68_1, c69_1, c70_1, c71_1, c72_1, c73_1, c74_1, c75_1, c76_1, c77_1, c78_1, c79_1, c81_1, c82_1, c33_1 ---------------------------------------- (27) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: G_3''(s(z0), z1) -> c60(F_2''(z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) ---------------------------------------- (28) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: F_1'(z0) -> c32(G_1'(z0, z0)) F_2'(z0) -> c34(G_2'(z0, z0)) G_2'(s(z0), z1) -> c35(F_1'(z1), G_2'(z0, z1)) F_3'(z0) -> c36(G_3'(z0, z0)) G_3'(s(z0), z1) -> c37(F_2'(z1), G_3'(z0, z1)) F_4'(z0) -> c38(G_4'(z0, z0)) G_4'(s(z0), z1) -> c39(F_3'(z1), G_4'(z0, z1)) F_5'(z0) -> c40(G_5'(z0, z0)) G_5'(s(z0), z1) -> c41(F_4'(z1), G_5'(z0, z1)) F_6'(z0) -> c42(G_6'(z0, z0)) G_6'(s(z0), z1) -> c43(F_5'(z1), G_6'(z0, z1)) F_7'(z0) -> c44(G_7'(z0, z0)) G_7'(s(z0), z1) -> c45(F_6'(z1), G_7'(z0, z1)) F_8'(z0) -> c46(G_8'(z0, z0)) G_8'(s(z0), z1) -> c47(F_7'(z1), G_8'(z0, z1)) F_9'(z0) -> c48(G_9'(z0, z0)) G_9'(s(z0), z1) -> c49(F_8'(z1), G_9'(z0, z1)) G_10'(s(z0), z1) -> c51(F_9'(z1), G_10'(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) G_1'(s(z0), z1) -> c33(G_1'(z0, z1)) S tuples: G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) K tuples: G_9''(s(z0), z1) -> c78(F_8''(z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) F_9''(z0) -> c77(G_9''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) F_4''(z0) -> c62(G_4''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) F_3''(z0) -> c59(G_3''(z0, z0)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_3''(s(z0), z1) -> c60(F_2''(z1)) F_2''(z0) -> c56(G_2''(z0, z0)) Defined Rule Symbols:none Defined Pair Symbols: F_1'_1, F_2'_1, G_2'_2, F_3'_1, G_3'_2, F_4'_1, G_4'_2, F_5'_1, G_5'_2, F_6'_1, G_6'_2, F_7'_1, G_7'_2, F_8'_1, G_8'_2, F_9'_1, G_9'_2, G_10'_2, F_1''_1, G_1''_2, F_2''_1, G_2''_2, F_3''_1, G_3''_2, F_4''_1, G_4''_2, F_5''_1, G_5''_2, F_6''_1, G_6''_2, F_7''_1, G_7''_2, F_8''_1, G_8''_2, F_9''_1, G_9''_2, G_10''_2, G_1'_2 Compound Symbols: c32_1, c34_1, c35_2, c36_1, c37_2, c38_1, c39_2, c40_1, c41_2, c42_1, c43_2, c44_1, c45_2, c46_1, c47_2, c48_1, c49_2, c51_2, c53_1, c55_1, c56_1, c57_1, c58_1, c59_1, c60_1, c61_1, c62_1, c63_1, c64_1, c65_1, c66_1, c67_1, c68_1, c69_1, c70_1, c71_1, c72_1, c73_1, c74_1, c75_1, c76_1, c77_1, c78_1, c79_1, c81_1, c82_1, c33_1 ---------------------------------------- (29) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. F_6''(z0) -> c68(G_6''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) We considered the (Usable) Rules:none And the Tuples: F_1'(z0) -> c32(G_1'(z0, z0)) F_2'(z0) -> c34(G_2'(z0, z0)) G_2'(s(z0), z1) -> c35(F_1'(z1), G_2'(z0, z1)) F_3'(z0) -> c36(G_3'(z0, z0)) G_3'(s(z0), z1) -> c37(F_2'(z1), G_3'(z0, z1)) F_4'(z0) -> c38(G_4'(z0, z0)) G_4'(s(z0), z1) -> c39(F_3'(z1), G_4'(z0, z1)) F_5'(z0) -> c40(G_5'(z0, z0)) G_5'(s(z0), z1) -> c41(F_4'(z1), G_5'(z0, z1)) F_6'(z0) -> c42(G_6'(z0, z0)) G_6'(s(z0), z1) -> c43(F_5'(z1), G_6'(z0, z1)) F_7'(z0) -> c44(G_7'(z0, z0)) G_7'(s(z0), z1) -> c45(F_6'(z1), G_7'(z0, z1)) F_8'(z0) -> c46(G_8'(z0, z0)) G_8'(s(z0), z1) -> c47(F_7'(z1), G_8'(z0, z1)) F_9'(z0) -> c48(G_9'(z0, z0)) G_9'(s(z0), z1) -> c49(F_8'(z1), G_9'(z0, z1)) G_10'(s(z0), z1) -> c51(F_9'(z1), G_10'(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) G_1'(s(z0), z1) -> c33(G_1'(z0, z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(F_1'(x_1)) = 0 POL(F_1''(x_1)) = 0 POL(F_2'(x_1)) = 0 POL(F_2''(x_1)) = 0 POL(F_3'(x_1)) = 0 POL(F_3''(x_1)) = 0 POL(F_4'(x_1)) = 0 POL(F_4''(x_1)) = 0 POL(F_5'(x_1)) = 0 POL(F_5''(x_1)) = 0 POL(F_6'(x_1)) = 0 POL(F_6''(x_1)) = [1] POL(F_7'(x_1)) = 0 POL(F_7''(x_1)) = [1] + x_1 POL(F_8'(x_1)) = 0 POL(F_8''(x_1)) = [1] + x_1 POL(F_9'(x_1)) = [1] POL(F_9''(x_1)) = [1] + x_1 POL(G_1'(x_1, x_2)) = 0 POL(G_1''(x_1, x_2)) = 0 POL(G_10'(x_1, x_2)) = x_1 POL(G_10''(x_1, x_2)) = [1] + x_2 POL(G_2'(x_1, x_2)) = 0 POL(G_2''(x_1, x_2)) = 0 POL(G_3'(x_1, x_2)) = 0 POL(G_3''(x_1, x_2)) = 0 POL(G_4'(x_1, x_2)) = 0 POL(G_4''(x_1, x_2)) = 0 POL(G_5'(x_1, x_2)) = 0 POL(G_5''(x_1, x_2)) = 0 POL(G_6'(x_1, x_2)) = 0 POL(G_6''(x_1, x_2)) = 0 POL(G_7'(x_1, x_2)) = 0 POL(G_7''(x_1, x_2)) = [1] + x_1 POL(G_8'(x_1, x_2)) = 0 POL(G_8''(x_1, x_2)) = [1] + x_2 POL(G_9'(x_1, x_2)) = [1] POL(G_9''(x_1, x_2)) = [1] + x_2 POL(c32(x_1)) = x_1 POL(c33(x_1)) = x_1 POL(c34(x_1)) = x_1 POL(c35(x_1, x_2)) = x_1 + x_2 POL(c36(x_1)) = x_1 POL(c37(x_1, x_2)) = x_1 + x_2 POL(c38(x_1)) = x_1 POL(c39(x_1, x_2)) = x_1 + x_2 POL(c40(x_1)) = x_1 POL(c41(x_1, x_2)) = x_1 + x_2 POL(c42(x_1)) = x_1 POL(c43(x_1, x_2)) = x_1 + x_2 POL(c44(x_1)) = x_1 POL(c45(x_1, x_2)) = x_1 + x_2 POL(c46(x_1)) = x_1 POL(c47(x_1, x_2)) = x_1 + x_2 POL(c48(x_1)) = x_1 POL(c49(x_1, x_2)) = x_1 + x_2 POL(c51(x_1, x_2)) = x_1 + x_2 POL(c53(x_1)) = x_1 POL(c55(x_1)) = x_1 POL(c56(x_1)) = x_1 POL(c57(x_1)) = x_1 POL(c58(x_1)) = x_1 POL(c59(x_1)) = x_1 POL(c60(x_1)) = x_1 POL(c61(x_1)) = x_1 POL(c62(x_1)) = x_1 POL(c63(x_1)) = x_1 POL(c64(x_1)) = x_1 POL(c65(x_1)) = x_1 POL(c66(x_1)) = x_1 POL(c67(x_1)) = x_1 POL(c68(x_1)) = x_1 POL(c69(x_1)) = x_1 POL(c70(x_1)) = x_1 POL(c71(x_1)) = x_1 POL(c72(x_1)) = x_1 POL(c73(x_1)) = x_1 POL(c74(x_1)) = x_1 POL(c75(x_1)) = x_1 POL(c76(x_1)) = x_1 POL(c77(x_1)) = x_1 POL(c78(x_1)) = x_1 POL(c79(x_1)) = x_1 POL(c81(x_1)) = x_1 POL(c82(x_1)) = x_1 POL(s(x_1)) = [1] + x_1 ---------------------------------------- (30) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: F_1'(z0) -> c32(G_1'(z0, z0)) F_2'(z0) -> c34(G_2'(z0, z0)) G_2'(s(z0), z1) -> c35(F_1'(z1), G_2'(z0, z1)) F_3'(z0) -> c36(G_3'(z0, z0)) G_3'(s(z0), z1) -> c37(F_2'(z1), G_3'(z0, z1)) F_4'(z0) -> c38(G_4'(z0, z0)) G_4'(s(z0), z1) -> c39(F_3'(z1), G_4'(z0, z1)) F_5'(z0) -> c40(G_5'(z0, z0)) G_5'(s(z0), z1) -> c41(F_4'(z1), G_5'(z0, z1)) F_6'(z0) -> c42(G_6'(z0, z0)) G_6'(s(z0), z1) -> c43(F_5'(z1), G_6'(z0, z1)) F_7'(z0) -> c44(G_7'(z0, z0)) G_7'(s(z0), z1) -> c45(F_6'(z1), G_7'(z0, z1)) F_8'(z0) -> c46(G_8'(z0, z0)) G_8'(s(z0), z1) -> c47(F_7'(z1), G_8'(z0, z1)) F_9'(z0) -> c48(G_9'(z0, z0)) G_9'(s(z0), z1) -> c49(F_8'(z1), G_9'(z0, z1)) G_10'(s(z0), z1) -> c51(F_9'(z1), G_10'(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) G_1'(s(z0), z1) -> c33(G_1'(z0, z1)) S tuples: G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) K tuples: G_9''(s(z0), z1) -> c78(F_8''(z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) F_9''(z0) -> c77(G_9''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) F_4''(z0) -> c62(G_4''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) F_3''(z0) -> c59(G_3''(z0, z0)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_3''(s(z0), z1) -> c60(F_2''(z1)) F_2''(z0) -> c56(G_2''(z0, z0)) F_6''(z0) -> c68(G_6''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) Defined Rule Symbols:none Defined Pair Symbols: F_1'_1, F_2'_1, G_2'_2, F_3'_1, G_3'_2, F_4'_1, G_4'_2, F_5'_1, G_5'_2, F_6'_1, G_6'_2, F_7'_1, G_7'_2, F_8'_1, G_8'_2, F_9'_1, G_9'_2, G_10'_2, F_1''_1, G_1''_2, F_2''_1, G_2''_2, F_3''_1, G_3''_2, F_4''_1, G_4''_2, F_5''_1, G_5''_2, F_6''_1, G_6''_2, F_7''_1, G_7''_2, F_8''_1, G_8''_2, F_9''_1, G_9''_2, G_10''_2, G_1'_2 Compound Symbols: c32_1, c34_1, c35_2, c36_1, c37_2, c38_1, c39_2, c40_1, c41_2, c42_1, c43_2, c44_1, c45_2, c46_1, c47_2, c48_1, c49_2, c51_2, c53_1, c55_1, c56_1, c57_1, c58_1, c59_1, c60_1, c61_1, c62_1, c63_1, c64_1, c65_1, c66_1, c67_1, c68_1, c69_1, c70_1, c71_1, c72_1, c73_1, c74_1, c75_1, c76_1, c77_1, c78_1, c79_1, c81_1, c82_1, c33_1 ---------------------------------------- (31) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. F_5''(z0) -> c65(G_5''(z0, z0)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) G_8''(s(z0), z1) -> c75(F_7''(z1)) We considered the (Usable) Rules:none And the Tuples: F_1'(z0) -> c32(G_1'(z0, z0)) F_2'(z0) -> c34(G_2'(z0, z0)) G_2'(s(z0), z1) -> c35(F_1'(z1), G_2'(z0, z1)) F_3'(z0) -> c36(G_3'(z0, z0)) G_3'(s(z0), z1) -> c37(F_2'(z1), G_3'(z0, z1)) F_4'(z0) -> c38(G_4'(z0, z0)) G_4'(s(z0), z1) -> c39(F_3'(z1), G_4'(z0, z1)) F_5'(z0) -> c40(G_5'(z0, z0)) G_5'(s(z0), z1) -> c41(F_4'(z1), G_5'(z0, z1)) F_6'(z0) -> c42(G_6'(z0, z0)) G_6'(s(z0), z1) -> c43(F_5'(z1), G_6'(z0, z1)) F_7'(z0) -> c44(G_7'(z0, z0)) G_7'(s(z0), z1) -> c45(F_6'(z1), G_7'(z0, z1)) F_8'(z0) -> c46(G_8'(z0, z0)) G_8'(s(z0), z1) -> c47(F_7'(z1), G_8'(z0, z1)) F_9'(z0) -> c48(G_9'(z0, z0)) G_9'(s(z0), z1) -> c49(F_8'(z1), G_9'(z0, z1)) G_10'(s(z0), z1) -> c51(F_9'(z1), G_10'(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) G_1'(s(z0), z1) -> c33(G_1'(z0, z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(F_1'(x_1)) = 0 POL(F_1''(x_1)) = 0 POL(F_2'(x_1)) = 0 POL(F_2''(x_1)) = 0 POL(F_3'(x_1)) = 0 POL(F_3''(x_1)) = 0 POL(F_4'(x_1)) = 0 POL(F_4''(x_1)) = 0 POL(F_5'(x_1)) = 0 POL(F_5''(x_1)) = [1] POL(F_6'(x_1)) = 0 POL(F_6''(x_1)) = x_1 POL(F_7'(x_1)) = 0 POL(F_7''(x_1)) = x_1 POL(F_8'(x_1)) = 0 POL(F_8''(x_1)) = [1] + x_1 POL(F_9'(x_1)) = [1] POL(F_9''(x_1)) = [1] + x_1 POL(G_1'(x_1, x_2)) = 0 POL(G_1''(x_1, x_2)) = 0 POL(G_10'(x_1, x_2)) = x_1 POL(G_10''(x_1, x_2)) = x_1 + x_2 POL(G_2'(x_1, x_2)) = 0 POL(G_2''(x_1, x_2)) = 0 POL(G_3'(x_1, x_2)) = 0 POL(G_3''(x_1, x_2)) = 0 POL(G_4'(x_1, x_2)) = 0 POL(G_4''(x_1, x_2)) = 0 POL(G_5'(x_1, x_2)) = 0 POL(G_5''(x_1, x_2)) = 0 POL(G_6'(x_1, x_2)) = 0 POL(G_6''(x_1, x_2)) = x_1 POL(G_7'(x_1, x_2)) = 0 POL(G_7''(x_1, x_2)) = x_2 POL(G_8'(x_1, x_2)) = 0 POL(G_8''(x_1, x_2)) = [1] + x_2 POL(G_9'(x_1, x_2)) = [1] POL(G_9''(x_1, x_2)) = [1] + x_2 POL(c32(x_1)) = x_1 POL(c33(x_1)) = x_1 POL(c34(x_1)) = x_1 POL(c35(x_1, x_2)) = x_1 + x_2 POL(c36(x_1)) = x_1 POL(c37(x_1, x_2)) = x_1 + x_2 POL(c38(x_1)) = x_1 POL(c39(x_1, x_2)) = x_1 + x_2 POL(c40(x_1)) = x_1 POL(c41(x_1, x_2)) = x_1 + x_2 POL(c42(x_1)) = x_1 POL(c43(x_1, x_2)) = x_1 + x_2 POL(c44(x_1)) = x_1 POL(c45(x_1, x_2)) = x_1 + x_2 POL(c46(x_1)) = x_1 POL(c47(x_1, x_2)) = x_1 + x_2 POL(c48(x_1)) = x_1 POL(c49(x_1, x_2)) = x_1 + x_2 POL(c51(x_1, x_2)) = x_1 + x_2 POL(c53(x_1)) = x_1 POL(c55(x_1)) = x_1 POL(c56(x_1)) = x_1 POL(c57(x_1)) = x_1 POL(c58(x_1)) = x_1 POL(c59(x_1)) = x_1 POL(c60(x_1)) = x_1 POL(c61(x_1)) = x_1 POL(c62(x_1)) = x_1 POL(c63(x_1)) = x_1 POL(c64(x_1)) = x_1 POL(c65(x_1)) = x_1 POL(c66(x_1)) = x_1 POL(c67(x_1)) = x_1 POL(c68(x_1)) = x_1 POL(c69(x_1)) = x_1 POL(c70(x_1)) = x_1 POL(c71(x_1)) = x_1 POL(c72(x_1)) = x_1 POL(c73(x_1)) = x_1 POL(c74(x_1)) = x_1 POL(c75(x_1)) = x_1 POL(c76(x_1)) = x_1 POL(c77(x_1)) = x_1 POL(c78(x_1)) = x_1 POL(c79(x_1)) = x_1 POL(c81(x_1)) = x_1 POL(c82(x_1)) = x_1 POL(s(x_1)) = [1] + x_1 ---------------------------------------- (32) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: F_1'(z0) -> c32(G_1'(z0, z0)) F_2'(z0) -> c34(G_2'(z0, z0)) G_2'(s(z0), z1) -> c35(F_1'(z1), G_2'(z0, z1)) F_3'(z0) -> c36(G_3'(z0, z0)) G_3'(s(z0), z1) -> c37(F_2'(z1), G_3'(z0, z1)) F_4'(z0) -> c38(G_4'(z0, z0)) G_4'(s(z0), z1) -> c39(F_3'(z1), G_4'(z0, z1)) F_5'(z0) -> c40(G_5'(z0, z0)) G_5'(s(z0), z1) -> c41(F_4'(z1), G_5'(z0, z1)) F_6'(z0) -> c42(G_6'(z0, z0)) G_6'(s(z0), z1) -> c43(F_5'(z1), G_6'(z0, z1)) F_7'(z0) -> c44(G_7'(z0, z0)) G_7'(s(z0), z1) -> c45(F_6'(z1), G_7'(z0, z1)) F_8'(z0) -> c46(G_8'(z0, z0)) G_8'(s(z0), z1) -> c47(F_7'(z1), G_8'(z0, z1)) F_9'(z0) -> c48(G_9'(z0, z0)) G_9'(s(z0), z1) -> c49(F_8'(z1), G_9'(z0, z1)) G_10'(s(z0), z1) -> c51(F_9'(z1), G_10'(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) G_1'(s(z0), z1) -> c33(G_1'(z0, z1)) S tuples: G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) K tuples: G_9''(s(z0), z1) -> c78(F_8''(z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) F_9''(z0) -> c77(G_9''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) F_4''(z0) -> c62(G_4''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) F_3''(z0) -> c59(G_3''(z0, z0)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_3''(s(z0), z1) -> c60(F_2''(z1)) F_2''(z0) -> c56(G_2''(z0, z0)) F_6''(z0) -> c68(G_6''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) G_8''(s(z0), z1) -> c75(F_7''(z1)) Defined Rule Symbols:none Defined Pair Symbols: F_1'_1, F_2'_1, G_2'_2, F_3'_1, G_3'_2, F_4'_1, G_4'_2, F_5'_1, G_5'_2, F_6'_1, G_6'_2, F_7'_1, G_7'_2, F_8'_1, G_8'_2, F_9'_1, G_9'_2, G_10'_2, F_1''_1, G_1''_2, F_2''_1, G_2''_2, F_3''_1, G_3''_2, F_4''_1, G_4''_2, F_5''_1, G_5''_2, F_6''_1, G_6''_2, F_7''_1, G_7''_2, F_8''_1, G_8''_2, F_9''_1, G_9''_2, G_10''_2, G_1'_2 Compound Symbols: c32_1, c34_1, c35_2, c36_1, c37_2, c38_1, c39_2, c40_1, c41_2, c42_1, c43_2, c44_1, c45_2, c46_1, c47_2, c48_1, c49_2, c51_2, c53_1, c55_1, c56_1, c57_1, c58_1, c59_1, c60_1, c61_1, c62_1, c63_1, c64_1, c65_1, c66_1, c67_1, c68_1, c69_1, c70_1, c71_1, c72_1, c73_1, c74_1, c75_1, c76_1, c77_1, c78_1, c79_1, c81_1, c82_1, c33_1 ---------------------------------------- (33) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: G_6''(s(z0), z1) -> c69(F_5''(z1)) F_5''(z0) -> c65(G_5''(z0, z0)) ---------------------------------------- (34) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: F_1'(z0) -> c32(G_1'(z0, z0)) F_2'(z0) -> c34(G_2'(z0, z0)) G_2'(s(z0), z1) -> c35(F_1'(z1), G_2'(z0, z1)) F_3'(z0) -> c36(G_3'(z0, z0)) G_3'(s(z0), z1) -> c37(F_2'(z1), G_3'(z0, z1)) F_4'(z0) -> c38(G_4'(z0, z0)) G_4'(s(z0), z1) -> c39(F_3'(z1), G_4'(z0, z1)) F_5'(z0) -> c40(G_5'(z0, z0)) G_5'(s(z0), z1) -> c41(F_4'(z1), G_5'(z0, z1)) F_6'(z0) -> c42(G_6'(z0, z0)) G_6'(s(z0), z1) -> c43(F_5'(z1), G_6'(z0, z1)) F_7'(z0) -> c44(G_7'(z0, z0)) G_7'(s(z0), z1) -> c45(F_6'(z1), G_7'(z0, z1)) F_8'(z0) -> c46(G_8'(z0, z0)) G_8'(s(z0), z1) -> c47(F_7'(z1), G_8'(z0, z1)) F_9'(z0) -> c48(G_9'(z0, z0)) G_9'(s(z0), z1) -> c49(F_8'(z1), G_9'(z0, z1)) G_10'(s(z0), z1) -> c51(F_9'(z1), G_10'(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) G_1'(s(z0), z1) -> c33(G_1'(z0, z1)) S tuples: G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) K tuples: G_9''(s(z0), z1) -> c78(F_8''(z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) F_9''(z0) -> c77(G_9''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) F_4''(z0) -> c62(G_4''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) F_3''(z0) -> c59(G_3''(z0, z0)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_3''(s(z0), z1) -> c60(F_2''(z1)) F_2''(z0) -> c56(G_2''(z0, z0)) F_6''(z0) -> c68(G_6''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_6''(s(z0), z1) -> c69(F_5''(z1)) Defined Rule Symbols:none Defined Pair Symbols: F_1'_1, F_2'_1, G_2'_2, F_3'_1, G_3'_2, F_4'_1, G_4'_2, F_5'_1, G_5'_2, F_6'_1, G_6'_2, F_7'_1, G_7'_2, F_8'_1, G_8'_2, F_9'_1, G_9'_2, G_10'_2, F_1''_1, G_1''_2, F_2''_1, G_2''_2, F_3''_1, G_3''_2, F_4''_1, G_4''_2, F_5''_1, G_5''_2, F_6''_1, G_6''_2, F_7''_1, G_7''_2, F_8''_1, G_8''_2, F_9''_1, G_9''_2, G_10''_2, G_1'_2 Compound Symbols: c32_1, c34_1, c35_2, c36_1, c37_2, c38_1, c39_2, c40_1, c41_2, c42_1, c43_2, c44_1, c45_2, c46_1, c47_2, c48_1, c49_2, c51_2, c53_1, c55_1, c56_1, c57_1, c58_1, c59_1, c60_1, c61_1, c62_1, c63_1, c64_1, c65_1, c66_1, c67_1, c68_1, c69_1, c70_1, c71_1, c72_1, c73_1, c74_1, c75_1, c76_1, c77_1, c78_1, c79_1, c81_1, c82_1, c33_1 ---------------------------------------- (35) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) We considered the (Usable) Rules:none And the Tuples: F_1'(z0) -> c32(G_1'(z0, z0)) F_2'(z0) -> c34(G_2'(z0, z0)) G_2'(s(z0), z1) -> c35(F_1'(z1), G_2'(z0, z1)) F_3'(z0) -> c36(G_3'(z0, z0)) G_3'(s(z0), z1) -> c37(F_2'(z1), G_3'(z0, z1)) F_4'(z0) -> c38(G_4'(z0, z0)) G_4'(s(z0), z1) -> c39(F_3'(z1), G_4'(z0, z1)) F_5'(z0) -> c40(G_5'(z0, z0)) G_5'(s(z0), z1) -> c41(F_4'(z1), G_5'(z0, z1)) F_6'(z0) -> c42(G_6'(z0, z0)) G_6'(s(z0), z1) -> c43(F_5'(z1), G_6'(z0, z1)) F_7'(z0) -> c44(G_7'(z0, z0)) G_7'(s(z0), z1) -> c45(F_6'(z1), G_7'(z0, z1)) F_8'(z0) -> c46(G_8'(z0, z0)) G_8'(s(z0), z1) -> c47(F_7'(z1), G_8'(z0, z1)) F_9'(z0) -> c48(G_9'(z0, z0)) G_9'(s(z0), z1) -> c49(F_8'(z1), G_9'(z0, z1)) G_10'(s(z0), z1) -> c51(F_9'(z1), G_10'(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) G_1'(s(z0), z1) -> c33(G_1'(z0, z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(F_1'(x_1)) = 0 POL(F_1''(x_1)) = [3]x_1 POL(F_2'(x_1)) = 0 POL(F_2''(x_1)) = [3]x_1 POL(F_3'(x_1)) = 0 POL(F_3''(x_1)) = [3]x_1 POL(F_4'(x_1)) = 0 POL(F_4''(x_1)) = [3]x_1 POL(F_5'(x_1)) = 0 POL(F_5''(x_1)) = [3]x_1 POL(F_6'(x_1)) = 0 POL(F_6''(x_1)) = [3]x_1 POL(F_7'(x_1)) = 0 POL(F_7''(x_1)) = [3]x_1 POL(F_8'(x_1)) = 0 POL(F_8''(x_1)) = [3]x_1 POL(F_9'(x_1)) = 0 POL(F_9''(x_1)) = [1] + [3]x_1 POL(G_1'(x_1, x_2)) = 0 POL(G_1''(x_1, x_2)) = [3]x_1 POL(G_10'(x_1, x_2)) = [3]x_1 POL(G_10''(x_1, x_2)) = [3] + [3]x_1 + [3]x_2 POL(G_2'(x_1, x_2)) = 0 POL(G_2''(x_1, x_2)) = [3]x_2 POL(G_3'(x_1, x_2)) = 0 POL(G_3''(x_1, x_2)) = [3]x_2 POL(G_4'(x_1, x_2)) = 0 POL(G_4''(x_1, x_2)) = [3]x_2 POL(G_5'(x_1, x_2)) = 0 POL(G_5''(x_1, x_2)) = [3]x_2 POL(G_6'(x_1, x_2)) = 0 POL(G_6''(x_1, x_2)) = [3]x_2 POL(G_7'(x_1, x_2)) = 0 POL(G_7''(x_1, x_2)) = [3]x_2 POL(G_8'(x_1, x_2)) = 0 POL(G_8''(x_1, x_2)) = [3]x_2 POL(G_9'(x_1, x_2)) = 0 POL(G_9''(x_1, x_2)) = [3]x_2 POL(c32(x_1)) = x_1 POL(c33(x_1)) = x_1 POL(c34(x_1)) = x_1 POL(c35(x_1, x_2)) = x_1 + x_2 POL(c36(x_1)) = x_1 POL(c37(x_1, x_2)) = x_1 + x_2 POL(c38(x_1)) = x_1 POL(c39(x_1, x_2)) = x_1 + x_2 POL(c40(x_1)) = x_1 POL(c41(x_1, x_2)) = x_1 + x_2 POL(c42(x_1)) = x_1 POL(c43(x_1, x_2)) = x_1 + x_2 POL(c44(x_1)) = x_1 POL(c45(x_1, x_2)) = x_1 + x_2 POL(c46(x_1)) = x_1 POL(c47(x_1, x_2)) = x_1 + x_2 POL(c48(x_1)) = x_1 POL(c49(x_1, x_2)) = x_1 + x_2 POL(c51(x_1, x_2)) = x_1 + x_2 POL(c53(x_1)) = x_1 POL(c55(x_1)) = x_1 POL(c56(x_1)) = x_1 POL(c57(x_1)) = x_1 POL(c58(x_1)) = x_1 POL(c59(x_1)) = x_1 POL(c60(x_1)) = x_1 POL(c61(x_1)) = x_1 POL(c62(x_1)) = x_1 POL(c63(x_1)) = x_1 POL(c64(x_1)) = x_1 POL(c65(x_1)) = x_1 POL(c66(x_1)) = x_1 POL(c67(x_1)) = x_1 POL(c68(x_1)) = x_1 POL(c69(x_1)) = x_1 POL(c70(x_1)) = x_1 POL(c71(x_1)) = x_1 POL(c72(x_1)) = x_1 POL(c73(x_1)) = x_1 POL(c74(x_1)) = x_1 POL(c75(x_1)) = x_1 POL(c76(x_1)) = x_1 POL(c77(x_1)) = x_1 POL(c78(x_1)) = x_1 POL(c79(x_1)) = x_1 POL(c81(x_1)) = x_1 POL(c82(x_1)) = x_1 POL(s(x_1)) = [3] + x_1 ---------------------------------------- (36) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: F_1'(z0) -> c32(G_1'(z0, z0)) F_2'(z0) -> c34(G_2'(z0, z0)) G_2'(s(z0), z1) -> c35(F_1'(z1), G_2'(z0, z1)) F_3'(z0) -> c36(G_3'(z0, z0)) G_3'(s(z0), z1) -> c37(F_2'(z1), G_3'(z0, z1)) F_4'(z0) -> c38(G_4'(z0, z0)) G_4'(s(z0), z1) -> c39(F_3'(z1), G_4'(z0, z1)) F_5'(z0) -> c40(G_5'(z0, z0)) G_5'(s(z0), z1) -> c41(F_4'(z1), G_5'(z0, z1)) F_6'(z0) -> c42(G_6'(z0, z0)) G_6'(s(z0), z1) -> c43(F_5'(z1), G_6'(z0, z1)) F_7'(z0) -> c44(G_7'(z0, z0)) G_7'(s(z0), z1) -> c45(F_6'(z1), G_7'(z0, z1)) F_8'(z0) -> c46(G_8'(z0, z0)) G_8'(s(z0), z1) -> c47(F_7'(z1), G_8'(z0, z1)) F_9'(z0) -> c48(G_9'(z0, z0)) G_9'(s(z0), z1) -> c49(F_8'(z1), G_9'(z0, z1)) G_10'(s(z0), z1) -> c51(F_9'(z1), G_10'(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) G_1'(s(z0), z1) -> c33(G_1'(z0, z1)) S tuples: G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) K tuples: G_9''(s(z0), z1) -> c78(F_8''(z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) F_9''(z0) -> c77(G_9''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) F_4''(z0) -> c62(G_4''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) F_3''(z0) -> c59(G_3''(z0, z0)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_3''(s(z0), z1) -> c60(F_2''(z1)) F_2''(z0) -> c56(G_2''(z0, z0)) F_6''(z0) -> c68(G_6''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) Defined Rule Symbols:none Defined Pair Symbols: F_1'_1, F_2'_1, G_2'_2, F_3'_1, G_3'_2, F_4'_1, G_4'_2, F_5'_1, G_5'_2, F_6'_1, G_6'_2, F_7'_1, G_7'_2, F_8'_1, G_8'_2, F_9'_1, G_9'_2, G_10'_2, F_1''_1, G_1''_2, F_2''_1, G_2''_2, F_3''_1, G_3''_2, F_4''_1, G_4''_2, F_5''_1, G_5''_2, F_6''_1, G_6''_2, F_7''_1, G_7''_2, F_8''_1, G_8''_2, F_9''_1, G_9''_2, G_10''_2, G_1'_2 Compound Symbols: c32_1, c34_1, c35_2, c36_1, c37_2, c38_1, c39_2, c40_1, c41_2, c42_1, c43_2, c44_1, c45_2, c46_1, c47_2, c48_1, c49_2, c51_2, c53_1, c55_1, c56_1, c57_1, c58_1, c59_1, c60_1, c61_1, c62_1, c63_1, c64_1, c65_1, c66_1, c67_1, c68_1, c69_1, c70_1, c71_1, c72_1, c73_1, c74_1, c75_1, c76_1, c77_1, c78_1, c79_1, c81_1, c82_1, c33_1 ---------------------------------------- (37) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) We considered the (Usable) Rules:none And the Tuples: F_1'(z0) -> c32(G_1'(z0, z0)) F_2'(z0) -> c34(G_2'(z0, z0)) G_2'(s(z0), z1) -> c35(F_1'(z1), G_2'(z0, z1)) F_3'(z0) -> c36(G_3'(z0, z0)) G_3'(s(z0), z1) -> c37(F_2'(z1), G_3'(z0, z1)) F_4'(z0) -> c38(G_4'(z0, z0)) G_4'(s(z0), z1) -> c39(F_3'(z1), G_4'(z0, z1)) F_5'(z0) -> c40(G_5'(z0, z0)) G_5'(s(z0), z1) -> c41(F_4'(z1), G_5'(z0, z1)) F_6'(z0) -> c42(G_6'(z0, z0)) G_6'(s(z0), z1) -> c43(F_5'(z1), G_6'(z0, z1)) F_7'(z0) -> c44(G_7'(z0, z0)) G_7'(s(z0), z1) -> c45(F_6'(z1), G_7'(z0, z1)) F_8'(z0) -> c46(G_8'(z0, z0)) G_8'(s(z0), z1) -> c47(F_7'(z1), G_8'(z0, z1)) F_9'(z0) -> c48(G_9'(z0, z0)) G_9'(s(z0), z1) -> c49(F_8'(z1), G_9'(z0, z1)) G_10'(s(z0), z1) -> c51(F_9'(z1), G_10'(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) G_1'(s(z0), z1) -> c33(G_1'(z0, z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(F_1'(x_1)) = 0 POL(F_1''(x_1)) = 0 POL(F_2'(x_1)) = 0 POL(F_2''(x_1)) = 0 POL(F_3'(x_1)) = 0 POL(F_3''(x_1)) = 0 POL(F_4'(x_1)) = 0 POL(F_4''(x_1)) = [1] + x_1 POL(F_5'(x_1)) = 0 POL(F_5''(x_1)) = [1] + x_1 POL(F_6'(x_1)) = 0 POL(F_6''(x_1)) = [1] + x_1 POL(F_7'(x_1)) = 0 POL(F_7''(x_1)) = [1] + x_1 POL(F_8'(x_1)) = 0 POL(F_8''(x_1)) = [1] + x_1 POL(F_9'(x_1)) = [1] POL(F_9''(x_1)) = [1] + x_1 POL(G_1'(x_1, x_2)) = 0 POL(G_1''(x_1, x_2)) = 0 POL(G_10'(x_1, x_2)) = x_1 POL(G_10''(x_1, x_2)) = [1] + x_2 POL(G_2'(x_1, x_2)) = 0 POL(G_2''(x_1, x_2)) = 0 POL(G_3'(x_1, x_2)) = 0 POL(G_3''(x_1, x_2)) = 0 POL(G_4'(x_1, x_2)) = 0 POL(G_4''(x_1, x_2)) = [1] + x_1 POL(G_5'(x_1, x_2)) = 0 POL(G_5''(x_1, x_2)) = [1] + x_2 POL(G_6'(x_1, x_2)) = 0 POL(G_6''(x_1, x_2)) = [1] + x_2 POL(G_7'(x_1, x_2)) = 0 POL(G_7''(x_1, x_2)) = [1] + x_2 POL(G_8'(x_1, x_2)) = 0 POL(G_8''(x_1, x_2)) = [1] + x_2 POL(G_9'(x_1, x_2)) = [1] POL(G_9''(x_1, x_2)) = [1] + x_2 POL(c32(x_1)) = x_1 POL(c33(x_1)) = x_1 POL(c34(x_1)) = x_1 POL(c35(x_1, x_2)) = x_1 + x_2 POL(c36(x_1)) = x_1 POL(c37(x_1, x_2)) = x_1 + x_2 POL(c38(x_1)) = x_1 POL(c39(x_1, x_2)) = x_1 + x_2 POL(c40(x_1)) = x_1 POL(c41(x_1, x_2)) = x_1 + x_2 POL(c42(x_1)) = x_1 POL(c43(x_1, x_2)) = x_1 + x_2 POL(c44(x_1)) = x_1 POL(c45(x_1, x_2)) = x_1 + x_2 POL(c46(x_1)) = x_1 POL(c47(x_1, x_2)) = x_1 + x_2 POL(c48(x_1)) = x_1 POL(c49(x_1, x_2)) = x_1 + x_2 POL(c51(x_1, x_2)) = x_1 + x_2 POL(c53(x_1)) = x_1 POL(c55(x_1)) = x_1 POL(c56(x_1)) = x_1 POL(c57(x_1)) = x_1 POL(c58(x_1)) = x_1 POL(c59(x_1)) = x_1 POL(c60(x_1)) = x_1 POL(c61(x_1)) = x_1 POL(c62(x_1)) = x_1 POL(c63(x_1)) = x_1 POL(c64(x_1)) = x_1 POL(c65(x_1)) = x_1 POL(c66(x_1)) = x_1 POL(c67(x_1)) = x_1 POL(c68(x_1)) = x_1 POL(c69(x_1)) = x_1 POL(c70(x_1)) = x_1 POL(c71(x_1)) = x_1 POL(c72(x_1)) = x_1 POL(c73(x_1)) = x_1 POL(c74(x_1)) = x_1 POL(c75(x_1)) = x_1 POL(c76(x_1)) = x_1 POL(c77(x_1)) = x_1 POL(c78(x_1)) = x_1 POL(c79(x_1)) = x_1 POL(c81(x_1)) = x_1 POL(c82(x_1)) = x_1 POL(s(x_1)) = [1] + x_1 ---------------------------------------- (38) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: F_1'(z0) -> c32(G_1'(z0, z0)) F_2'(z0) -> c34(G_2'(z0, z0)) G_2'(s(z0), z1) -> c35(F_1'(z1), G_2'(z0, z1)) F_3'(z0) -> c36(G_3'(z0, z0)) G_3'(s(z0), z1) -> c37(F_2'(z1), G_3'(z0, z1)) F_4'(z0) -> c38(G_4'(z0, z0)) G_4'(s(z0), z1) -> c39(F_3'(z1), G_4'(z0, z1)) F_5'(z0) -> c40(G_5'(z0, z0)) G_5'(s(z0), z1) -> c41(F_4'(z1), G_5'(z0, z1)) F_6'(z0) -> c42(G_6'(z0, z0)) G_6'(s(z0), z1) -> c43(F_5'(z1), G_6'(z0, z1)) F_7'(z0) -> c44(G_7'(z0, z0)) G_7'(s(z0), z1) -> c45(F_6'(z1), G_7'(z0, z1)) F_8'(z0) -> c46(G_8'(z0, z0)) G_8'(s(z0), z1) -> c47(F_7'(z1), G_8'(z0, z1)) F_9'(z0) -> c48(G_9'(z0, z0)) G_9'(s(z0), z1) -> c49(F_8'(z1), G_9'(z0, z1)) G_10'(s(z0), z1) -> c51(F_9'(z1), G_10'(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) G_1'(s(z0), z1) -> c33(G_1'(z0, z1)) S tuples: G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) K tuples: G_9''(s(z0), z1) -> c78(F_8''(z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) F_9''(z0) -> c77(G_9''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) F_4''(z0) -> c62(G_4''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) F_3''(z0) -> c59(G_3''(z0, z0)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_3''(s(z0), z1) -> c60(F_2''(z1)) F_2''(z0) -> c56(G_2''(z0, z0)) F_6''(z0) -> c68(G_6''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) Defined Rule Symbols:none Defined Pair Symbols: F_1'_1, F_2'_1, G_2'_2, F_3'_1, G_3'_2, F_4'_1, G_4'_2, F_5'_1, G_5'_2, F_6'_1, G_6'_2, F_7'_1, G_7'_2, F_8'_1, G_8'_2, F_9'_1, G_9'_2, G_10'_2, F_1''_1, G_1''_2, F_2''_1, G_2''_2, F_3''_1, G_3''_2, F_4''_1, G_4''_2, F_5''_1, G_5''_2, F_6''_1, G_6''_2, F_7''_1, G_7''_2, F_8''_1, G_8''_2, F_9''_1, G_9''_2, G_10''_2, G_1'_2 Compound Symbols: c32_1, c34_1, c35_2, c36_1, c37_2, c38_1, c39_2, c40_1, c41_2, c42_1, c43_2, c44_1, c45_2, c46_1, c47_2, c48_1, c49_2, c51_2, c53_1, c55_1, c56_1, c57_1, c58_1, c59_1, c60_1, c61_1, c62_1, c63_1, c64_1, c65_1, c66_1, c67_1, c68_1, c69_1, c70_1, c71_1, c72_1, c73_1, c74_1, c75_1, c76_1, c77_1, c78_1, c79_1, c81_1, c82_1, c33_1 ---------------------------------------- (39) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) We considered the (Usable) Rules:none And the Tuples: F_1'(z0) -> c32(G_1'(z0, z0)) F_2'(z0) -> c34(G_2'(z0, z0)) G_2'(s(z0), z1) -> c35(F_1'(z1), G_2'(z0, z1)) F_3'(z0) -> c36(G_3'(z0, z0)) G_3'(s(z0), z1) -> c37(F_2'(z1), G_3'(z0, z1)) F_4'(z0) -> c38(G_4'(z0, z0)) G_4'(s(z0), z1) -> c39(F_3'(z1), G_4'(z0, z1)) F_5'(z0) -> c40(G_5'(z0, z0)) G_5'(s(z0), z1) -> c41(F_4'(z1), G_5'(z0, z1)) F_6'(z0) -> c42(G_6'(z0, z0)) G_6'(s(z0), z1) -> c43(F_5'(z1), G_6'(z0, z1)) F_7'(z0) -> c44(G_7'(z0, z0)) G_7'(s(z0), z1) -> c45(F_6'(z1), G_7'(z0, z1)) F_8'(z0) -> c46(G_8'(z0, z0)) G_8'(s(z0), z1) -> c47(F_7'(z1), G_8'(z0, z1)) F_9'(z0) -> c48(G_9'(z0, z0)) G_9'(s(z0), z1) -> c49(F_8'(z1), G_9'(z0, z1)) G_10'(s(z0), z1) -> c51(F_9'(z1), G_10'(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) G_1'(s(z0), z1) -> c33(G_1'(z0, z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(F_1'(x_1)) = 0 POL(F_1''(x_1)) = 0 POL(F_2'(x_1)) = 0 POL(F_2''(x_1)) = 0 POL(F_3'(x_1)) = 0 POL(F_3''(x_1)) = 0 POL(F_4'(x_1)) = 0 POL(F_4''(x_1)) = 0 POL(F_5'(x_1)) = 0 POL(F_5''(x_1)) = [1] POL(F_6'(x_1)) = 0 POL(F_6''(x_1)) = [1] POL(F_7'(x_1)) = 0 POL(F_7''(x_1)) = [3] + [2]x_1 POL(F_8'(x_1)) = 0 POL(F_8''(x_1)) = [3]x_1 POL(F_9'(x_1)) = [2] POL(F_9''(x_1)) = [1] + [3]x_1 POL(G_1'(x_1, x_2)) = 0 POL(G_1''(x_1, x_2)) = 0 POL(G_10'(x_1, x_2)) = [2]x_1 POL(G_10''(x_1, x_2)) = [3] + [3]x_1 + [3]x_2 POL(G_2'(x_1, x_2)) = 0 POL(G_2''(x_1, x_2)) = 0 POL(G_3'(x_1, x_2)) = 0 POL(G_3''(x_1, x_2)) = 0 POL(G_4'(x_1, x_2)) = 0 POL(G_4''(x_1, x_2)) = 0 POL(G_5'(x_1, x_2)) = 0 POL(G_5''(x_1, x_2)) = 0 POL(G_6'(x_1, x_2)) = 0 POL(G_6''(x_1, x_2)) = [1] POL(G_7'(x_1, x_2)) = 0 POL(G_7''(x_1, x_2)) = [2] + x_1 + x_2 POL(G_8'(x_1, x_2)) = 0 POL(G_8''(x_1, x_2)) = x_1 + [2]x_2 POL(G_9'(x_1, x_2)) = [2] POL(G_9''(x_1, x_2)) = [3]x_2 POL(c32(x_1)) = x_1 POL(c33(x_1)) = x_1 POL(c34(x_1)) = x_1 POL(c35(x_1, x_2)) = x_1 + x_2 POL(c36(x_1)) = x_1 POL(c37(x_1, x_2)) = x_1 + x_2 POL(c38(x_1)) = x_1 POL(c39(x_1, x_2)) = x_1 + x_2 POL(c40(x_1)) = x_1 POL(c41(x_1, x_2)) = x_1 + x_2 POL(c42(x_1)) = x_1 POL(c43(x_1, x_2)) = x_1 + x_2 POL(c44(x_1)) = x_1 POL(c45(x_1, x_2)) = x_1 + x_2 POL(c46(x_1)) = x_1 POL(c47(x_1, x_2)) = x_1 + x_2 POL(c48(x_1)) = x_1 POL(c49(x_1, x_2)) = x_1 + x_2 POL(c51(x_1, x_2)) = x_1 + x_2 POL(c53(x_1)) = x_1 POL(c55(x_1)) = x_1 POL(c56(x_1)) = x_1 POL(c57(x_1)) = x_1 POL(c58(x_1)) = x_1 POL(c59(x_1)) = x_1 POL(c60(x_1)) = x_1 POL(c61(x_1)) = x_1 POL(c62(x_1)) = x_1 POL(c63(x_1)) = x_1 POL(c64(x_1)) = x_1 POL(c65(x_1)) = x_1 POL(c66(x_1)) = x_1 POL(c67(x_1)) = x_1 POL(c68(x_1)) = x_1 POL(c69(x_1)) = x_1 POL(c70(x_1)) = x_1 POL(c71(x_1)) = x_1 POL(c72(x_1)) = x_1 POL(c73(x_1)) = x_1 POL(c74(x_1)) = x_1 POL(c75(x_1)) = x_1 POL(c76(x_1)) = x_1 POL(c77(x_1)) = x_1 POL(c78(x_1)) = x_1 POL(c79(x_1)) = x_1 POL(c81(x_1)) = x_1 POL(c82(x_1)) = x_1 POL(s(x_1)) = [3] + x_1 ---------------------------------------- (40) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: F_1'(z0) -> c32(G_1'(z0, z0)) F_2'(z0) -> c34(G_2'(z0, z0)) G_2'(s(z0), z1) -> c35(F_1'(z1), G_2'(z0, z1)) F_3'(z0) -> c36(G_3'(z0, z0)) G_3'(s(z0), z1) -> c37(F_2'(z1), G_3'(z0, z1)) F_4'(z0) -> c38(G_4'(z0, z0)) G_4'(s(z0), z1) -> c39(F_3'(z1), G_4'(z0, z1)) F_5'(z0) -> c40(G_5'(z0, z0)) G_5'(s(z0), z1) -> c41(F_4'(z1), G_5'(z0, z1)) F_6'(z0) -> c42(G_6'(z0, z0)) G_6'(s(z0), z1) -> c43(F_5'(z1), G_6'(z0, z1)) F_7'(z0) -> c44(G_7'(z0, z0)) G_7'(s(z0), z1) -> c45(F_6'(z1), G_7'(z0, z1)) F_8'(z0) -> c46(G_8'(z0, z0)) G_8'(s(z0), z1) -> c47(F_7'(z1), G_8'(z0, z1)) F_9'(z0) -> c48(G_9'(z0, z0)) G_9'(s(z0), z1) -> c49(F_8'(z1), G_9'(z0, z1)) G_10'(s(z0), z1) -> c51(F_9'(z1), G_10'(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) F_2''(z0) -> c56(G_2''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_3''(z0) -> c59(G_3''(z0, z0)) G_3''(s(z0), z1) -> c60(F_2''(z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) F_4''(z0) -> c62(G_4''(z0, z0)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_6''(z0) -> c68(G_6''(z0, z0)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) F_9''(z0) -> c77(G_9''(z0, z0)) G_9''(s(z0), z1) -> c78(F_8''(z1)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) G_1'(s(z0), z1) -> c33(G_1'(z0, z1)) S tuples:none K tuples: G_9''(s(z0), z1) -> c78(F_8''(z1)) G_10''(s(z0), z1) -> c81(F_9''(z1)) G_10''(s(z0), z1) -> c82(G_10''(z0, z1)) F_8''(z0) -> c74(G_8''(z0, z0)) F_9''(z0) -> c77(G_9''(z0, z0)) G_5''(s(z0), z1) -> c66(F_4''(z1)) G_5''(s(z0), z1) -> c67(G_5''(z0, z1)) F_7''(z0) -> c71(G_7''(z0, z0)) F_4''(z0) -> c62(G_4''(z0, z0)) G_2''(s(z0), z1) -> c57(F_1''(z1)) G_2''(s(z0), z1) -> c58(G_2''(z0, z1)) F_1''(z0) -> c53(G_1''(z0, z0)) F_3''(z0) -> c59(G_3''(z0, z0)) G_9''(s(z0), z1) -> c79(G_9''(z0, z1)) G_3''(s(z0), z1) -> c61(G_3''(z0, z1)) G_4''(s(z0), z1) -> c63(F_3''(z1)) G_3''(s(z0), z1) -> c60(F_2''(z1)) F_2''(z0) -> c56(G_2''(z0, z0)) F_6''(z0) -> c68(G_6''(z0, z0)) G_7''(s(z0), z1) -> c72(F_6''(z1)) G_7''(s(z0), z1) -> c73(G_7''(z0, z1)) F_5''(z0) -> c65(G_5''(z0, z0)) G_6''(s(z0), z1) -> c70(G_6''(z0, z1)) G_8''(s(z0), z1) -> c75(F_7''(z1)) G_6''(s(z0), z1) -> c69(F_5''(z1)) G_1''(s(z0), z1) -> c55(G_1''(z0, z1)) G_4''(s(z0), z1) -> c64(G_4''(z0, z1)) G_8''(s(z0), z1) -> c76(G_8''(z0, z1)) Defined Rule Symbols:none Defined Pair Symbols: F_1'_1, F_2'_1, G_2'_2, F_3'_1, G_3'_2, F_4'_1, G_4'_2, F_5'_1, G_5'_2, F_6'_1, G_6'_2, F_7'_1, G_7'_2, F_8'_1, G_8'_2, F_9'_1, G_9'_2, G_10'_2, F_1''_1, G_1''_2, F_2''_1, G_2''_2, F_3''_1, G_3''_2, F_4''_1, G_4''_2, F_5''_1, G_5''_2, F_6''_1, G_6''_2, F_7''_1, G_7''_2, F_8''_1, G_8''_2, F_9''_1, G_9''_2, G_10''_2, G_1'_2 Compound Symbols: c32_1, c34_1, c35_2, c36_1, c37_2, c38_1, c39_2, c40_1, c41_2, c42_1, c43_2, c44_1, c45_2, c46_1, c47_2, c48_1, c49_2, c51_2, c53_1, c55_1, c56_1, c57_1, c58_1, c59_1, c60_1, c61_1, c62_1, c63_1, c64_1, c65_1, c66_1, c67_1, c68_1, c69_1, c70_1, c71_1, c72_1, c73_1, c74_1, c75_1, c76_1, c77_1, c78_1, c79_1, c81_1, c82_1, c33_1 ---------------------------------------- (41) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (42) BOUNDS(1, 1) ---------------------------------------- (43) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (44) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: F_0(z0) -> c F_1(z0) -> c1(G_1(z0, z0)) G_1(s(z0), z1) -> c2(F_0(z1)) G_1(s(z0), z1) -> c3(G_1(z0, z1)) F_2(z0) -> c4(G_2(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_3(z0) -> c7(G_3(z0, z0)) G_3(s(z0), z1) -> c8(F_2(z1)) G_3(s(z0), z1) -> c9(G_3(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) F_5(z0) -> c13(G_5(z0, z0)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) F_10(z0) -> c28(G_10(z0, z0)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(z0, z1)) The (relative) TRS S consists of the following rules: f_0(z0) -> a f_1(z0) -> g_1(z0, z0) g_1(s(z0), z1) -> b(f_0(z1), g_1(z0, z1)) f_2(z0) -> g_2(z0, z0) g_2(s(z0), z1) -> b(f_1(z1), g_2(z0, z1)) f_3(z0) -> g_3(z0, z0) g_3(s(z0), z1) -> b(f_2(z1), g_3(z0, z1)) f_4(z0) -> g_4(z0, z0) g_4(s(z0), z1) -> b(f_3(z1), g_4(z0, z1)) f_5(z0) -> g_5(z0, z0) g_5(s(z0), z1) -> b(f_4(z1), g_5(z0, z1)) f_6(z0) -> g_6(z0, z0) g_6(s(z0), z1) -> b(f_5(z1), g_6(z0, z1)) f_7(z0) -> g_7(z0, z0) g_7(s(z0), z1) -> b(f_6(z1), g_7(z0, z1)) f_8(z0) -> g_8(z0, z0) g_8(s(z0), z1) -> b(f_7(z1), g_8(z0, z1)) f_9(z0) -> g_9(z0, z0) g_9(s(z0), z1) -> b(f_8(z1), g_9(z0, z1)) f_10(z0) -> g_10(z0, z0) g_10(s(z0), z1) -> b(f_9(z1), g_10(z0, z1)) Rewrite Strategy: INNERMOST ---------------------------------------- (45) DecreasingLoopProof (LOWER BOUND(ID)) The following loop(s) give(s) rise to the lower bound Omega(n^1): The rewrite sequence G_5(s(z0), z1) ->^+ c15(G_5(z0, z1)) gives rise to a decreasing loop by considering the right hand sides subterm at position [0]. The pumping substitution is [z0 / s(z0)]. The result substitution is [ ]. ---------------------------------------- (46) Complex Obligation (BEST) ---------------------------------------- (47) Obligation: Proved the lower bound n^1 for the following obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: F_0(z0) -> c F_1(z0) -> c1(G_1(z0, z0)) G_1(s(z0), z1) -> c2(F_0(z1)) G_1(s(z0), z1) -> c3(G_1(z0, z1)) F_2(z0) -> c4(G_2(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_3(z0) -> c7(G_3(z0, z0)) G_3(s(z0), z1) -> c8(F_2(z1)) G_3(s(z0), z1) -> c9(G_3(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) F_5(z0) -> c13(G_5(z0, z0)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) F_10(z0) -> c28(G_10(z0, z0)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(z0, z1)) The (relative) TRS S consists of the following rules: f_0(z0) -> a f_1(z0) -> g_1(z0, z0) g_1(s(z0), z1) -> b(f_0(z1), g_1(z0, z1)) f_2(z0) -> g_2(z0, z0) g_2(s(z0), z1) -> b(f_1(z1), g_2(z0, z1)) f_3(z0) -> g_3(z0, z0) g_3(s(z0), z1) -> b(f_2(z1), g_3(z0, z1)) f_4(z0) -> g_4(z0, z0) g_4(s(z0), z1) -> b(f_3(z1), g_4(z0, z1)) f_5(z0) -> g_5(z0, z0) g_5(s(z0), z1) -> b(f_4(z1), g_5(z0, z1)) f_6(z0) -> g_6(z0, z0) g_6(s(z0), z1) -> b(f_5(z1), g_6(z0, z1)) f_7(z0) -> g_7(z0, z0) g_7(s(z0), z1) -> b(f_6(z1), g_7(z0, z1)) f_8(z0) -> g_8(z0, z0) g_8(s(z0), z1) -> b(f_7(z1), g_8(z0, z1)) f_9(z0) -> g_9(z0, z0) g_9(s(z0), z1) -> b(f_8(z1), g_9(z0, z1)) f_10(z0) -> g_10(z0, z0) g_10(s(z0), z1) -> b(f_9(z1), g_10(z0, z1)) Rewrite Strategy: INNERMOST ---------------------------------------- (48) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (49) BOUNDS(n^1, INF) ---------------------------------------- (50) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: F_0(z0) -> c F_1(z0) -> c1(G_1(z0, z0)) G_1(s(z0), z1) -> c2(F_0(z1)) G_1(s(z0), z1) -> c3(G_1(z0, z1)) F_2(z0) -> c4(G_2(z0, z0)) G_2(s(z0), z1) -> c5(F_1(z1)) G_2(s(z0), z1) -> c6(G_2(z0, z1)) F_3(z0) -> c7(G_3(z0, z0)) G_3(s(z0), z1) -> c8(F_2(z1)) G_3(s(z0), z1) -> c9(G_3(z0, z1)) F_4(z0) -> c10(G_4(z0, z0)) G_4(s(z0), z1) -> c11(F_3(z1)) G_4(s(z0), z1) -> c12(G_4(z0, z1)) F_5(z0) -> c13(G_5(z0, z0)) G_5(s(z0), z1) -> c14(F_4(z1)) G_5(s(z0), z1) -> c15(G_5(z0, z1)) F_6(z0) -> c16(G_6(z0, z0)) G_6(s(z0), z1) -> c17(F_5(z1)) G_6(s(z0), z1) -> c18(G_6(z0, z1)) F_7(z0) -> c19(G_7(z0, z0)) G_7(s(z0), z1) -> c20(F_6(z1)) G_7(s(z0), z1) -> c21(G_7(z0, z1)) F_8(z0) -> c22(G_8(z0, z0)) G_8(s(z0), z1) -> c23(F_7(z1)) G_8(s(z0), z1) -> c24(G_8(z0, z1)) F_9(z0) -> c25(G_9(z0, z0)) G_9(s(z0), z1) -> c26(F_8(z1)) G_9(s(z0), z1) -> c27(G_9(z0, z1)) F_10(z0) -> c28(G_10(z0, z0)) G_10(s(z0), z1) -> c29(F_9(z1)) G_10(s(z0), z1) -> c30(G_10(z0, z1)) The (relative) TRS S consists of the following rules: f_0(z0) -> a f_1(z0) -> g_1(z0, z0) g_1(s(z0), z1) -> b(f_0(z1), g_1(z0, z1)) f_2(z0) -> g_2(z0, z0) g_2(s(z0), z1) -> b(f_1(z1), g_2(z0, z1)) f_3(z0) -> g_3(z0, z0) g_3(s(z0), z1) -> b(f_2(z1), g_3(z0, z1)) f_4(z0) -> g_4(z0, z0) g_4(s(z0), z1) -> b(f_3(z1), g_4(z0, z1)) f_5(z0) -> g_5(z0, z0) g_5(s(z0), z1) -> b(f_4(z1), g_5(z0, z1)) f_6(z0) -> g_6(z0, z0) g_6(s(z0), z1) -> b(f_5(z1), g_6(z0, z1)) f_7(z0) -> g_7(z0, z0) g_7(s(z0), z1) -> b(f_6(z1), g_7(z0, z1)) f_8(z0) -> g_8(z0, z0) g_8(s(z0), z1) -> b(f_7(z1), g_8(z0, z1)) f_9(z0) -> g_9(z0, z0) g_9(s(z0), z1) -> b(f_8(z1), g_9(z0, z1)) f_10(z0) -> g_10(z0, z0) g_10(s(z0), z1) -> b(f_9(z1), g_10(z0, z1)) Rewrite Strategy: INNERMOST