We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict Trs:
{ bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) ->
dequeue(@dequeue@1, @dequeue@2)
, reverse(@xs) -> appendreverse(@xs, nil())
, bftMult'#5(@queue', @acc, @y) ->
bftMult'(@queue', matrixMult(@acc, @y))
, appendreverse#1(nil(), @sofar) -> @sofar
, appendreverse#1(::(@a, @as), @sofar) ->
appendreverse(@as, ::(@a, @sofar))
, computeLine#1(nil(), @acc, @m) -> @acc
, computeLine#1(::(@x, @xs), @acc, @m) ->
computeLine#2(@m, @acc, @x, @xs)
, bftMult'#3(nil(), @acc, @queue) -> @acc
, bftMult'#3(::(@t, @_@3), @acc, @queue) ->
bftMult'#4(@t, @acc, @queue)
, appendreverse(@toreverse, @sofar) ->
appendreverse#1(@toreverse, @sofar)
, matrixMult#1(nil(), @m2) -> nil()
, matrixMult#1(::(@l, @ls), @m2) ->
::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))
, bftMult(@t, @acc) ->
bftMult'(tuple#2(::(@t, nil()), nil()), @acc)
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, dequeue(@outq, @inq) -> dequeue#1(@outq, @inq)
, bftMult'#1(tuple#2(@elem, @queue), @acc) ->
bftMult'#3(@elem, @acc, @queue)
, bftMult'(@queue, @acc) -> bftMult'#1(bftMult'#2(@queue), @acc)
, computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m)
, bftMult'#4(leaf(), @acc, @queue) -> bftMult'(@queue, @acc)
, bftMult'#4(node(@y, @t1, @t2), @acc, @queue) ->
bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)
, dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq))
, dequeue#1(::(@t, @ts), @inq) ->
tuple#2(::(@t, nil()), tuple#2(@ts, @inq))
, +(@x, @y) -> #add(@x, @y)
, enqueue#1(tuple#2(@outq, @inq), @t) ->
tuple#2(@outq, ::(@t, @inq))
, matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2)
, *(@x, @y) -> #mult(@x, @y)
, enqueue(@t, @queue) -> enqueue#1(@queue, @t)
, dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil()))
, dequeue#2(::(@t, @ts)) ->
tuple#2(::(@t, nil()), tuple#2(@ts, nil()))
, lineMult#1(nil(), @l2, @n) -> nil()
, lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, computeLine#2(nil(), @acc, @x, @xs) -> nil()
, computeLine#2(::(@l, @ls), @acc, @x, @xs) ->
computeLine(@xs, @ls, lineMult(@x, @l, @acc)) }
Weak Trs:
{ #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
We add the following dependency tuples:
Strict DPs:
{ bftMult'#2^#(tuple#2(@dequeue@1, @dequeue@2)) ->
c_1(dequeue^#(@dequeue@1, @dequeue@2))
, dequeue^#(@outq, @inq) -> c_17(dequeue#1^#(@outq, @inq))
, reverse^#(@xs) -> c_2(appendreverse^#(@xs, nil()))
, appendreverse^#(@toreverse, @sofar) ->
c_10(appendreverse#1^#(@toreverse, @sofar))
, bftMult'#5^#(@queue', @acc, @y) ->
c_3(bftMult'^#(@queue', matrixMult(@acc, @y)),
matrixMult^#(@acc, @y))
, bftMult'^#(@queue, @acc) ->
c_19(bftMult'#1^#(bftMult'#2(@queue), @acc), bftMult'#2^#(@queue))
, matrixMult^#(@m1, @m2) -> c_27(matrixMult#1^#(@m1, @m2))
, appendreverse#1^#(nil(), @sofar) -> c_4()
, appendreverse#1^#(::(@a, @as), @sofar) ->
c_5(appendreverse^#(@as, ::(@a, @sofar)))
, computeLine#1^#(nil(), @acc, @m) -> c_6()
, computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_7(computeLine#2^#(@m, @acc, @x, @xs))
, computeLine#2^#(nil(), @acc, @x, @xs) -> c_34()
, computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_35(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, bftMult'#3^#(nil(), @acc, @queue) -> c_8()
, bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
c_9(bftMult'#4^#(@t, @acc, @queue))
, bftMult'#4^#(leaf(), @acc, @queue) ->
c_21(bftMult'^#(@queue, @acc))
, bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
c_22(bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y),
enqueue^#(@t2, enqueue(@t1, @queue)),
enqueue^#(@t1, @queue))
, matrixMult#1^#(nil(), @m2) -> c_11()
, matrixMult#1^#(::(@l, @ls), @m2) ->
c_12(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, computeLine^#(@line, @m, @acc) ->
c_20(computeLine#1^#(@line, @acc, @m))
, bftMult^#(@t, @acc) ->
c_13(bftMult'^#(tuple#2(::(@t, nil()), nil()), @acc))
, lineMult^#(@n, @l1, @l2) -> c_14(lineMult#1^#(@l1, @l2, @n))
, lineMult#1^#(nil(), @l2, @n) -> c_32()
, lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_33(lineMult#2^#(@l2, @n, @x, @xs))
, lineMult#2^#(nil(), @n, @x, @xs) ->
c_15(*^#(@x, @n), lineMult^#(@n, @xs, nil()))
, lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_16(+^#(*(@x, @n), @y), *^#(@x, @n), lineMult^#(@n, @xs, @ys))
, *^#(@x, @y) -> c_28(#mult^#(@x, @y))
, +^#(@x, @y) -> c_25(#add^#(@x, @y))
, dequeue#1^#(nil(), @inq) ->
c_23(dequeue#2^#(reverse(@inq)), reverse^#(@inq))
, dequeue#1^#(::(@t, @ts), @inq) -> c_24()
, bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
c_18(bftMult'#3^#(@elem, @acc, @queue))
, enqueue^#(@t, @queue) -> c_29(enqueue#1^#(@queue, @t))
, dequeue#2^#(nil()) -> c_30()
, dequeue#2^#(::(@t, @ts)) -> c_31()
, enqueue#1^#(tuple#2(@outq, @inq), @t) -> c_26() }
Weak DPs:
{ #add^#(#pos(#s(#0())), @y) -> c_38(#succ^#(@y))
, #add^#(#pos(#s(#s(@x))), @y) ->
c_39(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, #add^#(#0(), @y) -> c_40()
, #add^#(#neg(#s(#0())), @y) -> c_41(#pred^#(@y))
, #add^#(#neg(#s(#s(@x))), @y) ->
c_42(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, #mult^#(#pos(@x), #pos(@y)) -> c_43(#natmult^#(@x, @y))
, #mult^#(#pos(@x), #0()) -> c_44()
, #mult^#(#pos(@x), #neg(@y)) -> c_45(#natmult^#(@x, @y))
, #mult^#(#0(), #pos(@y)) -> c_46()
, #mult^#(#0(), #0()) -> c_47()
, #mult^#(#0(), #neg(@y)) -> c_48()
, #mult^#(#neg(@x), #pos(@y)) -> c_49(#natmult^#(@x, @y))
, #mult^#(#neg(@x), #0()) -> c_50()
, #mult^#(#neg(@x), #neg(@y)) -> c_51(#natmult^#(@x, @y))
, #natmult^#(#0(), @y) -> c_36()
, #natmult^#(#s(@x), @y) ->
c_37(#add^#(#pos(@y), #natmult(@x, @y)), #natmult^#(@x, @y))
, #succ^#(#pos(#s(@x))) -> c_52()
, #succ^#(#0()) -> c_53()
, #succ^#(#neg(#s(#0()))) -> c_54()
, #succ^#(#neg(#s(#s(@x)))) -> c_55()
, #pred^#(#pos(#s(#0()))) -> c_56()
, #pred^#(#pos(#s(#s(@x)))) -> c_57()
, #pred^#(#0()) -> c_58()
, #pred^#(#neg(#s(@x))) -> c_59() }
and mark the set of starting terms.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict DPs:
{ bftMult'#2^#(tuple#2(@dequeue@1, @dequeue@2)) ->
c_1(dequeue^#(@dequeue@1, @dequeue@2))
, dequeue^#(@outq, @inq) -> c_17(dequeue#1^#(@outq, @inq))
, reverse^#(@xs) -> c_2(appendreverse^#(@xs, nil()))
, appendreverse^#(@toreverse, @sofar) ->
c_10(appendreverse#1^#(@toreverse, @sofar))
, bftMult'#5^#(@queue', @acc, @y) ->
c_3(bftMult'^#(@queue', matrixMult(@acc, @y)),
matrixMult^#(@acc, @y))
, bftMult'^#(@queue, @acc) ->
c_19(bftMult'#1^#(bftMult'#2(@queue), @acc), bftMult'#2^#(@queue))
, matrixMult^#(@m1, @m2) -> c_27(matrixMult#1^#(@m1, @m2))
, appendreverse#1^#(nil(), @sofar) -> c_4()
, appendreverse#1^#(::(@a, @as), @sofar) ->
c_5(appendreverse^#(@as, ::(@a, @sofar)))
, computeLine#1^#(nil(), @acc, @m) -> c_6()
, computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_7(computeLine#2^#(@m, @acc, @x, @xs))
, computeLine#2^#(nil(), @acc, @x, @xs) -> c_34()
, computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_35(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, bftMult'#3^#(nil(), @acc, @queue) -> c_8()
, bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
c_9(bftMult'#4^#(@t, @acc, @queue))
, bftMult'#4^#(leaf(), @acc, @queue) ->
c_21(bftMult'^#(@queue, @acc))
, bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
c_22(bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y),
enqueue^#(@t2, enqueue(@t1, @queue)),
enqueue^#(@t1, @queue))
, matrixMult#1^#(nil(), @m2) -> c_11()
, matrixMult#1^#(::(@l, @ls), @m2) ->
c_12(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, computeLine^#(@line, @m, @acc) ->
c_20(computeLine#1^#(@line, @acc, @m))
, bftMult^#(@t, @acc) ->
c_13(bftMult'^#(tuple#2(::(@t, nil()), nil()), @acc))
, lineMult^#(@n, @l1, @l2) -> c_14(lineMult#1^#(@l1, @l2, @n))
, lineMult#1^#(nil(), @l2, @n) -> c_32()
, lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_33(lineMult#2^#(@l2, @n, @x, @xs))
, lineMult#2^#(nil(), @n, @x, @xs) ->
c_15(*^#(@x, @n), lineMult^#(@n, @xs, nil()))
, lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_16(+^#(*(@x, @n), @y), *^#(@x, @n), lineMult^#(@n, @xs, @ys))
, *^#(@x, @y) -> c_28(#mult^#(@x, @y))
, +^#(@x, @y) -> c_25(#add^#(@x, @y))
, dequeue#1^#(nil(), @inq) ->
c_23(dequeue#2^#(reverse(@inq)), reverse^#(@inq))
, dequeue#1^#(::(@t, @ts), @inq) -> c_24()
, bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
c_18(bftMult'#3^#(@elem, @acc, @queue))
, enqueue^#(@t, @queue) -> c_29(enqueue#1^#(@queue, @t))
, dequeue#2^#(nil()) -> c_30()
, dequeue#2^#(::(@t, @ts)) -> c_31()
, enqueue#1^#(tuple#2(@outq, @inq), @t) -> c_26() }
Weak DPs:
{ #add^#(#pos(#s(#0())), @y) -> c_38(#succ^#(@y))
, #add^#(#pos(#s(#s(@x))), @y) ->
c_39(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, #add^#(#0(), @y) -> c_40()
, #add^#(#neg(#s(#0())), @y) -> c_41(#pred^#(@y))
, #add^#(#neg(#s(#s(@x))), @y) ->
c_42(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, #mult^#(#pos(@x), #pos(@y)) -> c_43(#natmult^#(@x, @y))
, #mult^#(#pos(@x), #0()) -> c_44()
, #mult^#(#pos(@x), #neg(@y)) -> c_45(#natmult^#(@x, @y))
, #mult^#(#0(), #pos(@y)) -> c_46()
, #mult^#(#0(), #0()) -> c_47()
, #mult^#(#0(), #neg(@y)) -> c_48()
, #mult^#(#neg(@x), #pos(@y)) -> c_49(#natmult^#(@x, @y))
, #mult^#(#neg(@x), #0()) -> c_50()
, #mult^#(#neg(@x), #neg(@y)) -> c_51(#natmult^#(@x, @y))
, #natmult^#(#0(), @y) -> c_36()
, #natmult^#(#s(@x), @y) ->
c_37(#add^#(#pos(@y), #natmult(@x, @y)), #natmult^#(@x, @y))
, #succ^#(#pos(#s(@x))) -> c_52()
, #succ^#(#0()) -> c_53()
, #succ^#(#neg(#s(#0()))) -> c_54()
, #succ^#(#neg(#s(#s(@x)))) -> c_55()
, #pred^#(#pos(#s(#0()))) -> c_56()
, #pred^#(#pos(#s(#s(@x)))) -> c_57()
, #pred^#(#0()) -> c_58()
, #pred^#(#neg(#s(@x))) -> c_59() }
Weak Trs:
{ bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) ->
dequeue(@dequeue@1, @dequeue@2)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
, reverse(@xs) -> appendreverse(@xs, nil())
, bftMult'#5(@queue', @acc, @y) ->
bftMult'(@queue', matrixMult(@acc, @y))
, appendreverse#1(nil(), @sofar) -> @sofar
, appendreverse#1(::(@a, @as), @sofar) ->
appendreverse(@as, ::(@a, @sofar))
, computeLine#1(nil(), @acc, @m) -> @acc
, computeLine#1(::(@x, @xs), @acc, @m) ->
computeLine#2(@m, @acc, @x, @xs)
, bftMult'#3(nil(), @acc, @queue) -> @acc
, bftMult'#3(::(@t, @_@3), @acc, @queue) ->
bftMult'#4(@t, @acc, @queue)
, appendreverse(@toreverse, @sofar) ->
appendreverse#1(@toreverse, @sofar)
, matrixMult#1(nil(), @m2) -> nil()
, matrixMult#1(::(@l, @ls), @m2) ->
::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))
, bftMult(@t, @acc) ->
bftMult'(tuple#2(::(@t, nil()), nil()), @acc)
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, dequeue(@outq, @inq) -> dequeue#1(@outq, @inq)
, bftMult'#1(tuple#2(@elem, @queue), @acc) ->
bftMult'#3(@elem, @acc, @queue)
, bftMult'(@queue, @acc) -> bftMult'#1(bftMult'#2(@queue), @acc)
, computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m)
, bftMult'#4(leaf(), @acc, @queue) -> bftMult'(@queue, @acc)
, bftMult'#4(node(@y, @t1, @t2), @acc, @queue) ->
bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)
, dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq))
, dequeue#1(::(@t, @ts), @inq) ->
tuple#2(::(@t, nil()), tuple#2(@ts, @inq))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, +(@x, @y) -> #add(@x, @y)
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, enqueue#1(tuple#2(@outq, @inq), @t) ->
tuple#2(@outq, ::(@t, @inq))
, matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2)
, *(@x, @y) -> #mult(@x, @y)
, enqueue(@t, @queue) -> enqueue#1(@queue, @t)
, dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil()))
, dequeue#2(::(@t, @ts)) ->
tuple#2(::(@t, nil()), tuple#2(@ts, nil()))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, lineMult#1(nil(), @l2, @n) -> nil()
, lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, computeLine#2(nil(), @acc, @x, @xs) -> nil()
, computeLine#2(::(@l, @ls), @acc, @x, @xs) ->
computeLine(@xs, @ls, lineMult(@x, @l, @acc)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
We estimate the number of application of
{8,10,12,14,18,23,27,28,30,33,34,35} by applications of
Pre({8,10,12,14,18,23,27,28,30,33,34,35}) =
{2,4,7,11,20,22,25,26,29,31,32}. Here rules are labeled as follows:
DPs:
{ 1: bftMult'#2^#(tuple#2(@dequeue@1, @dequeue@2)) ->
c_1(dequeue^#(@dequeue@1, @dequeue@2))
, 2: dequeue^#(@outq, @inq) -> c_17(dequeue#1^#(@outq, @inq))
, 3: reverse^#(@xs) -> c_2(appendreverse^#(@xs, nil()))
, 4: appendreverse^#(@toreverse, @sofar) ->
c_10(appendreverse#1^#(@toreverse, @sofar))
, 5: bftMult'#5^#(@queue', @acc, @y) ->
c_3(bftMult'^#(@queue', matrixMult(@acc, @y)),
matrixMult^#(@acc, @y))
, 6: bftMult'^#(@queue, @acc) ->
c_19(bftMult'#1^#(bftMult'#2(@queue), @acc), bftMult'#2^#(@queue))
, 7: matrixMult^#(@m1, @m2) -> c_27(matrixMult#1^#(@m1, @m2))
, 8: appendreverse#1^#(nil(), @sofar) -> c_4()
, 9: appendreverse#1^#(::(@a, @as), @sofar) ->
c_5(appendreverse^#(@as, ::(@a, @sofar)))
, 10: computeLine#1^#(nil(), @acc, @m) -> c_6()
, 11: computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_7(computeLine#2^#(@m, @acc, @x, @xs))
, 12: computeLine#2^#(nil(), @acc, @x, @xs) -> c_34()
, 13: computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_35(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, 14: bftMult'#3^#(nil(), @acc, @queue) -> c_8()
, 15: bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
c_9(bftMult'#4^#(@t, @acc, @queue))
, 16: bftMult'#4^#(leaf(), @acc, @queue) ->
c_21(bftMult'^#(@queue, @acc))
, 17: bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
c_22(bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y),
enqueue^#(@t2, enqueue(@t1, @queue)),
enqueue^#(@t1, @queue))
, 18: matrixMult#1^#(nil(), @m2) -> c_11()
, 19: matrixMult#1^#(::(@l, @ls), @m2) ->
c_12(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, 20: computeLine^#(@line, @m, @acc) ->
c_20(computeLine#1^#(@line, @acc, @m))
, 21: bftMult^#(@t, @acc) ->
c_13(bftMult'^#(tuple#2(::(@t, nil()), nil()), @acc))
, 22: lineMult^#(@n, @l1, @l2) -> c_14(lineMult#1^#(@l1, @l2, @n))
, 23: lineMult#1^#(nil(), @l2, @n) -> c_32()
, 24: lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_33(lineMult#2^#(@l2, @n, @x, @xs))
, 25: lineMult#2^#(nil(), @n, @x, @xs) ->
c_15(*^#(@x, @n), lineMult^#(@n, @xs, nil()))
, 26: lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_16(+^#(*(@x, @n), @y), *^#(@x, @n), lineMult^#(@n, @xs, @ys))
, 27: *^#(@x, @y) -> c_28(#mult^#(@x, @y))
, 28: +^#(@x, @y) -> c_25(#add^#(@x, @y))
, 29: dequeue#1^#(nil(), @inq) ->
c_23(dequeue#2^#(reverse(@inq)), reverse^#(@inq))
, 30: dequeue#1^#(::(@t, @ts), @inq) -> c_24()
, 31: bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
c_18(bftMult'#3^#(@elem, @acc, @queue))
, 32: enqueue^#(@t, @queue) -> c_29(enqueue#1^#(@queue, @t))
, 33: dequeue#2^#(nil()) -> c_30()
, 34: dequeue#2^#(::(@t, @ts)) -> c_31()
, 35: enqueue#1^#(tuple#2(@outq, @inq), @t) -> c_26()
, 36: #add^#(#pos(#s(#0())), @y) -> c_38(#succ^#(@y))
, 37: #add^#(#pos(#s(#s(@x))), @y) ->
c_39(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, 38: #add^#(#0(), @y) -> c_40()
, 39: #add^#(#neg(#s(#0())), @y) -> c_41(#pred^#(@y))
, 40: #add^#(#neg(#s(#s(@x))), @y) ->
c_42(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, 41: #mult^#(#pos(@x), #pos(@y)) -> c_43(#natmult^#(@x, @y))
, 42: #mult^#(#pos(@x), #0()) -> c_44()
, 43: #mult^#(#pos(@x), #neg(@y)) -> c_45(#natmult^#(@x, @y))
, 44: #mult^#(#0(), #pos(@y)) -> c_46()
, 45: #mult^#(#0(), #0()) -> c_47()
, 46: #mult^#(#0(), #neg(@y)) -> c_48()
, 47: #mult^#(#neg(@x), #pos(@y)) -> c_49(#natmult^#(@x, @y))
, 48: #mult^#(#neg(@x), #0()) -> c_50()
, 49: #mult^#(#neg(@x), #neg(@y)) -> c_51(#natmult^#(@x, @y))
, 50: #natmult^#(#0(), @y) -> c_36()
, 51: #natmult^#(#s(@x), @y) ->
c_37(#add^#(#pos(@y), #natmult(@x, @y)), #natmult^#(@x, @y))
, 52: #succ^#(#pos(#s(@x))) -> c_52()
, 53: #succ^#(#0()) -> c_53()
, 54: #succ^#(#neg(#s(#0()))) -> c_54()
, 55: #succ^#(#neg(#s(#s(@x)))) -> c_55()
, 56: #pred^#(#pos(#s(#0()))) -> c_56()
, 57: #pred^#(#pos(#s(#s(@x)))) -> c_57()
, 58: #pred^#(#0()) -> c_58()
, 59: #pred^#(#neg(#s(@x))) -> c_59() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict DPs:
{ bftMult'#2^#(tuple#2(@dequeue@1, @dequeue@2)) ->
c_1(dequeue^#(@dequeue@1, @dequeue@2))
, dequeue^#(@outq, @inq) -> c_17(dequeue#1^#(@outq, @inq))
, reverse^#(@xs) -> c_2(appendreverse^#(@xs, nil()))
, appendreverse^#(@toreverse, @sofar) ->
c_10(appendreverse#1^#(@toreverse, @sofar))
, bftMult'#5^#(@queue', @acc, @y) ->
c_3(bftMult'^#(@queue', matrixMult(@acc, @y)),
matrixMult^#(@acc, @y))
, bftMult'^#(@queue, @acc) ->
c_19(bftMult'#1^#(bftMult'#2(@queue), @acc), bftMult'#2^#(@queue))
, matrixMult^#(@m1, @m2) -> c_27(matrixMult#1^#(@m1, @m2))
, appendreverse#1^#(::(@a, @as), @sofar) ->
c_5(appendreverse^#(@as, ::(@a, @sofar)))
, computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_7(computeLine#2^#(@m, @acc, @x, @xs))
, computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_35(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
c_9(bftMult'#4^#(@t, @acc, @queue))
, bftMult'#4^#(leaf(), @acc, @queue) ->
c_21(bftMult'^#(@queue, @acc))
, bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
c_22(bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y),
enqueue^#(@t2, enqueue(@t1, @queue)),
enqueue^#(@t1, @queue))
, matrixMult#1^#(::(@l, @ls), @m2) ->
c_12(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, computeLine^#(@line, @m, @acc) ->
c_20(computeLine#1^#(@line, @acc, @m))
, bftMult^#(@t, @acc) ->
c_13(bftMult'^#(tuple#2(::(@t, nil()), nil()), @acc))
, lineMult^#(@n, @l1, @l2) -> c_14(lineMult#1^#(@l1, @l2, @n))
, lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_33(lineMult#2^#(@l2, @n, @x, @xs))
, lineMult#2^#(nil(), @n, @x, @xs) ->
c_15(*^#(@x, @n), lineMult^#(@n, @xs, nil()))
, lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_16(+^#(*(@x, @n), @y), *^#(@x, @n), lineMult^#(@n, @xs, @ys))
, dequeue#1^#(nil(), @inq) ->
c_23(dequeue#2^#(reverse(@inq)), reverse^#(@inq))
, bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
c_18(bftMult'#3^#(@elem, @acc, @queue))
, enqueue^#(@t, @queue) -> c_29(enqueue#1^#(@queue, @t)) }
Weak DPs:
{ appendreverse#1^#(nil(), @sofar) -> c_4()
, computeLine#1^#(nil(), @acc, @m) -> c_6()
, computeLine#2^#(nil(), @acc, @x, @xs) -> c_34()
, bftMult'#3^#(nil(), @acc, @queue) -> c_8()
, matrixMult#1^#(nil(), @m2) -> c_11()
, lineMult#1^#(nil(), @l2, @n) -> c_32()
, *^#(@x, @y) -> c_28(#mult^#(@x, @y))
, +^#(@x, @y) -> c_25(#add^#(@x, @y))
, dequeue#1^#(::(@t, @ts), @inq) -> c_24()
, dequeue#2^#(nil()) -> c_30()
, dequeue#2^#(::(@t, @ts)) -> c_31()
, #add^#(#pos(#s(#0())), @y) -> c_38(#succ^#(@y))
, #add^#(#pos(#s(#s(@x))), @y) ->
c_39(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, #add^#(#0(), @y) -> c_40()
, #add^#(#neg(#s(#0())), @y) -> c_41(#pred^#(@y))
, #add^#(#neg(#s(#s(@x))), @y) ->
c_42(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, enqueue#1^#(tuple#2(@outq, @inq), @t) -> c_26()
, #mult^#(#pos(@x), #pos(@y)) -> c_43(#natmult^#(@x, @y))
, #mult^#(#pos(@x), #0()) -> c_44()
, #mult^#(#pos(@x), #neg(@y)) -> c_45(#natmult^#(@x, @y))
, #mult^#(#0(), #pos(@y)) -> c_46()
, #mult^#(#0(), #0()) -> c_47()
, #mult^#(#0(), #neg(@y)) -> c_48()
, #mult^#(#neg(@x), #pos(@y)) -> c_49(#natmult^#(@x, @y))
, #mult^#(#neg(@x), #0()) -> c_50()
, #mult^#(#neg(@x), #neg(@y)) -> c_51(#natmult^#(@x, @y))
, #natmult^#(#0(), @y) -> c_36()
, #natmult^#(#s(@x), @y) ->
c_37(#add^#(#pos(@y), #natmult(@x, @y)), #natmult^#(@x, @y))
, #succ^#(#pos(#s(@x))) -> c_52()
, #succ^#(#0()) -> c_53()
, #succ^#(#neg(#s(#0()))) -> c_54()
, #succ^#(#neg(#s(#s(@x)))) -> c_55()
, #pred^#(#pos(#s(#0()))) -> c_56()
, #pred^#(#pos(#s(#s(@x)))) -> c_57()
, #pred^#(#0()) -> c_58()
, #pred^#(#neg(#s(@x))) -> c_59() }
Weak Trs:
{ bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) ->
dequeue(@dequeue@1, @dequeue@2)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
, reverse(@xs) -> appendreverse(@xs, nil())
, bftMult'#5(@queue', @acc, @y) ->
bftMult'(@queue', matrixMult(@acc, @y))
, appendreverse#1(nil(), @sofar) -> @sofar
, appendreverse#1(::(@a, @as), @sofar) ->
appendreverse(@as, ::(@a, @sofar))
, computeLine#1(nil(), @acc, @m) -> @acc
, computeLine#1(::(@x, @xs), @acc, @m) ->
computeLine#2(@m, @acc, @x, @xs)
, bftMult'#3(nil(), @acc, @queue) -> @acc
, bftMult'#3(::(@t, @_@3), @acc, @queue) ->
bftMult'#4(@t, @acc, @queue)
, appendreverse(@toreverse, @sofar) ->
appendreverse#1(@toreverse, @sofar)
, matrixMult#1(nil(), @m2) -> nil()
, matrixMult#1(::(@l, @ls), @m2) ->
::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))
, bftMult(@t, @acc) ->
bftMult'(tuple#2(::(@t, nil()), nil()), @acc)
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, dequeue(@outq, @inq) -> dequeue#1(@outq, @inq)
, bftMult'#1(tuple#2(@elem, @queue), @acc) ->
bftMult'#3(@elem, @acc, @queue)
, bftMult'(@queue, @acc) -> bftMult'#1(bftMult'#2(@queue), @acc)
, computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m)
, bftMult'#4(leaf(), @acc, @queue) -> bftMult'(@queue, @acc)
, bftMult'#4(node(@y, @t1, @t2), @acc, @queue) ->
bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)
, dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq))
, dequeue#1(::(@t, @ts), @inq) ->
tuple#2(::(@t, nil()), tuple#2(@ts, @inq))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, +(@x, @y) -> #add(@x, @y)
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, enqueue#1(tuple#2(@outq, @inq), @t) ->
tuple#2(@outq, ::(@t, @inq))
, matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2)
, *(@x, @y) -> #mult(@x, @y)
, enqueue(@t, @queue) -> enqueue#1(@queue, @t)
, dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil()))
, dequeue#2(::(@t, @ts)) ->
tuple#2(::(@t, nil()), tuple#2(@ts, nil()))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, lineMult#1(nil(), @l2, @n) -> nil()
, lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, computeLine#2(nil(), @acc, @x, @xs) -> nil()
, computeLine#2(::(@l, @ls), @acc, @x, @xs) ->
computeLine(@xs, @ls, lineMult(@x, @l, @acc)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
We estimate the number of application of {23} by applications of
Pre({23}) = {13}. Here rules are labeled as follows:
DPs:
{ 1: bftMult'#2^#(tuple#2(@dequeue@1, @dequeue@2)) ->
c_1(dequeue^#(@dequeue@1, @dequeue@2))
, 2: dequeue^#(@outq, @inq) -> c_17(dequeue#1^#(@outq, @inq))
, 3: reverse^#(@xs) -> c_2(appendreverse^#(@xs, nil()))
, 4: appendreverse^#(@toreverse, @sofar) ->
c_10(appendreverse#1^#(@toreverse, @sofar))
, 5: bftMult'#5^#(@queue', @acc, @y) ->
c_3(bftMult'^#(@queue', matrixMult(@acc, @y)),
matrixMult^#(@acc, @y))
, 6: bftMult'^#(@queue, @acc) ->
c_19(bftMult'#1^#(bftMult'#2(@queue), @acc), bftMult'#2^#(@queue))
, 7: matrixMult^#(@m1, @m2) -> c_27(matrixMult#1^#(@m1, @m2))
, 8: appendreverse#1^#(::(@a, @as), @sofar) ->
c_5(appendreverse^#(@as, ::(@a, @sofar)))
, 9: computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_7(computeLine#2^#(@m, @acc, @x, @xs))
, 10: computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_35(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, 11: bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
c_9(bftMult'#4^#(@t, @acc, @queue))
, 12: bftMult'#4^#(leaf(), @acc, @queue) ->
c_21(bftMult'^#(@queue, @acc))
, 13: bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
c_22(bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y),
enqueue^#(@t2, enqueue(@t1, @queue)),
enqueue^#(@t1, @queue))
, 14: matrixMult#1^#(::(@l, @ls), @m2) ->
c_12(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, 15: computeLine^#(@line, @m, @acc) ->
c_20(computeLine#1^#(@line, @acc, @m))
, 16: bftMult^#(@t, @acc) ->
c_13(bftMult'^#(tuple#2(::(@t, nil()), nil()), @acc))
, 17: lineMult^#(@n, @l1, @l2) -> c_14(lineMult#1^#(@l1, @l2, @n))
, 18: lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_33(lineMult#2^#(@l2, @n, @x, @xs))
, 19: lineMult#2^#(nil(), @n, @x, @xs) ->
c_15(*^#(@x, @n), lineMult^#(@n, @xs, nil()))
, 20: lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_16(+^#(*(@x, @n), @y), *^#(@x, @n), lineMult^#(@n, @xs, @ys))
, 21: dequeue#1^#(nil(), @inq) ->
c_23(dequeue#2^#(reverse(@inq)), reverse^#(@inq))
, 22: bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
c_18(bftMult'#3^#(@elem, @acc, @queue))
, 23: enqueue^#(@t, @queue) -> c_29(enqueue#1^#(@queue, @t))
, 24: appendreverse#1^#(nil(), @sofar) -> c_4()
, 25: computeLine#1^#(nil(), @acc, @m) -> c_6()
, 26: computeLine#2^#(nil(), @acc, @x, @xs) -> c_34()
, 27: bftMult'#3^#(nil(), @acc, @queue) -> c_8()
, 28: matrixMult#1^#(nil(), @m2) -> c_11()
, 29: lineMult#1^#(nil(), @l2, @n) -> c_32()
, 30: *^#(@x, @y) -> c_28(#mult^#(@x, @y))
, 31: +^#(@x, @y) -> c_25(#add^#(@x, @y))
, 32: dequeue#1^#(::(@t, @ts), @inq) -> c_24()
, 33: dequeue#2^#(nil()) -> c_30()
, 34: dequeue#2^#(::(@t, @ts)) -> c_31()
, 35: #add^#(#pos(#s(#0())), @y) -> c_38(#succ^#(@y))
, 36: #add^#(#pos(#s(#s(@x))), @y) ->
c_39(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, 37: #add^#(#0(), @y) -> c_40()
, 38: #add^#(#neg(#s(#0())), @y) -> c_41(#pred^#(@y))
, 39: #add^#(#neg(#s(#s(@x))), @y) ->
c_42(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, 40: enqueue#1^#(tuple#2(@outq, @inq), @t) -> c_26()
, 41: #mult^#(#pos(@x), #pos(@y)) -> c_43(#natmult^#(@x, @y))
, 42: #mult^#(#pos(@x), #0()) -> c_44()
, 43: #mult^#(#pos(@x), #neg(@y)) -> c_45(#natmult^#(@x, @y))
, 44: #mult^#(#0(), #pos(@y)) -> c_46()
, 45: #mult^#(#0(), #0()) -> c_47()
, 46: #mult^#(#0(), #neg(@y)) -> c_48()
, 47: #mult^#(#neg(@x), #pos(@y)) -> c_49(#natmult^#(@x, @y))
, 48: #mult^#(#neg(@x), #0()) -> c_50()
, 49: #mult^#(#neg(@x), #neg(@y)) -> c_51(#natmult^#(@x, @y))
, 50: #natmult^#(#0(), @y) -> c_36()
, 51: #natmult^#(#s(@x), @y) ->
c_37(#add^#(#pos(@y), #natmult(@x, @y)), #natmult^#(@x, @y))
, 52: #succ^#(#pos(#s(@x))) -> c_52()
, 53: #succ^#(#0()) -> c_53()
, 54: #succ^#(#neg(#s(#0()))) -> c_54()
, 55: #succ^#(#neg(#s(#s(@x)))) -> c_55()
, 56: #pred^#(#pos(#s(#0()))) -> c_56()
, 57: #pred^#(#pos(#s(#s(@x)))) -> c_57()
, 58: #pred^#(#0()) -> c_58()
, 59: #pred^#(#neg(#s(@x))) -> c_59() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict DPs:
{ bftMult'#2^#(tuple#2(@dequeue@1, @dequeue@2)) ->
c_1(dequeue^#(@dequeue@1, @dequeue@2))
, dequeue^#(@outq, @inq) -> c_17(dequeue#1^#(@outq, @inq))
, reverse^#(@xs) -> c_2(appendreverse^#(@xs, nil()))
, appendreverse^#(@toreverse, @sofar) ->
c_10(appendreverse#1^#(@toreverse, @sofar))
, bftMult'#5^#(@queue', @acc, @y) ->
c_3(bftMult'^#(@queue', matrixMult(@acc, @y)),
matrixMult^#(@acc, @y))
, bftMult'^#(@queue, @acc) ->
c_19(bftMult'#1^#(bftMult'#2(@queue), @acc), bftMult'#2^#(@queue))
, matrixMult^#(@m1, @m2) -> c_27(matrixMult#1^#(@m1, @m2))
, appendreverse#1^#(::(@a, @as), @sofar) ->
c_5(appendreverse^#(@as, ::(@a, @sofar)))
, computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_7(computeLine#2^#(@m, @acc, @x, @xs))
, computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_35(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
c_9(bftMult'#4^#(@t, @acc, @queue))
, bftMult'#4^#(leaf(), @acc, @queue) ->
c_21(bftMult'^#(@queue, @acc))
, bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
c_22(bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y),
enqueue^#(@t2, enqueue(@t1, @queue)),
enqueue^#(@t1, @queue))
, matrixMult#1^#(::(@l, @ls), @m2) ->
c_12(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, computeLine^#(@line, @m, @acc) ->
c_20(computeLine#1^#(@line, @acc, @m))
, bftMult^#(@t, @acc) ->
c_13(bftMult'^#(tuple#2(::(@t, nil()), nil()), @acc))
, lineMult^#(@n, @l1, @l2) -> c_14(lineMult#1^#(@l1, @l2, @n))
, lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_33(lineMult#2^#(@l2, @n, @x, @xs))
, lineMult#2^#(nil(), @n, @x, @xs) ->
c_15(*^#(@x, @n), lineMult^#(@n, @xs, nil()))
, lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_16(+^#(*(@x, @n), @y), *^#(@x, @n), lineMult^#(@n, @xs, @ys))
, dequeue#1^#(nil(), @inq) ->
c_23(dequeue#2^#(reverse(@inq)), reverse^#(@inq))
, bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
c_18(bftMult'#3^#(@elem, @acc, @queue)) }
Weak DPs:
{ appendreverse#1^#(nil(), @sofar) -> c_4()
, computeLine#1^#(nil(), @acc, @m) -> c_6()
, computeLine#2^#(nil(), @acc, @x, @xs) -> c_34()
, bftMult'#3^#(nil(), @acc, @queue) -> c_8()
, matrixMult#1^#(nil(), @m2) -> c_11()
, lineMult#1^#(nil(), @l2, @n) -> c_32()
, *^#(@x, @y) -> c_28(#mult^#(@x, @y))
, +^#(@x, @y) -> c_25(#add^#(@x, @y))
, dequeue#1^#(::(@t, @ts), @inq) -> c_24()
, enqueue^#(@t, @queue) -> c_29(enqueue#1^#(@queue, @t))
, dequeue#2^#(nil()) -> c_30()
, dequeue#2^#(::(@t, @ts)) -> c_31()
, #add^#(#pos(#s(#0())), @y) -> c_38(#succ^#(@y))
, #add^#(#pos(#s(#s(@x))), @y) ->
c_39(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, #add^#(#0(), @y) -> c_40()
, #add^#(#neg(#s(#0())), @y) -> c_41(#pred^#(@y))
, #add^#(#neg(#s(#s(@x))), @y) ->
c_42(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, enqueue#1^#(tuple#2(@outq, @inq), @t) -> c_26()
, #mult^#(#pos(@x), #pos(@y)) -> c_43(#natmult^#(@x, @y))
, #mult^#(#pos(@x), #0()) -> c_44()
, #mult^#(#pos(@x), #neg(@y)) -> c_45(#natmult^#(@x, @y))
, #mult^#(#0(), #pos(@y)) -> c_46()
, #mult^#(#0(), #0()) -> c_47()
, #mult^#(#0(), #neg(@y)) -> c_48()
, #mult^#(#neg(@x), #pos(@y)) -> c_49(#natmult^#(@x, @y))
, #mult^#(#neg(@x), #0()) -> c_50()
, #mult^#(#neg(@x), #neg(@y)) -> c_51(#natmult^#(@x, @y))
, #natmult^#(#0(), @y) -> c_36()
, #natmult^#(#s(@x), @y) ->
c_37(#add^#(#pos(@y), #natmult(@x, @y)), #natmult^#(@x, @y))
, #succ^#(#pos(#s(@x))) -> c_52()
, #succ^#(#0()) -> c_53()
, #succ^#(#neg(#s(#0()))) -> c_54()
, #succ^#(#neg(#s(#s(@x)))) -> c_55()
, #pred^#(#pos(#s(#0()))) -> c_56()
, #pred^#(#pos(#s(#s(@x)))) -> c_57()
, #pred^#(#0()) -> c_58()
, #pred^#(#neg(#s(@x))) -> c_59() }
Weak Trs:
{ bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) ->
dequeue(@dequeue@1, @dequeue@2)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
, reverse(@xs) -> appendreverse(@xs, nil())
, bftMult'#5(@queue', @acc, @y) ->
bftMult'(@queue', matrixMult(@acc, @y))
, appendreverse#1(nil(), @sofar) -> @sofar
, appendreverse#1(::(@a, @as), @sofar) ->
appendreverse(@as, ::(@a, @sofar))
, computeLine#1(nil(), @acc, @m) -> @acc
, computeLine#1(::(@x, @xs), @acc, @m) ->
computeLine#2(@m, @acc, @x, @xs)
, bftMult'#3(nil(), @acc, @queue) -> @acc
, bftMult'#3(::(@t, @_@3), @acc, @queue) ->
bftMult'#4(@t, @acc, @queue)
, appendreverse(@toreverse, @sofar) ->
appendreverse#1(@toreverse, @sofar)
, matrixMult#1(nil(), @m2) -> nil()
, matrixMult#1(::(@l, @ls), @m2) ->
::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))
, bftMult(@t, @acc) ->
bftMult'(tuple#2(::(@t, nil()), nil()), @acc)
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, dequeue(@outq, @inq) -> dequeue#1(@outq, @inq)
, bftMult'#1(tuple#2(@elem, @queue), @acc) ->
bftMult'#3(@elem, @acc, @queue)
, bftMult'(@queue, @acc) -> bftMult'#1(bftMult'#2(@queue), @acc)
, computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m)
, bftMult'#4(leaf(), @acc, @queue) -> bftMult'(@queue, @acc)
, bftMult'#4(node(@y, @t1, @t2), @acc, @queue) ->
bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)
, dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq))
, dequeue#1(::(@t, @ts), @inq) ->
tuple#2(::(@t, nil()), tuple#2(@ts, @inq))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, +(@x, @y) -> #add(@x, @y)
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, enqueue#1(tuple#2(@outq, @inq), @t) ->
tuple#2(@outq, ::(@t, @inq))
, matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2)
, *(@x, @y) -> #mult(@x, @y)
, enqueue(@t, @queue) -> enqueue#1(@queue, @t)
, dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil()))
, dequeue#2(::(@t, @ts)) ->
tuple#2(::(@t, nil()), tuple#2(@ts, nil()))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, lineMult#1(nil(), @l2, @n) -> nil()
, lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, computeLine#2(nil(), @acc, @x, @xs) -> nil()
, computeLine#2(::(@l, @ls), @acc, @x, @xs) ->
computeLine(@xs, @ls, lineMult(@x, @l, @acc)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ appendreverse#1^#(nil(), @sofar) -> c_4()
, computeLine#1^#(nil(), @acc, @m) -> c_6()
, computeLine#2^#(nil(), @acc, @x, @xs) -> c_34()
, bftMult'#3^#(nil(), @acc, @queue) -> c_8()
, matrixMult#1^#(nil(), @m2) -> c_11()
, lineMult#1^#(nil(), @l2, @n) -> c_32()
, *^#(@x, @y) -> c_28(#mult^#(@x, @y))
, +^#(@x, @y) -> c_25(#add^#(@x, @y))
, dequeue#1^#(::(@t, @ts), @inq) -> c_24()
, enqueue^#(@t, @queue) -> c_29(enqueue#1^#(@queue, @t))
, dequeue#2^#(nil()) -> c_30()
, dequeue#2^#(::(@t, @ts)) -> c_31()
, #add^#(#pos(#s(#0())), @y) -> c_38(#succ^#(@y))
, #add^#(#pos(#s(#s(@x))), @y) ->
c_39(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, #add^#(#0(), @y) -> c_40()
, #add^#(#neg(#s(#0())), @y) -> c_41(#pred^#(@y))
, #add^#(#neg(#s(#s(@x))), @y) ->
c_42(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, enqueue#1^#(tuple#2(@outq, @inq), @t) -> c_26()
, #mult^#(#pos(@x), #pos(@y)) -> c_43(#natmult^#(@x, @y))
, #mult^#(#pos(@x), #0()) -> c_44()
, #mult^#(#pos(@x), #neg(@y)) -> c_45(#natmult^#(@x, @y))
, #mult^#(#0(), #pos(@y)) -> c_46()
, #mult^#(#0(), #0()) -> c_47()
, #mult^#(#0(), #neg(@y)) -> c_48()
, #mult^#(#neg(@x), #pos(@y)) -> c_49(#natmult^#(@x, @y))
, #mult^#(#neg(@x), #0()) -> c_50()
, #mult^#(#neg(@x), #neg(@y)) -> c_51(#natmult^#(@x, @y))
, #natmult^#(#0(), @y) -> c_36()
, #natmult^#(#s(@x), @y) ->
c_37(#add^#(#pos(@y), #natmult(@x, @y)), #natmult^#(@x, @y))
, #succ^#(#pos(#s(@x))) -> c_52()
, #succ^#(#0()) -> c_53()
, #succ^#(#neg(#s(#0()))) -> c_54()
, #succ^#(#neg(#s(#s(@x)))) -> c_55()
, #pred^#(#pos(#s(#0()))) -> c_56()
, #pred^#(#pos(#s(#s(@x)))) -> c_57()
, #pred^#(#0()) -> c_58()
, #pred^#(#neg(#s(@x))) -> c_59() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict DPs:
{ bftMult'#2^#(tuple#2(@dequeue@1, @dequeue@2)) ->
c_1(dequeue^#(@dequeue@1, @dequeue@2))
, dequeue^#(@outq, @inq) -> c_17(dequeue#1^#(@outq, @inq))
, reverse^#(@xs) -> c_2(appendreverse^#(@xs, nil()))
, appendreverse^#(@toreverse, @sofar) ->
c_10(appendreverse#1^#(@toreverse, @sofar))
, bftMult'#5^#(@queue', @acc, @y) ->
c_3(bftMult'^#(@queue', matrixMult(@acc, @y)),
matrixMult^#(@acc, @y))
, bftMult'^#(@queue, @acc) ->
c_19(bftMult'#1^#(bftMult'#2(@queue), @acc), bftMult'#2^#(@queue))
, matrixMult^#(@m1, @m2) -> c_27(matrixMult#1^#(@m1, @m2))
, appendreverse#1^#(::(@a, @as), @sofar) ->
c_5(appendreverse^#(@as, ::(@a, @sofar)))
, computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_7(computeLine#2^#(@m, @acc, @x, @xs))
, computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_35(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
c_9(bftMult'#4^#(@t, @acc, @queue))
, bftMult'#4^#(leaf(), @acc, @queue) ->
c_21(bftMult'^#(@queue, @acc))
, bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
c_22(bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y),
enqueue^#(@t2, enqueue(@t1, @queue)),
enqueue^#(@t1, @queue))
, matrixMult#1^#(::(@l, @ls), @m2) ->
c_12(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, computeLine^#(@line, @m, @acc) ->
c_20(computeLine#1^#(@line, @acc, @m))
, bftMult^#(@t, @acc) ->
c_13(bftMult'^#(tuple#2(::(@t, nil()), nil()), @acc))
, lineMult^#(@n, @l1, @l2) -> c_14(lineMult#1^#(@l1, @l2, @n))
, lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_33(lineMult#2^#(@l2, @n, @x, @xs))
, lineMult#2^#(nil(), @n, @x, @xs) ->
c_15(*^#(@x, @n), lineMult^#(@n, @xs, nil()))
, lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_16(+^#(*(@x, @n), @y), *^#(@x, @n), lineMult^#(@n, @xs, @ys))
, dequeue#1^#(nil(), @inq) ->
c_23(dequeue#2^#(reverse(@inq)), reverse^#(@inq))
, bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
c_18(bftMult'#3^#(@elem, @acc, @queue)) }
Weak Trs:
{ bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) ->
dequeue(@dequeue@1, @dequeue@2)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
, reverse(@xs) -> appendreverse(@xs, nil())
, bftMult'#5(@queue', @acc, @y) ->
bftMult'(@queue', matrixMult(@acc, @y))
, appendreverse#1(nil(), @sofar) -> @sofar
, appendreverse#1(::(@a, @as), @sofar) ->
appendreverse(@as, ::(@a, @sofar))
, computeLine#1(nil(), @acc, @m) -> @acc
, computeLine#1(::(@x, @xs), @acc, @m) ->
computeLine#2(@m, @acc, @x, @xs)
, bftMult'#3(nil(), @acc, @queue) -> @acc
, bftMult'#3(::(@t, @_@3), @acc, @queue) ->
bftMult'#4(@t, @acc, @queue)
, appendreverse(@toreverse, @sofar) ->
appendreverse#1(@toreverse, @sofar)
, matrixMult#1(nil(), @m2) -> nil()
, matrixMult#1(::(@l, @ls), @m2) ->
::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))
, bftMult(@t, @acc) ->
bftMult'(tuple#2(::(@t, nil()), nil()), @acc)
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, dequeue(@outq, @inq) -> dequeue#1(@outq, @inq)
, bftMult'#1(tuple#2(@elem, @queue), @acc) ->
bftMult'#3(@elem, @acc, @queue)
, bftMult'(@queue, @acc) -> bftMult'#1(bftMult'#2(@queue), @acc)
, computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m)
, bftMult'#4(leaf(), @acc, @queue) -> bftMult'(@queue, @acc)
, bftMult'#4(node(@y, @t1, @t2), @acc, @queue) ->
bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)
, dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq))
, dequeue#1(::(@t, @ts), @inq) ->
tuple#2(::(@t, nil()), tuple#2(@ts, @inq))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, +(@x, @y) -> #add(@x, @y)
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, enqueue#1(tuple#2(@outq, @inq), @t) ->
tuple#2(@outq, ::(@t, @inq))
, matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2)
, *(@x, @y) -> #mult(@x, @y)
, enqueue(@t, @queue) -> enqueue#1(@queue, @t)
, dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil()))
, dequeue#2(::(@t, @ts)) ->
tuple#2(::(@t, nil()), tuple#2(@ts, nil()))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, lineMult#1(nil(), @l2, @n) -> nil()
, lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, computeLine#2(nil(), @acc, @x, @xs) -> nil()
, computeLine#2(::(@l, @ls), @acc, @x, @xs) ->
computeLine(@xs, @ls, lineMult(@x, @l, @acc)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
c_22(bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y),
enqueue^#(@t2, enqueue(@t1, @queue)),
enqueue^#(@t1, @queue))
, lineMult#2^#(nil(), @n, @x, @xs) ->
c_15(*^#(@x, @n), lineMult^#(@n, @xs, nil()))
, lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_16(+^#(*(@x, @n), @y), *^#(@x, @n), lineMult^#(@n, @xs, @ys))
, dequeue#1^#(nil(), @inq) ->
c_23(dequeue#2^#(reverse(@inq)), reverse^#(@inq)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict DPs:
{ bftMult'#2^#(tuple#2(@dequeue@1, @dequeue@2)) ->
c_1(dequeue^#(@dequeue@1, @dequeue@2))
, dequeue^#(@outq, @inq) -> c_2(dequeue#1^#(@outq, @inq))
, reverse^#(@xs) -> c_3(appendreverse^#(@xs, nil()))
, appendreverse^#(@toreverse, @sofar) ->
c_4(appendreverse#1^#(@toreverse, @sofar))
, bftMult'#5^#(@queue', @acc, @y) ->
c_5(bftMult'^#(@queue', matrixMult(@acc, @y)),
matrixMult^#(@acc, @y))
, bftMult'^#(@queue, @acc) ->
c_6(bftMult'#1^#(bftMult'#2(@queue), @acc), bftMult'#2^#(@queue))
, matrixMult^#(@m1, @m2) -> c_7(matrixMult#1^#(@m1, @m2))
, appendreverse#1^#(::(@a, @as), @sofar) ->
c_8(appendreverse^#(@as, ::(@a, @sofar)))
, computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_9(computeLine#2^#(@m, @acc, @x, @xs))
, computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_10(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
c_11(bftMult'#4^#(@t, @acc, @queue))
, bftMult'#4^#(leaf(), @acc, @queue) ->
c_12(bftMult'^#(@queue, @acc))
, bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
c_13(bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y))
, matrixMult#1^#(::(@l, @ls), @m2) ->
c_14(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, computeLine^#(@line, @m, @acc) ->
c_15(computeLine#1^#(@line, @acc, @m))
, bftMult^#(@t, @acc) ->
c_16(bftMult'^#(tuple#2(::(@t, nil()), nil()), @acc))
, lineMult^#(@n, @l1, @l2) -> c_17(lineMult#1^#(@l1, @l2, @n))
, lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_18(lineMult#2^#(@l2, @n, @x, @xs))
, lineMult#2^#(nil(), @n, @x, @xs) ->
c_19(lineMult^#(@n, @xs, nil()))
, lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_20(lineMult^#(@n, @xs, @ys))
, dequeue#1^#(nil(), @inq) -> c_21(reverse^#(@inq))
, bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
c_22(bftMult'#3^#(@elem, @acc, @queue)) }
Weak Trs:
{ bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) ->
dequeue(@dequeue@1, @dequeue@2)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
, reverse(@xs) -> appendreverse(@xs, nil())
, bftMult'#5(@queue', @acc, @y) ->
bftMult'(@queue', matrixMult(@acc, @y))
, appendreverse#1(nil(), @sofar) -> @sofar
, appendreverse#1(::(@a, @as), @sofar) ->
appendreverse(@as, ::(@a, @sofar))
, computeLine#1(nil(), @acc, @m) -> @acc
, computeLine#1(::(@x, @xs), @acc, @m) ->
computeLine#2(@m, @acc, @x, @xs)
, bftMult'#3(nil(), @acc, @queue) -> @acc
, bftMult'#3(::(@t, @_@3), @acc, @queue) ->
bftMult'#4(@t, @acc, @queue)
, appendreverse(@toreverse, @sofar) ->
appendreverse#1(@toreverse, @sofar)
, matrixMult#1(nil(), @m2) -> nil()
, matrixMult#1(::(@l, @ls), @m2) ->
::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))
, bftMult(@t, @acc) ->
bftMult'(tuple#2(::(@t, nil()), nil()), @acc)
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, dequeue(@outq, @inq) -> dequeue#1(@outq, @inq)
, bftMult'#1(tuple#2(@elem, @queue), @acc) ->
bftMult'#3(@elem, @acc, @queue)
, bftMult'(@queue, @acc) -> bftMult'#1(bftMult'#2(@queue), @acc)
, computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m)
, bftMult'#4(leaf(), @acc, @queue) -> bftMult'(@queue, @acc)
, bftMult'#4(node(@y, @t1, @t2), @acc, @queue) ->
bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)
, dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq))
, dequeue#1(::(@t, @ts), @inq) ->
tuple#2(::(@t, nil()), tuple#2(@ts, @inq))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, +(@x, @y) -> #add(@x, @y)
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, enqueue#1(tuple#2(@outq, @inq), @t) ->
tuple#2(@outq, ::(@t, @inq))
, matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2)
, *(@x, @y) -> #mult(@x, @y)
, enqueue(@t, @queue) -> enqueue#1(@queue, @t)
, dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil()))
, dequeue#2(::(@t, @ts)) ->
tuple#2(::(@t, nil()), tuple#2(@ts, nil()))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, lineMult#1(nil(), @l2, @n) -> nil()
, lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, computeLine#2(nil(), @acc, @x, @xs) -> nil()
, computeLine#2(::(@l, @ls), @acc, @x, @xs) ->
computeLine(@xs, @ls, lineMult(@x, @l, @acc)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
We replace rewrite rules by usable rules:
Weak Usable Rules:
{ bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) ->
dequeue(@dequeue@1, @dequeue@2)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
, reverse(@xs) -> appendreverse(@xs, nil())
, appendreverse#1(nil(), @sofar) -> @sofar
, appendreverse#1(::(@a, @as), @sofar) ->
appendreverse(@as, ::(@a, @sofar))
, computeLine#1(nil(), @acc, @m) -> @acc
, computeLine#1(::(@x, @xs), @acc, @m) ->
computeLine#2(@m, @acc, @x, @xs)
, appendreverse(@toreverse, @sofar) ->
appendreverse#1(@toreverse, @sofar)
, matrixMult#1(nil(), @m2) -> nil()
, matrixMult#1(::(@l, @ls), @m2) ->
::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, dequeue(@outq, @inq) -> dequeue#1(@outq, @inq)
, computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m)
, dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq))
, dequeue#1(::(@t, @ts), @inq) ->
tuple#2(::(@t, nil()), tuple#2(@ts, @inq))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, +(@x, @y) -> #add(@x, @y)
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, enqueue#1(tuple#2(@outq, @inq), @t) ->
tuple#2(@outq, ::(@t, @inq))
, matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2)
, *(@x, @y) -> #mult(@x, @y)
, enqueue(@t, @queue) -> enqueue#1(@queue, @t)
, dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil()))
, dequeue#2(::(@t, @ts)) ->
tuple#2(::(@t, nil()), tuple#2(@ts, nil()))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, lineMult#1(nil(), @l2, @n) -> nil()
, lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, computeLine#2(nil(), @acc, @x, @xs) -> nil()
, computeLine#2(::(@l, @ls), @acc, @x, @xs) ->
computeLine(@xs, @ls, lineMult(@x, @l, @acc)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict DPs:
{ bftMult'#2^#(tuple#2(@dequeue@1, @dequeue@2)) ->
c_1(dequeue^#(@dequeue@1, @dequeue@2))
, dequeue^#(@outq, @inq) -> c_2(dequeue#1^#(@outq, @inq))
, reverse^#(@xs) -> c_3(appendreverse^#(@xs, nil()))
, appendreverse^#(@toreverse, @sofar) ->
c_4(appendreverse#1^#(@toreverse, @sofar))
, bftMult'#5^#(@queue', @acc, @y) ->
c_5(bftMult'^#(@queue', matrixMult(@acc, @y)),
matrixMult^#(@acc, @y))
, bftMult'^#(@queue, @acc) ->
c_6(bftMult'#1^#(bftMult'#2(@queue), @acc), bftMult'#2^#(@queue))
, matrixMult^#(@m1, @m2) -> c_7(matrixMult#1^#(@m1, @m2))
, appendreverse#1^#(::(@a, @as), @sofar) ->
c_8(appendreverse^#(@as, ::(@a, @sofar)))
, computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_9(computeLine#2^#(@m, @acc, @x, @xs))
, computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_10(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
c_11(bftMult'#4^#(@t, @acc, @queue))
, bftMult'#4^#(leaf(), @acc, @queue) ->
c_12(bftMult'^#(@queue, @acc))
, bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
c_13(bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y))
, matrixMult#1^#(::(@l, @ls), @m2) ->
c_14(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, computeLine^#(@line, @m, @acc) ->
c_15(computeLine#1^#(@line, @acc, @m))
, bftMult^#(@t, @acc) ->
c_16(bftMult'^#(tuple#2(::(@t, nil()), nil()), @acc))
, lineMult^#(@n, @l1, @l2) -> c_17(lineMult#1^#(@l1, @l2, @n))
, lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_18(lineMult#2^#(@l2, @n, @x, @xs))
, lineMult#2^#(nil(), @n, @x, @xs) ->
c_19(lineMult^#(@n, @xs, nil()))
, lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_20(lineMult^#(@n, @xs, @ys))
, dequeue#1^#(nil(), @inq) -> c_21(reverse^#(@inq))
, bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
c_22(bftMult'#3^#(@elem, @acc, @queue)) }
Weak Trs:
{ bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) ->
dequeue(@dequeue@1, @dequeue@2)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
, reverse(@xs) -> appendreverse(@xs, nil())
, appendreverse#1(nil(), @sofar) -> @sofar
, appendreverse#1(::(@a, @as), @sofar) ->
appendreverse(@as, ::(@a, @sofar))
, computeLine#1(nil(), @acc, @m) -> @acc
, computeLine#1(::(@x, @xs), @acc, @m) ->
computeLine#2(@m, @acc, @x, @xs)
, appendreverse(@toreverse, @sofar) ->
appendreverse#1(@toreverse, @sofar)
, matrixMult#1(nil(), @m2) -> nil()
, matrixMult#1(::(@l, @ls), @m2) ->
::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, dequeue(@outq, @inq) -> dequeue#1(@outq, @inq)
, computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m)
, dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq))
, dequeue#1(::(@t, @ts), @inq) ->
tuple#2(::(@t, nil()), tuple#2(@ts, @inq))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, +(@x, @y) -> #add(@x, @y)
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, enqueue#1(tuple#2(@outq, @inq), @t) ->
tuple#2(@outq, ::(@t, @inq))
, matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2)
, *(@x, @y) -> #mult(@x, @y)
, enqueue(@t, @queue) -> enqueue#1(@queue, @t)
, dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil()))
, dequeue#2(::(@t, @ts)) ->
tuple#2(::(@t, nil()), tuple#2(@ts, nil()))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, lineMult#1(nil(), @l2, @n) -> nil()
, lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, computeLine#2(nil(), @acc, @x, @xs) -> nil()
, computeLine#2(::(@l, @ls), @acc, @x, @xs) ->
computeLine(@xs, @ls, lineMult(@x, @l, @acc)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
Consider the dependency graph
1: bftMult'#2^#(tuple#2(@dequeue@1, @dequeue@2)) ->
c_1(dequeue^#(@dequeue@1, @dequeue@2))
-->_1 dequeue^#(@outq, @inq) -> c_2(dequeue#1^#(@outq, @inq)) :2
2: dequeue^#(@outq, @inq) -> c_2(dequeue#1^#(@outq, @inq))
-->_1 dequeue#1^#(nil(), @inq) -> c_21(reverse^#(@inq)) :21
3: reverse^#(@xs) -> c_3(appendreverse^#(@xs, nil()))
-->_1 appendreverse^#(@toreverse, @sofar) ->
c_4(appendreverse#1^#(@toreverse, @sofar)) :4
4: appendreverse^#(@toreverse, @sofar) ->
c_4(appendreverse#1^#(@toreverse, @sofar))
-->_1 appendreverse#1^#(::(@a, @as), @sofar) ->
c_8(appendreverse^#(@as, ::(@a, @sofar))) :8
5: bftMult'#5^#(@queue', @acc, @y) ->
c_5(bftMult'^#(@queue', matrixMult(@acc, @y)),
matrixMult^#(@acc, @y))
-->_2 matrixMult^#(@m1, @m2) -> c_7(matrixMult#1^#(@m1, @m2)) :7
-->_1 bftMult'^#(@queue, @acc) ->
c_6(bftMult'#1^#(bftMult'#2(@queue), @acc),
bftMult'#2^#(@queue)) :6
6: bftMult'^#(@queue, @acc) ->
c_6(bftMult'#1^#(bftMult'#2(@queue), @acc), bftMult'#2^#(@queue))
-->_1 bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
c_22(bftMult'#3^#(@elem, @acc, @queue)) :22
-->_2 bftMult'#2^#(tuple#2(@dequeue@1, @dequeue@2)) ->
c_1(dequeue^#(@dequeue@1, @dequeue@2)) :1
7: matrixMult^#(@m1, @m2) -> c_7(matrixMult#1^#(@m1, @m2))
-->_1 matrixMult#1^#(::(@l, @ls), @m2) ->
c_14(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2)) :14
8: appendreverse#1^#(::(@a, @as), @sofar) ->
c_8(appendreverse^#(@as, ::(@a, @sofar)))
-->_1 appendreverse^#(@toreverse, @sofar) ->
c_4(appendreverse#1^#(@toreverse, @sofar)) :4
9: computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_9(computeLine#2^#(@m, @acc, @x, @xs))
-->_1 computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_10(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc)) :10
10: computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_10(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
-->_2 lineMult^#(@n, @l1, @l2) ->
c_17(lineMult#1^#(@l1, @l2, @n)) :17
-->_1 computeLine^#(@line, @m, @acc) ->
c_15(computeLine#1^#(@line, @acc, @m)) :15
11: bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
c_11(bftMult'#4^#(@t, @acc, @queue))
-->_1 bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
c_13(bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)),
@acc,
@y)) :13
-->_1 bftMult'#4^#(leaf(), @acc, @queue) ->
c_12(bftMult'^#(@queue, @acc)) :12
12: bftMult'#4^#(leaf(), @acc, @queue) ->
c_12(bftMult'^#(@queue, @acc))
-->_1 bftMult'^#(@queue, @acc) ->
c_6(bftMult'#1^#(bftMult'#2(@queue), @acc),
bftMult'#2^#(@queue)) :6
13: bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
c_13(bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y))
-->_1 bftMult'#5^#(@queue', @acc, @y) ->
c_5(bftMult'^#(@queue', matrixMult(@acc, @y)),
matrixMult^#(@acc, @y)) :5
14: matrixMult#1^#(::(@l, @ls), @m2) ->
c_14(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
-->_1 computeLine^#(@line, @m, @acc) ->
c_15(computeLine#1^#(@line, @acc, @m)) :15
-->_2 matrixMult^#(@m1, @m2) -> c_7(matrixMult#1^#(@m1, @m2)) :7
15: computeLine^#(@line, @m, @acc) ->
c_15(computeLine#1^#(@line, @acc, @m))
-->_1 computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_9(computeLine#2^#(@m, @acc, @x, @xs)) :9
16: bftMult^#(@t, @acc) ->
c_16(bftMult'^#(tuple#2(::(@t, nil()), nil()), @acc))
-->_1 bftMult'^#(@queue, @acc) ->
c_6(bftMult'#1^#(bftMult'#2(@queue), @acc),
bftMult'#2^#(@queue)) :6
17: lineMult^#(@n, @l1, @l2) -> c_17(lineMult#1^#(@l1, @l2, @n))
-->_1 lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_18(lineMult#2^#(@l2, @n, @x, @xs)) :18
18: lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_18(lineMult#2^#(@l2, @n, @x, @xs))
-->_1 lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_20(lineMult^#(@n, @xs, @ys)) :20
-->_1 lineMult#2^#(nil(), @n, @x, @xs) ->
c_19(lineMult^#(@n, @xs, nil())) :19
19: lineMult#2^#(nil(), @n, @x, @xs) ->
c_19(lineMult^#(@n, @xs, nil()))
-->_1 lineMult^#(@n, @l1, @l2) ->
c_17(lineMult#1^#(@l1, @l2, @n)) :17
20: lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_20(lineMult^#(@n, @xs, @ys))
-->_1 lineMult^#(@n, @l1, @l2) ->
c_17(lineMult#1^#(@l1, @l2, @n)) :17
21: dequeue#1^#(nil(), @inq) -> c_21(reverse^#(@inq))
-->_1 reverse^#(@xs) -> c_3(appendreverse^#(@xs, nil())) :3
22: bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
c_22(bftMult'#3^#(@elem, @acc, @queue))
-->_1 bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
c_11(bftMult'#4^#(@t, @acc, @queue)) :11
Following roots of the dependency graph are removed, as the
considered set of starting terms is closed under reduction with
respect to these rules (modulo compound contexts).
{ bftMult^#(@t, @acc) ->
c_16(bftMult'^#(tuple#2(::(@t, nil()), nil()), @acc)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict DPs:
{ bftMult'#2^#(tuple#2(@dequeue@1, @dequeue@2)) ->
c_1(dequeue^#(@dequeue@1, @dequeue@2))
, dequeue^#(@outq, @inq) -> c_2(dequeue#1^#(@outq, @inq))
, reverse^#(@xs) -> c_3(appendreverse^#(@xs, nil()))
, appendreverse^#(@toreverse, @sofar) ->
c_4(appendreverse#1^#(@toreverse, @sofar))
, bftMult'#5^#(@queue', @acc, @y) ->
c_5(bftMult'^#(@queue', matrixMult(@acc, @y)),
matrixMult^#(@acc, @y))
, bftMult'^#(@queue, @acc) ->
c_6(bftMult'#1^#(bftMult'#2(@queue), @acc), bftMult'#2^#(@queue))
, matrixMult^#(@m1, @m2) -> c_7(matrixMult#1^#(@m1, @m2))
, appendreverse#1^#(::(@a, @as), @sofar) ->
c_8(appendreverse^#(@as, ::(@a, @sofar)))
, computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_9(computeLine#2^#(@m, @acc, @x, @xs))
, computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_10(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
c_11(bftMult'#4^#(@t, @acc, @queue))
, bftMult'#4^#(leaf(), @acc, @queue) ->
c_12(bftMult'^#(@queue, @acc))
, bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
c_13(bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y))
, matrixMult#1^#(::(@l, @ls), @m2) ->
c_14(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, computeLine^#(@line, @m, @acc) ->
c_15(computeLine#1^#(@line, @acc, @m))
, lineMult^#(@n, @l1, @l2) -> c_17(lineMult#1^#(@l1, @l2, @n))
, lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_18(lineMult#2^#(@l2, @n, @x, @xs))
, lineMult#2^#(nil(), @n, @x, @xs) ->
c_19(lineMult^#(@n, @xs, nil()))
, lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_20(lineMult^#(@n, @xs, @ys))
, dequeue#1^#(nil(), @inq) -> c_21(reverse^#(@inq))
, bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
c_22(bftMult'#3^#(@elem, @acc, @queue)) }
Weak Trs:
{ bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) ->
dequeue(@dequeue@1, @dequeue@2)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
, reverse(@xs) -> appendreverse(@xs, nil())
, appendreverse#1(nil(), @sofar) -> @sofar
, appendreverse#1(::(@a, @as), @sofar) ->
appendreverse(@as, ::(@a, @sofar))
, computeLine#1(nil(), @acc, @m) -> @acc
, computeLine#1(::(@x, @xs), @acc, @m) ->
computeLine#2(@m, @acc, @x, @xs)
, appendreverse(@toreverse, @sofar) ->
appendreverse#1(@toreverse, @sofar)
, matrixMult#1(nil(), @m2) -> nil()
, matrixMult#1(::(@l, @ls), @m2) ->
::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, dequeue(@outq, @inq) -> dequeue#1(@outq, @inq)
, computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m)
, dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq))
, dequeue#1(::(@t, @ts), @inq) ->
tuple#2(::(@t, nil()), tuple#2(@ts, @inq))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, +(@x, @y) -> #add(@x, @y)
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, enqueue#1(tuple#2(@outq, @inq), @t) ->
tuple#2(@outq, ::(@t, @inq))
, matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2)
, *(@x, @y) -> #mult(@x, @y)
, enqueue(@t, @queue) -> enqueue#1(@queue, @t)
, dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil()))
, dequeue#2(::(@t, @ts)) ->
tuple#2(::(@t, nil()), tuple#2(@ts, nil()))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, lineMult#1(nil(), @l2, @n) -> nil()
, lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, computeLine#2(nil(), @acc, @x, @xs) -> nil()
, computeLine#2(::(@l, @ls), @acc, @x, @xs) ->
computeLine(@xs, @ls, lineMult(@x, @l, @acc)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
We decompose the input problem according to the dependency graph
into the upper component
{ bftMult'#5^#(@queue', @acc, @y) ->
c_5(bftMult'^#(@queue', matrixMult(@acc, @y)),
matrixMult^#(@acc, @y))
, bftMult'^#(@queue, @acc) ->
c_6(bftMult'#1^#(bftMult'#2(@queue), @acc), bftMult'#2^#(@queue))
, bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
c_11(bftMult'#4^#(@t, @acc, @queue))
, bftMult'#4^#(leaf(), @acc, @queue) ->
c_12(bftMult'^#(@queue, @acc))
, bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
c_13(bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y))
, bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
c_22(bftMult'#3^#(@elem, @acc, @queue)) }
and lower component
{ bftMult'#2^#(tuple#2(@dequeue@1, @dequeue@2)) ->
c_1(dequeue^#(@dequeue@1, @dequeue@2))
, dequeue^#(@outq, @inq) -> c_2(dequeue#1^#(@outq, @inq))
, reverse^#(@xs) -> c_3(appendreverse^#(@xs, nil()))
, appendreverse^#(@toreverse, @sofar) ->
c_4(appendreverse#1^#(@toreverse, @sofar))
, matrixMult^#(@m1, @m2) -> c_7(matrixMult#1^#(@m1, @m2))
, appendreverse#1^#(::(@a, @as), @sofar) ->
c_8(appendreverse^#(@as, ::(@a, @sofar)))
, computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_9(computeLine#2^#(@m, @acc, @x, @xs))
, computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_10(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, matrixMult#1^#(::(@l, @ls), @m2) ->
c_14(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, computeLine^#(@line, @m, @acc) ->
c_15(computeLine#1^#(@line, @acc, @m))
, lineMult^#(@n, @l1, @l2) -> c_17(lineMult#1^#(@l1, @l2, @n))
, lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_18(lineMult#2^#(@l2, @n, @x, @xs))
, lineMult#2^#(nil(), @n, @x, @xs) ->
c_19(lineMult^#(@n, @xs, nil()))
, lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_20(lineMult^#(@n, @xs, @ys))
, dequeue#1^#(nil(), @inq) -> c_21(reverse^#(@inq)) }
Further, following extension rules are added to the lower
component.
{ bftMult'#5^#(@queue', @acc, @y) ->
bftMult'^#(@queue', matrixMult(@acc, @y))
, bftMult'#5^#(@queue', @acc, @y) -> matrixMult^#(@acc, @y)
, bftMult'^#(@queue, @acc) -> bftMult'#2^#(@queue)
, bftMult'^#(@queue, @acc) ->
bftMult'#1^#(bftMult'#2(@queue), @acc)
, bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
bftMult'#4^#(@t, @acc, @queue)
, bftMult'#4^#(leaf(), @acc, @queue) -> bftMult'^#(@queue, @acc)
, bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)
, bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
bftMult'#3^#(@elem, @acc, @queue) }
TcT solves the upper component with certificate YES(O(1),O(n^1)).
Sub-proof:
----------
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ bftMult'#5^#(@queue', @acc, @y) ->
c_5(bftMult'^#(@queue', matrixMult(@acc, @y)),
matrixMult^#(@acc, @y))
, bftMult'^#(@queue, @acc) ->
c_6(bftMult'#1^#(bftMult'#2(@queue), @acc), bftMult'#2^#(@queue))
, bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
c_11(bftMult'#4^#(@t, @acc, @queue))
, bftMult'#4^#(leaf(), @acc, @queue) ->
c_12(bftMult'^#(@queue, @acc))
, bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
c_13(bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y))
, bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
c_22(bftMult'#3^#(@elem, @acc, @queue)) }
Weak Trs:
{ bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) ->
dequeue(@dequeue@1, @dequeue@2)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
, reverse(@xs) -> appendreverse(@xs, nil())
, appendreverse#1(nil(), @sofar) -> @sofar
, appendreverse#1(::(@a, @as), @sofar) ->
appendreverse(@as, ::(@a, @sofar))
, computeLine#1(nil(), @acc, @m) -> @acc
, computeLine#1(::(@x, @xs), @acc, @m) ->
computeLine#2(@m, @acc, @x, @xs)
, appendreverse(@toreverse, @sofar) ->
appendreverse#1(@toreverse, @sofar)
, matrixMult#1(nil(), @m2) -> nil()
, matrixMult#1(::(@l, @ls), @m2) ->
::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, dequeue(@outq, @inq) -> dequeue#1(@outq, @inq)
, computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m)
, dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq))
, dequeue#1(::(@t, @ts), @inq) ->
tuple#2(::(@t, nil()), tuple#2(@ts, @inq))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, +(@x, @y) -> #add(@x, @y)
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, enqueue#1(tuple#2(@outq, @inq), @t) ->
tuple#2(@outq, ::(@t, @inq))
, matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2)
, *(@x, @y) -> #mult(@x, @y)
, enqueue(@t, @queue) -> enqueue#1(@queue, @t)
, dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil()))
, dequeue#2(::(@t, @ts)) ->
tuple#2(::(@t, nil()), tuple#2(@ts, nil()))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, lineMult#1(nil(), @l2, @n) -> nil()
, lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, computeLine#2(nil(), @acc, @x, @xs) -> nil()
, computeLine#2(::(@l, @ls), @acc, @x, @xs) ->
computeLine(@xs, @ls, lineMult(@x, @l, @acc)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
DPs:
{ 3: bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
c_11(bftMult'#4^#(@t, @acc, @queue))
, 4: bftMult'#4^#(leaf(), @acc, @queue) ->
c_12(bftMult'^#(@queue, @acc)) }
Trs:
{ matrixMult#1(nil(), @m2) -> nil()
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, dequeue(@outq, @inq) -> dequeue#1(@outq, @inq)
, dequeue#1(::(@t, @ts), @inq) ->
tuple#2(::(@t, nil()), tuple#2(@ts, @inq))
, *(@x, @y) -> #mult(@x, @y)
, dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil()))
, dequeue#2(::(@t, @ts)) ->
tuple#2(::(@t, nil()), tuple#2(@ts, nil())) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_5) = {1}, Uargs(c_6) = {1}, Uargs(c_11) = {1},
Uargs(c_12) = {1}, Uargs(c_13) = {1}, Uargs(c_22) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[bftMult'#2](x1) = [1] x1 + [3]
[#natmult](x1, x2) = [0]
[reverse](x1) = [1] x1 + [0]
[appendreverse#1](x1, x2) = [1] x1 + [1] x2 + [0]
[computeLine#1](x1, x2, x3) = [3] x2 + [0]
[appendreverse](x1, x2) = [1] x1 + [1] x2 + [0]
[matrixMult#1](x1, x2) = [1]
[leaf] = [0]
[lineMult](x1, x2, x3) = [2]
[lineMult#2](x1, x2, x3, x4) = [2] x4 + [0]
[#pos](x1) = [0]
[#add](x1, x2) = [0]
[node](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [7]
[dequeue](x1, x2) = [1] x1 + [1] x2 + [4]
[tuple#2](x1, x2) = [1] x1 + [1] x2 + [1]
[nil] = [0]
[computeLine](x1, x2, x3) = [4]
[dequeue#1](x1, x2) = [1] x1 + [1] x2 + [3]
[::](x1, x2) = [1] x1 + [1] x2 + [4]
[#mult](x1, x2) = [0]
[+](x1, x2) = [3] x1 + [0]
[#succ](x1) = [0]
[#0] = [0]
[enqueue#1](x1, x2) = [1] x1 + [1] x2 + [4]
[#neg](x1) = [0]
[matrixMult](x1, x2) = [1]
[*](x1, x2) = [2]
[enqueue](x1, x2) = [1] x1 + [1] x2 + [4]
[dequeue#2](x1) = [1] x1 + [3]
[#pred](x1) = [0]
[lineMult#1](x1, x2, x3) = [0]
[#s](x1) = [0]
[computeLine#2](x1, x2, x3, x4) = [0]
[bftMult'#2^#](x1) = [0]
[bftMult'#5^#](x1, x2, x3) = [1] x1 + [3]
[bftMult'^#](x1, x2) = [1] x1 + [3]
[matrixMult^#](x1, x2) = [0]
[bftMult'#3^#](x1, x2, x3) = [1] x1 + [1] x3 + [1]
[bftMult'#4^#](x1, x2, x3) = [1] x1 + [1] x3 + [4]
[bftMult'#1^#](x1, x2) = [1] x1 + [0]
[c_5](x1, x2) = [1] x1 + [1] x2 + [0]
[c_6](x1, x2) = [1] x1 + [1] x2 + [0]
[c_11](x1) = [1] x1 + [0]
[c_12](x1) = [1] x1 + [0]
[c_13](x1) = [1] x1 + [0]
[c_22](x1) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[bftMult'#2(tuple#2(@dequeue@1, @dequeue@2))] = [1] @dequeue@1 + [1] @dequeue@2 + [4]
>= [1] @dequeue@1 + [1] @dequeue@2 + [4]
= [dequeue(@dequeue@1, @dequeue@2)]
[#natmult(#0(), @y)] = [0]
>= [0]
= [#0()]
[#natmult(#s(@x), @y)] = [0]
>= [0]
= [#add(#pos(@y), #natmult(@x, @y))]
[reverse(@xs)] = [1] @xs + [0]
>= [1] @xs + [0]
= [appendreverse(@xs, nil())]
[appendreverse#1(nil(), @sofar)] = [1] @sofar + [0]
>= [1] @sofar + [0]
= [@sofar]
[appendreverse#1(::(@a, @as), @sofar)] = [1] @sofar + [1] @a + [1] @as + [4]
>= [1] @sofar + [1] @a + [1] @as + [4]
= [appendreverse(@as, ::(@a, @sofar))]
[computeLine#1(nil(), @acc, @m)] = [3] @acc + [0]
>= [1] @acc + [0]
= [@acc]
[computeLine#1(::(@x, @xs), @acc, @m)] = [3] @acc + [0]
>= [0]
= [computeLine#2(@m, @acc, @x, @xs)]
[appendreverse(@toreverse, @sofar)] = [1] @toreverse + [1] @sofar + [0]
>= [1] @toreverse + [1] @sofar + [0]
= [appendreverse#1(@toreverse, @sofar)]
[matrixMult#1(nil(), @m2)] = [1]
> [0]
= [nil()]
[matrixMult#1(::(@l, @ls), @m2)] = [1]
? [9]
= [::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))]
[lineMult(@n, @l1, @l2)] = [2]
> [0]
= [lineMult#1(@l1, @l2, @n)]
[lineMult#2(nil(), @n, @x, @xs)] = [2] @xs + [0]
? [8]
= [::(*(@x, @n), lineMult(@n, @xs, nil()))]
[lineMult#2(::(@y, @ys), @n, @x, @xs)] = [2] @xs + [0]
? [12]
= [::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))]
[#add(#pos(#s(#0())), @y)] = [0]
>= [0]
= [#succ(@y)]
[#add(#pos(#s(#s(@x))), @y)] = [0]
>= [0]
= [#succ(#add(#pos(#s(@x)), @y))]
[#add(#0(), @y)] = [0]
? [1] @y + [0]
= [@y]
[#add(#neg(#s(#0())), @y)] = [0]
>= [0]
= [#pred(@y)]
[#add(#neg(#s(#s(@x))), @y)] = [0]
>= [0]
= [#pred(#add(#pos(#s(@x)), @y))]
[dequeue(@outq, @inq)] = [1] @outq + [1] @inq + [4]
> [1] @outq + [1] @inq + [3]
= [dequeue#1(@outq, @inq)]
[computeLine(@line, @m, @acc)] = [4]
? [3] @acc + [0]
= [computeLine#1(@line, @acc, @m)]
[dequeue#1(nil(), @inq)] = [1] @inq + [3]
>= [1] @inq + [3]
= [dequeue#2(reverse(@inq))]
[dequeue#1(::(@t, @ts), @inq)] = [1] @t + [1] @inq + [1] @ts + [7]
> [1] @t + [1] @inq + [1] @ts + [6]
= [tuple#2(::(@t, nil()), tuple#2(@ts, @inq))]
[#mult(#pos(@x), #pos(@y))] = [0]
>= [0]
= [#pos(#natmult(@x, @y))]
[#mult(#pos(@x), #0())] = [0]
>= [0]
= [#0()]
[#mult(#pos(@x), #neg(@y))] = [0]
>= [0]
= [#neg(#natmult(@x, @y))]
[#mult(#0(), #pos(@y))] = [0]
>= [0]
= [#0()]
[#mult(#0(), #0())] = [0]
>= [0]
= [#0()]
[#mult(#0(), #neg(@y))] = [0]
>= [0]
= [#0()]
[#mult(#neg(@x), #pos(@y))] = [0]
>= [0]
= [#neg(#natmult(@x, @y))]
[#mult(#neg(@x), #0())] = [0]
>= [0]
= [#0()]
[#mult(#neg(@x), #neg(@y))] = [0]
>= [0]
= [#pos(#natmult(@x, @y))]
[+(@x, @y)] = [3] @x + [0]
>= [0]
= [#add(@x, @y)]
[#succ(#pos(#s(@x)))] = [0]
>= [0]
= [#pos(#s(#s(@x)))]
[#succ(#0())] = [0]
>= [0]
= [#pos(#s(#0()))]
[#succ(#neg(#s(#0())))] = [0]
>= [0]
= [#0()]
[#succ(#neg(#s(#s(@x))))] = [0]
>= [0]
= [#neg(#s(@x))]
[enqueue#1(tuple#2(@outq, @inq), @t)] = [1] @t + [1] @outq + [1] @inq + [5]
>= [1] @t + [1] @outq + [1] @inq + [5]
= [tuple#2(@outq, ::(@t, @inq))]
[matrixMult(@m1, @m2)] = [1]
>= [1]
= [matrixMult#1(@m1, @m2)]
[*(@x, @y)] = [2]
> [0]
= [#mult(@x, @y)]
[enqueue(@t, @queue)] = [1] @t + [1] @queue + [4]
>= [1] @t + [1] @queue + [4]
= [enqueue#1(@queue, @t)]
[dequeue#2(nil())] = [3]
> [2]
= [tuple#2(nil(), tuple#2(nil(), nil()))]
[dequeue#2(::(@t, @ts))] = [1] @t + [1] @ts + [7]
> [1] @t + [1] @ts + [6]
= [tuple#2(::(@t, nil()), tuple#2(@ts, nil()))]
[#pred(#pos(#s(#0())))] = [0]
>= [0]
= [#0()]
[#pred(#pos(#s(#s(@x))))] = [0]
>= [0]
= [#pos(#s(@x))]
[#pred(#0())] = [0]
>= [0]
= [#neg(#s(#0()))]
[#pred(#neg(#s(@x)))] = [0]
>= [0]
= [#neg(#s(#s(@x)))]
[lineMult#1(nil(), @l2, @n)] = [0]
>= [0]
= [nil()]
[lineMult#1(::(@x, @xs), @l2, @n)] = [0]
? [2] @xs + [0]
= [lineMult#2(@l2, @n, @x, @xs)]
[computeLine#2(nil(), @acc, @x, @xs)] = [0]
>= [0]
= [nil()]
[computeLine#2(::(@l, @ls), @acc, @x, @xs)] = [0]
? [4]
= [computeLine(@xs, @ls, lineMult(@x, @l, @acc))]
[bftMult'#5^#(@queue', @acc, @y)] = [1] @queue' + [3]
>= [1] @queue' + [3]
= [c_5(bftMult'^#(@queue', matrixMult(@acc, @y)),
matrixMult^#(@acc, @y))]
[bftMult'^#(@queue, @acc)] = [1] @queue + [3]
>= [1] @queue + [3]
= [c_6(bftMult'#1^#(bftMult'#2(@queue), @acc), bftMult'#2^#(@queue))]
[bftMult'#3^#(::(@t, @_@3), @acc, @queue)] = [1] @t + [1] @queue + [1] @_@3 + [5]
> [1] @t + [1] @queue + [4]
= [c_11(bftMult'#4^#(@t, @acc, @queue))]
[bftMult'#4^#(leaf(), @acc, @queue)] = [1] @queue + [4]
> [1] @queue + [3]
= [c_12(bftMult'^#(@queue, @acc))]
[bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue)] = [1] @y + [1] @queue + [1] @t1 + [1] @t2 + [11]
>= [1] @queue + [1] @t1 + [1] @t2 + [11]
= [c_13(bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y))]
[bftMult'#1^#(tuple#2(@elem, @queue), @acc)] = [1] @queue + [1] @elem + [1]
>= [1] @queue + [1] @elem + [1]
= [c_22(bftMult'#3^#(@elem, @acc, @queue))]
We return to the main proof. Consider the set of all dependency
pairs
:
{ 1: bftMult'#5^#(@queue', @acc, @y) ->
c_5(bftMult'^#(@queue', matrixMult(@acc, @y)),
matrixMult^#(@acc, @y))
, 2: bftMult'^#(@queue, @acc) ->
c_6(bftMult'#1^#(bftMult'#2(@queue), @acc), bftMult'#2^#(@queue))
, 3: bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
c_11(bftMult'#4^#(@t, @acc, @queue))
, 4: bftMult'#4^#(leaf(), @acc, @queue) ->
c_12(bftMult'^#(@queue, @acc))
, 5: bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
c_13(bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y))
, 6: bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
c_22(bftMult'#3^#(@elem, @acc, @queue)) }
Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of dependency
pairs {3,4}. These cover all (indirect) predecessors of dependency
pairs {1,2,3,4,5,6}, their number of application is equally
bounded. The dependency pairs are shifted into the weak component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak DPs:
{ bftMult'#5^#(@queue', @acc, @y) ->
c_5(bftMult'^#(@queue', matrixMult(@acc, @y)),
matrixMult^#(@acc, @y))
, bftMult'^#(@queue, @acc) ->
c_6(bftMult'#1^#(bftMult'#2(@queue), @acc), bftMult'#2^#(@queue))
, bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
c_11(bftMult'#4^#(@t, @acc, @queue))
, bftMult'#4^#(leaf(), @acc, @queue) ->
c_12(bftMult'^#(@queue, @acc))
, bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
c_13(bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y))
, bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
c_22(bftMult'#3^#(@elem, @acc, @queue)) }
Weak Trs:
{ bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) ->
dequeue(@dequeue@1, @dequeue@2)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
, reverse(@xs) -> appendreverse(@xs, nil())
, appendreverse#1(nil(), @sofar) -> @sofar
, appendreverse#1(::(@a, @as), @sofar) ->
appendreverse(@as, ::(@a, @sofar))
, computeLine#1(nil(), @acc, @m) -> @acc
, computeLine#1(::(@x, @xs), @acc, @m) ->
computeLine#2(@m, @acc, @x, @xs)
, appendreverse(@toreverse, @sofar) ->
appendreverse#1(@toreverse, @sofar)
, matrixMult#1(nil(), @m2) -> nil()
, matrixMult#1(::(@l, @ls), @m2) ->
::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, dequeue(@outq, @inq) -> dequeue#1(@outq, @inq)
, computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m)
, dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq))
, dequeue#1(::(@t, @ts), @inq) ->
tuple#2(::(@t, nil()), tuple#2(@ts, @inq))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, +(@x, @y) -> #add(@x, @y)
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, enqueue#1(tuple#2(@outq, @inq), @t) ->
tuple#2(@outq, ::(@t, @inq))
, matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2)
, *(@x, @y) -> #mult(@x, @y)
, enqueue(@t, @queue) -> enqueue#1(@queue, @t)
, dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil()))
, dequeue#2(::(@t, @ts)) ->
tuple#2(::(@t, nil()), tuple#2(@ts, nil()))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, lineMult#1(nil(), @l2, @n) -> nil()
, lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, computeLine#2(nil(), @acc, @x, @xs) -> nil()
, computeLine#2(::(@l, @ls), @acc, @x, @xs) ->
computeLine(@xs, @ls, lineMult(@x, @l, @acc)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ bftMult'#5^#(@queue', @acc, @y) ->
c_5(bftMult'^#(@queue', matrixMult(@acc, @y)),
matrixMult^#(@acc, @y))
, bftMult'^#(@queue, @acc) ->
c_6(bftMult'#1^#(bftMult'#2(@queue), @acc), bftMult'#2^#(@queue))
, bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
c_11(bftMult'#4^#(@t, @acc, @queue))
, bftMult'#4^#(leaf(), @acc, @queue) ->
c_12(bftMult'^#(@queue, @acc))
, bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
c_13(bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y))
, bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
c_22(bftMult'#3^#(@elem, @acc, @queue)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) ->
dequeue(@dequeue@1, @dequeue@2)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
, reverse(@xs) -> appendreverse(@xs, nil())
, appendreverse#1(nil(), @sofar) -> @sofar
, appendreverse#1(::(@a, @as), @sofar) ->
appendreverse(@as, ::(@a, @sofar))
, computeLine#1(nil(), @acc, @m) -> @acc
, computeLine#1(::(@x, @xs), @acc, @m) ->
computeLine#2(@m, @acc, @x, @xs)
, appendreverse(@toreverse, @sofar) ->
appendreverse#1(@toreverse, @sofar)
, matrixMult#1(nil(), @m2) -> nil()
, matrixMult#1(::(@l, @ls), @m2) ->
::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, dequeue(@outq, @inq) -> dequeue#1(@outq, @inq)
, computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m)
, dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq))
, dequeue#1(::(@t, @ts), @inq) ->
tuple#2(::(@t, nil()), tuple#2(@ts, @inq))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, +(@x, @y) -> #add(@x, @y)
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, enqueue#1(tuple#2(@outq, @inq), @t) ->
tuple#2(@outq, ::(@t, @inq))
, matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2)
, *(@x, @y) -> #mult(@x, @y)
, enqueue(@t, @queue) -> enqueue#1(@queue, @t)
, dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil()))
, dequeue#2(::(@t, @ts)) ->
tuple#2(::(@t, nil()), tuple#2(@ts, nil()))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, lineMult#1(nil(), @l2, @n) -> nil()
, lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, computeLine#2(nil(), @acc, @x, @xs) -> nil()
, computeLine#2(::(@l, @ls), @acc, @x, @xs) ->
computeLine(@xs, @ls, lineMult(@x, @l, @acc)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
No rule is usable, rules are removed from the input problem.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Rules: Empty
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ bftMult'#2^#(tuple#2(@dequeue@1, @dequeue@2)) ->
c_1(dequeue^#(@dequeue@1, @dequeue@2))
, dequeue^#(@outq, @inq) -> c_2(dequeue#1^#(@outq, @inq))
, reverse^#(@xs) -> c_3(appendreverse^#(@xs, nil()))
, appendreverse^#(@toreverse, @sofar) ->
c_4(appendreverse#1^#(@toreverse, @sofar))
, matrixMult^#(@m1, @m2) -> c_7(matrixMult#1^#(@m1, @m2))
, appendreverse#1^#(::(@a, @as), @sofar) ->
c_8(appendreverse^#(@as, ::(@a, @sofar)))
, computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_9(computeLine#2^#(@m, @acc, @x, @xs))
, computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_10(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, matrixMult#1^#(::(@l, @ls), @m2) ->
c_14(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, computeLine^#(@line, @m, @acc) ->
c_15(computeLine#1^#(@line, @acc, @m))
, lineMult^#(@n, @l1, @l2) -> c_17(lineMult#1^#(@l1, @l2, @n))
, lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_18(lineMult#2^#(@l2, @n, @x, @xs))
, lineMult#2^#(nil(), @n, @x, @xs) ->
c_19(lineMult^#(@n, @xs, nil()))
, lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_20(lineMult^#(@n, @xs, @ys))
, dequeue#1^#(nil(), @inq) -> c_21(reverse^#(@inq)) }
Weak DPs:
{ bftMult'#5^#(@queue', @acc, @y) ->
bftMult'^#(@queue', matrixMult(@acc, @y))
, bftMult'#5^#(@queue', @acc, @y) -> matrixMult^#(@acc, @y)
, bftMult'^#(@queue, @acc) -> bftMult'#2^#(@queue)
, bftMult'^#(@queue, @acc) ->
bftMult'#1^#(bftMult'#2(@queue), @acc)
, bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
bftMult'#4^#(@t, @acc, @queue)
, bftMult'#4^#(leaf(), @acc, @queue) -> bftMult'^#(@queue, @acc)
, bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)
, bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
bftMult'#3^#(@elem, @acc, @queue) }
Weak Trs:
{ bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) ->
dequeue(@dequeue@1, @dequeue@2)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
, reverse(@xs) -> appendreverse(@xs, nil())
, appendreverse#1(nil(), @sofar) -> @sofar
, appendreverse#1(::(@a, @as), @sofar) ->
appendreverse(@as, ::(@a, @sofar))
, computeLine#1(nil(), @acc, @m) -> @acc
, computeLine#1(::(@x, @xs), @acc, @m) ->
computeLine#2(@m, @acc, @x, @xs)
, appendreverse(@toreverse, @sofar) ->
appendreverse#1(@toreverse, @sofar)
, matrixMult#1(nil(), @m2) -> nil()
, matrixMult#1(::(@l, @ls), @m2) ->
::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, dequeue(@outq, @inq) -> dequeue#1(@outq, @inq)
, computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m)
, dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq))
, dequeue#1(::(@t, @ts), @inq) ->
tuple#2(::(@t, nil()), tuple#2(@ts, @inq))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, +(@x, @y) -> #add(@x, @y)
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, enqueue#1(tuple#2(@outq, @inq), @t) ->
tuple#2(@outq, ::(@t, @inq))
, matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2)
, *(@x, @y) -> #mult(@x, @y)
, enqueue(@t, @queue) -> enqueue#1(@queue, @t)
, dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil()))
, dequeue#2(::(@t, @ts)) ->
tuple#2(::(@t, nil()), tuple#2(@ts, nil()))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, lineMult#1(nil(), @l2, @n) -> nil()
, lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, computeLine#2(nil(), @acc, @x, @xs) -> nil()
, computeLine#2(::(@l, @ls), @acc, @x, @xs) ->
computeLine(@xs, @ls, lineMult(@x, @l, @acc)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
DPs:
{ 3: reverse^#(@xs) -> c_3(appendreverse^#(@xs, nil()))
, 6: appendreverse#1^#(::(@a, @as), @sofar) ->
c_8(appendreverse^#(@as, ::(@a, @sofar)))
, 17: bftMult'#5^#(@queue', @acc, @y) -> matrixMult^#(@acc, @y)
, 18: bftMult'^#(@queue, @acc) -> bftMult'#2^#(@queue)
, 19: bftMult'^#(@queue, @acc) ->
bftMult'#1^#(bftMult'#2(@queue), @acc) }
Trs:
{ computeLine#1(nil(), @acc, @m) -> @acc
, matrixMult#1(nil(), @m2) -> nil()
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, +(@x, @y) -> #add(@x, @y)
, enqueue(@t, @queue) -> enqueue#1(@queue, @t)
, lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, computeLine#2(nil(), @acc, @x, @xs) -> nil() }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1},
Uargs(c_4) = {1}, Uargs(c_7) = {1}, Uargs(c_8) = {1},
Uargs(c_9) = {1}, Uargs(c_10) = {1, 2}, Uargs(c_14) = {1, 2},
Uargs(c_15) = {1}, Uargs(c_17) = {1}, Uargs(c_18) = {1},
Uargs(c_19) = {1}, Uargs(c_20) = {1}, Uargs(c_21) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[bftMult'#2](x1) = [1] x1 + [2]
[#natmult](x1, x2) = [0]
[reverse](x1) = [1] x1 + [0]
[appendreverse#1](x1, x2) = [1] x1 + [1] x2 + [0]
[computeLine#1](x1, x2, x3) = [7] x2 + [1]
[appendreverse](x1, x2) = [1] x1 + [1] x2 + [0]
[matrixMult#1](x1, x2) = [3]
[leaf] = [0]
[lineMult](x1, x2, x3) = [4] x2 + [1] x3 + [0]
[lineMult#2](x1, x2, x3, x4) = [1] x1 + [4] x4 + [3]
[#pos](x1) = [0]
[#add](x1, x2) = [1] x2 + [0]
[node](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [4]
[dequeue](x1, x2) = [1] x1 + [1] x2 + [4]
[tuple#2](x1, x2) = [1] x1 + [1] x2 + [2]
[nil] = [0]
[computeLine](x1, x2, x3) = [1] x2 + [1] x3 + [6]
[dequeue#1](x1, x2) = [1] x1 + [1] x2 + [4]
[::](x1, x2) = [1] x1 + [1] x2 + [1]
[#mult](x1, x2) = [0]
[+](x1, x2) = [1] x2 + [2]
[#succ](x1) = [0]
[#0] = [0]
[enqueue#1](x1, x2) = [1] x1 + [1] x2 + [1]
[#neg](x1) = [0]
[matrixMult](x1, x2) = [0]
[*](x1, x2) = [0]
[enqueue](x1, x2) = [1] x1 + [1] x2 + [2]
[dequeue#2](x1) = [1] x1 + [4]
[#pred](x1) = [0]
[lineMult#1](x1, x2, x3) = [4] x1 + [1] x2 + [0]
[#s](x1) = [0]
[computeLine#2](x1, x2, x3, x4) = [1] x2 + [7]
[bftMult'#2^#](x1) = [1] x1 + [4]
[dequeue^#](x1, x2) = [1] x2 + [6]
[reverse^#](x1) = [1] x1 + [6]
[appendreverse^#](x1, x2) = [1] x1 + [0]
[bftMult'#5^#](x1, x2, x3) = [2] x1 + [7]
[bftMult'^#](x1, x2) = [2] x1 + [7]
[matrixMult^#](x1, x2) = [0]
[appendreverse#1^#](x1, x2) = [1] x1 + [0]
[computeLine#1^#](x1, x2, x3) = [0]
[computeLine#2^#](x1, x2, x3, x4) = [0]
[bftMult'#3^#](x1, x2, x3) = [2] x1 + [2] x3 + [5]
[bftMult'#4^#](x1, x2, x3) = [2] x1 + [2] x3 + [7]
[matrixMult#1^#](x1, x2) = [0]
[computeLine^#](x1, x2, x3) = [0]
[lineMult^#](x1, x2, x3) = [0]
[lineMult#1^#](x1, x2, x3) = [0]
[lineMult#2^#](x1, x2, x3, x4) = [0]
[dequeue#1^#](x1, x2) = [1] x2 + [6]
[bftMult'#1^#](x1, x2) = [2] x1 + [1]
[c_1](x1) = [1] x1 + [0]
[c_2](x1) = [1] x1 + [0]
[c_3](x1) = [1] x1 + [0]
[c_4](x1) = [1] x1 + [0]
[c_7](x1) = [2] x1 + [0]
[c_8](x1) = [1] x1 + [0]
[c_9](x1) = [1] x1 + [0]
[c_10](x1, x2) = [1] x1 + [1] x2 + [0]
[c_14](x1, x2) = [1] x1 + [1] x2 + [0]
[c_15](x1) = [1] x1 + [0]
[c_17](x1) = [1] x1 + [0]
[c_18](x1) = [1] x1 + [0]
[c_19](x1) = [1] x1 + [0]
[c_20](x1) = [1] x1 + [0]
[c_21](x1) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[bftMult'#2(tuple#2(@dequeue@1, @dequeue@2))] = [1] @dequeue@1 + [1] @dequeue@2 + [4]
>= [1] @dequeue@1 + [1] @dequeue@2 + [4]
= [dequeue(@dequeue@1, @dequeue@2)]
[#natmult(#0(), @y)] = [0]
>= [0]
= [#0()]
[#natmult(#s(@x), @y)] = [0]
>= [0]
= [#add(#pos(@y), #natmult(@x, @y))]
[reverse(@xs)] = [1] @xs + [0]
>= [1] @xs + [0]
= [appendreverse(@xs, nil())]
[appendreverse#1(nil(), @sofar)] = [1] @sofar + [0]
>= [1] @sofar + [0]
= [@sofar]
[appendreverse#1(::(@a, @as), @sofar)] = [1] @sofar + [1] @a + [1] @as + [1]
>= [1] @sofar + [1] @a + [1] @as + [1]
= [appendreverse(@as, ::(@a, @sofar))]
[computeLine#1(nil(), @acc, @m)] = [7] @acc + [1]
> [1] @acc + [0]
= [@acc]
[computeLine#1(::(@x, @xs), @acc, @m)] = [7] @acc + [1]
? [1] @acc + [7]
= [computeLine#2(@m, @acc, @x, @xs)]
[appendreverse(@toreverse, @sofar)] = [1] @toreverse + [1] @sofar + [0]
>= [1] @toreverse + [1] @sofar + [0]
= [appendreverse#1(@toreverse, @sofar)]
[matrixMult#1(nil(), @m2)] = [3]
> [0]
= [nil()]
[matrixMult#1(::(@l, @ls), @m2)] = [3]
? [1] @m2 + [7]
= [::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))]
[lineMult(@n, @l1, @l2)] = [4] @l1 + [1] @l2 + [0]
>= [4] @l1 + [1] @l2 + [0]
= [lineMult#1(@l1, @l2, @n)]
[lineMult#2(nil(), @n, @x, @xs)] = [4] @xs + [3]
> [4] @xs + [1]
= [::(*(@x, @n), lineMult(@n, @xs, nil()))]
[lineMult#2(::(@y, @ys), @n, @x, @xs)] = [1] @y + [4] @xs + [1] @ys + [4]
> [1] @y + [4] @xs + [1] @ys + [3]
= [::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))]
[#add(#pos(#s(#0())), @y)] = [1] @y + [0]
>= [0]
= [#succ(@y)]
[#add(#pos(#s(#s(@x))), @y)] = [1] @y + [0]
>= [0]
= [#succ(#add(#pos(#s(@x)), @y))]
[#add(#0(), @y)] = [1] @y + [0]
>= [1] @y + [0]
= [@y]
[#add(#neg(#s(#0())), @y)] = [1] @y + [0]
>= [0]
= [#pred(@y)]
[#add(#neg(#s(#s(@x))), @y)] = [1] @y + [0]
>= [0]
= [#pred(#add(#pos(#s(@x)), @y))]
[dequeue(@outq, @inq)] = [1] @outq + [1] @inq + [4]
>= [1] @outq + [1] @inq + [4]
= [dequeue#1(@outq, @inq)]
[computeLine(@line, @m, @acc)] = [1] @acc + [1] @m + [6]
? [7] @acc + [1]
= [computeLine#1(@line, @acc, @m)]
[dequeue#1(nil(), @inq)] = [1] @inq + [4]
>= [1] @inq + [4]
= [dequeue#2(reverse(@inq))]
[dequeue#1(::(@t, @ts), @inq)] = [1] @t + [1] @inq + [1] @ts + [5]
>= [1] @t + [1] @inq + [1] @ts + [5]
= [tuple#2(::(@t, nil()), tuple#2(@ts, @inq))]
[#mult(#pos(@x), #pos(@y))] = [0]
>= [0]
= [#pos(#natmult(@x, @y))]
[#mult(#pos(@x), #0())] = [0]
>= [0]
= [#0()]
[#mult(#pos(@x), #neg(@y))] = [0]
>= [0]
= [#neg(#natmult(@x, @y))]
[#mult(#0(), #pos(@y))] = [0]
>= [0]
= [#0()]
[#mult(#0(), #0())] = [0]
>= [0]
= [#0()]
[#mult(#0(), #neg(@y))] = [0]
>= [0]
= [#0()]
[#mult(#neg(@x), #pos(@y))] = [0]
>= [0]
= [#neg(#natmult(@x, @y))]
[#mult(#neg(@x), #0())] = [0]
>= [0]
= [#0()]
[#mult(#neg(@x), #neg(@y))] = [0]
>= [0]
= [#pos(#natmult(@x, @y))]
[+(@x, @y)] = [1] @y + [2]
> [1] @y + [0]
= [#add(@x, @y)]
[#succ(#pos(#s(@x)))] = [0]
>= [0]
= [#pos(#s(#s(@x)))]
[#succ(#0())] = [0]
>= [0]
= [#pos(#s(#0()))]
[#succ(#neg(#s(#0())))] = [0]
>= [0]
= [#0()]
[#succ(#neg(#s(#s(@x))))] = [0]
>= [0]
= [#neg(#s(@x))]
[enqueue#1(tuple#2(@outq, @inq), @t)] = [1] @t + [1] @outq + [1] @inq + [3]
>= [1] @t + [1] @outq + [1] @inq + [3]
= [tuple#2(@outq, ::(@t, @inq))]
[matrixMult(@m1, @m2)] = [0]
? [3]
= [matrixMult#1(@m1, @m2)]
[*(@x, @y)] = [0]
>= [0]
= [#mult(@x, @y)]
[enqueue(@t, @queue)] = [1] @t + [1] @queue + [2]
> [1] @t + [1] @queue + [1]
= [enqueue#1(@queue, @t)]
[dequeue#2(nil())] = [4]
>= [4]
= [tuple#2(nil(), tuple#2(nil(), nil()))]
[dequeue#2(::(@t, @ts))] = [1] @t + [1] @ts + [5]
>= [1] @t + [1] @ts + [5]
= [tuple#2(::(@t, nil()), tuple#2(@ts, nil()))]
[#pred(#pos(#s(#0())))] = [0]
>= [0]
= [#0()]
[#pred(#pos(#s(#s(@x))))] = [0]
>= [0]
= [#pos(#s(@x))]
[#pred(#0())] = [0]
>= [0]
= [#neg(#s(#0()))]
[#pred(#neg(#s(@x)))] = [0]
>= [0]
= [#neg(#s(#s(@x)))]
[lineMult#1(nil(), @l2, @n)] = [1] @l2 + [0]
>= [0]
= [nil()]
[lineMult#1(::(@x, @xs), @l2, @n)] = [4] @x + [4] @xs + [1] @l2 + [4]
> [4] @xs + [1] @l2 + [3]
= [lineMult#2(@l2, @n, @x, @xs)]
[computeLine#2(nil(), @acc, @x, @xs)] = [1] @acc + [7]
> [0]
= [nil()]
[computeLine#2(::(@l, @ls), @acc, @x, @xs)] = [1] @acc + [7]
? [1] @acc + [4] @l + [1] @ls + [6]
= [computeLine(@xs, @ls, lineMult(@x, @l, @acc))]
[bftMult'#2^#(tuple#2(@dequeue@1, @dequeue@2))] = [1] @dequeue@1 + [1] @dequeue@2 + [6]
>= [1] @dequeue@2 + [6]
= [c_1(dequeue^#(@dequeue@1, @dequeue@2))]
[dequeue^#(@outq, @inq)] = [1] @inq + [6]
>= [1] @inq + [6]
= [c_2(dequeue#1^#(@outq, @inq))]
[reverse^#(@xs)] = [1] @xs + [6]
> [1] @xs + [0]
= [c_3(appendreverse^#(@xs, nil()))]
[appendreverse^#(@toreverse, @sofar)] = [1] @toreverse + [0]
>= [1] @toreverse + [0]
= [c_4(appendreverse#1^#(@toreverse, @sofar))]
[bftMult'#5^#(@queue', @acc, @y)] = [2] @queue' + [7]
>= [2] @queue' + [7]
= [bftMult'^#(@queue', matrixMult(@acc, @y))]
[bftMult'#5^#(@queue', @acc, @y)] = [2] @queue' + [7]
> [0]
= [matrixMult^#(@acc, @y)]
[bftMult'^#(@queue, @acc)] = [2] @queue + [7]
> [1] @queue + [4]
= [bftMult'#2^#(@queue)]
[bftMult'^#(@queue, @acc)] = [2] @queue + [7]
> [2] @queue + [5]
= [bftMult'#1^#(bftMult'#2(@queue), @acc)]
[matrixMult^#(@m1, @m2)] = [0]
>= [0]
= [c_7(matrixMult#1^#(@m1, @m2))]
[appendreverse#1^#(::(@a, @as), @sofar)] = [1] @a + [1] @as + [1]
> [1] @as + [0]
= [c_8(appendreverse^#(@as, ::(@a, @sofar)))]
[computeLine#1^#(::(@x, @xs), @acc, @m)] = [0]
>= [0]
= [c_9(computeLine#2^#(@m, @acc, @x, @xs))]
[computeLine#2^#(::(@l, @ls), @acc, @x, @xs)] = [0]
>= [0]
= [c_10(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))]
[bftMult'#3^#(::(@t, @_@3), @acc, @queue)] = [2] @t + [2] @queue + [2] @_@3 + [7]
>= [2] @t + [2] @queue + [7]
= [bftMult'#4^#(@t, @acc, @queue)]
[bftMult'#4^#(leaf(), @acc, @queue)] = [2] @queue + [7]
>= [2] @queue + [7]
= [bftMult'^#(@queue, @acc)]
[bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue)] = [2] @y + [2] @queue + [2] @t1 + [2] @t2 + [15]
>= [2] @queue + [2] @t1 + [2] @t2 + [15]
= [bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)]
[matrixMult#1^#(::(@l, @ls), @m2)] = [0]
>= [0]
= [c_14(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))]
[computeLine^#(@line, @m, @acc)] = [0]
>= [0]
= [c_15(computeLine#1^#(@line, @acc, @m))]
[lineMult^#(@n, @l1, @l2)] = [0]
>= [0]
= [c_17(lineMult#1^#(@l1, @l2, @n))]
[lineMult#1^#(::(@x, @xs), @l2, @n)] = [0]
>= [0]
= [c_18(lineMult#2^#(@l2, @n, @x, @xs))]
[lineMult#2^#(nil(), @n, @x, @xs)] = [0]
>= [0]
= [c_19(lineMult^#(@n, @xs, nil()))]
[lineMult#2^#(::(@y, @ys), @n, @x, @xs)] = [0]
>= [0]
= [c_20(lineMult^#(@n, @xs, @ys))]
[dequeue#1^#(nil(), @inq)] = [1] @inq + [6]
>= [1] @inq + [6]
= [c_21(reverse^#(@inq))]
[bftMult'#1^#(tuple#2(@elem, @queue), @acc)] = [2] @queue + [2] @elem + [5]
>= [2] @queue + [2] @elem + [5]
= [bftMult'#3^#(@elem, @acc, @queue)]
We return to the main proof. Consider the set of all dependency
pairs
:
{ 1: bftMult'#2^#(tuple#2(@dequeue@1, @dequeue@2)) ->
c_1(dequeue^#(@dequeue@1, @dequeue@2))
, 2: dequeue^#(@outq, @inq) -> c_2(dequeue#1^#(@outq, @inq))
, 3: reverse^#(@xs) -> c_3(appendreverse^#(@xs, nil()))
, 4: appendreverse^#(@toreverse, @sofar) ->
c_4(appendreverse#1^#(@toreverse, @sofar))
, 5: matrixMult^#(@m1, @m2) -> c_7(matrixMult#1^#(@m1, @m2))
, 6: appendreverse#1^#(::(@a, @as), @sofar) ->
c_8(appendreverse^#(@as, ::(@a, @sofar)))
, 7: computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_9(computeLine#2^#(@m, @acc, @x, @xs))
, 8: computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_10(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, 9: matrixMult#1^#(::(@l, @ls), @m2) ->
c_14(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, 10: computeLine^#(@line, @m, @acc) ->
c_15(computeLine#1^#(@line, @acc, @m))
, 11: lineMult^#(@n, @l1, @l2) -> c_17(lineMult#1^#(@l1, @l2, @n))
, 12: lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_18(lineMult#2^#(@l2, @n, @x, @xs))
, 13: lineMult#2^#(nil(), @n, @x, @xs) ->
c_19(lineMult^#(@n, @xs, nil()))
, 14: lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_20(lineMult^#(@n, @xs, @ys))
, 15: dequeue#1^#(nil(), @inq) -> c_21(reverse^#(@inq))
, 16: bftMult'#5^#(@queue', @acc, @y) ->
bftMult'^#(@queue', matrixMult(@acc, @y))
, 17: bftMult'#5^#(@queue', @acc, @y) -> matrixMult^#(@acc, @y)
, 18: bftMult'^#(@queue, @acc) -> bftMult'#2^#(@queue)
, 19: bftMult'^#(@queue, @acc) ->
bftMult'#1^#(bftMult'#2(@queue), @acc)
, 20: bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
bftMult'#4^#(@t, @acc, @queue)
, 21: bftMult'#4^#(leaf(), @acc, @queue) ->
bftMult'^#(@queue, @acc)
, 22: bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)
, 23: bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
bftMult'#3^#(@elem, @acc, @queue) }
Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of dependency
pairs {3,6,17,18,19}. These cover all (indirect) predecessors of
dependency pairs {1,2,3,4,6,15,16,17,18,19,20,21,22,23}, their
number of application is equally bounded. The dependency pairs are
shifted into the weak component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ matrixMult^#(@m1, @m2) -> c_7(matrixMult#1^#(@m1, @m2))
, computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_9(computeLine#2^#(@m, @acc, @x, @xs))
, computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_10(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, matrixMult#1^#(::(@l, @ls), @m2) ->
c_14(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, computeLine^#(@line, @m, @acc) ->
c_15(computeLine#1^#(@line, @acc, @m))
, lineMult^#(@n, @l1, @l2) -> c_17(lineMult#1^#(@l1, @l2, @n))
, lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_18(lineMult#2^#(@l2, @n, @x, @xs))
, lineMult#2^#(nil(), @n, @x, @xs) ->
c_19(lineMult^#(@n, @xs, nil()))
, lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_20(lineMult^#(@n, @xs, @ys)) }
Weak DPs:
{ bftMult'#2^#(tuple#2(@dequeue@1, @dequeue@2)) ->
c_1(dequeue^#(@dequeue@1, @dequeue@2))
, dequeue^#(@outq, @inq) -> c_2(dequeue#1^#(@outq, @inq))
, reverse^#(@xs) -> c_3(appendreverse^#(@xs, nil()))
, appendreverse^#(@toreverse, @sofar) ->
c_4(appendreverse#1^#(@toreverse, @sofar))
, bftMult'#5^#(@queue', @acc, @y) ->
bftMult'^#(@queue', matrixMult(@acc, @y))
, bftMult'#5^#(@queue', @acc, @y) -> matrixMult^#(@acc, @y)
, bftMult'^#(@queue, @acc) -> bftMult'#2^#(@queue)
, bftMult'^#(@queue, @acc) ->
bftMult'#1^#(bftMult'#2(@queue), @acc)
, appendreverse#1^#(::(@a, @as), @sofar) ->
c_8(appendreverse^#(@as, ::(@a, @sofar)))
, bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
bftMult'#4^#(@t, @acc, @queue)
, bftMult'#4^#(leaf(), @acc, @queue) -> bftMult'^#(@queue, @acc)
, bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)
, dequeue#1^#(nil(), @inq) -> c_21(reverse^#(@inq))
, bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
bftMult'#3^#(@elem, @acc, @queue) }
Weak Trs:
{ bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) ->
dequeue(@dequeue@1, @dequeue@2)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
, reverse(@xs) -> appendreverse(@xs, nil())
, appendreverse#1(nil(), @sofar) -> @sofar
, appendreverse#1(::(@a, @as), @sofar) ->
appendreverse(@as, ::(@a, @sofar))
, computeLine#1(nil(), @acc, @m) -> @acc
, computeLine#1(::(@x, @xs), @acc, @m) ->
computeLine#2(@m, @acc, @x, @xs)
, appendreverse(@toreverse, @sofar) ->
appendreverse#1(@toreverse, @sofar)
, matrixMult#1(nil(), @m2) -> nil()
, matrixMult#1(::(@l, @ls), @m2) ->
::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, dequeue(@outq, @inq) -> dequeue#1(@outq, @inq)
, computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m)
, dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq))
, dequeue#1(::(@t, @ts), @inq) ->
tuple#2(::(@t, nil()), tuple#2(@ts, @inq))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, +(@x, @y) -> #add(@x, @y)
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, enqueue#1(tuple#2(@outq, @inq), @t) ->
tuple#2(@outq, ::(@t, @inq))
, matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2)
, *(@x, @y) -> #mult(@x, @y)
, enqueue(@t, @queue) -> enqueue#1(@queue, @t)
, dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil()))
, dequeue#2(::(@t, @ts)) ->
tuple#2(::(@t, nil()), tuple#2(@ts, nil()))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, lineMult#1(nil(), @l2, @n) -> nil()
, lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, computeLine#2(nil(), @acc, @x, @xs) -> nil()
, computeLine#2(::(@l, @ls), @acc, @x, @xs) ->
computeLine(@xs, @ls, lineMult(@x, @l, @acc)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ bftMult'#2^#(tuple#2(@dequeue@1, @dequeue@2)) ->
c_1(dequeue^#(@dequeue@1, @dequeue@2))
, dequeue^#(@outq, @inq) -> c_2(dequeue#1^#(@outq, @inq))
, reverse^#(@xs) -> c_3(appendreverse^#(@xs, nil()))
, appendreverse^#(@toreverse, @sofar) ->
c_4(appendreverse#1^#(@toreverse, @sofar))
, bftMult'^#(@queue, @acc) -> bftMult'#2^#(@queue)
, appendreverse#1^#(::(@a, @as), @sofar) ->
c_8(appendreverse^#(@as, ::(@a, @sofar)))
, dequeue#1^#(nil(), @inq) -> c_21(reverse^#(@inq)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ matrixMult^#(@m1, @m2) -> c_7(matrixMult#1^#(@m1, @m2))
, computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_9(computeLine#2^#(@m, @acc, @x, @xs))
, computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_10(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, matrixMult#1^#(::(@l, @ls), @m2) ->
c_14(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, computeLine^#(@line, @m, @acc) ->
c_15(computeLine#1^#(@line, @acc, @m))
, lineMult^#(@n, @l1, @l2) -> c_17(lineMult#1^#(@l1, @l2, @n))
, lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_18(lineMult#2^#(@l2, @n, @x, @xs))
, lineMult#2^#(nil(), @n, @x, @xs) ->
c_19(lineMult^#(@n, @xs, nil()))
, lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_20(lineMult^#(@n, @xs, @ys)) }
Weak DPs:
{ bftMult'#5^#(@queue', @acc, @y) ->
bftMult'^#(@queue', matrixMult(@acc, @y))
, bftMult'#5^#(@queue', @acc, @y) -> matrixMult^#(@acc, @y)
, bftMult'^#(@queue, @acc) ->
bftMult'#1^#(bftMult'#2(@queue), @acc)
, bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
bftMult'#4^#(@t, @acc, @queue)
, bftMult'#4^#(leaf(), @acc, @queue) -> bftMult'^#(@queue, @acc)
, bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)
, bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
bftMult'#3^#(@elem, @acc, @queue) }
Weak Trs:
{ bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) ->
dequeue(@dequeue@1, @dequeue@2)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
, reverse(@xs) -> appendreverse(@xs, nil())
, appendreverse#1(nil(), @sofar) -> @sofar
, appendreverse#1(::(@a, @as), @sofar) ->
appendreverse(@as, ::(@a, @sofar))
, computeLine#1(nil(), @acc, @m) -> @acc
, computeLine#1(::(@x, @xs), @acc, @m) ->
computeLine#2(@m, @acc, @x, @xs)
, appendreverse(@toreverse, @sofar) ->
appendreverse#1(@toreverse, @sofar)
, matrixMult#1(nil(), @m2) -> nil()
, matrixMult#1(::(@l, @ls), @m2) ->
::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, dequeue(@outq, @inq) -> dequeue#1(@outq, @inq)
, computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m)
, dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq))
, dequeue#1(::(@t, @ts), @inq) ->
tuple#2(::(@t, nil()), tuple#2(@ts, @inq))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, +(@x, @y) -> #add(@x, @y)
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, enqueue#1(tuple#2(@outq, @inq), @t) ->
tuple#2(@outq, ::(@t, @inq))
, matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2)
, *(@x, @y) -> #mult(@x, @y)
, enqueue(@t, @queue) -> enqueue#1(@queue, @t)
, dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil()))
, dequeue#2(::(@t, @ts)) ->
tuple#2(::(@t, nil()), tuple#2(@ts, nil()))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, lineMult#1(nil(), @l2, @n) -> nil()
, lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, computeLine#2(nil(), @acc, @x, @xs) -> nil()
, computeLine#2(::(@l, @ls), @acc, @x, @xs) ->
computeLine(@xs, @ls, lineMult(@x, @l, @acc)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We decompose the input problem according to the dependency graph
into the upper component
{ bftMult'#5^#(@queue', @acc, @y) ->
bftMult'^#(@queue', matrixMult(@acc, @y))
, bftMult'#5^#(@queue', @acc, @y) -> matrixMult^#(@acc, @y)
, bftMult'^#(@queue, @acc) ->
bftMult'#1^#(bftMult'#2(@queue), @acc)
, matrixMult^#(@m1, @m2) -> c_7(matrixMult#1^#(@m1, @m2))
, bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
bftMult'#4^#(@t, @acc, @queue)
, bftMult'#4^#(leaf(), @acc, @queue) -> bftMult'^#(@queue, @acc)
, bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)
, matrixMult#1^#(::(@l, @ls), @m2) ->
c_14(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
bftMult'#3^#(@elem, @acc, @queue) }
and lower component
{ computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_9(computeLine#2^#(@m, @acc, @x, @xs))
, computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_10(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, computeLine^#(@line, @m, @acc) ->
c_15(computeLine#1^#(@line, @acc, @m))
, lineMult^#(@n, @l1, @l2) -> c_17(lineMult#1^#(@l1, @l2, @n))
, lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_18(lineMult#2^#(@l2, @n, @x, @xs))
, lineMult#2^#(nil(), @n, @x, @xs) ->
c_19(lineMult^#(@n, @xs, nil()))
, lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_20(lineMult^#(@n, @xs, @ys)) }
Further, following extension rules are added to the lower
component.
{ bftMult'#5^#(@queue', @acc, @y) ->
bftMult'^#(@queue', matrixMult(@acc, @y))
, bftMult'#5^#(@queue', @acc, @y) -> matrixMult^#(@acc, @y)
, bftMult'^#(@queue, @acc) ->
bftMult'#1^#(bftMult'#2(@queue), @acc)
, matrixMult^#(@m1, @m2) -> matrixMult#1^#(@m1, @m2)
, bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
bftMult'#4^#(@t, @acc, @queue)
, bftMult'#4^#(leaf(), @acc, @queue) -> bftMult'^#(@queue, @acc)
, bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)
, matrixMult#1^#(::(@l, @ls), @m2) -> matrixMult^#(@ls, @m2)
, matrixMult#1^#(::(@l, @ls), @m2) -> computeLine^#(@l, @m2, nil())
, bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
bftMult'#3^#(@elem, @acc, @queue) }
TcT solves the upper component with certificate YES(O(1),O(n^1)).
Sub-proof:
----------
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ matrixMult^#(@m1, @m2) -> c_7(matrixMult#1^#(@m1, @m2))
, matrixMult#1^#(::(@l, @ls), @m2) ->
c_14(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2)) }
Weak DPs:
{ bftMult'#5^#(@queue', @acc, @y) ->
bftMult'^#(@queue', matrixMult(@acc, @y))
, bftMult'#5^#(@queue', @acc, @y) -> matrixMult^#(@acc, @y)
, bftMult'^#(@queue, @acc) ->
bftMult'#1^#(bftMult'#2(@queue), @acc)
, bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
bftMult'#4^#(@t, @acc, @queue)
, bftMult'#4^#(leaf(), @acc, @queue) -> bftMult'^#(@queue, @acc)
, bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)
, bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
bftMult'#3^#(@elem, @acc, @queue) }
Weak Trs:
{ bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) ->
dequeue(@dequeue@1, @dequeue@2)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
, reverse(@xs) -> appendreverse(@xs, nil())
, appendreverse#1(nil(), @sofar) -> @sofar
, appendreverse#1(::(@a, @as), @sofar) ->
appendreverse(@as, ::(@a, @sofar))
, computeLine#1(nil(), @acc, @m) -> @acc
, computeLine#1(::(@x, @xs), @acc, @m) ->
computeLine#2(@m, @acc, @x, @xs)
, appendreverse(@toreverse, @sofar) ->
appendreverse#1(@toreverse, @sofar)
, matrixMult#1(nil(), @m2) -> nil()
, matrixMult#1(::(@l, @ls), @m2) ->
::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, dequeue(@outq, @inq) -> dequeue#1(@outq, @inq)
, computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m)
, dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq))
, dequeue#1(::(@t, @ts), @inq) ->
tuple#2(::(@t, nil()), tuple#2(@ts, @inq))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, +(@x, @y) -> #add(@x, @y)
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, enqueue#1(tuple#2(@outq, @inq), @t) ->
tuple#2(@outq, ::(@t, @inq))
, matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2)
, *(@x, @y) -> #mult(@x, @y)
, enqueue(@t, @queue) -> enqueue#1(@queue, @t)
, dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil()))
, dequeue#2(::(@t, @ts)) ->
tuple#2(::(@t, nil()), tuple#2(@ts, nil()))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, lineMult#1(nil(), @l2, @n) -> nil()
, lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, computeLine#2(nil(), @acc, @x, @xs) -> nil()
, computeLine#2(::(@l, @ls), @acc, @x, @xs) ->
computeLine(@xs, @ls, lineMult(@x, @l, @acc)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
DPs:
{ 1: matrixMult^#(@m1, @m2) -> c_7(matrixMult#1^#(@m1, @m2))
, 4: bftMult'#5^#(@queue', @acc, @y) -> matrixMult^#(@acc, @y) }
Trs:
{ appendreverse#1(nil(), @sofar) -> @sofar
, computeLine#1(nil(), @acc, @m) -> @acc
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, +(@x, @y) -> #add(@x, @y)
, enqueue#1(tuple#2(@outq, @inq), @t) ->
tuple#2(@outq, ::(@t, @inq))
, *(@x, @y) -> #mult(@x, @y)
, lineMult#1(nil(), @l2, @n) -> nil()
, computeLine#2(nil(), @acc, @x, @xs) -> nil()
, computeLine#2(::(@l, @ls), @acc, @x, @xs) ->
computeLine(@xs, @ls, lineMult(@x, @l, @acc)) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_7) = {1}, Uargs(c_14) = {2}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[bftMult'#2](x1) = [1]
[#natmult](x1, x2) = [0]
[reverse](x1) = [5]
[appendreverse#1](x1, x2) = [7] x2 + [7]
[computeLine#1](x1, x2, x3) = [1] x1 + [3] x2 + [3]
[appendreverse](x1, x2) = [7] x2 + [6]
[matrixMult#1](x1, x2) = [1] x1 + [0]
[leaf] = [0]
[lineMult](x1, x2, x3) = [5] x2 + [1] x3 + [1]
[lineMult#2](x1, x2, x3, x4) = [1] x1 + [5] x4 + [6]
[#pos](x1) = [0]
[#add](x1, x2) = [1] x2 + [0]
[node](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
[dequeue](x1, x2) = [1]
[tuple#2](x1, x2) = [1]
[nil] = [1]
[computeLine](x1, x2, x3) = [1] x1 + [3]
[dequeue#1](x1, x2) = [1]
[::](x1, x2) = [1] x2 + [1]
[#mult](x1, x2) = [0]
[+](x1, x2) = [7] x2 + [7]
[#succ](x1) = [0]
[#0] = [0]
[enqueue#1](x1, x2) = [4]
[#neg](x1) = [1] x1 + [0]
[matrixMult](x1, x2) = [1] x1 + [0]
[*](x1, x2) = [2]
[enqueue](x1, x2) = [3]
[dequeue#2](x1) = [1]
[#pred](x1) = [0]
[lineMult#1](x1, x2, x3) = [5] x1 + [1] x2 + [1]
[#s](x1) = [0]
[computeLine#2](x1, x2, x3, x4) = [1] x4 + [7]
[bftMult'#5^#](x1, x2, x3) = [2] x2 + [7]
[bftMult'^#](x1, x2) = [2] x2 + [7]
[matrixMult^#](x1, x2) = [1] x1 + [1]
[bftMult'#3^#](x1, x2, x3) = [2] x2 + [7]
[bftMult'#4^#](x1, x2, x3) = [2] x2 + [7]
[matrixMult#1^#](x1, x2) = [1] x1 + [0]
[computeLine^#](x1, x2, x3) = [0]
[bftMult'#1^#](x1, x2) = [2] x1 + [2] x2 + [5]
[c_7](x1) = [1] x1 + [0]
[c_14](x1, x2) = [2] x1 + [1] x2 + [0]
The order satisfies the following ordering constraints:
[bftMult'#2(tuple#2(@dequeue@1, @dequeue@2))] = [1]
>= [1]
= [dequeue(@dequeue@1, @dequeue@2)]
[#natmult(#0(), @y)] = [0]
>= [0]
= [#0()]
[#natmult(#s(@x), @y)] = [0]
>= [0]
= [#add(#pos(@y), #natmult(@x, @y))]
[reverse(@xs)] = [5]
? [13]
= [appendreverse(@xs, nil())]
[appendreverse#1(nil(), @sofar)] = [7] @sofar + [7]
> [1] @sofar + [0]
= [@sofar]
[appendreverse#1(::(@a, @as), @sofar)] = [7] @sofar + [7]
? [7] @sofar + [13]
= [appendreverse(@as, ::(@a, @sofar))]
[computeLine#1(nil(), @acc, @m)] = [3] @acc + [4]
> [1] @acc + [0]
= [@acc]
[computeLine#1(::(@x, @xs), @acc, @m)] = [3] @acc + [1] @xs + [4]
? [1] @xs + [7]
= [computeLine#2(@m, @acc, @x, @xs)]
[appendreverse(@toreverse, @sofar)] = [7] @sofar + [6]
? [7] @sofar + [7]
= [appendreverse#1(@toreverse, @sofar)]
[matrixMult#1(nil(), @m2)] = [1]
>= [1]
= [nil()]
[matrixMult#1(::(@l, @ls), @m2)] = [1] @ls + [1]
>= [1] @ls + [1]
= [::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))]
[lineMult(@n, @l1, @l2)] = [5] @l1 + [1] @l2 + [1]
>= [5] @l1 + [1] @l2 + [1]
= [lineMult#1(@l1, @l2, @n)]
[lineMult#2(nil(), @n, @x, @xs)] = [5] @xs + [7]
> [5] @xs + [3]
= [::(*(@x, @n), lineMult(@n, @xs, nil()))]
[lineMult#2(::(@y, @ys), @n, @x, @xs)] = [5] @xs + [1] @ys + [7]
> [5] @xs + [1] @ys + [2]
= [::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))]
[#add(#pos(#s(#0())), @y)] = [1] @y + [0]
>= [0]
= [#succ(@y)]
[#add(#pos(#s(#s(@x))), @y)] = [1] @y + [0]
>= [0]
= [#succ(#add(#pos(#s(@x)), @y))]
[#add(#0(), @y)] = [1] @y + [0]
>= [1] @y + [0]
= [@y]
[#add(#neg(#s(#0())), @y)] = [1] @y + [0]
>= [0]
= [#pred(@y)]
[#add(#neg(#s(#s(@x))), @y)] = [1] @y + [0]
>= [0]
= [#pred(#add(#pos(#s(@x)), @y))]
[dequeue(@outq, @inq)] = [1]
>= [1]
= [dequeue#1(@outq, @inq)]
[computeLine(@line, @m, @acc)] = [1] @line + [3]
? [3] @acc + [1] @line + [3]
= [computeLine#1(@line, @acc, @m)]
[dequeue#1(nil(), @inq)] = [1]
>= [1]
= [dequeue#2(reverse(@inq))]
[dequeue#1(::(@t, @ts), @inq)] = [1]
>= [1]
= [tuple#2(::(@t, nil()), tuple#2(@ts, @inq))]
[#mult(#pos(@x), #pos(@y))] = [0]
>= [0]
= [#pos(#natmult(@x, @y))]
[#mult(#pos(@x), #0())] = [0]
>= [0]
= [#0()]
[#mult(#pos(@x), #neg(@y))] = [0]
>= [0]
= [#neg(#natmult(@x, @y))]
[#mult(#0(), #pos(@y))] = [0]
>= [0]
= [#0()]
[#mult(#0(), #0())] = [0]
>= [0]
= [#0()]
[#mult(#0(), #neg(@y))] = [0]
>= [0]
= [#0()]
[#mult(#neg(@x), #pos(@y))] = [0]
>= [0]
= [#neg(#natmult(@x, @y))]
[#mult(#neg(@x), #0())] = [0]
>= [0]
= [#0()]
[#mult(#neg(@x), #neg(@y))] = [0]
>= [0]
= [#pos(#natmult(@x, @y))]
[+(@x, @y)] = [7] @y + [7]
> [1] @y + [0]
= [#add(@x, @y)]
[#succ(#pos(#s(@x)))] = [0]
>= [0]
= [#pos(#s(#s(@x)))]
[#succ(#0())] = [0]
>= [0]
= [#pos(#s(#0()))]
[#succ(#neg(#s(#0())))] = [0]
>= [0]
= [#0()]
[#succ(#neg(#s(#s(@x))))] = [0]
>= [0]
= [#neg(#s(@x))]
[enqueue#1(tuple#2(@outq, @inq), @t)] = [4]
> [1]
= [tuple#2(@outq, ::(@t, @inq))]
[matrixMult(@m1, @m2)] = [1] @m1 + [0]
>= [1] @m1 + [0]
= [matrixMult#1(@m1, @m2)]
[*(@x, @y)] = [2]
> [0]
= [#mult(@x, @y)]
[enqueue(@t, @queue)] = [3]
? [4]
= [enqueue#1(@queue, @t)]
[dequeue#2(nil())] = [1]
>= [1]
= [tuple#2(nil(), tuple#2(nil(), nil()))]
[dequeue#2(::(@t, @ts))] = [1]
>= [1]
= [tuple#2(::(@t, nil()), tuple#2(@ts, nil()))]
[#pred(#pos(#s(#0())))] = [0]
>= [0]
= [#0()]
[#pred(#pos(#s(#s(@x))))] = [0]
>= [0]
= [#pos(#s(@x))]
[#pred(#0())] = [0]
>= [0]
= [#neg(#s(#0()))]
[#pred(#neg(#s(@x)))] = [0]
>= [0]
= [#neg(#s(#s(@x)))]
[lineMult#1(nil(), @l2, @n)] = [1] @l2 + [6]
> [1]
= [nil()]
[lineMult#1(::(@x, @xs), @l2, @n)] = [5] @xs + [1] @l2 + [6]
>= [5] @xs + [1] @l2 + [6]
= [lineMult#2(@l2, @n, @x, @xs)]
[computeLine#2(nil(), @acc, @x, @xs)] = [1] @xs + [7]
> [1]
= [nil()]
[computeLine#2(::(@l, @ls), @acc, @x, @xs)] = [1] @xs + [7]
> [1] @xs + [3]
= [computeLine(@xs, @ls, lineMult(@x, @l, @acc))]
[bftMult'#5^#(@queue', @acc, @y)] = [2] @acc + [7]
>= [2] @acc + [7]
= [bftMult'^#(@queue', matrixMult(@acc, @y))]
[bftMult'#5^#(@queue', @acc, @y)] = [2] @acc + [7]
> [1] @acc + [1]
= [matrixMult^#(@acc, @y)]
[bftMult'^#(@queue, @acc)] = [2] @acc + [7]
>= [2] @acc + [7]
= [bftMult'#1^#(bftMult'#2(@queue), @acc)]
[matrixMult^#(@m1, @m2)] = [1] @m1 + [1]
> [1] @m1 + [0]
= [c_7(matrixMult#1^#(@m1, @m2))]
[bftMult'#3^#(::(@t, @_@3), @acc, @queue)] = [2] @acc + [7]
>= [2] @acc + [7]
= [bftMult'#4^#(@t, @acc, @queue)]
[bftMult'#4^#(leaf(), @acc, @queue)] = [2] @acc + [7]
>= [2] @acc + [7]
= [bftMult'^#(@queue, @acc)]
[bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue)] = [2] @acc + [7]
>= [2] @acc + [7]
= [bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)]
[matrixMult#1^#(::(@l, @ls), @m2)] = [1] @ls + [1]
>= [1] @ls + [1]
= [c_14(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))]
[bftMult'#1^#(tuple#2(@elem, @queue), @acc)] = [2] @acc + [7]
>= [2] @acc + [7]
= [bftMult'#3^#(@elem, @acc, @queue)]
We return to the main proof. Consider the set of all dependency
pairs
:
{ 1: matrixMult^#(@m1, @m2) -> c_7(matrixMult#1^#(@m1, @m2))
, 2: matrixMult#1^#(::(@l, @ls), @m2) ->
c_14(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, 3: bftMult'#5^#(@queue', @acc, @y) ->
bftMult'^#(@queue', matrixMult(@acc, @y))
, 4: bftMult'#5^#(@queue', @acc, @y) -> matrixMult^#(@acc, @y)
, 5: bftMult'^#(@queue, @acc) ->
bftMult'#1^#(bftMult'#2(@queue), @acc)
, 6: bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
bftMult'#4^#(@t, @acc, @queue)
, 7: bftMult'#4^#(leaf(), @acc, @queue) -> bftMult'^#(@queue, @acc)
, 8: bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)
, 9: bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
bftMult'#3^#(@elem, @acc, @queue) }
Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of dependency
pairs {1,4}. These cover all (indirect) predecessors of dependency
pairs {1,2,4}, their number of application is equally bounded. The
dependency pairs are shifted into the weak component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak DPs:
{ bftMult'#5^#(@queue', @acc, @y) ->
bftMult'^#(@queue', matrixMult(@acc, @y))
, bftMult'#5^#(@queue', @acc, @y) -> matrixMult^#(@acc, @y)
, bftMult'^#(@queue, @acc) ->
bftMult'#1^#(bftMult'#2(@queue), @acc)
, matrixMult^#(@m1, @m2) -> c_7(matrixMult#1^#(@m1, @m2))
, bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
bftMult'#4^#(@t, @acc, @queue)
, bftMult'#4^#(leaf(), @acc, @queue) -> bftMult'^#(@queue, @acc)
, bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)
, matrixMult#1^#(::(@l, @ls), @m2) ->
c_14(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
bftMult'#3^#(@elem, @acc, @queue) }
Weak Trs:
{ bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) ->
dequeue(@dequeue@1, @dequeue@2)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
, reverse(@xs) -> appendreverse(@xs, nil())
, appendreverse#1(nil(), @sofar) -> @sofar
, appendreverse#1(::(@a, @as), @sofar) ->
appendreverse(@as, ::(@a, @sofar))
, computeLine#1(nil(), @acc, @m) -> @acc
, computeLine#1(::(@x, @xs), @acc, @m) ->
computeLine#2(@m, @acc, @x, @xs)
, appendreverse(@toreverse, @sofar) ->
appendreverse#1(@toreverse, @sofar)
, matrixMult#1(nil(), @m2) -> nil()
, matrixMult#1(::(@l, @ls), @m2) ->
::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, dequeue(@outq, @inq) -> dequeue#1(@outq, @inq)
, computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m)
, dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq))
, dequeue#1(::(@t, @ts), @inq) ->
tuple#2(::(@t, nil()), tuple#2(@ts, @inq))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, +(@x, @y) -> #add(@x, @y)
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, enqueue#1(tuple#2(@outq, @inq), @t) ->
tuple#2(@outq, ::(@t, @inq))
, matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2)
, *(@x, @y) -> #mult(@x, @y)
, enqueue(@t, @queue) -> enqueue#1(@queue, @t)
, dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil()))
, dequeue#2(::(@t, @ts)) ->
tuple#2(::(@t, nil()), tuple#2(@ts, nil()))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, lineMult#1(nil(), @l2, @n) -> nil()
, lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, computeLine#2(nil(), @acc, @x, @xs) -> nil()
, computeLine#2(::(@l, @ls), @acc, @x, @xs) ->
computeLine(@xs, @ls, lineMult(@x, @l, @acc)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ bftMult'#5^#(@queue', @acc, @y) ->
bftMult'^#(@queue', matrixMult(@acc, @y))
, bftMult'#5^#(@queue', @acc, @y) -> matrixMult^#(@acc, @y)
, bftMult'^#(@queue, @acc) ->
bftMult'#1^#(bftMult'#2(@queue), @acc)
, matrixMult^#(@m1, @m2) -> c_7(matrixMult#1^#(@m1, @m2))
, bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
bftMult'#4^#(@t, @acc, @queue)
, bftMult'#4^#(leaf(), @acc, @queue) -> bftMult'^#(@queue, @acc)
, bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)
, matrixMult#1^#(::(@l, @ls), @m2) ->
c_14(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
bftMult'#3^#(@elem, @acc, @queue) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) ->
dequeue(@dequeue@1, @dequeue@2)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
, reverse(@xs) -> appendreverse(@xs, nil())
, appendreverse#1(nil(), @sofar) -> @sofar
, appendreverse#1(::(@a, @as), @sofar) ->
appendreverse(@as, ::(@a, @sofar))
, computeLine#1(nil(), @acc, @m) -> @acc
, computeLine#1(::(@x, @xs), @acc, @m) ->
computeLine#2(@m, @acc, @x, @xs)
, appendreverse(@toreverse, @sofar) ->
appendreverse#1(@toreverse, @sofar)
, matrixMult#1(nil(), @m2) -> nil()
, matrixMult#1(::(@l, @ls), @m2) ->
::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, dequeue(@outq, @inq) -> dequeue#1(@outq, @inq)
, computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m)
, dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq))
, dequeue#1(::(@t, @ts), @inq) ->
tuple#2(::(@t, nil()), tuple#2(@ts, @inq))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, +(@x, @y) -> #add(@x, @y)
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, enqueue#1(tuple#2(@outq, @inq), @t) ->
tuple#2(@outq, ::(@t, @inq))
, matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2)
, *(@x, @y) -> #mult(@x, @y)
, enqueue(@t, @queue) -> enqueue#1(@queue, @t)
, dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil()))
, dequeue#2(::(@t, @ts)) ->
tuple#2(::(@t, nil()), tuple#2(@ts, nil()))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, lineMult#1(nil(), @l2, @n) -> nil()
, lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, computeLine#2(nil(), @acc, @x, @xs) -> nil()
, computeLine#2(::(@l, @ls), @acc, @x, @xs) ->
computeLine(@xs, @ls, lineMult(@x, @l, @acc)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
No rule is usable, rules are removed from the input problem.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Rules: Empty
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_9(computeLine#2^#(@m, @acc, @x, @xs))
, computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_10(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, computeLine^#(@line, @m, @acc) ->
c_15(computeLine#1^#(@line, @acc, @m))
, lineMult^#(@n, @l1, @l2) -> c_17(lineMult#1^#(@l1, @l2, @n))
, lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_18(lineMult#2^#(@l2, @n, @x, @xs))
, lineMult#2^#(nil(), @n, @x, @xs) ->
c_19(lineMult^#(@n, @xs, nil()))
, lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_20(lineMult^#(@n, @xs, @ys)) }
Weak DPs:
{ bftMult'#5^#(@queue', @acc, @y) ->
bftMult'^#(@queue', matrixMult(@acc, @y))
, bftMult'#5^#(@queue', @acc, @y) -> matrixMult^#(@acc, @y)
, bftMult'^#(@queue, @acc) ->
bftMult'#1^#(bftMult'#2(@queue), @acc)
, matrixMult^#(@m1, @m2) -> matrixMult#1^#(@m1, @m2)
, bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
bftMult'#4^#(@t, @acc, @queue)
, bftMult'#4^#(leaf(), @acc, @queue) -> bftMult'^#(@queue, @acc)
, bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)
, matrixMult#1^#(::(@l, @ls), @m2) -> matrixMult^#(@ls, @m2)
, matrixMult#1^#(::(@l, @ls), @m2) -> computeLine^#(@l, @m2, nil())
, bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
bftMult'#3^#(@elem, @acc, @queue) }
Weak Trs:
{ bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) ->
dequeue(@dequeue@1, @dequeue@2)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
, reverse(@xs) -> appendreverse(@xs, nil())
, appendreverse#1(nil(), @sofar) -> @sofar
, appendreverse#1(::(@a, @as), @sofar) ->
appendreverse(@as, ::(@a, @sofar))
, computeLine#1(nil(), @acc, @m) -> @acc
, computeLine#1(::(@x, @xs), @acc, @m) ->
computeLine#2(@m, @acc, @x, @xs)
, appendreverse(@toreverse, @sofar) ->
appendreverse#1(@toreverse, @sofar)
, matrixMult#1(nil(), @m2) -> nil()
, matrixMult#1(::(@l, @ls), @m2) ->
::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, dequeue(@outq, @inq) -> dequeue#1(@outq, @inq)
, computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m)
, dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq))
, dequeue#1(::(@t, @ts), @inq) ->
tuple#2(::(@t, nil()), tuple#2(@ts, @inq))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, +(@x, @y) -> #add(@x, @y)
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, enqueue#1(tuple#2(@outq, @inq), @t) ->
tuple#2(@outq, ::(@t, @inq))
, matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2)
, *(@x, @y) -> #mult(@x, @y)
, enqueue(@t, @queue) -> enqueue#1(@queue, @t)
, dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil()))
, dequeue#2(::(@t, @ts)) ->
tuple#2(::(@t, nil()), tuple#2(@ts, nil()))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, lineMult#1(nil(), @l2, @n) -> nil()
, lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, computeLine#2(nil(), @acc, @x, @xs) -> nil()
, computeLine#2(::(@l, @ls), @acc, @x, @xs) ->
computeLine(@xs, @ls, lineMult(@x, @l, @acc)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
DPs:
{ 1: computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_9(computeLine#2^#(@m, @acc, @x, @xs))
, 5: lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_18(lineMult#2^#(@l2, @n, @x, @xs))
, 9: bftMult'#5^#(@queue', @acc, @y) -> matrixMult^#(@acc, @y)
, 10: bftMult'^#(@queue, @acc) ->
bftMult'#1^#(bftMult'#2(@queue), @acc)
, 12: bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
bftMult'#4^#(@t, @acc, @queue)
, 13: bftMult'#4^#(leaf(), @acc, @queue) ->
bftMult'^#(@queue, @acc)
, 14: bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)
, 16: matrixMult#1^#(::(@l, @ls), @m2) ->
computeLine^#(@l, @m2, nil()) }
Trs:
{ lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, dequeue#1(::(@t, @ts), @inq) ->
tuple#2(::(@t, nil()), tuple#2(@ts, @inq))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil()))
, dequeue#2(::(@t, @ts)) ->
tuple#2(::(@t, nil()), tuple#2(@ts, nil()))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, computeLine#2(nil(), @acc, @x, @xs) -> nil()
, computeLine#2(::(@l, @ls), @acc, @x, @xs) ->
computeLine(@xs, @ls, lineMult(@x, @l, @acc)) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_9) = {1}, Uargs(c_10) = {1, 2}, Uargs(c_15) = {1},
Uargs(c_17) = {1}, Uargs(c_18) = {1}, Uargs(c_19) = {1},
Uargs(c_20) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[bftMult'#2](x1) = [1] x1 + [3]
[#natmult](x1, x2) = [0]
[reverse](x1) = [1] x1 + [0]
[appendreverse#1](x1, x2) = [1] x1 + [1] x2 + [0]
[computeLine#1](x1, x2, x3) = [7] x2 + [0]
[appendreverse](x1, x2) = [1] x1 + [1] x2 + [0]
[matrixMult#1](x1, x2) = [1] x1 + [2] x2 + [0]
[leaf] = [4]
[lineMult](x1, x2, x3) = [1] x3 + [0]
[lineMult#2](x1, x2, x3, x4) = [1] x1 + [1]
[#pos](x1) = [1] x1 + [1]
[#add](x1, x2) = [2] x1 + [1] x2 + [6]
[node](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [6]
[dequeue](x1, x2) = [1] x1 + [1] x2 + [3]
[tuple#2](x1, x2) = [1] x1 + [1] x2 + [0]
[nil] = [0]
[computeLine](x1, x2, x3) = [0]
[dequeue#1](x1, x2) = [1] x1 + [1] x2 + [3]
[::](x1, x2) = [1] x1 + [1] x2 + [1]
[#mult](x1, x2) = [1] x1 + [1]
[+](x1, x2) = [0]
[#succ](x1) = [2]
[#0] = [0]
[enqueue#1](x1, x2) = [1] x1 + [1] x2 + [1]
[#neg](x1) = [1]
[matrixMult](x1, x2) = [1] x1 + [2] x2 + [0]
[*](x1, x2) = [7]
[enqueue](x1, x2) = [1] x1 + [1] x2 + [1]
[dequeue#2](x1) = [1] x1 + [3]
[#pred](x1) = [4]
[lineMult#1](x1, x2, x3) = [1] x2 + [0]
[#s](x1) = [0]
[computeLine#2](x1, x2, x3, x4) = [4]
[bftMult'#5^#](x1, x2, x3) = [2] x1 + [2] x3 + [7]
[bftMult'^#](x1, x2) = [2] x1 + [7]
[matrixMult^#](x1, x2) = [2] x2 + [6]
[computeLine#1^#](x1, x2, x3) = [1] x3 + [3]
[computeLine#2^#](x1, x2, x3, x4) = [1] x1 + [2]
[bftMult'#3^#](x1, x2, x3) = [2] x1 + [2] x3 + [0]
[bftMult'#4^#](x1, x2, x3) = [2] x1 + [2] x3 + [1]
[matrixMult#1^#](x1, x2) = [2] x2 + [6]
[computeLine^#](x1, x2, x3) = [1] x2 + [3]
[lineMult^#](x1, x2, x3) = [1] x2 + [0]
[lineMult#1^#](x1, x2, x3) = [1] x1 + [0]
[lineMult#2^#](x1, x2, x3, x4) = [1] x4 + [0]
[bftMult'#1^#](x1, x2) = [2] x1 + [0]
[c_9](x1) = [1] x1 + [0]
[c_10](x1, x2) = [1] x1 + [1] x2 + [0]
[c_15](x1) = [1] x1 + [0]
[c_17](x1) = [1] x1 + [0]
[c_18](x1) = [1] x1 + [0]
[c_19](x1) = [1] x1 + [0]
[c_20](x1) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[bftMult'#2(tuple#2(@dequeue@1, @dequeue@2))] = [1] @dequeue@1 + [1] @dequeue@2 + [3]
>= [1] @dequeue@1 + [1] @dequeue@2 + [3]
= [dequeue(@dequeue@1, @dequeue@2)]
[#natmult(#0(), @y)] = [0]
>= [0]
= [#0()]
[#natmult(#s(@x), @y)] = [0]
? [2] @y + [8]
= [#add(#pos(@y), #natmult(@x, @y))]
[reverse(@xs)] = [1] @xs + [0]
>= [1] @xs + [0]
= [appendreverse(@xs, nil())]
[appendreverse#1(nil(), @sofar)] = [1] @sofar + [0]
>= [1] @sofar + [0]
= [@sofar]
[appendreverse#1(::(@a, @as), @sofar)] = [1] @sofar + [1] @a + [1] @as + [1]
>= [1] @sofar + [1] @a + [1] @as + [1]
= [appendreverse(@as, ::(@a, @sofar))]
[computeLine#1(nil(), @acc, @m)] = [7] @acc + [0]
>= [1] @acc + [0]
= [@acc]
[computeLine#1(::(@x, @xs), @acc, @m)] = [7] @acc + [0]
? [4]
= [computeLine#2(@m, @acc, @x, @xs)]
[appendreverse(@toreverse, @sofar)] = [1] @toreverse + [1] @sofar + [0]
>= [1] @toreverse + [1] @sofar + [0]
= [appendreverse#1(@toreverse, @sofar)]
[matrixMult#1(nil(), @m2)] = [2] @m2 + [0]
>= [0]
= [nil()]
[matrixMult#1(::(@l, @ls), @m2)] = [1] @l + [1] @ls + [2] @m2 + [1]
>= [1] @ls + [2] @m2 + [1]
= [::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))]
[lineMult(@n, @l1, @l2)] = [1] @l2 + [0]
>= [1] @l2 + [0]
= [lineMult#1(@l1, @l2, @n)]
[lineMult#2(nil(), @n, @x, @xs)] = [1]
? [8]
= [::(*(@x, @n), lineMult(@n, @xs, nil()))]
[lineMult#2(::(@y, @ys), @n, @x, @xs)] = [1] @y + [1] @ys + [2]
> [1] @ys + [1]
= [::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))]
[#add(#pos(#s(#0())), @y)] = [1] @y + [8]
> [2]
= [#succ(@y)]
[#add(#pos(#s(#s(@x))), @y)] = [1] @y + [8]
> [2]
= [#succ(#add(#pos(#s(@x)), @y))]
[#add(#0(), @y)] = [1] @y + [6]
> [1] @y + [0]
= [@y]
[#add(#neg(#s(#0())), @y)] = [1] @y + [8]
> [4]
= [#pred(@y)]
[#add(#neg(#s(#s(@x))), @y)] = [1] @y + [8]
> [4]
= [#pred(#add(#pos(#s(@x)), @y))]
[dequeue(@outq, @inq)] = [1] @outq + [1] @inq + [3]
>= [1] @outq + [1] @inq + [3]
= [dequeue#1(@outq, @inq)]
[computeLine(@line, @m, @acc)] = [0]
? [7] @acc + [0]
= [computeLine#1(@line, @acc, @m)]
[dequeue#1(nil(), @inq)] = [1] @inq + [3]
>= [1] @inq + [3]
= [dequeue#2(reverse(@inq))]
[dequeue#1(::(@t, @ts), @inq)] = [1] @t + [1] @inq + [1] @ts + [4]
> [1] @t + [1] @inq + [1] @ts + [1]
= [tuple#2(::(@t, nil()), tuple#2(@ts, @inq))]
[#mult(#pos(@x), #pos(@y))] = [1] @x + [2]
> [1]
= [#pos(#natmult(@x, @y))]
[#mult(#pos(@x), #0())] = [1] @x + [2]
> [0]
= [#0()]
[#mult(#pos(@x), #neg(@y))] = [1] @x + [2]
> [1]
= [#neg(#natmult(@x, @y))]
[#mult(#0(), #pos(@y))] = [1]
> [0]
= [#0()]
[#mult(#0(), #0())] = [1]
> [0]
= [#0()]
[#mult(#0(), #neg(@y))] = [1]
> [0]
= [#0()]
[#mult(#neg(@x), #pos(@y))] = [2]
> [1]
= [#neg(#natmult(@x, @y))]
[#mult(#neg(@x), #0())] = [2]
> [0]
= [#0()]
[#mult(#neg(@x), #neg(@y))] = [2]
> [1]
= [#pos(#natmult(@x, @y))]
[+(@x, @y)] = [0]
? [2] @x + [1] @y + [6]
= [#add(@x, @y)]
[#succ(#pos(#s(@x)))] = [2]
> [1]
= [#pos(#s(#s(@x)))]
[#succ(#0())] = [2]
> [1]
= [#pos(#s(#0()))]
[#succ(#neg(#s(#0())))] = [2]
> [0]
= [#0()]
[#succ(#neg(#s(#s(@x))))] = [2]
> [1]
= [#neg(#s(@x))]
[enqueue#1(tuple#2(@outq, @inq), @t)] = [1] @t + [1] @outq + [1] @inq + [1]
>= [1] @t + [1] @outq + [1] @inq + [1]
= [tuple#2(@outq, ::(@t, @inq))]
[matrixMult(@m1, @m2)] = [1] @m1 + [2] @m2 + [0]
>= [1] @m1 + [2] @m2 + [0]
= [matrixMult#1(@m1, @m2)]
[*(@x, @y)] = [7]
? [1] @x + [1]
= [#mult(@x, @y)]
[enqueue(@t, @queue)] = [1] @t + [1] @queue + [1]
>= [1] @t + [1] @queue + [1]
= [enqueue#1(@queue, @t)]
[dequeue#2(nil())] = [3]
> [0]
= [tuple#2(nil(), tuple#2(nil(), nil()))]
[dequeue#2(::(@t, @ts))] = [1] @t + [1] @ts + [4]
> [1] @t + [1] @ts + [1]
= [tuple#2(::(@t, nil()), tuple#2(@ts, nil()))]
[#pred(#pos(#s(#0())))] = [4]
> [0]
= [#0()]
[#pred(#pos(#s(#s(@x))))] = [4]
> [1]
= [#pos(#s(@x))]
[#pred(#0())] = [4]
> [1]
= [#neg(#s(#0()))]
[#pred(#neg(#s(@x)))] = [4]
> [1]
= [#neg(#s(#s(@x)))]
[lineMult#1(nil(), @l2, @n)] = [1] @l2 + [0]
>= [0]
= [nil()]
[lineMult#1(::(@x, @xs), @l2, @n)] = [1] @l2 + [0]
? [1] @l2 + [1]
= [lineMult#2(@l2, @n, @x, @xs)]
[computeLine#2(nil(), @acc, @x, @xs)] = [4]
> [0]
= [nil()]
[computeLine#2(::(@l, @ls), @acc, @x, @xs)] = [4]
> [0]
= [computeLine(@xs, @ls, lineMult(@x, @l, @acc))]
[bftMult'#5^#(@queue', @acc, @y)] = [2] @y + [2] @queue' + [7]
>= [2] @queue' + [7]
= [bftMult'^#(@queue', matrixMult(@acc, @y))]
[bftMult'#5^#(@queue', @acc, @y)] = [2] @y + [2] @queue' + [7]
> [2] @y + [6]
= [matrixMult^#(@acc, @y)]
[bftMult'^#(@queue, @acc)] = [2] @queue + [7]
> [2] @queue + [6]
= [bftMult'#1^#(bftMult'#2(@queue), @acc)]
[matrixMult^#(@m1, @m2)] = [2] @m2 + [6]
>= [2] @m2 + [6]
= [matrixMult#1^#(@m1, @m2)]
[computeLine#1^#(::(@x, @xs), @acc, @m)] = [1] @m + [3]
> [1] @m + [2]
= [c_9(computeLine#2^#(@m, @acc, @x, @xs))]
[computeLine#2^#(::(@l, @ls), @acc, @x, @xs)] = [1] @l + [1] @ls + [3]
>= [1] @l + [1] @ls + [3]
= [c_10(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))]
[bftMult'#3^#(::(@t, @_@3), @acc, @queue)] = [2] @t + [2] @queue + [2] @_@3 + [2]
> [2] @t + [2] @queue + [1]
= [bftMult'#4^#(@t, @acc, @queue)]
[bftMult'#4^#(leaf(), @acc, @queue)] = [2] @queue + [9]
> [2] @queue + [7]
= [bftMult'^#(@queue, @acc)]
[bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue)] = [2] @y + [2] @queue + [2] @t1 + [2] @t2 + [13]
> [2] @y + [2] @queue + [2] @t1 + [2] @t2 + [11]
= [bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)]
[matrixMult#1^#(::(@l, @ls), @m2)] = [2] @m2 + [6]
>= [2] @m2 + [6]
= [matrixMult^#(@ls, @m2)]
[matrixMult#1^#(::(@l, @ls), @m2)] = [2] @m2 + [6]
> [1] @m2 + [3]
= [computeLine^#(@l, @m2, nil())]
[computeLine^#(@line, @m, @acc)] = [1] @m + [3]
>= [1] @m + [3]
= [c_15(computeLine#1^#(@line, @acc, @m))]
[lineMult^#(@n, @l1, @l2)] = [1] @l1 + [0]
>= [1] @l1 + [0]
= [c_17(lineMult#1^#(@l1, @l2, @n))]
[lineMult#1^#(::(@x, @xs), @l2, @n)] = [1] @x + [1] @xs + [1]
> [1] @xs + [0]
= [c_18(lineMult#2^#(@l2, @n, @x, @xs))]
[lineMult#2^#(nil(), @n, @x, @xs)] = [1] @xs + [0]
>= [1] @xs + [0]
= [c_19(lineMult^#(@n, @xs, nil()))]
[lineMult#2^#(::(@y, @ys), @n, @x, @xs)] = [1] @xs + [0]
>= [1] @xs + [0]
= [c_20(lineMult^#(@n, @xs, @ys))]
[bftMult'#1^#(tuple#2(@elem, @queue), @acc)] = [2] @queue + [2] @elem + [0]
>= [2] @queue + [2] @elem + [0]
= [bftMult'#3^#(@elem, @acc, @queue)]
We return to the main proof. Consider the set of all dependency
pairs
:
{ 1: computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_9(computeLine#2^#(@m, @acc, @x, @xs))
, 2: computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_10(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, 3: computeLine^#(@line, @m, @acc) ->
c_15(computeLine#1^#(@line, @acc, @m))
, 4: lineMult^#(@n, @l1, @l2) -> c_17(lineMult#1^#(@l1, @l2, @n))
, 5: lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_18(lineMult#2^#(@l2, @n, @x, @xs))
, 6: lineMult#2^#(nil(), @n, @x, @xs) ->
c_19(lineMult^#(@n, @xs, nil()))
, 7: lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_20(lineMult^#(@n, @xs, @ys))
, 8: bftMult'#5^#(@queue', @acc, @y) ->
bftMult'^#(@queue', matrixMult(@acc, @y))
, 9: bftMult'#5^#(@queue', @acc, @y) -> matrixMult^#(@acc, @y)
, 10: bftMult'^#(@queue, @acc) ->
bftMult'#1^#(bftMult'#2(@queue), @acc)
, 11: matrixMult^#(@m1, @m2) -> matrixMult#1^#(@m1, @m2)
, 12: bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
bftMult'#4^#(@t, @acc, @queue)
, 13: bftMult'#4^#(leaf(), @acc, @queue) ->
bftMult'^#(@queue, @acc)
, 14: bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)
, 15: matrixMult#1^#(::(@l, @ls), @m2) -> matrixMult^#(@ls, @m2)
, 16: matrixMult#1^#(::(@l, @ls), @m2) ->
computeLine^#(@l, @m2, nil())
, 17: bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
bftMult'#3^#(@elem, @acc, @queue) }
Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of dependency
pairs {1,5,9,10,12,13,14,16}. These cover all (indirect)
predecessors of dependency pairs
{1,2,3,4,5,6,7,8,9,10,12,13,14,16,17}, their number of application
is equally bounded. The dependency pairs are shifted into the weak
component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak DPs:
{ bftMult'#5^#(@queue', @acc, @y) ->
bftMult'^#(@queue', matrixMult(@acc, @y))
, bftMult'#5^#(@queue', @acc, @y) -> matrixMult^#(@acc, @y)
, bftMult'^#(@queue, @acc) ->
bftMult'#1^#(bftMult'#2(@queue), @acc)
, matrixMult^#(@m1, @m2) -> matrixMult#1^#(@m1, @m2)
, computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_9(computeLine#2^#(@m, @acc, @x, @xs))
, computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_10(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
bftMult'#4^#(@t, @acc, @queue)
, bftMult'#4^#(leaf(), @acc, @queue) -> bftMult'^#(@queue, @acc)
, bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)
, matrixMult#1^#(::(@l, @ls), @m2) -> matrixMult^#(@ls, @m2)
, matrixMult#1^#(::(@l, @ls), @m2) -> computeLine^#(@l, @m2, nil())
, computeLine^#(@line, @m, @acc) ->
c_15(computeLine#1^#(@line, @acc, @m))
, lineMult^#(@n, @l1, @l2) -> c_17(lineMult#1^#(@l1, @l2, @n))
, lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_18(lineMult#2^#(@l2, @n, @x, @xs))
, lineMult#2^#(nil(), @n, @x, @xs) ->
c_19(lineMult^#(@n, @xs, nil()))
, lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_20(lineMult^#(@n, @xs, @ys))
, bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
bftMult'#3^#(@elem, @acc, @queue) }
Weak Trs:
{ bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) ->
dequeue(@dequeue@1, @dequeue@2)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
, reverse(@xs) -> appendreverse(@xs, nil())
, appendreverse#1(nil(), @sofar) -> @sofar
, appendreverse#1(::(@a, @as), @sofar) ->
appendreverse(@as, ::(@a, @sofar))
, computeLine#1(nil(), @acc, @m) -> @acc
, computeLine#1(::(@x, @xs), @acc, @m) ->
computeLine#2(@m, @acc, @x, @xs)
, appendreverse(@toreverse, @sofar) ->
appendreverse#1(@toreverse, @sofar)
, matrixMult#1(nil(), @m2) -> nil()
, matrixMult#1(::(@l, @ls), @m2) ->
::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, dequeue(@outq, @inq) -> dequeue#1(@outq, @inq)
, computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m)
, dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq))
, dequeue#1(::(@t, @ts), @inq) ->
tuple#2(::(@t, nil()), tuple#2(@ts, @inq))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, +(@x, @y) -> #add(@x, @y)
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, enqueue#1(tuple#2(@outq, @inq), @t) ->
tuple#2(@outq, ::(@t, @inq))
, matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2)
, *(@x, @y) -> #mult(@x, @y)
, enqueue(@t, @queue) -> enqueue#1(@queue, @t)
, dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil()))
, dequeue#2(::(@t, @ts)) ->
tuple#2(::(@t, nil()), tuple#2(@ts, nil()))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, lineMult#1(nil(), @l2, @n) -> nil()
, lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, computeLine#2(nil(), @acc, @x, @xs) -> nil()
, computeLine#2(::(@l, @ls), @acc, @x, @xs) ->
computeLine(@xs, @ls, lineMult(@x, @l, @acc)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ bftMult'#5^#(@queue', @acc, @y) ->
bftMult'^#(@queue', matrixMult(@acc, @y))
, bftMult'#5^#(@queue', @acc, @y) -> matrixMult^#(@acc, @y)
, bftMult'^#(@queue, @acc) ->
bftMult'#1^#(bftMult'#2(@queue), @acc)
, matrixMult^#(@m1, @m2) -> matrixMult#1^#(@m1, @m2)
, computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_9(computeLine#2^#(@m, @acc, @x, @xs))
, computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_10(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, bftMult'#3^#(::(@t, @_@3), @acc, @queue) ->
bftMult'#4^#(@t, @acc, @queue)
, bftMult'#4^#(leaf(), @acc, @queue) -> bftMult'^#(@queue, @acc)
, bftMult'#4^#(node(@y, @t1, @t2), @acc, @queue) ->
bftMult'#5^#(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)
, matrixMult#1^#(::(@l, @ls), @m2) -> matrixMult^#(@ls, @m2)
, matrixMult#1^#(::(@l, @ls), @m2) -> computeLine^#(@l, @m2, nil())
, computeLine^#(@line, @m, @acc) ->
c_15(computeLine#1^#(@line, @acc, @m))
, lineMult^#(@n, @l1, @l2) -> c_17(lineMult#1^#(@l1, @l2, @n))
, lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_18(lineMult#2^#(@l2, @n, @x, @xs))
, lineMult#2^#(nil(), @n, @x, @xs) ->
c_19(lineMult^#(@n, @xs, nil()))
, lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_20(lineMult^#(@n, @xs, @ys))
, bftMult'#1^#(tuple#2(@elem, @queue), @acc) ->
bftMult'#3^#(@elem, @acc, @queue) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) ->
dequeue(@dequeue@1, @dequeue@2)
, #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
, reverse(@xs) -> appendreverse(@xs, nil())
, appendreverse#1(nil(), @sofar) -> @sofar
, appendreverse#1(::(@a, @as), @sofar) ->
appendreverse(@as, ::(@a, @sofar))
, computeLine#1(nil(), @acc, @m) -> @acc
, computeLine#1(::(@x, @xs), @acc, @m) ->
computeLine#2(@m, @acc, @x, @xs)
, appendreverse(@toreverse, @sofar) ->
appendreverse#1(@toreverse, @sofar)
, matrixMult#1(nil(), @m2) -> nil()
, matrixMult#1(::(@l, @ls), @m2) ->
::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, #add(#pos(#s(#0())), @y) -> #succ(@y)
, #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
, #add(#0(), @y) -> @y
, #add(#neg(#s(#0())), @y) -> #pred(@y)
, #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
, dequeue(@outq, @inq) -> dequeue#1(@outq, @inq)
, computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m)
, dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq))
, dequeue#1(::(@t, @ts), @inq) ->
tuple#2(::(@t, nil()), tuple#2(@ts, @inq))
, #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
, #mult(#pos(@x), #0()) -> #0()
, #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
, #mult(#0(), #pos(@y)) -> #0()
, #mult(#0(), #0()) -> #0()
, #mult(#0(), #neg(@y)) -> #0()
, #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
, #mult(#neg(@x), #0()) -> #0()
, #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
, +(@x, @y) -> #add(@x, @y)
, #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
, #succ(#0()) -> #pos(#s(#0()))
, #succ(#neg(#s(#0()))) -> #0()
, #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
, enqueue#1(tuple#2(@outq, @inq), @t) ->
tuple#2(@outq, ::(@t, @inq))
, matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2)
, *(@x, @y) -> #mult(@x, @y)
, enqueue(@t, @queue) -> enqueue#1(@queue, @t)
, dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil()))
, dequeue#2(::(@t, @ts)) ->
tuple#2(::(@t, nil()), tuple#2(@ts, nil()))
, #pred(#pos(#s(#0()))) -> #0()
, #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
, #pred(#0()) -> #neg(#s(#0()))
, #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
, lineMult#1(nil(), @l2, @n) -> nil()
, lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, computeLine#2(nil(), @acc, @x, @xs) -> nil()
, computeLine#2(::(@l, @ls), @acc, @x, @xs) ->
computeLine(@xs, @ls, lineMult(@x, @l, @acc)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
No rule is usable, rules are removed from the input problem.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Rules: Empty
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
Hurray, we answered YES(O(1),O(n^3))