* Step 1: Sum 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:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: 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 3: 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 4: 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 5: 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 6: 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 7: 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 7.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 7.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 7.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 7.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 7.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 7.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 7.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 = 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:
          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 = 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
          {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 7.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 = 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) = [1]                                 
                              [0]                                 
                    p(#add) = [0 1] x2 + [0]                      
                              [0 0]      [0]                      
                   p(#mult) = [1 0] x1 + [0 0] x2 + [0]           
                              [0 1]      [1 0]      [1]           
                p(#natmult) = [0 1] x1 + [1]                      
                              [1 0]      [0]                      
                    p(#neg) = [0]                                 
                              [0]                                 
                    p(#pos) = [0 0] x1 + [1]                      
                              [0 1]      [1]                      
                   p(#pred) = [1 0] x1 + [1]                      
                              [1 0]      [1]                      
                      p(#s) = [0 1] x1 + [0]                      
                              [0 0]      [1]                      
                   p(#succ) = [1 0] x1 + [0]                      
                              [0 0]      [1]                      
                       p(*) = [0]                                 
                              [0]                                 
                       p(+) = [0]                                 
                              [1]                                 
                      p(::) = [0 0] x1 + [0 0] x2 + [0]           
                              [0 1]      [0 1]      [1]           
             p(computeLine) = [0]                                 
                              [0]                                 
           p(computeLine#1) = [0]                                 
                              [0]                                 
           p(computeLine#2) = [0]                                 
                              [0]                                 
                p(lineMult) = [0 0] x3 + [0]                      
                              [1 0]      [1]                      
              p(lineMult#1) = [0]                                 
                              [0]                                 
              p(lineMult#2) = [1 0] x1 + [1]                      
                              [0 0]      [0]                      
              p(matrixMult) = [0]                                 
                              [0]                                 
            p(matrixMult#1) = [0]                                 
                              [0]                                 
                     p(nil) = [1]                                 
                              [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#) = [0 1] x1 + [0 0] x2 + [0]           
                              [0 1]      [0 1]      [1]           
          p(computeLine#1#) = [0 1] x1 + [0]                      
                              [0 0]      [0]                      
          p(computeLine#2#) = [0 0] x2 + [0 1] x3 + [0 1] x4 + [0]
                              [0 1]      [1 1]      [1 1]      [0]
               p(lineMult#) = [0 0] x3 + [0]                      
                              [0 1]      [0]                      
             p(lineMult#1#) = [0]                                 
                              [1]                                 
             p(lineMult#2#) = [0 0] x1 + [0 0] x2 + [0]           
                              [1 1]      [0 1]      [0]           
             p(matrixMult#) = [0 1] x1 + [0 1] x2 + [0]           
                              [0 1]      [0 1]      [0]           
           p(matrixMult#1#) = [0 1] x1 + [0 1] x2 + [0]           
                              [0 0]      [1 1]      [1]           
                     p(c_1) = [0]                                 
                              [0]                                 
                     p(c_2) = [0]                                 
                              [0]                                 
                     p(c_3) = [1 0] x1 + [0]                      
                              [1 0]      [0]                      
                     p(c_4) = [1 0] x1 + [0]                      
                              [0 0]      [0]                      
                     p(c_5) = [0]                                 
                              [0]                                 
                     p(c_6) = [1 0] x1 + [1 0] x2 + [0]           
                              [1 0]      [0 1]      [0]           
                     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 1]      [1]                      
                    p(c_12) = [1 0] x1 + [0]                      
                              [0 0]      [0]                      
                    p(c_13) = [1 0] x1 + [0]                      
                              [0 0]      [0]                      
                    p(c_14) = [1 0] x1 + [1 0] x2 + [1]           
                              [0 0]      [0 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#1#(::(@x,@xs),@acc,@m) = [0 1] @x + [0 1] @xs + [1]         
                                             [0 0]      [0 0]       [0]         
                                           > [0 1] @x + [0 1] @xs + [0]         
                                             [0 0]      [0 0]       [0]         
                                           = c_4(computeLine#2#(@m,@acc,@x,@xs))
        
        
        Following rules are (at-least) weakly oriented:
                   computeLine#(@line,@m,@acc) =  [0 1] @line + [0 0] @m + [0]                                         
                                                  [0 1]         [0 1]      [1]                                         
                                               >= [0 1] @line + [0]                                                    
                                                  [0 1]         [0]                                                    
                                               =  c_3(computeLine#1#(@line,@acc,@m))                                   
        
        computeLine#2#(::(@l,@ls),@acc,@x,@xs) =  [0 0] @acc + [0 1] @x + [0 1] @xs + [0]                              
                                                  [0 1]        [1 1]      [1 1]       [0]                              
                                               >= [0 0] @acc + [0 1] @xs + [0]                                         
                                                  [0 1]        [0 1]       [0]                                         
                                               =  c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)),lineMult#(@x,@l,@acc))
        
                         lineMult#(@n,@l1,@l2) =  [0 0] @l2 + [0]                                                      
                                                  [0 1]       [0]                                                      
                                               >= [0]                                                                  
                                                  [0]                                                                  
                                               =  c_8(lineMult#1#(@l1,@l2,@n))                                         
        
                lineMult#1#(::(@x,@xs),@l2,@n) =  [0]                                                                  
                                                  [1]                                                                  
                                               >= [0]                                                                  
                                                  [0]                                                                  
                                               =  c_9(lineMult#2#(@l2,@n,@x,@xs))                                      
        
             lineMult#2#(::(@y,@ys),@n,@x,@xs) =  [0 0] @n + [0 0] @y + [0 0] @ys + [0]                                
                                                  [0 1]      [0 1]      [0 1]       [1]                                
                                               >= [0 0] @ys + [0]                                                      
                                                  [0 1]       [1]                                                      
                                               =  c_11(lineMult#(@n,@xs,@ys))                                          
        
                  lineMult#2#(nil(),@n,@x,@xs) =  [0 0] @n + [0]                                                       
                                                  [0 1]      [1]                                                       
                                               >= [0]                                                                  
                                                  [0]                                                                  
                                               =  c_12(lineMult#(@n,@xs,nil()))                                        
        
                          matrixMult#(@m1,@m2) =  [0 1] @m1 + [0 1] @m2 + [0]                                          
                                                  [0 1]       [0 1]       [0]                                          
                                               >= [0 1] @m1 + [0 1] @m2 + [0]                                          
                                                  [0 0]       [0 0]       [0]                                          
                                               =  c_13(matrixMult#1#(@m1,@m2))                                         
        
                 matrixMult#1#(::(@l,@ls),@m2) =  [0 1] @l + [0 1] @ls + [0 1] @m2 + [1]                               
                                                  [0 0]      [0 0]       [1 1]       [1]                               
                                               >= [0 1] @l + [0 1] @ls + [0 1] @m2 + [1]                               
                                                  [0 0]      [0 0]       [0 0]       [1]                               
                                               =  c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2))                
        
***** Step 7.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 7.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 7.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 7.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 7.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 7.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 7.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 7.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 7.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 7.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 7.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 7.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 7.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 7.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 7.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 7.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 7.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))