*** 1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
*(@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 DP Rules:
Weak TRS 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)))
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
basic terms: {#add,#mult,#natmult,#pred,#succ,*,+,computeLine,computeLine#1,computeLine#2,lineMult,lineMult#1,lineMult#2,matrixMult,matrixMult#1}/{#0,#neg,#pos,#s,::,nil}
Applied Processor:
DependencyPairs {dpKind_ = DT}
Proof:
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.
*** 1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
*#(@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()
Strict TRS Rules:
Weak DP Rules:
#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 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)
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
basic terms: {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine#,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult#,matrixMult#1#}/{#0,#neg,#pos,#s,::,nil}
Applied Processor:
UsableRules
Proof:
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()
*** 1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
*#(@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()
Strict TRS Rules:
Weak DP Rules:
#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 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()))
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
basic terms: {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine#,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult#,matrixMult#1#}/{#0,#neg,#pos,#s,::,nil}
Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
Proof:
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()
*** 1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
#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 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()))
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
basic terms: {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine#,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult#,matrixMult#1#}/{#0,#neg,#pos,#s,::,nil}
Applied Processor:
RemoveWeakSuffixes
Proof:
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()
*** 1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
Weak TRS 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()))
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
basic terms: {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine#,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult#,matrixMult#1#}/{#0,#neg,#pos,#s,::,nil}
Applied Processor:
SimplifyRHS
Proof:
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()))
*** 1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
Weak TRS 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()))
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
basic terms: {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine#,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult#,matrixMult#1#}/{#0,#neg,#pos,#s,::,nil}
Applied Processor:
Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
Proof:
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 DP Rules:
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()))
Strict TRS Rules:
Weak DP Rules:
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 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()))
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
basic terms: {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine#,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult#,matrixMult#1#}/{#0,#neg,#pos,#s,::,nil}
Problem (S)
Strict DP Rules:
matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2))
matrixMult#1#(::(@l,@ls),@m2) -> c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2))
Strict TRS Rules:
Weak DP Rules:
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 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()))
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
basic terms: {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine#,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult#,matrixMult#1#}/{#0,#neg,#pos,#s,::,nil}
*** 1.1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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()))
Strict TRS Rules:
Weak DP Rules:
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 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()))
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
basic terms: {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine#,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult#,matrixMult#1#}/{#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, greedy = NoGreedy}}
Proof:
We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
2: computeLine#1#(::(@x,@xs)
,@acc
,@m) -> c_4(computeLine#2#(@m
,@acc
,@x
,@xs))
5: 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: computeLine#2#(::(@l,@ls)
,@acc
,@x
,@xs) -> c_6(computeLine#(@xs
,@ls
,lineMult(@x,@l,@acc))
,lineMult#(@x,@l,@acc))
4: lineMult#(@n,@l1,@l2) ->
c_8(lineMult#1#(@l1,@l2,@n))
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, greedy = NoGreedy}induces the complexity certificateTIME (?,O(n^2))
SPACE(?,?)on application of the dependency pairs
{2,5}
These cover all (indirect) predecessors of dependency pairs
{2,3,4,5,6,7}
their number of applications is equally bounded.
The dependency pairs are shifted into the weak component.
*** 1.1.1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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()))
Strict TRS Rules:
Weak DP Rules:
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 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()))
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
basic terms: {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine#,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult#,matrixMult#1#}/{#0,#neg,#pos,#s,::,nil}
Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
Proof:
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) = 0
p(#mult) = 0
p(#natmult) = x2
p(#neg) = 0
p(#pos) = 0
p(#pred) = 0
p(#s) = 0
p(#succ) = 0
p(*) = 1
p(+) = 1 + x2^2
p(::) = 1 + x1 + x2
p(computeLine) = 0
p(computeLine#1) = 0
p(computeLine#2) = 0
p(lineMult) = x2
p(lineMult#1) = 0
p(lineMult#2) = x3
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#) = 1 + x1 + x3
p(computeLine#2#) = x1 + x4
p(lineMult#) = x2
p(lineMult#1#) = x1
p(lineMult#2#) = x3 + x4
p(matrixMult#) = x1 + x1*x2 + x2^2
p(matrixMult#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:
computeLine#1#(::(@x,@xs) = 2 + @m + @x + @xs
,@acc
,@m)
> @m + @xs
= c_4(computeLine#2#(@m
,@acc
,@x
,@xs))
lineMult#1#(::(@x,@xs),@l2,@n) = 1 + @x + @xs
> @x + @xs
= c_9(lineMult#2#(@l2,@n,@x,@xs))
Following rules are (at-least) weakly oriented:
computeLine#(@line,@m,@acc) = 1 + @line + @m
>= 1 + @line + @m
= c_3(computeLine#1#(@line
,@acc
,@m))
computeLine#2#(::(@l,@ls) = 1 + @l + @ls + @xs
,@acc
,@x
,@xs)
>= 1 + @l + @ls + @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) = @x + @xs
,@n
,@x
,@xs)
>= @xs
= c_11(lineMult#(@n,@xs,@ys))
lineMult#2#(nil(),@n,@x,@xs) = @x + @xs
>= @xs
= c_12(lineMult#(@n,@xs,nil()))
matrixMult#(@m1,@m2) = @m1 + @m1*@m2 + @m2^2
>= @m1 + @m1*@m2 + @m2^2
= c_13(matrixMult#1#(@m1,@m2))
matrixMult#1#(::(@l,@ls),@m2) = 1 + @l + @l*@m2 + @ls + @ls*@m2 + @m2 + @m2^2
>= 1 + @l + @ls + @ls*@m2 + @m2 + @m2^2
= c_14(computeLine#(@l,@m2,nil())
,matrixMult#(@ls,@m2))
*** 1.1.1.1.1.1.1.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m))
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#2#(::(@y,@ys),@n,@x,@xs) -> c_11(lineMult#(@n,@xs,@ys))
lineMult#2#(nil(),@n,@x,@xs) -> c_12(lineMult#(@n,@xs,nil()))
Strict TRS Rules:
Weak DP Rules:
computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs))
lineMult#1#(::(@x,@xs),@l2,@n) -> c_9(lineMult#2#(@l2,@n,@x,@xs))
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 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()))
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
basic terms: {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine#,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult#,matrixMult#1#}/{#0,#neg,#pos,#s,::,nil}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.1.1.2 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m))
Strict TRS Rules:
Weak DP Rules:
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 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()))
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
basic terms: {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine#,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult#,matrixMult#1#}/{#0,#neg,#pos,#s,::,nil}
Applied Processor:
RemoveWeakSuffixes
Proof:
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: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.
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))
*** 1.1.1.1.1.1.1.2.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m))
Strict TRS Rules:
Weak DP Rules:
computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs))
computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)),lineMult#(@x,@l,@acc))
matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2))
matrixMult#1#(::(@l,@ls),@m2) -> c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2))
Weak TRS 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()))
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
basic terms: {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine#,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult#,matrixMult#1#}/{#0,#neg,#pos,#s,::,nil}
Applied Processor:
SimplifyRHS
Proof:
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: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))
-->_1 computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)):1
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
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)))
*** 1.1.1.1.1.1.1.2.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m))
Strict TRS Rules:
Weak DP Rules:
computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs))
computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)))
matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2))
matrixMult#1#(::(@l,@ls),@m2) -> c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2))
Weak TRS 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()))
Signature:
{#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,+/2,computeLine/3,computeLine#1/3,computeLine#2/4,lineMult/3,lineMult#1/3,lineMult#2/4,matrixMult/2,matrixMult#1/2,#add#/2,#mult#/2,#natmult#/2,#pred#/1,#succ#/1,*#/2,+#/2,computeLine#/3,computeLine#1#/3,computeLine#2#/4,lineMult#/3,lineMult#1#/3,lineMult#2#/4,matrixMult#/2,matrixMult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/1,c_13/1,c_14/2,c_15/0,c_16/0,c_17/1,c_18/2,c_19/1,c_20/2,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/0,c_28/1,c_29/1,c_30/0,c_31/2,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0}
Obligation:
Innermost
basic terms: {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine#,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult#,matrixMult#1#}/{#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, greedy = NoGreedy}}
Proof:
We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} 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: computeLine#1#(::(@x,@xs)
,@acc
,@m) -> c_4(computeLine#2#(@m
,@acc
,@x
,@xs))
3: computeLine#2#(::(@l,@ls)
,@acc
,@x
,@xs) -> c_6(computeLine#(@xs
,@ls
,lineMult(@x,@l,@acc)))
4: matrixMult#(@m1,@m2) ->
c_13(matrixMult#1#(@m1,@m2))
5: matrixMult#1#(::(@l,@ls),@m2) ->
c_14(computeLine#(@l,@m2,nil())
,matrixMult#(@ls,@m2))
Processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}induces the complexity certificateTIME (?,O(n^1))
SPACE(?,?)on application of the dependency pairs
{1}
These cover all (indirect) predecessors of dependency pairs
{1,2,3}
their number of applications is equally bounded.
The dependency pairs are shifted into the weak component.
*** 1.1.1.1.1.1.1.2.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m))
Strict TRS Rules:
Weak DP Rules:
computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs))
computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)))
matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2))
matrixMult#1#(::(@l,@ls),@m2) -> c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2))
Weak TRS 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()))
Signature:
{#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,+/2,computeLine/3,computeLine#1/3,computeLine#2/4,lineMult/3,lineMult#1/3,lineMult#2/4,matrixMult/2,matrixMult#1/2,#add#/2,#mult#/2,#natmult#/2,#pred#/1,#succ#/1,*#/2,+#/2,computeLine#/3,computeLine#1#/3,computeLine#2#/4,lineMult#/3,lineMult#1#/3,lineMult#2#/4,matrixMult#/2,matrixMult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/1,c_13/1,c_14/2,c_15/0,c_16/0,c_17/1,c_18/2,c_19/1,c_20/2,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/0,c_28/1,c_29/1,c_30/0,c_31/2,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0}
Obligation:
Innermost
basic terms: {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine#,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult#,matrixMult#1#}/{#0,#neg,#pos,#s,::,nil}
Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
Proof:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_3) = {1},
uargs(c_4) = {1},
uargs(c_6) = {1},
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) = [4] x1 + [3]
p(#mult) = [1] x2 + [5]
p(#natmult) = [4] x2 + [0]
p(#neg) = [0]
p(#pos) = [1]
p(#pred) = [0]
p(#s) = [4]
p(#succ) = [2] x1 + [0]
p(*) = [1] x1 + [1]
p(+) = [7]
p(::) = [1] x1 + [1] x2 + [1]
p(computeLine) = [1] x3 + [1]
p(computeLine#1) = [1] x1 + [4] x3 + [1]
p(computeLine#2) = [1] x4 + [0]
p(lineMult) = [2] x1 + [5] x3 + [0]
p(lineMult#1) = [0]
p(lineMult#2) = [1] x2 + [0]
p(matrixMult) = [1]
p(matrixMult#1) = [1] x1 + [2] x2 + [0]
p(nil) = [1]
p(#add#) = [1] x1 + [0]
p(#mult#) = [0]
p(#natmult#) = [2] x2 + [0]
p(#pred#) = [1]
p(#succ#) = [1]
p(*#) = [1] x1 + [1] x2 + [0]
p(+#) = [0]
p(computeLine#) = [4] x1 + [1]
p(computeLine#1#) = [4] x1 + [0]
p(computeLine#2#) = [4] x4 + [1]
p(lineMult#) = [4] x2 + [4]
p(lineMult#1#) = [4] x1 + [4] x3 + [4]
p(lineMult#2#) = [1] x1 + [0]
p(matrixMult#) = [6] x1 + [0]
p(matrixMult#1#) = [6] x1 + [0]
p(c_1) = [4] x1 + [1]
p(c_2) = [4] x1 + [1]
p(c_3) = [1] x1 + [0]
p(c_4) = [1] x1 + [0]
p(c_5) = [1]
p(c_6) = [1] x1 + [0]
p(c_7) = [2]
p(c_8) = [0]
p(c_9) = [2]
p(c_10) = [1]
p(c_11) = [0]
p(c_12) = [0]
p(c_13) = [1] x1 + [0]
p(c_14) = [1] x1 + [1] x2 + [3]
p(c_15) = [0]
p(c_16) = [2]
p(c_17) = [0]
p(c_18) = [0]
p(c_19) = [4] x1 + [1]
p(c_20) = [1]
p(c_21) = [1]
p(c_22) = [0]
p(c_23) = [0]
p(c_24) = [1]
p(c_25) = [1] x1 + [4]
p(c_26) = [1]
p(c_27) = [2]
p(c_28) = [0]
p(c_29) = [1]
p(c_30) = [0]
p(c_31) = [1] x1 + [4] x2 + [0]
p(c_32) = [0]
p(c_33) = [0]
p(c_34) = [1]
p(c_35) = [0]
p(c_36) = [0]
p(c_37) = [0]
p(c_38) = [4]
p(c_39) = [0]
Following rules are strictly oriented:
computeLine#(@line,@m,@acc) = [4] @line + [1]
> [4] @line + [0]
= c_3(computeLine#1#(@line
,@acc
,@m))
Following rules are (at-least) weakly oriented:
computeLine#1#(::(@x,@xs) = [4] @x + [4] @xs + [4]
,@acc
,@m)
>= [4] @xs + [1]
= c_4(computeLine#2#(@m
,@acc
,@x
,@xs))
computeLine#2#(::(@l,@ls) = [4] @xs + [1]
,@acc
,@x
,@xs)
>= [4] @xs + [1]
= c_6(computeLine#(@xs
,@ls
,lineMult(@x,@l,@acc)))
matrixMult#(@m1,@m2) = [6] @m1 + [0]
>= [6] @m1 + [0]
= c_13(matrixMult#1#(@m1,@m2))
matrixMult#1#(::(@l,@ls),@m2) = [6] @l + [6] @ls + [6]
>= [4] @l + [6] @ls + [4]
= c_14(computeLine#(@l,@m2,nil())
,matrixMult#(@ls,@m2))
*** 1.1.1.1.1.1.1.2.1.1.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m))
computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs))
computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)))
matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2))
matrixMult#1#(::(@l,@ls),@m2) -> c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2))
Weak TRS 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()))
Signature:
{#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,+/2,computeLine/3,computeLine#1/3,computeLine#2/4,lineMult/3,lineMult#1/3,lineMult#2/4,matrixMult/2,matrixMult#1/2,#add#/2,#mult#/2,#natmult#/2,#pred#/1,#succ#/1,*#/2,+#/2,computeLine#/3,computeLine#1#/3,computeLine#2#/4,lineMult#/3,lineMult#1#/3,lineMult#2#/4,matrixMult#/2,matrixMult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/1,c_13/1,c_14/2,c_15/0,c_16/0,c_17/1,c_18/2,c_19/1,c_20/2,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/0,c_28/1,c_29/1,c_30/0,c_31/2,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0}
Obligation:
Innermost
basic terms: {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine#,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult#,matrixMult#1#}/{#0,#neg,#pos,#s,::,nil}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.1.1.2.1.1.2 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m))
computeLine#1#(::(@x,@xs),@acc,@m) -> c_4(computeLine#2#(@m,@acc,@x,@xs))
computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)))
matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2))
matrixMult#1#(::(@l,@ls),@m2) -> c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2))
Weak TRS 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()))
Signature:
{#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,+/2,computeLine/3,computeLine#1/3,computeLine#2/4,lineMult/3,lineMult#1/3,lineMult#2/4,matrixMult/2,matrixMult#1/2,#add#/2,#mult#/2,#natmult#/2,#pred#/1,#succ#/1,*#/2,+#/2,computeLine#/3,computeLine#1#/3,computeLine#2#/4,lineMult#/3,lineMult#1#/3,lineMult#2#/4,matrixMult#/2,matrixMult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/1,c_13/1,c_14/2,c_15/0,c_16/0,c_17/1,c_18/2,c_19/1,c_20/2,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/0,c_28/1,c_29/1,c_30/0,c_31/2,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0}
Obligation:
Innermost
basic terms: {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine#,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult#,matrixMult#1#}/{#0,#neg,#pos,#s,::,nil}
Applied Processor:
RemoveWeakSuffixes
Proof:
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))):3
3:W:computeLine#2#(::(@l,@ls),@acc,@x,@xs) -> c_6(computeLine#(@xs,@ls,lineMult(@x,@l,@acc)))
-->_1 computeLine#(@line,@m,@acc) -> c_3(computeLine#1#(@line,@acc,@m)):1
4: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)):5
5: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)):4
-->_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.
4: matrixMult#(@m1,@m2) ->
c_13(matrixMult#1#(@m1,@m2))
5: 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)))
2: computeLine#1#(::(@x,@xs)
,@acc
,@m) -> c_4(computeLine#2#(@m
,@acc
,@x
,@xs))
*** 1.1.1.1.1.1.1.2.1.1.2.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS 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()))
Signature:
{#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,+/2,computeLine/3,computeLine#1/3,computeLine#2/4,lineMult/3,lineMult#1/3,lineMult#2/4,matrixMult/2,matrixMult#1/2,#add#/2,#mult#/2,#natmult#/2,#pred#/1,#succ#/1,*#/2,+#/2,computeLine#/3,computeLine#1#/3,computeLine#2#/4,lineMult#/3,lineMult#1#/3,lineMult#2#/4,matrixMult#/2,matrixMult#1#/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/1,c_13/1,c_14/2,c_15/0,c_16/0,c_17/1,c_18/2,c_19/1,c_20/2,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/0,c_28/1,c_29/1,c_30/0,c_31/2,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0}
Obligation:
Innermost
basic terms: {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine#,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult#,matrixMult#1#}/{#0,#neg,#pos,#s,::,nil}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).
*** 1.1.1.1.1.1.2 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2))
matrixMult#1#(::(@l,@ls),@m2) -> c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2))
Strict TRS Rules:
Weak DP Rules:
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 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()))
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
basic terms: {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine#,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult#,matrixMult#1#}/{#0,#neg,#pos,#s,::,nil}
Applied Processor:
RemoveWeakSuffixes
Proof:
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))
*** 1.1.1.1.1.1.2.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2))
matrixMult#1#(::(@l,@ls),@m2) -> c_14(computeLine#(@l,@m2,nil()),matrixMult#(@ls,@m2))
Strict TRS Rules:
Weak DP Rules:
Weak TRS 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()))
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
basic terms: {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine#,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult#,matrixMult#1#}/{#0,#neg,#pos,#s,::,nil}
Applied Processor:
SimplifyRHS
Proof:
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))
*** 1.1.1.1.1.1.2.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2))
matrixMult#1#(::(@l,@ls),@m2) -> c_14(matrixMult#(@ls,@m2))
Strict TRS Rules:
Weak DP Rules:
Weak TRS 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()))
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
basic terms: {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine#,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult#,matrixMult#1#}/{#0,#neg,#pos,#s,::,nil}
Applied Processor:
UsableRules
Proof:
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))
*** 1.1.1.1.1.1.2.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2))
matrixMult#1#(::(@l,@ls),@m2) -> c_14(matrixMult#(@ls,@m2))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
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
basic terms: {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine#,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult#,matrixMult#1#}/{#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, greedy = NoGreedy}}
Proof:
We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} 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, greedy = NoGreedy}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.
*** 1.1.1.1.1.1.2.1.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2))
matrixMult#1#(::(@l,@ls),@m2) -> c_14(matrixMult#(@ls,@m2))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
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
basic terms: {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine#,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult#,matrixMult#1#}/{#0,#neg,#pos,#s,::,nil}
Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
Proof:
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) = [1]
p(#add) = [1]
p(#mult) = [0]
p(#natmult) = [4] x2 + [0]
p(#neg) = [0]
p(#pos) = [2]
p(#pred) = [1] x1 + [2]
p(#s) = [2]
p(#succ) = [0]
p(*) = [1]
p(+) = [1] x1 + [0]
p(::) = [1] x1 + [1] x2 + [7]
p(computeLine) = [4] x1 + [0]
p(computeLine#1) = [0]
p(computeLine#2) = [1] x1 + [1] 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 + [2] x2 + [1]
p(matrixMult#1#) = [1] x1 + [2] x2 + [0]
p(c_1) = [0]
p(c_2) = [0]
p(c_3) = [0]
p(c_4) = [0]
p(c_5) = [0]
p(c_6) = [0]
p(c_7) = [0]
p(c_8) = [0]
p(c_9) = [0]
p(c_10) = [0]
p(c_11) = [1] x1 + [0]
p(c_12) = [0]
p(c_13) = [1] x1 + [1]
p(c_14) = [1] x1 + [2]
p(c_15) = [2]
p(c_16) = [1]
p(c_17) = [1] x1 + [8]
p(c_18) = [1] x1 + [1] x2 + [1]
p(c_19) = [2] x1 + [8]
p(c_20) = [1] x1 + [1] x2 + [1]
p(c_21) = [1]
p(c_22) = [8]
p(c_23) = [1]
p(c_24) = [8]
p(c_25) = [1]
p(c_26) = [1] x1 + [1]
p(c_27) = [0]
p(c_28) = [2]
p(c_29) = [4] x1 + [1]
p(c_30) = [0]
p(c_31) = [2]
p(c_32) = [1]
p(c_33) = [1]
p(c_34) = [2]
p(c_35) = [1]
p(c_36) = [1]
p(c_37) = [2]
p(c_38) = [1]
p(c_39) = [1]
Following rules are strictly oriented:
matrixMult#1#(::(@l,@ls),@m2) = [1] @l + [1] @ls + [2] @m2 + [7]
> [1] @ls + [2] @m2 + [3]
= c_14(matrixMult#(@ls,@m2))
Following rules are (at-least) weakly oriented:
matrixMult#(@m1,@m2) = [1] @m1 + [2] @m2 + [1]
>= [1] @m1 + [2] @m2 + [1]
= c_13(matrixMult#1#(@m1,@m2))
*** 1.1.1.1.1.1.2.1.1.1.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2))
Strict TRS Rules:
Weak DP Rules:
matrixMult#1#(::(@l,@ls),@m2) -> c_14(matrixMult#(@ls,@m2))
Weak TRS Rules:
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
basic terms: {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine#,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult#,matrixMult#1#}/{#0,#neg,#pos,#s,::,nil}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.1.2.1.1.1.2 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
matrixMult#(@m1,@m2) -> c_13(matrixMult#1#(@m1,@m2))
matrixMult#1#(::(@l,@ls),@m2) -> c_14(matrixMult#(@ls,@m2))
Weak TRS Rules:
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
basic terms: {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine#,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult#,matrixMult#1#}/{#0,#neg,#pos,#s,::,nil}
Applied Processor:
RemoveWeakSuffixes
Proof:
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))
*** 1.1.1.1.1.1.2.1.1.1.2.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
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
basic terms: {#add#,#mult#,#natmult#,#pred#,#succ#,*#,+#,computeLine#,computeLine#1#,computeLine#2#,lineMult#,lineMult#1#,lineMult#2#,matrixMult#,matrixMult#1#}/{#0,#neg,#pos,#s,::,nil}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).