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