WORST_CASE(?,O(n^4)) * Step 1: DependencyPairs WORST_CASE(?,O(n^4)) + Considered Problem: - Strict TRS: #add(#0(),y) -> y #add(#neg(#s(#0())),y) -> #pred(y) #add(#neg(#s(#s(x))),y) -> #pred(#add(#pos(#s(x)),y)) #add(#pos(#s(#0())),y) -> #succ(y) #add(#pos(#s(#s(x))),y) -> #succ(#add(#pos(#s(x)),y)) #mult(#0(),#0()) -> #0() #mult(#0(),#neg(y)) -> #0() #mult(#0(),#pos(y)) -> #0() #mult(#neg(x),#0()) -> #0() #mult(#neg(x),#neg(y)) -> #pos(#natmult(x,y)) #mult(#neg(x),#pos(y)) -> #neg(#natmult(x,y)) #mult(#pos(x),#0()) -> #0() #mult(#pos(x),#neg(y)) -> #neg(#natmult(x,y)) #mult(#pos(x),#pos(y)) -> #pos(#natmult(x,y)) #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) #pred(#0()) -> #neg(#s(#0())) #pred(#neg(#s(x))) -> #neg(#s(#s(x))) #pred(#pos(#s(#0()))) -> #0() #pred(#pos(#s(#s(x)))) -> #pos(#s(x)) #succ(#0()) -> #pos(#s(#0())) #succ(#neg(#s(#0()))) -> #0() #succ(#neg(#s(#s(x)))) -> #neg(#s(x)) #succ(#pos(#s(x))) -> #pos(#s(#s(x))) dyade(l1,l2) -> dyade#1(l1,l2) dyade#1(dd(x,xs),l2) -> dd(mult(x,l2),dyade(xs,l2)) dyade#1(nil(),l2) -> nil() mult(n,l) -> mult#1(l,n) mult(x,y) -> #mult(x,y) mult#1(dd(x,xs),n) -> dd(mult(n,x),mult(n,xs)) mult#1(nil(),n) -> nil() - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2} / {#0/0,#neg/1 ,#pos/1,#s/1,dd/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add,#mult,#natadd,#natmult,#pred,#succ,dyade,dyade#1 ,mult,mult#1} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs #add#(#0(),y) -> c_1() #add#(#neg(#s(#0())),y) -> c_2(#pred#(y)) #add#(#neg(#s(#s(x))),y) -> c_3(#pred#(#add(#pos(#s(x)),y)),#add#(#pos(#s(x)),y)) #add#(#pos(#s(#0())),y) -> c_4(#succ#(y)) #add#(#pos(#s(#s(x))),y) -> c_5(#succ#(#add(#pos(#s(x)),y)),#add#(#pos(#s(x)),y)) #mult#(#0(),#0()) -> c_6() #mult#(#0(),#neg(y)) -> c_7() #mult#(#0(),#pos(y)) -> c_8() #mult#(#neg(x),#0()) -> c_9() #mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)) #mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)) #mult#(#pos(x),#0()) -> c_12() #mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)) #mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)) #natadd#(#0(),y) -> c_15() #natadd#(#s(x),y) -> c_16(#natadd#(x,y)) #natmult#(#0(),y) -> c_17() #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)) #pred#(#0()) -> c_19() #pred#(#neg(#s(x))) -> c_20() #pred#(#pos(#s(#0()))) -> c_21() #pred#(#pos(#s(#s(x)))) -> c_22() #succ#(#0()) -> c_23() #succ#(#neg(#s(#0()))) -> c_24() #succ#(#neg(#s(#s(x)))) -> c_25() #succ#(#pos(#s(x))) -> c_26() dyade#(l1,l2) -> c_27(dyade#1#(l1,l2)) dyade#1#(dd(x,xs),l2) -> c_28(mult#(x,l2),dyade#(xs,l2)) dyade#1#(nil(),l2) -> c_29() mult#(n,l) -> c_30(mult#1#(l,n)) mult#(x,y) -> c_31(#mult#(x,y)) mult#1#(dd(x,xs),n) -> c_32(mult#(n,x),mult#(n,xs)) mult#1#(nil(),n) -> c_33() Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation WORST_CASE(?,O(n^4)) + Considered Problem: - Strict DPs: #add#(#0(),y) -> c_1() #add#(#neg(#s(#0())),y) -> c_2(#pred#(y)) #add#(#neg(#s(#s(x))),y) -> c_3(#pred#(#add(#pos(#s(x)),y)),#add#(#pos(#s(x)),y)) #add#(#pos(#s(#0())),y) -> c_4(#succ#(y)) #add#(#pos(#s(#s(x))),y) -> c_5(#succ#(#add(#pos(#s(x)),y)),#add#(#pos(#s(x)),y)) #mult#(#0(),#0()) -> c_6() #mult#(#0(),#neg(y)) -> c_7() #mult#(#0(),#pos(y)) -> c_8() #mult#(#neg(x),#0()) -> c_9() #mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)) #mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)) #mult#(#pos(x),#0()) -> c_12() #mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)) #mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)) #natadd#(#0(),y) -> c_15() #natadd#(#s(x),y) -> c_16(#natadd#(x,y)) #natmult#(#0(),y) -> c_17() #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)) #pred#(#0()) -> c_19() #pred#(#neg(#s(x))) -> c_20() #pred#(#pos(#s(#0()))) -> c_21() #pred#(#pos(#s(#s(x)))) -> c_22() #succ#(#0()) -> c_23() #succ#(#neg(#s(#0()))) -> c_24() #succ#(#neg(#s(#s(x)))) -> c_25() #succ#(#pos(#s(x))) -> c_26() dyade#(l1,l2) -> c_27(dyade#1#(l1,l2)) dyade#1#(dd(x,xs),l2) -> c_28(mult#(x,l2),dyade#(xs,l2)) dyade#1#(nil(),l2) -> c_29() mult#(n,l) -> c_30(mult#1#(l,n)) mult#(x,y) -> c_31(#mult#(x,y)) mult#1#(dd(x,xs),n) -> c_32(mult#(n,x),mult#(n,xs)) mult#1#(nil(),n) -> c_33() - Weak TRS: #add(#0(),y) -> y #add(#neg(#s(#0())),y) -> #pred(y) #add(#neg(#s(#s(x))),y) -> #pred(#add(#pos(#s(x)),y)) #add(#pos(#s(#0())),y) -> #succ(y) #add(#pos(#s(#s(x))),y) -> #succ(#add(#pos(#s(x)),y)) #mult(#0(),#0()) -> #0() #mult(#0(),#neg(y)) -> #0() #mult(#0(),#pos(y)) -> #0() #mult(#neg(x),#0()) -> #0() #mult(#neg(x),#neg(y)) -> #pos(#natmult(x,y)) #mult(#neg(x),#pos(y)) -> #neg(#natmult(x,y)) #mult(#pos(x),#0()) -> #0() #mult(#pos(x),#neg(y)) -> #neg(#natmult(x,y)) #mult(#pos(x),#pos(y)) -> #pos(#natmult(x,y)) #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) #pred(#0()) -> #neg(#s(#0())) #pred(#neg(#s(x))) -> #neg(#s(#s(x))) #pred(#pos(#s(#0()))) -> #0() #pred(#pos(#s(#s(x)))) -> #pos(#s(x)) #succ(#0()) -> #pos(#s(#0())) #succ(#neg(#s(#0()))) -> #0() #succ(#neg(#s(#s(x)))) -> #neg(#s(x)) #succ(#pos(#s(x))) -> #pos(#s(#s(x))) dyade(l1,l2) -> dyade#1(l1,l2) dyade#1(dd(x,xs),l2) -> dd(mult(x,l2),dyade(xs,l2)) dyade#1(nil(),l2) -> nil() mult(n,l) -> mult#1(l,n) mult(x,y) -> #mult(x,y) mult#1(dd(x,xs),n) -> dd(mult(n,x),mult(n,xs)) mult#1(nil(),n) -> nil() - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2,#add#/2,#mult#/2 ,#natadd#/2,#natmult#/2,#pred#/1,#succ#/1,dyade#/2,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1 ,dd/2,nil/0,c_1/0,c_2/1,c_3/2,c_4/1,c_5/2,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/1,c_15/0 ,c_16/1,c_17/0,c_18/2,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/2,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natadd#,#natmult#,#pred#,#succ#,dyade# ,dyade#1#,mult#,mult#1#} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,6,7,8,9,12,15,17,19,20,21,22,23,24,25,26,29,33} by application of Pre({1,6,7,8,9,12,15,17,19,20,21,22,23,24,25,26,29,33}) = {2,3,4,5,10,11,13,14,16,18,27,30,31}. Here rules are labelled as follows: 1: #add#(#0(),y) -> c_1() 2: #add#(#neg(#s(#0())),y) -> c_2(#pred#(y)) 3: #add#(#neg(#s(#s(x))),y) -> c_3(#pred#(#add(#pos(#s(x)),y)),#add#(#pos(#s(x)),y)) 4: #add#(#pos(#s(#0())),y) -> c_4(#succ#(y)) 5: #add#(#pos(#s(#s(x))),y) -> c_5(#succ#(#add(#pos(#s(x)),y)),#add#(#pos(#s(x)),y)) 6: #mult#(#0(),#0()) -> c_6() 7: #mult#(#0(),#neg(y)) -> c_7() 8: #mult#(#0(),#pos(y)) -> c_8() 9: #mult#(#neg(x),#0()) -> c_9() 10: #mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)) 11: #mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)) 12: #mult#(#pos(x),#0()) -> c_12() 13: #mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)) 14: #mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)) 15: #natadd#(#0(),y) -> c_15() 16: #natadd#(#s(x),y) -> c_16(#natadd#(x,y)) 17: #natmult#(#0(),y) -> c_17() 18: #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)) 19: #pred#(#0()) -> c_19() 20: #pred#(#neg(#s(x))) -> c_20() 21: #pred#(#pos(#s(#0()))) -> c_21() 22: #pred#(#pos(#s(#s(x)))) -> c_22() 23: #succ#(#0()) -> c_23() 24: #succ#(#neg(#s(#0()))) -> c_24() 25: #succ#(#neg(#s(#s(x)))) -> c_25() 26: #succ#(#pos(#s(x))) -> c_26() 27: dyade#(l1,l2) -> c_27(dyade#1#(l1,l2)) 28: dyade#1#(dd(x,xs),l2) -> c_28(mult#(x,l2),dyade#(xs,l2)) 29: dyade#1#(nil(),l2) -> c_29() 30: mult#(n,l) -> c_30(mult#1#(l,n)) 31: mult#(x,y) -> c_31(#mult#(x,y)) 32: mult#1#(dd(x,xs),n) -> c_32(mult#(n,x),mult#(n,xs)) 33: mult#1#(nil(),n) -> c_33() * Step 3: PredecessorEstimation WORST_CASE(?,O(n^4)) + Considered Problem: - Strict DPs: #add#(#neg(#s(#0())),y) -> c_2(#pred#(y)) #add#(#neg(#s(#s(x))),y) -> c_3(#pred#(#add(#pos(#s(x)),y)),#add#(#pos(#s(x)),y)) #add#(#pos(#s(#0())),y) -> c_4(#succ#(y)) #add#(#pos(#s(#s(x))),y) -> c_5(#succ#(#add(#pos(#s(x)),y)),#add#(#pos(#s(x)),y)) #mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)) #mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)) #mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)) #mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)) #natadd#(#s(x),y) -> c_16(#natadd#(x,y)) #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)) dyade#(l1,l2) -> c_27(dyade#1#(l1,l2)) dyade#1#(dd(x,xs),l2) -> c_28(mult#(x,l2),dyade#(xs,l2)) mult#(n,l) -> c_30(mult#1#(l,n)) mult#(x,y) -> c_31(#mult#(x,y)) mult#1#(dd(x,xs),n) -> c_32(mult#(n,x),mult#(n,xs)) - Weak DPs: #add#(#0(),y) -> c_1() #mult#(#0(),#0()) -> c_6() #mult#(#0(),#neg(y)) -> c_7() #mult#(#0(),#pos(y)) -> c_8() #mult#(#neg(x),#0()) -> c_9() #mult#(#pos(x),#0()) -> c_12() #natadd#(#0(),y) -> c_15() #natmult#(#0(),y) -> c_17() #pred#(#0()) -> c_19() #pred#(#neg(#s(x))) -> c_20() #pred#(#pos(#s(#0()))) -> c_21() #pred#(#pos(#s(#s(x)))) -> c_22() #succ#(#0()) -> c_23() #succ#(#neg(#s(#0()))) -> c_24() #succ#(#neg(#s(#s(x)))) -> c_25() #succ#(#pos(#s(x))) -> c_26() dyade#1#(nil(),l2) -> c_29() mult#1#(nil(),n) -> c_33() - Weak TRS: #add(#0(),y) -> y #add(#neg(#s(#0())),y) -> #pred(y) #add(#neg(#s(#s(x))),y) -> #pred(#add(#pos(#s(x)),y)) #add(#pos(#s(#0())),y) -> #succ(y) #add(#pos(#s(#s(x))),y) -> #succ(#add(#pos(#s(x)),y)) #mult(#0(),#0()) -> #0() #mult(#0(),#neg(y)) -> #0() #mult(#0(),#pos(y)) -> #0() #mult(#neg(x),#0()) -> #0() #mult(#neg(x),#neg(y)) -> #pos(#natmult(x,y)) #mult(#neg(x),#pos(y)) -> #neg(#natmult(x,y)) #mult(#pos(x),#0()) -> #0() #mult(#pos(x),#neg(y)) -> #neg(#natmult(x,y)) #mult(#pos(x),#pos(y)) -> #pos(#natmult(x,y)) #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) #pred(#0()) -> #neg(#s(#0())) #pred(#neg(#s(x))) -> #neg(#s(#s(x))) #pred(#pos(#s(#0()))) -> #0() #pred(#pos(#s(#s(x)))) -> #pos(#s(x)) #succ(#0()) -> #pos(#s(#0())) #succ(#neg(#s(#0()))) -> #0() #succ(#neg(#s(#s(x)))) -> #neg(#s(x)) #succ(#pos(#s(x))) -> #pos(#s(#s(x))) dyade(l1,l2) -> dyade#1(l1,l2) dyade#1(dd(x,xs),l2) -> dd(mult(x,l2),dyade(xs,l2)) dyade#1(nil(),l2) -> nil() mult(n,l) -> mult#1(l,n) mult(x,y) -> #mult(x,y) mult#1(dd(x,xs),n) -> dd(mult(n,x),mult(n,xs)) mult#1(nil(),n) -> nil() - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2,#add#/2,#mult#/2 ,#natadd#/2,#natmult#/2,#pred#/1,#succ#/1,dyade#/2,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1 ,dd/2,nil/0,c_1/0,c_2/1,c_3/2,c_4/1,c_5/2,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/1,c_15/0 ,c_16/1,c_17/0,c_18/2,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/2,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natadd#,#natmult#,#pred#,#succ#,dyade# ,dyade#1#,mult#,mult#1#} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,3} by application of Pre({1,3}) = {2,4}. Here rules are labelled as follows: 1: #add#(#neg(#s(#0())),y) -> c_2(#pred#(y)) 2: #add#(#neg(#s(#s(x))),y) -> c_3(#pred#(#add(#pos(#s(x)),y)),#add#(#pos(#s(x)),y)) 3: #add#(#pos(#s(#0())),y) -> c_4(#succ#(y)) 4: #add#(#pos(#s(#s(x))),y) -> c_5(#succ#(#add(#pos(#s(x)),y)),#add#(#pos(#s(x)),y)) 5: #mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)) 6: #mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)) 7: #mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)) 8: #mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)) 9: #natadd#(#s(x),y) -> c_16(#natadd#(x,y)) 10: #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)) 11: dyade#(l1,l2) -> c_27(dyade#1#(l1,l2)) 12: dyade#1#(dd(x,xs),l2) -> c_28(mult#(x,l2),dyade#(xs,l2)) 13: mult#(n,l) -> c_30(mult#1#(l,n)) 14: mult#(x,y) -> c_31(#mult#(x,y)) 15: mult#1#(dd(x,xs),n) -> c_32(mult#(n,x),mult#(n,xs)) 16: #add#(#0(),y) -> c_1() 17: #mult#(#0(),#0()) -> c_6() 18: #mult#(#0(),#neg(y)) -> c_7() 19: #mult#(#0(),#pos(y)) -> c_8() 20: #mult#(#neg(x),#0()) -> c_9() 21: #mult#(#pos(x),#0()) -> c_12() 22: #natadd#(#0(),y) -> c_15() 23: #natmult#(#0(),y) -> c_17() 24: #pred#(#0()) -> c_19() 25: #pred#(#neg(#s(x))) -> c_20() 26: #pred#(#pos(#s(#0()))) -> c_21() 27: #pred#(#pos(#s(#s(x)))) -> c_22() 28: #succ#(#0()) -> c_23() 29: #succ#(#neg(#s(#0()))) -> c_24() 30: #succ#(#neg(#s(#s(x)))) -> c_25() 31: #succ#(#pos(#s(x))) -> c_26() 32: dyade#1#(nil(),l2) -> c_29() 33: mult#1#(nil(),n) -> c_33() * Step 4: RemoveWeakSuffixes WORST_CASE(?,O(n^4)) + Considered Problem: - Strict DPs: #add#(#neg(#s(#s(x))),y) -> c_3(#pred#(#add(#pos(#s(x)),y)),#add#(#pos(#s(x)),y)) #add#(#pos(#s(#s(x))),y) -> c_5(#succ#(#add(#pos(#s(x)),y)),#add#(#pos(#s(x)),y)) #mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)) #mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)) #mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)) #mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)) #natadd#(#s(x),y) -> c_16(#natadd#(x,y)) #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)) dyade#(l1,l2) -> c_27(dyade#1#(l1,l2)) dyade#1#(dd(x,xs),l2) -> c_28(mult#(x,l2),dyade#(xs,l2)) mult#(n,l) -> c_30(mult#1#(l,n)) mult#(x,y) -> c_31(#mult#(x,y)) mult#1#(dd(x,xs),n) -> c_32(mult#(n,x),mult#(n,xs)) - Weak DPs: #add#(#0(),y) -> c_1() #add#(#neg(#s(#0())),y) -> c_2(#pred#(y)) #add#(#pos(#s(#0())),y) -> c_4(#succ#(y)) #mult#(#0(),#0()) -> c_6() #mult#(#0(),#neg(y)) -> c_7() #mult#(#0(),#pos(y)) -> c_8() #mult#(#neg(x),#0()) -> c_9() #mult#(#pos(x),#0()) -> c_12() #natadd#(#0(),y) -> c_15() #natmult#(#0(),y) -> c_17() #pred#(#0()) -> c_19() #pred#(#neg(#s(x))) -> c_20() #pred#(#pos(#s(#0()))) -> c_21() #pred#(#pos(#s(#s(x)))) -> c_22() #succ#(#0()) -> c_23() #succ#(#neg(#s(#0()))) -> c_24() #succ#(#neg(#s(#s(x)))) -> c_25() #succ#(#pos(#s(x))) -> c_26() dyade#1#(nil(),l2) -> c_29() mult#1#(nil(),n) -> c_33() - Weak TRS: #add(#0(),y) -> y #add(#neg(#s(#0())),y) -> #pred(y) #add(#neg(#s(#s(x))),y) -> #pred(#add(#pos(#s(x)),y)) #add(#pos(#s(#0())),y) -> #succ(y) #add(#pos(#s(#s(x))),y) -> #succ(#add(#pos(#s(x)),y)) #mult(#0(),#0()) -> #0() #mult(#0(),#neg(y)) -> #0() #mult(#0(),#pos(y)) -> #0() #mult(#neg(x),#0()) -> #0() #mult(#neg(x),#neg(y)) -> #pos(#natmult(x,y)) #mult(#neg(x),#pos(y)) -> #neg(#natmult(x,y)) #mult(#pos(x),#0()) -> #0() #mult(#pos(x),#neg(y)) -> #neg(#natmult(x,y)) #mult(#pos(x),#pos(y)) -> #pos(#natmult(x,y)) #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) #pred(#0()) -> #neg(#s(#0())) #pred(#neg(#s(x))) -> #neg(#s(#s(x))) #pred(#pos(#s(#0()))) -> #0() #pred(#pos(#s(#s(x)))) -> #pos(#s(x)) #succ(#0()) -> #pos(#s(#0())) #succ(#neg(#s(#0()))) -> #0() #succ(#neg(#s(#s(x)))) -> #neg(#s(x)) #succ(#pos(#s(x))) -> #pos(#s(#s(x))) dyade(l1,l2) -> dyade#1(l1,l2) dyade#1(dd(x,xs),l2) -> dd(mult(x,l2),dyade(xs,l2)) dyade#1(nil(),l2) -> nil() mult(n,l) -> mult#1(l,n) mult(x,y) -> #mult(x,y) mult#1(dd(x,xs),n) -> dd(mult(n,x),mult(n,xs)) mult#1(nil(),n) -> nil() - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2,#add#/2,#mult#/2 ,#natadd#/2,#natmult#/2,#pred#/1,#succ#/1,dyade#/2,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1 ,dd/2,nil/0,c_1/0,c_2/1,c_3/2,c_4/1,c_5/2,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/1,c_15/0 ,c_16/1,c_17/0,c_18/2,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/2,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natadd#,#natmult#,#pred#,#succ#,dyade# ,dyade#1#,mult#,mult#1#} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:#add#(#neg(#s(#s(x))),y) -> c_3(#pred#(#add(#pos(#s(x)),y)),#add#(#pos(#s(x)),y)) -->_2 #add#(#pos(#s(#0())),y) -> c_4(#succ#(y)):16 -->_2 #add#(#pos(#s(#s(x))),y) -> c_5(#succ#(#add(#pos(#s(x)),y)),#add#(#pos(#s(x)),y)):2 -->_1 #pred#(#pos(#s(#s(x)))) -> c_22():27 -->_1 #pred#(#pos(#s(#0()))) -> c_21():26 -->_1 #pred#(#neg(#s(x))) -> c_20():25 -->_1 #pred#(#0()) -> c_19():24 2:S:#add#(#pos(#s(#s(x))),y) -> c_5(#succ#(#add(#pos(#s(x)),y)),#add#(#pos(#s(x)),y)) -->_2 #add#(#pos(#s(#0())),y) -> c_4(#succ#(y)):16 -->_1 #succ#(#pos(#s(x))) -> c_26():31 -->_1 #succ#(#neg(#s(#s(x)))) -> c_25():30 -->_1 #succ#(#neg(#s(#0()))) -> c_24():29 -->_1 #succ#(#0()) -> c_23():28 -->_2 #add#(#pos(#s(#s(x))),y) -> c_5(#succ#(#add(#pos(#s(x)),y)),#add#(#pos(#s(x)),y)):2 3:S:#mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)) -->_1 #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)):8 -->_1 #natmult#(#0(),y) -> c_17():23 4:S:#mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)) -->_1 #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)):8 -->_1 #natmult#(#0(),y) -> c_17():23 5:S:#mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)) -->_1 #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)):8 -->_1 #natmult#(#0(),y) -> c_17():23 6:S:#mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)) -->_1 #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)):8 -->_1 #natmult#(#0(),y) -> c_17():23 7:S:#natadd#(#s(x),y) -> c_16(#natadd#(x,y)) -->_1 #natadd#(#0(),y) -> c_15():22 -->_1 #natadd#(#s(x),y) -> c_16(#natadd#(x,y)):7 8:S:#natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)) -->_2 #natmult#(#0(),y) -> c_17():23 -->_1 #natadd#(#0(),y) -> c_15():22 -->_2 #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)):8 -->_1 #natadd#(#s(x),y) -> c_16(#natadd#(x,y)):7 9:S:dyade#(l1,l2) -> c_27(dyade#1#(l1,l2)) -->_1 dyade#1#(dd(x,xs),l2) -> c_28(mult#(x,l2),dyade#(xs,l2)):10 -->_1 dyade#1#(nil(),l2) -> c_29():32 10:S:dyade#1#(dd(x,xs),l2) -> c_28(mult#(x,l2),dyade#(xs,l2)) -->_1 mult#(x,y) -> c_31(#mult#(x,y)):12 -->_1 mult#(n,l) -> c_30(mult#1#(l,n)):11 -->_2 dyade#(l1,l2) -> c_27(dyade#1#(l1,l2)):9 11:S:mult#(n,l) -> c_30(mult#1#(l,n)) -->_1 mult#1#(dd(x,xs),n) -> c_32(mult#(n,x),mult#(n,xs)):13 -->_1 mult#1#(nil(),n) -> c_33():33 12:S:mult#(x,y) -> c_31(#mult#(x,y)) -->_1 #mult#(#pos(x),#0()) -> c_12():21 -->_1 #mult#(#neg(x),#0()) -> c_9():20 -->_1 #mult#(#0(),#pos(y)) -> c_8():19 -->_1 #mult#(#0(),#neg(y)) -> c_7():18 -->_1 #mult#(#0(),#0()) -> c_6():17 -->_1 #mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)):6 -->_1 #mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)):5 -->_1 #mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)):4 -->_1 #mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)):3 13:S:mult#1#(dd(x,xs),n) -> c_32(mult#(n,x),mult#(n,xs)) -->_2 mult#(x,y) -> c_31(#mult#(x,y)):12 -->_1 mult#(x,y) -> c_31(#mult#(x,y)):12 -->_2 mult#(n,l) -> c_30(mult#1#(l,n)):11 -->_1 mult#(n,l) -> c_30(mult#1#(l,n)):11 14:W:#add#(#0(),y) -> c_1() 15:W:#add#(#neg(#s(#0())),y) -> c_2(#pred#(y)) -->_1 #pred#(#pos(#s(#s(x)))) -> c_22():27 -->_1 #pred#(#pos(#s(#0()))) -> c_21():26 -->_1 #pred#(#neg(#s(x))) -> c_20():25 -->_1 #pred#(#0()) -> c_19():24 16:W:#add#(#pos(#s(#0())),y) -> c_4(#succ#(y)) -->_1 #succ#(#pos(#s(x))) -> c_26():31 -->_1 #succ#(#neg(#s(#s(x)))) -> c_25():30 -->_1 #succ#(#neg(#s(#0()))) -> c_24():29 -->_1 #succ#(#0()) -> c_23():28 17:W:#mult#(#0(),#0()) -> c_6() 18:W:#mult#(#0(),#neg(y)) -> c_7() 19:W:#mult#(#0(),#pos(y)) -> c_8() 20:W:#mult#(#neg(x),#0()) -> c_9() 21:W:#mult#(#pos(x),#0()) -> c_12() 22:W:#natadd#(#0(),y) -> c_15() 23:W:#natmult#(#0(),y) -> c_17() 24:W:#pred#(#0()) -> c_19() 25:W:#pred#(#neg(#s(x))) -> c_20() 26:W:#pred#(#pos(#s(#0()))) -> c_21() 27:W:#pred#(#pos(#s(#s(x)))) -> c_22() 28:W:#succ#(#0()) -> c_23() 29:W:#succ#(#neg(#s(#0()))) -> c_24() 30:W:#succ#(#neg(#s(#s(x)))) -> c_25() 31:W:#succ#(#pos(#s(x))) -> c_26() 32:W:dyade#1#(nil(),l2) -> c_29() 33:W:mult#1#(nil(),n) -> c_33() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 15: #add#(#neg(#s(#0())),y) -> c_2(#pred#(y)) 14: #add#(#0(),y) -> c_1() 32: dyade#1#(nil(),l2) -> c_29() 33: mult#1#(nil(),n) -> c_33() 17: #mult#(#0(),#0()) -> c_6() 18: #mult#(#0(),#neg(y)) -> c_7() 19: #mult#(#0(),#pos(y)) -> c_8() 20: #mult#(#neg(x),#0()) -> c_9() 21: #mult#(#pos(x),#0()) -> c_12() 22: #natadd#(#0(),y) -> c_15() 23: #natmult#(#0(),y) -> c_17() 24: #pred#(#0()) -> c_19() 25: #pred#(#neg(#s(x))) -> c_20() 26: #pred#(#pos(#s(#0()))) -> c_21() 27: #pred#(#pos(#s(#s(x)))) -> c_22() 16: #add#(#pos(#s(#0())),y) -> c_4(#succ#(y)) 28: #succ#(#0()) -> c_23() 29: #succ#(#neg(#s(#0()))) -> c_24() 30: #succ#(#neg(#s(#s(x)))) -> c_25() 31: #succ#(#pos(#s(x))) -> c_26() * Step 5: SimplifyRHS WORST_CASE(?,O(n^4)) + Considered Problem: - Strict DPs: #add#(#neg(#s(#s(x))),y) -> c_3(#pred#(#add(#pos(#s(x)),y)),#add#(#pos(#s(x)),y)) #add#(#pos(#s(#s(x))),y) -> c_5(#succ#(#add(#pos(#s(x)),y)),#add#(#pos(#s(x)),y)) #mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)) #mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)) #mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)) #mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)) #natadd#(#s(x),y) -> c_16(#natadd#(x,y)) #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)) dyade#(l1,l2) -> c_27(dyade#1#(l1,l2)) dyade#1#(dd(x,xs),l2) -> c_28(mult#(x,l2),dyade#(xs,l2)) mult#(n,l) -> c_30(mult#1#(l,n)) mult#(x,y) -> c_31(#mult#(x,y)) mult#1#(dd(x,xs),n) -> c_32(mult#(n,x),mult#(n,xs)) - Weak TRS: #add(#0(),y) -> y #add(#neg(#s(#0())),y) -> #pred(y) #add(#neg(#s(#s(x))),y) -> #pred(#add(#pos(#s(x)),y)) #add(#pos(#s(#0())),y) -> #succ(y) #add(#pos(#s(#s(x))),y) -> #succ(#add(#pos(#s(x)),y)) #mult(#0(),#0()) -> #0() #mult(#0(),#neg(y)) -> #0() #mult(#0(),#pos(y)) -> #0() #mult(#neg(x),#0()) -> #0() #mult(#neg(x),#neg(y)) -> #pos(#natmult(x,y)) #mult(#neg(x),#pos(y)) -> #neg(#natmult(x,y)) #mult(#pos(x),#0()) -> #0() #mult(#pos(x),#neg(y)) -> #neg(#natmult(x,y)) #mult(#pos(x),#pos(y)) -> #pos(#natmult(x,y)) #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) #pred(#0()) -> #neg(#s(#0())) #pred(#neg(#s(x))) -> #neg(#s(#s(x))) #pred(#pos(#s(#0()))) -> #0() #pred(#pos(#s(#s(x)))) -> #pos(#s(x)) #succ(#0()) -> #pos(#s(#0())) #succ(#neg(#s(#0()))) -> #0() #succ(#neg(#s(#s(x)))) -> #neg(#s(x)) #succ(#pos(#s(x))) -> #pos(#s(#s(x))) dyade(l1,l2) -> dyade#1(l1,l2) dyade#1(dd(x,xs),l2) -> dd(mult(x,l2),dyade(xs,l2)) dyade#1(nil(),l2) -> nil() mult(n,l) -> mult#1(l,n) mult(x,y) -> #mult(x,y) mult#1(dd(x,xs),n) -> dd(mult(n,x),mult(n,xs)) mult#1(nil(),n) -> nil() - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2,#add#/2,#mult#/2 ,#natadd#/2,#natmult#/2,#pred#/1,#succ#/1,dyade#/2,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1 ,dd/2,nil/0,c_1/0,c_2/1,c_3/2,c_4/1,c_5/2,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/1,c_15/0 ,c_16/1,c_17/0,c_18/2,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/2,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natadd#,#natmult#,#pred#,#succ#,dyade# ,dyade#1#,mult#,mult#1#} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:#add#(#neg(#s(#s(x))),y) -> c_3(#pred#(#add(#pos(#s(x)),y)),#add#(#pos(#s(x)),y)) -->_2 #add#(#pos(#s(#s(x))),y) -> c_5(#succ#(#add(#pos(#s(x)),y)),#add#(#pos(#s(x)),y)):2 2:S:#add#(#pos(#s(#s(x))),y) -> c_5(#succ#(#add(#pos(#s(x)),y)),#add#(#pos(#s(x)),y)) -->_2 #add#(#pos(#s(#s(x))),y) -> c_5(#succ#(#add(#pos(#s(x)),y)),#add#(#pos(#s(x)),y)):2 3:S:#mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)) -->_1 #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)):8 4:S:#mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)) -->_1 #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)):8 5:S:#mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)) -->_1 #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)):8 6:S:#mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)) -->_1 #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)):8 7:S:#natadd#(#s(x),y) -> c_16(#natadd#(x,y)) -->_1 #natadd#(#s(x),y) -> c_16(#natadd#(x,y)):7 8:S:#natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)) -->_2 #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)):8 -->_1 #natadd#(#s(x),y) -> c_16(#natadd#(x,y)):7 9:S:dyade#(l1,l2) -> c_27(dyade#1#(l1,l2)) -->_1 dyade#1#(dd(x,xs),l2) -> c_28(mult#(x,l2),dyade#(xs,l2)):10 10:S:dyade#1#(dd(x,xs),l2) -> c_28(mult#(x,l2),dyade#(xs,l2)) -->_1 mult#(x,y) -> c_31(#mult#(x,y)):12 -->_1 mult#(n,l) -> c_30(mult#1#(l,n)):11 -->_2 dyade#(l1,l2) -> c_27(dyade#1#(l1,l2)):9 11:S:mult#(n,l) -> c_30(mult#1#(l,n)) -->_1 mult#1#(dd(x,xs),n) -> c_32(mult#(n,x),mult#(n,xs)):13 12:S:mult#(x,y) -> c_31(#mult#(x,y)) -->_1 #mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)):6 -->_1 #mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)):5 -->_1 #mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)):4 -->_1 #mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)):3 13:S:mult#1#(dd(x,xs),n) -> c_32(mult#(n,x),mult#(n,xs)) -->_2 mult#(x,y) -> c_31(#mult#(x,y)):12 -->_1 mult#(x,y) -> c_31(#mult#(x,y)):12 -->_2 mult#(n,l) -> c_30(mult#1#(l,n)):11 -->_1 mult#(n,l) -> c_30(mult#1#(l,n)):11 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: #add#(#neg(#s(#s(x))),y) -> c_3(#add#(#pos(#s(x)),y)) #add#(#pos(#s(#s(x))),y) -> c_5(#add#(#pos(#s(x)),y)) * Step 6: UsableRules WORST_CASE(?,O(n^4)) + Considered Problem: - Strict DPs: #add#(#neg(#s(#s(x))),y) -> c_3(#add#(#pos(#s(x)),y)) #add#(#pos(#s(#s(x))),y) -> c_5(#add#(#pos(#s(x)),y)) #mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)) #mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)) #mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)) #mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)) #natadd#(#s(x),y) -> c_16(#natadd#(x,y)) #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)) dyade#(l1,l2) -> c_27(dyade#1#(l1,l2)) dyade#1#(dd(x,xs),l2) -> c_28(mult#(x,l2),dyade#(xs,l2)) mult#(n,l) -> c_30(mult#1#(l,n)) mult#(x,y) -> c_31(#mult#(x,y)) mult#1#(dd(x,xs),n) -> c_32(mult#(n,x),mult#(n,xs)) - Weak TRS: #add(#0(),y) -> y #add(#neg(#s(#0())),y) -> #pred(y) #add(#neg(#s(#s(x))),y) -> #pred(#add(#pos(#s(x)),y)) #add(#pos(#s(#0())),y) -> #succ(y) #add(#pos(#s(#s(x))),y) -> #succ(#add(#pos(#s(x)),y)) #mult(#0(),#0()) -> #0() #mult(#0(),#neg(y)) -> #0() #mult(#0(),#pos(y)) -> #0() #mult(#neg(x),#0()) -> #0() #mult(#neg(x),#neg(y)) -> #pos(#natmult(x,y)) #mult(#neg(x),#pos(y)) -> #neg(#natmult(x,y)) #mult(#pos(x),#0()) -> #0() #mult(#pos(x),#neg(y)) -> #neg(#natmult(x,y)) #mult(#pos(x),#pos(y)) -> #pos(#natmult(x,y)) #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) #pred(#0()) -> #neg(#s(#0())) #pred(#neg(#s(x))) -> #neg(#s(#s(x))) #pred(#pos(#s(#0()))) -> #0() #pred(#pos(#s(#s(x)))) -> #pos(#s(x)) #succ(#0()) -> #pos(#s(#0())) #succ(#neg(#s(#0()))) -> #0() #succ(#neg(#s(#s(x)))) -> #neg(#s(x)) #succ(#pos(#s(x))) -> #pos(#s(#s(x))) dyade(l1,l2) -> dyade#1(l1,l2) dyade#1(dd(x,xs),l2) -> dd(mult(x,l2),dyade(xs,l2)) dyade#1(nil(),l2) -> nil() mult(n,l) -> mult#1(l,n) mult(x,y) -> #mult(x,y) mult#1(dd(x,xs),n) -> dd(mult(n,x),mult(n,xs)) mult#1(nil(),n) -> nil() - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2,#add#/2,#mult#/2 ,#natadd#/2,#natmult#/2,#pred#/1,#succ#/1,dyade#/2,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1 ,dd/2,nil/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/1,c_15/0 ,c_16/1,c_17/0,c_18/2,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/2,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natadd#,#natmult#,#pred#,#succ#,dyade# ,dyade#1#,mult#,mult#1#} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) #add#(#neg(#s(#s(x))),y) -> c_3(#add#(#pos(#s(x)),y)) #add#(#pos(#s(#s(x))),y) -> c_5(#add#(#pos(#s(x)),y)) #mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)) #mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)) #mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)) #mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)) #natadd#(#s(x),y) -> c_16(#natadd#(x,y)) #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)) dyade#(l1,l2) -> c_27(dyade#1#(l1,l2)) dyade#1#(dd(x,xs),l2) -> c_28(mult#(x,l2),dyade#(xs,l2)) mult#(n,l) -> c_30(mult#1#(l,n)) mult#(x,y) -> c_31(#mult#(x,y)) mult#1#(dd(x,xs),n) -> c_32(mult#(n,x),mult#(n,xs)) * Step 7: RemoveHeads WORST_CASE(?,O(n^4)) + Considered Problem: - Strict DPs: #add#(#neg(#s(#s(x))),y) -> c_3(#add#(#pos(#s(x)),y)) #add#(#pos(#s(#s(x))),y) -> c_5(#add#(#pos(#s(x)),y)) #mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)) #mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)) #mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)) #mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)) #natadd#(#s(x),y) -> c_16(#natadd#(x,y)) #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)) dyade#(l1,l2) -> c_27(dyade#1#(l1,l2)) dyade#1#(dd(x,xs),l2) -> c_28(mult#(x,l2),dyade#(xs,l2)) mult#(n,l) -> c_30(mult#1#(l,n)) mult#(x,y) -> c_31(#mult#(x,y)) mult#1#(dd(x,xs),n) -> c_32(mult#(n,x),mult#(n,xs)) - Weak TRS: #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2,#add#/2,#mult#/2 ,#natadd#/2,#natmult#/2,#pred#/1,#succ#/1,dyade#/2,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1 ,dd/2,nil/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/1,c_15/0 ,c_16/1,c_17/0,c_18/2,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/2,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natadd#,#natmult#,#pred#,#succ#,dyade# ,dyade#1#,mult#,mult#1#} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:#add#(#neg(#s(#s(x))),y) -> c_3(#add#(#pos(#s(x)),y)) -->_1 #add#(#pos(#s(#s(x))),y) -> c_5(#add#(#pos(#s(x)),y)):2 2:S:#add#(#pos(#s(#s(x))),y) -> c_5(#add#(#pos(#s(x)),y)) -->_1 #add#(#pos(#s(#s(x))),y) -> c_5(#add#(#pos(#s(x)),y)):2 3:S:#mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)) -->_1 #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)):8 4:S:#mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)) -->_1 #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)):8 5:S:#mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)) -->_1 #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)):8 6:S:#mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)) -->_1 #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)):8 7:S:#natadd#(#s(x),y) -> c_16(#natadd#(x,y)) -->_1 #natadd#(#s(x),y) -> c_16(#natadd#(x,y)):7 8:S:#natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)) -->_2 #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)):8 -->_1 #natadd#(#s(x),y) -> c_16(#natadd#(x,y)):7 9:S:dyade#(l1,l2) -> c_27(dyade#1#(l1,l2)) -->_1 dyade#1#(dd(x,xs),l2) -> c_28(mult#(x,l2),dyade#(xs,l2)):10 10:S:dyade#1#(dd(x,xs),l2) -> c_28(mult#(x,l2),dyade#(xs,l2)) -->_1 mult#(x,y) -> c_31(#mult#(x,y)):12 -->_1 mult#(n,l) -> c_30(mult#1#(l,n)):11 -->_2 dyade#(l1,l2) -> c_27(dyade#1#(l1,l2)):9 11:S:mult#(n,l) -> c_30(mult#1#(l,n)) -->_1 mult#1#(dd(x,xs),n) -> c_32(mult#(n,x),mult#(n,xs)):13 12:S:mult#(x,y) -> c_31(#mult#(x,y)) -->_1 #mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)):6 -->_1 #mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)):5 -->_1 #mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)):4 -->_1 #mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)):3 13:S:mult#1#(dd(x,xs),n) -> c_32(mult#(n,x),mult#(n,xs)) -->_2 mult#(x,y) -> c_31(#mult#(x,y)):12 -->_1 mult#(x,y) -> c_31(#mult#(x,y)):12 -->_2 mult#(n,l) -> c_30(mult#1#(l,n)):11 -->_1 mult#(n,l) -> c_30(mult#1#(l,n)):11 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). [(1,#add#(#neg(#s(#s(x))),y) -> c_3(#add#(#pos(#s(x)),y)))] * Step 8: DecomposeDG WORST_CASE(?,O(n^4)) + Considered Problem: - Strict DPs: #add#(#pos(#s(#s(x))),y) -> c_5(#add#(#pos(#s(x)),y)) #mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)) #mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)) #mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)) #mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)) #natadd#(#s(x),y) -> c_16(#natadd#(x,y)) #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)) dyade#(l1,l2) -> c_27(dyade#1#(l1,l2)) dyade#1#(dd(x,xs),l2) -> c_28(mult#(x,l2),dyade#(xs,l2)) mult#(n,l) -> c_30(mult#1#(l,n)) mult#(x,y) -> c_31(#mult#(x,y)) mult#1#(dd(x,xs),n) -> c_32(mult#(n,x),mult#(n,xs)) - Weak TRS: #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2,#add#/2,#mult#/2 ,#natadd#/2,#natmult#/2,#pred#/1,#succ#/1,dyade#/2,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1 ,dd/2,nil/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/1,c_15/0 ,c_16/1,c_17/0,c_18/2,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/2,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natadd#,#natmult#,#pred#,#succ#,dyade# ,dyade#1#,mult#,mult#1#} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component #add#(#pos(#s(#s(x))),y) -> c_5(#add#(#pos(#s(x)),y)) dyade#(l1,l2) -> c_27(dyade#1#(l1,l2)) dyade#1#(dd(x,xs),l2) -> c_28(mult#(x,l2),dyade#(xs,l2)) and a lower component #mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)) #mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)) #mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)) #mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)) #natadd#(#s(x),y) -> c_16(#natadd#(x,y)) #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)) mult#(n,l) -> c_30(mult#1#(l,n)) mult#(x,y) -> c_31(#mult#(x,y)) mult#1#(dd(x,xs),n) -> c_32(mult#(n,x),mult#(n,xs)) Further, following extension rules are added to the lower component. #add#(#pos(#s(#s(x))),y) -> #add#(#pos(#s(x)),y) dyade#(l1,l2) -> dyade#1#(l1,l2) dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2) dyade#1#(dd(x,xs),l2) -> mult#(x,l2) ** Step 8.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: #add#(#pos(#s(#s(x))),y) -> c_5(#add#(#pos(#s(x)),y)) dyade#(l1,l2) -> c_27(dyade#1#(l1,l2)) dyade#1#(dd(x,xs),l2) -> c_28(mult#(x,l2),dyade#(xs,l2)) - Weak TRS: #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2,#add#/2,#mult#/2 ,#natadd#/2,#natmult#/2,#pred#/1,#succ#/1,dyade#/2,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1 ,dd/2,nil/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/1,c_15/0 ,c_16/1,c_17/0,c_18/2,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/2,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natadd#,#natmult#,#pred#,#succ#,dyade# ,dyade#1#,mult#,mult#1#} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:#add#(#pos(#s(#s(x))),y) -> c_5(#add#(#pos(#s(x)),y)) -->_1 #add#(#pos(#s(#s(x))),y) -> c_5(#add#(#pos(#s(x)),y)):1 2:S:dyade#(l1,l2) -> c_27(dyade#1#(l1,l2)) -->_1 dyade#1#(dd(x,xs),l2) -> c_28(mult#(x,l2),dyade#(xs,l2)):3 3:S:dyade#1#(dd(x,xs),l2) -> c_28(mult#(x,l2),dyade#(xs,l2)) -->_2 dyade#(l1,l2) -> c_27(dyade#1#(l1,l2)):2 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: dyade#1#(dd(x,xs),l2) -> c_28(dyade#(xs,l2)) ** Step 8.a:2: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: #add#(#pos(#s(#s(x))),y) -> c_5(#add#(#pos(#s(x)),y)) dyade#(l1,l2) -> c_27(dyade#1#(l1,l2)) dyade#1#(dd(x,xs),l2) -> c_28(dyade#(xs,l2)) - Weak TRS: #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2,#add#/2,#mult#/2 ,#natadd#/2,#natmult#/2,#pred#/1,#succ#/1,dyade#/2,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1 ,dd/2,nil/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/1,c_15/0 ,c_16/1,c_17/0,c_18/2,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/1,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natadd#,#natmult#,#pred#,#succ#,dyade# ,dyade#1#,mult#,mult#1#} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: #add#(#pos(#s(#s(x))),y) -> c_5(#add#(#pos(#s(x)),y)) dyade#(l1,l2) -> c_27(dyade#1#(l1,l2)) dyade#1#(dd(x,xs),l2) -> c_28(dyade#(xs,l2)) ** Step 8.a:3: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: #add#(#pos(#s(#s(x))),y) -> c_5(#add#(#pos(#s(x)),y)) dyade#(l1,l2) -> c_27(dyade#1#(l1,l2)) dyade#1#(dd(x,xs),l2) -> c_28(dyade#(xs,l2)) - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2,#add#/2,#mult#/2 ,#natadd#/2,#natmult#/2,#pred#/1,#succ#/1,dyade#/2,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1 ,dd/2,nil/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/1,c_15/0 ,c_16/1,c_17/0,c_18/2,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/1,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natadd#,#natmult#,#pred#,#succ#,dyade# ,dyade#1#,mult#,mult#1#} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_5) = {1}, uargs(c_27) = {1}, uargs(c_28) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#add) = [0] p(#mult) = [0] p(#natadd) = [0] p(#natmult) = [0] p(#neg) = [1] x1 + [0] p(#pos) = [1] x1 + [0] p(#pred) = [1] x1 + [0] p(#s) = [1] x1 + [0] p(#succ) = [0] p(dd) = [1] x1 + [1] x2 + [2] p(dyade) = [0] p(dyade#1) = [0] p(mult) = [0] p(mult#1) = [0] p(nil) = [0] p(#add#) = [0] p(#mult#) = [1] p(#natadd#) = [0] p(#natmult#) = [0] p(#pred#) = [0] p(#succ#) = [0] p(dyade#) = [4] x1 + [0] p(dyade#1#) = [4] x1 + [1] p(mult#) = [1] x2 + [0] p(mult#1#) = [8] x1 + [1] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [1] x1 + [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [1] x1 + [0] p(c_28) = [1] x1 + [0] p(c_29) = [0] p(c_30) = [0] p(c_31) = [0] p(c_32) = [0] p(c_33) = [0] Following rules are strictly oriented: dyade#1#(dd(x,xs),l2) = [4] x + [4] xs + [9] > [4] xs + [0] = c_28(dyade#(xs,l2)) Following rules are (at-least) weakly oriented: #add#(#pos(#s(#s(x))),y) = [0] >= [0] = c_5(#add#(#pos(#s(x)),y)) dyade#(l1,l2) = [4] l1 + [0] >= [4] l1 + [1] = c_27(dyade#1#(l1,l2)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 8.a:4: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: #add#(#pos(#s(#s(x))),y) -> c_5(#add#(#pos(#s(x)),y)) dyade#(l1,l2) -> c_27(dyade#1#(l1,l2)) - Weak DPs: dyade#1#(dd(x,xs),l2) -> c_28(dyade#(xs,l2)) - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2,#add#/2,#mult#/2 ,#natadd#/2,#natmult#/2,#pred#/1,#succ#/1,dyade#/2,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1 ,dd/2,nil/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/1,c_15/0 ,c_16/1,c_17/0,c_18/2,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/1,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natadd#,#natmult#,#pred#,#succ#,dyade# ,dyade#1#,mult#,mult#1#} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_5) = {1}, uargs(c_27) = {1}, uargs(c_28) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#add) = [0] p(#mult) = [0] p(#natadd) = [0] p(#natmult) = [0] p(#neg) = [1] x1 + [1] p(#pos) = [1] x1 + [1] p(#pred) = [0] p(#s) = [1] x1 + [0] p(#succ) = [0] p(dd) = [1] x1 + [1] x2 + [9] p(dyade) = [0] p(dyade#1) = [0] p(mult) = [0] p(mult#1) = [0] p(nil) = [0] p(#add#) = [10] x1 + [0] p(#mult#) = [0] p(#natadd#) = [0] p(#natmult#) = [0] p(#pred#) = [0] p(#succ#) = [0] p(dyade#) = [1] x1 + [9] p(dyade#1#) = [1] x1 + [0] p(mult#) = [0] p(mult#1#) = [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [1] x1 + [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [1] x1 + [0] p(c_28) = [1] x1 + [0] p(c_29) = [0] p(c_30) = [0] p(c_31) = [0] p(c_32) = [0] p(c_33) = [0] Following rules are strictly oriented: dyade#(l1,l2) = [1] l1 + [9] > [1] l1 + [0] = c_27(dyade#1#(l1,l2)) Following rules are (at-least) weakly oriented: #add#(#pos(#s(#s(x))),y) = [10] x + [10] >= [10] x + [10] = c_5(#add#(#pos(#s(x)),y)) dyade#1#(dd(x,xs),l2) = [1] x + [1] xs + [9] >= [1] xs + [9] = c_28(dyade#(xs,l2)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 8.a:5: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: #add#(#pos(#s(#s(x))),y) -> c_5(#add#(#pos(#s(x)),y)) - Weak DPs: dyade#(l1,l2) -> c_27(dyade#1#(l1,l2)) dyade#1#(dd(x,xs),l2) -> c_28(dyade#(xs,l2)) - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2,#add#/2,#mult#/2 ,#natadd#/2,#natmult#/2,#pred#/1,#succ#/1,dyade#/2,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1 ,dd/2,nil/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/1,c_15/0 ,c_16/1,c_17/0,c_18/2,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/1,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natadd#,#natmult#,#pred#,#succ#,dyade# ,dyade#1#,mult#,mult#1#} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_5) = {1}, uargs(c_27) = {1}, uargs(c_28) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#add) = [0] p(#mult) = [0] p(#natadd) = [0] p(#natmult) = [0] p(#neg) = [1] x1 + [0] p(#pos) = [1] x1 + [15] p(#pred) = [0] p(#s) = [1] x1 + [1] p(#succ) = [0] p(dd) = [1] x1 + [1] x2 + [1] p(dyade) = [0] p(dyade#1) = [0] p(mult) = [0] p(mult#1) = [0] p(nil) = [0] p(#add#) = [1] x1 + [4] x2 + [0] p(#mult#) = [8] x1 + [1] x2 + [0] p(#natadd#) = [8] x1 + [1] x2 + [1] p(#natmult#) = [1] x1 + [8] x2 + [4] p(#pred#) = [1] p(#succ#) = [1] x1 + [1] p(dyade#) = [5] x1 + [9] p(dyade#1#) = [5] x1 + [4] p(mult#) = [1] x1 + [1] x2 + [0] p(mult#1#) = [1] x1 + [1] p(c_1) = [8] p(c_2) = [1] x1 + [0] p(c_3) = [4] p(c_4) = [0] p(c_5) = [1] x1 + [0] p(c_6) = [1] p(c_7) = [1] p(c_8) = [1] p(c_9) = [2] p(c_10) = [2] x1 + [0] p(c_11) = [8] x1 + [1] p(c_12) = [0] p(c_13) = [2] x1 + [1] p(c_14) = [2] x1 + [0] p(c_15) = [2] p(c_16) = [1] x1 + [1] p(c_17) = [8] p(c_18) = [1] p(c_19) = [1] p(c_20) = [1] p(c_21) = [2] p(c_22) = [1] p(c_23) = [1] p(c_24) = [4] p(c_25) = [1] p(c_26) = [1] p(c_27) = [1] x1 + [4] p(c_28) = [1] x1 + [0] p(c_29) = [2] p(c_30) = [1] x1 + [2] p(c_31) = [8] x1 + [4] p(c_32) = [1] x1 + [2] x2 + [0] p(c_33) = [2] Following rules are strictly oriented: #add#(#pos(#s(#s(x))),y) = [1] x + [4] y + [17] > [1] x + [4] y + [16] = c_5(#add#(#pos(#s(x)),y)) Following rules are (at-least) weakly oriented: dyade#(l1,l2) = [5] l1 + [9] >= [5] l1 + [8] = c_27(dyade#1#(l1,l2)) dyade#1#(dd(x,xs),l2) = [5] x + [5] xs + [9] >= [5] xs + [9] = c_28(dyade#(xs,l2)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 8.a:6: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: #add#(#pos(#s(#s(x))),y) -> c_5(#add#(#pos(#s(x)),y)) dyade#(l1,l2) -> c_27(dyade#1#(l1,l2)) dyade#1#(dd(x,xs),l2) -> c_28(dyade#(xs,l2)) - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2,#add#/2,#mult#/2 ,#natadd#/2,#natmult#/2,#pred#/1,#succ#/1,dyade#/2,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1 ,dd/2,nil/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/1,c_15/0 ,c_16/1,c_17/0,c_18/2,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/1,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natadd#,#natmult#,#pred#,#succ#,dyade# ,dyade#1#,mult#,mult#1#} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). ** Step 8.b:1: DecomposeDG WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: #mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)) #mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)) #mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)) #mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)) #natadd#(#s(x),y) -> c_16(#natadd#(x,y)) #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)) mult#(n,l) -> c_30(mult#1#(l,n)) mult#(x,y) -> c_31(#mult#(x,y)) mult#1#(dd(x,xs),n) -> c_32(mult#(n,x),mult#(n,xs)) - Weak DPs: #add#(#pos(#s(#s(x))),y) -> #add#(#pos(#s(x)),y) dyade#(l1,l2) -> dyade#1#(l1,l2) dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2) dyade#1#(dd(x,xs),l2) -> mult#(x,l2) - Weak TRS: #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2,#add#/2,#mult#/2 ,#natadd#/2,#natmult#/2,#pred#/1,#succ#/1,dyade#/2,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1 ,dd/2,nil/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/1,c_15/0 ,c_16/1,c_17/0,c_18/2,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/2,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natadd#,#natmult#,#pred#,#succ#,dyade# ,dyade#1#,mult#,mult#1#} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component #add#(#pos(#s(#s(x))),y) -> #add#(#pos(#s(x)),y) dyade#(l1,l2) -> dyade#1#(l1,l2) dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2) dyade#1#(dd(x,xs),l2) -> mult#(x,l2) mult#(n,l) -> c_30(mult#1#(l,n)) mult#1#(dd(x,xs),n) -> c_32(mult#(n,x),mult#(n,xs)) and a lower component #mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)) #mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)) #mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)) #mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)) #natadd#(#s(x),y) -> c_16(#natadd#(x,y)) #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)) mult#(x,y) -> c_31(#mult#(x,y)) Further, following extension rules are added to the lower component. #add#(#pos(#s(#s(x))),y) -> #add#(#pos(#s(x)),y) dyade#(l1,l2) -> dyade#1#(l1,l2) dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2) dyade#1#(dd(x,xs),l2) -> mult#(x,l2) mult#(n,l) -> mult#1#(l,n) mult#1#(dd(x,xs),n) -> mult#(n,x) mult#1#(dd(x,xs),n) -> mult#(n,xs) *** Step 8.b:1.a:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: dyade#1#(dd(x,xs),l2) -> mult#(x,l2) mult#(n,l) -> c_30(mult#1#(l,n)) mult#1#(dd(x,xs),n) -> c_32(mult#(n,x),mult#(n,xs)) - Weak DPs: #add#(#pos(#s(#s(x))),y) -> #add#(#pos(#s(x)),y) dyade#(l1,l2) -> dyade#1#(l1,l2) dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2) - Weak TRS: #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2,#add#/2,#mult#/2 ,#natadd#/2,#natmult#/2,#pred#/1,#succ#/1,dyade#/2,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1 ,dd/2,nil/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/1,c_15/0 ,c_16/1,c_17/0,c_18/2,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/2,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natadd#,#natmult#,#pred#,#succ#,dyade# ,dyade#1#,mult#,mult#1#} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:dyade#1#(dd(x,xs),l2) -> mult#(x,l2) -->_1 mult#(n,l) -> c_30(mult#1#(l,n)):2 2:S:mult#(n,l) -> c_30(mult#1#(l,n)) -->_1 mult#1#(dd(x,xs),n) -> c_32(mult#(n,x),mult#(n,xs)):3 3:S:mult#1#(dd(x,xs),n) -> c_32(mult#(n,x),mult#(n,xs)) -->_2 mult#(n,l) -> c_30(mult#1#(l,n)):2 -->_1 mult#(n,l) -> c_30(mult#1#(l,n)):2 4:W:#add#(#pos(#s(#s(x))),y) -> #add#(#pos(#s(x)),y) -->_1 #add#(#pos(#s(#s(x))),y) -> #add#(#pos(#s(x)),y):4 5:W:dyade#(l1,l2) -> dyade#1#(l1,l2) -->_1 dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2):6 -->_1 dyade#1#(dd(x,xs),l2) -> mult#(x,l2):1 6:W:dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2) -->_1 dyade#(l1,l2) -> dyade#1#(l1,l2):5 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 4: #add#(#pos(#s(#s(x))),y) -> #add#(#pos(#s(x)),y) *** Step 8.b:1.a:2: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: dyade#1#(dd(x,xs),l2) -> mult#(x,l2) mult#(n,l) -> c_30(mult#1#(l,n)) mult#1#(dd(x,xs),n) -> c_32(mult#(n,x),mult#(n,xs)) - Weak DPs: dyade#(l1,l2) -> dyade#1#(l1,l2) dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2) - Weak TRS: #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2,#add#/2,#mult#/2 ,#natadd#/2,#natmult#/2,#pred#/1,#succ#/1,dyade#/2,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1 ,dd/2,nil/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/1,c_15/0 ,c_16/1,c_17/0,c_18/2,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/2,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natadd#,#natmult#,#pred#,#succ#,dyade# ,dyade#1#,mult#,mult#1#} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: dyade#(l1,l2) -> dyade#1#(l1,l2) dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2) dyade#1#(dd(x,xs),l2) -> mult#(x,l2) mult#(n,l) -> c_30(mult#1#(l,n)) mult#1#(dd(x,xs),n) -> c_32(mult#(n,x),mult#(n,xs)) *** Step 8.b:1.a:3: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: dyade#1#(dd(x,xs),l2) -> mult#(x,l2) mult#(n,l) -> c_30(mult#1#(l,n)) mult#1#(dd(x,xs),n) -> c_32(mult#(n,x),mult#(n,xs)) - Weak DPs: dyade#(l1,l2) -> dyade#1#(l1,l2) dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2) - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2,#add#/2,#mult#/2 ,#natadd#/2,#natmult#/2,#pred#/1,#succ#/1,dyade#/2,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1 ,dd/2,nil/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/1,c_15/0 ,c_16/1,c_17/0,c_18/2,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/2,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natadd#,#natmult#,#pred#,#succ#,dyade# ,dyade#1#,mult#,mult#1#} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_30) = {1}, uargs(c_32) = {1,2} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#add) = [0] p(#mult) = [1] x1 + [0] p(#natadd) = [1] p(#natmult) = [1] x1 + [0] p(#neg) = [1] x1 + [1] p(#pos) = [1] x1 + [0] p(#pred) = [1] x1 + [0] p(#s) = [1] x1 + [0] p(#succ) = [0] p(dd) = [1] x1 + [1] x2 + [2] p(dyade) = [0] p(dyade#1) = [0] p(mult) = [0] p(mult#1) = [0] p(nil) = [0] p(#add#) = [0] p(#mult#) = [0] p(#natadd#) = [0] p(#natmult#) = [4] x2 + [0] p(#pred#) = [1] x1 + [0] p(#succ#) = [8] x1 + [0] p(dyade#) = [10] x1 + [1] p(dyade#1#) = [10] x1 + [0] p(mult#) = [1] p(mult#1#) = [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [0] p(c_28) = [0] p(c_29) = [0] p(c_30) = [1] x1 + [0] p(c_31) = [0] p(c_32) = [1] x1 + [1] x2 + [0] p(c_33) = [0] Following rules are strictly oriented: dyade#1#(dd(x,xs),l2) = [10] x + [10] xs + [20] > [1] = mult#(x,l2) mult#(n,l) = [1] > [0] = c_30(mult#1#(l,n)) Following rules are (at-least) weakly oriented: dyade#(l1,l2) = [10] l1 + [1] >= [10] l1 + [0] = dyade#1#(l1,l2) dyade#1#(dd(x,xs),l2) = [10] x + [10] xs + [20] >= [10] xs + [1] = dyade#(xs,l2) mult#1#(dd(x,xs),n) = [0] >= [2] = c_32(mult#(n,x),mult#(n,xs)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 8.b:1.a:4: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: mult#1#(dd(x,xs),n) -> c_32(mult#(n,x),mult#(n,xs)) - Weak DPs: dyade#(l1,l2) -> dyade#1#(l1,l2) dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2) dyade#1#(dd(x,xs),l2) -> mult#(x,l2) mult#(n,l) -> c_30(mult#1#(l,n)) - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2,#add#/2,#mult#/2 ,#natadd#/2,#natmult#/2,#pred#/1,#succ#/1,dyade#/2,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1 ,dd/2,nil/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/1,c_15/0 ,c_16/1,c_17/0,c_18/2,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/2,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natadd#,#natmult#,#pred#,#succ#,dyade# ,dyade#1#,mult#,mult#1#} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_30) = {1}, uargs(c_32) = {1,2} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [1] p(#add) = [1] x2 + [1] p(#mult) = [2] x2 + [8] p(#natadd) = [1] x1 + [1] x2 + [0] p(#natmult) = [0] p(#neg) = [1] x1 + [0] p(#pos) = [1] x1 + [0] p(#pred) = [0] p(#s) = [1] p(#succ) = [2] x1 + [1] p(dd) = [1] x1 + [1] x2 + [2] p(dyade) = [0] p(dyade#1) = [0] p(mult) = [0] p(mult#1) = [0] p(nil) = [0] p(#add#) = [0] p(#mult#) = [0] p(#natadd#) = [0] p(#natmult#) = [0] p(#pred#) = [0] p(#succ#) = [0] p(dyade#) = [4] x1 + [8] x2 + [8] p(dyade#1#) = [4] x1 + [8] x2 + [8] p(mult#) = [4] x2 + [4] p(mult#1#) = [4] x1 + [3] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [2] p(c_28) = [1] x2 + [0] p(c_29) = [0] p(c_30) = [1] x1 + [1] p(c_31) = [1] x1 + [1] p(c_32) = [1] x1 + [1] x2 + [2] p(c_33) = [1] Following rules are strictly oriented: mult#1#(dd(x,xs),n) = [4] x + [4] xs + [11] > [4] x + [4] xs + [10] = c_32(mult#(n,x),mult#(n,xs)) Following rules are (at-least) weakly oriented: dyade#(l1,l2) = [4] l1 + [8] l2 + [8] >= [4] l1 + [8] l2 + [8] = dyade#1#(l1,l2) dyade#1#(dd(x,xs),l2) = [8] l2 + [4] x + [4] xs + [16] >= [8] l2 + [4] xs + [8] = dyade#(xs,l2) dyade#1#(dd(x,xs),l2) = [8] l2 + [4] x + [4] xs + [16] >= [4] l2 + [4] = mult#(x,l2) mult#(n,l) = [4] l + [4] >= [4] l + [4] = c_30(mult#1#(l,n)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 8.b:1.a:5: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: dyade#(l1,l2) -> dyade#1#(l1,l2) dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2) dyade#1#(dd(x,xs),l2) -> mult#(x,l2) mult#(n,l) -> c_30(mult#1#(l,n)) mult#1#(dd(x,xs),n) -> c_32(mult#(n,x),mult#(n,xs)) - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2,#add#/2,#mult#/2 ,#natadd#/2,#natmult#/2,#pred#/1,#succ#/1,dyade#/2,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1 ,dd/2,nil/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/1,c_15/0 ,c_16/1,c_17/0,c_18/2,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/2,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natadd#,#natmult#,#pred#,#succ#,dyade# ,dyade#1#,mult#,mult#1#} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). *** Step 8.b:1.b:1: DecomposeDG WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: #mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)) #mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)) #mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)) #mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)) #natadd#(#s(x),y) -> c_16(#natadd#(x,y)) #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)) mult#(x,y) -> c_31(#mult#(x,y)) - Weak DPs: #add#(#pos(#s(#s(x))),y) -> #add#(#pos(#s(x)),y) dyade#(l1,l2) -> dyade#1#(l1,l2) dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2) dyade#1#(dd(x,xs),l2) -> mult#(x,l2) mult#(n,l) -> mult#1#(l,n) mult#1#(dd(x,xs),n) -> mult#(n,x) mult#1#(dd(x,xs),n) -> mult#(n,xs) - Weak TRS: #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2,#add#/2,#mult#/2 ,#natadd#/2,#natmult#/2,#pred#/1,#succ#/1,dyade#/2,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1 ,dd/2,nil/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/1,c_15/0 ,c_16/1,c_17/0,c_18/2,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/2,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natadd#,#natmult#,#pred#,#succ#,dyade# ,dyade#1#,mult#,mult#1#} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component #add#(#pos(#s(#s(x))),y) -> #add#(#pos(#s(x)),y) #mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)) #mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)) #mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)) #mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)) #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)) dyade#(l1,l2) -> dyade#1#(l1,l2) dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2) dyade#1#(dd(x,xs),l2) -> mult#(x,l2) mult#(n,l) -> mult#1#(l,n) mult#(x,y) -> c_31(#mult#(x,y)) mult#1#(dd(x,xs),n) -> mult#(n,x) mult#1#(dd(x,xs),n) -> mult#(n,xs) and a lower component #natadd#(#s(x),y) -> c_16(#natadd#(x,y)) Further, following extension rules are added to the lower component. #add#(#pos(#s(#s(x))),y) -> #add#(#pos(#s(x)),y) #mult#(#neg(x),#neg(y)) -> #natmult#(x,y) #mult#(#neg(x),#pos(y)) -> #natmult#(x,y) #mult#(#pos(x),#neg(y)) -> #natmult#(x,y) #mult#(#pos(x),#pos(y)) -> #natmult#(x,y) #natmult#(#s(x),y) -> #natadd#(y,#natmult(x,y)) #natmult#(#s(x),y) -> #natmult#(x,y) dyade#(l1,l2) -> dyade#1#(l1,l2) dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2) dyade#1#(dd(x,xs),l2) -> mult#(x,l2) mult#(n,l) -> mult#1#(l,n) mult#(x,y) -> #mult#(x,y) mult#1#(dd(x,xs),n) -> mult#(n,x) mult#1#(dd(x,xs),n) -> mult#(n,xs) **** Step 8.b:1.b:1.a:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: #mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)) #mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)) #mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)) #mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)) #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)) mult#(x,y) -> c_31(#mult#(x,y)) - Weak DPs: #add#(#pos(#s(#s(x))),y) -> #add#(#pos(#s(x)),y) dyade#(l1,l2) -> dyade#1#(l1,l2) dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2) dyade#1#(dd(x,xs),l2) -> mult#(x,l2) mult#(n,l) -> mult#1#(l,n) mult#1#(dd(x,xs),n) -> mult#(n,x) mult#1#(dd(x,xs),n) -> mult#(n,xs) - Weak TRS: #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2,#add#/2,#mult#/2 ,#natadd#/2,#natmult#/2,#pred#/1,#succ#/1,dyade#/2,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1 ,dd/2,nil/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/1,c_15/0 ,c_16/1,c_17/0,c_18/2,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/2,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natadd#,#natmult#,#pred#,#succ#,dyade# ,dyade#1#,mult#,mult#1#} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:#mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)) -->_1 #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)):5 2:S:#mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)) -->_1 #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)):5 3:S:#mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)) -->_1 #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)):5 4:S:#mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)) -->_1 #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)):5 5:S:#natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)) -->_2 #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)):5 6:S:mult#(x,y) -> c_31(#mult#(x,y)) -->_1 #mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)):4 -->_1 #mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)):3 -->_1 #mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)):2 -->_1 #mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)):1 7:W:#add#(#pos(#s(#s(x))),y) -> #add#(#pos(#s(x)),y) -->_1 #add#(#pos(#s(#s(x))),y) -> #add#(#pos(#s(x)),y):7 8:W:dyade#(l1,l2) -> dyade#1#(l1,l2) -->_1 dyade#1#(dd(x,xs),l2) -> mult#(x,l2):10 -->_1 dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2):9 9:W:dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2) -->_1 dyade#(l1,l2) -> dyade#1#(l1,l2):8 10:W:dyade#1#(dd(x,xs),l2) -> mult#(x,l2) -->_1 mult#(n,l) -> mult#1#(l,n):11 -->_1 mult#(x,y) -> c_31(#mult#(x,y)):6 11:W:mult#(n,l) -> mult#1#(l,n) -->_1 mult#1#(dd(x,xs),n) -> mult#(n,xs):13 -->_1 mult#1#(dd(x,xs),n) -> mult#(n,x):12 12:W:mult#1#(dd(x,xs),n) -> mult#(n,x) -->_1 mult#(n,l) -> mult#1#(l,n):11 -->_1 mult#(x,y) -> c_31(#mult#(x,y)):6 13:W:mult#1#(dd(x,xs),n) -> mult#(n,xs) -->_1 mult#(n,l) -> mult#1#(l,n):11 -->_1 mult#(x,y) -> c_31(#mult#(x,y)):6 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 7: #add#(#pos(#s(#s(x))),y) -> #add#(#pos(#s(x)),y) **** Step 8.b:1.b:1.a:2: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: #mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)) #mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)) #mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)) #mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)) #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)) mult#(x,y) -> c_31(#mult#(x,y)) - Weak DPs: dyade#(l1,l2) -> dyade#1#(l1,l2) dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2) dyade#1#(dd(x,xs),l2) -> mult#(x,l2) mult#(n,l) -> mult#1#(l,n) mult#1#(dd(x,xs),n) -> mult#(n,x) mult#1#(dd(x,xs),n) -> mult#(n,xs) - Weak TRS: #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2,#add#/2,#mult#/2 ,#natadd#/2,#natmult#/2,#pred#/1,#succ#/1,dyade#/2,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1 ,dd/2,nil/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/1,c_15/0 ,c_16/1,c_17/0,c_18/2,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/2,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natadd#,#natmult#,#pred#,#succ#,dyade# ,dyade#1#,mult#,mult#1#} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:#mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)) -->_1 #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)):5 2:S:#mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)) -->_1 #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)):5 3:S:#mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)) -->_1 #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)):5 4:S:#mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)) -->_1 #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)):5 5:S:#natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)) -->_2 #natmult#(#s(x),y) -> c_18(#natadd#(y,#natmult(x,y)),#natmult#(x,y)):5 6:S:mult#(x,y) -> c_31(#mult#(x,y)) -->_1 #mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)):4 -->_1 #mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)):3 -->_1 #mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)):2 -->_1 #mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)):1 8:W:dyade#(l1,l2) -> dyade#1#(l1,l2) -->_1 dyade#1#(dd(x,xs),l2) -> mult#(x,l2):10 -->_1 dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2):9 9:W:dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2) -->_1 dyade#(l1,l2) -> dyade#1#(l1,l2):8 10:W:dyade#1#(dd(x,xs),l2) -> mult#(x,l2) -->_1 mult#(n,l) -> mult#1#(l,n):11 -->_1 mult#(x,y) -> c_31(#mult#(x,y)):6 11:W:mult#(n,l) -> mult#1#(l,n) -->_1 mult#1#(dd(x,xs),n) -> mult#(n,xs):13 -->_1 mult#1#(dd(x,xs),n) -> mult#(n,x):12 12:W:mult#1#(dd(x,xs),n) -> mult#(n,x) -->_1 mult#(n,l) -> mult#1#(l,n):11 -->_1 mult#(x,y) -> c_31(#mult#(x,y)):6 13:W:mult#1#(dd(x,xs),n) -> mult#(n,xs) -->_1 mult#(n,l) -> mult#1#(l,n):11 -->_1 mult#(x,y) -> c_31(#mult#(x,y)):6 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: #natmult#(#s(x),y) -> c_18(#natmult#(x,y)) **** Step 8.b:1.b:1.a:3: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: #mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)) #mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)) #mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)) #mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)) #natmult#(#s(x),y) -> c_18(#natmult#(x,y)) mult#(x,y) -> c_31(#mult#(x,y)) - Weak DPs: dyade#(l1,l2) -> dyade#1#(l1,l2) dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2) dyade#1#(dd(x,xs),l2) -> mult#(x,l2) mult#(n,l) -> mult#1#(l,n) mult#1#(dd(x,xs),n) -> mult#(n,x) mult#1#(dd(x,xs),n) -> mult#(n,xs) - Weak TRS: #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2,#add#/2,#mult#/2 ,#natadd#/2,#natmult#/2,#pred#/1,#succ#/1,dyade#/2,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1 ,dd/2,nil/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/1,c_15/0 ,c_16/1,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/2,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natadd#,#natmult#,#pred#,#succ#,dyade# ,dyade#1#,mult#,mult#1#} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: #mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)) #mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)) #mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)) #mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)) #natmult#(#s(x),y) -> c_18(#natmult#(x,y)) dyade#(l1,l2) -> dyade#1#(l1,l2) dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2) dyade#1#(dd(x,xs),l2) -> mult#(x,l2) mult#(n,l) -> mult#1#(l,n) mult#(x,y) -> c_31(#mult#(x,y)) mult#1#(dd(x,xs),n) -> mult#(n,x) mult#1#(dd(x,xs),n) -> mult#(n,xs) **** Step 8.b:1.b:1.a:4: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: #mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)) #mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)) #mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)) #mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)) #natmult#(#s(x),y) -> c_18(#natmult#(x,y)) mult#(x,y) -> c_31(#mult#(x,y)) - Weak DPs: dyade#(l1,l2) -> dyade#1#(l1,l2) dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2) dyade#1#(dd(x,xs),l2) -> mult#(x,l2) mult#(n,l) -> mult#1#(l,n) mult#1#(dd(x,xs),n) -> mult#(n,x) mult#1#(dd(x,xs),n) -> mult#(n,xs) - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2,#add#/2,#mult#/2 ,#natadd#/2,#natmult#/2,#pred#/1,#succ#/1,dyade#/2,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1 ,dd/2,nil/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/1,c_15/0 ,c_16/1,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/2,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natadd#,#natmult#,#pred#,#succ#,dyade# ,dyade#1#,mult#,mult#1#} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_10) = {1}, uargs(c_11) = {1}, uargs(c_13) = {1}, uargs(c_14) = {1}, uargs(c_18) = {1}, uargs(c_31) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#add) = [0] p(#mult) = [0] p(#natadd) = [0] p(#natmult) = [0] p(#neg) = [1] x1 + [0] p(#pos) = [0] p(#pred) = [0] p(#s) = [1] x1 + [0] p(#succ) = [0] p(dd) = [1] x2 + [4] p(dyade) = [0] p(dyade#1) = [0] p(mult) = [0] p(mult#1) = [0] p(nil) = [0] p(#add#) = [0] p(#mult#) = [3] p(#natadd#) = [0] p(#natmult#) = [0] p(#pred#) = [0] p(#succ#) = [0] p(dyade#) = [3] x1 + [4] p(dyade#1#) = [3] x1 + [0] p(mult#) = [1] p(mult#1#) = [1] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [2] p(c_10) = [1] x1 + [2] p(c_11) = [1] x1 + [0] p(c_12) = [0] p(c_13) = [1] x1 + [1] p(c_14) = [1] x1 + [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [1] x1 + [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [0] p(c_28) = [0] p(c_29) = [0] p(c_30) = [0] p(c_31) = [1] x1 + [0] p(c_32) = [0] p(c_33) = [0] Following rules are strictly oriented: #mult#(#neg(x),#neg(y)) = [3] > [2] = c_10(#natmult#(x,y)) #mult#(#neg(x),#pos(y)) = [3] > [0] = c_11(#natmult#(x,y)) #mult#(#pos(x),#neg(y)) = [3] > [1] = c_13(#natmult#(x,y)) #mult#(#pos(x),#pos(y)) = [3] > [0] = c_14(#natmult#(x,y)) Following rules are (at-least) weakly oriented: #natmult#(#s(x),y) = [0] >= [0] = c_18(#natmult#(x,y)) dyade#(l1,l2) = [3] l1 + [4] >= [3] l1 + [0] = dyade#1#(l1,l2) dyade#1#(dd(x,xs),l2) = [3] xs + [12] >= [3] xs + [4] = dyade#(xs,l2) dyade#1#(dd(x,xs),l2) = [3] xs + [12] >= [1] = mult#(x,l2) mult#(n,l) = [1] >= [1] = mult#1#(l,n) mult#(x,y) = [1] >= [3] = c_31(#mult#(x,y)) mult#1#(dd(x,xs),n) = [1] >= [1] = mult#(n,x) mult#1#(dd(x,xs),n) = [1] >= [1] = mult#(n,xs) Further, it can be verified that all rules not oriented are covered by the weightgap condition. **** Step 8.b:1.b:1.a:5: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: #natmult#(#s(x),y) -> c_18(#natmult#(x,y)) mult#(x,y) -> c_31(#mult#(x,y)) - Weak DPs: #mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)) #mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)) #mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)) #mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)) dyade#(l1,l2) -> dyade#1#(l1,l2) dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2) dyade#1#(dd(x,xs),l2) -> mult#(x,l2) mult#(n,l) -> mult#1#(l,n) mult#1#(dd(x,xs),n) -> mult#(n,x) mult#1#(dd(x,xs),n) -> mult#(n,xs) - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2,#add#/2,#mult#/2 ,#natadd#/2,#natmult#/2,#pred#/1,#succ#/1,dyade#/2,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1 ,dd/2,nil/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/1,c_15/0 ,c_16/1,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/2,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natadd#,#natmult#,#pred#,#succ#,dyade# ,dyade#1#,mult#,mult#1#} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_10) = {1}, uargs(c_11) = {1}, uargs(c_13) = {1}, uargs(c_14) = {1}, uargs(c_18) = {1}, uargs(c_31) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#add) = [0] p(#mult) = [0] p(#natadd) = [0] p(#natmult) = [0] p(#neg) = [1] p(#pos) = [1] p(#pred) = [0] p(#s) = [1] x1 + [0] p(#succ) = [0] p(dd) = [1] x1 + [1] x2 + [0] p(dyade) = [0] p(dyade#1) = [0] p(mult) = [0] p(mult#1) = [0] p(nil) = [0] p(#add#) = [0] p(#mult#) = [1] x2 + [0] p(#natadd#) = [0] p(#natmult#) = [1] p(#pred#) = [0] p(#succ#) = [0] p(dyade#) = [1] x2 + [1] p(dyade#1#) = [1] x2 + [1] p(mult#) = [1] x2 + [1] p(mult#1#) = [1] x1 + [1] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [1] x1 + [0] p(c_11) = [1] x1 + [0] p(c_12) = [0] p(c_13) = [1] x1 + [0] p(c_14) = [1] x1 + [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [1] x1 + [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [0] p(c_28) = [0] p(c_29) = [0] p(c_30) = [0] p(c_31) = [1] x1 + [0] p(c_32) = [0] p(c_33) = [0] Following rules are strictly oriented: mult#(x,y) = [1] y + [1] > [1] y + [0] = c_31(#mult#(x,y)) Following rules are (at-least) weakly oriented: #mult#(#neg(x),#neg(y)) = [1] >= [1] = c_10(#natmult#(x,y)) #mult#(#neg(x),#pos(y)) = [1] >= [1] = c_11(#natmult#(x,y)) #mult#(#pos(x),#neg(y)) = [1] >= [1] = c_13(#natmult#(x,y)) #mult#(#pos(x),#pos(y)) = [1] >= [1] = c_14(#natmult#(x,y)) #natmult#(#s(x),y) = [1] >= [1] = c_18(#natmult#(x,y)) dyade#(l1,l2) = [1] l2 + [1] >= [1] l2 + [1] = dyade#1#(l1,l2) dyade#1#(dd(x,xs),l2) = [1] l2 + [1] >= [1] l2 + [1] = dyade#(xs,l2) dyade#1#(dd(x,xs),l2) = [1] l2 + [1] >= [1] l2 + [1] = mult#(x,l2) mult#(n,l) = [1] l + [1] >= [1] l + [1] = mult#1#(l,n) mult#1#(dd(x,xs),n) = [1] x + [1] xs + [1] >= [1] x + [1] = mult#(n,x) mult#1#(dd(x,xs),n) = [1] x + [1] xs + [1] >= [1] xs + [1] = mult#(n,xs) Further, it can be verified that all rules not oriented are covered by the weightgap condition. **** Step 8.b:1.b:1.a:6: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: #natmult#(#s(x),y) -> c_18(#natmult#(x,y)) - Weak DPs: #mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)) #mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)) #mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)) #mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)) dyade#(l1,l2) -> dyade#1#(l1,l2) dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2) dyade#1#(dd(x,xs),l2) -> mult#(x,l2) mult#(n,l) -> mult#1#(l,n) mult#(x,y) -> c_31(#mult#(x,y)) mult#1#(dd(x,xs),n) -> mult#(n,x) mult#1#(dd(x,xs),n) -> mult#(n,xs) - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2,#add#/2,#mult#/2 ,#natadd#/2,#natmult#/2,#pred#/1,#succ#/1,dyade#/2,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1 ,dd/2,nil/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/1,c_15/0 ,c_16/1,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/2,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natadd#,#natmult#,#pred#,#succ#,dyade# ,dyade#1#,mult#,mult#1#} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_10) = {1}, uargs(c_11) = {1}, uargs(c_13) = {1}, uargs(c_14) = {1}, uargs(c_18) = {1}, uargs(c_31) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#add) = [0] p(#mult) = [0] p(#natadd) = [0] p(#natmult) = [0] p(#neg) = [1] x1 + [0] p(#pos) = [1] x1 + [0] p(#pred) = [0] p(#s) = [1] x1 + [5] p(#succ) = [0] p(dd) = [1] x1 + [1] x2 + [0] p(dyade) = [0] p(dyade#1) = [0] p(mult) = [0] p(mult#1) = [0] p(nil) = [0] p(#add#) = [0] p(#mult#) = [1] x1 + [0] p(#natadd#) = [0] p(#natmult#) = [1] x1 + [0] p(#pred#) = [0] p(#succ#) = [1] p(dyade#) = [1] x1 + [0] p(dyade#1#) = [1] x1 + [0] p(mult#) = [1] x1 + [0] p(mult#1#) = [1] x2 + [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [1] x1 + [0] p(c_11) = [1] x1 + [0] p(c_12) = [1] p(c_13) = [1] x1 + [0] p(c_14) = [1] x1 + [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [1] x1 + [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [0] p(c_28) = [0] p(c_29) = [0] p(c_30) = [0] p(c_31) = [1] x1 + [0] p(c_32) = [0] p(c_33) = [0] Following rules are strictly oriented: #natmult#(#s(x),y) = [1] x + [5] > [1] x + [0] = c_18(#natmult#(x,y)) Following rules are (at-least) weakly oriented: #mult#(#neg(x),#neg(y)) = [1] x + [0] >= [1] x + [0] = c_10(#natmult#(x,y)) #mult#(#neg(x),#pos(y)) = [1] x + [0] >= [1] x + [0] = c_11(#natmult#(x,y)) #mult#(#pos(x),#neg(y)) = [1] x + [0] >= [1] x + [0] = c_13(#natmult#(x,y)) #mult#(#pos(x),#pos(y)) = [1] x + [0] >= [1] x + [0] = c_14(#natmult#(x,y)) dyade#(l1,l2) = [1] l1 + [0] >= [1] l1 + [0] = dyade#1#(l1,l2) dyade#1#(dd(x,xs),l2) = [1] x + [1] xs + [0] >= [1] xs + [0] = dyade#(xs,l2) dyade#1#(dd(x,xs),l2) = [1] x + [1] xs + [0] >= [1] x + [0] = mult#(x,l2) mult#(n,l) = [1] n + [0] >= [1] n + [0] = mult#1#(l,n) mult#(x,y) = [1] x + [0] >= [1] x + [0] = c_31(#mult#(x,y)) mult#1#(dd(x,xs),n) = [1] n + [0] >= [1] n + [0] = mult#(n,x) mult#1#(dd(x,xs),n) = [1] n + [0] >= [1] n + [0] = mult#(n,xs) Further, it can be verified that all rules not oriented are covered by the weightgap condition. **** Step 8.b:1.b:1.a:7: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: #mult#(#neg(x),#neg(y)) -> c_10(#natmult#(x,y)) #mult#(#neg(x),#pos(y)) -> c_11(#natmult#(x,y)) #mult#(#pos(x),#neg(y)) -> c_13(#natmult#(x,y)) #mult#(#pos(x),#pos(y)) -> c_14(#natmult#(x,y)) #natmult#(#s(x),y) -> c_18(#natmult#(x,y)) dyade#(l1,l2) -> dyade#1#(l1,l2) dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2) dyade#1#(dd(x,xs),l2) -> mult#(x,l2) mult#(n,l) -> mult#1#(l,n) mult#(x,y) -> c_31(#mult#(x,y)) mult#1#(dd(x,xs),n) -> mult#(n,x) mult#1#(dd(x,xs),n) -> mult#(n,xs) - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2,#add#/2,#mult#/2 ,#natadd#/2,#natmult#/2,#pred#/1,#succ#/1,dyade#/2,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1 ,dd/2,nil/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/1,c_15/0 ,c_16/1,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/2,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natadd#,#natmult#,#pred#,#succ#,dyade# ,dyade#1#,mult#,mult#1#} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). **** Step 8.b:1.b:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: #natadd#(#s(x),y) -> c_16(#natadd#(x,y)) - Weak DPs: #add#(#pos(#s(#s(x))),y) -> #add#(#pos(#s(x)),y) #mult#(#neg(x),#neg(y)) -> #natmult#(x,y) #mult#(#neg(x),#pos(y)) -> #natmult#(x,y) #mult#(#pos(x),#neg(y)) -> #natmult#(x,y) #mult#(#pos(x),#pos(y)) -> #natmult#(x,y) #natmult#(#s(x),y) -> #natadd#(y,#natmult(x,y)) #natmult#(#s(x),y) -> #natmult#(x,y) dyade#(l1,l2) -> dyade#1#(l1,l2) dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2) dyade#1#(dd(x,xs),l2) -> mult#(x,l2) mult#(n,l) -> mult#1#(l,n) mult#(x,y) -> #mult#(x,y) mult#1#(dd(x,xs),n) -> mult#(n,x) mult#1#(dd(x,xs),n) -> mult#(n,xs) - Weak TRS: #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2,#add#/2,#mult#/2 ,#natadd#/2,#natmult#/2,#pred#/1,#succ#/1,dyade#/2,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1 ,dd/2,nil/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/1,c_15/0 ,c_16/1,c_17/0,c_18/2,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/2,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natadd#,#natmult#,#pred#,#succ#,dyade# ,dyade#1#,mult#,mult#1#} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:#natadd#(#s(x),y) -> c_16(#natadd#(x,y)) -->_1 #natadd#(#s(x),y) -> c_16(#natadd#(x,y)):1 2:W:#add#(#pos(#s(#s(x))),y) -> #add#(#pos(#s(x)),y) -->_1 #add#(#pos(#s(#s(x))),y) -> #add#(#pos(#s(x)),y):2 3:W:#mult#(#neg(x),#neg(y)) -> #natmult#(x,y) -->_1 #natmult#(#s(x),y) -> #natmult#(x,y):8 -->_1 #natmult#(#s(x),y) -> #natadd#(y,#natmult(x,y)):7 4:W:#mult#(#neg(x),#pos(y)) -> #natmult#(x,y) -->_1 #natmult#(#s(x),y) -> #natmult#(x,y):8 -->_1 #natmult#(#s(x),y) -> #natadd#(y,#natmult(x,y)):7 5:W:#mult#(#pos(x),#neg(y)) -> #natmult#(x,y) -->_1 #natmult#(#s(x),y) -> #natmult#(x,y):8 -->_1 #natmult#(#s(x),y) -> #natadd#(y,#natmult(x,y)):7 6:W:#mult#(#pos(x),#pos(y)) -> #natmult#(x,y) -->_1 #natmult#(#s(x),y) -> #natmult#(x,y):8 -->_1 #natmult#(#s(x),y) -> #natadd#(y,#natmult(x,y)):7 7:W:#natmult#(#s(x),y) -> #natadd#(y,#natmult(x,y)) -->_1 #natadd#(#s(x),y) -> c_16(#natadd#(x,y)):1 8:W:#natmult#(#s(x),y) -> #natmult#(x,y) -->_1 #natmult#(#s(x),y) -> #natmult#(x,y):8 -->_1 #natmult#(#s(x),y) -> #natadd#(y,#natmult(x,y)):7 9:W:dyade#(l1,l2) -> dyade#1#(l1,l2) -->_1 dyade#1#(dd(x,xs),l2) -> mult#(x,l2):11 -->_1 dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2):10 10:W:dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2) -->_1 dyade#(l1,l2) -> dyade#1#(l1,l2):9 11:W:dyade#1#(dd(x,xs),l2) -> mult#(x,l2) -->_1 mult#(x,y) -> #mult#(x,y):13 -->_1 mult#(n,l) -> mult#1#(l,n):12 12:W:mult#(n,l) -> mult#1#(l,n) -->_1 mult#1#(dd(x,xs),n) -> mult#(n,xs):15 -->_1 mult#1#(dd(x,xs),n) -> mult#(n,x):14 13:W:mult#(x,y) -> #mult#(x,y) -->_1 #mult#(#pos(x),#pos(y)) -> #natmult#(x,y):6 -->_1 #mult#(#pos(x),#neg(y)) -> #natmult#(x,y):5 -->_1 #mult#(#neg(x),#pos(y)) -> #natmult#(x,y):4 -->_1 #mult#(#neg(x),#neg(y)) -> #natmult#(x,y):3 14:W:mult#1#(dd(x,xs),n) -> mult#(n,x) -->_1 mult#(x,y) -> #mult#(x,y):13 -->_1 mult#(n,l) -> mult#1#(l,n):12 15:W:mult#1#(dd(x,xs),n) -> mult#(n,xs) -->_1 mult#(x,y) -> #mult#(x,y):13 -->_1 mult#(n,l) -> mult#1#(l,n):12 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 2: #add#(#pos(#s(#s(x))),y) -> #add#(#pos(#s(x)),y) **** Step 8.b:1.b:1.b:2: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: #natadd#(#s(x),y) -> c_16(#natadd#(x,y)) - Weak DPs: #mult#(#neg(x),#neg(y)) -> #natmult#(x,y) #mult#(#neg(x),#pos(y)) -> #natmult#(x,y) #mult#(#pos(x),#neg(y)) -> #natmult#(x,y) #mult#(#pos(x),#pos(y)) -> #natmult#(x,y) #natmult#(#s(x),y) -> #natadd#(y,#natmult(x,y)) #natmult#(#s(x),y) -> #natmult#(x,y) dyade#(l1,l2) -> dyade#1#(l1,l2) dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2) dyade#1#(dd(x,xs),l2) -> mult#(x,l2) mult#(n,l) -> mult#1#(l,n) mult#(x,y) -> #mult#(x,y) mult#1#(dd(x,xs),n) -> mult#(n,x) mult#1#(dd(x,xs),n) -> mult#(n,xs) - Weak TRS: #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2,#add#/2,#mult#/2 ,#natadd#/2,#natmult#/2,#pred#/1,#succ#/1,dyade#/2,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1 ,dd/2,nil/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/1,c_15/0 ,c_16/1,c_17/0,c_18/2,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/2,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natadd#,#natmult#,#pred#,#succ#,dyade# ,dyade#1#,mult#,mult#1#} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_16) = {1} Following symbols are considered usable: {#add#,#mult#,#natadd#,#natmult#,#pred#,#succ#,dyade#,dyade#1#,mult#,mult#1#} TcT has computed the following interpretation: p(#0) = [9] p(#add) = [0] p(#mult) = [0] p(#natadd) = [2] x1 + [0] p(#natmult) = [1] x1 + [0] p(#neg) = [1] x1 + [1] p(#pos) = [1] x1 + [1] p(#pred) = [0] p(#s) = [1] x1 + [4] p(#succ) = [0] p(dd) = [1] x1 + [1] x2 + [0] p(dyade) = [0] p(dyade#1) = [0] p(mult) = [0] p(mult#1) = [0] p(nil) = [1] p(#add#) = [0] p(#mult#) = [1] x2 + [0] p(#natadd#) = [1] x1 + [0] p(#natmult#) = [1] x2 + [1] p(#pred#) = [2] p(#succ#) = [1] x1 + [0] p(dyade#) = [3] x2 + [0] p(dyade#1#) = [3] x2 + [0] p(mult#) = [2] x2 + [0] p(mult#1#) = [2] x1 + [0] p(c_1) = [1] p(c_2) = [8] p(c_3) = [1] x1 + [1] p(c_4) = [1] x1 + [0] p(c_5) = [2] x1 + [2] p(c_6) = [2] p(c_7) = [1] p(c_8) = [1] p(c_9) = [0] p(c_10) = [1] x1 + [0] p(c_11) = [1] x1 + [0] p(c_12) = [1] p(c_13) = [1] x1 + [2] p(c_14) = [1] x1 + [0] p(c_15) = [2] p(c_16) = [1] x1 + [2] p(c_17) = [8] p(c_18) = [1] x1 + [1] x2 + [1] p(c_19) = [1] p(c_20) = [1] p(c_21) = [0] p(c_22) = [0] p(c_23) = [8] p(c_24) = [1] p(c_25) = [1] p(c_26) = [1] p(c_27) = [0] p(c_28) = [1] x1 + [1] p(c_29) = [1] p(c_30) = [1] x1 + [8] p(c_31) = [1] x1 + [2] p(c_32) = [1] p(c_33) = [0] Following rules are strictly oriented: #natadd#(#s(x),y) = [1] x + [4] > [1] x + [2] = c_16(#natadd#(x,y)) Following rules are (at-least) weakly oriented: #mult#(#neg(x),#neg(y)) = [1] y + [1] >= [1] y + [1] = #natmult#(x,y) #mult#(#neg(x),#pos(y)) = [1] y + [1] >= [1] y + [1] = #natmult#(x,y) #mult#(#pos(x),#neg(y)) = [1] y + [1] >= [1] y + [1] = #natmult#(x,y) #mult#(#pos(x),#pos(y)) = [1] y + [1] >= [1] y + [1] = #natmult#(x,y) #natmult#(#s(x),y) = [1] y + [1] >= [1] y + [0] = #natadd#(y,#natmult(x,y)) #natmult#(#s(x),y) = [1] y + [1] >= [1] y + [1] = #natmult#(x,y) dyade#(l1,l2) = [3] l2 + [0] >= [3] l2 + [0] = dyade#1#(l1,l2) dyade#1#(dd(x,xs),l2) = [3] l2 + [0] >= [3] l2 + [0] = dyade#(xs,l2) dyade#1#(dd(x,xs),l2) = [3] l2 + [0] >= [2] l2 + [0] = mult#(x,l2) mult#(n,l) = [2] l + [0] >= [2] l + [0] = mult#1#(l,n) mult#(x,y) = [2] y + [0] >= [1] y + [0] = #mult#(x,y) mult#1#(dd(x,xs),n) = [2] x + [2] xs + [0] >= [2] x + [0] = mult#(n,x) mult#1#(dd(x,xs),n) = [2] x + [2] xs + [0] >= [2] xs + [0] = mult#(n,xs) **** Step 8.b:1.b:1.b:3: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: #mult#(#neg(x),#neg(y)) -> #natmult#(x,y) #mult#(#neg(x),#pos(y)) -> #natmult#(x,y) #mult#(#pos(x),#neg(y)) -> #natmult#(x,y) #mult#(#pos(x),#pos(y)) -> #natmult#(x,y) #natadd#(#s(x),y) -> c_16(#natadd#(x,y)) #natmult#(#s(x),y) -> #natadd#(y,#natmult(x,y)) #natmult#(#s(x),y) -> #natmult#(x,y) dyade#(l1,l2) -> dyade#1#(l1,l2) dyade#1#(dd(x,xs),l2) -> dyade#(xs,l2) dyade#1#(dd(x,xs),l2) -> mult#(x,l2) mult#(n,l) -> mult#1#(l,n) mult#(x,y) -> #mult#(x,y) mult#1#(dd(x,xs),n) -> mult#(n,x) mult#1#(dd(x,xs),n) -> mult#(n,xs) - Weak TRS: #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2,#add#/2,#mult#/2 ,#natadd#/2,#natmult#/2,#pred#/1,#succ#/1,dyade#/2,dyade#1#/2,mult#/2,mult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1 ,dd/2,nil/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/1,c_15/0 ,c_16/1,c_17/0,c_18/2,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/2,c_29/0,c_30/1 ,c_31/1,c_32/2,c_33/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natadd#,#natmult#,#pred#,#succ#,dyade# ,dyade#1#,mult#,mult#1#} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^4))