YES(O(1),O(n^2)) 40.54/11.57 YES(O(1),O(n^2)) 40.54/11.57 40.54/11.57 We are left with following problem, upon which TcT provides the 40.54/11.57 certificate YES(O(1),O(n^2)). 40.54/11.57 40.54/11.57 Strict Trs: 40.54/11.57 { mult(@n, @l) -> mult#1(@l, @n) 40.54/11.57 , mult#1(::(@x, @xs), @n) -> ::(*(@n, @x), mult(@n, @xs)) 40.54/11.57 , mult#1(nil(), @n) -> nil() 40.54/11.57 , *(@x, @y) -> #mult(@x, @y) 40.54/11.57 , dyade#1(::(@x, @xs), @l2) -> ::(mult(@x, @l2), dyade(@xs, @l2)) 40.54/11.57 , dyade#1(nil(), @l2) -> nil() 40.54/11.57 , dyade(@l1, @l2) -> dyade#1(@l1, @l2) } 40.54/11.57 Weak Trs: 40.54/11.57 { #natmult(#0(), @y) -> #0() 40.54/11.57 , #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) 40.54/11.57 , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) 40.54/11.57 , #mult(#pos(@x), #0()) -> #0() 40.54/11.57 , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) 40.54/11.57 , #mult(#0(), #pos(@y)) -> #0() 40.54/11.57 , #mult(#0(), #0()) -> #0() 40.54/11.57 , #mult(#0(), #neg(@y)) -> #0() 40.54/11.57 , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) 40.54/11.57 , #mult(#neg(@x), #0()) -> #0() 40.54/11.57 , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) 40.54/11.57 , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) 40.54/11.57 , #succ(#0()) -> #pos(#s(#0())) 40.54/11.57 , #succ(#neg(#s(#0()))) -> #0() 40.54/11.57 , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) 40.54/11.57 , #add(#pos(#s(#0())), @y) -> #succ(@y) 40.54/11.57 , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) 40.54/11.57 , #add(#0(), @y) -> @y 40.54/11.57 , #add(#neg(#s(#0())), @y) -> #pred(@y) 40.54/11.57 , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) 40.54/11.57 , #pred(#pos(#s(#0()))) -> #0() 40.54/11.57 , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) 40.54/11.57 , #pred(#0()) -> #neg(#s(#0())) 40.54/11.57 , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) } 40.54/11.57 Obligation: 40.54/11.57 innermost runtime complexity 40.54/11.57 Answer: 40.54/11.57 YES(O(1),O(n^2)) 40.54/11.57 40.54/11.57 We add the following weak dependency pairs: 40.54/11.57 40.54/11.57 Strict DPs: 40.54/11.57 { mult^#(@n, @l) -> c_1(mult#1^#(@l, @n)) 40.54/11.57 , mult#1^#(::(@x, @xs), @n) -> c_2(*^#(@n, @x), mult^#(@n, @xs)) 40.54/11.57 , mult#1^#(nil(), @n) -> c_3() 40.54/11.57 , *^#(@x, @y) -> c_4(#mult^#(@x, @y)) 40.54/11.57 , dyade#1^#(::(@x, @xs), @l2) -> 40.54/11.57 c_5(mult^#(@x, @l2), dyade^#(@xs, @l2)) 40.54/11.57 , dyade#1^#(nil(), @l2) -> c_6() 40.54/11.57 , dyade^#(@l1, @l2) -> c_7(dyade#1^#(@l1, @l2)) } 40.54/11.57 Weak DPs: 40.54/11.57 { #mult^#(#pos(@x), #pos(@y)) -> c_10(#natmult^#(@x, @y)) 40.54/11.57 , #mult^#(#pos(@x), #0()) -> c_11() 40.54/11.57 , #mult^#(#pos(@x), #neg(@y)) -> c_12(#natmult^#(@x, @y)) 40.54/11.57 , #mult^#(#0(), #pos(@y)) -> c_13() 40.54/11.57 , #mult^#(#0(), #0()) -> c_14() 40.54/11.57 , #mult^#(#0(), #neg(@y)) -> c_15() 40.54/11.57 , #mult^#(#neg(@x), #pos(@y)) -> c_16(#natmult^#(@x, @y)) 40.54/11.57 , #mult^#(#neg(@x), #0()) -> c_17() 40.54/11.57 , #mult^#(#neg(@x), #neg(@y)) -> c_18(#natmult^#(@x, @y)) 40.54/11.57 , #natmult^#(#0(), @y) -> c_8() 40.54/11.57 , #natmult^#(#s(@x), @y) -> c_9(#add^#(#pos(@y), #natmult(@x, @y))) 40.54/11.57 , #add^#(#pos(#s(#0())), @y) -> c_23(#succ^#(@y)) 40.54/11.57 , #add^#(#pos(#s(#s(@x))), @y) -> 40.54/11.57 c_24(#succ^#(#add(#pos(#s(@x)), @y))) 40.54/11.57 , #add^#(#0(), @y) -> c_25() 40.54/11.57 , #add^#(#neg(#s(#0())), @y) -> c_26(#pred^#(@y)) 40.54/11.57 , #add^#(#neg(#s(#s(@x))), @y) -> 40.54/11.57 c_27(#pred^#(#add(#pos(#s(@x)), @y))) 40.54/11.57 , #succ^#(#pos(#s(@x))) -> c_19() 40.54/11.57 , #succ^#(#0()) -> c_20() 40.54/11.57 , #succ^#(#neg(#s(#0()))) -> c_21() 40.54/11.57 , #succ^#(#neg(#s(#s(@x)))) -> c_22() 40.54/11.57 , #pred^#(#pos(#s(#0()))) -> c_28() 40.54/11.57 , #pred^#(#pos(#s(#s(@x)))) -> c_29() 40.54/11.57 , #pred^#(#0()) -> c_30() 40.54/11.57 , #pred^#(#neg(#s(@x))) -> c_31() } 40.54/11.57 40.54/11.57 and mark the set of starting terms. 40.54/11.57 40.54/11.57 We are left with following problem, upon which TcT provides the 40.54/11.57 certificate YES(O(1),O(n^2)). 40.54/11.57 40.54/11.57 Strict DPs: 40.54/11.57 { mult^#(@n, @l) -> c_1(mult#1^#(@l, @n)) 40.54/11.57 , mult#1^#(::(@x, @xs), @n) -> c_2(*^#(@n, @x), mult^#(@n, @xs)) 40.54/11.57 , mult#1^#(nil(), @n) -> c_3() 40.54/11.57 , *^#(@x, @y) -> c_4(#mult^#(@x, @y)) 40.54/11.57 , dyade#1^#(::(@x, @xs), @l2) -> 40.54/11.57 c_5(mult^#(@x, @l2), dyade^#(@xs, @l2)) 40.54/11.57 , dyade#1^#(nil(), @l2) -> c_6() 40.54/11.57 , dyade^#(@l1, @l2) -> c_7(dyade#1^#(@l1, @l2)) } 40.54/11.57 Strict Trs: 40.54/11.57 { mult(@n, @l) -> mult#1(@l, @n) 40.54/11.57 , mult#1(::(@x, @xs), @n) -> ::(*(@n, @x), mult(@n, @xs)) 40.54/11.57 , mult#1(nil(), @n) -> nil() 40.54/11.57 , *(@x, @y) -> #mult(@x, @y) 40.54/11.57 , dyade#1(::(@x, @xs), @l2) -> ::(mult(@x, @l2), dyade(@xs, @l2)) 40.54/11.57 , dyade#1(nil(), @l2) -> nil() 40.54/11.57 , dyade(@l1, @l2) -> dyade#1(@l1, @l2) } 40.54/11.57 Weak DPs: 40.54/11.57 { #mult^#(#pos(@x), #pos(@y)) -> c_10(#natmult^#(@x, @y)) 40.54/11.57 , #mult^#(#pos(@x), #0()) -> c_11() 40.54/11.57 , #mult^#(#pos(@x), #neg(@y)) -> c_12(#natmult^#(@x, @y)) 40.54/11.57 , #mult^#(#0(), #pos(@y)) -> c_13() 40.54/11.57 , #mult^#(#0(), #0()) -> c_14() 40.54/11.57 , #mult^#(#0(), #neg(@y)) -> c_15() 40.54/11.57 , #mult^#(#neg(@x), #pos(@y)) -> c_16(#natmult^#(@x, @y)) 40.54/11.57 , #mult^#(#neg(@x), #0()) -> c_17() 40.54/11.57 , #mult^#(#neg(@x), #neg(@y)) -> c_18(#natmult^#(@x, @y)) 40.54/11.57 , #natmult^#(#0(), @y) -> c_8() 40.54/11.57 , #natmult^#(#s(@x), @y) -> c_9(#add^#(#pos(@y), #natmult(@x, @y))) 40.54/11.57 , #add^#(#pos(#s(#0())), @y) -> c_23(#succ^#(@y)) 40.54/11.57 , #add^#(#pos(#s(#s(@x))), @y) -> 40.54/11.57 c_24(#succ^#(#add(#pos(#s(@x)), @y))) 40.54/11.57 , #add^#(#0(), @y) -> c_25() 40.54/11.57 , #add^#(#neg(#s(#0())), @y) -> c_26(#pred^#(@y)) 40.54/11.57 , #add^#(#neg(#s(#s(@x))), @y) -> 40.54/11.57 c_27(#pred^#(#add(#pos(#s(@x)), @y))) 40.54/11.57 , #succ^#(#pos(#s(@x))) -> c_19() 40.54/11.57 , #succ^#(#0()) -> c_20() 40.54/11.57 , #succ^#(#neg(#s(#0()))) -> c_21() 40.54/11.57 , #succ^#(#neg(#s(#s(@x)))) -> c_22() 40.54/11.57 , #pred^#(#pos(#s(#0()))) -> c_28() 40.54/11.57 , #pred^#(#pos(#s(#s(@x)))) -> c_29() 40.54/11.57 , #pred^#(#0()) -> c_30() 40.54/11.57 , #pred^#(#neg(#s(@x))) -> c_31() } 40.54/11.57 Weak Trs: 40.54/11.57 { #natmult(#0(), @y) -> #0() 40.54/11.57 , #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) 40.54/11.57 , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) 40.54/11.57 , #mult(#pos(@x), #0()) -> #0() 40.54/11.57 , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) 40.54/11.57 , #mult(#0(), #pos(@y)) -> #0() 40.54/11.57 , #mult(#0(), #0()) -> #0() 40.54/11.57 , #mult(#0(), #neg(@y)) -> #0() 40.54/11.57 , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) 40.54/11.57 , #mult(#neg(@x), #0()) -> #0() 40.54/11.57 , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) 40.54/11.57 , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) 40.54/11.57 , #succ(#0()) -> #pos(#s(#0())) 40.54/11.57 , #succ(#neg(#s(#0()))) -> #0() 40.54/11.57 , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) 40.54/11.57 , #add(#pos(#s(#0())), @y) -> #succ(@y) 40.54/11.57 , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) 40.54/11.57 , #add(#0(), @y) -> @y 40.54/11.57 , #add(#neg(#s(#0())), @y) -> #pred(@y) 40.54/11.57 , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) 40.54/11.57 , #pred(#pos(#s(#0()))) -> #0() 40.54/11.57 , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) 40.54/11.57 , #pred(#0()) -> #neg(#s(#0())) 40.54/11.57 , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) } 40.54/11.57 Obligation: 40.54/11.57 innermost runtime complexity 40.54/11.57 Answer: 40.54/11.57 YES(O(1),O(n^2)) 40.54/11.57 40.54/11.57 We replace rewrite rules by usable rules: 40.54/11.57 40.54/11.57 Weak Usable Rules: 40.54/11.57 { #natmult(#0(), @y) -> #0() 40.54/11.57 , #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) 40.54/11.57 , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) 40.54/11.57 , #succ(#0()) -> #pos(#s(#0())) 40.54/11.57 , #succ(#neg(#s(#0()))) -> #0() 40.54/11.57 , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) 40.54/11.57 , #add(#pos(#s(#0())), @y) -> #succ(@y) 40.54/11.57 , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) 40.54/11.57 , #add(#0(), @y) -> @y 40.54/11.57 , #add(#neg(#s(#0())), @y) -> #pred(@y) 40.54/11.57 , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) 40.54/11.57 , #pred(#pos(#s(#0()))) -> #0() 40.54/11.57 , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) 40.54/11.57 , #pred(#0()) -> #neg(#s(#0())) 40.54/11.57 , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) } 40.54/11.57 40.54/11.57 We are left with following problem, upon which TcT provides the 40.54/11.57 certificate YES(O(1),O(n^2)). 40.54/11.57 40.54/11.57 Strict DPs: 40.54/11.57 { mult^#(@n, @l) -> c_1(mult#1^#(@l, @n)) 40.54/11.57 , mult#1^#(::(@x, @xs), @n) -> c_2(*^#(@n, @x), mult^#(@n, @xs)) 40.54/11.57 , mult#1^#(nil(), @n) -> c_3() 40.54/11.57 , *^#(@x, @y) -> c_4(#mult^#(@x, @y)) 40.54/11.57 , dyade#1^#(::(@x, @xs), @l2) -> 40.54/11.57 c_5(mult^#(@x, @l2), dyade^#(@xs, @l2)) 40.54/11.57 , dyade#1^#(nil(), @l2) -> c_6() 40.54/11.57 , dyade^#(@l1, @l2) -> c_7(dyade#1^#(@l1, @l2)) } 40.54/11.57 Weak DPs: 40.54/11.57 { #mult^#(#pos(@x), #pos(@y)) -> c_10(#natmult^#(@x, @y)) 40.54/11.57 , #mult^#(#pos(@x), #0()) -> c_11() 40.54/11.57 , #mult^#(#pos(@x), #neg(@y)) -> c_12(#natmult^#(@x, @y)) 40.54/11.57 , #mult^#(#0(), #pos(@y)) -> c_13() 40.54/11.57 , #mult^#(#0(), #0()) -> c_14() 40.54/11.57 , #mult^#(#0(), #neg(@y)) -> c_15() 40.54/11.57 , #mult^#(#neg(@x), #pos(@y)) -> c_16(#natmult^#(@x, @y)) 40.54/11.57 , #mult^#(#neg(@x), #0()) -> c_17() 40.54/11.57 , #mult^#(#neg(@x), #neg(@y)) -> c_18(#natmult^#(@x, @y)) 40.54/11.57 , #natmult^#(#0(), @y) -> c_8() 40.54/11.57 , #natmult^#(#s(@x), @y) -> c_9(#add^#(#pos(@y), #natmult(@x, @y))) 40.54/11.57 , #add^#(#pos(#s(#0())), @y) -> c_23(#succ^#(@y)) 40.54/11.57 , #add^#(#pos(#s(#s(@x))), @y) -> 40.54/11.57 c_24(#succ^#(#add(#pos(#s(@x)), @y))) 40.54/11.57 , #add^#(#0(), @y) -> c_25() 40.54/11.57 , #add^#(#neg(#s(#0())), @y) -> c_26(#pred^#(@y)) 40.54/11.57 , #add^#(#neg(#s(#s(@x))), @y) -> 40.54/11.57 c_27(#pred^#(#add(#pos(#s(@x)), @y))) 40.54/11.57 , #succ^#(#pos(#s(@x))) -> c_19() 40.54/11.57 , #succ^#(#0()) -> c_20() 40.54/11.57 , #succ^#(#neg(#s(#0()))) -> c_21() 40.54/11.57 , #succ^#(#neg(#s(#s(@x)))) -> c_22() 40.54/11.57 , #pred^#(#pos(#s(#0()))) -> c_28() 40.54/11.57 , #pred^#(#pos(#s(#s(@x)))) -> c_29() 40.54/11.57 , #pred^#(#0()) -> c_30() 40.54/11.57 , #pred^#(#neg(#s(@x))) -> c_31() } 40.54/11.57 Weak Trs: 40.54/11.57 { #natmult(#0(), @y) -> #0() 40.54/11.57 , #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) 40.54/11.57 , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) 40.54/11.57 , #succ(#0()) -> #pos(#s(#0())) 40.54/11.57 , #succ(#neg(#s(#0()))) -> #0() 40.54/11.57 , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) 40.54/11.57 , #add(#pos(#s(#0())), @y) -> #succ(@y) 40.54/11.57 , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) 40.54/11.57 , #add(#0(), @y) -> @y 40.54/11.57 , #add(#neg(#s(#0())), @y) -> #pred(@y) 40.54/11.57 , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) 40.54/11.57 , #pred(#pos(#s(#0()))) -> #0() 40.54/11.57 , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) 40.54/11.57 , #pred(#0()) -> #neg(#s(#0())) 40.54/11.57 , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) } 40.54/11.57 Obligation: 40.54/11.57 innermost runtime complexity 40.54/11.57 Answer: 40.54/11.57 YES(O(1),O(n^2)) 40.54/11.57 40.54/11.57 The weightgap principle applies (using the following constant 40.54/11.57 growth matrix-interpretation) 40.54/11.57 40.54/11.57 The following argument positions are usable: 40.54/11.57 Uargs(#succ) = {1}, Uargs(#add) = {2}, Uargs(#pred) = {1}, 40.54/11.57 Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_4) = {1}, 40.54/11.57 Uargs(c_5) = {1, 2}, Uargs(c_7) = {1}, Uargs(c_9) = {1}, 40.54/11.57 Uargs(#add^#) = {2}, Uargs(c_10) = {1}, Uargs(c_12) = {1}, 40.54/11.57 Uargs(c_16) = {1}, Uargs(c_18) = {1}, Uargs(#succ^#) = {1}, 40.54/11.57 Uargs(c_23) = {1}, Uargs(c_24) = {1}, Uargs(c_26) = {1}, 40.54/11.57 Uargs(#pred^#) = {1}, Uargs(c_27) = {1} 40.54/11.57 40.54/11.57 TcT has computed the following constructor-restricted matrix 40.54/11.57 interpretation. 40.54/11.57 40.54/11.57 [#natmult](x1, x2) = [0] 40.54/11.57 [0] 40.54/11.57 40.54/11.57 [::](x1, x2) = [1 2] x1 + [1 1] x2 + [2] 40.54/11.57 [0 1] [0 1] [1] 40.54/11.57 40.54/11.57 [#succ](x1) = [1 0] x1 + [0] 40.54/11.57 [0 0] [0] 40.54/11.57 40.54/11.57 [#pos](x1) = [0] 40.54/11.57 [0] 40.54/11.57 40.54/11.57 [#add](x1, x2) = [1 0] x2 + [0] 40.54/11.57 [0 2] [0] 40.54/11.57 40.54/11.57 [#0] = [0] 40.54/11.57 [0] 40.54/11.57 40.54/11.57 [#neg](x1) = [0] 40.54/11.57 [0] 40.54/11.57 40.54/11.57 [#pred](x1) = [1 0] x1 + [0] 40.54/11.57 [0 0] [0] 40.54/11.57 40.54/11.57 [#s](x1) = [0] 40.54/11.57 [0] 40.54/11.57 40.54/11.57 [nil] = [2] 40.54/11.57 [1] 40.54/11.57 40.54/11.57 [mult^#](x1, x2) = [1 1] x1 + [0 0] x2 + [1] 40.54/11.57 [2 2] [1 1] [1] 40.54/11.57 40.54/11.57 [c_1](x1) = [1 0] x1 + [1] 40.54/11.57 [0 1] [1] 40.54/11.57 40.54/11.57 [mult#1^#](x1, x2) = [0 0] x1 + [1 1] x2 + [1] 40.54/11.57 [1 2] [2 2] [2] 40.54/11.57 40.54/11.57 [c_2](x1, x2) = [1 0] x1 + [1 0] x2 + [1] 40.54/11.57 [0 1] [0 1] [1] 40.54/11.57 40.54/11.57 [*^#](x1, x2) = [0 0] x1 + [0 0] x2 + [1] 40.54/11.57 [2 2] [1 1] [1] 40.54/11.57 40.54/11.57 [c_3] = [0] 40.54/11.57 [1] 40.54/11.57 40.54/11.57 [c_4](x1) = [1 0] x1 + [1] 40.54/11.57 [0 1] [2] 40.54/11.57 40.54/11.57 [#mult^#](x1, x2) = [2] 40.54/11.57 [0] 40.54/11.57 40.54/11.57 [dyade#1^#](x1, x2) = [1 2] x1 + [1 1] x2 + [2] 40.54/11.57 [1 2] [2 2] [2] 40.54/11.57 40.54/11.57 [c_5](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 40.54/11.57 [0 1] [0 1] [1] 40.54/11.57 40.54/11.57 [dyade^#](x1, x2) = [1 2] x1 + [1 1] x2 + [2] 40.54/11.57 [1 2] [2 2] [2] 40.54/11.57 40.54/11.57 [c_6] = [1] 40.54/11.57 [1] 40.54/11.57 40.54/11.57 [c_7](x1) = [1 0] x1 + [1] 40.54/11.57 [0 1] [1] 40.54/11.57 40.54/11.57 [#natmult^#](x1, x2) = [2] 40.54/11.57 [0] 40.54/11.57 40.54/11.57 [c_8] = [1] 40.54/11.57 [0] 40.54/11.57 40.54/11.57 [c_9](x1) = [1 0] x1 + [2] 40.54/11.57 [0 1] [0] 40.54/11.57 40.54/11.57 [#add^#](x1, x2) = [2 0] x2 + [0] 40.54/11.57 [0 0] [0] 40.54/11.57 40.54/11.57 [c_10](x1) = [1 0] x1 + [0] 40.54/11.57 [0 1] [0] 40.54/11.57 40.54/11.57 [c_11] = [1] 40.54/11.57 [0] 40.54/11.57 40.54/11.57 [c_12](x1) = [1 0] x1 + [0] 40.54/11.57 [0 1] [0] 40.54/11.57 40.54/11.57 [c_13] = [1] 40.54/11.57 [0] 40.54/11.57 40.54/11.57 [c_14] = [1] 40.54/11.57 [0] 40.54/11.57 40.54/11.57 [c_15] = [1] 40.54/11.57 [0] 40.54/11.57 40.54/11.57 [c_16](x1) = [1 0] x1 + [0] 40.54/11.57 [0 1] [0] 40.54/11.57 40.54/11.57 [c_17] = [1] 40.54/11.57 [0] 40.54/11.57 40.54/11.57 [c_18](x1) = [1 0] x1 + [0] 40.54/11.57 [0 1] [0] 40.54/11.57 40.54/11.57 [#succ^#](x1) = [2 0] x1 + [0] 40.54/11.57 [0 0] [0] 40.54/11.57 40.54/11.57 [c_19] = [0] 40.54/11.57 [0] 40.54/11.57 40.54/11.57 [c_20] = [0] 40.54/11.57 [0] 40.54/11.57 40.54/11.57 [c_21] = [0] 40.54/11.57 [0] 40.54/11.57 40.54/11.57 [c_22] = [0] 40.54/11.57 [0] 40.54/11.57 40.54/11.57 [c_23](x1) = [1 0] x1 + [0] 40.54/11.57 [0 1] [0] 40.54/11.57 40.54/11.57 [c_24](x1) = [1 0] x1 + [0] 40.54/11.57 [0 1] [0] 40.54/11.57 40.54/11.57 [c_25] = [0] 40.54/11.57 [0] 40.54/11.57 40.54/11.57 [c_26](x1) = [1 0] x1 + [0] 40.54/11.57 [0 1] [0] 40.54/11.57 40.54/11.57 [#pred^#](x1) = [2 0] x1 + [0] 40.54/11.57 [0 0] [0] 40.54/11.57 40.54/11.57 [c_27](x1) = [1 0] x1 + [0] 40.54/11.57 [0 1] [0] 40.54/11.57 40.54/11.57 [c_28] = [0] 40.54/11.57 [0] 40.54/11.57 40.54/11.57 [c_29] = [0] 40.54/11.57 [0] 40.54/11.57 40.54/11.57 [c_30] = [0] 40.54/11.57 [0] 40.54/11.57 40.54/11.57 [c_31] = [0] 40.54/11.57 [0] 40.54/11.57 40.54/11.57 The order satisfies the following ordering constraints: 40.54/11.57 40.54/11.57 [#natmult(#0(), @y)] = [0] 40.54/11.57 [0] 40.54/11.57 >= [0] 40.54/11.57 [0] 40.54/11.57 = [#0()] 40.54/11.57 40.54/11.57 [#natmult(#s(@x), @y)] = [0] 40.54/11.57 [0] 40.54/11.57 >= [0] 40.54/11.57 [0] 40.54/11.57 = [#add(#pos(@y), #natmult(@x, @y))] 40.54/11.57 40.54/11.57 [#succ(#pos(#s(@x)))] = [0] 40.54/11.57 [0] 40.54/11.57 >= [0] 40.54/11.57 [0] 40.54/11.57 = [#pos(#s(#s(@x)))] 40.54/11.57 40.54/11.57 [#succ(#0())] = [0] 40.54/11.57 [0] 40.54/11.57 >= [0] 40.54/11.57 [0] 40.54/11.57 = [#pos(#s(#0()))] 40.54/11.57 40.54/11.57 [#succ(#neg(#s(#0())))] = [0] 40.54/11.57 [0] 40.54/11.57 >= [0] 40.54/11.57 [0] 40.54/11.57 = [#0()] 40.54/11.57 40.54/11.57 [#succ(#neg(#s(#s(@x))))] = [0] 40.54/11.57 [0] 40.54/11.57 >= [0] 40.54/11.57 [0] 40.54/11.57 = [#neg(#s(@x))] 40.54/11.57 40.54/11.57 [#add(#pos(#s(#0())), @y)] = [1 0] @y + [0] 40.54/11.57 [0 2] [0] 40.54/11.57 >= [1 0] @y + [0] 40.54/11.57 [0 0] [0] 40.54/11.57 = [#succ(@y)] 40.54/11.57 40.54/11.57 [#add(#pos(#s(#s(@x))), @y)] = [1 0] @y + [0] 40.54/11.57 [0 2] [0] 40.54/11.57 >= [1 0] @y + [0] 40.54/11.57 [0 0] [0] 40.54/11.57 = [#succ(#add(#pos(#s(@x)), @y))] 40.54/11.57 40.54/11.57 [#add(#0(), @y)] = [1 0] @y + [0] 40.54/11.57 [0 2] [0] 40.54/11.57 >= [1 0] @y + [0] 40.54/11.57 [0 1] [0] 40.54/11.57 = [@y] 40.54/11.57 40.54/11.57 [#add(#neg(#s(#0())), @y)] = [1 0] @y + [0] 40.54/11.57 [0 2] [0] 40.54/11.57 >= [1 0] @y + [0] 40.54/11.57 [0 0] [0] 40.54/11.57 = [#pred(@y)] 40.54/11.57 40.54/11.57 [#add(#neg(#s(#s(@x))), @y)] = [1 0] @y + [0] 40.54/11.57 [0 2] [0] 40.54/11.57 >= [1 0] @y + [0] 40.54/11.57 [0 0] [0] 40.54/11.57 = [#pred(#add(#pos(#s(@x)), @y))] 40.54/11.57 40.54/11.57 [#pred(#pos(#s(#0())))] = [0] 40.54/11.57 [0] 40.54/11.57 >= [0] 40.54/11.57 [0] 40.54/11.57 = [#0()] 40.54/11.57 40.54/11.57 [#pred(#pos(#s(#s(@x))))] = [0] 40.54/11.57 [0] 40.54/11.57 >= [0] 40.54/11.57 [0] 40.54/11.57 = [#pos(#s(@x))] 40.54/11.57 40.54/11.57 [#pred(#0())] = [0] 40.54/11.57 [0] 40.54/11.57 >= [0] 40.54/11.57 [0] 40.54/11.57 = [#neg(#s(#0()))] 40.54/11.57 40.54/11.57 [#pred(#neg(#s(@x)))] = [0] 40.54/11.57 [0] 40.54/11.57 >= [0] 40.54/11.58 [0] 40.54/11.58 = [#neg(#s(#s(@x)))] 40.54/11.58 40.54/11.58 [mult^#(@n, @l)] = [1 1] @n + [0 0] @l + [1] 40.54/11.58 [2 2] [1 1] [1] 40.54/11.58 ? [1 1] @n + [0 0] @l + [2] 40.54/11.58 [2 2] [1 2] [3] 40.54/11.58 = [c_1(mult#1^#(@l, @n))] 40.54/11.58 40.54/11.58 [mult#1^#(::(@x, @xs), @n)] = [0 0] @x + [0 0] @xs + [1 1] @n + [1] 40.54/11.58 [1 4] [1 3] [2 2] [6] 40.54/11.58 ? [0 0] @x + [0 0] @xs + [1 1] @n + [3] 40.54/11.58 [1 1] [1 1] [4 4] [3] 40.54/11.58 = [c_2(*^#(@n, @x), mult^#(@n, @xs))] 40.54/11.58 40.54/11.58 [mult#1^#(nil(), @n)] = [1 1] @n + [1] 40.54/11.58 [2 2] [6] 40.54/11.58 > [0] 40.54/11.58 [1] 40.54/11.58 = [c_3()] 40.54/11.58 40.54/11.58 [*^#(@x, @y)] = [0 0] @x + [0 0] @y + [1] 40.54/11.58 [2 2] [1 1] [1] 40.54/11.58 ? [3] 40.54/11.58 [2] 40.54/11.58 = [c_4(#mult^#(@x, @y))] 40.54/11.58 40.54/11.58 [#mult^#(#pos(@x), #pos(@y))] = [2] 40.54/11.58 [0] 40.54/11.58 >= [2] 40.54/11.58 [0] 40.54/11.58 = [c_10(#natmult^#(@x, @y))] 40.54/11.58 40.54/11.58 [#mult^#(#pos(@x), #0())] = [2] 40.54/11.58 [0] 40.54/11.58 > [1] 40.54/11.58 [0] 40.54/11.58 = [c_11()] 40.54/11.58 40.54/11.58 [#mult^#(#pos(@x), #neg(@y))] = [2] 40.54/11.58 [0] 40.54/11.58 >= [2] 40.54/11.58 [0] 40.54/11.58 = [c_12(#natmult^#(@x, @y))] 40.54/11.58 40.54/11.58 [#mult^#(#0(), #pos(@y))] = [2] 40.54/11.58 [0] 40.54/11.58 > [1] 40.54/11.58 [0] 40.54/11.58 = [c_13()] 40.54/11.58 40.54/11.58 [#mult^#(#0(), #0())] = [2] 40.54/11.58 [0] 40.54/11.58 > [1] 40.54/11.58 [0] 40.54/11.58 = [c_14()] 40.54/11.58 40.54/11.58 [#mult^#(#0(), #neg(@y))] = [2] 40.54/11.58 [0] 40.54/11.58 > [1] 40.54/11.58 [0] 40.54/11.58 = [c_15()] 40.54/11.58 40.54/11.58 [#mult^#(#neg(@x), #pos(@y))] = [2] 40.54/11.58 [0] 40.54/11.58 >= [2] 40.54/11.58 [0] 40.54/11.58 = [c_16(#natmult^#(@x, @y))] 40.54/11.58 40.54/11.58 [#mult^#(#neg(@x), #0())] = [2] 40.54/11.58 [0] 40.54/11.58 > [1] 40.54/11.58 [0] 40.54/11.58 = [c_17()] 40.54/11.58 40.54/11.58 [#mult^#(#neg(@x), #neg(@y))] = [2] 40.54/11.58 [0] 40.54/11.58 >= [2] 40.54/11.58 [0] 40.54/11.58 = [c_18(#natmult^#(@x, @y))] 40.54/11.58 40.54/11.58 [dyade#1^#(::(@x, @xs), @l2)] = [1 4] @x + [1 1] @l2 + [1 3] @xs + [6] 40.54/11.58 [1 4] [2 2] [1 3] [6] 40.54/11.58 ? [1 1] @x + [1 1] @l2 + [1 2] @xs + [3] 40.54/11.58 [2 2] [3 3] [1 2] [4] 40.54/11.58 = [c_5(mult^#(@x, @l2), dyade^#(@xs, @l2))] 40.54/11.58 40.54/11.58 [dyade#1^#(nil(), @l2)] = [1 1] @l2 + [6] 40.54/11.58 [2 2] [6] 40.54/11.58 > [1] 40.54/11.58 [1] 40.54/11.58 = [c_6()] 40.54/11.58 40.54/11.58 [dyade^#(@l1, @l2)] = [1 2] @l1 + [1 1] @l2 + [2] 40.54/11.58 [1 2] [2 2] [2] 40.54/11.58 ? [1 2] @l1 + [1 1] @l2 + [3] 40.54/11.58 [1 2] [2 2] [3] 40.54/11.58 = [c_7(dyade#1^#(@l1, @l2))] 40.54/11.58 40.54/11.58 [#natmult^#(#0(), @y)] = [2] 40.54/11.58 [0] 40.54/11.58 > [1] 40.54/11.58 [0] 40.54/11.58 = [c_8()] 40.54/11.58 40.54/11.58 [#natmult^#(#s(@x), @y)] = [2] 40.54/11.58 [0] 40.54/11.58 >= [2] 40.54/11.58 [0] 40.54/11.58 = [c_9(#add^#(#pos(@y), #natmult(@x, @y)))] 40.54/11.58 40.54/11.58 [#add^#(#pos(#s(#0())), @y)] = [2 0] @y + [0] 40.54/11.58 [0 0] [0] 40.54/11.58 >= [2 0] @y + [0] 40.54/11.58 [0 0] [0] 40.54/11.58 = [c_23(#succ^#(@y))] 40.54/11.58 40.54/11.58 [#add^#(#pos(#s(#s(@x))), @y)] = [2 0] @y + [0] 40.54/11.58 [0 0] [0] 40.54/11.58 >= [2 0] @y + [0] 40.54/11.58 [0 0] [0] 40.54/11.58 = [c_24(#succ^#(#add(#pos(#s(@x)), @y)))] 40.54/11.58 40.54/11.58 [#add^#(#0(), @y)] = [2 0] @y + [0] 40.54/11.58 [0 0] [0] 40.54/11.58 >= [0] 40.54/11.58 [0] 40.54/11.58 = [c_25()] 40.54/11.58 40.54/11.58 [#add^#(#neg(#s(#0())), @y)] = [2 0] @y + [0] 40.54/11.58 [0 0] [0] 40.54/11.58 >= [2 0] @y + [0] 40.54/11.58 [0 0] [0] 40.54/11.58 = [c_26(#pred^#(@y))] 40.54/11.58 40.54/11.58 [#add^#(#neg(#s(#s(@x))), @y)] = [2 0] @y + [0] 40.54/11.58 [0 0] [0] 40.54/11.58 >= [2 0] @y + [0] 40.54/11.58 [0 0] [0] 40.54/11.58 = [c_27(#pred^#(#add(#pos(#s(@x)), @y)))] 40.54/11.58 40.54/11.58 [#succ^#(#pos(#s(@x)))] = [0] 40.54/11.58 [0] 40.54/11.58 >= [0] 40.54/11.58 [0] 40.54/11.58 = [c_19()] 40.54/11.58 40.54/11.58 [#succ^#(#0())] = [0] 40.54/11.58 [0] 40.54/11.58 >= [0] 40.54/11.58 [0] 40.54/11.58 = [c_20()] 40.54/11.58 40.54/11.58 [#succ^#(#neg(#s(#0())))] = [0] 40.54/11.58 [0] 40.54/11.58 >= [0] 40.54/11.58 [0] 40.54/11.58 = [c_21()] 40.54/11.58 40.54/11.58 [#succ^#(#neg(#s(#s(@x))))] = [0] 40.54/11.58 [0] 40.54/11.58 >= [0] 40.54/11.58 [0] 40.54/11.58 = [c_22()] 40.54/11.58 40.54/11.58 [#pred^#(#pos(#s(#0())))] = [0] 40.54/11.58 [0] 40.54/11.58 >= [0] 40.54/11.58 [0] 40.54/11.58 = [c_28()] 40.54/11.58 40.54/11.58 [#pred^#(#pos(#s(#s(@x))))] = [0] 40.54/11.58 [0] 40.54/11.58 >= [0] 40.54/11.58 [0] 40.54/11.58 = [c_29()] 40.54/11.58 40.54/11.58 [#pred^#(#0())] = [0] 40.54/11.58 [0] 40.54/11.58 >= [0] 40.54/11.58 [0] 40.54/11.58 = [c_30()] 40.54/11.58 40.54/11.58 [#pred^#(#neg(#s(@x)))] = [0] 40.54/11.58 [0] 40.54/11.58 >= [0] 40.54/11.58 [0] 40.54/11.58 = [c_31()] 40.54/11.58 40.54/11.58 40.54/11.58 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 40.54/11.58 40.54/11.58 We are left with following problem, upon which TcT provides the 40.54/11.58 certificate YES(O(1),O(n^2)). 40.54/11.58 40.54/11.58 Strict DPs: 40.54/11.58 { mult^#(@n, @l) -> c_1(mult#1^#(@l, @n)) 40.54/11.58 , mult#1^#(::(@x, @xs), @n) -> c_2(*^#(@n, @x), mult^#(@n, @xs)) 40.54/11.58 , *^#(@x, @y) -> c_4(#mult^#(@x, @y)) 40.54/11.58 , dyade#1^#(::(@x, @xs), @l2) -> 40.54/11.58 c_5(mult^#(@x, @l2), dyade^#(@xs, @l2)) 40.54/11.58 , dyade^#(@l1, @l2) -> c_7(dyade#1^#(@l1, @l2)) } 40.54/11.58 Weak DPs: 40.54/11.58 { mult#1^#(nil(), @n) -> c_3() 40.54/11.58 , #mult^#(#pos(@x), #pos(@y)) -> c_10(#natmult^#(@x, @y)) 40.54/11.58 , #mult^#(#pos(@x), #0()) -> c_11() 40.54/11.58 , #mult^#(#pos(@x), #neg(@y)) -> c_12(#natmult^#(@x, @y)) 40.54/11.58 , #mult^#(#0(), #pos(@y)) -> c_13() 40.54/11.58 , #mult^#(#0(), #0()) -> c_14() 40.54/11.58 , #mult^#(#0(), #neg(@y)) -> c_15() 40.54/11.58 , #mult^#(#neg(@x), #pos(@y)) -> c_16(#natmult^#(@x, @y)) 40.54/11.58 , #mult^#(#neg(@x), #0()) -> c_17() 40.54/11.58 , #mult^#(#neg(@x), #neg(@y)) -> c_18(#natmult^#(@x, @y)) 40.54/11.58 , dyade#1^#(nil(), @l2) -> c_6() 40.54/11.58 , #natmult^#(#0(), @y) -> c_8() 40.54/11.58 , #natmult^#(#s(@x), @y) -> c_9(#add^#(#pos(@y), #natmult(@x, @y))) 40.54/11.58 , #add^#(#pos(#s(#0())), @y) -> c_23(#succ^#(@y)) 40.54/11.58 , #add^#(#pos(#s(#s(@x))), @y) -> 40.54/11.58 c_24(#succ^#(#add(#pos(#s(@x)), @y))) 40.54/11.58 , #add^#(#0(), @y) -> c_25() 40.54/11.58 , #add^#(#neg(#s(#0())), @y) -> c_26(#pred^#(@y)) 40.54/11.58 , #add^#(#neg(#s(#s(@x))), @y) -> 40.54/11.58 c_27(#pred^#(#add(#pos(#s(@x)), @y))) 40.54/11.58 , #succ^#(#pos(#s(@x))) -> c_19() 40.54/11.58 , #succ^#(#0()) -> c_20() 40.54/11.58 , #succ^#(#neg(#s(#0()))) -> c_21() 40.54/11.58 , #succ^#(#neg(#s(#s(@x)))) -> c_22() 40.54/11.58 , #pred^#(#pos(#s(#0()))) -> c_28() 40.54/11.58 , #pred^#(#pos(#s(#s(@x)))) -> c_29() 40.54/11.58 , #pred^#(#0()) -> c_30() 40.54/11.58 , #pred^#(#neg(#s(@x))) -> c_31() } 40.54/11.58 Weak Trs: 40.54/11.58 { #natmult(#0(), @y) -> #0() 40.54/11.58 , #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) 40.54/11.58 , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) 40.54/11.58 , #succ(#0()) -> #pos(#s(#0())) 40.54/11.58 , #succ(#neg(#s(#0()))) -> #0() 40.54/11.58 , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) 40.54/11.58 , #add(#pos(#s(#0())), @y) -> #succ(@y) 40.54/11.58 , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) 40.54/11.58 , #add(#0(), @y) -> @y 40.54/11.58 , #add(#neg(#s(#0())), @y) -> #pred(@y) 40.54/11.58 , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) 40.54/11.58 , #pred(#pos(#s(#0()))) -> #0() 40.54/11.58 , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) 40.54/11.58 , #pred(#0()) -> #neg(#s(#0())) 40.54/11.58 , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) } 40.54/11.58 Obligation: 40.54/11.58 innermost runtime complexity 40.54/11.58 Answer: 40.54/11.58 YES(O(1),O(n^2)) 40.54/11.58 40.54/11.58 We estimate the number of application of {3} by applications of 40.54/11.58 Pre({3}) = {2}. Here rules are labeled as follows: 40.54/11.58 40.54/11.58 DPs: 40.54/11.58 { 1: mult^#(@n, @l) -> c_1(mult#1^#(@l, @n)) 40.54/11.58 , 2: mult#1^#(::(@x, @xs), @n) -> c_2(*^#(@n, @x), mult^#(@n, @xs)) 40.54/11.58 , 3: *^#(@x, @y) -> c_4(#mult^#(@x, @y)) 40.54/11.58 , 4: dyade#1^#(::(@x, @xs), @l2) -> 40.54/11.58 c_5(mult^#(@x, @l2), dyade^#(@xs, @l2)) 40.54/11.58 , 5: dyade^#(@l1, @l2) -> c_7(dyade#1^#(@l1, @l2)) 40.54/11.58 , 6: mult#1^#(nil(), @n) -> c_3() 40.54/11.58 , 7: #mult^#(#pos(@x), #pos(@y)) -> c_10(#natmult^#(@x, @y)) 40.54/11.58 , 8: #mult^#(#pos(@x), #0()) -> c_11() 40.54/11.58 , 9: #mult^#(#pos(@x), #neg(@y)) -> c_12(#natmult^#(@x, @y)) 40.54/11.58 , 10: #mult^#(#0(), #pos(@y)) -> c_13() 40.54/11.58 , 11: #mult^#(#0(), #0()) -> c_14() 40.54/11.58 , 12: #mult^#(#0(), #neg(@y)) -> c_15() 40.54/11.58 , 13: #mult^#(#neg(@x), #pos(@y)) -> c_16(#natmult^#(@x, @y)) 40.54/11.58 , 14: #mult^#(#neg(@x), #0()) -> c_17() 40.54/11.58 , 15: #mult^#(#neg(@x), #neg(@y)) -> c_18(#natmult^#(@x, @y)) 40.54/11.58 , 16: dyade#1^#(nil(), @l2) -> c_6() 40.54/11.58 , 17: #natmult^#(#0(), @y) -> c_8() 40.54/11.58 , 18: #natmult^#(#s(@x), @y) -> 40.54/11.58 c_9(#add^#(#pos(@y), #natmult(@x, @y))) 40.54/11.58 , 19: #add^#(#pos(#s(#0())), @y) -> c_23(#succ^#(@y)) 40.54/11.58 , 20: #add^#(#pos(#s(#s(@x))), @y) -> 40.54/11.58 c_24(#succ^#(#add(#pos(#s(@x)), @y))) 40.54/11.58 , 21: #add^#(#0(), @y) -> c_25() 40.54/11.58 , 22: #add^#(#neg(#s(#0())), @y) -> c_26(#pred^#(@y)) 40.54/11.58 , 23: #add^#(#neg(#s(#s(@x))), @y) -> 40.54/11.58 c_27(#pred^#(#add(#pos(#s(@x)), @y))) 40.54/11.58 , 24: #succ^#(#pos(#s(@x))) -> c_19() 40.54/11.58 , 25: #succ^#(#0()) -> c_20() 40.54/11.58 , 26: #succ^#(#neg(#s(#0()))) -> c_21() 40.54/11.58 , 27: #succ^#(#neg(#s(#s(@x)))) -> c_22() 40.54/11.58 , 28: #pred^#(#pos(#s(#0()))) -> c_28() 40.54/11.58 , 29: #pred^#(#pos(#s(#s(@x)))) -> c_29() 40.54/11.58 , 30: #pred^#(#0()) -> c_30() 40.54/11.58 , 31: #pred^#(#neg(#s(@x))) -> c_31() } 40.54/11.58 40.54/11.58 We are left with following problem, upon which TcT provides the 40.54/11.58 certificate YES(O(1),O(n^2)). 40.54/11.58 40.54/11.58 Strict DPs: 40.54/11.58 { mult^#(@n, @l) -> c_1(mult#1^#(@l, @n)) 40.54/11.58 , mult#1^#(::(@x, @xs), @n) -> c_2(*^#(@n, @x), mult^#(@n, @xs)) 40.54/11.58 , dyade#1^#(::(@x, @xs), @l2) -> 40.54/11.58 c_5(mult^#(@x, @l2), dyade^#(@xs, @l2)) 40.54/11.58 , dyade^#(@l1, @l2) -> c_7(dyade#1^#(@l1, @l2)) } 40.54/11.58 Weak DPs: 40.54/11.58 { mult#1^#(nil(), @n) -> c_3() 40.54/11.58 , *^#(@x, @y) -> c_4(#mult^#(@x, @y)) 40.54/11.58 , #mult^#(#pos(@x), #pos(@y)) -> c_10(#natmult^#(@x, @y)) 40.54/11.58 , #mult^#(#pos(@x), #0()) -> c_11() 40.54/11.58 , #mult^#(#pos(@x), #neg(@y)) -> c_12(#natmult^#(@x, @y)) 40.54/11.58 , #mult^#(#0(), #pos(@y)) -> c_13() 40.54/11.58 , #mult^#(#0(), #0()) -> c_14() 40.54/11.58 , #mult^#(#0(), #neg(@y)) -> c_15() 40.54/11.58 , #mult^#(#neg(@x), #pos(@y)) -> c_16(#natmult^#(@x, @y)) 40.54/11.58 , #mult^#(#neg(@x), #0()) -> c_17() 40.54/11.58 , #mult^#(#neg(@x), #neg(@y)) -> c_18(#natmult^#(@x, @y)) 40.54/11.58 , dyade#1^#(nil(), @l2) -> c_6() 40.54/11.58 , #natmult^#(#0(), @y) -> c_8() 40.54/11.58 , #natmult^#(#s(@x), @y) -> c_9(#add^#(#pos(@y), #natmult(@x, @y))) 40.54/11.58 , #add^#(#pos(#s(#0())), @y) -> c_23(#succ^#(@y)) 40.54/11.58 , #add^#(#pos(#s(#s(@x))), @y) -> 40.54/11.58 c_24(#succ^#(#add(#pos(#s(@x)), @y))) 40.54/11.58 , #add^#(#0(), @y) -> c_25() 40.54/11.58 , #add^#(#neg(#s(#0())), @y) -> c_26(#pred^#(@y)) 40.54/11.58 , #add^#(#neg(#s(#s(@x))), @y) -> 40.54/11.58 c_27(#pred^#(#add(#pos(#s(@x)), @y))) 40.54/11.58 , #succ^#(#pos(#s(@x))) -> c_19() 40.54/11.58 , #succ^#(#0()) -> c_20() 40.54/11.58 , #succ^#(#neg(#s(#0()))) -> c_21() 40.54/11.58 , #succ^#(#neg(#s(#s(@x)))) -> c_22() 40.54/11.58 , #pred^#(#pos(#s(#0()))) -> c_28() 40.54/11.58 , #pred^#(#pos(#s(#s(@x)))) -> c_29() 40.54/11.58 , #pred^#(#0()) -> c_30() 40.54/11.58 , #pred^#(#neg(#s(@x))) -> c_31() } 40.54/11.58 Weak Trs: 40.54/11.58 { #natmult(#0(), @y) -> #0() 40.54/11.58 , #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) 40.54/11.58 , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) 40.54/11.58 , #succ(#0()) -> #pos(#s(#0())) 40.54/11.58 , #succ(#neg(#s(#0()))) -> #0() 40.54/11.58 , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) 40.54/11.58 , #add(#pos(#s(#0())), @y) -> #succ(@y) 40.54/11.58 , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) 40.54/11.58 , #add(#0(), @y) -> @y 40.54/11.58 , #add(#neg(#s(#0())), @y) -> #pred(@y) 40.54/11.58 , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) 40.54/11.58 , #pred(#pos(#s(#0()))) -> #0() 40.54/11.58 , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) 40.54/11.58 , #pred(#0()) -> #neg(#s(#0())) 40.54/11.58 , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) } 40.54/11.58 Obligation: 40.54/11.58 innermost runtime complexity 40.54/11.58 Answer: 40.54/11.58 YES(O(1),O(n^2)) 40.54/11.58 40.54/11.58 The following weak DPs constitute a sub-graph of the DG that is 40.54/11.58 closed under successors. The DPs are removed. 40.54/11.58 40.54/11.58 { mult#1^#(nil(), @n) -> c_3() 40.54/11.58 , *^#(@x, @y) -> c_4(#mult^#(@x, @y)) 40.54/11.58 , #mult^#(#pos(@x), #pos(@y)) -> c_10(#natmult^#(@x, @y)) 40.54/11.58 , #mult^#(#pos(@x), #0()) -> c_11() 40.54/11.58 , #mult^#(#pos(@x), #neg(@y)) -> c_12(#natmult^#(@x, @y)) 40.54/11.58 , #mult^#(#0(), #pos(@y)) -> c_13() 40.54/11.58 , #mult^#(#0(), #0()) -> c_14() 40.54/11.58 , #mult^#(#0(), #neg(@y)) -> c_15() 40.54/11.58 , #mult^#(#neg(@x), #pos(@y)) -> c_16(#natmult^#(@x, @y)) 40.54/11.58 , #mult^#(#neg(@x), #0()) -> c_17() 40.54/11.58 , #mult^#(#neg(@x), #neg(@y)) -> c_18(#natmult^#(@x, @y)) 40.54/11.58 , dyade#1^#(nil(), @l2) -> c_6() 40.54/11.58 , #natmult^#(#0(), @y) -> c_8() 40.54/11.58 , #natmult^#(#s(@x), @y) -> c_9(#add^#(#pos(@y), #natmult(@x, @y))) 40.54/11.58 , #add^#(#pos(#s(#0())), @y) -> c_23(#succ^#(@y)) 40.54/11.58 , #add^#(#pos(#s(#s(@x))), @y) -> 40.54/11.58 c_24(#succ^#(#add(#pos(#s(@x)), @y))) 40.54/11.58 , #add^#(#0(), @y) -> c_25() 40.54/11.58 , #add^#(#neg(#s(#0())), @y) -> c_26(#pred^#(@y)) 40.54/11.58 , #add^#(#neg(#s(#s(@x))), @y) -> 40.54/11.58 c_27(#pred^#(#add(#pos(#s(@x)), @y))) 40.54/11.58 , #succ^#(#pos(#s(@x))) -> c_19() 40.54/11.58 , #succ^#(#0()) -> c_20() 40.54/11.58 , #succ^#(#neg(#s(#0()))) -> c_21() 40.54/11.58 , #succ^#(#neg(#s(#s(@x)))) -> c_22() 40.54/11.58 , #pred^#(#pos(#s(#0()))) -> c_28() 40.54/11.58 , #pred^#(#pos(#s(#s(@x)))) -> c_29() 40.54/11.58 , #pred^#(#0()) -> c_30() 40.54/11.58 , #pred^#(#neg(#s(@x))) -> c_31() } 40.54/11.58 40.54/11.58 We are left with following problem, upon which TcT provides the 40.54/11.58 certificate YES(O(1),O(n^2)). 40.54/11.58 40.54/11.58 Strict DPs: 40.54/11.58 { mult^#(@n, @l) -> c_1(mult#1^#(@l, @n)) 40.54/11.58 , mult#1^#(::(@x, @xs), @n) -> c_2(*^#(@n, @x), mult^#(@n, @xs)) 40.54/11.58 , dyade#1^#(::(@x, @xs), @l2) -> 40.54/11.58 c_5(mult^#(@x, @l2), dyade^#(@xs, @l2)) 40.54/11.58 , dyade^#(@l1, @l2) -> c_7(dyade#1^#(@l1, @l2)) } 40.54/11.58 Weak Trs: 40.54/11.58 { #natmult(#0(), @y) -> #0() 40.54/11.58 , #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) 40.54/11.58 , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) 40.54/11.58 , #succ(#0()) -> #pos(#s(#0())) 40.54/11.58 , #succ(#neg(#s(#0()))) -> #0() 40.54/11.58 , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) 40.54/11.58 , #add(#pos(#s(#0())), @y) -> #succ(@y) 40.54/11.58 , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) 40.54/11.58 , #add(#0(), @y) -> @y 40.54/11.58 , #add(#neg(#s(#0())), @y) -> #pred(@y) 40.54/11.58 , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) 40.54/11.58 , #pred(#pos(#s(#0()))) -> #0() 40.54/11.58 , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) 40.54/11.58 , #pred(#0()) -> #neg(#s(#0())) 40.54/11.58 , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) } 40.54/11.58 Obligation: 40.54/11.58 innermost runtime complexity 40.54/11.58 Answer: 40.54/11.58 YES(O(1),O(n^2)) 40.54/11.58 40.54/11.58 Due to missing edges in the dependency-graph, the right-hand sides 40.54/11.58 of following rules could be simplified: 40.54/11.58 40.54/11.58 { mult#1^#(::(@x, @xs), @n) -> c_2(*^#(@n, @x), mult^#(@n, @xs)) } 40.54/11.58 40.54/11.58 We are left with following problem, upon which TcT provides the 40.54/11.58 certificate YES(O(1),O(n^2)). 40.54/11.58 40.54/11.58 Strict DPs: 40.54/11.58 { mult^#(@n, @l) -> c_1(mult#1^#(@l, @n)) 40.54/11.58 , mult#1^#(::(@x, @xs), @n) -> c_2(mult^#(@n, @xs)) 40.54/11.58 , dyade#1^#(::(@x, @xs), @l2) -> 40.54/11.58 c_3(mult^#(@x, @l2), dyade^#(@xs, @l2)) 40.54/11.58 , dyade^#(@l1, @l2) -> c_4(dyade#1^#(@l1, @l2)) } 40.54/11.58 Weak Trs: 40.54/11.58 { #natmult(#0(), @y) -> #0() 40.54/11.58 , #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) 40.54/11.58 , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) 40.54/11.58 , #succ(#0()) -> #pos(#s(#0())) 40.54/11.58 , #succ(#neg(#s(#0()))) -> #0() 40.54/11.58 , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) 40.54/11.58 , #add(#pos(#s(#0())), @y) -> #succ(@y) 40.54/11.58 , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) 40.54/11.58 , #add(#0(), @y) -> @y 40.54/11.58 , #add(#neg(#s(#0())), @y) -> #pred(@y) 40.54/11.58 , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) 40.54/11.58 , #pred(#pos(#s(#0()))) -> #0() 40.54/11.58 , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) 40.54/11.58 , #pred(#0()) -> #neg(#s(#0())) 40.54/11.58 , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) } 40.54/11.58 Obligation: 40.54/11.58 innermost runtime complexity 40.54/11.58 Answer: 40.54/11.58 YES(O(1),O(n^2)) 40.54/11.58 40.54/11.58 No rule is usable, rules are removed from the input problem. 40.54/11.58 40.54/11.58 We are left with following problem, upon which TcT provides the 40.54/11.58 certificate YES(O(1),O(n^2)). 40.54/11.58 40.54/11.58 Strict DPs: 40.54/11.58 { mult^#(@n, @l) -> c_1(mult#1^#(@l, @n)) 40.54/11.58 , mult#1^#(::(@x, @xs), @n) -> c_2(mult^#(@n, @xs)) 40.54/11.58 , dyade#1^#(::(@x, @xs), @l2) -> 40.54/11.58 c_3(mult^#(@x, @l2), dyade^#(@xs, @l2)) 40.54/11.58 , dyade^#(@l1, @l2) -> c_4(dyade#1^#(@l1, @l2)) } 40.54/11.58 Obligation: 40.54/11.58 innermost runtime complexity 40.54/11.58 Answer: 40.54/11.58 YES(O(1),O(n^2)) 40.54/11.58 40.54/11.58 We use the processor 'polynomial interpretation' to orient 40.54/11.58 following rules strictly. 40.54/11.58 40.54/11.58 DPs: 40.54/11.58 { 2: mult#1^#(::(@x, @xs), @n) -> c_2(mult^#(@n, @xs)) } 40.54/11.58 40.54/11.58 Sub-proof: 40.54/11.58 ---------- 40.54/11.58 We consider the following typing: 40.54/11.58 40.54/11.58 :: :: (a,b) -> b 40.54/11.58 mult^# :: (a,b) -> d 40.54/11.58 mult#1^# :: (b,a) -> c 40.54/11.58 dyade#1^# :: (b,b) -> e 40.54/11.58 dyade^# :: (b,b) -> f 40.54/11.58 c_1 :: c -> d 40.54/11.58 c_2 :: d -> c 40.54/11.58 c_3 :: (d,f) -> e 40.54/11.58 c_4 :: e -> f 40.54/11.58 40.54/11.58 The following argument positions are considered usable: 40.54/11.58 40.54/11.58 Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1, 2}, 40.54/11.58 Uargs(c_4) = {1} 40.54/11.58 40.54/11.58 TcT has computed the following constructor-restricted 40.54/11.58 typedpolynomial interpretation. 40.54/11.58 40.54/11.58 [::](x1, x2) = 1 + x2 40.54/11.58 40.54/11.58 [mult^#](x1, x2) = x2 40.54/11.58 40.54/11.58 [mult#1^#](x1, x2) = x1 40.54/11.58 40.54/11.58 [dyade#1^#](x1, x2) = x1*x2 40.54/11.58 40.54/11.58 [dyade^#](x1, x2) = x1*x2 40.54/11.58 40.54/11.58 [c_1](x1) = x1 40.54/11.58 40.54/11.58 [c_2](x1) = x1 40.54/11.58 40.54/11.58 [c_3](x1, x2) = x1 + x2 40.54/11.58 40.54/11.58 [c_4](x1) = x1 40.54/11.58 40.54/11.58 40.54/11.58 This order satisfies the following ordering constraints. 40.54/11.58 40.54/11.58 [mult^#(@n, @l)] = @l 40.54/11.58 >= @l 40.54/11.58 = [c_1(mult#1^#(@l, @n))] 40.54/11.58 40.54/11.58 [mult#1^#(::(@x, @xs), @n)] = 1 + @xs 40.54/11.58 > @xs 40.54/11.58 = [c_2(mult^#(@n, @xs))] 40.54/11.58 40.54/11.58 [dyade#1^#(::(@x, @xs), @l2)] = @l2 + @xs*@l2 40.54/11.58 >= @l2 + @xs*@l2 40.54/11.58 = [c_3(mult^#(@x, @l2), dyade^#(@xs, @l2))] 40.54/11.58 40.54/11.58 [dyade^#(@l1, @l2)] = @l1*@l2 40.54/11.58 >= @l1*@l2 40.54/11.58 = [c_4(dyade#1^#(@l1, @l2))] 40.54/11.58 40.54/11.58 40.54/11.58 The strictly oriented rules are moved into the weak component. 40.54/11.58 40.54/11.58 We are left with following problem, upon which TcT provides the 40.54/11.58 certificate YES(O(1),O(n^2)). 40.54/11.58 40.54/11.58 Strict DPs: 40.54/11.58 { mult^#(@n, @l) -> c_1(mult#1^#(@l, @n)) 40.54/11.58 , dyade#1^#(::(@x, @xs), @l2) -> 40.54/11.58 c_3(mult^#(@x, @l2), dyade^#(@xs, @l2)) 40.54/11.58 , dyade^#(@l1, @l2) -> c_4(dyade#1^#(@l1, @l2)) } 40.54/11.58 Weak DPs: { mult#1^#(::(@x, @xs), @n) -> c_2(mult^#(@n, @xs)) } 40.54/11.58 Obligation: 40.54/11.58 innermost runtime complexity 40.54/11.58 Answer: 40.54/11.58 YES(O(1),O(n^2)) 40.54/11.58 40.54/11.58 We use the processor 'polynomial interpretation' to orient 40.54/11.58 following rules strictly. 40.54/11.58 40.54/11.58 DPs: 40.54/11.58 { 2: dyade#1^#(::(@x, @xs), @l2) -> 40.54/11.58 c_3(mult^#(@x, @l2), dyade^#(@xs, @l2)) 40.54/11.58 , 4: mult#1^#(::(@x, @xs), @n) -> c_2(mult^#(@n, @xs)) } 40.54/11.58 40.54/11.58 Sub-proof: 40.54/11.58 ---------- 40.54/11.58 We consider the following typing: 40.54/11.58 40.54/11.58 :: :: (a,b) -> b 40.54/11.58 mult^# :: (a,b) -> d 40.54/11.58 mult#1^# :: (b,a) -> c 40.54/11.58 dyade#1^# :: (b,b) -> e 40.54/11.58 dyade^# :: (b,b) -> f 40.54/11.58 c_1 :: c -> d 40.54/11.58 c_2 :: d -> c 40.54/11.58 c_3 :: (d,f) -> e 40.54/11.58 c_4 :: e -> f 40.54/11.58 40.54/11.58 The following argument positions are considered usable: 40.54/11.58 40.54/11.58 Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1, 2}, 40.54/11.58 Uargs(c_4) = {1} 40.54/11.58 40.54/11.58 TcT has computed the following constructor-restricted 40.54/11.58 typedpolynomial interpretation. 40.54/11.58 40.54/11.58 [::](x1, x2) = 2 + x2 40.54/11.58 40.54/11.58 [mult^#](x1, x2) = x2 40.54/11.58 40.54/11.58 [mult#1^#](x1, x2) = x1 40.54/11.58 40.54/11.58 [dyade#1^#](x1, x2) = x1 + 2*x1*x2 40.54/11.58 40.54/11.58 [dyade^#](x1, x2) = x1 + 2*x1*x2 40.54/11.58 40.54/11.58 [c_1](x1) = x1 40.54/11.58 40.54/11.58 [c_2](x1) = x1 40.54/11.58 40.54/11.58 [c_3](x1, x2) = x1 + x2 40.54/11.58 40.54/11.58 [c_4](x1) = x1 40.54/11.58 40.54/11.58 40.54/11.58 This order satisfies the following ordering constraints. 40.54/11.58 40.54/11.58 [mult^#(@n, @l)] = @l 40.54/11.58 >= @l 40.54/11.58 = [c_1(mult#1^#(@l, @n))] 40.54/11.58 40.54/11.58 [mult#1^#(::(@x, @xs), @n)] = 2 + @xs 40.54/11.58 > @xs 40.54/11.58 = [c_2(mult^#(@n, @xs))] 40.54/11.58 40.54/11.58 [dyade#1^#(::(@x, @xs), @l2)] = 2 + @xs + 4*@l2 + 2*@xs*@l2 40.54/11.58 > @l2 + @xs + 2*@xs*@l2 40.54/11.58 = [c_3(mult^#(@x, @l2), dyade^#(@xs, @l2))] 40.54/11.58 40.54/11.58 [dyade^#(@l1, @l2)] = @l1 + 2*@l1*@l2 40.54/11.58 >= @l1 + 2*@l1*@l2 40.54/11.58 = [c_4(dyade#1^#(@l1, @l2))] 40.54/11.58 40.54/11.58 40.54/11.58 We return to the main proof. Consider the set of all dependency 40.54/11.58 pairs 40.54/11.58 40.54/11.58 : 40.54/11.58 { 1: mult^#(@n, @l) -> c_1(mult#1^#(@l, @n)) 40.54/11.58 , 2: dyade#1^#(::(@x, @xs), @l2) -> 40.54/11.58 c_3(mult^#(@x, @l2), dyade^#(@xs, @l2)) 40.54/11.58 , 3: dyade^#(@l1, @l2) -> c_4(dyade#1^#(@l1, @l2)) 40.54/11.58 , 4: mult#1^#(::(@x, @xs), @n) -> c_2(mult^#(@n, @xs)) } 40.54/11.58 40.54/11.58 Processor 'polynomial interpretation' induces the complexity 40.54/11.58 certificate YES(?,O(n^2)) on application of dependency pairs {2,4}. 40.54/11.58 These cover all (indirect) predecessors of dependency pairs 40.54/11.58 {1,2,3,4}, their number of application is equally bounded. The 40.54/11.58 dependency pairs are shifted into the weak component. 40.54/11.58 40.54/11.58 We are left with following problem, upon which TcT provides the 40.54/11.58 certificate YES(O(1),O(1)). 40.54/11.58 40.54/11.58 Weak DPs: 40.54/11.58 { mult^#(@n, @l) -> c_1(mult#1^#(@l, @n)) 40.54/11.58 , mult#1^#(::(@x, @xs), @n) -> c_2(mult^#(@n, @xs)) 40.54/11.58 , dyade#1^#(::(@x, @xs), @l2) -> 40.54/11.58 c_3(mult^#(@x, @l2), dyade^#(@xs, @l2)) 40.54/11.58 , dyade^#(@l1, @l2) -> c_4(dyade#1^#(@l1, @l2)) } 40.54/11.58 Obligation: 40.54/11.58 innermost runtime complexity 40.54/11.58 Answer: 40.54/11.58 YES(O(1),O(1)) 40.54/11.58 40.54/11.58 The following weak DPs constitute a sub-graph of the DG that is 40.54/11.58 closed under successors. The DPs are removed. 40.54/11.58 40.54/11.58 { mult^#(@n, @l) -> c_1(mult#1^#(@l, @n)) 40.54/11.58 , mult#1^#(::(@x, @xs), @n) -> c_2(mult^#(@n, @xs)) 40.54/11.58 , dyade#1^#(::(@x, @xs), @l2) -> 40.54/11.58 c_3(mult^#(@x, @l2), dyade^#(@xs, @l2)) 40.54/11.58 , dyade^#(@l1, @l2) -> c_4(dyade#1^#(@l1, @l2)) } 40.54/11.58 40.54/11.58 We are left with following problem, upon which TcT provides the 40.54/11.59 certificate YES(O(1),O(1)). 40.54/11.59 40.54/11.59 Rules: Empty 40.54/11.59 Obligation: 40.54/11.59 innermost runtime complexity 40.54/11.59 Answer: 40.54/11.59 YES(O(1),O(1)) 40.54/11.59 40.54/11.59 Empty rules are trivially bounded 40.54/11.59 40.54/11.59 Hurray, we answered YES(O(1),O(n^2)) 40.54/11.59 EOF