WORST_CASE(?,O(n^3)) * Step 1: DependencyPairs WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: *(@x,@y) -> #mult(@x,@y) +(@x,@y) -> #add(@x,@y) computeLine(@line,@m,@acc) -> computeLine#1(@line,@acc,@m) computeLine#1(::(@x,@xs),@acc,@m) -> computeLine#2(@m,@acc,@x,@xs) computeLine#1(nil(),@acc,@m) -> @acc computeLine#2(::(@l,@ls),@acc,@x,@xs) -> computeLine(@xs,@ls,lineMult(@x,@l,@acc)) computeLine#2(nil(),@acc,@x,@xs) -> nil() lineMult(@n,@l1,@l2) -> lineMult#1(@l1,@l2,@n) lineMult#1(::(@x,@xs),@l2,@n) -> lineMult#2(@l2,@n,@x,@xs) lineMult#1(nil(),@l2,@n) -> nil() lineMult#2(::(@y,@ys),@n,@x,@xs) -> ::(+(*(@x,@n),@y),lineMult(@n,@xs,@ys)) lineMult#2(nil(),@n,@x,@xs) -> ::(*(@x,@n),lineMult(@n,@xs,nil())) matrixMult(@m1,@m2) -> matrixMult#1(@m1,@m2) matrixMult#1(::(@l,@ls),@m2) -> ::(computeLine(@l,@m2,nil()),matrixMult(@ls,@m2)) matrixMult#1(nil(),@m2) -> nil() - 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)) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@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))) - Signature: {#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,+/2,computeLine/3,computeLine#1/3,computeLine#2/4,lineMult/3 ,lineMult#1/3,lineMult#2/4,matrixMult/2,matrixMult#1/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add,#mult,#natmult,#pred,#succ,*,+,computeLine ,computeLine#1,computeLine#2,lineMult,lineMult#1,lineMult#2,matrixMult,matrixMult#1} and constructors {#0 ,#neg,#pos,#s,::,nil} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs *#(@x,@y) -> c_1(#mult#(@x,@y)) +#(@x,@y) -> c_2(#add#(@x,@y)) computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)) computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs)) computeLine#1#(nil(),@acc,@m) -> c_5() computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) ,lineMult#(@x,@l,@acc)) computeLine#2#(nil(),@acc,@x,@xs) -> c_7() lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) lineMult#1#(::(@x,@xs),@l2,@n) -> c_9(lineMult#2#(@l2,@n,@x,@xs)) lineMult#1#(nil(),@l2,@n) -> c_10() lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(+#(*(@x,@n),@y),*#(@x,@n),lineMult#(@n,@xs,@ys)) lineMult#2#(nil(),@n,@x,@xs) -> c_12(*#(@x,@n),lineMult#(@n,@xs,nil())) matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2)) matrixMult#1#(::(@l,@ls),@m2) -> c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2)) matrixMult#1#(nil(),@m2) -> c_15() Weak DPs #add#(#0(),@y) -> c_16() #add#(#neg(#s(#0())),@y) -> c_17(#pred#(@y)) #add#(#neg(#s(#s(@x))),@y) -> c_18(#pred#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) #add#(#pos(#s(#0())),@y) -> c_19(#succ#(@y)) #add#(#pos(#s(#s(@x))),@y) -> c_20(#succ#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) #mult#(#0(),#0()) -> c_21() #mult#(#0(),#neg(@y)) -> c_22() #mult#(#0(),#pos(@y)) -> c_23() #mult#(#neg(@x),#0()) -> c_24() #mult#(#neg(@x),#neg(@y)) -> c_25(#natmult#(@x,@y)) #mult#(#neg(@x),#pos(@y)) -> c_26(#natmult#(@x,@y)) #mult#(#pos(@x),#0()) -> c_27() #mult#(#pos(@x),#neg(@y)) -> c_28(#natmult#(@x,@y)) #mult#(#pos(@x),#pos(@y)) -> c_29(#natmult#(@x,@y)) #natmult#(#0(),@y) -> c_30() #natmult#(#s(@x),@y) -> c_31(#add#(#pos(@y),#natmult(@x,@y)),#natmult#(@x,@y)) #pred#(#0()) -> c_32() #pred#(#neg(#s(@x))) -> c_33() #pred#(#pos(#s(#0()))) -> c_34() #pred#(#pos(#s(#s(@x)))) -> c_35() #succ#(#0()) -> c_36() #succ#(#neg(#s(#0()))) -> c_37() #succ#(#neg(#s(#s(@x)))) -> c_38() #succ#(#pos(#s(@x))) -> c_39() and mark the set of starting terms. * Step 2: PredecessorEstimation WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: *#(@x,@y) -> c_1(#mult#(@x,@y)) +#(@x,@y) -> c_2(#add#(@x,@y)) computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)) computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs)) computeLine#1#(nil(),@acc,@m) -> c_5() computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) ,lineMult#(@x,@l,@acc)) computeLine#2#(nil(),@acc,@x,@xs) -> c_7() lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) lineMult#1#(::(@x,@xs),@l2,@n) -> c_9(lineMult#2#(@l2,@n,@x,@xs)) lineMult#1#(nil(),@l2,@n) -> c_10() lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(+#(*(@x,@n),@y),*#(@x,@n),lineMult#(@n,@xs,@ys)) lineMult#2#(nil(),@n,@x,@xs) -> c_12(*#(@x,@n),lineMult#(@n,@xs,nil())) matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2)) matrixMult#1#(::(@l,@ls),@m2) -> c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2)) matrixMult#1#(nil(),@m2) -> c_15() - Weak DPs: #add#(#0(),@y) -> c_16() #add#(#neg(#s(#0())),@y) -> c_17(#pred#(@y)) #add#(#neg(#s(#s(@x))),@y) -> c_18(#pred#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) #add#(#pos(#s(#0())),@y) -> c_19(#succ#(@y)) #add#(#pos(#s(#s(@x))),@y) -> c_20(#succ#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) #mult#(#0(),#0()) -> c_21() #mult#(#0(),#neg(@y)) -> c_22() #mult#(#0(),#pos(@y)) -> c_23() #mult#(#neg(@x),#0()) -> c_24() #mult#(#neg(@x),#neg(@y)) -> c_25(#natmult#(@x,@y)) #mult#(#neg(@x),#pos(@y)) -> c_26(#natmult#(@x,@y)) #mult#(#pos(@x),#0()) -> c_27() #mult#(#pos(@x),#neg(@y)) -> c_28(#natmult#(@x,@y)) #mult#(#pos(@x),#pos(@y)) -> c_29(#natmult#(@x,@y)) #natmult#(#0(),@y) -> c_30() #natmult#(#s(@x),@y) -> c_31(#add#(#pos(@y),#natmult(@x,@y)),#natmult#(@x,@y)) #pred#(#0()) -> c_32() #pred#(#neg(#s(@x))) -> c_33() #pred#(#pos(#s(#0()))) -> c_34() #pred#(#pos(#s(#s(@x)))) -> c_35() #succ#(#0()) -> c_36() #succ#(#neg(#s(#0()))) -> c_37() #succ#(#neg(#s(#s(@x)))) -> c_38() #succ#(#pos(#s(@x))) -> c_39() - 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)) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@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))) *(@x,@y) -> #mult(@x,@y) +(@x,@y) -> #add(@x,@y) computeLine(@line,@m,@acc) -> computeLine#1(@line,@acc,@m) computeLine#1(::(@x,@xs),@acc,@m) -> computeLine#2(@m,@acc,@x,@xs) computeLine#1(nil(),@acc,@m) -> @acc computeLine#2(::(@l,@ls),@acc,@x,@xs) -> computeLine(@xs,@ls,lineMult(@x,@l,@acc)) computeLine#2(nil(),@acc,@x,@xs) -> nil() lineMult(@n,@l1,@l2) -> lineMult#1(@l1,@l2,@n) lineMult#1(::(@x,@xs),@l2,@n) -> lineMult#2(@l2,@n,@x,@xs) lineMult#1(nil(),@l2,@n) -> nil() lineMult#2(::(@y,@ys),@n,@x,@xs) -> ::(+(*(@x,@n),@y),lineMult(@n,@xs,@ys)) lineMult#2(nil(),@n,@x,@xs) -> ::(*(@x,@n),lineMult(@n,@xs,nil())) matrixMult(@m1,@m2) -> matrixMult#1(@m1,@m2) matrixMult#1(::(@l,@ls),@m2) -> ::(computeLine(@l,@m2,nil()),matrixMult(@ls,@m2)) matrixMult#1(nil(),@m2) -> nil() - Signature: {#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,+/2,computeLine/3,computeLine#1/3,computeLine#2/4,lineMult/3 ,lineMult#1/3,lineMult#2/4,matrixMult/2,matrixMult#1/2,#add#/2,#mult#/2,#natmult#/2,#pred#/1,#succ#/1,*#/2 ,+#/2,computeLine#/3,computeLine#1#/3,computeLine#2#/4,lineMult#/3,lineMult#1#/3,lineMult#2#/4,matrixMult#/2 ,matrixMult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/2,c_7/0,c_8/1 ,c_9/1,c_10/0,c_11/3,c_12/2,c_13/1,c_14/2,c_15/0,c_16/0,c_17/1,c_18/2,c_19/1,c_20/2,c_21/0,c_22/0,c_23/0 ,c_24/0,c_25/1,c_26/1,c_27/0,c_28/1,c_29/1,c_30/0,c_31/2,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0 ,c_39/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine# ,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult# ,matrixMult#1#} and constructors {#0,#neg,#pos,#s,::,nil} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,5,7,10,15} by application of Pre({1,2,5,7,10,15}) = {3,4,8,11,12,13}. Here rules are labelled as follows: 1: *#(@x,@y) -> c_1(#mult#(@x,@y)) 2: +#(@x,@y) -> c_2(#add#(@x,@y)) 3: computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)) 4: computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs)) 5: computeLine#1#(nil(),@acc,@m) -> c_5() 6: computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) ,lineMult#(@x,@l,@acc)) 7: computeLine#2#(nil(),@acc,@x,@xs) -> c_7() 8: lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) 9: lineMult#1#(::(@x,@xs),@l2,@n) -> c_9(lineMult#2#(@l2,@n,@x,@xs)) 10: lineMult#1#(nil(),@l2,@n) -> c_10() 11: lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(+#(*(@x,@n),@y),*#(@x,@n),lineMult#(@n,@xs,@ys)) 12: lineMult#2#(nil(),@n,@x,@xs) -> c_12(*#(@x,@n),lineMult#(@n,@xs,nil())) 13: matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2)) 14: matrixMult#1#(::(@l,@ls),@m2) -> c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2)) 15: matrixMult#1#(nil(),@m2) -> c_15() 16: #add#(#0(),@y) -> c_16() 17: #add#(#neg(#s(#0())),@y) -> c_17(#pred#(@y)) 18: #add#(#neg(#s(#s(@x))),@y) -> c_18(#pred#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) 19: #add#(#pos(#s(#0())),@y) -> c_19(#succ#(@y)) 20: #add#(#pos(#s(#s(@x))),@y) -> c_20(#succ#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) 21: #mult#(#0(),#0()) -> c_21() 22: #mult#(#0(),#neg(@y)) -> c_22() 23: #mult#(#0(),#pos(@y)) -> c_23() 24: #mult#(#neg(@x),#0()) -> c_24() 25: #mult#(#neg(@x),#neg(@y)) -> c_25(#natmult#(@x,@y)) 26: #mult#(#neg(@x),#pos(@y)) -> c_26(#natmult#(@x,@y)) 27: #mult#(#pos(@x),#0()) -> c_27() 28: #mult#(#pos(@x),#neg(@y)) -> c_28(#natmult#(@x,@y)) 29: #mult#(#pos(@x),#pos(@y)) -> c_29(#natmult#(@x,@y)) 30: #natmult#(#0(),@y) -> c_30() 31: #natmult#(#s(@x),@y) -> c_31(#add#(#pos(@y),#natmult(@x,@y)),#natmult#(@x,@y)) 32: #pred#(#0()) -> c_32() 33: #pred#(#neg(#s(@x))) -> c_33() 34: #pred#(#pos(#s(#0()))) -> c_34() 35: #pred#(#pos(#s(#s(@x)))) -> c_35() 36: #succ#(#0()) -> c_36() 37: #succ#(#neg(#s(#0()))) -> c_37() 38: #succ#(#neg(#s(#s(@x)))) -> c_38() 39: #succ#(#pos(#s(@x))) -> c_39() * Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)) computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs)) computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) ,lineMult#(@x,@l,@acc)) lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) lineMult#1#(::(@x,@xs),@l2,@n) -> c_9(lineMult#2#(@l2,@n,@x,@xs)) lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(+#(*(@x,@n),@y),*#(@x,@n),lineMult#(@n,@xs,@ys)) lineMult#2#(nil(),@n,@x,@xs) -> c_12(*#(@x,@n),lineMult#(@n,@xs,nil())) matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2)) matrixMult#1#(::(@l,@ls),@m2) -> c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2)) - Weak DPs: #add#(#0(),@y) -> c_16() #add#(#neg(#s(#0())),@y) -> c_17(#pred#(@y)) #add#(#neg(#s(#s(@x))),@y) -> c_18(#pred#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) #add#(#pos(#s(#0())),@y) -> c_19(#succ#(@y)) #add#(#pos(#s(#s(@x))),@y) -> c_20(#succ#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) #mult#(#0(),#0()) -> c_21() #mult#(#0(),#neg(@y)) -> c_22() #mult#(#0(),#pos(@y)) -> c_23() #mult#(#neg(@x),#0()) -> c_24() #mult#(#neg(@x),#neg(@y)) -> c_25(#natmult#(@x,@y)) #mult#(#neg(@x),#pos(@y)) -> c_26(#natmult#(@x,@y)) #mult#(#pos(@x),#0()) -> c_27() #mult#(#pos(@x),#neg(@y)) -> c_28(#natmult#(@x,@y)) #mult#(#pos(@x),#pos(@y)) -> c_29(#natmult#(@x,@y)) #natmult#(#0(),@y) -> c_30() #natmult#(#s(@x),@y) -> c_31(#add#(#pos(@y),#natmult(@x,@y)),#natmult#(@x,@y)) #pred#(#0()) -> c_32() #pred#(#neg(#s(@x))) -> c_33() #pred#(#pos(#s(#0()))) -> c_34() #pred#(#pos(#s(#s(@x)))) -> c_35() #succ#(#0()) -> c_36() #succ#(#neg(#s(#0()))) -> c_37() #succ#(#neg(#s(#s(@x)))) -> c_38() #succ#(#pos(#s(@x))) -> c_39() *#(@x,@y) -> c_1(#mult#(@x,@y)) +#(@x,@y) -> c_2(#add#(@x,@y)) computeLine#1#(nil(),@acc,@m) -> c_5() computeLine#2#(nil(),@acc,@x,@xs) -> c_7() lineMult#1#(nil(),@l2,@n) -> c_10() matrixMult#1#(nil(),@m2) -> c_15() - 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)) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@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))) *(@x,@y) -> #mult(@x,@y) +(@x,@y) -> #add(@x,@y) computeLine(@line,@m,@acc) -> computeLine#1(@line,@acc,@m) computeLine#1(::(@x,@xs),@acc,@m) -> computeLine#2(@m,@acc,@x,@xs) computeLine#1(nil(),@acc,@m) -> @acc computeLine#2(::(@l,@ls),@acc,@x,@xs) -> computeLine(@xs,@ls,lineMult(@x,@l,@acc)) computeLine#2(nil(),@acc,@x,@xs) -> nil() lineMult(@n,@l1,@l2) -> lineMult#1(@l1,@l2,@n) lineMult#1(::(@x,@xs),@l2,@n) -> lineMult#2(@l2,@n,@x,@xs) lineMult#1(nil(),@l2,@n) -> nil() lineMult#2(::(@y,@ys),@n,@x,@xs) -> ::(+(*(@x,@n),@y),lineMult(@n,@xs,@ys)) lineMult#2(nil(),@n,@x,@xs) -> ::(*(@x,@n),lineMult(@n,@xs,nil())) matrixMult(@m1,@m2) -> matrixMult#1(@m1,@m2) matrixMult#1(::(@l,@ls),@m2) -> ::(computeLine(@l,@m2,nil()),matrixMult(@ls,@m2)) matrixMult#1(nil(),@m2) -> nil() - Signature: {#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,+/2,computeLine/3,computeLine#1/3,computeLine#2/4,lineMult/3 ,lineMult#1/3,lineMult#2/4,matrixMult/2,matrixMult#1/2,#add#/2,#mult#/2,#natmult#/2,#pred#/1,#succ#/1,*#/2 ,+#/2,computeLine#/3,computeLine#1#/3,computeLine#2#/4,lineMult#/3,lineMult#1#/3,lineMult#2#/4,matrixMult#/2 ,matrixMult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/2,c_7/0,c_8/1 ,c_9/1,c_10/0,c_11/3,c_12/2,c_13/1,c_14/2,c_15/0,c_16/0,c_17/1,c_18/2,c_19/1,c_20/2,c_21/0,c_22/0,c_23/0 ,c_24/0,c_25/1,c_26/1,c_27/0,c_28/1,c_29/1,c_30/0,c_31/2,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0 ,c_39/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine# ,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult# ,matrixMult#1#} and constructors {#0,#neg,#pos,#s,::,nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)) -->_1 computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs)):2 -->_1 computeLine#1#(nil(),@acc,@m) -> c_5():36 2:S:computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs)) -->_1 computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) ,lineMult#(@x,@l,@acc)):3 -->_1 computeLine#2#(nil(),@acc,@x,@xs) -> c_7():37 3:S:computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) ,lineMult#(@x,@l,@acc)) -->_2 lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)):4 -->_1 computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)):1 4:S:lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) -->_1 lineMult#1#(::(@x,@xs),@l2,@n) -> c_9(lineMult#2#(@l2,@n,@x,@xs)):5 -->_1 lineMult#1#(nil(),@l2,@n) -> c_10():38 5:S:lineMult#1#(::(@x,@xs),@l2,@n) -> c_9(lineMult#2#(@l2,@n,@x,@xs)) -->_1 lineMult#2#(nil(),@n,@x,@xs) -> c_12(*#(@x,@n),lineMult#(@n,@xs,nil())):7 -->_1 lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(+#(*(@x,@n),@y),*#(@x,@n),lineMult#(@n,@xs,@ys)):6 6:S:lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(+#(*(@x,@n),@y),*#(@x,@n),lineMult#(@n,@xs,@ys)) -->_1 +#(@x,@y) -> c_2(#add#(@x,@y)):35 -->_2 *#(@x,@y) -> c_1(#mult#(@x,@y)):34 -->_3 lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)):4 7:S:lineMult#2#(nil(),@n,@x,@xs) -> c_12(*#(@x,@n),lineMult#(@n,@xs,nil())) -->_1 *#(@x,@y) -> c_1(#mult#(@x,@y)):34 -->_2 lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)):4 8:S:matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2)) -->_1 matrixMult#1#(::(@l,@ls),@m2) -> c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2)):9 -->_1 matrixMult#1#(nil(),@m2) -> c_15():39 9:S:matrixMult#1#(::(@l,@ls),@m2) -> c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2)) -->_2 matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2)):8 -->_1 computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)):1 10:W:#add#(#0(),@y) -> c_16() 11:W:#add#(#neg(#s(#0())),@y) -> c_17(#pred#(@y)) -->_1 #pred#(#pos(#s(#s(@x)))) -> c_35():29 -->_1 #pred#(#pos(#s(#0()))) -> c_34():28 -->_1 #pred#(#neg(#s(@x))) -> c_33():27 -->_1 #pred#(#0()) -> c_32():26 12:W:#add#(#neg(#s(#s(@x))),@y) -> c_18(#pred#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) -->_2 #add#(#pos(#s(#s(@x))),@y) -> c_20(#succ#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)):14 -->_2 #add#(#pos(#s(#0())),@y) -> c_19(#succ#(@y)):13 -->_1 #pred#(#pos(#s(#s(@x)))) -> c_35():29 -->_1 #pred#(#pos(#s(#0()))) -> c_34():28 -->_1 #pred#(#neg(#s(@x))) -> c_33():27 -->_1 #pred#(#0()) -> c_32():26 13:W:#add#(#pos(#s(#0())),@y) -> c_19(#succ#(@y)) -->_1 #succ#(#pos(#s(@x))) -> c_39():33 -->_1 #succ#(#neg(#s(#s(@x)))) -> c_38():32 -->_1 #succ#(#neg(#s(#0()))) -> c_37():31 -->_1 #succ#(#0()) -> c_36():30 14:W:#add#(#pos(#s(#s(@x))),@y) -> c_20(#succ#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) -->_1 #succ#(#pos(#s(@x))) -> c_39():33 -->_1 #succ#(#neg(#s(#s(@x)))) -> c_38():32 -->_1 #succ#(#neg(#s(#0()))) -> c_37():31 -->_1 #succ#(#0()) -> c_36():30 -->_2 #add#(#pos(#s(#s(@x))),@y) -> c_20(#succ#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)):14 -->_2 #add#(#pos(#s(#0())),@y) -> c_19(#succ#(@y)):13 15:W:#mult#(#0(),#0()) -> c_21() 16:W:#mult#(#0(),#neg(@y)) -> c_22() 17:W:#mult#(#0(),#pos(@y)) -> c_23() 18:W:#mult#(#neg(@x),#0()) -> c_24() 19:W:#mult#(#neg(@x),#neg(@y)) -> c_25(#natmult#(@x,@y)) -->_1 #natmult#(#s(@x),@y) -> c_31(#add#(#pos(@y),#natmult(@x,@y)),#natmult#(@x,@y)):25 -->_1 #natmult#(#0(),@y) -> c_30():24 20:W:#mult#(#neg(@x),#pos(@y)) -> c_26(#natmult#(@x,@y)) -->_1 #natmult#(#s(@x),@y) -> c_31(#add#(#pos(@y),#natmult(@x,@y)),#natmult#(@x,@y)):25 -->_1 #natmult#(#0(),@y) -> c_30():24 21:W:#mult#(#pos(@x),#0()) -> c_27() 22:W:#mult#(#pos(@x),#neg(@y)) -> c_28(#natmult#(@x,@y)) -->_1 #natmult#(#s(@x),@y) -> c_31(#add#(#pos(@y),#natmult(@x,@y)),#natmult#(@x,@y)):25 -->_1 #natmult#(#0(),@y) -> c_30():24 23:W:#mult#(#pos(@x),#pos(@y)) -> c_29(#natmult#(@x,@y)) -->_1 #natmult#(#s(@x),@y) -> c_31(#add#(#pos(@y),#natmult(@x,@y)),#natmult#(@x,@y)):25 -->_1 #natmult#(#0(),@y) -> c_30():24 24:W:#natmult#(#0(),@y) -> c_30() 25:W:#natmult#(#s(@x),@y) -> c_31(#add#(#pos(@y),#natmult(@x,@y)),#natmult#(@x,@y)) -->_2 #natmult#(#s(@x),@y) -> c_31(#add#(#pos(@y),#natmult(@x,@y)),#natmult#(@x,@y)):25 -->_2 #natmult#(#0(),@y) -> c_30():24 -->_1 #add#(#pos(#s(#s(@x))),@y) -> c_20(#succ#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)):14 -->_1 #add#(#pos(#s(#0())),@y) -> c_19(#succ#(@y)):13 26:W:#pred#(#0()) -> c_32() 27:W:#pred#(#neg(#s(@x))) -> c_33() 28:W:#pred#(#pos(#s(#0()))) -> c_34() 29:W:#pred#(#pos(#s(#s(@x)))) -> c_35() 30:W:#succ#(#0()) -> c_36() 31:W:#succ#(#neg(#s(#0()))) -> c_37() 32:W:#succ#(#neg(#s(#s(@x)))) -> c_38() 33:W:#succ#(#pos(#s(@x))) -> c_39() 34:W:*#(@x,@y) -> c_1(#mult#(@x,@y)) -->_1 #mult#(#pos(@x),#pos(@y)) -> c_29(#natmult#(@x,@y)):23 -->_1 #mult#(#pos(@x),#neg(@y)) -> c_28(#natmult#(@x,@y)):22 -->_1 #mult#(#pos(@x),#0()) -> c_27():21 -->_1 #mult#(#neg(@x),#pos(@y)) -> c_26(#natmult#(@x,@y)):20 -->_1 #mult#(#neg(@x),#neg(@y)) -> c_25(#natmult#(@x,@y)):19 -->_1 #mult#(#neg(@x),#0()) -> c_24():18 -->_1 #mult#(#0(),#pos(@y)) -> c_23():17 -->_1 #mult#(#0(),#neg(@y)) -> c_22():16 -->_1 #mult#(#0(),#0()) -> c_21():15 35:W:+#(@x,@y) -> c_2(#add#(@x,@y)) -->_1 #add#(#pos(#s(#s(@x))),@y) -> c_20(#succ#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)):14 -->_1 #add#(#pos(#s(#0())),@y) -> c_19(#succ#(@y)):13 -->_1 #add#(#neg(#s(#s(@x))),@y) -> c_18(#pred#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)):12 -->_1 #add#(#neg(#s(#0())),@y) -> c_17(#pred#(@y)):11 -->_1 #add#(#0(),@y) -> c_16():10 36:W:computeLine#1#(nil(),@acc,@m) -> c_5() 37:W:computeLine#2#(nil(),@acc,@x,@xs) -> c_7() 38:W:lineMult#1#(nil(),@l2,@n) -> c_10() 39:W:matrixMult#1#(nil(),@m2) -> c_15() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 39: matrixMult#1#(nil(),@m2) -> c_15() 36: computeLine#1#(nil(),@acc,@m) -> c_5() 37: computeLine#2#(nil(),@acc,@x,@xs) -> c_7() 38: lineMult#1#(nil(),@l2,@n) -> c_10() 35: +#(@x,@y) -> c_2(#add#(@x,@y)) 10: #add#(#0(),@y) -> c_16() 11: #add#(#neg(#s(#0())),@y) -> c_17(#pred#(@y)) 12: #add#(#neg(#s(#s(@x))),@y) -> c_18(#pred#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) 26: #pred#(#0()) -> c_32() 27: #pred#(#neg(#s(@x))) -> c_33() 28: #pred#(#pos(#s(#0()))) -> c_34() 29: #pred#(#pos(#s(#s(@x)))) -> c_35() 34: *#(@x,@y) -> c_1(#mult#(@x,@y)) 15: #mult#(#0(),#0()) -> c_21() 16: #mult#(#0(),#neg(@y)) -> c_22() 17: #mult#(#0(),#pos(@y)) -> c_23() 18: #mult#(#neg(@x),#0()) -> c_24() 19: #mult#(#neg(@x),#neg(@y)) -> c_25(#natmult#(@x,@y)) 20: #mult#(#neg(@x),#pos(@y)) -> c_26(#natmult#(@x,@y)) 21: #mult#(#pos(@x),#0()) -> c_27() 22: #mult#(#pos(@x),#neg(@y)) -> c_28(#natmult#(@x,@y)) 23: #mult#(#pos(@x),#pos(@y)) -> c_29(#natmult#(@x,@y)) 25: #natmult#(#s(@x),@y) -> c_31(#add#(#pos(@y),#natmult(@x,@y)),#natmult#(@x,@y)) 14: #add#(#pos(#s(#s(@x))),@y) -> c_20(#succ#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) 13: #add#(#pos(#s(#0())),@y) -> c_19(#succ#(@y)) 30: #succ#(#0()) -> c_36() 31: #succ#(#neg(#s(#0()))) -> c_37() 32: #succ#(#neg(#s(#s(@x)))) -> c_38() 33: #succ#(#pos(#s(@x))) -> c_39() 24: #natmult#(#0(),@y) -> c_30() * Step 4: SimplifyRHS WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)) computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs)) computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) ,lineMult#(@x,@l,@acc)) lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) lineMult#1#(::(@x,@xs),@l2,@n) -> c_9(lineMult#2#(@l2,@n,@x,@xs)) lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(+#(*(@x,@n),@y),*#(@x,@n),lineMult#(@n,@xs,@ys)) lineMult#2#(nil(),@n,@x,@xs) -> c_12(*#(@x,@n),lineMult#(@n,@xs,nil())) matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2)) matrixMult#1#(::(@l,@ls),@m2) -> c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2)) - 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)) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@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))) *(@x,@y) -> #mult(@x,@y) +(@x,@y) -> #add(@x,@y) computeLine(@line,@m,@acc) -> computeLine#1(@line,@acc,@m) computeLine#1(::(@x,@xs),@acc,@m) -> computeLine#2(@m,@acc,@x,@xs) computeLine#1(nil(),@acc,@m) -> @acc computeLine#2(::(@l,@ls),@acc,@x,@xs) -> computeLine(@xs,@ls,lineMult(@x,@l,@acc)) computeLine#2(nil(),@acc,@x,@xs) -> nil() lineMult(@n,@l1,@l2) -> lineMult#1(@l1,@l2,@n) lineMult#1(::(@x,@xs),@l2,@n) -> lineMult#2(@l2,@n,@x,@xs) lineMult#1(nil(),@l2,@n) -> nil() lineMult#2(::(@y,@ys),@n,@x,@xs) -> ::(+(*(@x,@n),@y),lineMult(@n,@xs,@ys)) lineMult#2(nil(),@n,@x,@xs) -> ::(*(@x,@n),lineMult(@n,@xs,nil())) matrixMult(@m1,@m2) -> matrixMult#1(@m1,@m2) matrixMult#1(::(@l,@ls),@m2) -> ::(computeLine(@l,@m2,nil()),matrixMult(@ls,@m2)) matrixMult#1(nil(),@m2) -> nil() - Signature: {#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,+/2,computeLine/3,computeLine#1/3,computeLine#2/4,lineMult/3 ,lineMult#1/3,lineMult#2/4,matrixMult/2,matrixMult#1/2,#add#/2,#mult#/2,#natmult#/2,#pred#/1,#succ#/1,*#/2 ,+#/2,computeLine#/3,computeLine#1#/3,computeLine#2#/4,lineMult#/3,lineMult#1#/3,lineMult#2#/4,matrixMult#/2 ,matrixMult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/2,c_7/0,c_8/1 ,c_9/1,c_10/0,c_11/3,c_12/2,c_13/1,c_14/2,c_15/0,c_16/0,c_17/1,c_18/2,c_19/1,c_20/2,c_21/0,c_22/0,c_23/0 ,c_24/0,c_25/1,c_26/1,c_27/0,c_28/1,c_29/1,c_30/0,c_31/2,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0 ,c_39/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine# ,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult# ,matrixMult#1#} and constructors {#0,#neg,#pos,#s,::,nil} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)) -->_1 computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs)):2 2:S:computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs)) -->_1 computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) ,lineMult#(@x,@l,@acc)):3 3:S:computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) ,lineMult#(@x,@l,@acc)) -->_2 lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)):4 -->_1 computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)):1 4:S:lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) -->_1 lineMult#1#(::(@x,@xs),@l2,@n) -> c_9(lineMult#2#(@l2,@n,@x,@xs)):5 5:S:lineMult#1#(::(@x,@xs),@l2,@n) -> c_9(lineMult#2#(@l2,@n,@x,@xs)) -->_1 lineMult#2#(nil(),@n,@x,@xs) -> c_12(*#(@x,@n),lineMult#(@n,@xs,nil())):7 -->_1 lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(+#(*(@x,@n),@y),*#(@x,@n),lineMult#(@n,@xs,@ys)):6 6:S:lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(+#(*(@x,@n),@y),*#(@x,@n),lineMult#(@n,@xs,@ys)) -->_3 lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)):4 7:S:lineMult#2#(nil(),@n,@x,@xs) -> c_12(*#(@x,@n),lineMult#(@n,@xs,nil())) -->_2 lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)):4 8:S:matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2)) -->_1 matrixMult#1#(::(@l,@ls),@m2) -> c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2)):9 9:S:matrixMult#1#(::(@l,@ls),@m2) -> c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2)) -->_2 matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2)):8 -->_1 computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(lineMult#(@n,@xs,@ys)) lineMult#2#(nil(),@n,@x,@xs) -> c_12(lineMult#(@n,@xs,nil())) * Step 5: UsableRules WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)) computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs)) computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) ,lineMult#(@x,@l,@acc)) lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) lineMult#1#(::(@x,@xs),@l2,@n) -> c_9(lineMult#2#(@l2,@n,@x,@xs)) lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(lineMult#(@n,@xs,@ys)) lineMult#2#(nil(),@n,@x,@xs) -> c_12(lineMult#(@n,@xs,nil())) matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2)) matrixMult#1#(::(@l,@ls),@m2) -> c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2)) - 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)) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@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))) *(@x,@y) -> #mult(@x,@y) +(@x,@y) -> #add(@x,@y) computeLine(@line,@m,@acc) -> computeLine#1(@line,@acc,@m) computeLine#1(::(@x,@xs),@acc,@m) -> computeLine#2(@m,@acc,@x,@xs) computeLine#1(nil(),@acc,@m) -> @acc computeLine#2(::(@l,@ls),@acc,@x,@xs) -> computeLine(@xs,@ls,lineMult(@x,@l,@acc)) computeLine#2(nil(),@acc,@x,@xs) -> nil() lineMult(@n,@l1,@l2) -> lineMult#1(@l1,@l2,@n) lineMult#1(::(@x,@xs),@l2,@n) -> lineMult#2(@l2,@n,@x,@xs) lineMult#1(nil(),@l2,@n) -> nil() lineMult#2(::(@y,@ys),@n,@x,@xs) -> ::(+(*(@x,@n),@y),lineMult(@n,@xs,@ys)) lineMult#2(nil(),@n,@x,@xs) -> ::(*(@x,@n),lineMult(@n,@xs,nil())) matrixMult(@m1,@m2) -> matrixMult#1(@m1,@m2) matrixMult#1(::(@l,@ls),@m2) -> ::(computeLine(@l,@m2,nil()),matrixMult(@ls,@m2)) matrixMult#1(nil(),@m2) -> nil() - Signature: {#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,+/2,computeLine/3,computeLine#1/3,computeLine#2/4,lineMult/3 ,lineMult#1/3,lineMult#2/4,matrixMult/2,matrixMult#1/2,#add#/2,#mult#/2,#natmult#/2,#pred#/1,#succ#/1,*#/2 ,+#/2,computeLine#/3,computeLine#1#/3,computeLine#2#/4,lineMult#/3,lineMult#1#/3,lineMult#2#/4,matrixMult#/2 ,matrixMult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/2,c_7/0,c_8/1 ,c_9/1,c_10/0,c_11/1,c_12/1,c_13/1,c_14/2,c_15/0,c_16/0,c_17/1,c_18/2,c_19/1,c_20/2,c_21/0,c_22/0,c_23/0 ,c_24/0,c_25/1,c_26/1,c_27/0,c_28/1,c_29/1,c_30/0,c_31/2,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0 ,c_39/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine# ,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult# ,matrixMult#1#} and constructors {#0,#neg,#pos,#s,::,nil} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: #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)) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@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))) *(@x,@y) -> #mult(@x,@y) +(@x,@y) -> #add(@x,@y) lineMult(@n,@l1,@l2) -> lineMult#1(@l1,@l2,@n) lineMult#1(::(@x,@xs),@l2,@n) -> lineMult#2(@l2,@n,@x,@xs) lineMult#1(nil(),@l2,@n) -> nil() lineMult#2(::(@y,@ys),@n,@x,@xs) -> ::(+(*(@x,@n),@y),lineMult(@n,@xs,@ys)) lineMult#2(nil(),@n,@x,@xs) -> ::(*(@x,@n),lineMult(@n,@xs,nil())) computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)) computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs)) computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) ,lineMult#(@x,@l,@acc)) lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) lineMult#1#(::(@x,@xs),@l2,@n) -> c_9(lineMult#2#(@l2,@n,@x,@xs)) lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(lineMult#(@n,@xs,@ys)) lineMult#2#(nil(),@n,@x,@xs) -> c_12(lineMult#(@n,@xs,nil())) matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2)) matrixMult#1#(::(@l,@ls),@m2) -> c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2)) * Step 6: DecomposeDG WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)) computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs)) computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) ,lineMult#(@x,@l,@acc)) lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) lineMult#1#(::(@x,@xs),@l2,@n) -> c_9(lineMult#2#(@l2,@n,@x,@xs)) lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(lineMult#(@n,@xs,@ys)) lineMult#2#(nil(),@n,@x,@xs) -> c_12(lineMult#(@n,@xs,nil())) matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2)) matrixMult#1#(::(@l,@ls),@m2) -> c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2)) - 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)) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@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))) *(@x,@y) -> #mult(@x,@y) +(@x,@y) -> #add(@x,@y) lineMult(@n,@l1,@l2) -> lineMult#1(@l1,@l2,@n) lineMult#1(::(@x,@xs),@l2,@n) -> lineMult#2(@l2,@n,@x,@xs) lineMult#1(nil(),@l2,@n) -> nil() lineMult#2(::(@y,@ys),@n,@x,@xs) -> ::(+(*(@x,@n),@y),lineMult(@n,@xs,@ys)) lineMult#2(nil(),@n,@x,@xs) -> ::(*(@x,@n),lineMult(@n,@xs,nil())) - Signature: {#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,+/2,computeLine/3,computeLine#1/3,computeLine#2/4,lineMult/3 ,lineMult#1/3,lineMult#2/4,matrixMult/2,matrixMult#1/2,#add#/2,#mult#/2,#natmult#/2,#pred#/1,#succ#/1,*#/2 ,+#/2,computeLine#/3,computeLine#1#/3,computeLine#2#/4,lineMult#/3,lineMult#1#/3,lineMult#2#/4,matrixMult#/2 ,matrixMult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/2,c_7/0,c_8/1 ,c_9/1,c_10/0,c_11/1,c_12/1,c_13/1,c_14/2,c_15/0,c_16/0,c_17/1,c_18/2,c_19/1,c_20/2,c_21/0,c_22/0,c_23/0 ,c_24/0,c_25/1,c_26/1,c_27/0,c_28/1,c_29/1,c_30/0,c_31/2,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0 ,c_39/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine# ,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult# ,matrixMult#1#} and constructors {#0,#neg,#pos,#s,::,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 matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2)) matrixMult#1#(::(@l,@ls),@m2) -> c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2)) and a lower component computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)) computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs)) computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) ,lineMult#(@x,@l,@acc)) lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) lineMult#1#(::(@x,@xs),@l2,@n) -> c_9(lineMult#2#(@l2,@n,@x,@xs)) lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(lineMult#(@n,@xs,@ys)) lineMult#2#(nil(),@n,@x,@xs) -> c_12(lineMult#(@n,@xs,nil())) Further, following extension rules are added to the lower component. matrixMult#(@m1,@m2) -> matrixMult#1#(@m1,@m2) matrixMult#1#(::(@l,@ls),@m2) -> computeLine#(@l,@m2,nil()) matrixMult#1#(::(@l,@ls),@m2) -> matrixMult#(@ls,@m2) ** Step 6.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2)) matrixMult#1#(::(@l,@ls),@m2) -> c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2)) - 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)) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@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))) *(@x,@y) -> #mult(@x,@y) +(@x,@y) -> #add(@x,@y) lineMult(@n,@l1,@l2) -> lineMult#1(@l1,@l2,@n) lineMult#1(::(@x,@xs),@l2,@n) -> lineMult#2(@l2,@n,@x,@xs) lineMult#1(nil(),@l2,@n) -> nil() lineMult#2(::(@y,@ys),@n,@x,@xs) -> ::(+(*(@x,@n),@y),lineMult(@n,@xs,@ys)) lineMult#2(nil(),@n,@x,@xs) -> ::(*(@x,@n),lineMult(@n,@xs,nil())) - Signature: {#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,+/2,computeLine/3,computeLine#1/3,computeLine#2/4,lineMult/3 ,lineMult#1/3,lineMult#2/4,matrixMult/2,matrixMult#1/2,#add#/2,#mult#/2,#natmult#/2,#pred#/1,#succ#/1,*#/2 ,+#/2,computeLine#/3,computeLine#1#/3,computeLine#2#/4,lineMult#/3,lineMult#1#/3,lineMult#2#/4,matrixMult#/2 ,matrixMult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/2,c_7/0,c_8/1 ,c_9/1,c_10/0,c_11/1,c_12/1,c_13/1,c_14/2,c_15/0,c_16/0,c_17/1,c_18/2,c_19/1,c_20/2,c_21/0,c_22/0,c_23/0 ,c_24/0,c_25/1,c_26/1,c_27/0,c_28/1,c_29/1,c_30/0,c_31/2,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0 ,c_39/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine# ,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult# ,matrixMult#1#} and constructors {#0,#neg,#pos,#s,::,nil} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2)) -->_1 matrixMult#1#(::(@l,@ls),@m2) -> c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2)):2 2:S:matrixMult#1#(::(@l,@ls),@m2) -> c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2)) -->_2 matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: matrixMult#1#(::(@l,@ls),@m2) -> c_14(matrixMult#(@ls,@m2)) ** Step 6.a:2: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2)) matrixMult#1#(::(@l,@ls),@m2) -> c_14(matrixMult#(@ls,@m2)) - 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)) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@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))) *(@x,@y) -> #mult(@x,@y) +(@x,@y) -> #add(@x,@y) lineMult(@n,@l1,@l2) -> lineMult#1(@l1,@l2,@n) lineMult#1(::(@x,@xs),@l2,@n) -> lineMult#2(@l2,@n,@x,@xs) lineMult#1(nil(),@l2,@n) -> nil() lineMult#2(::(@y,@ys),@n,@x,@xs) -> ::(+(*(@x,@n),@y),lineMult(@n,@xs,@ys)) lineMult#2(nil(),@n,@x,@xs) -> ::(*(@x,@n),lineMult(@n,@xs,nil())) - Signature: {#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,+/2,computeLine/3,computeLine#1/3,computeLine#2/4,lineMult/3 ,lineMult#1/3,lineMult#2/4,matrixMult/2,matrixMult#1/2,#add#/2,#mult#/2,#natmult#/2,#pred#/1,#succ#/1,*#/2 ,+#/2,computeLine#/3,computeLine#1#/3,computeLine#2#/4,lineMult#/3,lineMult#1#/3,lineMult#2#/4,matrixMult#/2 ,matrixMult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/2,c_7/0,c_8/1 ,c_9/1,c_10/0,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/0,c_17/1,c_18/2,c_19/1,c_20/2,c_21/0,c_22/0,c_23/0 ,c_24/0,c_25/1,c_26/1,c_27/0,c_28/1,c_29/1,c_30/0,c_31/2,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0 ,c_39/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine# ,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult# ,matrixMult#1#} and constructors {#0,#neg,#pos,#s,::,nil} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2)) matrixMult#1#(::(@l,@ls),@m2) -> c_14(matrixMult#(@ls,@m2)) ** Step 6.a:3: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2)) matrixMult#1#(::(@l,@ls),@m2) -> c_14(matrixMult#(@ls,@m2)) - Signature: {#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,+/2,computeLine/3,computeLine#1/3,computeLine#2/4,lineMult/3 ,lineMult#1/3,lineMult#2/4,matrixMult/2,matrixMult#1/2,#add#/2,#mult#/2,#natmult#/2,#pred#/1,#succ#/1,*#/2 ,+#/2,computeLine#/3,computeLine#1#/3,computeLine#2#/4,lineMult#/3,lineMult#1#/3,lineMult#2#/4,matrixMult#/2 ,matrixMult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/2,c_7/0,c_8/1 ,c_9/1,c_10/0,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/0,c_17/1,c_18/2,c_19/1,c_20/2,c_21/0,c_22/0,c_23/0 ,c_24/0,c_25/1,c_26/1,c_27/0,c_28/1,c_29/1,c_30/0,c_31/2,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0 ,c_39/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine# ,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult# ,matrixMult#1#} and constructors {#0,#neg,#pos,#s,::,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_13) = {1}, uargs(c_14) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#add) = [0] p(#mult) = [0] p(#natmult) = [0] p(#neg) = [1] x1 + [0] p(#pos) = [1] x1 + [0] p(#pred) = [0] p(#s) = [1] x1 + [0] p(#succ) = [0] p(*) = [0] p(+) = [0] p(::) = [1] x1 + [1] x2 + [0] p(computeLine) = [0] p(computeLine#1) = [0] p(computeLine#2) = [0] p(lineMult) = [0] p(lineMult#1) = [0] p(lineMult#2) = [0] p(matrixMult) = [0] p(matrixMult#1) = [0] p(nil) = [0] p(#add#) = [0] p(#mult#) = [0] p(#natmult#) = [0] p(#pred#) = [0] p(#succ#) = [0] p(*#) = [0] p(+#) = [1] x1 + [0] p(computeLine#) = [0] p(computeLine#1#) = [0] p(computeLine#2#) = [0] p(lineMult#) = [0] p(lineMult#1#) = [0] p(lineMult#2#) = [0] p(matrixMult#) = [0] p(matrixMult#1#) = [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) = [1] x1 + [0] p(c_14) = [1] x1 + [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) = [0] p(c_31) = [0] p(c_32) = [0] p(c_33) = [0] p(c_34) = [0] p(c_35) = [0] p(c_36) = [0] p(c_37) = [0] p(c_38) = [0] p(c_39) = [0] Following rules are strictly oriented: matrixMult#1#(::(@l,@ls),@m2) = [3] > [0] = c_14(matrixMult#(@ls,@m2)) Following rules are (at-least) weakly oriented: matrixMult#(@m1,@m2) = [0] >= [3] = c_13(matrixMult#1#(@m1,@m2)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 6.a:4: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2)) - Weak DPs: matrixMult#1#(::(@l,@ls),@m2) -> c_14(matrixMult#(@ls,@m2)) - Signature: {#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,+/2,computeLine/3,computeLine#1/3,computeLine#2/4,lineMult/3 ,lineMult#1/3,lineMult#2/4,matrixMult/2,matrixMult#1/2,#add#/2,#mult#/2,#natmult#/2,#pred#/1,#succ#/1,*#/2 ,+#/2,computeLine#/3,computeLine#1#/3,computeLine#2#/4,lineMult#/3,lineMult#1#/3,lineMult#2#/4,matrixMult#/2 ,matrixMult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/2,c_7/0,c_8/1 ,c_9/1,c_10/0,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/0,c_17/1,c_18/2,c_19/1,c_20/2,c_21/0,c_22/0,c_23/0 ,c_24/0,c_25/1,c_26/1,c_27/0,c_28/1,c_29/1,c_30/0,c_31/2,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0 ,c_39/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine# ,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult# ,matrixMult#1#} and constructors {#0,#neg,#pos,#s,::,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_13) = {1}, uargs(c_14) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#add) = [0] p(#mult) = [0] p(#natmult) = [0] p(#neg) = [1] x1 + [1] p(#pos) = [1] x1 + [0] p(#pred) = [0] p(#s) = [1] x1 + [0] p(#succ) = [0] p(*) = [0] p(+) = [0] p(::) = [1] x1 + [1] x2 + [11] p(computeLine) = [0] p(computeLine#1) = [0] p(computeLine#2) = [0] p(lineMult) = [0] p(lineMult#1) = [0] p(lineMult#2) = [0] p(matrixMult) = [0] p(matrixMult#1) = [0] p(nil) = [0] p(#add#) = [0] p(#mult#) = [0] p(#natmult#) = [0] p(#pred#) = [0] p(#succ#) = [1] p(*#) = [0] p(+#) = [0] p(computeLine#) = [0] p(computeLine#1#) = [0] p(computeLine#2#) = [0] p(lineMult#) = [0] p(lineMult#1#) = [0] p(lineMult#2#) = [0] p(matrixMult#) = [1] x1 + [11] p(matrixMult#1#) = [1] x1 + [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) = [1] x1 + [0] p(c_14) = [1] x1 + [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) = [0] p(c_31) = [0] p(c_32) = [0] p(c_33) = [0] p(c_34) = [0] p(c_35) = [0] p(c_36) = [0] p(c_37) = [0] p(c_38) = [0] p(c_39) = [0] Following rules are strictly oriented: matrixMult#(@m1,@m2) = [1] @m1 + [11] > [1] @m1 + [0] = c_13(matrixMult#1#(@m1,@m2)) Following rules are (at-least) weakly oriented: matrixMult#1#(::(@l,@ls),@m2) = [1] @l + [1] @ls + [11] >= [1] @ls + [11] = c_14(matrixMult#(@ls,@m2)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 6.a:5: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2)) matrixMult#1#(::(@l,@ls),@m2) -> c_14(matrixMult#(@ls,@m2)) - Signature: {#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,+/2,computeLine/3,computeLine#1/3,computeLine#2/4,lineMult/3 ,lineMult#1/3,lineMult#2/4,matrixMult/2,matrixMult#1/2,#add#/2,#mult#/2,#natmult#/2,#pred#/1,#succ#/1,*#/2 ,+#/2,computeLine#/3,computeLine#1#/3,computeLine#2#/4,lineMult#/3,lineMult#1#/3,lineMult#2#/4,matrixMult#/2 ,matrixMult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/2,c_7/0,c_8/1 ,c_9/1,c_10/0,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/0,c_17/1,c_18/2,c_19/1,c_20/2,c_21/0,c_22/0,c_23/0 ,c_24/0,c_25/1,c_26/1,c_27/0,c_28/1,c_29/1,c_30/0,c_31/2,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0 ,c_39/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine# ,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult# ,matrixMult#1#} and constructors {#0,#neg,#pos,#s,::,nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). ** Step 6.b:1: DecomposeDG WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)) computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs)) computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) ,lineMult#(@x,@l,@acc)) lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) lineMult#1#(::(@x,@xs),@l2,@n) -> c_9(lineMult#2#(@l2,@n,@x,@xs)) lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(lineMult#(@n,@xs,@ys)) lineMult#2#(nil(),@n,@x,@xs) -> c_12(lineMult#(@n,@xs,nil())) - Weak DPs: matrixMult#(@m1,@m2) -> matrixMult#1#(@m1,@m2) matrixMult#1#(::(@l,@ls),@m2) -> computeLine#(@l,@m2,nil()) matrixMult#1#(::(@l,@ls),@m2) -> matrixMult#(@ls,@m2) - 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)) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@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))) *(@x,@y) -> #mult(@x,@y) +(@x,@y) -> #add(@x,@y) lineMult(@n,@l1,@l2) -> lineMult#1(@l1,@l2,@n) lineMult#1(::(@x,@xs),@l2,@n) -> lineMult#2(@l2,@n,@x,@xs) lineMult#1(nil(),@l2,@n) -> nil() lineMult#2(::(@y,@ys),@n,@x,@xs) -> ::(+(*(@x,@n),@y),lineMult(@n,@xs,@ys)) lineMult#2(nil(),@n,@x,@xs) -> ::(*(@x,@n),lineMult(@n,@xs,nil())) - Signature: {#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,+/2,computeLine/3,computeLine#1/3,computeLine#2/4,lineMult/3 ,lineMult#1/3,lineMult#2/4,matrixMult/2,matrixMult#1/2,#add#/2,#mult#/2,#natmult#/2,#pred#/1,#succ#/1,*#/2 ,+#/2,computeLine#/3,computeLine#1#/3,computeLine#2#/4,lineMult#/3,lineMult#1#/3,lineMult#2#/4,matrixMult#/2 ,matrixMult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/2,c_7/0,c_8/1 ,c_9/1,c_10/0,c_11/1,c_12/1,c_13/1,c_14/2,c_15/0,c_16/0,c_17/1,c_18/2,c_19/1,c_20/2,c_21/0,c_22/0,c_23/0 ,c_24/0,c_25/1,c_26/1,c_27/0,c_28/1,c_29/1,c_30/0,c_31/2,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0 ,c_39/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine# ,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult# ,matrixMult#1#} and constructors {#0,#neg,#pos,#s,::,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 computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)) computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs)) computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) ,lineMult#(@x,@l,@acc)) matrixMult#(@m1,@m2) -> matrixMult#1#(@m1,@m2) matrixMult#1#(::(@l,@ls),@m2) -> computeLine#(@l,@m2,nil()) matrixMult#1#(::(@l,@ls),@m2) -> matrixMult#(@ls,@m2) and a lower component lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) lineMult#1#(::(@x,@xs),@l2,@n) -> c_9(lineMult#2#(@l2,@n,@x,@xs)) lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(lineMult#(@n,@xs,@ys)) lineMult#2#(nil(),@n,@x,@xs) -> c_12(lineMult#(@n,@xs,nil())) Further, following extension rules are added to the lower component. computeLine#(@line,@m,@acc) -> computeLine#1#(@line,@acc,@m) computeLine#1#(::(@x,@xs),@acc,@m) -> computeLine#2#(@m,@acc,@x,@xs) computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> lineMult#(@x,@l,@acc) matrixMult#(@m1,@m2) -> matrixMult#1#(@m1,@m2) matrixMult#1#(::(@l,@ls),@m2) -> computeLine#(@l,@m2,nil()) matrixMult#1#(::(@l,@ls),@m2) -> matrixMult#(@ls,@m2) *** Step 6.b:1.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)) computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs)) computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) ,lineMult#(@x,@l,@acc)) - Weak DPs: matrixMult#(@m1,@m2) -> matrixMult#1#(@m1,@m2) matrixMult#1#(::(@l,@ls),@m2) -> computeLine#(@l,@m2,nil()) matrixMult#1#(::(@l,@ls),@m2) -> matrixMult#(@ls,@m2) - 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)) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@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))) *(@x,@y) -> #mult(@x,@y) +(@x,@y) -> #add(@x,@y) lineMult(@n,@l1,@l2) -> lineMult#1(@l1,@l2,@n) lineMult#1(::(@x,@xs),@l2,@n) -> lineMult#2(@l2,@n,@x,@xs) lineMult#1(nil(),@l2,@n) -> nil() lineMult#2(::(@y,@ys),@n,@x,@xs) -> ::(+(*(@x,@n),@y),lineMult(@n,@xs,@ys)) lineMult#2(nil(),@n,@x,@xs) -> ::(*(@x,@n),lineMult(@n,@xs,nil())) - Signature: {#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,+/2,computeLine/3,computeLine#1/3,computeLine#2/4,lineMult/3 ,lineMult#1/3,lineMult#2/4,matrixMult/2,matrixMult#1/2,#add#/2,#mult#/2,#natmult#/2,#pred#/1,#succ#/1,*#/2 ,+#/2,computeLine#/3,computeLine#1#/3,computeLine#2#/4,lineMult#/3,lineMult#1#/3,lineMult#2#/4,matrixMult#/2 ,matrixMult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/2,c_7/0,c_8/1 ,c_9/1,c_10/0,c_11/1,c_12/1,c_13/1,c_14/2,c_15/0,c_16/0,c_17/1,c_18/2,c_19/1,c_20/2,c_21/0,c_22/0,c_23/0 ,c_24/0,c_25/1,c_26/1,c_27/0,c_28/1,c_29/1,c_30/0,c_31/2,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0 ,c_39/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine# ,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult# ,matrixMult#1#} and constructors {#0,#neg,#pos,#s,::,nil} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)) -->_1 computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs)):2 2:S:computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs)) -->_1 computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) ,lineMult#(@x,@l,@acc)):3 3:S:computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) ,lineMult#(@x,@l,@acc)) -->_1 computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)):1 4:W:matrixMult#(@m1,@m2) -> matrixMult#1#(@m1,@m2) -->_1 matrixMult#1#(::(@l,@ls),@m2) -> matrixMult#(@ls,@m2):6 -->_1 matrixMult#1#(::(@l,@ls),@m2) -> computeLine#(@l,@m2,nil()):5 5:W:matrixMult#1#(::(@l,@ls),@m2) -> computeLine#(@l,@m2,nil()) -->_1 computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)):1 6:W:matrixMult#1#(::(@l,@ls),@m2) -> matrixMult#(@ls,@m2) -->_1 matrixMult#(@m1,@m2) -> matrixMult#1#(@m1,@m2):4 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc))) *** Step 6.b:1.a:2: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)) computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs)) computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc))) - Weak DPs: matrixMult#(@m1,@m2) -> matrixMult#1#(@m1,@m2) matrixMult#1#(::(@l,@ls),@m2) -> computeLine#(@l,@m2,nil()) matrixMult#1#(::(@l,@ls),@m2) -> matrixMult#(@ls,@m2) - 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)) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@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))) *(@x,@y) -> #mult(@x,@y) +(@x,@y) -> #add(@x,@y) lineMult(@n,@l1,@l2) -> lineMult#1(@l1,@l2,@n) lineMult#1(::(@x,@xs),@l2,@n) -> lineMult#2(@l2,@n,@x,@xs) lineMult#1(nil(),@l2,@n) -> nil() lineMult#2(::(@y,@ys),@n,@x,@xs) -> ::(+(*(@x,@n),@y),lineMult(@n,@xs,@ys)) lineMult#2(nil(),@n,@x,@xs) -> ::(*(@x,@n),lineMult(@n,@xs,nil())) - Signature: {#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,+/2,computeLine/3,computeLine#1/3,computeLine#2/4,lineMult/3 ,lineMult#1/3,lineMult#2/4,matrixMult/2,matrixMult#1/2,#add#/2,#mult#/2,#natmult#/2,#pred#/1,#succ#/1,*#/2 ,+#/2,computeLine#/3,computeLine#1#/3,computeLine#2#/4,lineMult#/3,lineMult#1#/3,lineMult#2#/4,matrixMult#/2 ,matrixMult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1 ,c_9/1,c_10/0,c_11/1,c_12/1,c_13/1,c_14/2,c_15/0,c_16/0,c_17/1,c_18/2,c_19/1,c_20/2,c_21/0,c_22/0,c_23/0 ,c_24/0,c_25/1,c_26/1,c_27/0,c_28/1,c_29/1,c_30/0,c_31/2,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0 ,c_39/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine# ,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult# ,matrixMult#1#} and constructors {#0,#neg,#pos,#s,::,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(#add) = {2}, uargs(#neg) = {1}, uargs(#pos) = {1}, uargs(#pred) = {1}, uargs(#succ) = {1}, uargs(+) = {1}, uargs(::) = {1,2}, uargs(computeLine#) = {3}, uargs(c_3) = {1}, uargs(c_4) = {1}, uargs(c_6) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#add) = [1] x2 + [0] p(#mult) = [0] p(#natmult) = [0] p(#neg) = [1] x1 + [0] p(#pos) = [1] x1 + [0] p(#pred) = [1] x1 + [0] p(#s) = [0] p(#succ) = [1] x1 + [0] p(*) = [0] p(+) = [1] x1 + [1] x2 + [0] p(::) = [1] x1 + [1] x2 + [5] p(computeLine) = [0] p(computeLine#1) = [0] p(computeLine#2) = [0] p(lineMult) = [1] x2 + [1] x3 + [1] p(lineMult#1) = [1] x1 + [1] x2 + [1] p(lineMult#2) = [1] x1 + [1] x4 + [6] p(matrixMult) = [0] p(matrixMult#1) = [0] p(nil) = [2] p(#add#) = [0] p(#mult#) = [0] p(#natmult#) = [0] p(#pred#) = [0] p(#succ#) = [0] p(*#) = [0] p(+#) = [0] p(computeLine#) = [2] x1 + [2] x2 + [1] x3 + [2] p(computeLine#1#) = [2] x1 + [1] x2 + [2] x3 + [0] p(computeLine#2#) = [2] x1 + [1] x2 + [2] x4 + [1] p(lineMult#) = [0] p(lineMult#1#) = [0] p(lineMult#2#) = [1] x4 + [0] p(matrixMult#) = [2] x1 + [4] x2 + [4] p(matrixMult#1#) = [2] x1 + [4] x2 + [2] p(c_1) = [0] p(c_2) = [1] p(c_3) = [1] x1 + [0] p(c_4) = [1] x1 + [3] p(c_5) = [1] p(c_6) = [1] x1 + [0] p(c_7) = [0] p(c_8) = [4] x1 + [1] p(c_9) = [2] p(c_10) = [0] p(c_11) = [1] x1 + [0] p(c_12) = [4] x1 + [1] p(c_13) = [4] p(c_14) = [1] x1 + [1] x2 + [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [4] p(c_18) = [1] x1 + [1] x2 + [1] p(c_19) = [1] x1 + [0] p(c_20) = [1] x2 + [0] p(c_21) = [1] p(c_22) = [2] p(c_23) = [1] p(c_24) = [0] p(c_25) = [1] x1 + [0] p(c_26) = [2] p(c_27) = [1] p(c_28) = [1] x1 + [1] p(c_29) = [1] x1 + [0] p(c_30) = [2] p(c_31) = [2] x2 + [2] p(c_32) = [0] p(c_33) = [0] p(c_34) = [0] p(c_35) = [1] p(c_36) = [2] p(c_37) = [0] p(c_38) = [1] p(c_39) = [2] Following rules are strictly oriented: computeLine#(@line,@m,@acc) = [1] @acc + [2] @line + [2] @m + [2] > [1] @acc + [2] @line + [2] @m + [0] = c_3(computeLine#1#(@line,@acc,@m)) computeLine#1#(::(@x,@xs),@acc,@m) = [1] @acc + [2] @m + [2] @x + [2] @xs + [10] > [1] @acc + [2] @m + [2] @xs + [4] = c_4(computeLine#2#(@m,@acc,@x,@xs)) computeLine#2#(::(@l,@ls),@acc,@x,@xs) = [1] @acc + [2] @l + [2] @ls + [2] @xs + [11] > [1] @acc + [1] @l + [2] @ls + [2] @xs + [3] = c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc))) Following rules are (at-least) weakly oriented: matrixMult#(@m1,@m2) = [2] @m1 + [4] @m2 + [4] >= [2] @m1 + [4] @m2 + [2] = matrixMult#1#(@m1,@m2) matrixMult#1#(::(@l,@ls),@m2) = [2] @l + [2] @ls + [4] @m2 + [12] >= [2] @l + [2] @m2 + [4] = computeLine#(@l,@m2,nil()) matrixMult#1#(::(@l,@ls),@m2) = [2] @l + [2] @ls + [4] @m2 + [12] >= [2] @ls + [4] @m2 + [4] = matrixMult#(@ls,@m2) #add(#0(),@y) = [1] @y + [0] >= [1] @y + [0] = @y #add(#neg(#s(#0())),@y) = [1] @y + [0] >= [1] @y + [0] = #pred(@y) #add(#neg(#s(#s(@x))),@y) = [1] @y + [0] >= [1] @y + [0] = #pred(#add(#pos(#s(@x)),@y)) #add(#pos(#s(#0())),@y) = [1] @y + [0] >= [1] @y + [0] = #succ(@y) #add(#pos(#s(#s(@x))),@y) = [1] @y + [0] >= [1] @y + [0] = #succ(#add(#pos(#s(@x)),@y)) #mult(#0(),#0()) = [0] >= [0] = #0() #mult(#0(),#neg(@y)) = [0] >= [0] = #0() #mult(#0(),#pos(@y)) = [0] >= [0] = #0() #mult(#neg(@x),#0()) = [0] >= [0] = #0() #mult(#neg(@x),#neg(@y)) = [0] >= [0] = #pos(#natmult(@x,@y)) #mult(#neg(@x),#pos(@y)) = [0] >= [0] = #neg(#natmult(@x,@y)) #mult(#pos(@x),#0()) = [0] >= [0] = #0() #mult(#pos(@x),#neg(@y)) = [0] >= [0] = #neg(#natmult(@x,@y)) #mult(#pos(@x),#pos(@y)) = [0] >= [0] = #pos(#natmult(@x,@y)) #natmult(#0(),@y) = [0] >= [0] = #0() #natmult(#s(@x),@y) = [0] >= [0] = #add(#pos(@y),#natmult(@x,@y)) #pred(#0()) = [0] >= [0] = #neg(#s(#0())) #pred(#neg(#s(@x))) = [0] >= [0] = #neg(#s(#s(@x))) #pred(#pos(#s(#0()))) = [0] >= [0] = #0() #pred(#pos(#s(#s(@x)))) = [0] >= [0] = #pos(#s(@x)) #succ(#0()) = [0] >= [0] = #pos(#s(#0())) #succ(#neg(#s(#0()))) = [0] >= [0] = #0() #succ(#neg(#s(#s(@x)))) = [0] >= [0] = #neg(#s(@x)) #succ(#pos(#s(@x))) = [0] >= [0] = #pos(#s(#s(@x))) *(@x,@y) = [0] >= [0] = #mult(@x,@y) +(@x,@y) = [1] @x + [1] @y + [0] >= [1] @y + [0] = #add(@x,@y) lineMult(@n,@l1,@l2) = [1] @l1 + [1] @l2 + [1] >= [1] @l1 + [1] @l2 + [1] = lineMult#1(@l1,@l2,@n) lineMult#1(::(@x,@xs),@l2,@n) = [1] @l2 + [1] @x + [1] @xs + [6] >= [1] @l2 + [1] @xs + [6] = lineMult#2(@l2,@n,@x,@xs) lineMult#1(nil(),@l2,@n) = [1] @l2 + [3] >= [2] = nil() lineMult#2(::(@y,@ys),@n,@x,@xs) = [1] @xs + [1] @y + [1] @ys + [11] >= [1] @xs + [1] @y + [1] @ys + [6] = ::(+(*(@x,@n),@y),lineMult(@n,@xs,@ys)) lineMult#2(nil(),@n,@x,@xs) = [1] @xs + [8] >= [1] @xs + [8] = ::(*(@x,@n),lineMult(@n,@xs,nil())) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 6.b:1.a:3: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)) computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs)) computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc))) matrixMult#(@m1,@m2) -> matrixMult#1#(@m1,@m2) matrixMult#1#(::(@l,@ls),@m2) -> computeLine#(@l,@m2,nil()) matrixMult#1#(::(@l,@ls),@m2) -> matrixMult#(@ls,@m2) - 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)) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@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))) *(@x,@y) -> #mult(@x,@y) +(@x,@y) -> #add(@x,@y) lineMult(@n,@l1,@l2) -> lineMult#1(@l1,@l2,@n) lineMult#1(::(@x,@xs),@l2,@n) -> lineMult#2(@l2,@n,@x,@xs) lineMult#1(nil(),@l2,@n) -> nil() lineMult#2(::(@y,@ys),@n,@x,@xs) -> ::(+(*(@x,@n),@y),lineMult(@n,@xs,@ys)) lineMult#2(nil(),@n,@x,@xs) -> ::(*(@x,@n),lineMult(@n,@xs,nil())) - Signature: {#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,+/2,computeLine/3,computeLine#1/3,computeLine#2/4,lineMult/3 ,lineMult#1/3,lineMult#2/4,matrixMult/2,matrixMult#1/2,#add#/2,#mult#/2,#natmult#/2,#pred#/1,#succ#/1,*#/2 ,+#/2,computeLine#/3,computeLine#1#/3,computeLine#2#/4,lineMult#/3,lineMult#1#/3,lineMult#2#/4,matrixMult#/2 ,matrixMult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1 ,c_9/1,c_10/0,c_11/1,c_12/1,c_13/1,c_14/2,c_15/0,c_16/0,c_17/1,c_18/2,c_19/1,c_20/2,c_21/0,c_22/0,c_23/0 ,c_24/0,c_25/1,c_26/1,c_27/0,c_28/1,c_29/1,c_30/0,c_31/2,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0 ,c_39/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine# ,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult# ,matrixMult#1#} and constructors {#0,#neg,#pos,#s,::,nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). *** Step 6.b:1.b:1: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) lineMult#1#(::(@x,@xs),@l2,@n) -> c_9(lineMult#2#(@l2,@n,@x,@xs)) lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(lineMult#(@n,@xs,@ys)) lineMult#2#(nil(),@n,@x,@xs) -> c_12(lineMult#(@n,@xs,nil())) - Weak DPs: computeLine#(@line,@m,@acc) -> computeLine#1#(@line,@acc,@m) computeLine#1#(::(@x,@xs),@acc,@m) -> computeLine#2#(@m,@acc,@x,@xs) computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> lineMult#(@x,@l,@acc) matrixMult#(@m1,@m2) -> matrixMult#1#(@m1,@m2) matrixMult#1#(::(@l,@ls),@m2) -> computeLine#(@l,@m2,nil()) matrixMult#1#(::(@l,@ls),@m2) -> matrixMult#(@ls,@m2) - 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)) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@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))) *(@x,@y) -> #mult(@x,@y) +(@x,@y) -> #add(@x,@y) lineMult(@n,@l1,@l2) -> lineMult#1(@l1,@l2,@n) lineMult#1(::(@x,@xs),@l2,@n) -> lineMult#2(@l2,@n,@x,@xs) lineMult#1(nil(),@l2,@n) -> nil() lineMult#2(::(@y,@ys),@n,@x,@xs) -> ::(+(*(@x,@n),@y),lineMult(@n,@xs,@ys)) lineMult#2(nil(),@n,@x,@xs) -> ::(*(@x,@n),lineMult(@n,@xs,nil())) - Signature: {#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,+/2,computeLine/3,computeLine#1/3,computeLine#2/4,lineMult/3 ,lineMult#1/3,lineMult#2/4,matrixMult/2,matrixMult#1/2,#add#/2,#mult#/2,#natmult#/2,#pred#/1,#succ#/1,*#/2 ,+#/2,computeLine#/3,computeLine#1#/3,computeLine#2#/4,lineMult#/3,lineMult#1#/3,lineMult#2#/4,matrixMult#/2 ,matrixMult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/2,c_7/0,c_8/1 ,c_9/1,c_10/0,c_11/1,c_12/1,c_13/1,c_14/2,c_15/0,c_16/0,c_17/1,c_18/2,c_19/1,c_20/2,c_21/0,c_22/0,c_23/0 ,c_24/0,c_25/1,c_26/1,c_27/0,c_28/1,c_29/1,c_30/0,c_31/2,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0 ,c_39/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine# ,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult# ,matrixMult#1#} and constructors {#0,#neg,#pos,#s,::,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(#add) = {2}, uargs(#neg) = {1}, uargs(#pos) = {1}, uargs(#pred) = {1}, uargs(#succ) = {1}, uargs(+) = {1}, uargs(::) = {1,2}, uargs(computeLine#) = {3}, uargs(c_8) = {1}, uargs(c_9) = {1}, uargs(c_11) = {1}, uargs(c_12) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#add) = [1] x2 + [0] p(#mult) = [0] p(#natmult) = [0] p(#neg) = [1] x1 + [0] p(#pos) = [1] x1 + [0] p(#pred) = [1] x1 + [0] p(#s) = [0] p(#succ) = [1] x1 + [0] p(*) = [0] p(+) = [1] x1 + [1] x2 + [0] p(::) = [1] x1 + [1] x2 + [0] p(computeLine) = [1] p(computeLine#1) = [0] p(computeLine#2) = [0] p(lineMult) = [1] x3 + [0] p(lineMult#1) = [1] x2 + [0] p(lineMult#2) = [1] x1 + [0] p(matrixMult) = [0] p(matrixMult#1) = [0] p(nil) = [0] p(#add#) = [0] p(#mult#) = [0] p(#natmult#) = [0] p(#pred#) = [0] p(#succ#) = [0] p(*#) = [0] p(+#) = [2] x1 + [1] x2 + [4] p(computeLine#) = [1] x3 + [0] p(computeLine#1#) = [1] x2 + [0] p(computeLine#2#) = [1] x2 + [0] p(lineMult#) = [0] p(lineMult#1#) = [1] p(lineMult#2#) = [3] p(matrixMult#) = [4] x2 + [0] p(matrixMult#1#) = [4] 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) = [1] x1 + [0] p(c_9) = [1] x1 + [0] p(c_10) = [0] p(c_11) = [1] x1 + [0] p(c_12) = [1] x1 + [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) = [4] x1 + [0] p(c_29) = [0] p(c_30) = [1] p(c_31) = [1] x2 + [0] p(c_32) = [1] p(c_33) = [0] p(c_34) = [2] p(c_35) = [0] p(c_36) = [0] p(c_37) = [1] p(c_38) = [0] p(c_39) = [0] Following rules are strictly oriented: lineMult#2#(::(@y,@ys),@n,@x,@xs) = [3] > [0] = c_11(lineMult#(@n,@xs,@ys)) lineMult#2#(nil(),@n,@x,@xs) = [3] > [0] = c_12(lineMult#(@n,@xs,nil())) Following rules are (at-least) weakly oriented: computeLine#(@line,@m,@acc) = [1] @acc + [0] >= [1] @acc + [0] = computeLine#1#(@line,@acc,@m) computeLine#1#(::(@x,@xs),@acc,@m) = [1] @acc + [0] >= [1] @acc + [0] = computeLine#2#(@m,@acc,@x,@xs) computeLine#2#(::(@l,@ls),@acc,@x,@xs) = [1] @acc + [0] >= [1] @acc + [0] = computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) computeLine#2#(::(@l,@ls),@acc,@x,@xs) = [1] @acc + [0] >= [0] = lineMult#(@x,@l,@acc) lineMult#(@n,@l1,@l2) = [0] >= [1] = c_8(lineMult#1#(@l1,@l2,@n)) lineMult#1#(::(@x,@xs),@l2,@n) = [1] >= [3] = c_9(lineMult#2#(@l2,@n,@x,@xs)) matrixMult#(@m1,@m2) = [4] @m2 + [0] >= [4] @m2 + [0] = matrixMult#1#(@m1,@m2) matrixMult#1#(::(@l,@ls),@m2) = [4] @m2 + [0] >= [0] = computeLine#(@l,@m2,nil()) matrixMult#1#(::(@l,@ls),@m2) = [4] @m2 + [0] >= [4] @m2 + [0] = matrixMult#(@ls,@m2) #add(#0(),@y) = [1] @y + [0] >= [1] @y + [0] = @y #add(#neg(#s(#0())),@y) = [1] @y + [0] >= [1] @y + [0] = #pred(@y) #add(#neg(#s(#s(@x))),@y) = [1] @y + [0] >= [1] @y + [0] = #pred(#add(#pos(#s(@x)),@y)) #add(#pos(#s(#0())),@y) = [1] @y + [0] >= [1] @y + [0] = #succ(@y) #add(#pos(#s(#s(@x))),@y) = [1] @y + [0] >= [1] @y + [0] = #succ(#add(#pos(#s(@x)),@y)) #mult(#0(),#0()) = [0] >= [0] = #0() #mult(#0(),#neg(@y)) = [0] >= [0] = #0() #mult(#0(),#pos(@y)) = [0] >= [0] = #0() #mult(#neg(@x),#0()) = [0] >= [0] = #0() #mult(#neg(@x),#neg(@y)) = [0] >= [0] = #pos(#natmult(@x,@y)) #mult(#neg(@x),#pos(@y)) = [0] >= [0] = #neg(#natmult(@x,@y)) #mult(#pos(@x),#0()) = [0] >= [0] = #0() #mult(#pos(@x),#neg(@y)) = [0] >= [0] = #neg(#natmult(@x,@y)) #mult(#pos(@x),#pos(@y)) = [0] >= [0] = #pos(#natmult(@x,@y)) #natmult(#0(),@y) = [0] >= [0] = #0() #natmult(#s(@x),@y) = [0] >= [0] = #add(#pos(@y),#natmult(@x,@y)) #pred(#0()) = [0] >= [0] = #neg(#s(#0())) #pred(#neg(#s(@x))) = [0] >= [0] = #neg(#s(#s(@x))) #pred(#pos(#s(#0()))) = [0] >= [0] = #0() #pred(#pos(#s(#s(@x)))) = [0] >= [0] = #pos(#s(@x)) #succ(#0()) = [0] >= [0] = #pos(#s(#0())) #succ(#neg(#s(#0()))) = [0] >= [0] = #0() #succ(#neg(#s(#s(@x)))) = [0] >= [0] = #neg(#s(@x)) #succ(#pos(#s(@x))) = [0] >= [0] = #pos(#s(#s(@x))) *(@x,@y) = [0] >= [0] = #mult(@x,@y) +(@x,@y) = [1] @x + [1] @y + [0] >= [1] @y + [0] = #add(@x,@y) lineMult(@n,@l1,@l2) = [1] @l2 + [0] >= [1] @l2 + [0] = lineMult#1(@l1,@l2,@n) lineMult#1(::(@x,@xs),@l2,@n) = [1] @l2 + [0] >= [1] @l2 + [0] = lineMult#2(@l2,@n,@x,@xs) lineMult#1(nil(),@l2,@n) = [1] @l2 + [0] >= [0] = nil() lineMult#2(::(@y,@ys),@n,@x,@xs) = [1] @y + [1] @ys + [0] >= [1] @y + [1] @ys + [0] = ::(+(*(@x,@n),@y),lineMult(@n,@xs,@ys)) lineMult#2(nil(),@n,@x,@xs) = [0] >= [0] = ::(*(@x,@n),lineMult(@n,@xs,nil())) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 6.b:1.b:2: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) lineMult#1#(::(@x,@xs),@l2,@n) -> c_9(lineMult#2#(@l2,@n,@x,@xs)) - Weak DPs: computeLine#(@line,@m,@acc) -> computeLine#1#(@line,@acc,@m) computeLine#1#(::(@x,@xs),@acc,@m) -> computeLine#2#(@m,@acc,@x,@xs) computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> lineMult#(@x,@l,@acc) lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(lineMult#(@n,@xs,@ys)) lineMult#2#(nil(),@n,@x,@xs) -> c_12(lineMult#(@n,@xs,nil())) matrixMult#(@m1,@m2) -> matrixMult#1#(@m1,@m2) matrixMult#1#(::(@l,@ls),@m2) -> computeLine#(@l,@m2,nil()) matrixMult#1#(::(@l,@ls),@m2) -> matrixMult#(@ls,@m2) - 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)) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@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))) *(@x,@y) -> #mult(@x,@y) +(@x,@y) -> #add(@x,@y) lineMult(@n,@l1,@l2) -> lineMult#1(@l1,@l2,@n) lineMult#1(::(@x,@xs),@l2,@n) -> lineMult#2(@l2,@n,@x,@xs) lineMult#1(nil(),@l2,@n) -> nil() lineMult#2(::(@y,@ys),@n,@x,@xs) -> ::(+(*(@x,@n),@y),lineMult(@n,@xs,@ys)) lineMult#2(nil(),@n,@x,@xs) -> ::(*(@x,@n),lineMult(@n,@xs,nil())) - Signature: {#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,+/2,computeLine/3,computeLine#1/3,computeLine#2/4,lineMult/3 ,lineMult#1/3,lineMult#2/4,matrixMult/2,matrixMult#1/2,#add#/2,#mult#/2,#natmult#/2,#pred#/1,#succ#/1,*#/2 ,+#/2,computeLine#/3,computeLine#1#/3,computeLine#2#/4,lineMult#/3,lineMult#1#/3,lineMult#2#/4,matrixMult#/2 ,matrixMult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/2,c_7/0,c_8/1 ,c_9/1,c_10/0,c_11/1,c_12/1,c_13/1,c_14/2,c_15/0,c_16/0,c_17/1,c_18/2,c_19/1,c_20/2,c_21/0,c_22/0,c_23/0 ,c_24/0,c_25/1,c_26/1,c_27/0,c_28/1,c_29/1,c_30/0,c_31/2,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0 ,c_39/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine# ,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult# ,matrixMult#1#} and constructors {#0,#neg,#pos,#s,::,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(#add) = {2}, uargs(#neg) = {1}, uargs(#pos) = {1}, uargs(#pred) = {1}, uargs(#succ) = {1}, uargs(+) = {1}, uargs(::) = {1,2}, uargs(computeLine#) = {3}, uargs(c_8) = {1}, uargs(c_9) = {1}, uargs(c_11) = {1}, uargs(c_12) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#add) = [1] x2 + [0] p(#mult) = [1] p(#natmult) = [1] p(#neg) = [1] x1 + [0] p(#pos) = [1] x1 + [0] p(#pred) = [1] x1 + [0] p(#s) = [0] p(#succ) = [1] x1 + [0] p(*) = [2] p(+) = [1] x1 + [1] x2 + [0] p(::) = [1] x1 + [1] x2 + [1] p(computeLine) = [0] p(computeLine#1) = [0] p(computeLine#2) = [0] p(lineMult) = [3] x2 + [1] x3 + [0] p(lineMult#1) = [3] x1 + [1] x2 + [0] p(lineMult#2) = [1] x1 + [3] x3 + [3] x4 + [3] p(matrixMult) = [0] p(matrixMult#1) = [0] p(nil) = [0] p(#add#) = [0] p(#mult#) = [0] p(#natmult#) = [0] p(#pred#) = [0] p(#succ#) = [0] p(*#) = [2] p(+#) = [1] p(computeLine#) = [3] x2 + [1] x3 + [0] p(computeLine#1#) = [1] x2 + [3] x3 + [0] p(computeLine#2#) = [3] x1 + [1] x2 + [0] p(lineMult#) = [3] p(lineMult#1#) = [0] p(lineMult#2#) = [7] p(matrixMult#) = [7] x1 + [4] x2 + [4] p(matrixMult#1#) = [7] x1 + [4] x2 + [2] p(c_1) = [0] p(c_2) = [0] p(c_3) = [2] x1 + [2] p(c_4) = [1] x1 + [0] p(c_5) = [1] p(c_6) = [1] x1 + [2] x2 + [2] p(c_7) = [1] p(c_8) = [1] x1 + [1] p(c_9) = [1] x1 + [0] p(c_10) = [0] p(c_11) = [1] x1 + [4] p(c_12) = [1] x1 + [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) = [1] x1 + [2] p(c_20) = [1] x1 + [0] p(c_21) = [1] p(c_22) = [0] p(c_23) = [4] p(c_24) = [2] p(c_25) = [1] p(c_26) = [1] x1 + [1] p(c_27) = [4] p(c_28) = [2] p(c_29) = [0] p(c_30) = [1] p(c_31) = [1] x1 + [0] p(c_32) = [0] p(c_33) = [4] p(c_34) = [0] p(c_35) = [0] p(c_36) = [1] p(c_37) = [2] p(c_38) = [0] p(c_39) = [0] Following rules are strictly oriented: lineMult#(@n,@l1,@l2) = [3] > [1] = c_8(lineMult#1#(@l1,@l2,@n)) Following rules are (at-least) weakly oriented: computeLine#(@line,@m,@acc) = [1] @acc + [3] @m + [0] >= [1] @acc + [3] @m + [0] = computeLine#1#(@line,@acc,@m) computeLine#1#(::(@x,@xs),@acc,@m) = [1] @acc + [3] @m + [0] >= [1] @acc + [3] @m + [0] = computeLine#2#(@m,@acc,@x,@xs) computeLine#2#(::(@l,@ls),@acc,@x,@xs) = [1] @acc + [3] @l + [3] @ls + [3] >= [1] @acc + [3] @l + [3] @ls + [0] = computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) computeLine#2#(::(@l,@ls),@acc,@x,@xs) = [1] @acc + [3] @l + [3] @ls + [3] >= [3] = lineMult#(@x,@l,@acc) lineMult#1#(::(@x,@xs),@l2,@n) = [0] >= [7] = c_9(lineMult#2#(@l2,@n,@x,@xs)) lineMult#2#(::(@y,@ys),@n,@x,@xs) = [7] >= [7] = c_11(lineMult#(@n,@xs,@ys)) lineMult#2#(nil(),@n,@x,@xs) = [7] >= [3] = c_12(lineMult#(@n,@xs,nil())) matrixMult#(@m1,@m2) = [7] @m1 + [4] @m2 + [4] >= [7] @m1 + [4] @m2 + [2] = matrixMult#1#(@m1,@m2) matrixMult#1#(::(@l,@ls),@m2) = [7] @l + [7] @ls + [4] @m2 + [9] >= [3] @m2 + [0] = computeLine#(@l,@m2,nil()) matrixMult#1#(::(@l,@ls),@m2) = [7] @l + [7] @ls + [4] @m2 + [9] >= [7] @ls + [4] @m2 + [4] = matrixMult#(@ls,@m2) #add(#0(),@y) = [1] @y + [0] >= [1] @y + [0] = @y #add(#neg(#s(#0())),@y) = [1] @y + [0] >= [1] @y + [0] = #pred(@y) #add(#neg(#s(#s(@x))),@y) = [1] @y + [0] >= [1] @y + [0] = #pred(#add(#pos(#s(@x)),@y)) #add(#pos(#s(#0())),@y) = [1] @y + [0] >= [1] @y + [0] = #succ(@y) #add(#pos(#s(#s(@x))),@y) = [1] @y + [0] >= [1] @y + [0] = #succ(#add(#pos(#s(@x)),@y)) #mult(#0(),#0()) = [1] >= [0] = #0() #mult(#0(),#neg(@y)) = [1] >= [0] = #0() #mult(#0(),#pos(@y)) = [1] >= [0] = #0() #mult(#neg(@x),#0()) = [1] >= [0] = #0() #mult(#neg(@x),#neg(@y)) = [1] >= [1] = #pos(#natmult(@x,@y)) #mult(#neg(@x),#pos(@y)) = [1] >= [1] = #neg(#natmult(@x,@y)) #mult(#pos(@x),#0()) = [1] >= [0] = #0() #mult(#pos(@x),#neg(@y)) = [1] >= [1] = #neg(#natmult(@x,@y)) #mult(#pos(@x),#pos(@y)) = [1] >= [1] = #pos(#natmult(@x,@y)) #natmult(#0(),@y) = [1] >= [0] = #0() #natmult(#s(@x),@y) = [1] >= [1] = #add(#pos(@y),#natmult(@x,@y)) #pred(#0()) = [0] >= [0] = #neg(#s(#0())) #pred(#neg(#s(@x))) = [0] >= [0] = #neg(#s(#s(@x))) #pred(#pos(#s(#0()))) = [0] >= [0] = #0() #pred(#pos(#s(#s(@x)))) = [0] >= [0] = #pos(#s(@x)) #succ(#0()) = [0] >= [0] = #pos(#s(#0())) #succ(#neg(#s(#0()))) = [0] >= [0] = #0() #succ(#neg(#s(#s(@x)))) = [0] >= [0] = #neg(#s(@x)) #succ(#pos(#s(@x))) = [0] >= [0] = #pos(#s(#s(@x))) *(@x,@y) = [2] >= [1] = #mult(@x,@y) +(@x,@y) = [1] @x + [1] @y + [0] >= [1] @y + [0] = #add(@x,@y) lineMult(@n,@l1,@l2) = [3] @l1 + [1] @l2 + [0] >= [3] @l1 + [1] @l2 + [0] = lineMult#1(@l1,@l2,@n) lineMult#1(::(@x,@xs),@l2,@n) = [1] @l2 + [3] @x + [3] @xs + [3] >= [1] @l2 + [3] @x + [3] @xs + [3] = lineMult#2(@l2,@n,@x,@xs) lineMult#1(nil(),@l2,@n) = [1] @l2 + [0] >= [0] = nil() lineMult#2(::(@y,@ys),@n,@x,@xs) = [3] @x + [3] @xs + [1] @y + [1] @ys + [4] >= [3] @xs + [1] @y + [1] @ys + [3] = ::(+(*(@x,@n),@y),lineMult(@n,@xs,@ys)) lineMult#2(nil(),@n,@x,@xs) = [3] @x + [3] @xs + [3] >= [3] @xs + [3] = ::(*(@x,@n),lineMult(@n,@xs,nil())) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 6.b:1.b:3: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: lineMult#1#(::(@x,@xs),@l2,@n) -> c_9(lineMult#2#(@l2,@n,@x,@xs)) - Weak DPs: computeLine#(@line,@m,@acc) -> computeLine#1#(@line,@acc,@m) computeLine#1#(::(@x,@xs),@acc,@m) -> computeLine#2#(@m,@acc,@x,@xs) computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> lineMult#(@x,@l,@acc) lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(lineMult#(@n,@xs,@ys)) lineMult#2#(nil(),@n,@x,@xs) -> c_12(lineMult#(@n,@xs,nil())) matrixMult#(@m1,@m2) -> matrixMult#1#(@m1,@m2) matrixMult#1#(::(@l,@ls),@m2) -> computeLine#(@l,@m2,nil()) matrixMult#1#(::(@l,@ls),@m2) -> matrixMult#(@ls,@m2) - 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)) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@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))) *(@x,@y) -> #mult(@x,@y) +(@x,@y) -> #add(@x,@y) lineMult(@n,@l1,@l2) -> lineMult#1(@l1,@l2,@n) lineMult#1(::(@x,@xs),@l2,@n) -> lineMult#2(@l2,@n,@x,@xs) lineMult#1(nil(),@l2,@n) -> nil() lineMult#2(::(@y,@ys),@n,@x,@xs) -> ::(+(*(@x,@n),@y),lineMult(@n,@xs,@ys)) lineMult#2(nil(),@n,@x,@xs) -> ::(*(@x,@n),lineMult(@n,@xs,nil())) - Signature: {#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,+/2,computeLine/3,computeLine#1/3,computeLine#2/4,lineMult/3 ,lineMult#1/3,lineMult#2/4,matrixMult/2,matrixMult#1/2,#add#/2,#mult#/2,#natmult#/2,#pred#/1,#succ#/1,*#/2 ,+#/2,computeLine#/3,computeLine#1#/3,computeLine#2#/4,lineMult#/3,lineMult#1#/3,lineMult#2#/4,matrixMult#/2 ,matrixMult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/2,c_7/0,c_8/1 ,c_9/1,c_10/0,c_11/1,c_12/1,c_13/1,c_14/2,c_15/0,c_16/0,c_17/1,c_18/2,c_19/1,c_20/2,c_21/0,c_22/0,c_23/0 ,c_24/0,c_25/1,c_26/1,c_27/0,c_28/1,c_29/1,c_30/0,c_31/2,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0 ,c_39/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine# ,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult# ,matrixMult#1#} and constructors {#0,#neg,#pos,#s,::,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(#add) = {2}, uargs(#neg) = {1}, uargs(#pos) = {1}, uargs(#pred) = {1}, uargs(#succ) = {1}, uargs(+) = {1}, uargs(::) = {1,2}, uargs(computeLine#) = {3}, uargs(c_8) = {1}, uargs(c_9) = {1}, uargs(c_11) = {1}, uargs(c_12) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#add) = [1] x2 + [0] p(#mult) = [0] p(#natmult) = [0] p(#neg) = [1] x1 + [0] p(#pos) = [1] x1 + [0] p(#pred) = [1] x1 + [0] p(#s) = [0] p(#succ) = [1] x1 + [0] p(*) = [1] x1 + [1] p(+) = [1] x1 + [1] x2 + [2] p(::) = [1] x1 + [1] x2 + [2] p(computeLine) = [2] x1 + [1] x3 + [1] p(computeLine#1) = [1] x1 + [4] p(computeLine#2) = [2] x2 + [2] x4 + [0] p(lineMult) = [4] x2 + [1] x3 + [1] p(lineMult#1) = [4] x1 + [1] x2 + [1] p(lineMult#2) = [1] x1 + [4] x3 + [4] x4 + [4] p(matrixMult) = [4] x1 + [1] p(matrixMult#1) = [2] p(nil) = [0] p(#add#) = [1] x1 + [1] x2 + [4] p(#mult#) = [1] x1 + [4] x2 + [0] p(#natmult#) = [1] x2 + [1] p(#pred#) = [0] p(#succ#) = [2] x1 + [1] p(*#) = [0] p(+#) = [1] x1 + [1] p(computeLine#) = [4] x2 + [1] x3 + [0] p(computeLine#1#) = [1] x2 + [4] x3 + [0] p(computeLine#2#) = [4] x1 + [1] x2 + [0] p(lineMult#) = [1] x2 + [0] p(lineMult#1#) = [1] x1 + [0] p(lineMult#2#) = [1] x3 + [1] x4 + [0] p(matrixMult#) = [4] x2 + [0] p(matrixMult#1#) = [4] x2 + [0] p(c_1) = [1] p(c_2) = [0] p(c_3) = [1] p(c_4) = [2] x1 + [1] p(c_5) = [4] p(c_6) = [2] x1 + [1] x2 + [1] p(c_7) = [1] p(c_8) = [1] x1 + [0] p(c_9) = [1] x1 + [1] p(c_10) = [4] p(c_11) = [1] x1 + [0] p(c_12) = [1] x1 + [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [4] p(c_16) = [1] p(c_17) = [4] p(c_18) = [1] x2 + [2] p(c_19) = [4] x1 + [1] p(c_20) = [2] p(c_21) = [0] p(c_22) = [2] p(c_23) = [1] p(c_24) = [1] p(c_25) = [0] p(c_26) = [1] x1 + [1] p(c_27) = [2] p(c_28) = [1] p(c_29) = [2] p(c_30) = [1] p(c_31) = [4] x2 + [0] p(c_32) = [4] p(c_33) = [2] p(c_34) = [2] p(c_35) = [0] p(c_36) = [0] p(c_37) = [0] p(c_38) = [1] p(c_39) = [1] Following rules are strictly oriented: lineMult#1#(::(@x,@xs),@l2,@n) = [1] @x + [1] @xs + [2] > [1] @x + [1] @xs + [1] = c_9(lineMult#2#(@l2,@n,@x,@xs)) Following rules are (at-least) weakly oriented: computeLine#(@line,@m,@acc) = [1] @acc + [4] @m + [0] >= [1] @acc + [4] @m + [0] = computeLine#1#(@line,@acc,@m) computeLine#1#(::(@x,@xs),@acc,@m) = [1] @acc + [4] @m + [0] >= [1] @acc + [4] @m + [0] = computeLine#2#(@m,@acc,@x,@xs) computeLine#2#(::(@l,@ls),@acc,@x,@xs) = [1] @acc + [4] @l + [4] @ls + [8] >= [1] @acc + [4] @l + [4] @ls + [1] = computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) computeLine#2#(::(@l,@ls),@acc,@x,@xs) = [1] @acc + [4] @l + [4] @ls + [8] >= [1] @l + [0] = lineMult#(@x,@l,@acc) lineMult#(@n,@l1,@l2) = [1] @l1 + [0] >= [1] @l1 + [0] = c_8(lineMult#1#(@l1,@l2,@n)) lineMult#2#(::(@y,@ys),@n,@x,@xs) = [1] @x + [1] @xs + [0] >= [1] @xs + [0] = c_11(lineMult#(@n,@xs,@ys)) lineMult#2#(nil(),@n,@x,@xs) = [1] @x + [1] @xs + [0] >= [1] @xs + [0] = c_12(lineMult#(@n,@xs,nil())) matrixMult#(@m1,@m2) = [4] @m2 + [0] >= [4] @m2 + [0] = matrixMult#1#(@m1,@m2) matrixMult#1#(::(@l,@ls),@m2) = [4] @m2 + [0] >= [4] @m2 + [0] = computeLine#(@l,@m2,nil()) matrixMult#1#(::(@l,@ls),@m2) = [4] @m2 + [0] >= [4] @m2 + [0] = matrixMult#(@ls,@m2) #add(#0(),@y) = [1] @y + [0] >= [1] @y + [0] = @y #add(#neg(#s(#0())),@y) = [1] @y + [0] >= [1] @y + [0] = #pred(@y) #add(#neg(#s(#s(@x))),@y) = [1] @y + [0] >= [1] @y + [0] = #pred(#add(#pos(#s(@x)),@y)) #add(#pos(#s(#0())),@y) = [1] @y + [0] >= [1] @y + [0] = #succ(@y) #add(#pos(#s(#s(@x))),@y) = [1] @y + [0] >= [1] @y + [0] = #succ(#add(#pos(#s(@x)),@y)) #mult(#0(),#0()) = [0] >= [0] = #0() #mult(#0(),#neg(@y)) = [0] >= [0] = #0() #mult(#0(),#pos(@y)) = [0] >= [0] = #0() #mult(#neg(@x),#0()) = [0] >= [0] = #0() #mult(#neg(@x),#neg(@y)) = [0] >= [0] = #pos(#natmult(@x,@y)) #mult(#neg(@x),#pos(@y)) = [0] >= [0] = #neg(#natmult(@x,@y)) #mult(#pos(@x),#0()) = [0] >= [0] = #0() #mult(#pos(@x),#neg(@y)) = [0] >= [0] = #neg(#natmult(@x,@y)) #mult(#pos(@x),#pos(@y)) = [0] >= [0] = #pos(#natmult(@x,@y)) #natmult(#0(),@y) = [0] >= [0] = #0() #natmult(#s(@x),@y) = [0] >= [0] = #add(#pos(@y),#natmult(@x,@y)) #pred(#0()) = [0] >= [0] = #neg(#s(#0())) #pred(#neg(#s(@x))) = [0] >= [0] = #neg(#s(#s(@x))) #pred(#pos(#s(#0()))) = [0] >= [0] = #0() #pred(#pos(#s(#s(@x)))) = [0] >= [0] = #pos(#s(@x)) #succ(#0()) = [0] >= [0] = #pos(#s(#0())) #succ(#neg(#s(#0()))) = [0] >= [0] = #0() #succ(#neg(#s(#s(@x)))) = [0] >= [0] = #neg(#s(@x)) #succ(#pos(#s(@x))) = [0] >= [0] = #pos(#s(#s(@x))) *(@x,@y) = [1] @x + [1] >= [0] = #mult(@x,@y) +(@x,@y) = [1] @x + [1] @y + [2] >= [1] @y + [0] = #add(@x,@y) lineMult(@n,@l1,@l2) = [4] @l1 + [1] @l2 + [1] >= [4] @l1 + [1] @l2 + [1] = lineMult#1(@l1,@l2,@n) lineMult#1(::(@x,@xs),@l2,@n) = [1] @l2 + [4] @x + [4] @xs + [9] >= [1] @l2 + [4] @x + [4] @xs + [4] = lineMult#2(@l2,@n,@x,@xs) lineMult#1(nil(),@l2,@n) = [1] @l2 + [1] >= [0] = nil() lineMult#2(::(@y,@ys),@n,@x,@xs) = [4] @x + [4] @xs + [1] @y + [1] @ys + [6] >= [1] @x + [4] @xs + [1] @y + [1] @ys + [6] = ::(+(*(@x,@n),@y),lineMult(@n,@xs,@ys)) lineMult#2(nil(),@n,@x,@xs) = [4] @x + [4] @xs + [4] >= [1] @x + [4] @xs + [4] = ::(*(@x,@n),lineMult(@n,@xs,nil())) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 6.b:1.b:4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: computeLine#(@line,@m,@acc) -> computeLine#1#(@line,@acc,@m) computeLine#1#(::(@x,@xs),@acc,@m) -> computeLine#2#(@m,@acc,@x,@xs) computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> lineMult#(@x,@l,@acc) lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) lineMult#1#(::(@x,@xs),@l2,@n) -> c_9(lineMult#2#(@l2,@n,@x,@xs)) lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(lineMult#(@n,@xs,@ys)) lineMult#2#(nil(),@n,@x,@xs) -> c_12(lineMult#(@n,@xs,nil())) matrixMult#(@m1,@m2) -> matrixMult#1#(@m1,@m2) matrixMult#1#(::(@l,@ls),@m2) -> computeLine#(@l,@m2,nil()) matrixMult#1#(::(@l,@ls),@m2) -> matrixMult#(@ls,@m2) - 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)) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@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))) *(@x,@y) -> #mult(@x,@y) +(@x,@y) -> #add(@x,@y) lineMult(@n,@l1,@l2) -> lineMult#1(@l1,@l2,@n) lineMult#1(::(@x,@xs),@l2,@n) -> lineMult#2(@l2,@n,@x,@xs) lineMult#1(nil(),@l2,@n) -> nil() lineMult#2(::(@y,@ys),@n,@x,@xs) -> ::(+(*(@x,@n),@y),lineMult(@n,@xs,@ys)) lineMult#2(nil(),@n,@x,@xs) -> ::(*(@x,@n),lineMult(@n,@xs,nil())) - Signature: {#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,+/2,computeLine/3,computeLine#1/3,computeLine#2/4,lineMult/3 ,lineMult#1/3,lineMult#2/4,matrixMult/2,matrixMult#1/2,#add#/2,#mult#/2,#natmult#/2,#pred#/1,#succ#/1,*#/2 ,+#/2,computeLine#/3,computeLine#1#/3,computeLine#2#/4,lineMult#/3,lineMult#1#/3,lineMult#2#/4,matrixMult#/2 ,matrixMult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/2,c_7/0,c_8/1 ,c_9/1,c_10/0,c_11/1,c_12/1,c_13/1,c_14/2,c_15/0,c_16/0,c_17/1,c_18/2,c_19/1,c_20/2,c_21/0,c_22/0,c_23/0 ,c_24/0,c_25/1,c_26/1,c_27/0,c_28/1,c_29/1,c_30/0,c_31/2,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0 ,c_39/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine# ,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult# ,matrixMult#1#} and constructors {#0,#neg,#pos,#s,::,nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^3))