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), 1009 ms] (2) CpxRelTRS (3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (4) CdtProblem (5) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 1 ms] (6) CdtProblem (7) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CdtProblem (9) CdtGraphSplitRhsProof [BOTH BOUNDS(ID, ID), 0 ms] (10) CdtProblem (11) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms] (12) CdtProblem (13) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (14) CdtProblem (15) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 131 ms] (16) CdtProblem (17) CdtKnowledgeProof [FINISHED, 0 ms] (18) BOUNDS(1, 1) (19) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (20) TRS for Loop Detection (21) DecreasingLoopProof [LOWER BOUND(ID), 46 ms] (22) BEST (23) proven lower bound (24) LowerBoundPropagationProof [FINISHED, 0 ms] (25) BOUNDS(n^1, INF) (26) 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: *'(z0, z1) -> c24(#MULT(z0, z1)) DYADE(z0, z1) -> c25(DYADE#1(z0, z1)) DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2)) DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2)) DYADE#1(nil, z0) -> c28 MULT(z0, z1) -> c29(MULT#1(z1, z0)) MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0)) MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1)) MULT#1(nil, z0) -> c32 The (relative) TRS S consists of the following rules: #ADD(#0, z0) -> c #ADD(#neg(#s(#0)), z0) -> c1(#PRED(z0)) #ADD(#neg(#s(#s(z0))), z1) -> c2(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #ADD(#pos(#s(#0)), z0) -> c3(#SUCC(z0)) #ADD(#pos(#s(#s(z0))), z1) -> c4(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #MULT(#0, #0) -> c5 #MULT(#0, #neg(z0)) -> c6 #MULT(#0, #pos(z0)) -> c7 #MULT(#neg(z0), #0) -> c8 #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1)) #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1)) #MULT(#pos(z0), #0) -> c11 #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1)) #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1)) #NATMULT(#0, z0) -> c14 #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) #PRED(#0) -> c16 #PRED(#neg(#s(z0))) -> c17 #PRED(#pos(#s(#0))) -> c18 #PRED(#pos(#s(#s(z0)))) -> c19 #SUCC(#0) -> c20 #SUCC(#neg(#s(#0))) -> c21 #SUCC(#neg(#s(#s(z0)))) -> c22 #SUCC(#pos(#s(z0))) -> c23 #add(#0, z0) -> z0 #add(#neg(#s(#0)), z0) -> #pred(z0) #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1)) #add(#pos(#s(#0)), z0) -> #succ(z0) #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1)) #mult(#0, #0) -> #0 #mult(#0, #neg(z0)) -> #0 #mult(#0, #pos(z0)) -> #0 #mult(#neg(z0), #0) -> #0 #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1)) #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #0) -> #0 #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1)) #natmult(#0, z0) -> #0 #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1)) #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(z0))) -> #neg(#s(#s(z0))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0)) #succ(#pos(#s(z0))) -> #pos(#s(#s(z0))) *(z0, z1) -> #mult(z0, z1) dyade(z0, z1) -> dyade#1(z0, z1) dyade#1(::(z0, z1), z2) -> ::(mult(z0, z2), dyade(z1, z2)) dyade#1(nil, z0) -> nil mult(z0, z1) -> mult#1(z1, z0) mult#1(::(z0, z1), z2) -> ::(*(z2, z0), mult(z2, z1)) mult#1(nil, z0) -> nil 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: *'(z0, z1) -> c24(#MULT(z0, z1)) DYADE(z0, z1) -> c25(DYADE#1(z0, z1)) DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2)) DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2)) DYADE#1(nil, z0) -> c28 MULT(z0, z1) -> c29(MULT#1(z1, z0)) MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0)) MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1)) MULT#1(nil, z0) -> c32 The (relative) TRS S consists of the following rules: #ADD(#0, z0) -> c #ADD(#neg(#s(#0)), z0) -> c1(#PRED(z0)) #ADD(#neg(#s(#s(z0))), z1) -> c2(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #ADD(#pos(#s(#0)), z0) -> c3(#SUCC(z0)) #ADD(#pos(#s(#s(z0))), z1) -> c4(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #MULT(#0, #0) -> c5 #MULT(#0, #neg(z0)) -> c6 #MULT(#0, #pos(z0)) -> c7 #MULT(#neg(z0), #0) -> c8 #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1)) #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1)) #MULT(#pos(z0), #0) -> c11 #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1)) #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1)) #NATMULT(#0, z0) -> c14 #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) #PRED(#0) -> c16 #PRED(#neg(#s(z0))) -> c17 #PRED(#pos(#s(#0))) -> c18 #PRED(#pos(#s(#s(z0)))) -> c19 #SUCC(#0) -> c20 #SUCC(#neg(#s(#0))) -> c21 #SUCC(#neg(#s(#s(z0)))) -> c22 #SUCC(#pos(#s(z0))) -> c23 #add(#0, z0) -> z0 #add(#neg(#s(#0)), z0) -> #pred(z0) #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1)) #add(#pos(#s(#0)), z0) -> #succ(z0) #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1)) #mult(#0, #0) -> #0 #mult(#0, #neg(z0)) -> #0 #mult(#0, #pos(z0)) -> #0 #mult(#neg(z0), #0) -> #0 #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1)) #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #0) -> #0 #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1)) #natmult(#0, z0) -> #0 #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1)) #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(z0))) -> #neg(#s(#s(z0))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0)) #succ(#pos(#s(z0))) -> #pos(#s(#s(z0))) *(z0, z1) -> #mult(z0, z1) dyade(z0, z1) -> dyade#1(z0, z1) dyade#1(::(z0, z1), z2) -> ::(mult(z0, z2), dyade(z1, z2)) dyade#1(nil, z0) -> nil mult(z0, z1) -> mult#1(z1, z0) mult#1(::(z0, z1), z2) -> ::(*(z2, z0), mult(z2, z1)) mult#1(nil, z0) -> nil Rewrite Strategy: INNERMOST ---------------------------------------- (3) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS to CDT ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: #ADD(#0, z0) -> c #ADD(#neg(#s(#0)), z0) -> c1(#PRED(z0)) #ADD(#neg(#s(#s(z0))), z1) -> c2(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #ADD(#pos(#s(#0)), z0) -> c3(#SUCC(z0)) #ADD(#pos(#s(#s(z0))), z1) -> c4(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #MULT(#0, #0) -> c5 #MULT(#0, #neg(z0)) -> c6 #MULT(#0, #pos(z0)) -> c7 #MULT(#neg(z0), #0) -> c8 #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1)) #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1)) #MULT(#pos(z0), #0) -> c11 #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1)) #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1)) #NATMULT(#0, z0) -> c14 #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) #PRED(#0) -> c16 #PRED(#neg(#s(z0))) -> c17 #PRED(#pos(#s(#0))) -> c18 #PRED(#pos(#s(#s(z0)))) -> c19 #SUCC(#0) -> c20 #SUCC(#neg(#s(#0))) -> c21 #SUCC(#neg(#s(#s(z0)))) -> c22 #SUCC(#pos(#s(z0))) -> c23 #add(#0, z0) -> z0 #add(#neg(#s(#0)), z0) -> #pred(z0) #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1)) #add(#pos(#s(#0)), z0) -> #succ(z0) #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1)) #mult(#0, #0) -> #0 #mult(#0, #neg(z0)) -> #0 #mult(#0, #pos(z0)) -> #0 #mult(#neg(z0), #0) -> #0 #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1)) #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #0) -> #0 #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1)) #natmult(#0, z0) -> #0 #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1)) #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(z0))) -> #neg(#s(#s(z0))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0)) #succ(#pos(#s(z0))) -> #pos(#s(#s(z0))) *(z0, z1) -> #mult(z0, z1) dyade(z0, z1) -> dyade#1(z0, z1) dyade#1(::(z0, z1), z2) -> ::(mult(z0, z2), dyade(z1, z2)) dyade#1(nil, z0) -> nil mult(z0, z1) -> mult#1(z1, z0) mult#1(::(z0, z1), z2) -> ::(*(z2, z0), mult(z2, z1)) mult#1(nil, z0) -> nil *'(z0, z1) -> c24(#MULT(z0, z1)) DYADE(z0, z1) -> c25(DYADE#1(z0, z1)) DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2)) DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2)) DYADE#1(nil, z0) -> c28 MULT(z0, z1) -> c29(MULT#1(z1, z0)) MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0)) MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1)) MULT#1(nil, z0) -> c32 Tuples: #ADD'(#0, z0) -> c33 #ADD'(#neg(#s(#0)), z0) -> c34(#PRED'(z0)) #ADD'(#neg(#s(#s(z0))), z1) -> c35(#PRED'(#add(#pos(#s(z0)), z1)), #ADD''(#pos(#s(z0)), z1), #ADD'(#pos(#s(z0)), z1)) #ADD'(#pos(#s(#0)), z0) -> c36(#SUCC'(z0)) #ADD'(#pos(#s(#s(z0))), z1) -> c37(#SUCC'(#add(#pos(#s(z0)), z1)), #ADD''(#pos(#s(z0)), z1), #ADD'(#pos(#s(z0)), z1)) #MULT'(#0, #0) -> c38 #MULT'(#0, #neg(z0)) -> c39 #MULT'(#0, #pos(z0)) -> c40 #MULT'(#neg(z0), #0) -> c41 #MULT'(#neg(z0), #neg(z1)) -> c42(#NATMULT'(z0, z1)) #MULT'(#neg(z0), #pos(z1)) -> c43(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #0) -> c44 #MULT'(#pos(z0), #neg(z1)) -> c45(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #pos(z1)) -> c46(#NATMULT'(z0, z1)) #NATMULT'(#0, z0) -> c47 #NATMULT'(#s(z0), z1) -> c48(#ADD'(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1), #NATMULT'(z0, z1)) #PRED'(#0) -> c49 #PRED'(#neg(#s(z0))) -> c50 #PRED'(#pos(#s(#0))) -> c51 #PRED'(#pos(#s(#s(z0)))) -> c52 #SUCC'(#0) -> c53 #SUCC'(#neg(#s(#0))) -> c54 #SUCC'(#neg(#s(#s(z0)))) -> c55 #SUCC'(#pos(#s(z0))) -> c56 #ADD''(#0, z0) -> c57 #ADD''(#neg(#s(#0)), z0) -> c58(#PRED''(z0)) #ADD''(#neg(#s(#s(z0))), z1) -> c59(#PRED''(#add(#pos(#s(z0)), z1)), #ADD''(#pos(#s(z0)), z1)) #ADD''(#pos(#s(#0)), z0) -> c60(#SUCC''(z0)) #ADD''(#pos(#s(#s(z0))), z1) -> c61(#SUCC''(#add(#pos(#s(z0)), z1)), #ADD''(#pos(#s(z0)), z1)) #MULT''(#0, #0) -> c62 #MULT''(#0, #neg(z0)) -> c63 #MULT''(#0, #pos(z0)) -> c64 #MULT''(#neg(z0), #0) -> c65 #MULT''(#neg(z0), #neg(z1)) -> c66(#NATMULT''(z0, z1)) #MULT''(#neg(z0), #pos(z1)) -> c67(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #0) -> c68 #MULT''(#pos(z0), #neg(z1)) -> c69(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #pos(z1)) -> c70(#NATMULT''(z0, z1)) #NATMULT''(#0, z0) -> c71 #NATMULT''(#s(z0), z1) -> c72(#ADD''(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1)) #PRED''(#0) -> c73 #PRED''(#neg(#s(z0))) -> c74 #PRED''(#pos(#s(#0))) -> c75 #PRED''(#pos(#s(#s(z0)))) -> c76 #SUCC''(#0) -> c77 #SUCC''(#neg(#s(#0))) -> c78 #SUCC''(#neg(#s(#s(z0)))) -> c79 #SUCC''(#pos(#s(z0))) -> c80 *''(z0, z1) -> c81(#MULT''(z0, z1)) DYADE'(z0, z1) -> c82(DYADE#1'(z0, z1)) DYADE#1'(::(z0, z1), z2) -> c83(MULT'(z0, z2), DYADE'(z1, z2)) DYADE#1'(nil, z0) -> c84 MULT'(z0, z1) -> c85(MULT#1'(z1, z0)) MULT#1'(::(z0, z1), z2) -> c86(*''(z2, z0), MULT'(z2, z1)) MULT#1'(nil, z0) -> c87 *'''(z0, z1) -> c88(#MULT'(z0, z1)) DYADE''(z0, z1) -> c89(DYADE#1''(z0, z1)) DYADE#1''(::(z0, z1), z2) -> c90(MULT''(z0, z2)) DYADE#1''(::(z0, z1), z2) -> c91(DYADE''(z1, z2)) DYADE#1''(nil, z0) -> c92 MULT''(z0, z1) -> c93(MULT#1''(z1, z0)) MULT#1''(::(z0, z1), z2) -> c94(*'''(z2, z0)) MULT#1''(::(z0, z1), z2) -> c95(MULT''(z2, z1)) MULT#1''(nil, z0) -> c96 S tuples: *'''(z0, z1) -> c88(#MULT'(z0, z1)) DYADE''(z0, z1) -> c89(DYADE#1''(z0, z1)) DYADE#1''(::(z0, z1), z2) -> c90(MULT''(z0, z2)) DYADE#1''(::(z0, z1), z2) -> c91(DYADE''(z1, z2)) DYADE#1''(nil, z0) -> c92 MULT''(z0, z1) -> c93(MULT#1''(z1, z0)) MULT#1''(::(z0, z1), z2) -> c94(*'''(z2, z0)) MULT#1''(::(z0, z1), z2) -> c95(MULT''(z2, z1)) MULT#1''(nil, z0) -> c96 K tuples:none Defined Rule Symbols: *'_2, DYADE_2, DYADE#1_2, MULT_2, MULT#1_2, #ADD_2, #MULT_2, #NATMULT_2, #PRED_1, #SUCC_1, #add_2, #mult_2, #natmult_2, #pred_1, #succ_1, *_2, dyade_2, dyade#1_2, mult_2, mult#1_2 Defined Pair Symbols: #ADD'_2, #MULT'_2, #NATMULT'_2, #PRED'_1, #SUCC'_1, #ADD''_2, #MULT''_2, #NATMULT''_2, #PRED''_1, #SUCC''_1, *''_2, DYADE'_2, DYADE#1'_2, MULT'_2, MULT#1'_2, *'''_2, DYADE''_2, DYADE#1''_2, MULT''_2, MULT#1''_2 Compound Symbols: c33, c34_1, c35_3, c36_1, c37_3, c38, c39, c40, c41, c42_1, c43_1, c44, c45_1, c46_1, c47, c48_3, c49, c50, c51, c52, c53, c54, c55, c56, c57, c58_1, c59_2, c60_1, c61_2, c62, c63, c64, c65, c66_1, c67_1, c68, c69_1, c70_1, c71, c72_2, c73, c74, c75, c76, c77, c78, c79, c80, c81_1, c82_1, c83_2, c84, c85_1, c86_2, c87, c88_1, c89_1, c90_1, c91_1, c92, c93_1, c94_1, c95_1, c96 ---------------------------------------- (5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 38 trailing nodes: #PRED'(#0) -> c49 #MULT'(#0, #neg(z0)) -> c39 #MULT''(#0, #neg(z0)) -> c63 #PRED''(#pos(#s(#0))) -> c75 #NATMULT'(#0, z0) -> c47 #ADD''(#0, z0) -> c57 DYADE#1''(nil, z0) -> c92 #PRED''(#pos(#s(#s(z0)))) -> c76 #SUCC'(#0) -> c53 #MULT'(#0, #0) -> c38 #PRED''(#neg(#s(z0))) -> c74 #ADD''(#neg(#s(#0)), z0) -> c58(#PRED''(z0)) #SUCC''(#pos(#s(z0))) -> c80 #NATMULT''(#0, z0) -> c71 #SUCC'(#neg(#s(#s(z0)))) -> c55 MULT#1'(nil, z0) -> c87 #MULT'(#pos(z0), #0) -> c44 #MULT''(#0, #pos(z0)) -> c64 #SUCC''(#0) -> c77 #SUCC''(#neg(#s(#s(z0)))) -> c79 #ADD'(#neg(#s(#0)), z0) -> c34(#PRED'(z0)) #ADD''(#pos(#s(#0)), z0) -> c60(#SUCC''(z0)) #SUCC'(#neg(#s(#0))) -> c54 #MULT''(#neg(z0), #0) -> c65 #PRED''(#0) -> c73 #PRED'(#neg(#s(z0))) -> c50 #MULT''(#pos(z0), #0) -> c68 #ADD'(#pos(#s(#0)), z0) -> c36(#SUCC'(z0)) #PRED'(#pos(#s(#s(z0)))) -> c52 MULT#1''(nil, z0) -> c96 #MULT''(#0, #0) -> c62 #SUCC'(#pos(#s(z0))) -> c56 #MULT'(#0, #pos(z0)) -> c40 #MULT'(#neg(z0), #0) -> c41 #ADD'(#0, z0) -> c33 #PRED'(#pos(#s(#0))) -> c51 DYADE#1'(nil, z0) -> c84 #SUCC''(#neg(#s(#0))) -> c78 ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: #ADD(#0, z0) -> c #ADD(#neg(#s(#0)), z0) -> c1(#PRED(z0)) #ADD(#neg(#s(#s(z0))), z1) -> c2(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #ADD(#pos(#s(#0)), z0) -> c3(#SUCC(z0)) #ADD(#pos(#s(#s(z0))), z1) -> c4(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #MULT(#0, #0) -> c5 #MULT(#0, #neg(z0)) -> c6 #MULT(#0, #pos(z0)) -> c7 #MULT(#neg(z0), #0) -> c8 #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1)) #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1)) #MULT(#pos(z0), #0) -> c11 #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1)) #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1)) #NATMULT(#0, z0) -> c14 #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) #PRED(#0) -> c16 #PRED(#neg(#s(z0))) -> c17 #PRED(#pos(#s(#0))) -> c18 #PRED(#pos(#s(#s(z0)))) -> c19 #SUCC(#0) -> c20 #SUCC(#neg(#s(#0))) -> c21 #SUCC(#neg(#s(#s(z0)))) -> c22 #SUCC(#pos(#s(z0))) -> c23 #add(#0, z0) -> z0 #add(#neg(#s(#0)), z0) -> #pred(z0) #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1)) #add(#pos(#s(#0)), z0) -> #succ(z0) #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1)) #mult(#0, #0) -> #0 #mult(#0, #neg(z0)) -> #0 #mult(#0, #pos(z0)) -> #0 #mult(#neg(z0), #0) -> #0 #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1)) #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #0) -> #0 #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1)) #natmult(#0, z0) -> #0 #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1)) #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(z0))) -> #neg(#s(#s(z0))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0)) #succ(#pos(#s(z0))) -> #pos(#s(#s(z0))) *(z0, z1) -> #mult(z0, z1) dyade(z0, z1) -> dyade#1(z0, z1) dyade#1(::(z0, z1), z2) -> ::(mult(z0, z2), dyade(z1, z2)) dyade#1(nil, z0) -> nil mult(z0, z1) -> mult#1(z1, z0) mult#1(::(z0, z1), z2) -> ::(*(z2, z0), mult(z2, z1)) mult#1(nil, z0) -> nil *'(z0, z1) -> c24(#MULT(z0, z1)) DYADE(z0, z1) -> c25(DYADE#1(z0, z1)) DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2)) DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2)) DYADE#1(nil, z0) -> c28 MULT(z0, z1) -> c29(MULT#1(z1, z0)) MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0)) MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1)) MULT#1(nil, z0) -> c32 Tuples: #ADD'(#neg(#s(#s(z0))), z1) -> c35(#PRED'(#add(#pos(#s(z0)), z1)), #ADD''(#pos(#s(z0)), z1), #ADD'(#pos(#s(z0)), z1)) #ADD'(#pos(#s(#s(z0))), z1) -> c37(#SUCC'(#add(#pos(#s(z0)), z1)), #ADD''(#pos(#s(z0)), z1), #ADD'(#pos(#s(z0)), z1)) #MULT'(#neg(z0), #neg(z1)) -> c42(#NATMULT'(z0, z1)) #MULT'(#neg(z0), #pos(z1)) -> c43(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #neg(z1)) -> c45(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #pos(z1)) -> c46(#NATMULT'(z0, z1)) #NATMULT'(#s(z0), z1) -> c48(#ADD'(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1), #NATMULT'(z0, z1)) #ADD''(#neg(#s(#s(z0))), z1) -> c59(#PRED''(#add(#pos(#s(z0)), z1)), #ADD''(#pos(#s(z0)), z1)) #ADD''(#pos(#s(#s(z0))), z1) -> c61(#SUCC''(#add(#pos(#s(z0)), z1)), #ADD''(#pos(#s(z0)), z1)) #MULT''(#neg(z0), #neg(z1)) -> c66(#NATMULT''(z0, z1)) #MULT''(#neg(z0), #pos(z1)) -> c67(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #neg(z1)) -> c69(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #pos(z1)) -> c70(#NATMULT''(z0, z1)) #NATMULT''(#s(z0), z1) -> c72(#ADD''(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1)) *''(z0, z1) -> c81(#MULT''(z0, z1)) DYADE'(z0, z1) -> c82(DYADE#1'(z0, z1)) DYADE#1'(::(z0, z1), z2) -> c83(MULT'(z0, z2), DYADE'(z1, z2)) MULT'(z0, z1) -> c85(MULT#1'(z1, z0)) MULT#1'(::(z0, z1), z2) -> c86(*''(z2, z0), MULT'(z2, z1)) *'''(z0, z1) -> c88(#MULT'(z0, z1)) DYADE''(z0, z1) -> c89(DYADE#1''(z0, z1)) DYADE#1''(::(z0, z1), z2) -> c90(MULT''(z0, z2)) DYADE#1''(::(z0, z1), z2) -> c91(DYADE''(z1, z2)) MULT''(z0, z1) -> c93(MULT#1''(z1, z0)) MULT#1''(::(z0, z1), z2) -> c94(*'''(z2, z0)) MULT#1''(::(z0, z1), z2) -> c95(MULT''(z2, z1)) S tuples: *'''(z0, z1) -> c88(#MULT'(z0, z1)) DYADE''(z0, z1) -> c89(DYADE#1''(z0, z1)) DYADE#1''(::(z0, z1), z2) -> c90(MULT''(z0, z2)) DYADE#1''(::(z0, z1), z2) -> c91(DYADE''(z1, z2)) MULT''(z0, z1) -> c93(MULT#1''(z1, z0)) MULT#1''(::(z0, z1), z2) -> c94(*'''(z2, z0)) MULT#1''(::(z0, z1), z2) -> c95(MULT''(z2, z1)) K tuples:none Defined Rule Symbols: *'_2, DYADE_2, DYADE#1_2, MULT_2, MULT#1_2, #ADD_2, #MULT_2, #NATMULT_2, #PRED_1, #SUCC_1, #add_2, #mult_2, #natmult_2, #pred_1, #succ_1, *_2, dyade_2, dyade#1_2, mult_2, mult#1_2 Defined Pair Symbols: #ADD'_2, #MULT'_2, #NATMULT'_2, #ADD''_2, #MULT''_2, #NATMULT''_2, *''_2, DYADE'_2, DYADE#1'_2, MULT'_2, MULT#1'_2, *'''_2, DYADE''_2, DYADE#1''_2, MULT''_2, MULT#1''_2 Compound Symbols: c35_3, c37_3, c42_1, c43_1, c45_1, c46_1, c48_3, c59_2, c61_2, c66_1, c67_1, c69_1, c70_1, c72_2, c81_1, c82_1, c83_2, c85_1, c86_2, c88_1, c89_1, c90_1, c91_1, c93_1, c94_1, c95_1 ---------------------------------------- (7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 4 trailing tuple parts ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules: #ADD(#0, z0) -> c #ADD(#neg(#s(#0)), z0) -> c1(#PRED(z0)) #ADD(#neg(#s(#s(z0))), z1) -> c2(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #ADD(#pos(#s(#0)), z0) -> c3(#SUCC(z0)) #ADD(#pos(#s(#s(z0))), z1) -> c4(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #MULT(#0, #0) -> c5 #MULT(#0, #neg(z0)) -> c6 #MULT(#0, #pos(z0)) -> c7 #MULT(#neg(z0), #0) -> c8 #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1)) #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1)) #MULT(#pos(z0), #0) -> c11 #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1)) #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1)) #NATMULT(#0, z0) -> c14 #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) #PRED(#0) -> c16 #PRED(#neg(#s(z0))) -> c17 #PRED(#pos(#s(#0))) -> c18 #PRED(#pos(#s(#s(z0)))) -> c19 #SUCC(#0) -> c20 #SUCC(#neg(#s(#0))) -> c21 #SUCC(#neg(#s(#s(z0)))) -> c22 #SUCC(#pos(#s(z0))) -> c23 #add(#0, z0) -> z0 #add(#neg(#s(#0)), z0) -> #pred(z0) #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1)) #add(#pos(#s(#0)), z0) -> #succ(z0) #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1)) #mult(#0, #0) -> #0 #mult(#0, #neg(z0)) -> #0 #mult(#0, #pos(z0)) -> #0 #mult(#neg(z0), #0) -> #0 #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1)) #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #0) -> #0 #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1)) #natmult(#0, z0) -> #0 #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1)) #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(z0))) -> #neg(#s(#s(z0))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0)) #succ(#pos(#s(z0))) -> #pos(#s(#s(z0))) *(z0, z1) -> #mult(z0, z1) dyade(z0, z1) -> dyade#1(z0, z1) dyade#1(::(z0, z1), z2) -> ::(mult(z0, z2), dyade(z1, z2)) dyade#1(nil, z0) -> nil mult(z0, z1) -> mult#1(z1, z0) mult#1(::(z0, z1), z2) -> ::(*(z2, z0), mult(z2, z1)) mult#1(nil, z0) -> nil *'(z0, z1) -> c24(#MULT(z0, z1)) DYADE(z0, z1) -> c25(DYADE#1(z0, z1)) DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2)) DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2)) DYADE#1(nil, z0) -> c28 MULT(z0, z1) -> c29(MULT#1(z1, z0)) MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0)) MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1)) MULT#1(nil, z0) -> c32 Tuples: #MULT'(#neg(z0), #neg(z1)) -> c42(#NATMULT'(z0, z1)) #MULT'(#neg(z0), #pos(z1)) -> c43(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #neg(z1)) -> c45(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #pos(z1)) -> c46(#NATMULT'(z0, z1)) #NATMULT'(#s(z0), z1) -> c48(#ADD'(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1), #NATMULT'(z0, z1)) #MULT''(#neg(z0), #neg(z1)) -> c66(#NATMULT''(z0, z1)) #MULT''(#neg(z0), #pos(z1)) -> c67(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #neg(z1)) -> c69(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #pos(z1)) -> c70(#NATMULT''(z0, z1)) #NATMULT''(#s(z0), z1) -> c72(#ADD''(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1)) *''(z0, z1) -> c81(#MULT''(z0, z1)) DYADE'(z0, z1) -> c82(DYADE#1'(z0, z1)) DYADE#1'(::(z0, z1), z2) -> c83(MULT'(z0, z2), DYADE'(z1, z2)) MULT'(z0, z1) -> c85(MULT#1'(z1, z0)) MULT#1'(::(z0, z1), z2) -> c86(*''(z2, z0), MULT'(z2, z1)) *'''(z0, z1) -> c88(#MULT'(z0, z1)) DYADE''(z0, z1) -> c89(DYADE#1''(z0, z1)) DYADE#1''(::(z0, z1), z2) -> c90(MULT''(z0, z2)) DYADE#1''(::(z0, z1), z2) -> c91(DYADE''(z1, z2)) MULT''(z0, z1) -> c93(MULT#1''(z1, z0)) MULT#1''(::(z0, z1), z2) -> c94(*'''(z2, z0)) MULT#1''(::(z0, z1), z2) -> c95(MULT''(z2, z1)) #ADD'(#neg(#s(#s(z0))), z1) -> c35(#ADD''(#pos(#s(z0)), z1), #ADD'(#pos(#s(z0)), z1)) #ADD'(#pos(#s(#s(z0))), z1) -> c37(#ADD''(#pos(#s(z0)), z1), #ADD'(#pos(#s(z0)), z1)) #ADD''(#neg(#s(#s(z0))), z1) -> c59(#ADD''(#pos(#s(z0)), z1)) #ADD''(#pos(#s(#s(z0))), z1) -> c61(#ADD''(#pos(#s(z0)), z1)) S tuples: *'''(z0, z1) -> c88(#MULT'(z0, z1)) DYADE''(z0, z1) -> c89(DYADE#1''(z0, z1)) DYADE#1''(::(z0, z1), z2) -> c90(MULT''(z0, z2)) DYADE#1''(::(z0, z1), z2) -> c91(DYADE''(z1, z2)) MULT''(z0, z1) -> c93(MULT#1''(z1, z0)) MULT#1''(::(z0, z1), z2) -> c94(*'''(z2, z0)) MULT#1''(::(z0, z1), z2) -> c95(MULT''(z2, z1)) K tuples:none Defined Rule Symbols: *'_2, DYADE_2, DYADE#1_2, MULT_2, MULT#1_2, #ADD_2, #MULT_2, #NATMULT_2, #PRED_1, #SUCC_1, #add_2, #mult_2, #natmult_2, #pred_1, #succ_1, *_2, dyade_2, dyade#1_2, mult_2, mult#1_2 Defined Pair Symbols: #MULT'_2, #NATMULT'_2, #MULT''_2, #NATMULT''_2, *''_2, DYADE'_2, DYADE#1'_2, MULT'_2, MULT#1'_2, *'''_2, DYADE''_2, DYADE#1''_2, MULT''_2, MULT#1''_2, #ADD'_2, #ADD''_2 Compound Symbols: c42_1, c43_1, c45_1, c46_1, c48_3, c66_1, c67_1, c69_1, c70_1, c72_2, c81_1, c82_1, c83_2, c85_1, c86_2, c88_1, c89_1, c90_1, c91_1, c93_1, c94_1, c95_1, c35_2, c37_2, c59_1, c61_1 ---------------------------------------- (9) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID)) Split RHS of tuples not part of any SCC ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules: #ADD(#0, z0) -> c #ADD(#neg(#s(#0)), z0) -> c1(#PRED(z0)) #ADD(#neg(#s(#s(z0))), z1) -> c2(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #ADD(#pos(#s(#0)), z0) -> c3(#SUCC(z0)) #ADD(#pos(#s(#s(z0))), z1) -> c4(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #MULT(#0, #0) -> c5 #MULT(#0, #neg(z0)) -> c6 #MULT(#0, #pos(z0)) -> c7 #MULT(#neg(z0), #0) -> c8 #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1)) #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1)) #MULT(#pos(z0), #0) -> c11 #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1)) #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1)) #NATMULT(#0, z0) -> c14 #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) #PRED(#0) -> c16 #PRED(#neg(#s(z0))) -> c17 #PRED(#pos(#s(#0))) -> c18 #PRED(#pos(#s(#s(z0)))) -> c19 #SUCC(#0) -> c20 #SUCC(#neg(#s(#0))) -> c21 #SUCC(#neg(#s(#s(z0)))) -> c22 #SUCC(#pos(#s(z0))) -> c23 #add(#0, z0) -> z0 #add(#neg(#s(#0)), z0) -> #pred(z0) #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1)) #add(#pos(#s(#0)), z0) -> #succ(z0) #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1)) #mult(#0, #0) -> #0 #mult(#0, #neg(z0)) -> #0 #mult(#0, #pos(z0)) -> #0 #mult(#neg(z0), #0) -> #0 #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1)) #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #0) -> #0 #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1)) #natmult(#0, z0) -> #0 #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1)) #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(z0))) -> #neg(#s(#s(z0))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0)) #succ(#pos(#s(z0))) -> #pos(#s(#s(z0))) *(z0, z1) -> #mult(z0, z1) dyade(z0, z1) -> dyade#1(z0, z1) dyade#1(::(z0, z1), z2) -> ::(mult(z0, z2), dyade(z1, z2)) dyade#1(nil, z0) -> nil mult(z0, z1) -> mult#1(z1, z0) mult#1(::(z0, z1), z2) -> ::(*(z2, z0), mult(z2, z1)) mult#1(nil, z0) -> nil *'(z0, z1) -> c24(#MULT(z0, z1)) DYADE(z0, z1) -> c25(DYADE#1(z0, z1)) DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2)) DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2)) DYADE#1(nil, z0) -> c28 MULT(z0, z1) -> c29(MULT#1(z1, z0)) MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0)) MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1)) MULT#1(nil, z0) -> c32 Tuples: #MULT'(#neg(z0), #neg(z1)) -> c42(#NATMULT'(z0, z1)) #MULT'(#neg(z0), #pos(z1)) -> c43(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #neg(z1)) -> c45(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #pos(z1)) -> c46(#NATMULT'(z0, z1)) #NATMULT'(#s(z0), z1) -> c48(#ADD'(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1), #NATMULT'(z0, z1)) #MULT''(#neg(z0), #neg(z1)) -> c66(#NATMULT''(z0, z1)) #MULT''(#neg(z0), #pos(z1)) -> c67(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #neg(z1)) -> c69(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #pos(z1)) -> c70(#NATMULT''(z0, z1)) #NATMULT''(#s(z0), z1) -> c72(#ADD''(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1)) *''(z0, z1) -> c81(#MULT''(z0, z1)) DYADE'(z0, z1) -> c82(DYADE#1'(z0, z1)) DYADE#1'(::(z0, z1), z2) -> c83(MULT'(z0, z2), DYADE'(z1, z2)) MULT'(z0, z1) -> c85(MULT#1'(z1, z0)) MULT#1'(::(z0, z1), z2) -> c86(*''(z2, z0), MULT'(z2, z1)) *'''(z0, z1) -> c88(#MULT'(z0, z1)) DYADE''(z0, z1) -> c89(DYADE#1''(z0, z1)) DYADE#1''(::(z0, z1), z2) -> c90(MULT''(z0, z2)) DYADE#1''(::(z0, z1), z2) -> c91(DYADE''(z1, z2)) MULT''(z0, z1) -> c93(MULT#1''(z1, z0)) MULT#1''(::(z0, z1), z2) -> c94(*'''(z2, z0)) MULT#1''(::(z0, z1), z2) -> c95(MULT''(z2, z1)) #ADD'(#pos(#s(#s(z0))), z1) -> c37(#ADD''(#pos(#s(z0)), z1), #ADD'(#pos(#s(z0)), z1)) #ADD''(#neg(#s(#s(z0))), z1) -> c59(#ADD''(#pos(#s(z0)), z1)) #ADD''(#pos(#s(#s(z0))), z1) -> c61(#ADD''(#pos(#s(z0)), z1)) #ADD'(#neg(#s(#s(z0))), z1) -> c33(#ADD''(#pos(#s(z0)), z1)) #ADD'(#neg(#s(#s(z0))), z1) -> c33(#ADD'(#pos(#s(z0)), z1)) S tuples: *'''(z0, z1) -> c88(#MULT'(z0, z1)) DYADE''(z0, z1) -> c89(DYADE#1''(z0, z1)) DYADE#1''(::(z0, z1), z2) -> c90(MULT''(z0, z2)) DYADE#1''(::(z0, z1), z2) -> c91(DYADE''(z1, z2)) MULT''(z0, z1) -> c93(MULT#1''(z1, z0)) MULT#1''(::(z0, z1), z2) -> c94(*'''(z2, z0)) MULT#1''(::(z0, z1), z2) -> c95(MULT''(z2, z1)) K tuples:none Defined Rule Symbols: *'_2, DYADE_2, DYADE#1_2, MULT_2, MULT#1_2, #ADD_2, #MULT_2, #NATMULT_2, #PRED_1, #SUCC_1, #add_2, #mult_2, #natmult_2, #pred_1, #succ_1, *_2, dyade_2, dyade#1_2, mult_2, mult#1_2 Defined Pair Symbols: #MULT'_2, #NATMULT'_2, #MULT''_2, #NATMULT''_2, *''_2, DYADE'_2, DYADE#1'_2, MULT'_2, MULT#1'_2, *'''_2, DYADE''_2, DYADE#1''_2, MULT''_2, MULT#1''_2, #ADD'_2, #ADD''_2 Compound Symbols: c42_1, c43_1, c45_1, c46_1, c48_3, c66_1, c67_1, c69_1, c70_1, c72_2, c81_1, c82_1, c83_2, c85_1, c86_2, c88_1, c89_1, c90_1, c91_1, c93_1, c94_1, c95_1, c37_2, c59_1, c61_1, c33_1 ---------------------------------------- (11) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 3 leading nodes: #ADD'(#neg(#s(#s(z0))), z1) -> c33(#ADD'(#pos(#s(z0)), z1)) #ADD''(#neg(#s(#s(z0))), z1) -> c59(#ADD''(#pos(#s(z0)), z1)) #ADD'(#neg(#s(#s(z0))), z1) -> c33(#ADD''(#pos(#s(z0)), z1)) ---------------------------------------- (12) Obligation: Complexity Dependency Tuples Problem Rules: #ADD(#0, z0) -> c #ADD(#neg(#s(#0)), z0) -> c1(#PRED(z0)) #ADD(#neg(#s(#s(z0))), z1) -> c2(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #ADD(#pos(#s(#0)), z0) -> c3(#SUCC(z0)) #ADD(#pos(#s(#s(z0))), z1) -> c4(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #MULT(#0, #0) -> c5 #MULT(#0, #neg(z0)) -> c6 #MULT(#0, #pos(z0)) -> c7 #MULT(#neg(z0), #0) -> c8 #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1)) #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1)) #MULT(#pos(z0), #0) -> c11 #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1)) #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1)) #NATMULT(#0, z0) -> c14 #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) #PRED(#0) -> c16 #PRED(#neg(#s(z0))) -> c17 #PRED(#pos(#s(#0))) -> c18 #PRED(#pos(#s(#s(z0)))) -> c19 #SUCC(#0) -> c20 #SUCC(#neg(#s(#0))) -> c21 #SUCC(#neg(#s(#s(z0)))) -> c22 #SUCC(#pos(#s(z0))) -> c23 #add(#0, z0) -> z0 #add(#neg(#s(#0)), z0) -> #pred(z0) #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1)) #add(#pos(#s(#0)), z0) -> #succ(z0) #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1)) #mult(#0, #0) -> #0 #mult(#0, #neg(z0)) -> #0 #mult(#0, #pos(z0)) -> #0 #mult(#neg(z0), #0) -> #0 #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1)) #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #0) -> #0 #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1)) #natmult(#0, z0) -> #0 #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1)) #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(z0))) -> #neg(#s(#s(z0))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0)) #succ(#pos(#s(z0))) -> #pos(#s(#s(z0))) *(z0, z1) -> #mult(z0, z1) dyade(z0, z1) -> dyade#1(z0, z1) dyade#1(::(z0, z1), z2) -> ::(mult(z0, z2), dyade(z1, z2)) dyade#1(nil, z0) -> nil mult(z0, z1) -> mult#1(z1, z0) mult#1(::(z0, z1), z2) -> ::(*(z2, z0), mult(z2, z1)) mult#1(nil, z0) -> nil *'(z0, z1) -> c24(#MULT(z0, z1)) DYADE(z0, z1) -> c25(DYADE#1(z0, z1)) DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2)) DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2)) DYADE#1(nil, z0) -> c28 MULT(z0, z1) -> c29(MULT#1(z1, z0)) MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0)) MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1)) MULT#1(nil, z0) -> c32 Tuples: #MULT'(#neg(z0), #neg(z1)) -> c42(#NATMULT'(z0, z1)) #MULT'(#neg(z0), #pos(z1)) -> c43(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #neg(z1)) -> c45(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #pos(z1)) -> c46(#NATMULT'(z0, z1)) #NATMULT'(#s(z0), z1) -> c48(#ADD'(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1), #NATMULT'(z0, z1)) #MULT''(#neg(z0), #neg(z1)) -> c66(#NATMULT''(z0, z1)) #MULT''(#neg(z0), #pos(z1)) -> c67(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #neg(z1)) -> c69(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #pos(z1)) -> c70(#NATMULT''(z0, z1)) #NATMULT''(#s(z0), z1) -> c72(#ADD''(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1)) *''(z0, z1) -> c81(#MULT''(z0, z1)) DYADE'(z0, z1) -> c82(DYADE#1'(z0, z1)) DYADE#1'(::(z0, z1), z2) -> c83(MULT'(z0, z2), DYADE'(z1, z2)) MULT'(z0, z1) -> c85(MULT#1'(z1, z0)) MULT#1'(::(z0, z1), z2) -> c86(*''(z2, z0), MULT'(z2, z1)) *'''(z0, z1) -> c88(#MULT'(z0, z1)) DYADE''(z0, z1) -> c89(DYADE#1''(z0, z1)) DYADE#1''(::(z0, z1), z2) -> c90(MULT''(z0, z2)) DYADE#1''(::(z0, z1), z2) -> c91(DYADE''(z1, z2)) MULT''(z0, z1) -> c93(MULT#1''(z1, z0)) MULT#1''(::(z0, z1), z2) -> c94(*'''(z2, z0)) MULT#1''(::(z0, z1), z2) -> c95(MULT''(z2, z1)) #ADD'(#pos(#s(#s(z0))), z1) -> c37(#ADD''(#pos(#s(z0)), z1), #ADD'(#pos(#s(z0)), z1)) #ADD''(#pos(#s(#s(z0))), z1) -> c61(#ADD''(#pos(#s(z0)), z1)) S tuples: *'''(z0, z1) -> c88(#MULT'(z0, z1)) DYADE''(z0, z1) -> c89(DYADE#1''(z0, z1)) DYADE#1''(::(z0, z1), z2) -> c90(MULT''(z0, z2)) DYADE#1''(::(z0, z1), z2) -> c91(DYADE''(z1, z2)) MULT''(z0, z1) -> c93(MULT#1''(z1, z0)) MULT#1''(::(z0, z1), z2) -> c94(*'''(z2, z0)) MULT#1''(::(z0, z1), z2) -> c95(MULT''(z2, z1)) K tuples:none Defined Rule Symbols: *'_2, DYADE_2, DYADE#1_2, MULT_2, MULT#1_2, #ADD_2, #MULT_2, #NATMULT_2, #PRED_1, #SUCC_1, #add_2, #mult_2, #natmult_2, #pred_1, #succ_1, *_2, dyade_2, dyade#1_2, mult_2, mult#1_2 Defined Pair Symbols: #MULT'_2, #NATMULT'_2, #MULT''_2, #NATMULT''_2, *''_2, DYADE'_2, DYADE#1'_2, MULT'_2, MULT#1'_2, *'''_2, DYADE''_2, DYADE#1''_2, MULT''_2, MULT#1''_2, #ADD'_2, #ADD''_2 Compound Symbols: c42_1, c43_1, c45_1, c46_1, c48_3, c66_1, c67_1, c69_1, c70_1, c72_2, c81_1, c82_1, c83_2, c85_1, c86_2, c88_1, c89_1, c90_1, c91_1, c93_1, c94_1, c95_1, c37_2, c61_1 ---------------------------------------- (13) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: #ADD(#0, z0) -> c #ADD(#neg(#s(#0)), z0) -> c1(#PRED(z0)) #ADD(#neg(#s(#s(z0))), z1) -> c2(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #ADD(#pos(#s(#0)), z0) -> c3(#SUCC(z0)) #ADD(#pos(#s(#s(z0))), z1) -> c4(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #MULT(#0, #0) -> c5 #MULT(#0, #neg(z0)) -> c6 #MULT(#0, #pos(z0)) -> c7 #MULT(#neg(z0), #0) -> c8 #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1)) #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1)) #MULT(#pos(z0), #0) -> c11 #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1)) #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1)) #NATMULT(#0, z0) -> c14 #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) #PRED(#0) -> c16 #PRED(#neg(#s(z0))) -> c17 #PRED(#pos(#s(#0))) -> c18 #PRED(#pos(#s(#s(z0)))) -> c19 #SUCC(#0) -> c20 #SUCC(#neg(#s(#0))) -> c21 #SUCC(#neg(#s(#s(z0)))) -> c22 #SUCC(#pos(#s(z0))) -> c23 #add(#0, z0) -> z0 #add(#neg(#s(#0)), z0) -> #pred(z0) #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1)) #mult(#0, #0) -> #0 #mult(#0, #neg(z0)) -> #0 #mult(#0, #pos(z0)) -> #0 #mult(#neg(z0), #0) -> #0 #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1)) #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #0) -> #0 #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1)) #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(z0))) -> #neg(#s(#s(z0))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0)) *(z0, z1) -> #mult(z0, z1) dyade(z0, z1) -> dyade#1(z0, z1) dyade#1(::(z0, z1), z2) -> ::(mult(z0, z2), dyade(z1, z2)) dyade#1(nil, z0) -> nil mult(z0, z1) -> mult#1(z1, z0) mult#1(::(z0, z1), z2) -> ::(*(z2, z0), mult(z2, z1)) mult#1(nil, z0) -> nil *'(z0, z1) -> c24(#MULT(z0, z1)) DYADE(z0, z1) -> c25(DYADE#1(z0, z1)) DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2)) DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2)) DYADE#1(nil, z0) -> c28 MULT(z0, z1) -> c29(MULT#1(z1, z0)) MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0)) MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1)) MULT#1(nil, z0) -> c32 ---------------------------------------- (14) Obligation: Complexity Dependency Tuples Problem Rules: #natmult(#0, z0) -> #0 #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1)) #add(#pos(#s(#0)), z0) -> #succ(z0) #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0)) #succ(#pos(#s(z0))) -> #pos(#s(#s(z0))) Tuples: #MULT'(#neg(z0), #neg(z1)) -> c42(#NATMULT'(z0, z1)) #MULT'(#neg(z0), #pos(z1)) -> c43(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #neg(z1)) -> c45(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #pos(z1)) -> c46(#NATMULT'(z0, z1)) #NATMULT'(#s(z0), z1) -> c48(#ADD'(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1), #NATMULT'(z0, z1)) #MULT''(#neg(z0), #neg(z1)) -> c66(#NATMULT''(z0, z1)) #MULT''(#neg(z0), #pos(z1)) -> c67(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #neg(z1)) -> c69(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #pos(z1)) -> c70(#NATMULT''(z0, z1)) #NATMULT''(#s(z0), z1) -> c72(#ADD''(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1)) *''(z0, z1) -> c81(#MULT''(z0, z1)) DYADE'(z0, z1) -> c82(DYADE#1'(z0, z1)) DYADE#1'(::(z0, z1), z2) -> c83(MULT'(z0, z2), DYADE'(z1, z2)) MULT'(z0, z1) -> c85(MULT#1'(z1, z0)) MULT#1'(::(z0, z1), z2) -> c86(*''(z2, z0), MULT'(z2, z1)) *'''(z0, z1) -> c88(#MULT'(z0, z1)) DYADE''(z0, z1) -> c89(DYADE#1''(z0, z1)) DYADE#1''(::(z0, z1), z2) -> c90(MULT''(z0, z2)) DYADE#1''(::(z0, z1), z2) -> c91(DYADE''(z1, z2)) MULT''(z0, z1) -> c93(MULT#1''(z1, z0)) MULT#1''(::(z0, z1), z2) -> c94(*'''(z2, z0)) MULT#1''(::(z0, z1), z2) -> c95(MULT''(z2, z1)) #ADD'(#pos(#s(#s(z0))), z1) -> c37(#ADD''(#pos(#s(z0)), z1), #ADD'(#pos(#s(z0)), z1)) #ADD''(#pos(#s(#s(z0))), z1) -> c61(#ADD''(#pos(#s(z0)), z1)) S tuples: *'''(z0, z1) -> c88(#MULT'(z0, z1)) DYADE''(z0, z1) -> c89(DYADE#1''(z0, z1)) DYADE#1''(::(z0, z1), z2) -> c90(MULT''(z0, z2)) DYADE#1''(::(z0, z1), z2) -> c91(DYADE''(z1, z2)) MULT''(z0, z1) -> c93(MULT#1''(z1, z0)) MULT#1''(::(z0, z1), z2) -> c94(*'''(z2, z0)) MULT#1''(::(z0, z1), z2) -> c95(MULT''(z2, z1)) K tuples:none Defined Rule Symbols: #natmult_2, #add_2, #succ_1 Defined Pair Symbols: #MULT'_2, #NATMULT'_2, #MULT''_2, #NATMULT''_2, *''_2, DYADE'_2, DYADE#1'_2, MULT'_2, MULT#1'_2, *'''_2, DYADE''_2, DYADE#1''_2, MULT''_2, MULT#1''_2, #ADD'_2, #ADD''_2 Compound Symbols: c42_1, c43_1, c45_1, c46_1, c48_3, c66_1, c67_1, c69_1, c70_1, c72_2, c81_1, c82_1, c83_2, c85_1, c86_2, c88_1, c89_1, c90_1, c91_1, c93_1, c94_1, c95_1, c37_2, c61_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. *'''(z0, z1) -> c88(#MULT'(z0, z1)) DYADE#1''(::(z0, z1), z2) -> c90(MULT''(z0, z2)) DYADE#1''(::(z0, z1), z2) -> c91(DYADE''(z1, z2)) MULT''(z0, z1) -> c93(MULT#1''(z1, z0)) We considered the (Usable) Rules:none And the Tuples: #MULT'(#neg(z0), #neg(z1)) -> c42(#NATMULT'(z0, z1)) #MULT'(#neg(z0), #pos(z1)) -> c43(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #neg(z1)) -> c45(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #pos(z1)) -> c46(#NATMULT'(z0, z1)) #NATMULT'(#s(z0), z1) -> c48(#ADD'(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1), #NATMULT'(z0, z1)) #MULT''(#neg(z0), #neg(z1)) -> c66(#NATMULT''(z0, z1)) #MULT''(#neg(z0), #pos(z1)) -> c67(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #neg(z1)) -> c69(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #pos(z1)) -> c70(#NATMULT''(z0, z1)) #NATMULT''(#s(z0), z1) -> c72(#ADD''(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1)) *''(z0, z1) -> c81(#MULT''(z0, z1)) DYADE'(z0, z1) -> c82(DYADE#1'(z0, z1)) DYADE#1'(::(z0, z1), z2) -> c83(MULT'(z0, z2), DYADE'(z1, z2)) MULT'(z0, z1) -> c85(MULT#1'(z1, z0)) MULT#1'(::(z0, z1), z2) -> c86(*''(z2, z0), MULT'(z2, z1)) *'''(z0, z1) -> c88(#MULT'(z0, z1)) DYADE''(z0, z1) -> c89(DYADE#1''(z0, z1)) DYADE#1''(::(z0, z1), z2) -> c90(MULT''(z0, z2)) DYADE#1''(::(z0, z1), z2) -> c91(DYADE''(z1, z2)) MULT''(z0, z1) -> c93(MULT#1''(z1, z0)) MULT#1''(::(z0, z1), z2) -> c94(*'''(z2, z0)) MULT#1''(::(z0, z1), z2) -> c95(MULT''(z2, z1)) #ADD'(#pos(#s(#s(z0))), z1) -> c37(#ADD''(#pos(#s(z0)), z1), #ADD'(#pos(#s(z0)), z1)) #ADD''(#pos(#s(#s(z0))), z1) -> c61(#ADD''(#pos(#s(z0)), z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(#0) = [1] POL(#ADD'(x_1, x_2)) = 0 POL(#ADD''(x_1, x_2)) = 0 POL(#MULT'(x_1, x_2)) = x_1 + x_2 POL(#MULT''(x_1, x_2)) = 0 POL(#NATMULT'(x_1, x_2)) = 0 POL(#NATMULT''(x_1, x_2)) = 0 POL(#add(x_1, x_2)) = [1] + x_1 + x_2 POL(#natmult(x_1, x_2)) = [1] + x_1 + x_2 POL(#neg(x_1)) = [1] POL(#pos(x_1)) = [1] POL(#s(x_1)) = [1] POL(#succ(x_1)) = [1] POL(*''(x_1, x_2)) = 0 POL(*'''(x_1, x_2)) = [1] + x_1 + x_2 POL(::(x_1, x_2)) = [1] + x_1 + x_2 POL(DYADE#1'(x_1, x_2)) = [1] + x_1 + x_2 POL(DYADE#1''(x_1, x_2)) = [1] + x_1 + x_2 POL(DYADE'(x_1, x_2)) = [1] + x_1 + x_2 POL(DYADE''(x_1, x_2)) = [1] + x_1 + x_2 POL(MULT#1'(x_1, x_2)) = [1] + x_2 POL(MULT#1''(x_1, x_2)) = x_1 + x_2 POL(MULT'(x_1, x_2)) = [1] + x_1 POL(MULT''(x_1, x_2)) = [1] + x_1 + x_2 POL(c37(x_1, x_2)) = x_1 + x_2 POL(c42(x_1)) = x_1 POL(c43(x_1)) = x_1 POL(c45(x_1)) = x_1 POL(c46(x_1)) = x_1 POL(c48(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c61(x_1)) = x_1 POL(c66(x_1)) = x_1 POL(c67(x_1)) = x_1 POL(c69(x_1)) = x_1 POL(c70(x_1)) = x_1 POL(c72(x_1, x_2)) = x_1 + x_2 POL(c81(x_1)) = x_1 POL(c82(x_1)) = x_1 POL(c83(x_1, x_2)) = x_1 + x_2 POL(c85(x_1)) = x_1 POL(c86(x_1, x_2)) = x_1 + x_2 POL(c88(x_1)) = x_1 POL(c89(x_1)) = x_1 POL(c90(x_1)) = x_1 POL(c91(x_1)) = x_1 POL(c93(x_1)) = x_1 POL(c94(x_1)) = x_1 POL(c95(x_1)) = x_1 ---------------------------------------- (16) Obligation: Complexity Dependency Tuples Problem Rules: #natmult(#0, z0) -> #0 #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1)) #add(#pos(#s(#0)), z0) -> #succ(z0) #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0)) #succ(#pos(#s(z0))) -> #pos(#s(#s(z0))) Tuples: #MULT'(#neg(z0), #neg(z1)) -> c42(#NATMULT'(z0, z1)) #MULT'(#neg(z0), #pos(z1)) -> c43(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #neg(z1)) -> c45(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #pos(z1)) -> c46(#NATMULT'(z0, z1)) #NATMULT'(#s(z0), z1) -> c48(#ADD'(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1), #NATMULT'(z0, z1)) #MULT''(#neg(z0), #neg(z1)) -> c66(#NATMULT''(z0, z1)) #MULT''(#neg(z0), #pos(z1)) -> c67(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #neg(z1)) -> c69(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #pos(z1)) -> c70(#NATMULT''(z0, z1)) #NATMULT''(#s(z0), z1) -> c72(#ADD''(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1)) *''(z0, z1) -> c81(#MULT''(z0, z1)) DYADE'(z0, z1) -> c82(DYADE#1'(z0, z1)) DYADE#1'(::(z0, z1), z2) -> c83(MULT'(z0, z2), DYADE'(z1, z2)) MULT'(z0, z1) -> c85(MULT#1'(z1, z0)) MULT#1'(::(z0, z1), z2) -> c86(*''(z2, z0), MULT'(z2, z1)) *'''(z0, z1) -> c88(#MULT'(z0, z1)) DYADE''(z0, z1) -> c89(DYADE#1''(z0, z1)) DYADE#1''(::(z0, z1), z2) -> c90(MULT''(z0, z2)) DYADE#1''(::(z0, z1), z2) -> c91(DYADE''(z1, z2)) MULT''(z0, z1) -> c93(MULT#1''(z1, z0)) MULT#1''(::(z0, z1), z2) -> c94(*'''(z2, z0)) MULT#1''(::(z0, z1), z2) -> c95(MULT''(z2, z1)) #ADD'(#pos(#s(#s(z0))), z1) -> c37(#ADD''(#pos(#s(z0)), z1), #ADD'(#pos(#s(z0)), z1)) #ADD''(#pos(#s(#s(z0))), z1) -> c61(#ADD''(#pos(#s(z0)), z1)) S tuples: DYADE''(z0, z1) -> c89(DYADE#1''(z0, z1)) MULT#1''(::(z0, z1), z2) -> c94(*'''(z2, z0)) MULT#1''(::(z0, z1), z2) -> c95(MULT''(z2, z1)) K tuples: *'''(z0, z1) -> c88(#MULT'(z0, z1)) DYADE#1''(::(z0, z1), z2) -> c90(MULT''(z0, z2)) DYADE#1''(::(z0, z1), z2) -> c91(DYADE''(z1, z2)) MULT''(z0, z1) -> c93(MULT#1''(z1, z0)) Defined Rule Symbols: #natmult_2, #add_2, #succ_1 Defined Pair Symbols: #MULT'_2, #NATMULT'_2, #MULT''_2, #NATMULT''_2, *''_2, DYADE'_2, DYADE#1'_2, MULT'_2, MULT#1'_2, *'''_2, DYADE''_2, DYADE#1''_2, MULT''_2, MULT#1''_2, #ADD'_2, #ADD''_2 Compound Symbols: c42_1, c43_1, c45_1, c46_1, c48_3, c66_1, c67_1, c69_1, c70_1, c72_2, c81_1, c82_1, c83_2, c85_1, c86_2, c88_1, c89_1, c90_1, c91_1, c93_1, c94_1, c95_1, c37_2, c61_1 ---------------------------------------- (17) CdtKnowledgeProof (FINISHED) The following tuples could be moved from S to K by knowledge propagation: DYADE''(z0, z1) -> c89(DYADE#1''(z0, z1)) MULT#1''(::(z0, z1), z2) -> c94(*'''(z2, z0)) MULT#1''(::(z0, z1), z2) -> c95(MULT''(z2, z1)) DYADE#1''(::(z0, z1), z2) -> c90(MULT''(z0, z2)) DYADE#1''(::(z0, z1), z2) -> c91(DYADE''(z1, z2)) *'''(z0, z1) -> c88(#MULT'(z0, z1)) MULT''(z0, z1) -> c93(MULT#1''(z1, z0)) Now S is empty ---------------------------------------- (18) BOUNDS(1, 1) ---------------------------------------- (19) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (20) 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: *'(z0, z1) -> c24(#MULT(z0, z1)) DYADE(z0, z1) -> c25(DYADE#1(z0, z1)) DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2)) DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2)) DYADE#1(nil, z0) -> c28 MULT(z0, z1) -> c29(MULT#1(z1, z0)) MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0)) MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1)) MULT#1(nil, z0) -> c32 The (relative) TRS S consists of the following rules: #ADD(#0, z0) -> c #ADD(#neg(#s(#0)), z0) -> c1(#PRED(z0)) #ADD(#neg(#s(#s(z0))), z1) -> c2(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #ADD(#pos(#s(#0)), z0) -> c3(#SUCC(z0)) #ADD(#pos(#s(#s(z0))), z1) -> c4(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #MULT(#0, #0) -> c5 #MULT(#0, #neg(z0)) -> c6 #MULT(#0, #pos(z0)) -> c7 #MULT(#neg(z0), #0) -> c8 #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1)) #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1)) #MULT(#pos(z0), #0) -> c11 #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1)) #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1)) #NATMULT(#0, z0) -> c14 #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) #PRED(#0) -> c16 #PRED(#neg(#s(z0))) -> c17 #PRED(#pos(#s(#0))) -> c18 #PRED(#pos(#s(#s(z0)))) -> c19 #SUCC(#0) -> c20 #SUCC(#neg(#s(#0))) -> c21 #SUCC(#neg(#s(#s(z0)))) -> c22 #SUCC(#pos(#s(z0))) -> c23 #add(#0, z0) -> z0 #add(#neg(#s(#0)), z0) -> #pred(z0) #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1)) #add(#pos(#s(#0)), z0) -> #succ(z0) #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1)) #mult(#0, #0) -> #0 #mult(#0, #neg(z0)) -> #0 #mult(#0, #pos(z0)) -> #0 #mult(#neg(z0), #0) -> #0 #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1)) #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #0) -> #0 #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1)) #natmult(#0, z0) -> #0 #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1)) #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(z0))) -> #neg(#s(#s(z0))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0)) #succ(#pos(#s(z0))) -> #pos(#s(#s(z0))) *(z0, z1) -> #mult(z0, z1) dyade(z0, z1) -> dyade#1(z0, z1) dyade#1(::(z0, z1), z2) -> ::(mult(z0, z2), dyade(z1, z2)) dyade#1(nil, z0) -> nil mult(z0, z1) -> mult#1(z1, z0) mult#1(::(z0, z1), z2) -> ::(*(z2, z0), mult(z2, z1)) mult#1(nil, z0) -> nil Rewrite Strategy: INNERMOST ---------------------------------------- (21) DecreasingLoopProof (LOWER BOUND(ID)) The following loop(s) give(s) rise to the lower bound Omega(n^1): The rewrite sequence DYADE#1(::(z0, z1), z2) ->^+ c27(c25(DYADE#1(z1, z2))) gives rise to a decreasing loop by considering the right hand sides subterm at position [0,0]. The pumping substitution is [z1 / ::(z0, z1)]. The result substitution is [ ]. ---------------------------------------- (22) Complex Obligation (BEST) ---------------------------------------- (23) 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: *'(z0, z1) -> c24(#MULT(z0, z1)) DYADE(z0, z1) -> c25(DYADE#1(z0, z1)) DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2)) DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2)) DYADE#1(nil, z0) -> c28 MULT(z0, z1) -> c29(MULT#1(z1, z0)) MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0)) MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1)) MULT#1(nil, z0) -> c32 The (relative) TRS S consists of the following rules: #ADD(#0, z0) -> c #ADD(#neg(#s(#0)), z0) -> c1(#PRED(z0)) #ADD(#neg(#s(#s(z0))), z1) -> c2(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #ADD(#pos(#s(#0)), z0) -> c3(#SUCC(z0)) #ADD(#pos(#s(#s(z0))), z1) -> c4(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #MULT(#0, #0) -> c5 #MULT(#0, #neg(z0)) -> c6 #MULT(#0, #pos(z0)) -> c7 #MULT(#neg(z0), #0) -> c8 #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1)) #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1)) #MULT(#pos(z0), #0) -> c11 #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1)) #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1)) #NATMULT(#0, z0) -> c14 #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) #PRED(#0) -> c16 #PRED(#neg(#s(z0))) -> c17 #PRED(#pos(#s(#0))) -> c18 #PRED(#pos(#s(#s(z0)))) -> c19 #SUCC(#0) -> c20 #SUCC(#neg(#s(#0))) -> c21 #SUCC(#neg(#s(#s(z0)))) -> c22 #SUCC(#pos(#s(z0))) -> c23 #add(#0, z0) -> z0 #add(#neg(#s(#0)), z0) -> #pred(z0) #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1)) #add(#pos(#s(#0)), z0) -> #succ(z0) #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1)) #mult(#0, #0) -> #0 #mult(#0, #neg(z0)) -> #0 #mult(#0, #pos(z0)) -> #0 #mult(#neg(z0), #0) -> #0 #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1)) #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #0) -> #0 #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1)) #natmult(#0, z0) -> #0 #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1)) #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(z0))) -> #neg(#s(#s(z0))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0)) #succ(#pos(#s(z0))) -> #pos(#s(#s(z0))) *(z0, z1) -> #mult(z0, z1) dyade(z0, z1) -> dyade#1(z0, z1) dyade#1(::(z0, z1), z2) -> ::(mult(z0, z2), dyade(z1, z2)) dyade#1(nil, z0) -> nil mult(z0, z1) -> mult#1(z1, z0) mult#1(::(z0, z1), z2) -> ::(*(z2, z0), mult(z2, z1)) mult#1(nil, z0) -> nil Rewrite Strategy: INNERMOST ---------------------------------------- (24) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (25) BOUNDS(n^1, INF) ---------------------------------------- (26) 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: *'(z0, z1) -> c24(#MULT(z0, z1)) DYADE(z0, z1) -> c25(DYADE#1(z0, z1)) DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2)) DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2)) DYADE#1(nil, z0) -> c28 MULT(z0, z1) -> c29(MULT#1(z1, z0)) MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0)) MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1)) MULT#1(nil, z0) -> c32 The (relative) TRS S consists of the following rules: #ADD(#0, z0) -> c #ADD(#neg(#s(#0)), z0) -> c1(#PRED(z0)) #ADD(#neg(#s(#s(z0))), z1) -> c2(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #ADD(#pos(#s(#0)), z0) -> c3(#SUCC(z0)) #ADD(#pos(#s(#s(z0))), z1) -> c4(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #MULT(#0, #0) -> c5 #MULT(#0, #neg(z0)) -> c6 #MULT(#0, #pos(z0)) -> c7 #MULT(#neg(z0), #0) -> c8 #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1)) #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1)) #MULT(#pos(z0), #0) -> c11 #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1)) #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1)) #NATMULT(#0, z0) -> c14 #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) #PRED(#0) -> c16 #PRED(#neg(#s(z0))) -> c17 #PRED(#pos(#s(#0))) -> c18 #PRED(#pos(#s(#s(z0)))) -> c19 #SUCC(#0) -> c20 #SUCC(#neg(#s(#0))) -> c21 #SUCC(#neg(#s(#s(z0)))) -> c22 #SUCC(#pos(#s(z0))) -> c23 #add(#0, z0) -> z0 #add(#neg(#s(#0)), z0) -> #pred(z0) #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1)) #add(#pos(#s(#0)), z0) -> #succ(z0) #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1)) #mult(#0, #0) -> #0 #mult(#0, #neg(z0)) -> #0 #mult(#0, #pos(z0)) -> #0 #mult(#neg(z0), #0) -> #0 #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1)) #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #0) -> #0 #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1)) #natmult(#0, z0) -> #0 #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1)) #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(z0))) -> #neg(#s(#s(z0))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0)) #succ(#pos(#s(z0))) -> #pos(#s(#s(z0))) *(z0, z1) -> #mult(z0, z1) dyade(z0, z1) -> dyade#1(z0, z1) dyade#1(::(z0, z1), z2) -> ::(mult(z0, z2), dyade(z1, z2)) dyade#1(nil, z0) -> nil mult(z0, z1) -> mult#1(z1, z0) mult#1(::(z0, z1), z2) -> ::(*(z2, z0), mult(z2, z1)) mult#1(nil, z0) -> nil Rewrite Strategy: INNERMOST