WORST_CASE(?,O(n^2)) * Step 1: DependencyPairs WORST_CASE(?,O(n^2)) + 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: UsableRules WORST_CASE(?,O(n^2)) + 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: 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())) #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#(@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() * Step 3: PredecessorEstimation WORST_CASE(?,O(n^2)) + 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) 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/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 4: RemoveWeakSuffixes 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(+#(*(@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) 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/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 5: SimplifyRHS 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(+#(*(@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) 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/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 6: Decompose 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())) 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: Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd} + Details: We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component. Problem (R) - 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) -> 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} Problem (S) - 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 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 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} ** Step 6.a:1: PredecessorEstimationCP 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) -> 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: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 3: computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) ,lineMult#(@x,@l,@acc)) 6: lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(lineMult#(@n,@xs,@ys)) The strictly oriented rules are moved into the weak component. *** Step 6.a:1.a:1: NaturalPI 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) -> 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: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(c_3) = {1}, uargs(c_4) = {1}, uargs(c_6) = {1,2}, uargs(c_8) = {1}, uargs(c_9) = {1}, uargs(c_11) = {1}, uargs(c_12) = {1}, uargs(c_13) = {1}, uargs(c_14) = {1,2} Following symbols are considered usable: {#add,#mult,#pred,#succ,*,+,lineMult,lineMult#1,lineMult#2,#add#,#mult#,#natmult#,#pred#,#succ#,*#,+# ,computeLine#,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult#,matrixMult#1#} TcT has computed the following interpretation: p(#0) = 0 p(#add) = x2 p(#mult) = 0 p(#natmult) = 0 p(#neg) = 0 p(#pos) = 0 p(#pred) = 0 p(#s) = 0 p(#succ) = 0 p(*) = 0 p(+) = 1 + x2 p(::) = 1 + x1 + x2 p(computeLine) = 0 p(computeLine#1) = 0 p(computeLine#2) = 0 p(lineMult) = x2 + x3 p(lineMult#1) = x1 + x2 p(lineMult#2) = 1 + x1 + x3 + x4 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(+#) = 0 p(computeLine#) = x1*x2 + x1*x3 + x1^2 p(computeLine#1#) = x1*x2 + x1*x3 + x1^2 p(computeLine#2#) = 1 + x1 + x1*x4 + x2 + x2*x4 + x4^2 p(lineMult#) = x3 p(lineMult#1#) = x2 p(lineMult#2#) = x1 p(matrixMult#) = x1*x2 + x1^2 p(matrixMult#1#) = x1*x2 + x1^2 p(c_1) = 0 p(c_2) = 0 p(c_3) = x1 p(c_4) = x1 p(c_5) = 0 p(c_6) = 1 + x1 + x2 p(c_7) = 0 p(c_8) = x1 p(c_9) = x1 p(c_10) = 0 p(c_11) = x1 p(c_12) = x1 p(c_13) = x1 p(c_14) = x1 + x2 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: computeLine#2#(::(@l,@ls),@acc,@x,@xs) = 2 + @acc + @acc*@xs + @l + @l*@xs + @ls + @ls*@xs + @xs + @xs^2 > 1 + @acc + @acc*@xs + @l*@xs + @ls*@xs + @xs^2 = c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)),lineMult#(@x,@l,@acc)) lineMult#2#(::(@y,@ys),@n,@x,@xs) = 1 + @y + @ys > @ys = c_11(lineMult#(@n,@xs,@ys)) Following rules are (at-least) weakly oriented: computeLine#(@line,@m,@acc) = @acc*@line + @line*@m + @line^2 >= @acc*@line + @line*@m + @line^2 = c_3(computeLine#1#(@line,@acc,@m)) computeLine#1#(::(@x,@xs),@acc,@m) = 1 + @acc + @acc*@x + @acc*@xs + @m + @m*@x + @m*@xs + 2*@x + 2*@x*@xs + @x^2 + 2*@xs + @xs^2 >= 1 + @acc + @acc*@xs + @m + @m*@xs + @xs^2 = c_4(computeLine#2#(@m,@acc,@x,@xs)) lineMult#(@n,@l1,@l2) = @l2 >= @l2 = c_8(lineMult#1#(@l1,@l2,@n)) lineMult#1#(::(@x,@xs),@l2,@n) = @l2 >= @l2 = c_9(lineMult#2#(@l2,@n,@x,@xs)) lineMult#2#(nil(),@n,@x,@xs) = 0 >= 0 = c_12(lineMult#(@n,@xs,nil())) matrixMult#(@m1,@m2) = @m1*@m2 + @m1^2 >= @m1*@m2 + @m1^2 = c_13(matrixMult#1#(@m1,@m2)) matrixMult#1#(::(@l,@ls),@m2) = 1 + 2*@l + 2*@l*@ls + @l*@m2 + @l^2 + 2*@ls + @ls*@m2 + @ls^2 + @m2 >= @l*@m2 + @l^2 + @ls*@m2 + @ls^2 = c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2)) #add(#0(),@y) = @y >= @y = @y #add(#neg(#s(#0())),@y) = @y >= 0 = #pred(@y) #add(#neg(#s(#s(@x))),@y) = @y >= 0 = #pred(#add(#pos(#s(@x)),@y)) #add(#pos(#s(#0())),@y) = @y >= 0 = #succ(@y) #add(#pos(#s(#s(@x))),@y) = @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)) #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 + @y >= @y = #add(@x,@y) lineMult(@n,@l1,@l2) = @l1 + @l2 >= @l1 + @l2 = lineMult#1(@l1,@l2,@n) lineMult#1(::(@x,@xs),@l2,@n) = 1 + @l2 + @x + @xs >= 1 + @l2 + @x + @xs = lineMult#2(@l2,@n,@x,@xs) lineMult#1(nil(),@l2,@n) = @l2 >= 0 = nil() lineMult#2(::(@y,@ys),@n,@x,@xs) = 2 + @x + @xs + @y + @ys >= 2 + @xs + @y + @ys = ::(+(*(@x,@n),@y),lineMult(@n,@xs,@ys)) lineMult#2(nil(),@n,@x,@xs) = 1 + @x + @xs >= 1 + @xs = ::(*(@x,@n),lineMult(@n,@xs,nil())) *** Step 6.a:1.a:2: Assumption WORST_CASE(?,O(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)) 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#(nil(),@n,@x,@xs) -> c_12(lineMult#(@n,@xs,nil())) - Weak DPs: computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) ,lineMult#(@x,@l,@acc)) lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(lineMult#(@n,@xs,@ys)) 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: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () *** Step 6.a:1.b:1: PredecessorEstimationCP 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)) 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#(nil(),@n,@x,@xs) -> c_12(lineMult#(@n,@xs,nil())) - Weak DPs: computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) ,lineMult#(@x,@l,@acc)) lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(lineMult#(@n,@xs,@ys)) 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: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 4: lineMult#1#(::(@x,@xs),@l2,@n) -> c_9(lineMult#2#(@l2,@n,@x,@xs)) Consider the set of all dependency pairs 1: computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)) 2: computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs)) 3: lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) 4: lineMult#1#(::(@x,@xs),@l2,@n) -> c_9(lineMult#2#(@l2,@n,@x,@xs)) 5: lineMult#2#(nil(),@n,@x,@xs) -> c_12(lineMult#(@n,@xs,nil())) 6: computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) ,lineMult#(@x,@l,@acc)) 7: lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(lineMult#(@n,@xs,@ys)) 8: matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2)) 9: matrixMult#1#(::(@l,@ls),@m2) -> c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2)) Processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^2)) SPACE(?,?)on application of the dependency pairs {4} These cover all (indirect) predecessors of dependency pairs {4,5,7} their number of applications is equally bounded. The dependency pairs are shifted into the weak component. **** Step 6.a:1.b:1.a:1: NaturalPI 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)) 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#(nil(),@n,@x,@xs) -> c_12(lineMult#(@n,@xs,nil())) - Weak DPs: computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) ,lineMult#(@x,@l,@acc)) lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(lineMult#(@n,@xs,@ys)) 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: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(c_3) = {1}, uargs(c_4) = {1}, uargs(c_6) = {1,2}, uargs(c_8) = {1}, uargs(c_9) = {1}, uargs(c_11) = {1}, uargs(c_12) = {1}, uargs(c_13) = {1}, uargs(c_14) = {1,2} Following symbols are considered usable: {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine#,computeLine#1#,computeLine#2#,lineMult# ,lineMult#1#,lineMult#2#,matrixMult#,matrixMult#1#} TcT has computed the following interpretation: p(#0) = 1 p(#add) = x2^2 p(#mult) = 1 + x1 p(#natmult) = 1 p(#neg) = 0 p(#pos) = 0 p(#pred) = 1 + x1 p(#s) = 0 p(#succ) = 1 p(*) = x2^2 p(+) = 1 + x1*x2 + x2^2 p(::) = 1 + x1 + x2 p(computeLine) = 0 p(computeLine#1) = 0 p(computeLine#2) = 0 p(lineMult) = x1 p(lineMult#1) = 1 + x3^2 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(+#) = 0 p(computeLine#) = x1 + x1*x2 + x2 p(computeLine#1#) = x1*x3 p(computeLine#2#) = x1 + x1*x4 p(lineMult#) = x2 p(lineMult#1#) = x1 p(lineMult#2#) = x4 p(matrixMult#) = 1 + x1*x2 + x1^2 p(matrixMult#1#) = 1 + x1*x2 + x1^2 p(c_1) = 0 p(c_2) = 0 p(c_3) = x1 p(c_4) = x1 p(c_5) = 0 p(c_6) = 1 + x1 + x2 p(c_7) = 0 p(c_8) = x1 p(c_9) = x1 p(c_10) = 0 p(c_11) = x1 p(c_12) = x1 p(c_13) = x1 p(c_14) = 1 + x1 + x2 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: lineMult#1#(::(@x,@xs),@l2,@n) = 1 + @x + @xs > @xs = c_9(lineMult#2#(@l2,@n,@x,@xs)) Following rules are (at-least) weakly oriented: computeLine#(@line,@m,@acc) = @line + @line*@m + @m >= @line*@m = c_3(computeLine#1#(@line,@acc,@m)) computeLine#1#(::(@x,@xs),@acc,@m) = @m + @m*@x + @m*@xs >= @m + @m*@xs = c_4(computeLine#2#(@m,@acc,@x,@xs)) computeLine#2#(::(@l,@ls),@acc,@x,@xs) = 1 + @l + @l*@xs + @ls + @ls*@xs + @xs >= 1 + @l + @ls + @ls*@xs + @xs = c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)),lineMult#(@x,@l,@acc)) lineMult#(@n,@l1,@l2) = @l1 >= @l1 = c_8(lineMult#1#(@l1,@l2,@n)) lineMult#2#(::(@y,@ys),@n,@x,@xs) = @xs >= @xs = c_11(lineMult#(@n,@xs,@ys)) lineMult#2#(nil(),@n,@x,@xs) = @xs >= @xs = c_12(lineMult#(@n,@xs,nil())) matrixMult#(@m1,@m2) = 1 + @m1*@m2 + @m1^2 >= 1 + @m1*@m2 + @m1^2 = c_13(matrixMult#1#(@m1,@m2)) matrixMult#1#(::(@l,@ls),@m2) = 2 + 2*@l + 2*@l*@ls + @l*@m2 + @l^2 + 2*@ls + @ls*@m2 + @ls^2 + @m2 >= 2 + @l + @l*@m2 + @ls*@m2 + @ls^2 + @m2 = c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2)) **** Step 6.a:1.b:1.a:2: Assumption WORST_CASE(?,O(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)) lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) lineMult#2#(nil(),@n,@x,@xs) -> c_12(lineMult#(@n,@xs,nil())) - Weak DPs: computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) ,lineMult#(@x,@l,@acc)) 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)) 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: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () **** Step 6.a:1.b:1.b:1: PredecessorEstimationCP 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)) lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) - Weak DPs: computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) ,lineMult#(@x,@l,@acc)) 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: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 2: computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs)) Consider the set of all dependency pairs 1: computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)) 2: computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs)) 3: lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) 4: computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) ,lineMult#(@x,@l,@acc)) 5: lineMult#1#(::(@x,@xs),@l2,@n) -> c_9(lineMult#2#(@l2,@n,@x,@xs)) 6: lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(lineMult#(@n,@xs,@ys)) 7: lineMult#2#(nil(),@n,@x,@xs) -> c_12(lineMult#(@n,@xs,nil())) 8: matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2)) 9: matrixMult#1#(::(@l,@ls),@m2) -> c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2)) Processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^1)) SPACE(?,?)on application of the dependency pairs {2} These cover all (indirect) predecessors of dependency pairs {2,4} their number of applications is equally bounded. The dependency pairs are shifted into the weak component. ***** Step 6.a:1.b:1.b:1.a:1: NaturalMI 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)) lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) - Weak DPs: computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) ,lineMult#(@x,@l,@acc)) 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: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_3) = {1}, uargs(c_4) = {1}, uargs(c_6) = {1,2}, uargs(c_8) = {1}, uargs(c_9) = {1}, uargs(c_11) = {1}, uargs(c_12) = {1}, uargs(c_13) = {1}, uargs(c_14) = {1,2} Following symbols are considered usable: {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine#,computeLine#1#,computeLine#2#,lineMult# ,lineMult#1#,lineMult#2#,matrixMult#,matrixMult#1#} TcT has computed the following interpretation: p(#0) = [0] p(#add) = [4] x1 + [6] p(#mult) = [1] x2 + [1] p(#natmult) = [2] x1 + [3] p(#neg) = [0] p(#pos) = [2] p(#pred) = [0] p(#s) = [0] p(#succ) = [0] p(*) = [2] x1 + [2] p(+) = [3] x1 + [0] p(::) = [1] x1 + [1] x2 + [2] p(computeLine) = [1] p(computeLine#1) = [4] x1 + [1] x2 + [1] x3 + [1] p(computeLine#2) = [2] x2 + [2] x3 + [1] x4 + [1] p(lineMult) = [0] p(lineMult#1) = [0] p(lineMult#2) = [2] x4 + [0] p(matrixMult) = [2] x1 + [1] x2 + [0] p(matrixMult#1) = [1] x1 + [0] p(nil) = [0] p(#add#) = [4] x1 + [0] p(#mult#) = [2] x1 + [1] x2 + [0] p(#natmult#) = [1] x2 + [1] p(#pred#) = [4] x1 + [1] p(#succ#) = [2] p(*#) = [4] x1 + [0] p(+#) = [1] x2 + [1] p(computeLine#) = [2] x1 + [4] p(computeLine#1#) = [2] x1 + [4] p(computeLine#2#) = [2] x3 + [2] x4 + [5] p(lineMult#) = [0] p(lineMult#1#) = [0] p(lineMult#2#) = [0] p(matrixMult#) = [5] x1 + [0] p(matrixMult#1#) = [5] x1 + [0] p(c_1) = [1] x1 + [0] p(c_2) = [2] x1 + [1] p(c_3) = [1] x1 + [0] p(c_4) = [1] x1 + [1] p(c_5) = [0] p(c_6) = [1] x1 + [2] x2 + [1] p(c_7) = [1] p(c_8) = [2] x1 + [0] p(c_9) = [2] x1 + [0] p(c_10) = [4] p(c_11) = [2] x1 + [0] p(c_12) = [1] x1 + [0] p(c_13) = [1] x1 + [0] p(c_14) = [2] x1 + [1] x2 + [2] p(c_15) = [1] p(c_16) = [1] p(c_17) = [0] p(c_18) = [2] p(c_19) = [1] p(c_20) = [1] x1 + [1] p(c_21) = [1] p(c_22) = [2] p(c_23) = [1] p(c_24) = [0] p(c_25) = [0] p(c_26) = [1] x1 + [0] p(c_27) = [1] p(c_28) = [1] x1 + [1] p(c_29) = [1] x1 + [1] p(c_30) = [1] p(c_31) = [0] p(c_32) = [0] p(c_33) = [0] p(c_34) = [2] p(c_35) = [0] p(c_36) = [1] p(c_37) = [0] p(c_38) = [0] p(c_39) = [1] Following rules are strictly oriented: computeLine#1#(::(@x,@xs),@acc,@m) = [2] @x + [2] @xs + [8] > [2] @x + [2] @xs + [6] = c_4(computeLine#2#(@m,@acc,@x,@xs)) Following rules are (at-least) weakly oriented: computeLine#(@line,@m,@acc) = [2] @line + [4] >= [2] @line + [4] = c_3(computeLine#1#(@line,@acc,@m)) computeLine#2#(::(@l,@ls),@acc,@x,@xs) = [2] @x + [2] @xs + [5] >= [2] @xs + [5] = c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)),lineMult#(@x,@l,@acc)) lineMult#(@n,@l1,@l2) = [0] >= [0] = c_8(lineMult#1#(@l1,@l2,@n)) lineMult#1#(::(@x,@xs),@l2,@n) = [0] >= [0] = c_9(lineMult#2#(@l2,@n,@x,@xs)) lineMult#2#(::(@y,@ys),@n,@x,@xs) = [0] >= [0] = c_11(lineMult#(@n,@xs,@ys)) lineMult#2#(nil(),@n,@x,@xs) = [0] >= [0] = c_12(lineMult#(@n,@xs,nil())) matrixMult#(@m1,@m2) = [5] @m1 + [0] >= [5] @m1 + [0] = c_13(matrixMult#1#(@m1,@m2)) matrixMult#1#(::(@l,@ls),@m2) = [5] @l + [5] @ls + [10] >= [4] @l + [5] @ls + [10] = c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2)) ***** Step 6.a:1.b:1.b:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)) lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) - Weak DPs: 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#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: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () ***** Step 6.a:1.b:1.b:1.b:1: PredecessorEstimationCP WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)) lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) - Weak DPs: 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#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: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 2, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 2, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)) Consider the set of all dependency pairs 1: computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)) 2: lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) 3: computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs)) 4: computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) ,lineMult#(@x,@l,@acc)) 5: lineMult#1#(::(@x,@xs),@l2,@n) -> c_9(lineMult#2#(@l2,@n,@x,@xs)) 6: lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(lineMult#(@n,@xs,@ys)) 7: lineMult#2#(nil(),@n,@x,@xs) -> c_12(lineMult#(@n,@xs,nil())) 8: matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2)) 9: matrixMult#1#(::(@l,@ls),@m2) -> c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2)) Processor NaturalMI {miDimension = 2, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^1)) SPACE(?,?)on application of the dependency pairs {1} These cover all (indirect) predecessors of dependency pairs {1,3,4} their number of applications is equally bounded. The dependency pairs are shifted into the weak component. ****** Step 6.a:1.b:1.b:1.b:1.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)) lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) - Weak DPs: 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#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: NaturalMI {miDimension = 2, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 1 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_3) = {1}, uargs(c_4) = {1}, uargs(c_6) = {1,2}, uargs(c_8) = {1}, uargs(c_9) = {1}, uargs(c_11) = {1}, uargs(c_12) = {1}, uargs(c_13) = {1}, uargs(c_14) = {1,2} Following symbols are considered usable: {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine#,computeLine#1#,computeLine#2#,lineMult# ,lineMult#1#,lineMult#2#,matrixMult#,matrixMult#1#} TcT has computed the following interpretation: p(#0) = [0] [1] p(#add) = [0 1] x1 + [0 0] x2 + [0] [0 0] [1 0] [0] p(#mult) = [0 0] x1 + [0 0] x2 + [0] [0 1] [0 1] [1] p(#natmult) = [0] [0] p(#neg) = [1 0] x1 + [0] [0 0] [1] p(#pos) = [0] [1] p(#pred) = [0 0] x1 + [1] [1 0] [1] p(#s) = [0 1] x1 + [1] [0 0] [0] p(#succ) = [0 1] x1 + [1] [0 0] [0] p(*) = [0] [0] p(+) = [0] [0] p(::) = [1 1] x1 + [1 1] x2 + [1] [0 0] [0 0] [0] p(computeLine) = [0] [0] p(computeLine#1) = [0] [0] p(computeLine#2) = [0] [0] p(lineMult) = [0 1] x1 + [0] [0 0] [0] p(lineMult#1) = [1 0] x1 + [1] [0 0] [0] p(lineMult#2) = [0 0] x1 + [1] [1 0] [1] p(matrixMult) = [0] [0] p(matrixMult#1) = [0] [0] p(nil) = [0] [0] p(#add#) = [0] [0] p(#mult#) = [0] [0] p(#natmult#) = [0] [0] p(#pred#) = [0] [0] p(#succ#) = [0] [0] p(*#) = [0] [0] p(+#) = [0] [0] p(computeLine#) = [1 0] x1 + [1] [0 1] [0] p(computeLine#1#) = [1 0] x1 + [0 0] x2 + [0] [0 0] [0 1] [1] p(computeLine#2#) = [0 0] x1 + [0 0] x2 + [1 1] x3 + [1 0] x4 + [1] [1 0] [1 1] [1 1] [0 0] [0] p(lineMult#) = [0 0] x1 + [0 0] x2 + [0] [0 1] [0 1] [0] p(lineMult#1#) = [0 0] x3 + [0] [1 1] [1] p(lineMult#2#) = [0 0] x1 + [0 0] x4 + [0] [1 0] [0 1] [1] p(matrixMult#) = [1 0] x1 + [0 1] x2 + [0] [0 0] [1 0] [1] p(matrixMult#1#) = [1 0] x1 + [0 1] x2 + [0] [1 0] [0 1] [0] p(c_1) = [0] [0] p(c_2) = [0] [0] p(c_3) = [1 0] x1 + [0] [0 0] [0] p(c_4) = [1 0] x1 + [0] [0 0] [1] p(c_5) = [0] [0] p(c_6) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 1] [1] p(c_7) = [0] [0] p(c_8) = [1 0] x1 + [0] [0 0] [0] p(c_9) = [1 0] x1 + [0] [0 0] [0] p(c_10) = [0] [0] p(c_11) = [1 0] x1 + [0] [0 0] [0] p(c_12) = [1 0] x1 + [0] [0 0] [0] p(c_13) = [1 0] x1 + [0] [0 0] [1] p(c_14) = [1 1] x1 + [1 0] x2 + [0] [0 0] [1 0] [1] p(c_15) = [0] [0] p(c_16) = [0] [0] p(c_17) = [0] [0] p(c_18) = [0] [0] p(c_19) = [0] [0] p(c_20) = [0] [0] p(c_21) = [0] [0] p(c_22) = [0] [0] p(c_23) = [0] [0] p(c_24) = [0] [0] p(c_25) = [0] [0] p(c_26) = [0] [0] p(c_27) = [0] [0] p(c_28) = [0] [0] p(c_29) = [0] [0] p(c_30) = [0] [0] p(c_31) = [0] [0] p(c_32) = [0] [0] p(c_33) = [0] [0] p(c_34) = [0] [0] p(c_35) = [0] [0] p(c_36) = [0] [0] p(c_37) = [0] [0] p(c_38) = [0] [0] p(c_39) = [0] [0] Following rules are strictly oriented: computeLine#(@line,@m,@acc) = [1 0] @line + [1] [0 1] [0] > [1 0] @line + [0] [0 0] [0] = c_3(computeLine#1#(@line,@acc,@m)) Following rules are (at-least) weakly oriented: computeLine#1#(::(@x,@xs),@acc,@m) = [0 0] @acc + [1 1] @x + [1 1] @xs + [1] [0 1] [0 0] [0 0] [1] >= [1 1] @x + [1 0] @xs + [1] [0 0] [0 0] [1] = c_4(computeLine#2#(@m,@acc,@x,@xs)) computeLine#2#(::(@l,@ls),@acc,@x,@xs) = [0 0] @acc + [0 0] @l + [0 0] @ls + [1 1] @x + [1 0] @xs + [1] [1 1] [1 1] [1 1] [1 1] [0 0] [1] >= [0 0] @l + [0 0] @x + [1 0] @xs + [1] [0 1] [0 1] [0 0] [1] = c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)),lineMult#(@x,@l,@acc)) lineMult#(@n,@l1,@l2) = [0 0] @l1 + [0 0] @n + [0] [0 1] [0 1] [0] >= [0] [0] = c_8(lineMult#1#(@l1,@l2,@n)) lineMult#1#(::(@x,@xs),@l2,@n) = [0 0] @n + [0] [1 1] [1] >= [0] [0] = c_9(lineMult#2#(@l2,@n,@x,@xs)) lineMult#2#(::(@y,@ys),@n,@x,@xs) = [0 0] @xs + [0 0] @y + [0 0] @ys + [0] [0 1] [1 1] [1 1] [2] >= [0] [0] = c_11(lineMult#(@n,@xs,@ys)) lineMult#2#(nil(),@n,@x,@xs) = [0 0] @xs + [0] [0 1] [1] >= [0] [0] = c_12(lineMult#(@n,@xs,nil())) matrixMult#(@m1,@m2) = [1 0] @m1 + [0 1] @m2 + [0] [0 0] [1 0] [1] >= [1 0] @m1 + [0 1] @m2 + [0] [0 0] [0 0] [1] = c_13(matrixMult#1#(@m1,@m2)) matrixMult#1#(::(@l,@ls),@m2) = [1 1] @l + [1 1] @ls + [0 1] @m2 + [1] [1 1] [1 1] [0 1] [1] >= [1 1] @l + [1 0] @ls + [0 1] @m2 + [1] [0 0] [1 0] [0 1] [1] = c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2)) ****** Step 6.a:1.b:1.b:1.b:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) - 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)) ,lineMult#(@x,@l,@acc)) 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: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () ****** Step 6.a:1.b:1.b:1.b:1.b:1: PredecessorEstimationCP WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) - 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)) ,lineMult#(@x,@l,@acc)) 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: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) Consider the set of all dependency pairs 1: lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) 2: computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)) 3: computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs)) 4: computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) ,lineMult#(@x,@l,@acc)) 5: lineMult#1#(::(@x,@xs),@l2,@n) -> c_9(lineMult#2#(@l2,@n,@x,@xs)) 6: lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(lineMult#(@n,@xs,@ys)) 7: lineMult#2#(nil(),@n,@x,@xs) -> c_12(lineMult#(@n,@xs,nil())) 8: matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2)) 9: matrixMult#1#(::(@l,@ls),@m2) -> c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2)) Processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^2)) SPACE(?,?)on application of the dependency pairs {1} These cover all (indirect) predecessors of dependency pairs {1,5,6,7} their number of applications is equally bounded. The dependency pairs are shifted into the weak component. ******* Step 6.a:1.b:1.b:1.b:1.b:1.a:1: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) - 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)) ,lineMult#(@x,@l,@acc)) 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: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(c_3) = {1}, uargs(c_4) = {1}, uargs(c_6) = {1,2}, uargs(c_8) = {1}, uargs(c_9) = {1}, uargs(c_11) = {1}, uargs(c_12) = {1}, uargs(c_13) = {1}, uargs(c_14) = {1,2} Following symbols are considered usable: {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine#,computeLine#1#,computeLine#2#,lineMult# ,lineMult#1#,lineMult#2#,matrixMult#,matrixMult#1#} TcT has computed the following interpretation: p(#0) = 0 p(#add) = 1 + x1*x2 p(#mult) = x1^2 p(#natmult) = x2^2 p(#neg) = x1 p(#pos) = 0 p(#pred) = 1 + x1^2 p(#s) = 0 p(#succ) = x1 p(*) = x2^2 p(+) = x1^2 + x2 p(::) = 1 + x1 + x2 p(computeLine) = 0 p(computeLine#1) = 0 p(computeLine#2) = 0 p(lineMult) = 0 p(lineMult#1) = x1^2 + x2 + x3^2 p(lineMult#2) = x1^2 + x2*x3 + x2^2 + x3*x4 + x3^2 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(+#) = 0 p(computeLine#) = 1 + x1 + x2 p(computeLine#1#) = x1 + x3 p(computeLine#2#) = 1 + x1 + x3 + x4 p(lineMult#) = 1 + x1 + x2 p(lineMult#1#) = x1 + x3 p(lineMult#2#) = 1 + x2 + x3 + x4 p(matrixMult#) = 1 + x1 + x1*x2 + x2^2 p(matrixMult#1#) = 1 + x1 + x1*x2 + x2^2 p(c_1) = 0 p(c_2) = 0 p(c_3) = x1 p(c_4) = x1 p(c_5) = 0 p(c_6) = x1 + x2 p(c_7) = 0 p(c_8) = x1 p(c_9) = x1 p(c_10) = 0 p(c_11) = x1 p(c_12) = x1 p(c_13) = x1 p(c_14) = x1 + x2 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: lineMult#(@n,@l1,@l2) = 1 + @l1 + @n > @l1 + @n = c_8(lineMult#1#(@l1,@l2,@n)) Following rules are (at-least) weakly oriented: computeLine#(@line,@m,@acc) = 1 + @line + @m >= @line + @m = c_3(computeLine#1#(@line,@acc,@m)) computeLine#1#(::(@x,@xs),@acc,@m) = 1 + @m + @x + @xs >= 1 + @m + @x + @xs = c_4(computeLine#2#(@m,@acc,@x,@xs)) computeLine#2#(::(@l,@ls),@acc,@x,@xs) = 2 + @l + @ls + @x + @xs >= 2 + @l + @ls + @x + @xs = c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)),lineMult#(@x,@l,@acc)) lineMult#1#(::(@x,@xs),@l2,@n) = 1 + @n + @x + @xs >= 1 + @n + @x + @xs = c_9(lineMult#2#(@l2,@n,@x,@xs)) lineMult#2#(::(@y,@ys),@n,@x,@xs) = 1 + @n + @x + @xs >= 1 + @n + @xs = c_11(lineMult#(@n,@xs,@ys)) lineMult#2#(nil(),@n,@x,@xs) = 1 + @n + @x + @xs >= 1 + @n + @xs = c_12(lineMult#(@n,@xs,nil())) matrixMult#(@m1,@m2) = 1 + @m1 + @m1*@m2 + @m2^2 >= 1 + @m1 + @m1*@m2 + @m2^2 = c_13(matrixMult#1#(@m1,@m2)) matrixMult#1#(::(@l,@ls),@m2) = 2 + @l + @l*@m2 + @ls + @ls*@m2 + @m2 + @m2^2 >= 2 + @l + @ls + @ls*@m2 + @m2 + @m2^2 = c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2)) ******* Step 6.a:1.b:1.b:1.b:1.b:1.a:2: Assumption 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)) ,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: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () ******* Step 6.a:1.b:1.b:1.b:1.b:1.b:1: RemoveWeakSuffixes 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)) ,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: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W: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:W: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:W: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:W: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:W:lineMult#1#(::(@x,@xs),@l2,@n) -> c_9(lineMult#2#(@l2,@n,@x,@xs)) -->_1 lineMult#2#(nil(),@n,@x,@xs) -> c_12(lineMult#(@n,@xs,nil())):7 -->_1 lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(lineMult#(@n,@xs,@ys)):6 6:W:lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(lineMult#(@n,@xs,@ys)) -->_1 lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)):4 7:W:lineMult#2#(nil(),@n,@x,@xs) -> c_12(lineMult#(@n,@xs,nil())) -->_1 lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)):4 8:W: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:W: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 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 8: matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2)) 9: matrixMult#1#(::(@l,@ls),@m2) -> c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2)) 1: computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)) 3: computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) ,lineMult#(@x,@l,@acc)) 2: computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs)) 4: lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) 7: lineMult#2#(nil(),@n,@x,@xs) -> c_12(lineMult#(@n,@xs,nil())) 5: lineMult#1#(::(@x,@xs),@l2,@n) -> c_9(lineMult#2#(@l2,@n,@x,@xs)) 6: lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(lineMult#(@n,@xs,@ys)) ******* Step 6.a:1.b:1.b:1.b:1.b:1.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - 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). ** Step 6.b:1: RemoveWeakSuffixes 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 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 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: RemoveWeakSuffixes + 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)) -->_1 computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)):3 -->_2 matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2)):1 3:W: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)):4 4:W: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)):5 5:W: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)):6 -->_1 computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)):3 6:W: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)):7 7:W:lineMult#1#(::(@x,@xs),@l2,@n) -> c_9(lineMult#2#(@l2,@n,@x,@xs)) -->_1 lineMult#2#(nil(),@n,@x,@xs) -> c_12(lineMult#(@n,@xs,nil())):9 -->_1 lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(lineMult#(@n,@xs,@ys)):8 8:W:lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(lineMult#(@n,@xs,@ys)) -->_1 lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)):6 9:W:lineMult#2#(nil(),@n,@x,@xs) -> c_12(lineMult#(@n,@xs,nil())) -->_1 lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)):6 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 3: computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)) 5: computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)) ,lineMult#(@x,@l,@acc)) 4: computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs)) 6: lineMult#(@n,@l1,@l2) -> c_8(lineMult#1#(@l1,@l2,@n)) 9: lineMult#2#(nil(),@n,@x,@xs) -> c_12(lineMult#(@n,@xs,nil())) 7: lineMult#1#(::(@x,@xs),@l2,@n) -> c_9(lineMult#2#(@l2,@n,@x,@xs)) 8: lineMult#2#(::(@y,@ys),@n,@x,@xs) -> c_11(lineMult#(@n,@xs,@ys)) ** Step 6.b:2: 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.b:3: 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.b:4: PredecessorEstimationCP 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: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 2: matrixMult#1#(::(@l,@ls),@m2) -> c_14(matrixMult#(@ls,@m2)) Consider the set of all dependency pairs 1: matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2)) 2: matrixMult#1#(::(@l,@ls),@m2) -> c_14(matrixMult#(@ls,@m2)) Processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^1)) SPACE(?,?)on application of the dependency pairs {2} These cover all (indirect) predecessors of dependency pairs {1,2} their number of applications is equally bounded. The dependency pairs are shifted into the weak component. *** Step 6.b:4.a:1: NaturalMI 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: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_13) = {1}, uargs(c_14) = {1} Following symbols are considered usable: {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine#,computeLine#1#,computeLine#2#,lineMult# ,lineMult#1#,lineMult#2#,matrixMult#,matrixMult#1#} TcT has computed the following interpretation: p(#0) = [0] p(#add) = [8] p(#mult) = [8] x1 + [0] p(#natmult) = [1] p(#neg) = [0] p(#pos) = [2] p(#pred) = [2] p(#s) = [1] x1 + [1] p(#succ) = [0] p(*) = [0] p(+) = [0] p(::) = [1] x2 + [8] p(computeLine) = [1] x3 + [8] p(computeLine#1) = [1] x1 + [1] x2 + [1] p(computeLine#2) = [1] x1 + [2] x2 + [4] x3 + [1] 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(+#) = [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 + [3] 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 + [3] p(c_14) = [1] x1 + [3] p(c_15) = [0] p(c_16) = [1] p(c_17) = [2] x1 + [1] p(c_18) = [1] x1 + [1] x2 + [0] p(c_19) = [1] p(c_20) = [1] x1 + [1] x2 + [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [1] p(c_24) = [0] p(c_25) = [2] x1 + [1] p(c_26) = [1] p(c_27) = [1] p(c_28) = [0] p(c_29) = [1] x1 + [0] p(c_30) = [1] p(c_31) = [0] p(c_32) = [0] p(c_33) = [2] p(c_34) = [0] p(c_35) = [1] p(c_36) = [1] p(c_37) = [0] p(c_38) = [2] p(c_39) = [8] Following rules are strictly oriented: matrixMult#1#(::(@l,@ls),@m2) = [1] @ls + [8] > [1] @ls + [6] = c_14(matrixMult#(@ls,@m2)) Following rules are (at-least) weakly oriented: matrixMult#(@m1,@m2) = [1] @m1 + [3] >= [1] @m1 + [3] = c_13(matrixMult#1#(@m1,@m2)) *** Step 6.b:4.a:2: Assumption WORST_CASE(?,O(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: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () *** Step 6.b:4.b:1: RemoveWeakSuffixes 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: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2)) -->_1 matrixMult#1#(::(@l,@ls),@m2) -> c_14(matrixMult#(@ls,@m2)):2 2:W:matrixMult#1#(::(@l,@ls),@m2) -> c_14(matrixMult#(@ls,@m2)) -->_1 matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2)) 2: matrixMult#1#(::(@l,@ls),@m2) -> c_14(matrixMult#(@ls,@m2)) *** Step 6.b:4.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - 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). WORST_CASE(?,O(n^2))