* 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))