We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m)
, computeLine#1(::(@x, @xs), @acc, @m) ->
computeLine#2(@m, @acc, @x, @xs)
, computeLine#1(nil(), @acc, @m) -> @acc
, matrixMult#1(::(@l, @ls), @m2) ->
::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))
, matrixMult#1(nil(), @m2) -> nil()
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, +(@x, @y) -> #add(@x, @y)
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2)
, *(@x, @y) -> #mult(@x, @y)
, lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, lineMult#1(nil(), @l2, @n) -> nil()
, computeLine#2(::(@l, @ls), @acc, @x, @xs) ->
computeLine(@xs, @ls, lineMult(@x, @l, @acc))
, computeLine#2(nil(), @acc, @x, @xs) -> nil() }
Weak Trs:
{ #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@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))
, #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))
, #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^2))
We add the following dependency tuples:
Strict DPs:
{ computeLine^#(@line, @m, @acc) ->
c_1(computeLine#1^#(@line, @acc, @m))
, computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_2(computeLine#2^#(@m, @acc, @x, @xs))
, computeLine#1^#(nil(), @acc, @m) -> c_3()
, computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_14(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, computeLine#2^#(nil(), @acc, @x, @xs) -> c_15()
, matrixMult#1^#(::(@l, @ls), @m2) ->
c_4(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, matrixMult#1^#(nil(), @m2) -> c_5()
, matrixMult^#(@m1, @m2) -> c_10(matrixMult#1^#(@m1, @m2))
, lineMult^#(@n, @l1, @l2) -> c_6(lineMult#1^#(@l1, @l2, @n))
, lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_12(lineMult#2^#(@l2, @n, @x, @xs))
, lineMult#1^#(nil(), @l2, @n) -> c_13()
, +^#(@x, @y) -> c_7(#add^#(@x, @y))
, lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_8(+^#(*(@x, @n), @y), *^#(@x, @n), lineMult^#(@n, @xs, @ys))
, lineMult#2^#(nil(), @n, @x, @xs) ->
c_9(*^#(@x, @n), lineMult^#(@n, @xs, nil()))
, *^#(@x, @y) -> c_11(#mult^#(@x, @y)) }
Weak DPs:
{ #add^#(#pos(#s(#0())), @y) -> c_31(#succ^#(@y))
, #add^#(#pos(#s(#s(@x))), @y) ->
c_32(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, #add^#(#0(), @y) -> c_33()
, #add^#(#neg(#s(#0())), @y) -> c_34(#pred^#(@y))
, #add^#(#neg(#s(#s(@x))), @y) ->
c_35(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, #mult^#(#pos(@x), #pos(@y)) -> c_18(#natmult^#(@x, @y))
, #mult^#(#pos(@x), #0()) -> c_19()
, #mult^#(#pos(@x), #neg(@y)) -> c_20(#natmult^#(@x, @y))
, #mult^#(#0(), #pos(@y)) -> c_21()
, #mult^#(#0(), #0()) -> c_22()
, #mult^#(#0(), #neg(@y)) -> c_23()
, #mult^#(#neg(@x), #pos(@y)) -> c_24(#natmult^#(@x, @y))
, #mult^#(#neg(@x), #0()) -> c_25()
, #mult^#(#neg(@x), #neg(@y)) -> c_26(#natmult^#(@x, @y))
, #natmult^#(#0(), @y) -> c_16()
, #natmult^#(#s(@x), @y) ->
c_17(#add^#(#pos(@y), #natmult(@x, @y)), #natmult^#(@x, @y))
, #succ^#(#pos(#s(@x))) -> c_27()
, #succ^#(#0()) -> c_28()
, #succ^#(#neg(#s(#0()))) -> c_29()
, #succ^#(#neg(#s(#s(@x)))) -> c_30()
, #pred^#(#pos(#s(#0()))) -> c_36()
, #pred^#(#pos(#s(#s(@x)))) -> c_37()
, #pred^#(#0()) -> c_38()
, #pred^#(#neg(#s(@x))) -> c_39() }
and mark the set of starting terms.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ computeLine^#(@line, @m, @acc) ->
c_1(computeLine#1^#(@line, @acc, @m))
, computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_2(computeLine#2^#(@m, @acc, @x, @xs))
, computeLine#1^#(nil(), @acc, @m) -> c_3()
, computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_14(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, computeLine#2^#(nil(), @acc, @x, @xs) -> c_15()
, matrixMult#1^#(::(@l, @ls), @m2) ->
c_4(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, matrixMult#1^#(nil(), @m2) -> c_5()
, matrixMult^#(@m1, @m2) -> c_10(matrixMult#1^#(@m1, @m2))
, lineMult^#(@n, @l1, @l2) -> c_6(lineMult#1^#(@l1, @l2, @n))
, lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_12(lineMult#2^#(@l2, @n, @x, @xs))
, lineMult#1^#(nil(), @l2, @n) -> c_13()
, +^#(@x, @y) -> c_7(#add^#(@x, @y))
, lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_8(+^#(*(@x, @n), @y), *^#(@x, @n), lineMult^#(@n, @xs, @ys))
, lineMult#2^#(nil(), @n, @x, @xs) ->
c_9(*^#(@x, @n), lineMult^#(@n, @xs, nil()))
, *^#(@x, @y) -> c_11(#mult^#(@x, @y)) }
Weak DPs:
{ #add^#(#pos(#s(#0())), @y) -> c_31(#succ^#(@y))
, #add^#(#pos(#s(#s(@x))), @y) ->
c_32(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, #add^#(#0(), @y) -> c_33()
, #add^#(#neg(#s(#0())), @y) -> c_34(#pred^#(@y))
, #add^#(#neg(#s(#s(@x))), @y) ->
c_35(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, #mult^#(#pos(@x), #pos(@y)) -> c_18(#natmult^#(@x, @y))
, #mult^#(#pos(@x), #0()) -> c_19()
, #mult^#(#pos(@x), #neg(@y)) -> c_20(#natmult^#(@x, @y))
, #mult^#(#0(), #pos(@y)) -> c_21()
, #mult^#(#0(), #0()) -> c_22()
, #mult^#(#0(), #neg(@y)) -> c_23()
, #mult^#(#neg(@x), #pos(@y)) -> c_24(#natmult^#(@x, @y))
, #mult^#(#neg(@x), #0()) -> c_25()
, #mult^#(#neg(@x), #neg(@y)) -> c_26(#natmult^#(@x, @y))
, #natmult^#(#0(), @y) -> c_16()
, #natmult^#(#s(@x), @y) ->
c_17(#add^#(#pos(@y), #natmult(@x, @y)), #natmult^#(@x, @y))
, #succ^#(#pos(#s(@x))) -> c_27()
, #succ^#(#0()) -> c_28()
, #succ^#(#neg(#s(#0()))) -> c_29()
, #succ^#(#neg(#s(#s(@x)))) -> c_30()
, #pred^#(#pos(#s(#0()))) -> c_36()
, #pred^#(#pos(#s(#s(@x)))) -> c_37()
, #pred^#(#0()) -> c_38()
, #pred^#(#neg(#s(@x))) -> c_39() }
Weak Trs:
{ #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
, computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m)
, computeLine#1(::(@x, @xs), @acc, @m) ->
computeLine#2(@m, @acc, @x, @xs)
, computeLine#1(nil(), @acc, @m) -> @acc
, matrixMult#1(::(@l, @ls), @m2) ->
::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))
, matrixMult#1(nil(), @m2) -> nil()
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, #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))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, #add(#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))
, matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2)
, *(@x, @y) -> #mult(@x, @y)
, #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(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, lineMult#1(nil(), @l2, @n) -> nil()
, computeLine#2(::(@l, @ls), @acc, @x, @xs) ->
computeLine(@xs, @ls, lineMult(@x, @l, @acc))
, computeLine#2(nil(), @acc, @x, @xs) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We estimate the number of application of {3,5,7,11,12,15} by
applications of Pre({3,5,7,11,12,15}) = {1,2,8,9,13,14}. Here rules
are labeled as follows:
DPs:
{ 1: computeLine^#(@line, @m, @acc) ->
c_1(computeLine#1^#(@line, @acc, @m))
, 2: computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_2(computeLine#2^#(@m, @acc, @x, @xs))
, 3: computeLine#1^#(nil(), @acc, @m) -> c_3()
, 4: computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_14(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, 5: computeLine#2^#(nil(), @acc, @x, @xs) -> c_15()
, 6: matrixMult#1^#(::(@l, @ls), @m2) ->
c_4(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, 7: matrixMult#1^#(nil(), @m2) -> c_5()
, 8: matrixMult^#(@m1, @m2) -> c_10(matrixMult#1^#(@m1, @m2))
, 9: lineMult^#(@n, @l1, @l2) -> c_6(lineMult#1^#(@l1, @l2, @n))
, 10: lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_12(lineMult#2^#(@l2, @n, @x, @xs))
, 11: lineMult#1^#(nil(), @l2, @n) -> c_13()
, 12: +^#(@x, @y) -> c_7(#add^#(@x, @y))
, 13: lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_8(+^#(*(@x, @n), @y), *^#(@x, @n), lineMult^#(@n, @xs, @ys))
, 14: lineMult#2^#(nil(), @n, @x, @xs) ->
c_9(*^#(@x, @n), lineMult^#(@n, @xs, nil()))
, 15: *^#(@x, @y) -> c_11(#mult^#(@x, @y))
, 16: #add^#(#pos(#s(#0())), @y) -> c_31(#succ^#(@y))
, 17: #add^#(#pos(#s(#s(@x))), @y) ->
c_32(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, 18: #add^#(#0(), @y) -> c_33()
, 19: #add^#(#neg(#s(#0())), @y) -> c_34(#pred^#(@y))
, 20: #add^#(#neg(#s(#s(@x))), @y) ->
c_35(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, 21: #mult^#(#pos(@x), #pos(@y)) -> c_18(#natmult^#(@x, @y))
, 22: #mult^#(#pos(@x), #0()) -> c_19()
, 23: #mult^#(#pos(@x), #neg(@y)) -> c_20(#natmult^#(@x, @y))
, 24: #mult^#(#0(), #pos(@y)) -> c_21()
, 25: #mult^#(#0(), #0()) -> c_22()
, 26: #mult^#(#0(), #neg(@y)) -> c_23()
, 27: #mult^#(#neg(@x), #pos(@y)) -> c_24(#natmult^#(@x, @y))
, 28: #mult^#(#neg(@x), #0()) -> c_25()
, 29: #mult^#(#neg(@x), #neg(@y)) -> c_26(#natmult^#(@x, @y))
, 30: #natmult^#(#0(), @y) -> c_16()
, 31: #natmult^#(#s(@x), @y) ->
c_17(#add^#(#pos(@y), #natmult(@x, @y)), #natmult^#(@x, @y))
, 32: #succ^#(#pos(#s(@x))) -> c_27()
, 33: #succ^#(#0()) -> c_28()
, 34: #succ^#(#neg(#s(#0()))) -> c_29()
, 35: #succ^#(#neg(#s(#s(@x)))) -> c_30()
, 36: #pred^#(#pos(#s(#0()))) -> c_36()
, 37: #pred^#(#pos(#s(#s(@x)))) -> c_37()
, 38: #pred^#(#0()) -> c_38()
, 39: #pred^#(#neg(#s(@x))) -> c_39() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ computeLine^#(@line, @m, @acc) ->
c_1(computeLine#1^#(@line, @acc, @m))
, computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_2(computeLine#2^#(@m, @acc, @x, @xs))
, computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_14(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, matrixMult#1^#(::(@l, @ls), @m2) ->
c_4(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, matrixMult^#(@m1, @m2) -> c_10(matrixMult#1^#(@m1, @m2))
, lineMult^#(@n, @l1, @l2) -> c_6(lineMult#1^#(@l1, @l2, @n))
, lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_12(lineMult#2^#(@l2, @n, @x, @xs))
, lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_8(+^#(*(@x, @n), @y), *^#(@x, @n), lineMult^#(@n, @xs, @ys))
, lineMult#2^#(nil(), @n, @x, @xs) ->
c_9(*^#(@x, @n), lineMult^#(@n, @xs, nil())) }
Weak DPs:
{ computeLine#1^#(nil(), @acc, @m) -> c_3()
, computeLine#2^#(nil(), @acc, @x, @xs) -> c_15()
, matrixMult#1^#(nil(), @m2) -> c_5()
, lineMult#1^#(nil(), @l2, @n) -> c_13()
, +^#(@x, @y) -> c_7(#add^#(@x, @y))
, #add^#(#pos(#s(#0())), @y) -> c_31(#succ^#(@y))
, #add^#(#pos(#s(#s(@x))), @y) ->
c_32(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, #add^#(#0(), @y) -> c_33()
, #add^#(#neg(#s(#0())), @y) -> c_34(#pred^#(@y))
, #add^#(#neg(#s(#s(@x))), @y) ->
c_35(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, *^#(@x, @y) -> c_11(#mult^#(@x, @y))
, #mult^#(#pos(@x), #pos(@y)) -> c_18(#natmult^#(@x, @y))
, #mult^#(#pos(@x), #0()) -> c_19()
, #mult^#(#pos(@x), #neg(@y)) -> c_20(#natmult^#(@x, @y))
, #mult^#(#0(), #pos(@y)) -> c_21()
, #mult^#(#0(), #0()) -> c_22()
, #mult^#(#0(), #neg(@y)) -> c_23()
, #mult^#(#neg(@x), #pos(@y)) -> c_24(#natmult^#(@x, @y))
, #mult^#(#neg(@x), #0()) -> c_25()
, #mult^#(#neg(@x), #neg(@y)) -> c_26(#natmult^#(@x, @y))
, #natmult^#(#0(), @y) -> c_16()
, #natmult^#(#s(@x), @y) ->
c_17(#add^#(#pos(@y), #natmult(@x, @y)), #natmult^#(@x, @y))
, #succ^#(#pos(#s(@x))) -> c_27()
, #succ^#(#0()) -> c_28()
, #succ^#(#neg(#s(#0()))) -> c_29()
, #succ^#(#neg(#s(#s(@x)))) -> c_30()
, #pred^#(#pos(#s(#0()))) -> c_36()
, #pred^#(#pos(#s(#s(@x)))) -> c_37()
, #pred^#(#0()) -> c_38()
, #pred^#(#neg(#s(@x))) -> c_39() }
Weak Trs:
{ #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
, computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m)
, computeLine#1(::(@x, @xs), @acc, @m) ->
computeLine#2(@m, @acc, @x, @xs)
, computeLine#1(nil(), @acc, @m) -> @acc
, matrixMult#1(::(@l, @ls), @m2) ->
::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))
, matrixMult#1(nil(), @m2) -> nil()
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, #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))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, #add(#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))
, matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2)
, *(@x, @y) -> #mult(@x, @y)
, #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(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, lineMult#1(nil(), @l2, @n) -> nil()
, computeLine#2(::(@l, @ls), @acc, @x, @xs) ->
computeLine(@xs, @ls, lineMult(@x, @l, @acc))
, computeLine#2(nil(), @acc, @x, @xs) -> nil() }
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.
{ computeLine#1^#(nil(), @acc, @m) -> c_3()
, computeLine#2^#(nil(), @acc, @x, @xs) -> c_15()
, matrixMult#1^#(nil(), @m2) -> c_5()
, lineMult#1^#(nil(), @l2, @n) -> c_13()
, +^#(@x, @y) -> c_7(#add^#(@x, @y))
, #add^#(#pos(#s(#0())), @y) -> c_31(#succ^#(@y))
, #add^#(#pos(#s(#s(@x))), @y) ->
c_32(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, #add^#(#0(), @y) -> c_33()
, #add^#(#neg(#s(#0())), @y) -> c_34(#pred^#(@y))
, #add^#(#neg(#s(#s(@x))), @y) ->
c_35(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y))
, *^#(@x, @y) -> c_11(#mult^#(@x, @y))
, #mult^#(#pos(@x), #pos(@y)) -> c_18(#natmult^#(@x, @y))
, #mult^#(#pos(@x), #0()) -> c_19()
, #mult^#(#pos(@x), #neg(@y)) -> c_20(#natmult^#(@x, @y))
, #mult^#(#0(), #pos(@y)) -> c_21()
, #mult^#(#0(), #0()) -> c_22()
, #mult^#(#0(), #neg(@y)) -> c_23()
, #mult^#(#neg(@x), #pos(@y)) -> c_24(#natmult^#(@x, @y))
, #mult^#(#neg(@x), #0()) -> c_25()
, #mult^#(#neg(@x), #neg(@y)) -> c_26(#natmult^#(@x, @y))
, #natmult^#(#0(), @y) -> c_16()
, #natmult^#(#s(@x), @y) ->
c_17(#add^#(#pos(@y), #natmult(@x, @y)), #natmult^#(@x, @y))
, #succ^#(#pos(#s(@x))) -> c_27()
, #succ^#(#0()) -> c_28()
, #succ^#(#neg(#s(#0()))) -> c_29()
, #succ^#(#neg(#s(#s(@x)))) -> c_30()
, #pred^#(#pos(#s(#0()))) -> c_36()
, #pred^#(#pos(#s(#s(@x)))) -> c_37()
, #pred^#(#0()) -> c_38()
, #pred^#(#neg(#s(@x))) -> c_39() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ computeLine^#(@line, @m, @acc) ->
c_1(computeLine#1^#(@line, @acc, @m))
, computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_2(computeLine#2^#(@m, @acc, @x, @xs))
, computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_14(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, matrixMult#1^#(::(@l, @ls), @m2) ->
c_4(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, matrixMult^#(@m1, @m2) -> c_10(matrixMult#1^#(@m1, @m2))
, lineMult^#(@n, @l1, @l2) -> c_6(lineMult#1^#(@l1, @l2, @n))
, lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_12(lineMult#2^#(@l2, @n, @x, @xs))
, lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_8(+^#(*(@x, @n), @y), *^#(@x, @n), lineMult^#(@n, @xs, @ys))
, lineMult#2^#(nil(), @n, @x, @xs) ->
c_9(*^#(@x, @n), lineMult^#(@n, @xs, nil())) }
Weak Trs:
{ #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
, computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m)
, computeLine#1(::(@x, @xs), @acc, @m) ->
computeLine#2(@m, @acc, @x, @xs)
, computeLine#1(nil(), @acc, @m) -> @acc
, matrixMult#1(::(@l, @ls), @m2) ->
::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))
, matrixMult#1(nil(), @m2) -> nil()
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, #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))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, #add(#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))
, matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2)
, *(@x, @y) -> #mult(@x, @y)
, #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(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, lineMult#1(nil(), @l2, @n) -> nil()
, computeLine#2(::(@l, @ls), @acc, @x, @xs) ->
computeLine(@xs, @ls, lineMult(@x, @l, @acc))
, computeLine#2(nil(), @acc, @x, @xs) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_8(+^#(*(@x, @n), @y), *^#(@x, @n), lineMult^#(@n, @xs, @ys))
, lineMult#2^#(nil(), @n, @x, @xs) ->
c_9(*^#(@x, @n), lineMult^#(@n, @xs, nil())) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ computeLine^#(@line, @m, @acc) ->
c_1(computeLine#1^#(@line, @acc, @m))
, computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_2(computeLine#2^#(@m, @acc, @x, @xs))
, computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_3(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, matrixMult#1^#(::(@l, @ls), @m2) ->
c_4(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, matrixMult^#(@m1, @m2) -> c_5(matrixMult#1^#(@m1, @m2))
, lineMult^#(@n, @l1, @l2) -> c_6(lineMult#1^#(@l1, @l2, @n))
, lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_7(lineMult#2^#(@l2, @n, @x, @xs))
, lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_8(lineMult^#(@n, @xs, @ys))
, lineMult#2^#(nil(), @n, @x, @xs) ->
c_9(lineMult^#(@n, @xs, nil())) }
Weak Trs:
{ #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
, computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m)
, computeLine#1(::(@x, @xs), @acc, @m) ->
computeLine#2(@m, @acc, @x, @xs)
, computeLine#1(nil(), @acc, @m) -> @acc
, matrixMult#1(::(@l, @ls), @m2) ->
::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))
, matrixMult#1(nil(), @m2) -> nil()
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, #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))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, #add(#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))
, matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2)
, *(@x, @y) -> #mult(@x, @y)
, #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(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, lineMult#1(nil(), @l2, @n) -> nil()
, computeLine#2(::(@l, @ls), @acc, @x, @xs) ->
computeLine(@xs, @ls, lineMult(@x, @l, @acc))
, computeLine#2(nil(), @acc, @x, @xs) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We replace rewrite rules by usable rules:
Weak Usable Rules:
{ #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, #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))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, #add(#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))
, *(@x, @y) -> #mult(@x, @y)
, #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(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, lineMult#1(nil(), @l2, @n) -> nil() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ computeLine^#(@line, @m, @acc) ->
c_1(computeLine#1^#(@line, @acc, @m))
, computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_2(computeLine#2^#(@m, @acc, @x, @xs))
, computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_3(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, matrixMult#1^#(::(@l, @ls), @m2) ->
c_4(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, matrixMult^#(@m1, @m2) -> c_5(matrixMult#1^#(@m1, @m2))
, lineMult^#(@n, @l1, @l2) -> c_6(lineMult#1^#(@l1, @l2, @n))
, lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_7(lineMult#2^#(@l2, @n, @x, @xs))
, lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_8(lineMult^#(@n, @xs, @ys))
, lineMult#2^#(nil(), @n, @x, @xs) ->
c_9(lineMult^#(@n, @xs, nil())) }
Weak Trs:
{ #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, #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))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, #add(#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))
, *(@x, @y) -> #mult(@x, @y)
, #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(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, lineMult#1(nil(), @l2, @n) -> nil() }
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
{ matrixMult#1^#(::(@l, @ls), @m2) ->
c_4(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, matrixMult^#(@m1, @m2) -> c_5(matrixMult#1^#(@m1, @m2)) }
and lower component
{ computeLine^#(@line, @m, @acc) ->
c_1(computeLine#1^#(@line, @acc, @m))
, computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_2(computeLine#2^#(@m, @acc, @x, @xs))
, computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_3(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, lineMult^#(@n, @l1, @l2) -> c_6(lineMult#1^#(@l1, @l2, @n))
, lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_7(lineMult#2^#(@l2, @n, @x, @xs))
, lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_8(lineMult^#(@n, @xs, @ys))
, lineMult#2^#(nil(), @n, @x, @xs) ->
c_9(lineMult^#(@n, @xs, nil())) }
Further, following extension rules are added to the lower
component.
{ matrixMult#1^#(::(@l, @ls), @m2) -> computeLine^#(@l, @m2, nil())
, matrixMult#1^#(::(@l, @ls), @m2) -> matrixMult^#(@ls, @m2)
, matrixMult^#(@m1, @m2) -> matrixMult#1^#(@m1, @m2) }
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#1^#(::(@l, @ls), @m2) ->
c_4(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, matrixMult^#(@m1, @m2) -> c_5(matrixMult#1^#(@m1, @m2)) }
Weak Trs:
{ #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, #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))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, #add(#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))
, *(@x, @y) -> #mult(@x, @y)
, #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(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, lineMult#1(nil(), @l2, @n) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^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(n^1)).
Strict DPs:
{ matrixMult#1^#(::(@l, @ls), @m2) ->
c_4(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, matrixMult^#(@m1, @m2) -> c_5(matrixMult#1^#(@m1, @m2)) }
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:
{ 2: matrixMult^#(@m1, @m2) -> c_5(matrixMult#1^#(@m1, @m2)) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_4) = {2}, Uargs(c_5) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[#natmult](x1, x2) = [0]
[lineMult](x1, x2, x3) = [0]
[::](x1, x2) = [1] x1 + [1] x2 + [2]
[#mult](x1, x2) = [0]
[+](x1, x2) = [0]
[#succ](x1) = [0]
[lineMult#2](x1, x2, x3, x4) = [0]
[#pos](x1) = [0]
[#add](x1, x2) = [0]
[#0] = [0]
[#neg](x1) = [0]
[*](x1, x2) = [0]
[#pred](x1) = [0]
[lineMult#1](x1, x2, x3) = [0]
[#s](x1) = [0]
[nil] = [0]
[computeLine^#](x1, x2, x3) = [0]
[matrixMult#1^#](x1, x2) = [4] x1 + [4] x2 + [0]
[matrixMult^#](x1, x2) = [4] x1 + [4] x2 + [4]
[c_4](x1, x2) = [1] x2 + [4]
[c_5](x1) = [1] x1 + [3]
The order satisfies the following ordering constraints:
[matrixMult#1^#(::(@l, @ls), @m2)] = [4] @l + [4] @ls + [4] @m2 + [8]
>= [4] @ls + [4] @m2 + [8]
= [c_4(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))]
[matrixMult^#(@m1, @m2)] = [4] @m1 + [4] @m2 + [4]
> [4] @m1 + [4] @m2 + [3]
= [c_5(matrixMult#1^#(@m1, @m2))]
We return to the main proof. Consider the set of all dependency
pairs
:
{ 1: matrixMult#1^#(::(@l, @ls), @m2) ->
c_4(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, 2: matrixMult^#(@m1, @m2) -> c_5(matrixMult#1^#(@m1, @m2)) }
Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of dependency
pairs {2}. These cover all (indirect) predecessors of dependency
pairs {1,2}, 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:
{ matrixMult#1^#(::(@l, @ls), @m2) ->
c_4(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, matrixMult^#(@m1, @m2) -> c_5(matrixMult#1^#(@m1, @m2)) }
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.
{ matrixMult#1^#(::(@l, @ls), @m2) ->
c_4(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))
, matrixMult^#(@m1, @m2) -> c_5(matrixMult#1^#(@m1, @m2)) }
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^#(@line, @m, @acc) ->
c_1(computeLine#1^#(@line, @acc, @m))
, computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_2(computeLine#2^#(@m, @acc, @x, @xs))
, computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_3(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, lineMult^#(@n, @l1, @l2) -> c_6(lineMult#1^#(@l1, @l2, @n))
, lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_7(lineMult#2^#(@l2, @n, @x, @xs))
, lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_8(lineMult^#(@n, @xs, @ys))
, lineMult#2^#(nil(), @n, @x, @xs) ->
c_9(lineMult^#(@n, @xs, nil())) }
Weak DPs:
{ matrixMult#1^#(::(@l, @ls), @m2) -> computeLine^#(@l, @m2, nil())
, matrixMult#1^#(::(@l, @ls), @m2) -> matrixMult^#(@ls, @m2)
, matrixMult^#(@m1, @m2) -> matrixMult#1^#(@m1, @m2) }
Weak Trs:
{ #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, #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))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, #add(#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))
, *(@x, @y) -> #mult(@x, @y)
, #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(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, lineMult#1(nil(), @l2, @n) -> nil() }
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^#(@line, @m, @acc) ->
c_1(computeLine#1^#(@line, @acc, @m))
, 3: computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_3(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, 5: lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_7(lineMult#2^#(@l2, @n, @x, @xs))
, 8: matrixMult#1^#(::(@l, @ls), @m2) ->
computeLine^#(@l, @m2, nil()) }
Trs:
{ +(@x, @y) -> #add(@x, @y)
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, lineMult#1(nil(), @l2, @n) -> nil() }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1, 2},
Uargs(c_6) = {1}, Uargs(c_7) = {1}, Uargs(c_8) = {1},
Uargs(c_9) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[#natmult](x1, x2) = [0]
[lineMult](x1, x2, x3) = [2] x2 + [1] x3 + [2]
[::](x1, x2) = [1] x1 + [1] x2 + [3]
[#mult](x1, x2) = [0]
[+](x1, x2) = [1] x2 + [1]
[#succ](x1) = [0]
[lineMult#2](x1, x2, x3, x4) = [1] x1 + [2] x4 + [6]
[#pos](x1) = [0]
[#add](x1, x2) = [1] x2 + [0]
[#0] = [0]
[#neg](x1) = [0]
[*](x1, x2) = [0]
[#pred](x1) = [0]
[lineMult#1](x1, x2, x3) = [2] x1 + [1] x2 + [2]
[#s](x1) = [0]
[nil] = [1]
[computeLine^#](x1, x2, x3) = [5] x2 + [2] x3 + [1]
[computeLine#1^#](x1, x2, x3) = [2] x2 + [5] x3 + [0]
[computeLine#2^#](x1, x2, x3, x4) = [5] x1 + [2] x2 + [0]
[matrixMult#1^#](x1, x2) = [7] x2 + [7]
[matrixMult^#](x1, x2) = [7] x2 + [7]
[lineMult^#](x1, x2, x3) = [1] x2 + [1]
[lineMult#1^#](x1, x2, x3) = [1] x1 + [1]
[lineMult#2^#](x1, x2, x3, x4) = [1] x4 + [1]
[c_1](x1) = [1] x1 + [0]
[c_2](x1) = [1] x1 + [0]
[c_3](x1, x2) = [1] x1 + [1] x2 + [4]
[c_6](x1) = [1] x1 + [0]
[c_7](x1) = [1] x1 + [2]
[c_8](x1) = [1] x1 + [0]
[c_9](x1) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[#natmult(#0(), @y)] = [0]
>= [0]
= [#0()]
[#natmult(#s(@x), @y)] = [0]
>= [0]
= [#add(#pos(@y), #natmult(@x, @y))]
[lineMult(@n, @l1, @l2)] = [2] @l1 + [1] @l2 + [2]
>= [2] @l1 + [1] @l2 + [2]
= [lineMult#1(@l1, @l2, @n)]
[#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 + [1]
> [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))]
[lineMult#2(::(@y, @ys), @n, @x, @xs)] = [1] @y + [2] @xs + [1] @ys + [9]
> [1] @y + [2] @xs + [1] @ys + [6]
= [::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))]
[lineMult#2(nil(), @n, @x, @xs)] = [2] @xs + [7]
> [2] @xs + [6]
= [::(*(@x, @n), lineMult(@n, @xs, nil()))]
[#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))]
[*(@x, @y)] = [0]
>= [0]
= [#mult(@x, @y)]
[#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(::(@x, @xs), @l2, @n)] = [2] @x + [2] @xs + [1] @l2 + [8]
> [2] @xs + [1] @l2 + [6]
= [lineMult#2(@l2, @n, @x, @xs)]
[lineMult#1(nil(), @l2, @n)] = [1] @l2 + [4]
> [1]
= [nil()]
[computeLine^#(@line, @m, @acc)] = [5] @m + [2] @acc + [1]
> [5] @m + [2] @acc + [0]
= [c_1(computeLine#1^#(@line, @acc, @m))]
[computeLine#1^#(::(@x, @xs), @acc, @m)] = [5] @m + [2] @acc + [0]
>= [5] @m + [2] @acc + [0]
= [c_2(computeLine#2^#(@m, @acc, @x, @xs))]
[computeLine#2^#(::(@l, @ls), @acc, @x, @xs)] = [2] @acc + [5] @l + [5] @ls + [15]
> [2] @acc + [5] @l + [5] @ls + [10]
= [c_3(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))]
[matrixMult#1^#(::(@l, @ls), @m2)] = [7] @m2 + [7]
> [5] @m2 + [3]
= [computeLine^#(@l, @m2, nil())]
[matrixMult#1^#(::(@l, @ls), @m2)] = [7] @m2 + [7]
>= [7] @m2 + [7]
= [matrixMult^#(@ls, @m2)]
[matrixMult^#(@m1, @m2)] = [7] @m2 + [7]
>= [7] @m2 + [7]
= [matrixMult#1^#(@m1, @m2)]
[lineMult^#(@n, @l1, @l2)] = [1] @l1 + [1]
>= [1] @l1 + [1]
= [c_6(lineMult#1^#(@l1, @l2, @n))]
[lineMult#1^#(::(@x, @xs), @l2, @n)] = [1] @x + [1] @xs + [4]
> [1] @xs + [3]
= [c_7(lineMult#2^#(@l2, @n, @x, @xs))]
[lineMult#2^#(::(@y, @ys), @n, @x, @xs)] = [1] @xs + [1]
>= [1] @xs + [1]
= [c_8(lineMult^#(@n, @xs, @ys))]
[lineMult#2^#(nil(), @n, @x, @xs)] = [1] @xs + [1]
>= [1] @xs + [1]
= [c_9(lineMult^#(@n, @xs, nil()))]
We return to the main proof. Consider the set of all dependency
pairs
:
{ 1: computeLine^#(@line, @m, @acc) ->
c_1(computeLine#1^#(@line, @acc, @m))
, 2: computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_2(computeLine#2^#(@m, @acc, @x, @xs))
, 3: computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_3(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, 4: lineMult^#(@n, @l1, @l2) -> c_6(lineMult#1^#(@l1, @l2, @n))
, 5: lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_7(lineMult#2^#(@l2, @n, @x, @xs))
, 6: lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_8(lineMult^#(@n, @xs, @ys))
, 7: lineMult#2^#(nil(), @n, @x, @xs) ->
c_9(lineMult^#(@n, @xs, nil()))
, 8: matrixMult#1^#(::(@l, @ls), @m2) ->
computeLine^#(@l, @m2, nil())
, 9: matrixMult#1^#(::(@l, @ls), @m2) -> matrixMult^#(@ls, @m2)
, 10: matrixMult^#(@m1, @m2) -> matrixMult#1^#(@m1, @m2) }
Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of dependency
pairs {1,3,5,8}. These cover all (indirect) predecessors of
dependency pairs {1,2,3,4,5,6,7,8}, 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:
{ computeLine^#(@line, @m, @acc) ->
c_1(computeLine#1^#(@line, @acc, @m))
, computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_2(computeLine#2^#(@m, @acc, @x, @xs))
, computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_3(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, matrixMult#1^#(::(@l, @ls), @m2) -> computeLine^#(@l, @m2, nil())
, matrixMult#1^#(::(@l, @ls), @m2) -> matrixMult^#(@ls, @m2)
, matrixMult^#(@m1, @m2) -> matrixMult#1^#(@m1, @m2)
, lineMult^#(@n, @l1, @l2) -> c_6(lineMult#1^#(@l1, @l2, @n))
, lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_7(lineMult#2^#(@l2, @n, @x, @xs))
, lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_8(lineMult^#(@n, @xs, @ys))
, lineMult#2^#(nil(), @n, @x, @xs) ->
c_9(lineMult^#(@n, @xs, nil())) }
Weak Trs:
{ #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, #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))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, #add(#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))
, *(@x, @y) -> #mult(@x, @y)
, #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(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, lineMult#1(nil(), @l2, @n) -> nil() }
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.
{ computeLine^#(@line, @m, @acc) ->
c_1(computeLine#1^#(@line, @acc, @m))
, computeLine#1^#(::(@x, @xs), @acc, @m) ->
c_2(computeLine#2^#(@m, @acc, @x, @xs))
, computeLine#2^#(::(@l, @ls), @acc, @x, @xs) ->
c_3(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)),
lineMult^#(@x, @l, @acc))
, matrixMult#1^#(::(@l, @ls), @m2) -> computeLine^#(@l, @m2, nil())
, matrixMult#1^#(::(@l, @ls), @m2) -> matrixMult^#(@ls, @m2)
, matrixMult^#(@m1, @m2) -> matrixMult#1^#(@m1, @m2)
, lineMult^#(@n, @l1, @l2) -> c_6(lineMult#1^#(@l1, @l2, @n))
, lineMult#1^#(::(@x, @xs), @l2, @n) ->
c_7(lineMult#2^#(@l2, @n, @x, @xs))
, lineMult#2^#(::(@y, @ys), @n, @x, @xs) ->
c_8(lineMult^#(@n, @xs, @ys))
, lineMult#2^#(nil(), @n, @x, @xs) ->
c_9(lineMult^#(@n, @xs, nil())) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ #natmult(#0(), @y) -> #0()
, #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
, lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
, #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))
, lineMult#2(::(@y, @ys), @n, @x, @xs) ->
::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
, lineMult#2(nil(), @n, @x, @xs) ->
::(*(@x, @n), lineMult(@n, @xs, nil()))
, #add(#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))
, *(@x, @y) -> #mult(@x, @y)
, #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(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
, lineMult#1(nil(), @l2, @n) -> nil() }
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^2))