WORST_CASE(?,O(n^1)) * Step 1: Sum. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: *'(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() - Weak TRS: #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() - Signature: {#ADD/2,#MULT/2,#NATMULT/2,#PRED/1,#SUCC/1,#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,*'/2,DYADE/2 ,DYADE#1/2,MULT/2,MULT#1/2,dyade/2,dyade#1/2,mult/2,mult#1/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,c/0,c1/1,c10/1 ,c11/0,c12/1,c13/1,c14/0,c15/2,c16/0,c17/0,c18/0,c19/0,c2/2,c20/0,c21/0,c22/0,c23/0,c24/1,c25/1,c26/1,c27/1 ,c28/0,c29/1,c3/1,c30/1,c31/1,c32/0,c4/2,c5/0,c6/0,c7/0,c8/0,c9/1,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#ADD,#MULT,#NATMULT,#PRED,#SUCC,#add,#mult,#natmult,#pred ,#succ,*,*',DYADE,DYADE#1,MULT,MULT#1,dyade,dyade#1,mult,mult#1} and constructors {#0,#neg,#pos,#s,::,c,c1 ,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c4,c5,c6 ,c7,c8,c9,nil} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: DependencyPairs. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: *'(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() - Weak TRS: #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() - Signature: {#ADD/2,#MULT/2,#NATMULT/2,#PRED/1,#SUCC/1,#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,*'/2,DYADE/2 ,DYADE#1/2,MULT/2,MULT#1/2,dyade/2,dyade#1/2,mult/2,mult#1/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,c/0,c1/1,c10/1 ,c11/0,c12/1,c13/1,c14/0,c15/2,c16/0,c17/0,c18/0,c19/0,c2/2,c20/0,c21/0,c22/0,c23/0,c24/1,c25/1,c26/1,c27/1 ,c28/0,c29/1,c3/1,c30/1,c31/1,c32/0,c4/2,c5/0,c6/0,c7/0,c8/0,c9/1,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#ADD,#MULT,#NATMULT,#PRED,#SUCC,#add,#mult,#natmult,#pred ,#succ,*,*',DYADE,DYADE#1,MULT,MULT#1,dyade,dyade#1,mult,mult#1} and constructors {#0,#neg,#pos,#s,::,c,c1 ,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c4,c5,c6 ,c7,c8,c9,nil} + Applied Processor: DependencyPairs {dpKind_ = WIDP} + Details: We add the following weak innermost dependency pairs: Strict DPs *'#(z0,z1) -> c_1(#MULT#(z0,z1)) DYADE#(z0,z1) -> c_2(DYADE#1#(z0,z1)) DYADE#1#(::(z0,z1),z2) -> c_3(MULT#(z0,z2)) DYADE#1#(::(z0,z1),z2) -> c_4(DYADE#(z1,z2)) DYADE#1#(nil(),z0) -> c_5() MULT#(z0,z1) -> c_6(MULT#1#(z1,z0)) MULT#1#(::(z0,z1),z2) -> c_7(*'#(z2,z0)) MULT#1#(::(z0,z1),z2) -> c_8(MULT#(z2,z1)) MULT#1#(nil(),z0) -> c_9() Weak DPs #ADD#(#0(),z0) -> c_10() #ADD#(#neg(#s(#0())),z0) -> c_11(#PRED#(z0)) #ADD#(#neg(#s(#s(z0))),z1) -> c_12(#PRED#(#add(#pos(#s(z0)),z1)),#ADD#(#pos(#s(z0)),z1)) #ADD#(#pos(#s(#0())),z0) -> c_13(#SUCC#(z0)) #ADD#(#pos(#s(#s(z0))),z1) -> c_14(#SUCC#(#add(#pos(#s(z0)),z1)),#ADD#(#pos(#s(z0)),z1)) #MULT#(#0(),#0()) -> c_15() #MULT#(#0(),#neg(z0)) -> c_16() #MULT#(#0(),#pos(z0)) -> c_17() #MULT#(#neg(z0),#0()) -> c_18() #MULT#(#neg(z0),#neg(z1)) -> c_19(#NATMULT#(z0,z1)) #MULT#(#neg(z0),#pos(z1)) -> c_20(#NATMULT#(z0,z1)) #MULT#(#pos(z0),#0()) -> c_21() #MULT#(#pos(z0),#neg(z1)) -> c_22(#NATMULT#(z0,z1)) #MULT#(#pos(z0),#pos(z1)) -> c_23(#NATMULT#(z0,z1)) #NATMULT#(#0(),z0) -> c_24() #NATMULT#(#s(z0),z1) -> c_25(#ADD#(#pos(z1),#natmult(z0,z1)),#NATMULT#(z0,z1)) #PRED#(#0()) -> c_26() #PRED#(#neg(#s(z0))) -> c_27() #PRED#(#pos(#s(#0()))) -> c_28() #PRED#(#pos(#s(#s(z0)))) -> c_29() #SUCC#(#0()) -> c_30() #SUCC#(#neg(#s(#0()))) -> c_31() #SUCC#(#neg(#s(#s(z0)))) -> c_32() #SUCC#(#pos(#s(z0))) -> c_33() #add#(#0(),z0) -> c_34() #add#(#neg(#s(#0())),z0) -> c_35(#pred#(z0)) #add#(#neg(#s(#s(z0))),z1) -> c_36(#pred#(#add(#pos(#s(z0)),z1))) #add#(#pos(#s(#0())),z0) -> c_37(#succ#(z0)) #add#(#pos(#s(#s(z0))),z1) -> c_38(#succ#(#add(#pos(#s(z0)),z1))) #mult#(#0(),#0()) -> c_39() #mult#(#0(),#neg(z0)) -> c_40() #mult#(#0(),#pos(z0)) -> c_41() #mult#(#neg(z0),#0()) -> c_42() #mult#(#neg(z0),#neg(z1)) -> c_43(#natmult#(z0,z1)) #mult#(#neg(z0),#pos(z1)) -> c_44(#natmult#(z0,z1)) #mult#(#pos(z0),#0()) -> c_45() #mult#(#pos(z0),#neg(z1)) -> c_46(#natmult#(z0,z1)) #mult#(#pos(z0),#pos(z1)) -> c_47(#natmult#(z0,z1)) #natmult#(#0(),z0) -> c_48() #natmult#(#s(z0),z1) -> c_49(#add#(#pos(z1),#natmult(z0,z1))) #pred#(#0()) -> c_50() #pred#(#neg(#s(z0))) -> c_51() #pred#(#pos(#s(#0()))) -> c_52() #pred#(#pos(#s(#s(z0)))) -> c_53() #succ#(#0()) -> c_54() #succ#(#neg(#s(#0()))) -> c_55() #succ#(#neg(#s(#s(z0)))) -> c_56() #succ#(#pos(#s(z0))) -> c_57() *#(z0,z1) -> c_58(#mult#(z0,z1)) dyade#(z0,z1) -> c_59(dyade#1#(z0,z1)) dyade#1#(::(z0,z1),z2) -> c_60(mult#(z0,z2),dyade#(z1,z2)) dyade#1#(nil(),z0) -> c_61() mult#(z0,z1) -> c_62(mult#1#(z1,z0)) mult#1#(::(z0,z1),z2) -> c_63(*#(z2,z0),mult#(z2,z1)) mult#1#(nil(),z0) -> c_64() and mark the set of starting terms. * Step 3: UsableRules. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: *'#(z0,z1) -> c_1(#MULT#(z0,z1)) DYADE#(z0,z1) -> c_2(DYADE#1#(z0,z1)) DYADE#1#(::(z0,z1),z2) -> c_3(MULT#(z0,z2)) DYADE#1#(::(z0,z1),z2) -> c_4(DYADE#(z1,z2)) DYADE#1#(nil(),z0) -> c_5() MULT#(z0,z1) -> c_6(MULT#1#(z1,z0)) MULT#1#(::(z0,z1),z2) -> c_7(*'#(z2,z0)) MULT#1#(::(z0,z1),z2) -> c_8(MULT#(z2,z1)) MULT#1#(nil(),z0) -> c_9() - Strict TRS: *'(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() - Weak DPs: #ADD#(#0(),z0) -> c_10() #ADD#(#neg(#s(#0())),z0) -> c_11(#PRED#(z0)) #ADD#(#neg(#s(#s(z0))),z1) -> c_12(#PRED#(#add(#pos(#s(z0)),z1)),#ADD#(#pos(#s(z0)),z1)) #ADD#(#pos(#s(#0())),z0) -> c_13(#SUCC#(z0)) #ADD#(#pos(#s(#s(z0))),z1) -> c_14(#SUCC#(#add(#pos(#s(z0)),z1)),#ADD#(#pos(#s(z0)),z1)) #MULT#(#0(),#0()) -> c_15() #MULT#(#0(),#neg(z0)) -> c_16() #MULT#(#0(),#pos(z0)) -> c_17() #MULT#(#neg(z0),#0()) -> c_18() #MULT#(#neg(z0),#neg(z1)) -> c_19(#NATMULT#(z0,z1)) #MULT#(#neg(z0),#pos(z1)) -> c_20(#NATMULT#(z0,z1)) #MULT#(#pos(z0),#0()) -> c_21() #MULT#(#pos(z0),#neg(z1)) -> c_22(#NATMULT#(z0,z1)) #MULT#(#pos(z0),#pos(z1)) -> c_23(#NATMULT#(z0,z1)) #NATMULT#(#0(),z0) -> c_24() #NATMULT#(#s(z0),z1) -> c_25(#ADD#(#pos(z1),#natmult(z0,z1)),#NATMULT#(z0,z1)) #PRED#(#0()) -> c_26() #PRED#(#neg(#s(z0))) -> c_27() #PRED#(#pos(#s(#0()))) -> c_28() #PRED#(#pos(#s(#s(z0)))) -> c_29() #SUCC#(#0()) -> c_30() #SUCC#(#neg(#s(#0()))) -> c_31() #SUCC#(#neg(#s(#s(z0)))) -> c_32() #SUCC#(#pos(#s(z0))) -> c_33() #add#(#0(),z0) -> c_34() #add#(#neg(#s(#0())),z0) -> c_35(#pred#(z0)) #add#(#neg(#s(#s(z0))),z1) -> c_36(#pred#(#add(#pos(#s(z0)),z1))) #add#(#pos(#s(#0())),z0) -> c_37(#succ#(z0)) #add#(#pos(#s(#s(z0))),z1) -> c_38(#succ#(#add(#pos(#s(z0)),z1))) #mult#(#0(),#0()) -> c_39() #mult#(#0(),#neg(z0)) -> c_40() #mult#(#0(),#pos(z0)) -> c_41() #mult#(#neg(z0),#0()) -> c_42() #mult#(#neg(z0),#neg(z1)) -> c_43(#natmult#(z0,z1)) #mult#(#neg(z0),#pos(z1)) -> c_44(#natmult#(z0,z1)) #mult#(#pos(z0),#0()) -> c_45() #mult#(#pos(z0),#neg(z1)) -> c_46(#natmult#(z0,z1)) #mult#(#pos(z0),#pos(z1)) -> c_47(#natmult#(z0,z1)) #natmult#(#0(),z0) -> c_48() #natmult#(#s(z0),z1) -> c_49(#add#(#pos(z1),#natmult(z0,z1))) #pred#(#0()) -> c_50() #pred#(#neg(#s(z0))) -> c_51() #pred#(#pos(#s(#0()))) -> c_52() #pred#(#pos(#s(#s(z0)))) -> c_53() #succ#(#0()) -> c_54() #succ#(#neg(#s(#0()))) -> c_55() #succ#(#neg(#s(#s(z0)))) -> c_56() #succ#(#pos(#s(z0))) -> c_57() *#(z0,z1) -> c_58(#mult#(z0,z1)) dyade#(z0,z1) -> c_59(dyade#1#(z0,z1)) dyade#1#(::(z0,z1),z2) -> c_60(mult#(z0,z2),dyade#(z1,z2)) dyade#1#(nil(),z0) -> c_61() mult#(z0,z1) -> c_62(mult#1#(z1,z0)) mult#1#(::(z0,z1),z2) -> c_63(*#(z2,z0),mult#(z2,z1)) mult#1#(nil(),z0) -> c_64() - Weak TRS: #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() - Signature: {#ADD/2,#MULT/2,#NATMULT/2,#PRED/1,#SUCC/1,#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,*'/2,DYADE/2 ,DYADE#1/2,MULT/2,MULT#1/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,*'#/2,DYADE#/2,DYADE#1#/2,MULT#/2,MULT#1#/2,dyade#/2 ,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,c/0,c1/1,c10/1,c11/0,c12/1,c13/1,c14/0,c15/2 ,c16/0,c17/0,c18/0,c19/0,c2/2,c20/0,c21/0,c22/0,c23/0,c24/1,c25/1,c26/1,c27/1,c28/0,c29/1,c3/1,c30/1,c31/1 ,c32/0,c4/2,c5/0,c6/0,c7/0,c8/0,c9/1,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/1,c_7/1,c_8/1,c_9/0,c_10/0 ,c_11/1,c_12/2,c_13/1,c_14/2,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/0,c_22/1,c_23/1,c_24/0,c_25/2 ,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/1,c_36/1,c_37/1,c_38/1,c_39/0,c_40/0 ,c_41/0,c_42/0,c_43/1,c_44/1,c_45/0,c_46/1,c_47/1,c_48/0,c_49/1,c_50/0,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0 ,c_56/0,c_57/0,c_58/1,c_59/1,c_60/2,c_61/0,c_62/1,c_63/2,c_64/0} - Obligation: innermost runtime complexity wrt. defined symbols {#ADD#,#MULT#,#NATMULT#,#PRED#,#SUCC#,#add#,#mult# ,#natmult#,#pred#,#succ#,*#,*'#,DYADE#,DYADE#1#,MULT#,MULT#1#,dyade#,dyade#1#,mult# ,mult#1#} and constructors {#0,#neg,#pos,#s,::,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c4,c5,c6,c7,c8,c9,nil} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: #add(#pos(#s(#0())),z0) -> #succ(z0) #add(#pos(#s(#s(z0))),z1) -> #succ(#add(#pos(#s(z0)),z1)) #natmult(#0(),z0) -> #0() #natmult(#s(z0),z1) -> #add(#pos(z1),#natmult(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))) #ADD#(#0(),z0) -> c_10() #ADD#(#neg(#s(#0())),z0) -> c_11(#PRED#(z0)) #ADD#(#neg(#s(#s(z0))),z1) -> c_12(#PRED#(#add(#pos(#s(z0)),z1)),#ADD#(#pos(#s(z0)),z1)) #ADD#(#pos(#s(#0())),z0) -> c_13(#SUCC#(z0)) #ADD#(#pos(#s(#s(z0))),z1) -> c_14(#SUCC#(#add(#pos(#s(z0)),z1)),#ADD#(#pos(#s(z0)),z1)) #MULT#(#0(),#0()) -> c_15() #MULT#(#0(),#neg(z0)) -> c_16() #MULT#(#0(),#pos(z0)) -> c_17() #MULT#(#neg(z0),#0()) -> c_18() #MULT#(#neg(z0),#neg(z1)) -> c_19(#NATMULT#(z0,z1)) #MULT#(#neg(z0),#pos(z1)) -> c_20(#NATMULT#(z0,z1)) #MULT#(#pos(z0),#0()) -> c_21() #MULT#(#pos(z0),#neg(z1)) -> c_22(#NATMULT#(z0,z1)) #MULT#(#pos(z0),#pos(z1)) -> c_23(#NATMULT#(z0,z1)) #NATMULT#(#0(),z0) -> c_24() #NATMULT#(#s(z0),z1) -> c_25(#ADD#(#pos(z1),#natmult(z0,z1)),#NATMULT#(z0,z1)) #PRED#(#0()) -> c_26() #PRED#(#neg(#s(z0))) -> c_27() #PRED#(#pos(#s(#0()))) -> c_28() #PRED#(#pos(#s(#s(z0)))) -> c_29() #SUCC#(#0()) -> c_30() #SUCC#(#neg(#s(#0()))) -> c_31() #SUCC#(#neg(#s(#s(z0)))) -> c_32() #SUCC#(#pos(#s(z0))) -> c_33() #add#(#0(),z0) -> c_34() #add#(#neg(#s(#0())),z0) -> c_35(#pred#(z0)) #add#(#neg(#s(#s(z0))),z1) -> c_36(#pred#(#add(#pos(#s(z0)),z1))) #add#(#pos(#s(#0())),z0) -> c_37(#succ#(z0)) #add#(#pos(#s(#s(z0))),z1) -> c_38(#succ#(#add(#pos(#s(z0)),z1))) #mult#(#0(),#0()) -> c_39() #mult#(#0(),#neg(z0)) -> c_40() #mult#(#0(),#pos(z0)) -> c_41() #mult#(#neg(z0),#0()) -> c_42() #mult#(#neg(z0),#neg(z1)) -> c_43(#natmult#(z0,z1)) #mult#(#neg(z0),#pos(z1)) -> c_44(#natmult#(z0,z1)) #mult#(#pos(z0),#0()) -> c_45() #mult#(#pos(z0),#neg(z1)) -> c_46(#natmult#(z0,z1)) #mult#(#pos(z0),#pos(z1)) -> c_47(#natmult#(z0,z1)) #natmult#(#0(),z0) -> c_48() #natmult#(#s(z0),z1) -> c_49(#add#(#pos(z1),#natmult(z0,z1))) #pred#(#0()) -> c_50() #pred#(#neg(#s(z0))) -> c_51() #pred#(#pos(#s(#0()))) -> c_52() #pred#(#pos(#s(#s(z0)))) -> c_53() #succ#(#0()) -> c_54() #succ#(#neg(#s(#0()))) -> c_55() #succ#(#neg(#s(#s(z0)))) -> c_56() #succ#(#pos(#s(z0))) -> c_57() *#(z0,z1) -> c_58(#mult#(z0,z1)) *'#(z0,z1) -> c_1(#MULT#(z0,z1)) DYADE#(z0,z1) -> c_2(DYADE#1#(z0,z1)) DYADE#1#(::(z0,z1),z2) -> c_3(MULT#(z0,z2)) DYADE#1#(::(z0,z1),z2) -> c_4(DYADE#(z1,z2)) DYADE#1#(nil(),z0) -> c_5() MULT#(z0,z1) -> c_6(MULT#1#(z1,z0)) MULT#1#(::(z0,z1),z2) -> c_7(*'#(z2,z0)) MULT#1#(::(z0,z1),z2) -> c_8(MULT#(z2,z1)) MULT#1#(nil(),z0) -> c_9() dyade#(z0,z1) -> c_59(dyade#1#(z0,z1)) dyade#1#(::(z0,z1),z2) -> c_60(mult#(z0,z2),dyade#(z1,z2)) dyade#1#(nil(),z0) -> c_61() mult#(z0,z1) -> c_62(mult#1#(z1,z0)) mult#1#(::(z0,z1),z2) -> c_63(*#(z2,z0),mult#(z2,z1)) mult#1#(nil(),z0) -> c_64() * Step 4: PredecessorEstimation. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: *'#(z0,z1) -> c_1(#MULT#(z0,z1)) DYADE#(z0,z1) -> c_2(DYADE#1#(z0,z1)) DYADE#1#(::(z0,z1),z2) -> c_3(MULT#(z0,z2)) DYADE#1#(::(z0,z1),z2) -> c_4(DYADE#(z1,z2)) DYADE#1#(nil(),z0) -> c_5() MULT#(z0,z1) -> c_6(MULT#1#(z1,z0)) MULT#1#(::(z0,z1),z2) -> c_7(*'#(z2,z0)) MULT#1#(::(z0,z1),z2) -> c_8(MULT#(z2,z1)) MULT#1#(nil(),z0) -> c_9() - Weak DPs: #ADD#(#0(),z0) -> c_10() #ADD#(#neg(#s(#0())),z0) -> c_11(#PRED#(z0)) #ADD#(#neg(#s(#s(z0))),z1) -> c_12(#PRED#(#add(#pos(#s(z0)),z1)),#ADD#(#pos(#s(z0)),z1)) #ADD#(#pos(#s(#0())),z0) -> c_13(#SUCC#(z0)) #ADD#(#pos(#s(#s(z0))),z1) -> c_14(#SUCC#(#add(#pos(#s(z0)),z1)),#ADD#(#pos(#s(z0)),z1)) #MULT#(#0(),#0()) -> c_15() #MULT#(#0(),#neg(z0)) -> c_16() #MULT#(#0(),#pos(z0)) -> c_17() #MULT#(#neg(z0),#0()) -> c_18() #MULT#(#neg(z0),#neg(z1)) -> c_19(#NATMULT#(z0,z1)) #MULT#(#neg(z0),#pos(z1)) -> c_20(#NATMULT#(z0,z1)) #MULT#(#pos(z0),#0()) -> c_21() #MULT#(#pos(z0),#neg(z1)) -> c_22(#NATMULT#(z0,z1)) #MULT#(#pos(z0),#pos(z1)) -> c_23(#NATMULT#(z0,z1)) #NATMULT#(#0(),z0) -> c_24() #NATMULT#(#s(z0),z1) -> c_25(#ADD#(#pos(z1),#natmult(z0,z1)),#NATMULT#(z0,z1)) #PRED#(#0()) -> c_26() #PRED#(#neg(#s(z0))) -> c_27() #PRED#(#pos(#s(#0()))) -> c_28() #PRED#(#pos(#s(#s(z0)))) -> c_29() #SUCC#(#0()) -> c_30() #SUCC#(#neg(#s(#0()))) -> c_31() #SUCC#(#neg(#s(#s(z0)))) -> c_32() #SUCC#(#pos(#s(z0))) -> c_33() #add#(#0(),z0) -> c_34() #add#(#neg(#s(#0())),z0) -> c_35(#pred#(z0)) #add#(#neg(#s(#s(z0))),z1) -> c_36(#pred#(#add(#pos(#s(z0)),z1))) #add#(#pos(#s(#0())),z0) -> c_37(#succ#(z0)) #add#(#pos(#s(#s(z0))),z1) -> c_38(#succ#(#add(#pos(#s(z0)),z1))) #mult#(#0(),#0()) -> c_39() #mult#(#0(),#neg(z0)) -> c_40() #mult#(#0(),#pos(z0)) -> c_41() #mult#(#neg(z0),#0()) -> c_42() #mult#(#neg(z0),#neg(z1)) -> c_43(#natmult#(z0,z1)) #mult#(#neg(z0),#pos(z1)) -> c_44(#natmult#(z0,z1)) #mult#(#pos(z0),#0()) -> c_45() #mult#(#pos(z0),#neg(z1)) -> c_46(#natmult#(z0,z1)) #mult#(#pos(z0),#pos(z1)) -> c_47(#natmult#(z0,z1)) #natmult#(#0(),z0) -> c_48() #natmult#(#s(z0),z1) -> c_49(#add#(#pos(z1),#natmult(z0,z1))) #pred#(#0()) -> c_50() #pred#(#neg(#s(z0))) -> c_51() #pred#(#pos(#s(#0()))) -> c_52() #pred#(#pos(#s(#s(z0)))) -> c_53() #succ#(#0()) -> c_54() #succ#(#neg(#s(#0()))) -> c_55() #succ#(#neg(#s(#s(z0)))) -> c_56() #succ#(#pos(#s(z0))) -> c_57() *#(z0,z1) -> c_58(#mult#(z0,z1)) dyade#(z0,z1) -> c_59(dyade#1#(z0,z1)) dyade#1#(::(z0,z1),z2) -> c_60(mult#(z0,z2),dyade#(z1,z2)) dyade#1#(nil(),z0) -> c_61() mult#(z0,z1) -> c_62(mult#1#(z1,z0)) mult#1#(::(z0,z1),z2) -> c_63(*#(z2,z0),mult#(z2,z1)) mult#1#(nil(),z0) -> c_64() - Weak TRS: #add(#pos(#s(#0())),z0) -> #succ(z0) #add(#pos(#s(#s(z0))),z1) -> #succ(#add(#pos(#s(z0)),z1)) #natmult(#0(),z0) -> #0() #natmult(#s(z0),z1) -> #add(#pos(z1),#natmult(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))) - Signature: {#ADD/2,#MULT/2,#NATMULT/2,#PRED/1,#SUCC/1,#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,*'/2,DYADE/2 ,DYADE#1/2,MULT/2,MULT#1/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,*'#/2,DYADE#/2,DYADE#1#/2,MULT#/2,MULT#1#/2,dyade#/2 ,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,c/0,c1/1,c10/1,c11/0,c12/1,c13/1,c14/0,c15/2 ,c16/0,c17/0,c18/0,c19/0,c2/2,c20/0,c21/0,c22/0,c23/0,c24/1,c25/1,c26/1,c27/1,c28/0,c29/1,c3/1,c30/1,c31/1 ,c32/0,c4/2,c5/0,c6/0,c7/0,c8/0,c9/1,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/1,c_7/1,c_8/1,c_9/0,c_10/0 ,c_11/1,c_12/2,c_13/1,c_14/2,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/0,c_22/1,c_23/1,c_24/0,c_25/2 ,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/1,c_36/1,c_37/1,c_38/1,c_39/0,c_40/0 ,c_41/0,c_42/0,c_43/1,c_44/1,c_45/0,c_46/1,c_47/1,c_48/0,c_49/1,c_50/0,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0 ,c_56/0,c_57/0,c_58/1,c_59/1,c_60/2,c_61/0,c_62/1,c_63/2,c_64/0} - Obligation: innermost runtime complexity wrt. defined symbols {#ADD#,#MULT#,#NATMULT#,#PRED#,#SUCC#,#add#,#mult# ,#natmult#,#pred#,#succ#,*#,*'#,DYADE#,DYADE#1#,MULT#,MULT#1#,dyade#,dyade#1#,mult# ,mult#1#} and constructors {#0,#neg,#pos,#s,::,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c4,c5,c6,c7,c8,c9,nil} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,5,9} by application of Pre({1,5,9}) = {2,6,7}. Here rules are labelled as follows: 1: *'#(z0,z1) -> c_1(#MULT#(z0,z1)) 2: DYADE#(z0,z1) -> c_2(DYADE#1#(z0,z1)) 3: DYADE#1#(::(z0,z1),z2) -> c_3(MULT#(z0,z2)) 4: DYADE#1#(::(z0,z1),z2) -> c_4(DYADE#(z1,z2)) 5: DYADE#1#(nil(),z0) -> c_5() 6: MULT#(z0,z1) -> c_6(MULT#1#(z1,z0)) 7: MULT#1#(::(z0,z1),z2) -> c_7(*'#(z2,z0)) 8: MULT#1#(::(z0,z1),z2) -> c_8(MULT#(z2,z1)) 9: MULT#1#(nil(),z0) -> c_9() 10: #ADD#(#0(),z0) -> c_10() 11: #ADD#(#neg(#s(#0())),z0) -> c_11(#PRED#(z0)) 12: #ADD#(#neg(#s(#s(z0))),z1) -> c_12(#PRED#(#add(#pos(#s(z0)),z1)),#ADD#(#pos(#s(z0)),z1)) 13: #ADD#(#pos(#s(#0())),z0) -> c_13(#SUCC#(z0)) 14: #ADD#(#pos(#s(#s(z0))),z1) -> c_14(#SUCC#(#add(#pos(#s(z0)),z1)),#ADD#(#pos(#s(z0)),z1)) 15: #MULT#(#0(),#0()) -> c_15() 16: #MULT#(#0(),#neg(z0)) -> c_16() 17: #MULT#(#0(),#pos(z0)) -> c_17() 18: #MULT#(#neg(z0),#0()) -> c_18() 19: #MULT#(#neg(z0),#neg(z1)) -> c_19(#NATMULT#(z0,z1)) 20: #MULT#(#neg(z0),#pos(z1)) -> c_20(#NATMULT#(z0,z1)) 21: #MULT#(#pos(z0),#0()) -> c_21() 22: #MULT#(#pos(z0),#neg(z1)) -> c_22(#NATMULT#(z0,z1)) 23: #MULT#(#pos(z0),#pos(z1)) -> c_23(#NATMULT#(z0,z1)) 24: #NATMULT#(#0(),z0) -> c_24() 25: #NATMULT#(#s(z0),z1) -> c_25(#ADD#(#pos(z1),#natmult(z0,z1)),#NATMULT#(z0,z1)) 26: #PRED#(#0()) -> c_26() 27: #PRED#(#neg(#s(z0))) -> c_27() 28: #PRED#(#pos(#s(#0()))) -> c_28() 29: #PRED#(#pos(#s(#s(z0)))) -> c_29() 30: #SUCC#(#0()) -> c_30() 31: #SUCC#(#neg(#s(#0()))) -> c_31() 32: #SUCC#(#neg(#s(#s(z0)))) -> c_32() 33: #SUCC#(#pos(#s(z0))) -> c_33() 34: #add#(#0(),z0) -> c_34() 35: #add#(#neg(#s(#0())),z0) -> c_35(#pred#(z0)) 36: #add#(#neg(#s(#s(z0))),z1) -> c_36(#pred#(#add(#pos(#s(z0)),z1))) 37: #add#(#pos(#s(#0())),z0) -> c_37(#succ#(z0)) 38: #add#(#pos(#s(#s(z0))),z1) -> c_38(#succ#(#add(#pos(#s(z0)),z1))) 39: #mult#(#0(),#0()) -> c_39() 40: #mult#(#0(),#neg(z0)) -> c_40() 41: #mult#(#0(),#pos(z0)) -> c_41() 42: #mult#(#neg(z0),#0()) -> c_42() 43: #mult#(#neg(z0),#neg(z1)) -> c_43(#natmult#(z0,z1)) 44: #mult#(#neg(z0),#pos(z1)) -> c_44(#natmult#(z0,z1)) 45: #mult#(#pos(z0),#0()) -> c_45() 46: #mult#(#pos(z0),#neg(z1)) -> c_46(#natmult#(z0,z1)) 47: #mult#(#pos(z0),#pos(z1)) -> c_47(#natmult#(z0,z1)) 48: #natmult#(#0(),z0) -> c_48() 49: #natmult#(#s(z0),z1) -> c_49(#add#(#pos(z1),#natmult(z0,z1))) 50: #pred#(#0()) -> c_50() 51: #pred#(#neg(#s(z0))) -> c_51() 52: #pred#(#pos(#s(#0()))) -> c_52() 53: #pred#(#pos(#s(#s(z0)))) -> c_53() 54: #succ#(#0()) -> c_54() 55: #succ#(#neg(#s(#0()))) -> c_55() 56: #succ#(#neg(#s(#s(z0)))) -> c_56() 57: #succ#(#pos(#s(z0))) -> c_57() 58: *#(z0,z1) -> c_58(#mult#(z0,z1)) 59: dyade#(z0,z1) -> c_59(dyade#1#(z0,z1)) 60: dyade#1#(::(z0,z1),z2) -> c_60(mult#(z0,z2),dyade#(z1,z2)) 61: dyade#1#(nil(),z0) -> c_61() 62: mult#(z0,z1) -> c_62(mult#1#(z1,z0)) 63: mult#1#(::(z0,z1),z2) -> c_63(*#(z2,z0),mult#(z2,z1)) 64: mult#1#(nil(),z0) -> c_64() * Step 5: PredecessorEstimation. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: DYADE#(z0,z1) -> c_2(DYADE#1#(z0,z1)) DYADE#1#(::(z0,z1),z2) -> c_3(MULT#(z0,z2)) DYADE#1#(::(z0,z1),z2) -> c_4(DYADE#(z1,z2)) MULT#(z0,z1) -> c_6(MULT#1#(z1,z0)) MULT#1#(::(z0,z1),z2) -> c_7(*'#(z2,z0)) MULT#1#(::(z0,z1),z2) -> c_8(MULT#(z2,z1)) - Weak DPs: #ADD#(#0(),z0) -> c_10() #ADD#(#neg(#s(#0())),z0) -> c_11(#PRED#(z0)) #ADD#(#neg(#s(#s(z0))),z1) -> c_12(#PRED#(#add(#pos(#s(z0)),z1)),#ADD#(#pos(#s(z0)),z1)) #ADD#(#pos(#s(#0())),z0) -> c_13(#SUCC#(z0)) #ADD#(#pos(#s(#s(z0))),z1) -> c_14(#SUCC#(#add(#pos(#s(z0)),z1)),#ADD#(#pos(#s(z0)),z1)) #MULT#(#0(),#0()) -> c_15() #MULT#(#0(),#neg(z0)) -> c_16() #MULT#(#0(),#pos(z0)) -> c_17() #MULT#(#neg(z0),#0()) -> c_18() #MULT#(#neg(z0),#neg(z1)) -> c_19(#NATMULT#(z0,z1)) #MULT#(#neg(z0),#pos(z1)) -> c_20(#NATMULT#(z0,z1)) #MULT#(#pos(z0),#0()) -> c_21() #MULT#(#pos(z0),#neg(z1)) -> c_22(#NATMULT#(z0,z1)) #MULT#(#pos(z0),#pos(z1)) -> c_23(#NATMULT#(z0,z1)) #NATMULT#(#0(),z0) -> c_24() #NATMULT#(#s(z0),z1) -> c_25(#ADD#(#pos(z1),#natmult(z0,z1)),#NATMULT#(z0,z1)) #PRED#(#0()) -> c_26() #PRED#(#neg(#s(z0))) -> c_27() #PRED#(#pos(#s(#0()))) -> c_28() #PRED#(#pos(#s(#s(z0)))) -> c_29() #SUCC#(#0()) -> c_30() #SUCC#(#neg(#s(#0()))) -> c_31() #SUCC#(#neg(#s(#s(z0)))) -> c_32() #SUCC#(#pos(#s(z0))) -> c_33() #add#(#0(),z0) -> c_34() #add#(#neg(#s(#0())),z0) -> c_35(#pred#(z0)) #add#(#neg(#s(#s(z0))),z1) -> c_36(#pred#(#add(#pos(#s(z0)),z1))) #add#(#pos(#s(#0())),z0) -> c_37(#succ#(z0)) #add#(#pos(#s(#s(z0))),z1) -> c_38(#succ#(#add(#pos(#s(z0)),z1))) #mult#(#0(),#0()) -> c_39() #mult#(#0(),#neg(z0)) -> c_40() #mult#(#0(),#pos(z0)) -> c_41() #mult#(#neg(z0),#0()) -> c_42() #mult#(#neg(z0),#neg(z1)) -> c_43(#natmult#(z0,z1)) #mult#(#neg(z0),#pos(z1)) -> c_44(#natmult#(z0,z1)) #mult#(#pos(z0),#0()) -> c_45() #mult#(#pos(z0),#neg(z1)) -> c_46(#natmult#(z0,z1)) #mult#(#pos(z0),#pos(z1)) -> c_47(#natmult#(z0,z1)) #natmult#(#0(),z0) -> c_48() #natmult#(#s(z0),z1) -> c_49(#add#(#pos(z1),#natmult(z0,z1))) #pred#(#0()) -> c_50() #pred#(#neg(#s(z0))) -> c_51() #pred#(#pos(#s(#0()))) -> c_52() #pred#(#pos(#s(#s(z0)))) -> c_53() #succ#(#0()) -> c_54() #succ#(#neg(#s(#0()))) -> c_55() #succ#(#neg(#s(#s(z0)))) -> c_56() #succ#(#pos(#s(z0))) -> c_57() *#(z0,z1) -> c_58(#mult#(z0,z1)) *'#(z0,z1) -> c_1(#MULT#(z0,z1)) DYADE#1#(nil(),z0) -> c_5() MULT#1#(nil(),z0) -> c_9() dyade#(z0,z1) -> c_59(dyade#1#(z0,z1)) dyade#1#(::(z0,z1),z2) -> c_60(mult#(z0,z2),dyade#(z1,z2)) dyade#1#(nil(),z0) -> c_61() mult#(z0,z1) -> c_62(mult#1#(z1,z0)) mult#1#(::(z0,z1),z2) -> c_63(*#(z2,z0),mult#(z2,z1)) mult#1#(nil(),z0) -> c_64() - Weak TRS: #add(#pos(#s(#0())),z0) -> #succ(z0) #add(#pos(#s(#s(z0))),z1) -> #succ(#add(#pos(#s(z0)),z1)) #natmult(#0(),z0) -> #0() #natmult(#s(z0),z1) -> #add(#pos(z1),#natmult(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))) - Signature: {#ADD/2,#MULT/2,#NATMULT/2,#PRED/1,#SUCC/1,#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,*'/2,DYADE/2 ,DYADE#1/2,MULT/2,MULT#1/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,*'#/2,DYADE#/2,DYADE#1#/2,MULT#/2,MULT#1#/2,dyade#/2 ,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,c/0,c1/1,c10/1,c11/0,c12/1,c13/1,c14/0,c15/2 ,c16/0,c17/0,c18/0,c19/0,c2/2,c20/0,c21/0,c22/0,c23/0,c24/1,c25/1,c26/1,c27/1,c28/0,c29/1,c3/1,c30/1,c31/1 ,c32/0,c4/2,c5/0,c6/0,c7/0,c8/0,c9/1,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/1,c_7/1,c_8/1,c_9/0,c_10/0 ,c_11/1,c_12/2,c_13/1,c_14/2,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/0,c_22/1,c_23/1,c_24/0,c_25/2 ,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/1,c_36/1,c_37/1,c_38/1,c_39/0,c_40/0 ,c_41/0,c_42/0,c_43/1,c_44/1,c_45/0,c_46/1,c_47/1,c_48/0,c_49/1,c_50/0,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0 ,c_56/0,c_57/0,c_58/1,c_59/1,c_60/2,c_61/0,c_62/1,c_63/2,c_64/0} - Obligation: innermost runtime complexity wrt. defined symbols {#ADD#,#MULT#,#NATMULT#,#PRED#,#SUCC#,#add#,#mult# ,#natmult#,#pred#,#succ#,*#,*'#,DYADE#,DYADE#1#,MULT#,MULT#1#,dyade#,dyade#1#,mult# ,mult#1#} and constructors {#0,#neg,#pos,#s,::,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c4,c5,c6,c7,c8,c9,nil} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {5} by application of Pre({5}) = {4}. Here rules are labelled as follows: 1: DYADE#(z0,z1) -> c_2(DYADE#1#(z0,z1)) 2: DYADE#1#(::(z0,z1),z2) -> c_3(MULT#(z0,z2)) 3: DYADE#1#(::(z0,z1),z2) -> c_4(DYADE#(z1,z2)) 4: MULT#(z0,z1) -> c_6(MULT#1#(z1,z0)) 5: MULT#1#(::(z0,z1),z2) -> c_7(*'#(z2,z0)) 6: MULT#1#(::(z0,z1),z2) -> c_8(MULT#(z2,z1)) 7: #ADD#(#0(),z0) -> c_10() 8: #ADD#(#neg(#s(#0())),z0) -> c_11(#PRED#(z0)) 9: #ADD#(#neg(#s(#s(z0))),z1) -> c_12(#PRED#(#add(#pos(#s(z0)),z1)),#ADD#(#pos(#s(z0)),z1)) 10: #ADD#(#pos(#s(#0())),z0) -> c_13(#SUCC#(z0)) 11: #ADD#(#pos(#s(#s(z0))),z1) -> c_14(#SUCC#(#add(#pos(#s(z0)),z1)),#ADD#(#pos(#s(z0)),z1)) 12: #MULT#(#0(),#0()) -> c_15() 13: #MULT#(#0(),#neg(z0)) -> c_16() 14: #MULT#(#0(),#pos(z0)) -> c_17() 15: #MULT#(#neg(z0),#0()) -> c_18() 16: #MULT#(#neg(z0),#neg(z1)) -> c_19(#NATMULT#(z0,z1)) 17: #MULT#(#neg(z0),#pos(z1)) -> c_20(#NATMULT#(z0,z1)) 18: #MULT#(#pos(z0),#0()) -> c_21() 19: #MULT#(#pos(z0),#neg(z1)) -> c_22(#NATMULT#(z0,z1)) 20: #MULT#(#pos(z0),#pos(z1)) -> c_23(#NATMULT#(z0,z1)) 21: #NATMULT#(#0(),z0) -> c_24() 22: #NATMULT#(#s(z0),z1) -> c_25(#ADD#(#pos(z1),#natmult(z0,z1)),#NATMULT#(z0,z1)) 23: #PRED#(#0()) -> c_26() 24: #PRED#(#neg(#s(z0))) -> c_27() 25: #PRED#(#pos(#s(#0()))) -> c_28() 26: #PRED#(#pos(#s(#s(z0)))) -> c_29() 27: #SUCC#(#0()) -> c_30() 28: #SUCC#(#neg(#s(#0()))) -> c_31() 29: #SUCC#(#neg(#s(#s(z0)))) -> c_32() 30: #SUCC#(#pos(#s(z0))) -> c_33() 31: #add#(#0(),z0) -> c_34() 32: #add#(#neg(#s(#0())),z0) -> c_35(#pred#(z0)) 33: #add#(#neg(#s(#s(z0))),z1) -> c_36(#pred#(#add(#pos(#s(z0)),z1))) 34: #add#(#pos(#s(#0())),z0) -> c_37(#succ#(z0)) 35: #add#(#pos(#s(#s(z0))),z1) -> c_38(#succ#(#add(#pos(#s(z0)),z1))) 36: #mult#(#0(),#0()) -> c_39() 37: #mult#(#0(),#neg(z0)) -> c_40() 38: #mult#(#0(),#pos(z0)) -> c_41() 39: #mult#(#neg(z0),#0()) -> c_42() 40: #mult#(#neg(z0),#neg(z1)) -> c_43(#natmult#(z0,z1)) 41: #mult#(#neg(z0),#pos(z1)) -> c_44(#natmult#(z0,z1)) 42: #mult#(#pos(z0),#0()) -> c_45() 43: #mult#(#pos(z0),#neg(z1)) -> c_46(#natmult#(z0,z1)) 44: #mult#(#pos(z0),#pos(z1)) -> c_47(#natmult#(z0,z1)) 45: #natmult#(#0(),z0) -> c_48() 46: #natmult#(#s(z0),z1) -> c_49(#add#(#pos(z1),#natmult(z0,z1))) 47: #pred#(#0()) -> c_50() 48: #pred#(#neg(#s(z0))) -> c_51() 49: #pred#(#pos(#s(#0()))) -> c_52() 50: #pred#(#pos(#s(#s(z0)))) -> c_53() 51: #succ#(#0()) -> c_54() 52: #succ#(#neg(#s(#0()))) -> c_55() 53: #succ#(#neg(#s(#s(z0)))) -> c_56() 54: #succ#(#pos(#s(z0))) -> c_57() 55: *#(z0,z1) -> c_58(#mult#(z0,z1)) 56: *'#(z0,z1) -> c_1(#MULT#(z0,z1)) 57: DYADE#1#(nil(),z0) -> c_5() 58: MULT#1#(nil(),z0) -> c_9() 59: dyade#(z0,z1) -> c_59(dyade#1#(z0,z1)) 60: dyade#1#(::(z0,z1),z2) -> c_60(mult#(z0,z2),dyade#(z1,z2)) 61: dyade#1#(nil(),z0) -> c_61() 62: mult#(z0,z1) -> c_62(mult#1#(z1,z0)) 63: mult#1#(::(z0,z1),z2) -> c_63(*#(z2,z0),mult#(z2,z1)) 64: mult#1#(nil(),z0) -> c_64() * Step 6: RemoveWeakSuffixes. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: DYADE#(z0,z1) -> c_2(DYADE#1#(z0,z1)) DYADE#1#(::(z0,z1),z2) -> c_3(MULT#(z0,z2)) DYADE#1#(::(z0,z1),z2) -> c_4(DYADE#(z1,z2)) MULT#(z0,z1) -> c_6(MULT#1#(z1,z0)) MULT#1#(::(z0,z1),z2) -> c_8(MULT#(z2,z1)) - Weak DPs: #ADD#(#0(),z0) -> c_10() #ADD#(#neg(#s(#0())),z0) -> c_11(#PRED#(z0)) #ADD#(#neg(#s(#s(z0))),z1) -> c_12(#PRED#(#add(#pos(#s(z0)),z1)),#ADD#(#pos(#s(z0)),z1)) #ADD#(#pos(#s(#0())),z0) -> c_13(#SUCC#(z0)) #ADD#(#pos(#s(#s(z0))),z1) -> c_14(#SUCC#(#add(#pos(#s(z0)),z1)),#ADD#(#pos(#s(z0)),z1)) #MULT#(#0(),#0()) -> c_15() #MULT#(#0(),#neg(z0)) -> c_16() #MULT#(#0(),#pos(z0)) -> c_17() #MULT#(#neg(z0),#0()) -> c_18() #MULT#(#neg(z0),#neg(z1)) -> c_19(#NATMULT#(z0,z1)) #MULT#(#neg(z0),#pos(z1)) -> c_20(#NATMULT#(z0,z1)) #MULT#(#pos(z0),#0()) -> c_21() #MULT#(#pos(z0),#neg(z1)) -> c_22(#NATMULT#(z0,z1)) #MULT#(#pos(z0),#pos(z1)) -> c_23(#NATMULT#(z0,z1)) #NATMULT#(#0(),z0) -> c_24() #NATMULT#(#s(z0),z1) -> c_25(#ADD#(#pos(z1),#natmult(z0,z1)),#NATMULT#(z0,z1)) #PRED#(#0()) -> c_26() #PRED#(#neg(#s(z0))) -> c_27() #PRED#(#pos(#s(#0()))) -> c_28() #PRED#(#pos(#s(#s(z0)))) -> c_29() #SUCC#(#0()) -> c_30() #SUCC#(#neg(#s(#0()))) -> c_31() #SUCC#(#neg(#s(#s(z0)))) -> c_32() #SUCC#(#pos(#s(z0))) -> c_33() #add#(#0(),z0) -> c_34() #add#(#neg(#s(#0())),z0) -> c_35(#pred#(z0)) #add#(#neg(#s(#s(z0))),z1) -> c_36(#pred#(#add(#pos(#s(z0)),z1))) #add#(#pos(#s(#0())),z0) -> c_37(#succ#(z0)) #add#(#pos(#s(#s(z0))),z1) -> c_38(#succ#(#add(#pos(#s(z0)),z1))) #mult#(#0(),#0()) -> c_39() #mult#(#0(),#neg(z0)) -> c_40() #mult#(#0(),#pos(z0)) -> c_41() #mult#(#neg(z0),#0()) -> c_42() #mult#(#neg(z0),#neg(z1)) -> c_43(#natmult#(z0,z1)) #mult#(#neg(z0),#pos(z1)) -> c_44(#natmult#(z0,z1)) #mult#(#pos(z0),#0()) -> c_45() #mult#(#pos(z0),#neg(z1)) -> c_46(#natmult#(z0,z1)) #mult#(#pos(z0),#pos(z1)) -> c_47(#natmult#(z0,z1)) #natmult#(#0(),z0) -> c_48() #natmult#(#s(z0),z1) -> c_49(#add#(#pos(z1),#natmult(z0,z1))) #pred#(#0()) -> c_50() #pred#(#neg(#s(z0))) -> c_51() #pred#(#pos(#s(#0()))) -> c_52() #pred#(#pos(#s(#s(z0)))) -> c_53() #succ#(#0()) -> c_54() #succ#(#neg(#s(#0()))) -> c_55() #succ#(#neg(#s(#s(z0)))) -> c_56() #succ#(#pos(#s(z0))) -> c_57() *#(z0,z1) -> c_58(#mult#(z0,z1)) *'#(z0,z1) -> c_1(#MULT#(z0,z1)) DYADE#1#(nil(),z0) -> c_5() MULT#1#(::(z0,z1),z2) -> c_7(*'#(z2,z0)) MULT#1#(nil(),z0) -> c_9() dyade#(z0,z1) -> c_59(dyade#1#(z0,z1)) dyade#1#(::(z0,z1),z2) -> c_60(mult#(z0,z2),dyade#(z1,z2)) dyade#1#(nil(),z0) -> c_61() mult#(z0,z1) -> c_62(mult#1#(z1,z0)) mult#1#(::(z0,z1),z2) -> c_63(*#(z2,z0),mult#(z2,z1)) mult#1#(nil(),z0) -> c_64() - Weak TRS: #add(#pos(#s(#0())),z0) -> #succ(z0) #add(#pos(#s(#s(z0))),z1) -> #succ(#add(#pos(#s(z0)),z1)) #natmult(#0(),z0) -> #0() #natmult(#s(z0),z1) -> #add(#pos(z1),#natmult(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))) - Signature: {#ADD/2,#MULT/2,#NATMULT/2,#PRED/1,#SUCC/1,#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,*'/2,DYADE/2 ,DYADE#1/2,MULT/2,MULT#1/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,*'#/2,DYADE#/2,DYADE#1#/2,MULT#/2,MULT#1#/2,dyade#/2 ,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,c/0,c1/1,c10/1,c11/0,c12/1,c13/1,c14/0,c15/2 ,c16/0,c17/0,c18/0,c19/0,c2/2,c20/0,c21/0,c22/0,c23/0,c24/1,c25/1,c26/1,c27/1,c28/0,c29/1,c3/1,c30/1,c31/1 ,c32/0,c4/2,c5/0,c6/0,c7/0,c8/0,c9/1,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/1,c_7/1,c_8/1,c_9/0,c_10/0 ,c_11/1,c_12/2,c_13/1,c_14/2,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/0,c_22/1,c_23/1,c_24/0,c_25/2 ,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/1,c_36/1,c_37/1,c_38/1,c_39/0,c_40/0 ,c_41/0,c_42/0,c_43/1,c_44/1,c_45/0,c_46/1,c_47/1,c_48/0,c_49/1,c_50/0,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0 ,c_56/0,c_57/0,c_58/1,c_59/1,c_60/2,c_61/0,c_62/1,c_63/2,c_64/0} - Obligation: innermost runtime complexity wrt. defined symbols {#ADD#,#MULT#,#NATMULT#,#PRED#,#SUCC#,#add#,#mult# ,#natmult#,#pred#,#succ#,*#,*'#,DYADE#,DYADE#1#,MULT#,MULT#1#,dyade#,dyade#1#,mult# ,mult#1#} and constructors {#0,#neg,#pos,#s,::,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c4,c5,c6,c7,c8,c9,nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:DYADE#(z0,z1) -> c_2(DYADE#1#(z0,z1)) -->_1 DYADE#1#(::(z0,z1),z2) -> c_4(DYADE#(z1,z2)):3 -->_1 DYADE#1#(::(z0,z1),z2) -> c_3(MULT#(z0,z2)):2 -->_1 DYADE#1#(nil(),z0) -> c_5():56 2:S:DYADE#1#(::(z0,z1),z2) -> c_3(MULT#(z0,z2)) -->_1 MULT#(z0,z1) -> c_6(MULT#1#(z1,z0)):4 3:S:DYADE#1#(::(z0,z1),z2) -> c_4(DYADE#(z1,z2)) -->_1 DYADE#(z0,z1) -> c_2(DYADE#1#(z0,z1)):1 4:S:MULT#(z0,z1) -> c_6(MULT#1#(z1,z0)) -->_1 MULT#1#(::(z0,z1),z2) -> c_7(*'#(z2,z0)):57 -->_1 MULT#1#(::(z0,z1),z2) -> c_8(MULT#(z2,z1)):5 -->_1 MULT#1#(nil(),z0) -> c_9():58 5:S:MULT#1#(::(z0,z1),z2) -> c_8(MULT#(z2,z1)) -->_1 MULT#(z0,z1) -> c_6(MULT#1#(z1,z0)):4 6:W:#ADD#(#0(),z0) -> c_10() 7:W:#ADD#(#neg(#s(#0())),z0) -> c_11(#PRED#(z0)) -->_1 #PRED#(#pos(#s(#s(z0)))) -> c_29():25 -->_1 #PRED#(#pos(#s(#0()))) -> c_28():24 -->_1 #PRED#(#neg(#s(z0))) -> c_27():23 -->_1 #PRED#(#0()) -> c_26():22 8:W:#ADD#(#neg(#s(#s(z0))),z1) -> c_12(#PRED#(#add(#pos(#s(z0)),z1)),#ADD#(#pos(#s(z0)),z1)) -->_2 #ADD#(#pos(#s(#s(z0))),z1) -> c_14(#SUCC#(#add(#pos(#s(z0)),z1)),#ADD#(#pos(#s(z0)),z1)):10 -->_2 #ADD#(#pos(#s(#0())),z0) -> c_13(#SUCC#(z0)):9 -->_1 #PRED#(#pos(#s(#s(z0)))) -> c_29():25 -->_1 #PRED#(#pos(#s(#0()))) -> c_28():24 -->_1 #PRED#(#neg(#s(z0))) -> c_27():23 -->_1 #PRED#(#0()) -> c_26():22 9:W:#ADD#(#pos(#s(#0())),z0) -> c_13(#SUCC#(z0)) -->_1 #SUCC#(#pos(#s(z0))) -> c_33():29 -->_1 #SUCC#(#neg(#s(#s(z0)))) -> c_32():28 -->_1 #SUCC#(#neg(#s(#0()))) -> c_31():27 -->_1 #SUCC#(#0()) -> c_30():26 10:W:#ADD#(#pos(#s(#s(z0))),z1) -> c_14(#SUCC#(#add(#pos(#s(z0)),z1)),#ADD#(#pos(#s(z0)),z1)) -->_1 #SUCC#(#pos(#s(z0))) -> c_33():29 -->_1 #SUCC#(#neg(#s(#s(z0)))) -> c_32():28 -->_1 #SUCC#(#neg(#s(#0()))) -> c_31():27 -->_1 #SUCC#(#0()) -> c_30():26 -->_2 #ADD#(#pos(#s(#s(z0))),z1) -> c_14(#SUCC#(#add(#pos(#s(z0)),z1)),#ADD#(#pos(#s(z0)),z1)):10 -->_2 #ADD#(#pos(#s(#0())),z0) -> c_13(#SUCC#(z0)):9 11:W:#MULT#(#0(),#0()) -> c_15() 12:W:#MULT#(#0(),#neg(z0)) -> c_16() 13:W:#MULT#(#0(),#pos(z0)) -> c_17() 14:W:#MULT#(#neg(z0),#0()) -> c_18() 15:W:#MULT#(#neg(z0),#neg(z1)) -> c_19(#NATMULT#(z0,z1)) -->_1 #NATMULT#(#s(z0),z1) -> c_25(#ADD#(#pos(z1),#natmult(z0,z1)),#NATMULT#(z0,z1)):21 -->_1 #NATMULT#(#0(),z0) -> c_24():20 16:W:#MULT#(#neg(z0),#pos(z1)) -> c_20(#NATMULT#(z0,z1)) -->_1 #NATMULT#(#s(z0),z1) -> c_25(#ADD#(#pos(z1),#natmult(z0,z1)),#NATMULT#(z0,z1)):21 -->_1 #NATMULT#(#0(),z0) -> c_24():20 17:W:#MULT#(#pos(z0),#0()) -> c_21() 18:W:#MULT#(#pos(z0),#neg(z1)) -> c_22(#NATMULT#(z0,z1)) -->_1 #NATMULT#(#s(z0),z1) -> c_25(#ADD#(#pos(z1),#natmult(z0,z1)),#NATMULT#(z0,z1)):21 -->_1 #NATMULT#(#0(),z0) -> c_24():20 19:W:#MULT#(#pos(z0),#pos(z1)) -> c_23(#NATMULT#(z0,z1)) -->_1 #NATMULT#(#s(z0),z1) -> c_25(#ADD#(#pos(z1),#natmult(z0,z1)),#NATMULT#(z0,z1)):21 -->_1 #NATMULT#(#0(),z0) -> c_24():20 20:W:#NATMULT#(#0(),z0) -> c_24() 21:W:#NATMULT#(#s(z0),z1) -> c_25(#ADD#(#pos(z1),#natmult(z0,z1)),#NATMULT#(z0,z1)) -->_2 #NATMULT#(#s(z0),z1) -> c_25(#ADD#(#pos(z1),#natmult(z0,z1)),#NATMULT#(z0,z1)):21 -->_2 #NATMULT#(#0(),z0) -> c_24():20 -->_1 #ADD#(#pos(#s(#s(z0))),z1) -> c_14(#SUCC#(#add(#pos(#s(z0)),z1)),#ADD#(#pos(#s(z0)),z1)):10 -->_1 #ADD#(#pos(#s(#0())),z0) -> c_13(#SUCC#(z0)):9 22:W:#PRED#(#0()) -> c_26() 23:W:#PRED#(#neg(#s(z0))) -> c_27() 24:W:#PRED#(#pos(#s(#0()))) -> c_28() 25:W:#PRED#(#pos(#s(#s(z0)))) -> c_29() 26:W:#SUCC#(#0()) -> c_30() 27:W:#SUCC#(#neg(#s(#0()))) -> c_31() 28:W:#SUCC#(#neg(#s(#s(z0)))) -> c_32() 29:W:#SUCC#(#pos(#s(z0))) -> c_33() 30:W:#add#(#0(),z0) -> c_34() 31:W:#add#(#neg(#s(#0())),z0) -> c_35(#pred#(z0)) -->_1 #pred#(#pos(#s(#s(z0)))) -> c_53():49 -->_1 #pred#(#pos(#s(#0()))) -> c_52():48 -->_1 #pred#(#neg(#s(z0))) -> c_51():47 -->_1 #pred#(#0()) -> c_50():46 32:W:#add#(#neg(#s(#s(z0))),z1) -> c_36(#pred#(#add(#pos(#s(z0)),z1))) -->_1 #pred#(#pos(#s(#s(z0)))) -> c_53():49 -->_1 #pred#(#pos(#s(#0()))) -> c_52():48 -->_1 #pred#(#neg(#s(z0))) -> c_51():47 -->_1 #pred#(#0()) -> c_50():46 33:W:#add#(#pos(#s(#0())),z0) -> c_37(#succ#(z0)) -->_1 #succ#(#pos(#s(z0))) -> c_57():53 -->_1 #succ#(#neg(#s(#s(z0)))) -> c_56():52 -->_1 #succ#(#neg(#s(#0()))) -> c_55():51 -->_1 #succ#(#0()) -> c_54():50 34:W:#add#(#pos(#s(#s(z0))),z1) -> c_38(#succ#(#add(#pos(#s(z0)),z1))) -->_1 #succ#(#pos(#s(z0))) -> c_57():53 -->_1 #succ#(#neg(#s(#s(z0)))) -> c_56():52 -->_1 #succ#(#neg(#s(#0()))) -> c_55():51 -->_1 #succ#(#0()) -> c_54():50 35:W:#mult#(#0(),#0()) -> c_39() 36:W:#mult#(#0(),#neg(z0)) -> c_40() 37:W:#mult#(#0(),#pos(z0)) -> c_41() 38:W:#mult#(#neg(z0),#0()) -> c_42() 39:W:#mult#(#neg(z0),#neg(z1)) -> c_43(#natmult#(z0,z1)) -->_1 #natmult#(#s(z0),z1) -> c_49(#add#(#pos(z1),#natmult(z0,z1))):45 -->_1 #natmult#(#0(),z0) -> c_48():44 40:W:#mult#(#neg(z0),#pos(z1)) -> c_44(#natmult#(z0,z1)) -->_1 #natmult#(#s(z0),z1) -> c_49(#add#(#pos(z1),#natmult(z0,z1))):45 -->_1 #natmult#(#0(),z0) -> c_48():44 41:W:#mult#(#pos(z0),#0()) -> c_45() 42:W:#mult#(#pos(z0),#neg(z1)) -> c_46(#natmult#(z0,z1)) -->_1 #natmult#(#s(z0),z1) -> c_49(#add#(#pos(z1),#natmult(z0,z1))):45 -->_1 #natmult#(#0(),z0) -> c_48():44 43:W:#mult#(#pos(z0),#pos(z1)) -> c_47(#natmult#(z0,z1)) -->_1 #natmult#(#s(z0),z1) -> c_49(#add#(#pos(z1),#natmult(z0,z1))):45 -->_1 #natmult#(#0(),z0) -> c_48():44 44:W:#natmult#(#0(),z0) -> c_48() 45:W:#natmult#(#s(z0),z1) -> c_49(#add#(#pos(z1),#natmult(z0,z1))) -->_1 #add#(#pos(#s(#s(z0))),z1) -> c_38(#succ#(#add(#pos(#s(z0)),z1))):34 -->_1 #add#(#pos(#s(#0())),z0) -> c_37(#succ#(z0)):33 46:W:#pred#(#0()) -> c_50() 47:W:#pred#(#neg(#s(z0))) -> c_51() 48:W:#pred#(#pos(#s(#0()))) -> c_52() 49:W:#pred#(#pos(#s(#s(z0)))) -> c_53() 50:W:#succ#(#0()) -> c_54() 51:W:#succ#(#neg(#s(#0()))) -> c_55() 52:W:#succ#(#neg(#s(#s(z0)))) -> c_56() 53:W:#succ#(#pos(#s(z0))) -> c_57() 54:W:*#(z0,z1) -> c_58(#mult#(z0,z1)) -->_1 #mult#(#pos(z0),#pos(z1)) -> c_47(#natmult#(z0,z1)):43 -->_1 #mult#(#pos(z0),#neg(z1)) -> c_46(#natmult#(z0,z1)):42 -->_1 #mult#(#pos(z0),#0()) -> c_45():41 -->_1 #mult#(#neg(z0),#pos(z1)) -> c_44(#natmult#(z0,z1)):40 -->_1 #mult#(#neg(z0),#neg(z1)) -> c_43(#natmult#(z0,z1)):39 -->_1 #mult#(#neg(z0),#0()) -> c_42():38 -->_1 #mult#(#0(),#pos(z0)) -> c_41():37 -->_1 #mult#(#0(),#neg(z0)) -> c_40():36 -->_1 #mult#(#0(),#0()) -> c_39():35 55:W:*'#(z0,z1) -> c_1(#MULT#(z0,z1)) -->_1 #MULT#(#pos(z0),#pos(z1)) -> c_23(#NATMULT#(z0,z1)):19 -->_1 #MULT#(#pos(z0),#neg(z1)) -> c_22(#NATMULT#(z0,z1)):18 -->_1 #MULT#(#pos(z0),#0()) -> c_21():17 -->_1 #MULT#(#neg(z0),#pos(z1)) -> c_20(#NATMULT#(z0,z1)):16 -->_1 #MULT#(#neg(z0),#neg(z1)) -> c_19(#NATMULT#(z0,z1)):15 -->_1 #MULT#(#neg(z0),#0()) -> c_18():14 -->_1 #MULT#(#0(),#pos(z0)) -> c_17():13 -->_1 #MULT#(#0(),#neg(z0)) -> c_16():12 -->_1 #MULT#(#0(),#0()) -> c_15():11 56:W:DYADE#1#(nil(),z0) -> c_5() 57:W:MULT#1#(::(z0,z1),z2) -> c_7(*'#(z2,z0)) -->_1 *'#(z0,z1) -> c_1(#MULT#(z0,z1)):55 58:W:MULT#1#(nil(),z0) -> c_9() 59:W:dyade#(z0,z1) -> c_59(dyade#1#(z0,z1)) -->_1 dyade#1#(::(z0,z1),z2) -> c_60(mult#(z0,z2),dyade#(z1,z2)):60 -->_1 dyade#1#(nil(),z0) -> c_61():61 60:W:dyade#1#(::(z0,z1),z2) -> c_60(mult#(z0,z2),dyade#(z1,z2)) -->_1 mult#(z0,z1) -> c_62(mult#1#(z1,z0)):62 -->_2 dyade#(z0,z1) -> c_59(dyade#1#(z0,z1)):59 61:W:dyade#1#(nil(),z0) -> c_61() 62:W:mult#(z0,z1) -> c_62(mult#1#(z1,z0)) -->_1 mult#1#(::(z0,z1),z2) -> c_63(*#(z2,z0),mult#(z2,z1)):63 -->_1 mult#1#(nil(),z0) -> c_64():64 63:W:mult#1#(::(z0,z1),z2) -> c_63(*#(z2,z0),mult#(z2,z1)) -->_2 mult#(z0,z1) -> c_62(mult#1#(z1,z0)):62 -->_1 *#(z0,z1) -> c_58(#mult#(z0,z1)):54 64:W:mult#1#(nil(),z0) -> c_64() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 59: dyade#(z0,z1) -> c_59(dyade#1#(z0,z1)) 60: dyade#1#(::(z0,z1),z2) -> c_60(mult#(z0,z2),dyade#(z1,z2)) 61: dyade#1#(nil(),z0) -> c_61() 62: mult#(z0,z1) -> c_62(mult#1#(z1,z0)) 63: mult#1#(::(z0,z1),z2) -> c_63(*#(z2,z0),mult#(z2,z1)) 64: mult#1#(nil(),z0) -> c_64() 54: *#(z0,z1) -> c_58(#mult#(z0,z1)) 43: #mult#(#pos(z0),#pos(z1)) -> c_47(#natmult#(z0,z1)) 42: #mult#(#pos(z0),#neg(z1)) -> c_46(#natmult#(z0,z1)) 41: #mult#(#pos(z0),#0()) -> c_45() 40: #mult#(#neg(z0),#pos(z1)) -> c_44(#natmult#(z0,z1)) 39: #mult#(#neg(z0),#neg(z1)) -> c_43(#natmult#(z0,z1)) 44: #natmult#(#0(),z0) -> c_48() 45: #natmult#(#s(z0),z1) -> c_49(#add#(#pos(z1),#natmult(z0,z1))) 38: #mult#(#neg(z0),#0()) -> c_42() 37: #mult#(#0(),#pos(z0)) -> c_41() 36: #mult#(#0(),#neg(z0)) -> c_40() 35: #mult#(#0(),#0()) -> c_39() 34: #add#(#pos(#s(#s(z0))),z1) -> c_38(#succ#(#add(#pos(#s(z0)),z1))) 33: #add#(#pos(#s(#0())),z0) -> c_37(#succ#(z0)) 50: #succ#(#0()) -> c_54() 51: #succ#(#neg(#s(#0()))) -> c_55() 52: #succ#(#neg(#s(#s(z0)))) -> c_56() 53: #succ#(#pos(#s(z0))) -> c_57() 32: #add#(#neg(#s(#s(z0))),z1) -> c_36(#pred#(#add(#pos(#s(z0)),z1))) 31: #add#(#neg(#s(#0())),z0) -> c_35(#pred#(z0)) 46: #pred#(#0()) -> c_50() 47: #pred#(#neg(#s(z0))) -> c_51() 48: #pred#(#pos(#s(#0()))) -> c_52() 49: #pred#(#pos(#s(#s(z0)))) -> c_53() 30: #add#(#0(),z0) -> c_34() 8: #ADD#(#neg(#s(#s(z0))),z1) -> c_12(#PRED#(#add(#pos(#s(z0)),z1)),#ADD#(#pos(#s(z0)),z1)) 7: #ADD#(#neg(#s(#0())),z0) -> c_11(#PRED#(z0)) 22: #PRED#(#0()) -> c_26() 23: #PRED#(#neg(#s(z0))) -> c_27() 24: #PRED#(#pos(#s(#0()))) -> c_28() 25: #PRED#(#pos(#s(#s(z0)))) -> c_29() 6: #ADD#(#0(),z0) -> c_10() 56: DYADE#1#(nil(),z0) -> c_5() 58: MULT#1#(nil(),z0) -> c_9() 57: MULT#1#(::(z0,z1),z2) -> c_7(*'#(z2,z0)) 55: *'#(z0,z1) -> c_1(#MULT#(z0,z1)) 11: #MULT#(#0(),#0()) -> c_15() 12: #MULT#(#0(),#neg(z0)) -> c_16() 13: #MULT#(#0(),#pos(z0)) -> c_17() 14: #MULT#(#neg(z0),#0()) -> c_18() 15: #MULT#(#neg(z0),#neg(z1)) -> c_19(#NATMULT#(z0,z1)) 16: #MULT#(#neg(z0),#pos(z1)) -> c_20(#NATMULT#(z0,z1)) 17: #MULT#(#pos(z0),#0()) -> c_21() 18: #MULT#(#pos(z0),#neg(z1)) -> c_22(#NATMULT#(z0,z1)) 19: #MULT#(#pos(z0),#pos(z1)) -> c_23(#NATMULT#(z0,z1)) 21: #NATMULT#(#s(z0),z1) -> c_25(#ADD#(#pos(z1),#natmult(z0,z1)),#NATMULT#(z0,z1)) 10: #ADD#(#pos(#s(#s(z0))),z1) -> c_14(#SUCC#(#add(#pos(#s(z0)),z1)),#ADD#(#pos(#s(z0)),z1)) 9: #ADD#(#pos(#s(#0())),z0) -> c_13(#SUCC#(z0)) 26: #SUCC#(#0()) -> c_30() 27: #SUCC#(#neg(#s(#0()))) -> c_31() 28: #SUCC#(#neg(#s(#s(z0)))) -> c_32() 29: #SUCC#(#pos(#s(z0))) -> c_33() 20: #NATMULT#(#0(),z0) -> c_24() * Step 7: UsableRules. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: DYADE#(z0,z1) -> c_2(DYADE#1#(z0,z1)) DYADE#1#(::(z0,z1),z2) -> c_3(MULT#(z0,z2)) DYADE#1#(::(z0,z1),z2) -> c_4(DYADE#(z1,z2)) MULT#(z0,z1) -> c_6(MULT#1#(z1,z0)) MULT#1#(::(z0,z1),z2) -> c_8(MULT#(z2,z1)) - Weak TRS: #add(#pos(#s(#0())),z0) -> #succ(z0) #add(#pos(#s(#s(z0))),z1) -> #succ(#add(#pos(#s(z0)),z1)) #natmult(#0(),z0) -> #0() #natmult(#s(z0),z1) -> #add(#pos(z1),#natmult(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))) - Signature: {#ADD/2,#MULT/2,#NATMULT/2,#PRED/1,#SUCC/1,#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,*'/2,DYADE/2 ,DYADE#1/2,MULT/2,MULT#1/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,*'#/2,DYADE#/2,DYADE#1#/2,MULT#/2,MULT#1#/2,dyade#/2 ,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,c/0,c1/1,c10/1,c11/0,c12/1,c13/1,c14/0,c15/2 ,c16/0,c17/0,c18/0,c19/0,c2/2,c20/0,c21/0,c22/0,c23/0,c24/1,c25/1,c26/1,c27/1,c28/0,c29/1,c3/1,c30/1,c31/1 ,c32/0,c4/2,c5/0,c6/0,c7/0,c8/0,c9/1,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/1,c_7/1,c_8/1,c_9/0,c_10/0 ,c_11/1,c_12/2,c_13/1,c_14/2,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/0,c_22/1,c_23/1,c_24/0,c_25/2 ,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/1,c_36/1,c_37/1,c_38/1,c_39/0,c_40/0 ,c_41/0,c_42/0,c_43/1,c_44/1,c_45/0,c_46/1,c_47/1,c_48/0,c_49/1,c_50/0,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0 ,c_56/0,c_57/0,c_58/1,c_59/1,c_60/2,c_61/0,c_62/1,c_63/2,c_64/0} - Obligation: innermost runtime complexity wrt. defined symbols {#ADD#,#MULT#,#NATMULT#,#PRED#,#SUCC#,#add#,#mult# ,#natmult#,#pred#,#succ#,*#,*'#,DYADE#,DYADE#1#,MULT#,MULT#1#,dyade#,dyade#1#,mult# ,mult#1#} and constructors {#0,#neg,#pos,#s,::,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c4,c5,c6,c7,c8,c9,nil} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: DYADE#(z0,z1) -> c_2(DYADE#1#(z0,z1)) DYADE#1#(::(z0,z1),z2) -> c_3(MULT#(z0,z2)) DYADE#1#(::(z0,z1),z2) -> c_4(DYADE#(z1,z2)) MULT#(z0,z1) -> c_6(MULT#1#(z1,z0)) MULT#1#(::(z0,z1),z2) -> c_8(MULT#(z2,z1)) * Step 8: PredecessorEstimationCP. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: DYADE#(z0,z1) -> c_2(DYADE#1#(z0,z1)) DYADE#1#(::(z0,z1),z2) -> c_3(MULT#(z0,z2)) DYADE#1#(::(z0,z1),z2) -> c_4(DYADE#(z1,z2)) MULT#(z0,z1) -> c_6(MULT#1#(z1,z0)) MULT#1#(::(z0,z1),z2) -> c_8(MULT#(z2,z1)) - Signature: {#ADD/2,#MULT/2,#NATMULT/2,#PRED/1,#SUCC/1,#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,*'/2,DYADE/2 ,DYADE#1/2,MULT/2,MULT#1/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,*'#/2,DYADE#/2,DYADE#1#/2,MULT#/2,MULT#1#/2,dyade#/2 ,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,c/0,c1/1,c10/1,c11/0,c12/1,c13/1,c14/0,c15/2 ,c16/0,c17/0,c18/0,c19/0,c2/2,c20/0,c21/0,c22/0,c23/0,c24/1,c25/1,c26/1,c27/1,c28/0,c29/1,c3/1,c30/1,c31/1 ,c32/0,c4/2,c5/0,c6/0,c7/0,c8/0,c9/1,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/1,c_7/1,c_8/1,c_9/0,c_10/0 ,c_11/1,c_12/2,c_13/1,c_14/2,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/0,c_22/1,c_23/1,c_24/0,c_25/2 ,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/1,c_36/1,c_37/1,c_38/1,c_39/0,c_40/0 ,c_41/0,c_42/0,c_43/1,c_44/1,c_45/0,c_46/1,c_47/1,c_48/0,c_49/1,c_50/0,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0 ,c_56/0,c_57/0,c_58/1,c_59/1,c_60/2,c_61/0,c_62/1,c_63/2,c_64/0} - Obligation: innermost runtime complexity wrt. defined symbols {#ADD#,#MULT#,#NATMULT#,#PRED#,#SUCC#,#add#,#mult# ,#natmult#,#pred#,#succ#,*#,*'#,DYADE#,DYADE#1#,MULT#,MULT#1#,dyade#,dyade#1#,mult# ,mult#1#} and constructors {#0,#neg,#pos,#s,::,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c4,c5,c6,c7,c8,c9,nil} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: DYADE#(z0,z1) -> c_2(DYADE#1#(z0,z1)) 2: DYADE#1#(::(z0,z1),z2) -> c_3(MULT#(z0,z2)) 3: DYADE#1#(::(z0,z1),z2) -> c_4(DYADE#(z1,z2)) 5: MULT#1#(::(z0,z1),z2) -> c_8(MULT#(z2,z1)) Consider the set of all dependency pairs 1: DYADE#(z0,z1) -> c_2(DYADE#1#(z0,z1)) 2: DYADE#1#(::(z0,z1),z2) -> c_3(MULT#(z0,z2)) 3: DYADE#1#(::(z0,z1),z2) -> c_4(DYADE#(z1,z2)) 4: MULT#(z0,z1) -> c_6(MULT#1#(z1,z0)) 5: MULT#1#(::(z0,z1),z2) -> c_8(MULT#(z2,z1)) Processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^1)) BEST_CASE TIME (?,?) SPACE(?,?)on application of the dependency pairs {1,2,3,5} These cover all (indirect) predecessors of dependency pairs {1,2,3,4,5} their number of applications is equally bounded. The dependency pairs are shifted into the weak component. ** Step 8.a:1: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: DYADE#(z0,z1) -> c_2(DYADE#1#(z0,z1)) DYADE#1#(::(z0,z1),z2) -> c_3(MULT#(z0,z2)) DYADE#1#(::(z0,z1),z2) -> c_4(DYADE#(z1,z2)) MULT#(z0,z1) -> c_6(MULT#1#(z1,z0)) MULT#1#(::(z0,z1),z2) -> c_8(MULT#(z2,z1)) - Signature: {#ADD/2,#MULT/2,#NATMULT/2,#PRED/1,#SUCC/1,#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,*'/2,DYADE/2 ,DYADE#1/2,MULT/2,MULT#1/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,*'#/2,DYADE#/2,DYADE#1#/2,MULT#/2,MULT#1#/2,dyade#/2 ,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,c/0,c1/1,c10/1,c11/0,c12/1,c13/1,c14/0,c15/2 ,c16/0,c17/0,c18/0,c19/0,c2/2,c20/0,c21/0,c22/0,c23/0,c24/1,c25/1,c26/1,c27/1,c28/0,c29/1,c3/1,c30/1,c31/1 ,c32/0,c4/2,c5/0,c6/0,c7/0,c8/0,c9/1,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/1,c_7/1,c_8/1,c_9/0,c_10/0 ,c_11/1,c_12/2,c_13/1,c_14/2,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/0,c_22/1,c_23/1,c_24/0,c_25/2 ,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/1,c_36/1,c_37/1,c_38/1,c_39/0,c_40/0 ,c_41/0,c_42/0,c_43/1,c_44/1,c_45/0,c_46/1,c_47/1,c_48/0,c_49/1,c_50/0,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0 ,c_56/0,c_57/0,c_58/1,c_59/1,c_60/2,c_61/0,c_62/1,c_63/2,c_64/0} - Obligation: innermost runtime complexity wrt. defined symbols {#ADD#,#MULT#,#NATMULT#,#PRED#,#SUCC#,#add#,#mult# ,#natmult#,#pred#,#succ#,*#,*'#,DYADE#,DYADE#1#,MULT#,MULT#1#,dyade#,dyade#1#,mult# ,mult#1#} and constructors {#0,#neg,#pos,#s,::,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c4,c5,c6,c7,c8,c9,nil} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_2) = {1}, uargs(c_3) = {1}, uargs(c_4) = {1}, uargs(c_6) = {1}, uargs(c_8) = {1} Following symbols are considered usable: {#ADD#,#MULT#,#NATMULT#,#PRED#,#SUCC#,#add#,#mult#,#natmult#,#pred#,#succ#,*#,*'#,DYADE#,DYADE#1#,MULT# ,MULT#1#,dyade#,dyade#1#,mult#,mult#1#} TcT has computed the following interpretation: p(#0) = [0] p(#ADD) = [1] x1 + [2] x2 + [1] p(#MULT) = [2] x1 + [1] x2 + [1] p(#NATMULT) = [2] x1 + [0] p(#PRED) = [1] p(#SUCC) = [2] x1 + [1] p(#add) = [1] x1 + [1] p(#mult) = [2] p(#natmult) = [1] x2 + [2] p(#neg) = [0] p(#pos) = [4] p(#pred) = [0] p(#s) = [1] x1 + [1] p(#succ) = [4] x1 + [1] p(*) = [1] x1 + [1] x2 + [1] p(*') = [1] x1 + [0] p(::) = [1] x1 + [1] x2 + [3] p(DYADE) = [1] x1 + [1] x2 + [1] p(DYADE#1) = [1] x1 + [1] x2 + [0] p(MULT) = [1] x2 + [2] p(MULT#1) = [8] x2 + [1] p(c) = [1] p(c1) = [1] x1 + [2] p(c10) = [1] x1 + [0] p(c11) = [0] p(c12) = [1] x1 + [0] p(c13) = [1] x1 + [0] p(c14) = [0] p(c15) = [1] x1 + [1] x2 + [0] p(c16) = [0] p(c17) = [0] p(c18) = [0] p(c19) = [0] p(c2) = [1] x1 + [1] x2 + [0] p(c20) = [0] p(c21) = [0] p(c22) = [0] p(c23) = [0] p(c24) = [1] x1 + [0] p(c25) = [1] x1 + [0] p(c26) = [0] p(c27) = [1] x1 + [0] p(c28) = [0] p(c29) = [1] x1 + [0] p(c3) = [1] x1 + [0] p(c30) = [1] x1 + [0] p(c31) = [1] x1 + [0] p(c32) = [0] p(c4) = [1] x1 + [1] x2 + [0] p(c5) = [0] p(c6) = [0] p(c7) = [0] p(c8) = [0] p(c9) = [1] x1 + [0] p(dyade) = [0] p(dyade#1) = [0] p(mult) = [0] p(mult#1) = [0] p(nil) = [0] p(#ADD#) = [1] x1 + [1] x2 + [1] p(#MULT#) = [0] p(#NATMULT#) = [1] x2 + [0] p(#PRED#) = [0] p(#SUCC#) = [8] x1 + [0] p(#add#) = [4] p(#mult#) = [1] x1 + [0] p(#natmult#) = [1] x1 + [1] x2 + [4] p(#pred#) = [2] x1 + [4] p(#succ#) = [1] x1 + [1] p(*#) = [1] x1 + [1] p(*'#) = [2] x1 + [1] x2 + [0] p(DYADE#) = [8] x1 + [8] x2 + [7] p(DYADE#1#) = [8] x1 + [8] x2 + [5] p(MULT#) = [8] x2 + [4] p(MULT#1#) = [8] x1 + [4] p(dyade#) = [8] x2 + [2] p(dyade#1#) = [1] x1 + [1] p(mult#) = [1] x1 + [1] p(mult#1#) = [1] x1 + [1] x2 + [8] p(c_1) = [1] x1 + [4] p(c_2) = [1] x1 + [0] p(c_3) = [1] x1 + [0] p(c_4) = [1] x1 + [0] p(c_5) = [1] p(c_6) = [1] x1 + [0] p(c_7) = [2] p(c_8) = [1] x1 + [4] p(c_9) = [1] p(c_10) = [2] p(c_11) = [1] x1 + [2] p(c_12) = [1] x1 + [0] p(c_13) = [1] p(c_14) = [2] x2 + [0] p(c_15) = [8] p(c_16) = [0] p(c_17) = [0] p(c_18) = [1] p(c_19) = [1] x1 + [1] p(c_20) = [2] p(c_21) = [2] p(c_22) = [2] p(c_23) = [1] x1 + [1] p(c_24) = [0] p(c_25) = [1] x2 + [1] p(c_26) = [0] p(c_27) = [0] p(c_28) = [0] p(c_29) = [0] p(c_30) = [4] p(c_31) = [1] p(c_32) = [0] p(c_33) = [0] p(c_34) = [0] p(c_35) = [1] p(c_36) = [2] x1 + [2] p(c_37) = [1] p(c_38) = [4] p(c_39) = [1] p(c_40) = [1] p(c_41) = [0] p(c_42) = [0] p(c_43) = [4] x1 + [1] p(c_44) = [1] p(c_45) = [0] p(c_46) = [0] p(c_47) = [8] x1 + [4] p(c_48) = [1] p(c_49) = [1] x1 + [4] p(c_50) = [1] p(c_51) = [1] p(c_52) = [1] p(c_53) = [1] p(c_54) = [1] p(c_55) = [1] p(c_56) = [1] p(c_57) = [1] p(c_58) = [1] x1 + [1] p(c_59) = [0] p(c_60) = [2] x1 + [0] p(c_61) = [1] p(c_62) = [0] p(c_63) = [1] x1 + [1] p(c_64) = [2] Following rules are strictly oriented: DYADE#(z0,z1) = [8] z0 + [8] z1 + [7] > [8] z0 + [8] z1 + [5] = c_2(DYADE#1#(z0,z1)) DYADE#1#(::(z0,z1),z2) = [8] z0 + [8] z1 + [8] z2 + [29] > [8] z2 + [4] = c_3(MULT#(z0,z2)) DYADE#1#(::(z0,z1),z2) = [8] z0 + [8] z1 + [8] z2 + [29] > [8] z1 + [8] z2 + [7] = c_4(DYADE#(z1,z2)) MULT#1#(::(z0,z1),z2) = [8] z0 + [8] z1 + [28] > [8] z1 + [8] = c_8(MULT#(z2,z1)) Following rules are (at-least) weakly oriented: MULT#(z0,z1) = [8] z1 + [4] >= [8] z1 + [4] = c_6(MULT#1#(z1,z0)) ** Step 8.a:2: Assumption. WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: MULT#(z0,z1) -> c_6(MULT#1#(z1,z0)) - Weak DPs: DYADE#(z0,z1) -> c_2(DYADE#1#(z0,z1)) DYADE#1#(::(z0,z1),z2) -> c_3(MULT#(z0,z2)) DYADE#1#(::(z0,z1),z2) -> c_4(DYADE#(z1,z2)) MULT#1#(::(z0,z1),z2) -> c_8(MULT#(z2,z1)) - Signature: {#ADD/2,#MULT/2,#NATMULT/2,#PRED/1,#SUCC/1,#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,*'/2,DYADE/2 ,DYADE#1/2,MULT/2,MULT#1/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,*'#/2,DYADE#/2,DYADE#1#/2,MULT#/2,MULT#1#/2,dyade#/2 ,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,c/0,c1/1,c10/1,c11/0,c12/1,c13/1,c14/0,c15/2 ,c16/0,c17/0,c18/0,c19/0,c2/2,c20/0,c21/0,c22/0,c23/0,c24/1,c25/1,c26/1,c27/1,c28/0,c29/1,c3/1,c30/1,c31/1 ,c32/0,c4/2,c5/0,c6/0,c7/0,c8/0,c9/1,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/1,c_7/1,c_8/1,c_9/0,c_10/0 ,c_11/1,c_12/2,c_13/1,c_14/2,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/0,c_22/1,c_23/1,c_24/0,c_25/2 ,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/1,c_36/1,c_37/1,c_38/1,c_39/0,c_40/0 ,c_41/0,c_42/0,c_43/1,c_44/1,c_45/0,c_46/1,c_47/1,c_48/0,c_49/1,c_50/0,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0 ,c_56/0,c_57/0,c_58/1,c_59/1,c_60/2,c_61/0,c_62/1,c_63/2,c_64/0} - Obligation: innermost runtime complexity wrt. defined symbols {#ADD#,#MULT#,#NATMULT#,#PRED#,#SUCC#,#add#,#mult# ,#natmult#,#pred#,#succ#,*#,*'#,DYADE#,DYADE#1#,MULT#,MULT#1#,dyade#,dyade#1#,mult# ,mult#1#} and constructors {#0,#neg,#pos,#s,::,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c4,c5,c6,c7,c8,c9,nil} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown, timeBCUB = Unknown, timeBCLB = Unknown}} + Details: () ** Step 8.b:1: RemoveWeakSuffixes. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: DYADE#(z0,z1) -> c_2(DYADE#1#(z0,z1)) DYADE#1#(::(z0,z1),z2) -> c_3(MULT#(z0,z2)) DYADE#1#(::(z0,z1),z2) -> c_4(DYADE#(z1,z2)) MULT#(z0,z1) -> c_6(MULT#1#(z1,z0)) MULT#1#(::(z0,z1),z2) -> c_8(MULT#(z2,z1)) - Signature: {#ADD/2,#MULT/2,#NATMULT/2,#PRED/1,#SUCC/1,#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,*'/2,DYADE/2 ,DYADE#1/2,MULT/2,MULT#1/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,*'#/2,DYADE#/2,DYADE#1#/2,MULT#/2,MULT#1#/2,dyade#/2 ,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,c/0,c1/1,c10/1,c11/0,c12/1,c13/1,c14/0,c15/2 ,c16/0,c17/0,c18/0,c19/0,c2/2,c20/0,c21/0,c22/0,c23/0,c24/1,c25/1,c26/1,c27/1,c28/0,c29/1,c3/1,c30/1,c31/1 ,c32/0,c4/2,c5/0,c6/0,c7/0,c8/0,c9/1,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/1,c_7/1,c_8/1,c_9/0,c_10/0 ,c_11/1,c_12/2,c_13/1,c_14/2,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/0,c_22/1,c_23/1,c_24/0,c_25/2 ,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/1,c_36/1,c_37/1,c_38/1,c_39/0,c_40/0 ,c_41/0,c_42/0,c_43/1,c_44/1,c_45/0,c_46/1,c_47/1,c_48/0,c_49/1,c_50/0,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0 ,c_56/0,c_57/0,c_58/1,c_59/1,c_60/2,c_61/0,c_62/1,c_63/2,c_64/0} - Obligation: innermost runtime complexity wrt. defined symbols {#ADD#,#MULT#,#NATMULT#,#PRED#,#SUCC#,#add#,#mult# ,#natmult#,#pred#,#succ#,*#,*'#,DYADE#,DYADE#1#,MULT#,MULT#1#,dyade#,dyade#1#,mult# ,mult#1#} and constructors {#0,#neg,#pos,#s,::,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c4,c5,c6,c7,c8,c9,nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:DYADE#(z0,z1) -> c_2(DYADE#1#(z0,z1)) -->_1 DYADE#1#(::(z0,z1),z2) -> c_4(DYADE#(z1,z2)):3 -->_1 DYADE#1#(::(z0,z1),z2) -> c_3(MULT#(z0,z2)):2 2:W:DYADE#1#(::(z0,z1),z2) -> c_3(MULT#(z0,z2)) -->_1 MULT#(z0,z1) -> c_6(MULT#1#(z1,z0)):4 3:W:DYADE#1#(::(z0,z1),z2) -> c_4(DYADE#(z1,z2)) -->_1 DYADE#(z0,z1) -> c_2(DYADE#1#(z0,z1)):1 4:W:MULT#(z0,z1) -> c_6(MULT#1#(z1,z0)) -->_1 MULT#1#(::(z0,z1),z2) -> c_8(MULT#(z2,z1)):5 5:W:MULT#1#(::(z0,z1),z2) -> c_8(MULT#(z2,z1)) -->_1 MULT#(z0,z1) -> c_6(MULT#1#(z1,z0)):4 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: DYADE#(z0,z1) -> c_2(DYADE#1#(z0,z1)) 3: DYADE#1#(::(z0,z1),z2) -> c_4(DYADE#(z1,z2)) 2: DYADE#1#(::(z0,z1),z2) -> c_3(MULT#(z0,z2)) 4: MULT#(z0,z1) -> c_6(MULT#1#(z1,z0)) 5: MULT#1#(::(z0,z1),z2) -> c_8(MULT#(z2,z1)) ** Step 8.b:2: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Signature: {#ADD/2,#MULT/2,#NATMULT/2,#PRED/1,#SUCC/1,#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,*'/2,DYADE/2 ,DYADE#1/2,MULT/2,MULT#1/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,*'#/2,DYADE#/2,DYADE#1#/2,MULT#/2,MULT#1#/2,dyade#/2 ,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,c/0,c1/1,c10/1,c11/0,c12/1,c13/1,c14/0,c15/2 ,c16/0,c17/0,c18/0,c19/0,c2/2,c20/0,c21/0,c22/0,c23/0,c24/1,c25/1,c26/1,c27/1,c28/0,c29/1,c3/1,c30/1,c31/1 ,c32/0,c4/2,c5/0,c6/0,c7/0,c8/0,c9/1,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/1,c_7/1,c_8/1,c_9/0,c_10/0 ,c_11/1,c_12/2,c_13/1,c_14/2,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/1,c_21/0,c_22/1,c_23/1,c_24/0,c_25/2 ,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/1,c_36/1,c_37/1,c_38/1,c_39/0,c_40/0 ,c_41/0,c_42/0,c_43/1,c_44/1,c_45/0,c_46/1,c_47/1,c_48/0,c_49/1,c_50/0,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0 ,c_56/0,c_57/0,c_58/1,c_59/1,c_60/2,c_61/0,c_62/1,c_63/2,c_64/0} - Obligation: innermost runtime complexity wrt. defined symbols {#ADD#,#MULT#,#NATMULT#,#PRED#,#SUCC#,#add#,#mult# ,#natmult#,#pred#,#succ#,*#,*'#,DYADE#,DYADE#1#,MULT#,MULT#1#,dyade#,dyade#1#,mult# ,mult#1#} and constructors {#0,#neg,#pos,#s,::,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c4,c5,c6,c7,c8,c9,nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))