YES(O(1),O(n^2)) 555.06/148.07 YES(O(1),O(n^2)) 555.06/148.07 555.06/148.07 We are left with following problem, upon which TcT provides the 555.06/148.07 certificate YES(O(1),O(n^2)). 555.06/148.07 555.06/148.07 Strict Trs: 555.06/148.07 { #equal(@x, @y) -> #eq(@x, @y) 555.06/148.07 , -(@x, @y) -> #sub(@x, @y) 555.06/148.07 , eratos(@l) -> eratos#1(@l) 555.06/148.07 , div(@x, @y) -> #div(@x, @y) 555.06/148.07 , mod(@x, @y) -> -(@x, *(@x, div(@x, @y))) 555.06/148.07 , filter(@p, @l) -> filter#1(@l, @p) 555.06/148.07 , eratos#1(nil()) -> nil() 555.06/148.07 , eratos#1(::(@x, @xs)) -> ::(@x, eratos(filter(@x, @xs))) 555.06/148.07 , filter#3(#true(), @x, @xs') -> @xs' 555.06/148.07 , filter#3(#false(), @x, @xs') -> ::(@x, @xs') 555.06/148.07 , filter#1(nil(), @p) -> nil() 555.06/148.07 , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) 555.06/148.07 , *(@x, @y) -> #mult(@x, @y) 555.06/148.07 , filter#2(@xs', @p, @x) -> 555.06/148.07 filter#3(#equal(mod(@x, @p), #0()), @x, @xs') } 555.06/148.07 Weak Trs: 555.06/148.07 { #natsub(@x, #0()) -> @x 555.06/148.07 , #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) 555.06/148.07 , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) 555.06/148.07 , #eq(#pos(@x), #0()) -> #false() 555.06/148.07 , #eq(#pos(@x), #neg(@y)) -> #false() 555.06/148.07 , #eq(nil(), nil()) -> #true() 555.06/148.07 , #eq(nil(), ::(@y_1, @y_2)) -> #false() 555.06/148.07 , #eq(::(@x_1, @x_2), nil()) -> #false() 555.06/148.07 , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> 555.06/148.07 #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) 555.06/148.07 , #eq(#0(), #pos(@y)) -> #false() 555.06/148.07 , #eq(#0(), #0()) -> #true() 555.06/148.07 , #eq(#0(), #neg(@y)) -> #false() 555.06/148.07 , #eq(#0(), #s(@y)) -> #false() 555.06/148.07 , #eq(#neg(@x), #pos(@y)) -> #false() 555.06/148.07 , #eq(#neg(@x), #0()) -> #false() 555.06/148.07 , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) 555.06/148.07 , #eq(#s(@x), #0()) -> #false() 555.06/148.07 , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) 555.06/148.07 , #natmult(#0(), @y) -> #0() 555.06/148.07 , #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) 555.06/148.07 , #natdiv(#0(), #0()) -> #divByZero() 555.06/148.07 , #natdiv(#s(@x), #s(@y)) -> #s(#natdiv(#natsub(@x, @y), #s(@y))) 555.06/148.07 , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) 555.06/148.07 , #sub(@x, #0()) -> @x 555.06/148.07 , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) 555.06/148.07 , #add(#pos(#s(#0())), @y) -> #succ(@y) 555.06/148.07 , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) 555.06/148.07 , #add(#0(), @y) -> @y 555.06/148.07 , #add(#neg(#s(#0())), @y) -> #pred(@y) 555.06/148.07 , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) 555.06/148.07 , #and(#true(), #true()) -> #true() 555.06/148.07 , #and(#true(), #false()) -> #false() 555.06/148.07 , #and(#false(), #true()) -> #false() 555.06/148.07 , #and(#false(), #false()) -> #false() 555.06/148.07 , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) 555.06/148.07 , #mult(#pos(@x), #0()) -> #0() 555.06/148.07 , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) 555.06/148.07 , #mult(#0(), #pos(@y)) -> #0() 555.06/148.07 , #mult(#0(), #0()) -> #0() 555.06/148.07 , #mult(#0(), #neg(@y)) -> #0() 555.06/148.07 , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) 555.06/148.07 , #mult(#neg(@x), #0()) -> #0() 555.06/148.07 , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) 555.06/148.07 , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) 555.06/148.07 , #succ(#0()) -> #pos(#s(#0())) 555.06/148.07 , #succ(#neg(#s(#0()))) -> #0() 555.06/148.07 , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) 555.06/148.07 , #div(#pos(@x), #pos(@y)) -> #pos(#natdiv(@x, @y)) 555.06/148.07 , #div(#pos(@x), #0()) -> #divByZero() 555.06/148.07 , #div(#pos(@x), #neg(@y)) -> #neg(#natdiv(@x, @y)) 555.06/148.07 , #div(#0(), #pos(@y)) -> #0() 555.06/148.07 , #div(#0(), #0()) -> #divByZero() 555.06/148.07 , #div(#0(), #neg(@y)) -> #0() 555.06/148.07 , #div(#neg(@x), #pos(@y)) -> #neg(#natdiv(@x, @y)) 555.06/148.07 , #div(#neg(@x), #0()) -> #divByZero() 555.06/148.07 , #div(#neg(@x), #neg(@y)) -> #pos(#natdiv(@x, @y)) 555.06/148.07 , #pred(#pos(#s(#0()))) -> #0() 555.06/148.07 , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) 555.06/148.07 , #pred(#0()) -> #neg(#s(#0())) 555.06/148.07 , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) } 555.06/148.07 Obligation: 555.06/148.07 innermost runtime complexity 555.06/148.07 Answer: 555.06/148.07 YES(O(1),O(n^2)) 555.06/148.07 555.06/148.07 We add the following dependency tuples: 555.06/148.07 555.06/148.07 Strict DPs: 555.06/148.07 { #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) 555.06/148.07 , -^#(@x, @y) -> c_2(#sub^#(@x, @y)) 555.06/148.07 , eratos^#(@l) -> c_3(eratos#1^#(@l)) 555.06/148.07 , eratos#1^#(nil()) -> c_7() 555.06/148.07 , eratos#1^#(::(@x, @xs)) -> 555.06/148.07 c_8(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) 555.06/148.07 , div^#(@x, @y) -> c_4(#div^#(@x, @y)) 555.06/148.07 , mod^#(@x, @y) -> 555.06/148.07 c_5(-^#(@x, *(@x, div(@x, @y))), 555.06/148.07 *^#(@x, div(@x, @y)), 555.06/148.07 div^#(@x, @y)) 555.06/148.07 , *^#(@x, @y) -> c_13(#mult^#(@x, @y)) 555.06/148.07 , filter^#(@p, @l) -> c_6(filter#1^#(@l, @p)) 555.06/148.07 , filter#1^#(nil(), @p) -> c_11() 555.06/148.07 , filter#1^#(::(@x, @xs), @p) -> 555.06/148.07 c_12(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) 555.06/148.07 , filter#3^#(#true(), @x, @xs') -> c_9() 555.06/148.07 , filter#3^#(#false(), @x, @xs') -> c_10() 555.06/148.07 , filter#2^#(@xs', @p, @x) -> 555.06/148.07 c_14(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'), 555.06/148.07 #equal^#(mod(@x, @p), #0()), 555.06/148.07 mod^#(@x, @p)) } 555.06/148.07 Weak DPs: 555.06/148.07 { #eq^#(#pos(@x), #pos(@y)) -> c_17(#eq^#(@x, @y)) 555.06/148.07 , #eq^#(#pos(@x), #0()) -> c_18() 555.06/148.07 , #eq^#(#pos(@x), #neg(@y)) -> c_19() 555.06/148.07 , #eq^#(nil(), nil()) -> c_20() 555.06/148.07 , #eq^#(nil(), ::(@y_1, @y_2)) -> c_21() 555.06/148.07 , #eq^#(::(@x_1, @x_2), nil()) -> c_22() 555.06/148.07 , #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> 555.06/148.07 c_23(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), 555.06/148.07 #eq^#(@x_1, @y_1), 555.06/148.07 #eq^#(@x_2, @y_2)) 555.06/148.07 , #eq^#(#0(), #pos(@y)) -> c_24() 555.06/148.07 , #eq^#(#0(), #0()) -> c_25() 555.06/148.07 , #eq^#(#0(), #neg(@y)) -> c_26() 555.06/148.07 , #eq^#(#0(), #s(@y)) -> c_27() 555.06/148.07 , #eq^#(#neg(@x), #pos(@y)) -> c_28() 555.06/148.07 , #eq^#(#neg(@x), #0()) -> c_29() 555.06/148.07 , #eq^#(#neg(@x), #neg(@y)) -> c_30(#eq^#(@x, @y)) 555.06/148.07 , #eq^#(#s(@x), #0()) -> c_31() 555.06/148.07 , #eq^#(#s(@x), #s(@y)) -> c_32(#eq^#(@x, @y)) 555.06/148.07 , #sub^#(@x, #pos(@y)) -> c_37(#add^#(@x, #neg(@y))) 555.06/148.07 , #sub^#(@x, #0()) -> c_38() 555.06/148.07 , #sub^#(@x, #neg(@y)) -> c_39(#add^#(@x, #pos(@y))) 555.06/148.07 , #div^#(#pos(@x), #pos(@y)) -> c_62(#natdiv^#(@x, @y)) 555.06/148.07 , #div^#(#pos(@x), #0()) -> c_63() 555.06/148.07 , #div^#(#pos(@x), #neg(@y)) -> c_64(#natdiv^#(@x, @y)) 555.06/148.07 , #div^#(#0(), #pos(@y)) -> c_65() 555.06/148.07 , #div^#(#0(), #0()) -> c_66() 555.06/148.07 , #div^#(#0(), #neg(@y)) -> c_67() 555.06/148.07 , #div^#(#neg(@x), #pos(@y)) -> c_68(#natdiv^#(@x, @y)) 555.06/148.07 , #div^#(#neg(@x), #0()) -> c_69() 555.06/148.07 , #div^#(#neg(@x), #neg(@y)) -> c_70(#natdiv^#(@x, @y)) 555.06/148.07 , #mult^#(#pos(@x), #pos(@y)) -> c_49(#natmult^#(@x, @y)) 555.06/148.07 , #mult^#(#pos(@x), #0()) -> c_50() 555.06/148.07 , #mult^#(#pos(@x), #neg(@y)) -> c_51(#natmult^#(@x, @y)) 555.06/148.07 , #mult^#(#0(), #pos(@y)) -> c_52() 555.06/148.07 , #mult^#(#0(), #0()) -> c_53() 555.06/148.07 , #mult^#(#0(), #neg(@y)) -> c_54() 555.06/148.07 , #mult^#(#neg(@x), #pos(@y)) -> c_55(#natmult^#(@x, @y)) 555.06/148.07 , #mult^#(#neg(@x), #0()) -> c_56() 555.06/148.07 , #mult^#(#neg(@x), #neg(@y)) -> c_57(#natmult^#(@x, @y)) 555.06/148.07 , #natsub^#(@x, #0()) -> c_15() 555.06/148.07 , #natsub^#(#s(@x), #s(@y)) -> c_16(#natsub^#(@x, @y)) 555.06/148.07 , #and^#(#true(), #true()) -> c_45() 555.06/148.07 , #and^#(#true(), #false()) -> c_46() 555.06/148.07 , #and^#(#false(), #true()) -> c_47() 555.06/148.07 , #and^#(#false(), #false()) -> c_48() 555.06/148.07 , #natmult^#(#0(), @y) -> c_33() 555.06/148.07 , #natmult^#(#s(@x), @y) -> 555.06/148.07 c_34(#add^#(#pos(@y), #natmult(@x, @y)), #natmult^#(@x, @y)) 555.06/148.07 , #add^#(#pos(#s(#0())), @y) -> c_40(#succ^#(@y)) 555.06/148.07 , #add^#(#pos(#s(#s(@x))), @y) -> 555.06/148.07 c_41(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) 555.06/148.07 , #add^#(#0(), @y) -> c_42() 555.06/148.07 , #add^#(#neg(#s(#0())), @y) -> c_43(#pred^#(@y)) 555.06/148.07 , #add^#(#neg(#s(#s(@x))), @y) -> 555.06/148.07 c_44(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) 555.06/148.07 , #natdiv^#(#0(), #0()) -> c_35() 555.06/148.07 , #natdiv^#(#s(@x), #s(@y)) -> 555.06/148.07 c_36(#natdiv^#(#natsub(@x, @y), #s(@y)), #natsub^#(@x, @y)) 555.06/148.07 , #succ^#(#pos(#s(@x))) -> c_58() 555.06/148.07 , #succ^#(#0()) -> c_59() 555.06/148.07 , #succ^#(#neg(#s(#0()))) -> c_60() 555.06/148.07 , #succ^#(#neg(#s(#s(@x)))) -> c_61() 555.06/148.07 , #pred^#(#pos(#s(#0()))) -> c_71() 555.06/148.07 , #pred^#(#pos(#s(#s(@x)))) -> c_72() 555.06/148.07 , #pred^#(#0()) -> c_73() 555.06/148.07 , #pred^#(#neg(#s(@x))) -> c_74() } 555.06/148.07 555.06/148.07 and mark the set of starting terms. 555.06/148.07 555.06/148.07 We are left with following problem, upon which TcT provides the 555.06/148.07 certificate YES(O(1),O(n^2)). 555.06/148.07 555.06/148.07 Strict DPs: 555.06/148.07 { #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) 555.06/148.07 , -^#(@x, @y) -> c_2(#sub^#(@x, @y)) 555.06/148.07 , eratos^#(@l) -> c_3(eratos#1^#(@l)) 555.06/148.07 , eratos#1^#(nil()) -> c_7() 555.06/148.07 , eratos#1^#(::(@x, @xs)) -> 555.06/148.07 c_8(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) 555.06/148.07 , div^#(@x, @y) -> c_4(#div^#(@x, @y)) 555.06/148.07 , mod^#(@x, @y) -> 555.06/148.07 c_5(-^#(@x, *(@x, div(@x, @y))), 555.06/148.07 *^#(@x, div(@x, @y)), 555.06/148.07 div^#(@x, @y)) 555.06/148.07 , *^#(@x, @y) -> c_13(#mult^#(@x, @y)) 555.06/148.07 , filter^#(@p, @l) -> c_6(filter#1^#(@l, @p)) 555.06/148.07 , filter#1^#(nil(), @p) -> c_11() 555.06/148.07 , filter#1^#(::(@x, @xs), @p) -> 555.06/148.07 c_12(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) 555.06/148.07 , filter#3^#(#true(), @x, @xs') -> c_9() 555.06/148.07 , filter#3^#(#false(), @x, @xs') -> c_10() 555.06/148.07 , filter#2^#(@xs', @p, @x) -> 555.06/148.07 c_14(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'), 555.06/148.07 #equal^#(mod(@x, @p), #0()), 555.06/148.07 mod^#(@x, @p)) } 555.06/148.07 Weak DPs: 555.06/148.07 { #eq^#(#pos(@x), #pos(@y)) -> c_17(#eq^#(@x, @y)) 555.06/148.07 , #eq^#(#pos(@x), #0()) -> c_18() 555.06/148.07 , #eq^#(#pos(@x), #neg(@y)) -> c_19() 555.06/148.07 , #eq^#(nil(), nil()) -> c_20() 555.06/148.07 , #eq^#(nil(), ::(@y_1, @y_2)) -> c_21() 555.06/148.07 , #eq^#(::(@x_1, @x_2), nil()) -> c_22() 555.06/148.07 , #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> 555.06/148.07 c_23(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), 555.06/148.07 #eq^#(@x_1, @y_1), 555.06/148.07 #eq^#(@x_2, @y_2)) 555.06/148.07 , #eq^#(#0(), #pos(@y)) -> c_24() 555.06/148.07 , #eq^#(#0(), #0()) -> c_25() 555.06/148.07 , #eq^#(#0(), #neg(@y)) -> c_26() 555.06/148.07 , #eq^#(#0(), #s(@y)) -> c_27() 555.06/148.07 , #eq^#(#neg(@x), #pos(@y)) -> c_28() 555.06/148.07 , #eq^#(#neg(@x), #0()) -> c_29() 555.06/148.07 , #eq^#(#neg(@x), #neg(@y)) -> c_30(#eq^#(@x, @y)) 555.06/148.07 , #eq^#(#s(@x), #0()) -> c_31() 555.06/148.07 , #eq^#(#s(@x), #s(@y)) -> c_32(#eq^#(@x, @y)) 555.06/148.07 , #sub^#(@x, #pos(@y)) -> c_37(#add^#(@x, #neg(@y))) 555.06/148.07 , #sub^#(@x, #0()) -> c_38() 555.06/148.07 , #sub^#(@x, #neg(@y)) -> c_39(#add^#(@x, #pos(@y))) 555.06/148.07 , #div^#(#pos(@x), #pos(@y)) -> c_62(#natdiv^#(@x, @y)) 555.06/148.07 , #div^#(#pos(@x), #0()) -> c_63() 555.06/148.07 , #div^#(#pos(@x), #neg(@y)) -> c_64(#natdiv^#(@x, @y)) 555.06/148.07 , #div^#(#0(), #pos(@y)) -> c_65() 555.06/148.07 , #div^#(#0(), #0()) -> c_66() 555.06/148.07 , #div^#(#0(), #neg(@y)) -> c_67() 555.06/148.07 , #div^#(#neg(@x), #pos(@y)) -> c_68(#natdiv^#(@x, @y)) 555.06/148.07 , #div^#(#neg(@x), #0()) -> c_69() 555.06/148.07 , #div^#(#neg(@x), #neg(@y)) -> c_70(#natdiv^#(@x, @y)) 555.06/148.07 , #mult^#(#pos(@x), #pos(@y)) -> c_49(#natmult^#(@x, @y)) 555.06/148.07 , #mult^#(#pos(@x), #0()) -> c_50() 555.06/148.07 , #mult^#(#pos(@x), #neg(@y)) -> c_51(#natmult^#(@x, @y)) 555.06/148.07 , #mult^#(#0(), #pos(@y)) -> c_52() 555.06/148.07 , #mult^#(#0(), #0()) -> c_53() 555.06/148.07 , #mult^#(#0(), #neg(@y)) -> c_54() 555.06/148.07 , #mult^#(#neg(@x), #pos(@y)) -> c_55(#natmult^#(@x, @y)) 555.06/148.07 , #mult^#(#neg(@x), #0()) -> c_56() 555.06/148.07 , #mult^#(#neg(@x), #neg(@y)) -> c_57(#natmult^#(@x, @y)) 555.06/148.07 , #natsub^#(@x, #0()) -> c_15() 555.06/148.07 , #natsub^#(#s(@x), #s(@y)) -> c_16(#natsub^#(@x, @y)) 555.06/148.07 , #and^#(#true(), #true()) -> c_45() 555.06/148.07 , #and^#(#true(), #false()) -> c_46() 555.06/148.07 , #and^#(#false(), #true()) -> c_47() 555.06/148.07 , #and^#(#false(), #false()) -> c_48() 555.06/148.07 , #natmult^#(#0(), @y) -> c_33() 555.06/148.07 , #natmult^#(#s(@x), @y) -> 555.06/148.07 c_34(#add^#(#pos(@y), #natmult(@x, @y)), #natmult^#(@x, @y)) 555.06/148.07 , #add^#(#pos(#s(#0())), @y) -> c_40(#succ^#(@y)) 555.06/148.07 , #add^#(#pos(#s(#s(@x))), @y) -> 555.06/148.07 c_41(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) 555.06/148.07 , #add^#(#0(), @y) -> c_42() 555.06/148.07 , #add^#(#neg(#s(#0())), @y) -> c_43(#pred^#(@y)) 555.06/148.07 , #add^#(#neg(#s(#s(@x))), @y) -> 555.06/148.07 c_44(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) 555.06/148.07 , #natdiv^#(#0(), #0()) -> c_35() 555.06/148.07 , #natdiv^#(#s(@x), #s(@y)) -> 555.06/148.07 c_36(#natdiv^#(#natsub(@x, @y), #s(@y)), #natsub^#(@x, @y)) 555.06/148.07 , #succ^#(#pos(#s(@x))) -> c_58() 555.06/148.07 , #succ^#(#0()) -> c_59() 555.06/148.07 , #succ^#(#neg(#s(#0()))) -> c_60() 555.06/148.07 , #succ^#(#neg(#s(#s(@x)))) -> c_61() 555.06/148.07 , #pred^#(#pos(#s(#0()))) -> c_71() 555.06/148.07 , #pred^#(#pos(#s(#s(@x)))) -> c_72() 555.06/148.07 , #pred^#(#0()) -> c_73() 555.06/148.07 , #pred^#(#neg(#s(@x))) -> c_74() } 555.06/148.07 Weak Trs: 555.06/148.07 { #equal(@x, @y) -> #eq(@x, @y) 555.06/148.07 , #natsub(@x, #0()) -> @x 555.06/148.07 , #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) 555.06/148.07 , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) 555.06/148.07 , #eq(#pos(@x), #0()) -> #false() 555.06/148.07 , #eq(#pos(@x), #neg(@y)) -> #false() 555.06/148.07 , #eq(nil(), nil()) -> #true() 555.06/148.07 , #eq(nil(), ::(@y_1, @y_2)) -> #false() 555.06/148.07 , #eq(::(@x_1, @x_2), nil()) -> #false() 555.06/148.07 , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> 555.06/148.07 #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) 555.06/148.07 , #eq(#0(), #pos(@y)) -> #false() 555.06/148.07 , #eq(#0(), #0()) -> #true() 555.06/148.07 , #eq(#0(), #neg(@y)) -> #false() 555.06/148.07 , #eq(#0(), #s(@y)) -> #false() 555.06/148.07 , #eq(#neg(@x), #pos(@y)) -> #false() 555.06/148.07 , #eq(#neg(@x), #0()) -> #false() 555.06/148.07 , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) 555.06/148.07 , #eq(#s(@x), #0()) -> #false() 555.06/148.07 , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) 555.06/148.07 , #natmult(#0(), @y) -> #0() 555.06/148.07 , #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) 555.06/148.07 , -(@x, @y) -> #sub(@x, @y) 555.06/148.07 , eratos(@l) -> eratos#1(@l) 555.06/148.07 , #natdiv(#0(), #0()) -> #divByZero() 555.06/148.07 , #natdiv(#s(@x), #s(@y)) -> #s(#natdiv(#natsub(@x, @y), #s(@y))) 555.06/148.07 , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) 555.06/148.07 , #sub(@x, #0()) -> @x 555.06/148.07 , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) 555.06/148.07 , #add(#pos(#s(#0())), @y) -> #succ(@y) 555.06/148.07 , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) 555.06/148.07 , #add(#0(), @y) -> @y 555.06/148.07 , #add(#neg(#s(#0())), @y) -> #pred(@y) 555.06/148.07 , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) 555.06/148.07 , div(@x, @y) -> #div(@x, @y) 555.06/148.07 , mod(@x, @y) -> -(@x, *(@x, div(@x, @y))) 555.06/148.07 , filter(@p, @l) -> filter#1(@l, @p) 555.06/148.07 , eratos#1(nil()) -> nil() 555.06/148.07 , eratos#1(::(@x, @xs)) -> ::(@x, eratos(filter(@x, @xs))) 555.06/148.07 , #and(#true(), #true()) -> #true() 555.06/148.07 , #and(#true(), #false()) -> #false() 555.06/148.07 , #and(#false(), #true()) -> #false() 555.06/148.07 , #and(#false(), #false()) -> #false() 555.06/148.07 , filter#3(#true(), @x, @xs') -> @xs' 555.06/148.07 , filter#3(#false(), @x, @xs') -> ::(@x, @xs') 555.06/148.07 , filter#1(nil(), @p) -> nil() 555.06/148.07 , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) 555.06/148.07 , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) 555.06/148.07 , #mult(#pos(@x), #0()) -> #0() 555.06/148.07 , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) 555.06/148.07 , #mult(#0(), #pos(@y)) -> #0() 555.06/148.07 , #mult(#0(), #0()) -> #0() 555.06/148.07 , #mult(#0(), #neg(@y)) -> #0() 555.06/148.07 , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) 555.06/148.07 , #mult(#neg(@x), #0()) -> #0() 555.06/148.07 , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) 555.06/148.07 , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) 555.06/148.07 , #succ(#0()) -> #pos(#s(#0())) 555.06/148.07 , #succ(#neg(#s(#0()))) -> #0() 555.06/148.07 , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) 555.06/148.07 , #div(#pos(@x), #pos(@y)) -> #pos(#natdiv(@x, @y)) 555.06/148.07 , #div(#pos(@x), #0()) -> #divByZero() 555.06/148.07 , #div(#pos(@x), #neg(@y)) -> #neg(#natdiv(@x, @y)) 555.06/148.07 , #div(#0(), #pos(@y)) -> #0() 555.06/148.07 , #div(#0(), #0()) -> #divByZero() 555.06/148.07 , #div(#0(), #neg(@y)) -> #0() 555.06/148.07 , #div(#neg(@x), #pos(@y)) -> #neg(#natdiv(@x, @y)) 555.06/148.07 , #div(#neg(@x), #0()) -> #divByZero() 555.06/148.07 , #div(#neg(@x), #neg(@y)) -> #pos(#natdiv(@x, @y)) 555.06/148.07 , *(@x, @y) -> #mult(@x, @y) 555.06/148.07 , filter#2(@xs', @p, @x) -> 555.06/148.07 filter#3(#equal(mod(@x, @p), #0()), @x, @xs') 555.06/148.07 , #pred(#pos(#s(#0()))) -> #0() 555.06/148.07 , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) 555.06/148.07 , #pred(#0()) -> #neg(#s(#0())) 555.06/148.07 , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) } 555.06/148.07 Obligation: 555.06/148.07 innermost runtime complexity 555.06/148.07 Answer: 555.06/148.07 YES(O(1),O(n^2)) 555.06/148.07 555.06/148.07 We estimate the number of application of {1,2,4,6,8,10,12,13} by 555.06/148.07 applications of Pre({1,2,4,6,8,10,12,13}) = {3,7,9,14}. Here rules 555.06/148.07 are labeled as follows: 555.06/148.07 555.06/148.07 DPs: 555.06/148.07 { 1: #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) 555.06/148.07 , 2: -^#(@x, @y) -> c_2(#sub^#(@x, @y)) 555.06/148.07 , 3: eratos^#(@l) -> c_3(eratos#1^#(@l)) 555.06/148.07 , 4: eratos#1^#(nil()) -> c_7() 555.06/148.07 , 5: eratos#1^#(::(@x, @xs)) -> 555.06/148.07 c_8(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) 555.06/148.07 , 6: div^#(@x, @y) -> c_4(#div^#(@x, @y)) 555.06/148.07 , 7: mod^#(@x, @y) -> 555.06/148.07 c_5(-^#(@x, *(@x, div(@x, @y))), 555.06/148.07 *^#(@x, div(@x, @y)), 555.06/148.07 div^#(@x, @y)) 555.06/148.07 , 8: *^#(@x, @y) -> c_13(#mult^#(@x, @y)) 555.06/148.07 , 9: filter^#(@p, @l) -> c_6(filter#1^#(@l, @p)) 555.06/148.07 , 10: filter#1^#(nil(), @p) -> c_11() 555.06/148.07 , 11: filter#1^#(::(@x, @xs), @p) -> 555.06/148.07 c_12(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) 555.06/148.07 , 12: filter#3^#(#true(), @x, @xs') -> c_9() 555.06/148.07 , 13: filter#3^#(#false(), @x, @xs') -> c_10() 555.06/148.07 , 14: filter#2^#(@xs', @p, @x) -> 555.06/148.07 c_14(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'), 555.06/148.07 #equal^#(mod(@x, @p), #0()), 555.06/148.07 mod^#(@x, @p)) 555.06/148.07 , 15: #eq^#(#pos(@x), #pos(@y)) -> c_17(#eq^#(@x, @y)) 555.06/148.07 , 16: #eq^#(#pos(@x), #0()) -> c_18() 555.06/148.07 , 17: #eq^#(#pos(@x), #neg(@y)) -> c_19() 555.06/148.07 , 18: #eq^#(nil(), nil()) -> c_20() 555.06/148.07 , 19: #eq^#(nil(), ::(@y_1, @y_2)) -> c_21() 555.06/148.07 , 20: #eq^#(::(@x_1, @x_2), nil()) -> c_22() 555.06/148.07 , 21: #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> 555.06/148.07 c_23(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), 555.06/148.07 #eq^#(@x_1, @y_1), 555.06/148.07 #eq^#(@x_2, @y_2)) 555.06/148.07 , 22: #eq^#(#0(), #pos(@y)) -> c_24() 555.06/148.07 , 23: #eq^#(#0(), #0()) -> c_25() 555.06/148.07 , 24: #eq^#(#0(), #neg(@y)) -> c_26() 555.06/148.07 , 25: #eq^#(#0(), #s(@y)) -> c_27() 555.06/148.07 , 26: #eq^#(#neg(@x), #pos(@y)) -> c_28() 555.06/148.07 , 27: #eq^#(#neg(@x), #0()) -> c_29() 555.06/148.07 , 28: #eq^#(#neg(@x), #neg(@y)) -> c_30(#eq^#(@x, @y)) 555.06/148.07 , 29: #eq^#(#s(@x), #0()) -> c_31() 555.06/148.08 , 30: #eq^#(#s(@x), #s(@y)) -> c_32(#eq^#(@x, @y)) 555.06/148.08 , 31: #sub^#(@x, #pos(@y)) -> c_37(#add^#(@x, #neg(@y))) 555.06/148.08 , 32: #sub^#(@x, #0()) -> c_38() 555.06/148.08 , 33: #sub^#(@x, #neg(@y)) -> c_39(#add^#(@x, #pos(@y))) 555.06/148.08 , 34: #div^#(#pos(@x), #pos(@y)) -> c_62(#natdiv^#(@x, @y)) 555.06/148.08 , 35: #div^#(#pos(@x), #0()) -> c_63() 555.06/148.08 , 36: #div^#(#pos(@x), #neg(@y)) -> c_64(#natdiv^#(@x, @y)) 555.06/148.08 , 37: #div^#(#0(), #pos(@y)) -> c_65() 555.06/148.08 , 38: #div^#(#0(), #0()) -> c_66() 555.06/148.08 , 39: #div^#(#0(), #neg(@y)) -> c_67() 555.06/148.08 , 40: #div^#(#neg(@x), #pos(@y)) -> c_68(#natdiv^#(@x, @y)) 555.06/148.08 , 41: #div^#(#neg(@x), #0()) -> c_69() 555.06/148.08 , 42: #div^#(#neg(@x), #neg(@y)) -> c_70(#natdiv^#(@x, @y)) 555.06/148.08 , 43: #mult^#(#pos(@x), #pos(@y)) -> c_49(#natmult^#(@x, @y)) 555.06/148.08 , 44: #mult^#(#pos(@x), #0()) -> c_50() 555.06/148.08 , 45: #mult^#(#pos(@x), #neg(@y)) -> c_51(#natmult^#(@x, @y)) 555.06/148.08 , 46: #mult^#(#0(), #pos(@y)) -> c_52() 555.06/148.08 , 47: #mult^#(#0(), #0()) -> c_53() 555.06/148.08 , 48: #mult^#(#0(), #neg(@y)) -> c_54() 555.06/148.08 , 49: #mult^#(#neg(@x), #pos(@y)) -> c_55(#natmult^#(@x, @y)) 555.06/148.08 , 50: #mult^#(#neg(@x), #0()) -> c_56() 555.06/148.08 , 51: #mult^#(#neg(@x), #neg(@y)) -> c_57(#natmult^#(@x, @y)) 555.06/148.08 , 52: #natsub^#(@x, #0()) -> c_15() 555.06/148.08 , 53: #natsub^#(#s(@x), #s(@y)) -> c_16(#natsub^#(@x, @y)) 555.06/148.08 , 54: #and^#(#true(), #true()) -> c_45() 555.06/148.08 , 55: #and^#(#true(), #false()) -> c_46() 555.06/148.08 , 56: #and^#(#false(), #true()) -> c_47() 555.06/148.08 , 57: #and^#(#false(), #false()) -> c_48() 555.06/148.08 , 58: #natmult^#(#0(), @y) -> c_33() 555.06/148.08 , 59: #natmult^#(#s(@x), @y) -> 555.06/148.08 c_34(#add^#(#pos(@y), #natmult(@x, @y)), #natmult^#(@x, @y)) 555.06/148.08 , 60: #add^#(#pos(#s(#0())), @y) -> c_40(#succ^#(@y)) 555.06/148.08 , 61: #add^#(#pos(#s(#s(@x))), @y) -> 555.06/148.08 c_41(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) 555.06/148.08 , 62: #add^#(#0(), @y) -> c_42() 555.06/148.08 , 63: #add^#(#neg(#s(#0())), @y) -> c_43(#pred^#(@y)) 555.06/148.08 , 64: #add^#(#neg(#s(#s(@x))), @y) -> 555.06/148.08 c_44(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) 555.06/148.08 , 65: #natdiv^#(#0(), #0()) -> c_35() 555.06/148.08 , 66: #natdiv^#(#s(@x), #s(@y)) -> 555.06/148.08 c_36(#natdiv^#(#natsub(@x, @y), #s(@y)), #natsub^#(@x, @y)) 555.06/148.08 , 67: #succ^#(#pos(#s(@x))) -> c_58() 555.06/148.08 , 68: #succ^#(#0()) -> c_59() 555.06/148.08 , 69: #succ^#(#neg(#s(#0()))) -> c_60() 555.06/148.08 , 70: #succ^#(#neg(#s(#s(@x)))) -> c_61() 555.06/148.08 , 71: #pred^#(#pos(#s(#0()))) -> c_71() 555.06/148.08 , 72: #pred^#(#pos(#s(#s(@x)))) -> c_72() 555.06/148.08 , 73: #pred^#(#0()) -> c_73() 555.06/148.08 , 74: #pred^#(#neg(#s(@x))) -> c_74() } 555.06/148.08 555.06/148.08 We are left with following problem, upon which TcT provides the 555.06/148.08 certificate YES(O(1),O(n^2)). 555.06/148.08 555.06/148.08 Strict DPs: 555.06/148.08 { eratos^#(@l) -> c_3(eratos#1^#(@l)) 555.06/148.08 , eratos#1^#(::(@x, @xs)) -> 555.06/148.08 c_8(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) 555.06/148.08 , mod^#(@x, @y) -> 555.06/148.08 c_5(-^#(@x, *(@x, div(@x, @y))), 555.06/148.08 *^#(@x, div(@x, @y)), 555.06/148.08 div^#(@x, @y)) 555.06/148.08 , filter^#(@p, @l) -> c_6(filter#1^#(@l, @p)) 555.06/148.08 , filter#1^#(::(@x, @xs), @p) -> 555.06/148.08 c_12(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) 555.06/148.08 , filter#2^#(@xs', @p, @x) -> 555.06/148.08 c_14(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'), 555.06/148.08 #equal^#(mod(@x, @p), #0()), 555.06/148.08 mod^#(@x, @p)) } 555.06/148.08 Weak DPs: 555.06/148.08 { #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) 555.06/148.08 , #eq^#(#pos(@x), #pos(@y)) -> c_17(#eq^#(@x, @y)) 555.06/148.08 , #eq^#(#pos(@x), #0()) -> c_18() 555.06/148.08 , #eq^#(#pos(@x), #neg(@y)) -> c_19() 555.06/148.08 , #eq^#(nil(), nil()) -> c_20() 555.06/148.08 , #eq^#(nil(), ::(@y_1, @y_2)) -> c_21() 555.06/148.08 , #eq^#(::(@x_1, @x_2), nil()) -> c_22() 555.06/148.08 , #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> 555.06/148.08 c_23(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), 555.06/148.08 #eq^#(@x_1, @y_1), 555.06/148.08 #eq^#(@x_2, @y_2)) 555.06/148.08 , #eq^#(#0(), #pos(@y)) -> c_24() 555.06/148.08 , #eq^#(#0(), #0()) -> c_25() 555.06/148.08 , #eq^#(#0(), #neg(@y)) -> c_26() 555.06/148.08 , #eq^#(#0(), #s(@y)) -> c_27() 555.06/148.08 , #eq^#(#neg(@x), #pos(@y)) -> c_28() 555.06/148.08 , #eq^#(#neg(@x), #0()) -> c_29() 555.06/148.08 , #eq^#(#neg(@x), #neg(@y)) -> c_30(#eq^#(@x, @y)) 555.06/148.08 , #eq^#(#s(@x), #0()) -> c_31() 555.06/148.08 , #eq^#(#s(@x), #s(@y)) -> c_32(#eq^#(@x, @y)) 555.06/148.08 , -^#(@x, @y) -> c_2(#sub^#(@x, @y)) 555.06/148.08 , #sub^#(@x, #pos(@y)) -> c_37(#add^#(@x, #neg(@y))) 555.06/148.08 , #sub^#(@x, #0()) -> c_38() 555.06/148.08 , #sub^#(@x, #neg(@y)) -> c_39(#add^#(@x, #pos(@y))) 555.06/148.08 , eratos#1^#(nil()) -> c_7() 555.06/148.08 , div^#(@x, @y) -> c_4(#div^#(@x, @y)) 555.06/148.08 , #div^#(#pos(@x), #pos(@y)) -> c_62(#natdiv^#(@x, @y)) 555.06/148.08 , #div^#(#pos(@x), #0()) -> c_63() 555.06/148.08 , #div^#(#pos(@x), #neg(@y)) -> c_64(#natdiv^#(@x, @y)) 555.06/148.08 , #div^#(#0(), #pos(@y)) -> c_65() 555.06/148.08 , #div^#(#0(), #0()) -> c_66() 555.06/148.08 , #div^#(#0(), #neg(@y)) -> c_67() 555.06/148.08 , #div^#(#neg(@x), #pos(@y)) -> c_68(#natdiv^#(@x, @y)) 555.06/148.08 , #div^#(#neg(@x), #0()) -> c_69() 555.06/148.08 , #div^#(#neg(@x), #neg(@y)) -> c_70(#natdiv^#(@x, @y)) 555.06/148.08 , *^#(@x, @y) -> c_13(#mult^#(@x, @y)) 555.06/148.08 , filter#1^#(nil(), @p) -> c_11() 555.06/148.08 , filter#3^#(#true(), @x, @xs') -> c_9() 555.06/148.08 , filter#3^#(#false(), @x, @xs') -> c_10() 555.06/148.08 , #mult^#(#pos(@x), #pos(@y)) -> c_49(#natmult^#(@x, @y)) 555.06/148.08 , #mult^#(#pos(@x), #0()) -> c_50() 555.06/148.08 , #mult^#(#pos(@x), #neg(@y)) -> c_51(#natmult^#(@x, @y)) 555.06/148.08 , #mult^#(#0(), #pos(@y)) -> c_52() 555.06/148.08 , #mult^#(#0(), #0()) -> c_53() 555.06/148.08 , #mult^#(#0(), #neg(@y)) -> c_54() 555.06/148.08 , #mult^#(#neg(@x), #pos(@y)) -> c_55(#natmult^#(@x, @y)) 555.06/148.08 , #mult^#(#neg(@x), #0()) -> c_56() 555.06/148.08 , #mult^#(#neg(@x), #neg(@y)) -> c_57(#natmult^#(@x, @y)) 555.06/148.08 , #natsub^#(@x, #0()) -> c_15() 555.06/148.08 , #natsub^#(#s(@x), #s(@y)) -> c_16(#natsub^#(@x, @y)) 555.06/148.08 , #and^#(#true(), #true()) -> c_45() 555.06/148.08 , #and^#(#true(), #false()) -> c_46() 555.06/148.08 , #and^#(#false(), #true()) -> c_47() 555.06/148.08 , #and^#(#false(), #false()) -> c_48() 555.06/148.08 , #natmult^#(#0(), @y) -> c_33() 555.06/148.08 , #natmult^#(#s(@x), @y) -> 555.06/148.08 c_34(#add^#(#pos(@y), #natmult(@x, @y)), #natmult^#(@x, @y)) 555.06/148.08 , #add^#(#pos(#s(#0())), @y) -> c_40(#succ^#(@y)) 555.06/148.08 , #add^#(#pos(#s(#s(@x))), @y) -> 555.06/148.08 c_41(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) 555.06/148.08 , #add^#(#0(), @y) -> c_42() 555.06/148.08 , #add^#(#neg(#s(#0())), @y) -> c_43(#pred^#(@y)) 555.06/148.08 , #add^#(#neg(#s(#s(@x))), @y) -> 555.06/148.08 c_44(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) 555.06/148.08 , #natdiv^#(#0(), #0()) -> c_35() 555.06/148.08 , #natdiv^#(#s(@x), #s(@y)) -> 555.06/148.08 c_36(#natdiv^#(#natsub(@x, @y), #s(@y)), #natsub^#(@x, @y)) 555.06/148.08 , #succ^#(#pos(#s(@x))) -> c_58() 555.06/148.08 , #succ^#(#0()) -> c_59() 555.06/148.08 , #succ^#(#neg(#s(#0()))) -> c_60() 555.06/148.08 , #succ^#(#neg(#s(#s(@x)))) -> c_61() 555.06/148.08 , #pred^#(#pos(#s(#0()))) -> c_71() 555.06/148.08 , #pred^#(#pos(#s(#s(@x)))) -> c_72() 555.06/148.08 , #pred^#(#0()) -> c_73() 555.06/148.08 , #pred^#(#neg(#s(@x))) -> c_74() } 555.06/148.08 Weak Trs: 555.06/148.08 { #equal(@x, @y) -> #eq(@x, @y) 555.06/148.08 , #natsub(@x, #0()) -> @x 555.06/148.08 , #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) 555.06/148.08 , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) 555.06/148.08 , #eq(#pos(@x), #0()) -> #false() 555.06/148.08 , #eq(#pos(@x), #neg(@y)) -> #false() 555.06/148.08 , #eq(nil(), nil()) -> #true() 555.06/148.08 , #eq(nil(), ::(@y_1, @y_2)) -> #false() 555.06/148.08 , #eq(::(@x_1, @x_2), nil()) -> #false() 555.06/148.08 , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> 555.06/148.08 #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) 555.06/148.08 , #eq(#0(), #pos(@y)) -> #false() 555.06/148.08 , #eq(#0(), #0()) -> #true() 555.06/148.08 , #eq(#0(), #neg(@y)) -> #false() 555.06/148.08 , #eq(#0(), #s(@y)) -> #false() 555.06/148.08 , #eq(#neg(@x), #pos(@y)) -> #false() 555.06/148.08 , #eq(#neg(@x), #0()) -> #false() 555.06/148.08 , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) 555.06/148.08 , #eq(#s(@x), #0()) -> #false() 555.06/148.08 , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) 555.06/148.08 , #natmult(#0(), @y) -> #0() 555.06/148.08 , #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) 555.06/148.08 , -(@x, @y) -> #sub(@x, @y) 555.06/148.08 , eratos(@l) -> eratos#1(@l) 555.06/148.08 , #natdiv(#0(), #0()) -> #divByZero() 555.06/148.08 , #natdiv(#s(@x), #s(@y)) -> #s(#natdiv(#natsub(@x, @y), #s(@y))) 555.06/148.08 , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) 555.06/148.08 , #sub(@x, #0()) -> @x 555.06/148.08 , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) 555.06/148.08 , #add(#pos(#s(#0())), @y) -> #succ(@y) 555.06/148.08 , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) 555.06/148.08 , #add(#0(), @y) -> @y 555.06/148.08 , #add(#neg(#s(#0())), @y) -> #pred(@y) 555.06/148.08 , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) 555.06/148.08 , div(@x, @y) -> #div(@x, @y) 555.06/148.08 , mod(@x, @y) -> -(@x, *(@x, div(@x, @y))) 555.06/148.08 , filter(@p, @l) -> filter#1(@l, @p) 555.06/148.08 , eratos#1(nil()) -> nil() 555.06/148.08 , eratos#1(::(@x, @xs)) -> ::(@x, eratos(filter(@x, @xs))) 555.06/148.08 , #and(#true(), #true()) -> #true() 555.06/148.08 , #and(#true(), #false()) -> #false() 555.06/148.08 , #and(#false(), #true()) -> #false() 555.06/148.08 , #and(#false(), #false()) -> #false() 555.06/148.08 , filter#3(#true(), @x, @xs') -> @xs' 555.06/148.08 , filter#3(#false(), @x, @xs') -> ::(@x, @xs') 555.06/148.08 , filter#1(nil(), @p) -> nil() 555.06/148.08 , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) 555.06/148.08 , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) 555.06/148.08 , #mult(#pos(@x), #0()) -> #0() 555.06/148.08 , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) 555.06/148.08 , #mult(#0(), #pos(@y)) -> #0() 555.06/148.08 , #mult(#0(), #0()) -> #0() 555.06/148.08 , #mult(#0(), #neg(@y)) -> #0() 555.06/148.08 , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) 555.06/148.08 , #mult(#neg(@x), #0()) -> #0() 555.06/148.08 , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) 555.06/148.08 , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) 555.06/148.08 , #succ(#0()) -> #pos(#s(#0())) 555.06/148.08 , #succ(#neg(#s(#0()))) -> #0() 555.06/148.08 , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) 555.06/148.08 , #div(#pos(@x), #pos(@y)) -> #pos(#natdiv(@x, @y)) 555.06/148.08 , #div(#pos(@x), #0()) -> #divByZero() 555.06/148.08 , #div(#pos(@x), #neg(@y)) -> #neg(#natdiv(@x, @y)) 555.06/148.08 , #div(#0(), #pos(@y)) -> #0() 555.06/148.08 , #div(#0(), #0()) -> #divByZero() 555.06/148.08 , #div(#0(), #neg(@y)) -> #0() 555.06/148.08 , #div(#neg(@x), #pos(@y)) -> #neg(#natdiv(@x, @y)) 555.06/148.08 , #div(#neg(@x), #0()) -> #divByZero() 555.06/148.08 , #div(#neg(@x), #neg(@y)) -> #pos(#natdiv(@x, @y)) 555.06/148.08 , *(@x, @y) -> #mult(@x, @y) 555.06/148.08 , filter#2(@xs', @p, @x) -> 555.06/148.08 filter#3(#equal(mod(@x, @p), #0()), @x, @xs') 555.06/148.08 , #pred(#pos(#s(#0()))) -> #0() 555.06/148.08 , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) 555.06/148.08 , #pred(#0()) -> #neg(#s(#0())) 555.06/148.08 , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) } 555.06/148.08 Obligation: 555.06/148.08 innermost runtime complexity 555.06/148.08 Answer: 555.06/148.08 YES(O(1),O(n^2)) 555.06/148.08 555.06/148.08 We estimate the number of application of {3} by applications of 555.06/148.08 Pre({3}) = {6}. Here rules are labeled as follows: 555.06/148.08 555.06/148.08 DPs: 555.06/148.08 { 1: eratos^#(@l) -> c_3(eratos#1^#(@l)) 555.06/148.08 , 2: eratos#1^#(::(@x, @xs)) -> 555.06/148.08 c_8(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) 555.06/148.08 , 3: mod^#(@x, @y) -> 555.06/148.08 c_5(-^#(@x, *(@x, div(@x, @y))), 555.06/148.08 *^#(@x, div(@x, @y)), 555.06/148.08 div^#(@x, @y)) 555.06/148.08 , 4: filter^#(@p, @l) -> c_6(filter#1^#(@l, @p)) 555.06/148.08 , 5: filter#1^#(::(@x, @xs), @p) -> 555.06/148.08 c_12(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) 555.06/148.08 , 6: filter#2^#(@xs', @p, @x) -> 555.06/148.08 c_14(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'), 555.06/148.08 #equal^#(mod(@x, @p), #0()), 555.06/148.08 mod^#(@x, @p)) 555.06/148.08 , 7: #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) 555.06/148.08 , 8: #eq^#(#pos(@x), #pos(@y)) -> c_17(#eq^#(@x, @y)) 555.06/148.08 , 9: #eq^#(#pos(@x), #0()) -> c_18() 555.06/148.08 , 10: #eq^#(#pos(@x), #neg(@y)) -> c_19() 555.06/148.08 , 11: #eq^#(nil(), nil()) -> c_20() 555.06/148.08 , 12: #eq^#(nil(), ::(@y_1, @y_2)) -> c_21() 555.06/148.08 , 13: #eq^#(::(@x_1, @x_2), nil()) -> c_22() 555.06/148.08 , 14: #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> 555.06/148.08 c_23(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), 555.06/148.08 #eq^#(@x_1, @y_1), 555.06/148.08 #eq^#(@x_2, @y_2)) 555.06/148.08 , 15: #eq^#(#0(), #pos(@y)) -> c_24() 555.06/148.08 , 16: #eq^#(#0(), #0()) -> c_25() 555.06/148.08 , 17: #eq^#(#0(), #neg(@y)) -> c_26() 555.06/148.08 , 18: #eq^#(#0(), #s(@y)) -> c_27() 555.06/148.08 , 19: #eq^#(#neg(@x), #pos(@y)) -> c_28() 555.06/148.08 , 20: #eq^#(#neg(@x), #0()) -> c_29() 555.06/148.08 , 21: #eq^#(#neg(@x), #neg(@y)) -> c_30(#eq^#(@x, @y)) 555.06/148.08 , 22: #eq^#(#s(@x), #0()) -> c_31() 555.06/148.08 , 23: #eq^#(#s(@x), #s(@y)) -> c_32(#eq^#(@x, @y)) 555.06/148.08 , 24: -^#(@x, @y) -> c_2(#sub^#(@x, @y)) 555.06/148.08 , 25: #sub^#(@x, #pos(@y)) -> c_37(#add^#(@x, #neg(@y))) 555.06/148.08 , 26: #sub^#(@x, #0()) -> c_38() 555.06/148.08 , 27: #sub^#(@x, #neg(@y)) -> c_39(#add^#(@x, #pos(@y))) 555.06/148.08 , 28: eratos#1^#(nil()) -> c_7() 555.06/148.08 , 29: div^#(@x, @y) -> c_4(#div^#(@x, @y)) 555.06/148.08 , 30: #div^#(#pos(@x), #pos(@y)) -> c_62(#natdiv^#(@x, @y)) 555.06/148.08 , 31: #div^#(#pos(@x), #0()) -> c_63() 555.06/148.08 , 32: #div^#(#pos(@x), #neg(@y)) -> c_64(#natdiv^#(@x, @y)) 555.06/148.08 , 33: #div^#(#0(), #pos(@y)) -> c_65() 555.06/148.08 , 34: #div^#(#0(), #0()) -> c_66() 555.06/148.08 , 35: #div^#(#0(), #neg(@y)) -> c_67() 555.06/148.08 , 36: #div^#(#neg(@x), #pos(@y)) -> c_68(#natdiv^#(@x, @y)) 555.06/148.08 , 37: #div^#(#neg(@x), #0()) -> c_69() 555.06/148.08 , 38: #div^#(#neg(@x), #neg(@y)) -> c_70(#natdiv^#(@x, @y)) 555.06/148.08 , 39: *^#(@x, @y) -> c_13(#mult^#(@x, @y)) 555.06/148.08 , 40: filter#1^#(nil(), @p) -> c_11() 555.06/148.08 , 41: filter#3^#(#true(), @x, @xs') -> c_9() 555.06/148.08 , 42: filter#3^#(#false(), @x, @xs') -> c_10() 555.06/148.08 , 43: #mult^#(#pos(@x), #pos(@y)) -> c_49(#natmult^#(@x, @y)) 555.06/148.08 , 44: #mult^#(#pos(@x), #0()) -> c_50() 555.06/148.08 , 45: #mult^#(#pos(@x), #neg(@y)) -> c_51(#natmult^#(@x, @y)) 555.06/148.08 , 46: #mult^#(#0(), #pos(@y)) -> c_52() 555.06/148.08 , 47: #mult^#(#0(), #0()) -> c_53() 555.06/148.08 , 48: #mult^#(#0(), #neg(@y)) -> c_54() 555.06/148.08 , 49: #mult^#(#neg(@x), #pos(@y)) -> c_55(#natmult^#(@x, @y)) 555.06/148.08 , 50: #mult^#(#neg(@x), #0()) -> c_56() 555.06/148.08 , 51: #mult^#(#neg(@x), #neg(@y)) -> c_57(#natmult^#(@x, @y)) 555.06/148.08 , 52: #natsub^#(@x, #0()) -> c_15() 555.06/148.08 , 53: #natsub^#(#s(@x), #s(@y)) -> c_16(#natsub^#(@x, @y)) 555.06/148.08 , 54: #and^#(#true(), #true()) -> c_45() 555.06/148.08 , 55: #and^#(#true(), #false()) -> c_46() 555.06/148.08 , 56: #and^#(#false(), #true()) -> c_47() 555.06/148.08 , 57: #and^#(#false(), #false()) -> c_48() 555.06/148.08 , 58: #natmult^#(#0(), @y) -> c_33() 555.06/148.08 , 59: #natmult^#(#s(@x), @y) -> 555.06/148.08 c_34(#add^#(#pos(@y), #natmult(@x, @y)), #natmult^#(@x, @y)) 555.06/148.08 , 60: #add^#(#pos(#s(#0())), @y) -> c_40(#succ^#(@y)) 555.06/148.08 , 61: #add^#(#pos(#s(#s(@x))), @y) -> 555.06/148.08 c_41(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) 555.06/148.08 , 62: #add^#(#0(), @y) -> c_42() 555.06/148.08 , 63: #add^#(#neg(#s(#0())), @y) -> c_43(#pred^#(@y)) 555.06/148.08 , 64: #add^#(#neg(#s(#s(@x))), @y) -> 555.06/148.08 c_44(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) 555.06/148.08 , 65: #natdiv^#(#0(), #0()) -> c_35() 555.06/148.08 , 66: #natdiv^#(#s(@x), #s(@y)) -> 555.06/148.08 c_36(#natdiv^#(#natsub(@x, @y), #s(@y)), #natsub^#(@x, @y)) 555.06/148.08 , 67: #succ^#(#pos(#s(@x))) -> c_58() 555.06/148.08 , 68: #succ^#(#0()) -> c_59() 555.06/148.08 , 69: #succ^#(#neg(#s(#0()))) -> c_60() 555.06/148.08 , 70: #succ^#(#neg(#s(#s(@x)))) -> c_61() 555.06/148.08 , 71: #pred^#(#pos(#s(#0()))) -> c_71() 555.06/148.08 , 72: #pred^#(#pos(#s(#s(@x)))) -> c_72() 555.06/148.08 , 73: #pred^#(#0()) -> c_73() 555.06/148.08 , 74: #pred^#(#neg(#s(@x))) -> c_74() } 555.06/148.08 555.06/148.08 We are left with following problem, upon which TcT provides the 555.06/148.08 certificate YES(O(1),O(n^2)). 555.06/148.08 555.06/148.08 Strict DPs: 555.06/148.08 { eratos^#(@l) -> c_3(eratos#1^#(@l)) 555.06/148.08 , eratos#1^#(::(@x, @xs)) -> 555.06/148.08 c_8(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) 555.06/148.08 , filter^#(@p, @l) -> c_6(filter#1^#(@l, @p)) 555.06/148.08 , filter#1^#(::(@x, @xs), @p) -> 555.06/148.08 c_12(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) 555.06/148.08 , filter#2^#(@xs', @p, @x) -> 555.06/148.08 c_14(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'), 555.06/148.08 #equal^#(mod(@x, @p), #0()), 555.06/148.08 mod^#(@x, @p)) } 555.06/148.08 Weak DPs: 555.06/148.08 { #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) 555.06/148.08 , #eq^#(#pos(@x), #pos(@y)) -> c_17(#eq^#(@x, @y)) 555.06/148.08 , #eq^#(#pos(@x), #0()) -> c_18() 555.06/148.08 , #eq^#(#pos(@x), #neg(@y)) -> c_19() 555.06/148.08 , #eq^#(nil(), nil()) -> c_20() 555.06/148.08 , #eq^#(nil(), ::(@y_1, @y_2)) -> c_21() 555.06/148.08 , #eq^#(::(@x_1, @x_2), nil()) -> c_22() 555.06/148.08 , #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> 555.06/148.08 c_23(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), 555.06/148.08 #eq^#(@x_1, @y_1), 555.06/148.08 #eq^#(@x_2, @y_2)) 555.06/148.08 , #eq^#(#0(), #pos(@y)) -> c_24() 555.06/148.08 , #eq^#(#0(), #0()) -> c_25() 555.06/148.08 , #eq^#(#0(), #neg(@y)) -> c_26() 555.06/148.08 , #eq^#(#0(), #s(@y)) -> c_27() 555.06/148.08 , #eq^#(#neg(@x), #pos(@y)) -> c_28() 555.06/148.08 , #eq^#(#neg(@x), #0()) -> c_29() 555.06/148.08 , #eq^#(#neg(@x), #neg(@y)) -> c_30(#eq^#(@x, @y)) 555.06/148.08 , #eq^#(#s(@x), #0()) -> c_31() 555.06/148.08 , #eq^#(#s(@x), #s(@y)) -> c_32(#eq^#(@x, @y)) 555.06/148.08 , -^#(@x, @y) -> c_2(#sub^#(@x, @y)) 555.06/148.08 , #sub^#(@x, #pos(@y)) -> c_37(#add^#(@x, #neg(@y))) 555.06/148.08 , #sub^#(@x, #0()) -> c_38() 555.06/148.08 , #sub^#(@x, #neg(@y)) -> c_39(#add^#(@x, #pos(@y))) 555.06/148.08 , eratos#1^#(nil()) -> c_7() 555.06/148.08 , div^#(@x, @y) -> c_4(#div^#(@x, @y)) 555.06/148.08 , #div^#(#pos(@x), #pos(@y)) -> c_62(#natdiv^#(@x, @y)) 555.06/148.08 , #div^#(#pos(@x), #0()) -> c_63() 555.06/148.08 , #div^#(#pos(@x), #neg(@y)) -> c_64(#natdiv^#(@x, @y)) 555.06/148.08 , #div^#(#0(), #pos(@y)) -> c_65() 555.06/148.08 , #div^#(#0(), #0()) -> c_66() 555.06/148.08 , #div^#(#0(), #neg(@y)) -> c_67() 555.06/148.08 , #div^#(#neg(@x), #pos(@y)) -> c_68(#natdiv^#(@x, @y)) 555.06/148.08 , #div^#(#neg(@x), #0()) -> c_69() 555.06/148.08 , #div^#(#neg(@x), #neg(@y)) -> c_70(#natdiv^#(@x, @y)) 555.06/148.08 , mod^#(@x, @y) -> 555.06/148.08 c_5(-^#(@x, *(@x, div(@x, @y))), 555.06/148.08 *^#(@x, div(@x, @y)), 555.06/148.08 div^#(@x, @y)) 555.06/148.08 , *^#(@x, @y) -> c_13(#mult^#(@x, @y)) 555.06/148.08 , filter#1^#(nil(), @p) -> c_11() 555.06/148.08 , filter#3^#(#true(), @x, @xs') -> c_9() 555.06/148.08 , filter#3^#(#false(), @x, @xs') -> c_10() 555.06/148.08 , #mult^#(#pos(@x), #pos(@y)) -> c_49(#natmult^#(@x, @y)) 555.06/148.08 , #mult^#(#pos(@x), #0()) -> c_50() 555.06/148.08 , #mult^#(#pos(@x), #neg(@y)) -> c_51(#natmult^#(@x, @y)) 555.06/148.08 , #mult^#(#0(), #pos(@y)) -> c_52() 555.06/148.08 , #mult^#(#0(), #0()) -> c_53() 555.06/148.08 , #mult^#(#0(), #neg(@y)) -> c_54() 555.06/148.08 , #mult^#(#neg(@x), #pos(@y)) -> c_55(#natmult^#(@x, @y)) 555.06/148.08 , #mult^#(#neg(@x), #0()) -> c_56() 555.06/148.08 , #mult^#(#neg(@x), #neg(@y)) -> c_57(#natmult^#(@x, @y)) 555.06/148.08 , #natsub^#(@x, #0()) -> c_15() 555.06/148.08 , #natsub^#(#s(@x), #s(@y)) -> c_16(#natsub^#(@x, @y)) 555.06/148.08 , #and^#(#true(), #true()) -> c_45() 555.06/148.08 , #and^#(#true(), #false()) -> c_46() 555.06/148.08 , #and^#(#false(), #true()) -> c_47() 555.06/148.08 , #and^#(#false(), #false()) -> c_48() 555.06/148.08 , #natmult^#(#0(), @y) -> c_33() 555.06/148.08 , #natmult^#(#s(@x), @y) -> 555.06/148.08 c_34(#add^#(#pos(@y), #natmult(@x, @y)), #natmult^#(@x, @y)) 555.06/148.08 , #add^#(#pos(#s(#0())), @y) -> c_40(#succ^#(@y)) 555.06/148.08 , #add^#(#pos(#s(#s(@x))), @y) -> 555.06/148.08 c_41(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) 555.06/148.08 , #add^#(#0(), @y) -> c_42() 555.06/148.08 , #add^#(#neg(#s(#0())), @y) -> c_43(#pred^#(@y)) 555.06/148.08 , #add^#(#neg(#s(#s(@x))), @y) -> 555.06/148.08 c_44(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) 555.06/148.08 , #natdiv^#(#0(), #0()) -> c_35() 555.06/148.08 , #natdiv^#(#s(@x), #s(@y)) -> 555.06/148.08 c_36(#natdiv^#(#natsub(@x, @y), #s(@y)), #natsub^#(@x, @y)) 555.06/148.08 , #succ^#(#pos(#s(@x))) -> c_58() 555.06/148.08 , #succ^#(#0()) -> c_59() 555.06/148.08 , #succ^#(#neg(#s(#0()))) -> c_60() 555.06/148.08 , #succ^#(#neg(#s(#s(@x)))) -> c_61() 555.06/148.08 , #pred^#(#pos(#s(#0()))) -> c_71() 555.06/148.08 , #pred^#(#pos(#s(#s(@x)))) -> c_72() 555.06/148.08 , #pred^#(#0()) -> c_73() 555.06/148.08 , #pred^#(#neg(#s(@x))) -> c_74() } 555.06/148.08 Weak Trs: 555.06/148.08 { #equal(@x, @y) -> #eq(@x, @y) 555.06/148.08 , #natsub(@x, #0()) -> @x 555.06/148.08 , #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) 555.06/148.08 , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) 555.06/148.08 , #eq(#pos(@x), #0()) -> #false() 555.06/148.08 , #eq(#pos(@x), #neg(@y)) -> #false() 555.06/148.08 , #eq(nil(), nil()) -> #true() 555.06/148.08 , #eq(nil(), ::(@y_1, @y_2)) -> #false() 555.06/148.08 , #eq(::(@x_1, @x_2), nil()) -> #false() 555.06/148.08 , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> 555.06/148.08 #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) 555.06/148.08 , #eq(#0(), #pos(@y)) -> #false() 555.06/148.08 , #eq(#0(), #0()) -> #true() 555.06/148.08 , #eq(#0(), #neg(@y)) -> #false() 555.06/148.08 , #eq(#0(), #s(@y)) -> #false() 555.06/148.08 , #eq(#neg(@x), #pos(@y)) -> #false() 555.06/148.08 , #eq(#neg(@x), #0()) -> #false() 555.06/148.08 , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) 555.06/148.08 , #eq(#s(@x), #0()) -> #false() 555.06/148.08 , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) 555.06/148.08 , #natmult(#0(), @y) -> #0() 555.06/148.08 , #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) 555.06/148.08 , -(@x, @y) -> #sub(@x, @y) 555.06/148.08 , eratos(@l) -> eratos#1(@l) 555.06/148.08 , #natdiv(#0(), #0()) -> #divByZero() 555.06/148.08 , #natdiv(#s(@x), #s(@y)) -> #s(#natdiv(#natsub(@x, @y), #s(@y))) 555.06/148.08 , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) 555.06/148.08 , #sub(@x, #0()) -> @x 555.06/148.08 , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) 555.06/148.08 , #add(#pos(#s(#0())), @y) -> #succ(@y) 555.06/148.08 , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) 555.06/148.08 , #add(#0(), @y) -> @y 555.06/148.08 , #add(#neg(#s(#0())), @y) -> #pred(@y) 555.06/148.08 , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) 555.06/148.08 , div(@x, @y) -> #div(@x, @y) 555.06/148.08 , mod(@x, @y) -> -(@x, *(@x, div(@x, @y))) 555.06/148.08 , filter(@p, @l) -> filter#1(@l, @p) 555.06/148.08 , eratos#1(nil()) -> nil() 555.06/148.08 , eratos#1(::(@x, @xs)) -> ::(@x, eratos(filter(@x, @xs))) 555.06/148.08 , #and(#true(), #true()) -> #true() 555.06/148.08 , #and(#true(), #false()) -> #false() 555.06/148.08 , #and(#false(), #true()) -> #false() 555.06/148.08 , #and(#false(), #false()) -> #false() 555.06/148.08 , filter#3(#true(), @x, @xs') -> @xs' 555.06/148.08 , filter#3(#false(), @x, @xs') -> ::(@x, @xs') 555.06/148.08 , filter#1(nil(), @p) -> nil() 555.06/148.08 , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) 555.06/148.08 , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) 555.06/148.08 , #mult(#pos(@x), #0()) -> #0() 555.06/148.08 , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) 555.06/148.08 , #mult(#0(), #pos(@y)) -> #0() 555.06/148.08 , #mult(#0(), #0()) -> #0() 555.06/148.08 , #mult(#0(), #neg(@y)) -> #0() 555.06/148.08 , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) 555.06/148.08 , #mult(#neg(@x), #0()) -> #0() 555.06/148.08 , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) 555.06/148.08 , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) 555.06/148.08 , #succ(#0()) -> #pos(#s(#0())) 555.06/148.08 , #succ(#neg(#s(#0()))) -> #0() 555.06/148.08 , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) 555.06/148.08 , #div(#pos(@x), #pos(@y)) -> #pos(#natdiv(@x, @y)) 555.06/148.08 , #div(#pos(@x), #0()) -> #divByZero() 555.06/148.08 , #div(#pos(@x), #neg(@y)) -> #neg(#natdiv(@x, @y)) 555.06/148.08 , #div(#0(), #pos(@y)) -> #0() 555.06/148.08 , #div(#0(), #0()) -> #divByZero() 555.06/148.08 , #div(#0(), #neg(@y)) -> #0() 555.06/148.08 , #div(#neg(@x), #pos(@y)) -> #neg(#natdiv(@x, @y)) 555.06/148.08 , #div(#neg(@x), #0()) -> #divByZero() 555.06/148.08 , #div(#neg(@x), #neg(@y)) -> #pos(#natdiv(@x, @y)) 555.06/148.08 , *(@x, @y) -> #mult(@x, @y) 555.06/148.08 , filter#2(@xs', @p, @x) -> 555.06/148.08 filter#3(#equal(mod(@x, @p), #0()), @x, @xs') 555.06/148.08 , #pred(#pos(#s(#0()))) -> #0() 555.06/148.08 , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) 555.06/148.08 , #pred(#0()) -> #neg(#s(#0())) 555.06/148.08 , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) } 555.06/148.08 Obligation: 555.06/148.08 innermost runtime complexity 555.06/148.08 Answer: 555.06/148.08 YES(O(1),O(n^2)) 555.06/148.08 555.06/148.08 We estimate the number of application of {5} by applications of 555.06/148.08 Pre({5}) = {4}. Here rules are labeled as follows: 555.06/148.08 555.06/148.08 DPs: 555.06/148.08 { 1: eratos^#(@l) -> c_3(eratos#1^#(@l)) 555.06/148.08 , 2: eratos#1^#(::(@x, @xs)) -> 555.06/148.08 c_8(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) 555.06/148.08 , 3: filter^#(@p, @l) -> c_6(filter#1^#(@l, @p)) 555.06/148.09 , 4: filter#1^#(::(@x, @xs), @p) -> 555.06/148.09 c_12(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) 555.06/148.09 , 5: filter#2^#(@xs', @p, @x) -> 555.06/148.09 c_14(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'), 555.06/148.09 #equal^#(mod(@x, @p), #0()), 555.06/148.09 mod^#(@x, @p)) 555.06/148.09 , 6: #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) 555.06/148.09 , 7: #eq^#(#pos(@x), #pos(@y)) -> c_17(#eq^#(@x, @y)) 555.06/148.09 , 8: #eq^#(#pos(@x), #0()) -> c_18() 555.06/148.09 , 9: #eq^#(#pos(@x), #neg(@y)) -> c_19() 555.06/148.09 , 10: #eq^#(nil(), nil()) -> c_20() 555.06/148.09 , 11: #eq^#(nil(), ::(@y_1, @y_2)) -> c_21() 555.06/148.09 , 12: #eq^#(::(@x_1, @x_2), nil()) -> c_22() 555.06/148.09 , 13: #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> 555.06/148.09 c_23(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), 555.06/148.09 #eq^#(@x_1, @y_1), 555.06/148.09 #eq^#(@x_2, @y_2)) 555.06/148.09 , 14: #eq^#(#0(), #pos(@y)) -> c_24() 555.06/148.09 , 15: #eq^#(#0(), #0()) -> c_25() 555.06/148.09 , 16: #eq^#(#0(), #neg(@y)) -> c_26() 555.06/148.09 , 17: #eq^#(#0(), #s(@y)) -> c_27() 555.06/148.09 , 18: #eq^#(#neg(@x), #pos(@y)) -> c_28() 555.06/148.09 , 19: #eq^#(#neg(@x), #0()) -> c_29() 555.06/148.09 , 20: #eq^#(#neg(@x), #neg(@y)) -> c_30(#eq^#(@x, @y)) 555.06/148.09 , 21: #eq^#(#s(@x), #0()) -> c_31() 555.06/148.09 , 22: #eq^#(#s(@x), #s(@y)) -> c_32(#eq^#(@x, @y)) 555.06/148.09 , 23: -^#(@x, @y) -> c_2(#sub^#(@x, @y)) 555.06/148.09 , 24: #sub^#(@x, #pos(@y)) -> c_37(#add^#(@x, #neg(@y))) 555.06/148.09 , 25: #sub^#(@x, #0()) -> c_38() 555.06/148.09 , 26: #sub^#(@x, #neg(@y)) -> c_39(#add^#(@x, #pos(@y))) 555.06/148.09 , 27: eratos#1^#(nil()) -> c_7() 555.06/148.09 , 28: div^#(@x, @y) -> c_4(#div^#(@x, @y)) 555.06/148.09 , 29: #div^#(#pos(@x), #pos(@y)) -> c_62(#natdiv^#(@x, @y)) 555.06/148.09 , 30: #div^#(#pos(@x), #0()) -> c_63() 555.06/148.09 , 31: #div^#(#pos(@x), #neg(@y)) -> c_64(#natdiv^#(@x, @y)) 555.06/148.09 , 32: #div^#(#0(), #pos(@y)) -> c_65() 555.06/148.09 , 33: #div^#(#0(), #0()) -> c_66() 555.06/148.09 , 34: #div^#(#0(), #neg(@y)) -> c_67() 555.06/148.09 , 35: #div^#(#neg(@x), #pos(@y)) -> c_68(#natdiv^#(@x, @y)) 555.06/148.09 , 36: #div^#(#neg(@x), #0()) -> c_69() 555.06/148.09 , 37: #div^#(#neg(@x), #neg(@y)) -> c_70(#natdiv^#(@x, @y)) 555.06/148.09 , 38: mod^#(@x, @y) -> 555.06/148.09 c_5(-^#(@x, *(@x, div(@x, @y))), 555.06/148.09 *^#(@x, div(@x, @y)), 555.06/148.09 div^#(@x, @y)) 555.06/148.09 , 39: *^#(@x, @y) -> c_13(#mult^#(@x, @y)) 555.06/148.09 , 40: filter#1^#(nil(), @p) -> c_11() 555.06/148.09 , 41: filter#3^#(#true(), @x, @xs') -> c_9() 555.06/148.09 , 42: filter#3^#(#false(), @x, @xs') -> c_10() 555.06/148.09 , 43: #mult^#(#pos(@x), #pos(@y)) -> c_49(#natmult^#(@x, @y)) 555.06/148.09 , 44: #mult^#(#pos(@x), #0()) -> c_50() 555.06/148.09 , 45: #mult^#(#pos(@x), #neg(@y)) -> c_51(#natmult^#(@x, @y)) 555.06/148.09 , 46: #mult^#(#0(), #pos(@y)) -> c_52() 555.06/148.09 , 47: #mult^#(#0(), #0()) -> c_53() 555.06/148.09 , 48: #mult^#(#0(), #neg(@y)) -> c_54() 555.06/148.09 , 49: #mult^#(#neg(@x), #pos(@y)) -> c_55(#natmult^#(@x, @y)) 555.06/148.09 , 50: #mult^#(#neg(@x), #0()) -> c_56() 555.06/148.09 , 51: #mult^#(#neg(@x), #neg(@y)) -> c_57(#natmult^#(@x, @y)) 555.06/148.09 , 52: #natsub^#(@x, #0()) -> c_15() 555.06/148.09 , 53: #natsub^#(#s(@x), #s(@y)) -> c_16(#natsub^#(@x, @y)) 555.06/148.09 , 54: #and^#(#true(), #true()) -> c_45() 555.06/148.09 , 55: #and^#(#true(), #false()) -> c_46() 555.06/148.09 , 56: #and^#(#false(), #true()) -> c_47() 555.06/148.09 , 57: #and^#(#false(), #false()) -> c_48() 555.06/148.09 , 58: #natmult^#(#0(), @y) -> c_33() 555.06/148.09 , 59: #natmult^#(#s(@x), @y) -> 555.06/148.09 c_34(#add^#(#pos(@y), #natmult(@x, @y)), #natmult^#(@x, @y)) 555.06/148.09 , 60: #add^#(#pos(#s(#0())), @y) -> c_40(#succ^#(@y)) 555.06/148.09 , 61: #add^#(#pos(#s(#s(@x))), @y) -> 555.06/148.09 c_41(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) 555.06/148.09 , 62: #add^#(#0(), @y) -> c_42() 555.06/148.09 , 63: #add^#(#neg(#s(#0())), @y) -> c_43(#pred^#(@y)) 555.06/148.09 , 64: #add^#(#neg(#s(#s(@x))), @y) -> 555.06/148.09 c_44(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) 555.06/148.09 , 65: #natdiv^#(#0(), #0()) -> c_35() 555.06/148.09 , 66: #natdiv^#(#s(@x), #s(@y)) -> 555.06/148.09 c_36(#natdiv^#(#natsub(@x, @y), #s(@y)), #natsub^#(@x, @y)) 555.06/148.09 , 67: #succ^#(#pos(#s(@x))) -> c_58() 555.06/148.09 , 68: #succ^#(#0()) -> c_59() 555.06/148.09 , 69: #succ^#(#neg(#s(#0()))) -> c_60() 555.06/148.09 , 70: #succ^#(#neg(#s(#s(@x)))) -> c_61() 555.06/148.09 , 71: #pred^#(#pos(#s(#0()))) -> c_71() 555.06/148.09 , 72: #pred^#(#pos(#s(#s(@x)))) -> c_72() 555.06/148.09 , 73: #pred^#(#0()) -> c_73() 555.06/148.09 , 74: #pred^#(#neg(#s(@x))) -> c_74() } 555.06/148.09 555.06/148.09 We are left with following problem, upon which TcT provides the 555.06/148.09 certificate YES(O(1),O(n^2)). 555.06/148.09 555.06/148.09 Strict DPs: 555.06/148.09 { eratos^#(@l) -> c_3(eratos#1^#(@l)) 555.06/148.09 , eratos#1^#(::(@x, @xs)) -> 555.06/148.09 c_8(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) 555.06/148.09 , filter^#(@p, @l) -> c_6(filter#1^#(@l, @p)) 555.06/148.09 , filter#1^#(::(@x, @xs), @p) -> 555.06/148.09 c_12(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) } 555.06/148.09 Weak DPs: 555.06/148.09 { #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) 555.06/148.09 , #eq^#(#pos(@x), #pos(@y)) -> c_17(#eq^#(@x, @y)) 555.06/148.09 , #eq^#(#pos(@x), #0()) -> c_18() 555.06/148.09 , #eq^#(#pos(@x), #neg(@y)) -> c_19() 555.06/148.09 , #eq^#(nil(), nil()) -> c_20() 555.06/148.09 , #eq^#(nil(), ::(@y_1, @y_2)) -> c_21() 555.06/148.09 , #eq^#(::(@x_1, @x_2), nil()) -> c_22() 555.06/148.09 , #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> 555.06/148.09 c_23(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), 555.06/148.09 #eq^#(@x_1, @y_1), 555.06/148.09 #eq^#(@x_2, @y_2)) 555.06/148.09 , #eq^#(#0(), #pos(@y)) -> c_24() 555.06/148.09 , #eq^#(#0(), #0()) -> c_25() 555.06/148.09 , #eq^#(#0(), #neg(@y)) -> c_26() 555.06/148.09 , #eq^#(#0(), #s(@y)) -> c_27() 555.06/148.09 , #eq^#(#neg(@x), #pos(@y)) -> c_28() 555.06/148.09 , #eq^#(#neg(@x), #0()) -> c_29() 555.06/148.09 , #eq^#(#neg(@x), #neg(@y)) -> c_30(#eq^#(@x, @y)) 555.06/148.09 , #eq^#(#s(@x), #0()) -> c_31() 555.06/148.09 , #eq^#(#s(@x), #s(@y)) -> c_32(#eq^#(@x, @y)) 555.06/148.09 , -^#(@x, @y) -> c_2(#sub^#(@x, @y)) 555.06/148.09 , #sub^#(@x, #pos(@y)) -> c_37(#add^#(@x, #neg(@y))) 555.06/148.09 , #sub^#(@x, #0()) -> c_38() 555.06/148.09 , #sub^#(@x, #neg(@y)) -> c_39(#add^#(@x, #pos(@y))) 555.06/148.09 , eratos#1^#(nil()) -> c_7() 555.06/148.09 , div^#(@x, @y) -> c_4(#div^#(@x, @y)) 555.06/148.09 , #div^#(#pos(@x), #pos(@y)) -> c_62(#natdiv^#(@x, @y)) 555.06/148.09 , #div^#(#pos(@x), #0()) -> c_63() 555.06/148.09 , #div^#(#pos(@x), #neg(@y)) -> c_64(#natdiv^#(@x, @y)) 555.06/148.09 , #div^#(#0(), #pos(@y)) -> c_65() 555.06/148.09 , #div^#(#0(), #0()) -> c_66() 555.06/148.09 , #div^#(#0(), #neg(@y)) -> c_67() 555.06/148.09 , #div^#(#neg(@x), #pos(@y)) -> c_68(#natdiv^#(@x, @y)) 555.06/148.09 , #div^#(#neg(@x), #0()) -> c_69() 555.06/148.09 , #div^#(#neg(@x), #neg(@y)) -> c_70(#natdiv^#(@x, @y)) 555.06/148.09 , mod^#(@x, @y) -> 555.06/148.09 c_5(-^#(@x, *(@x, div(@x, @y))), 555.06/148.09 *^#(@x, div(@x, @y)), 555.06/148.09 div^#(@x, @y)) 555.06/148.09 , *^#(@x, @y) -> c_13(#mult^#(@x, @y)) 555.06/148.09 , filter#1^#(nil(), @p) -> c_11() 555.06/148.09 , filter#3^#(#true(), @x, @xs') -> c_9() 555.06/148.09 , filter#3^#(#false(), @x, @xs') -> c_10() 555.06/148.09 , filter#2^#(@xs', @p, @x) -> 555.06/148.09 c_14(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'), 555.06/148.09 #equal^#(mod(@x, @p), #0()), 555.06/148.09 mod^#(@x, @p)) 555.06/148.09 , #mult^#(#pos(@x), #pos(@y)) -> c_49(#natmult^#(@x, @y)) 555.06/148.09 , #mult^#(#pos(@x), #0()) -> c_50() 555.06/148.09 , #mult^#(#pos(@x), #neg(@y)) -> c_51(#natmult^#(@x, @y)) 555.06/148.09 , #mult^#(#0(), #pos(@y)) -> c_52() 555.06/148.09 , #mult^#(#0(), #0()) -> c_53() 555.06/148.09 , #mult^#(#0(), #neg(@y)) -> c_54() 555.06/148.09 , #mult^#(#neg(@x), #pos(@y)) -> c_55(#natmult^#(@x, @y)) 555.06/148.09 , #mult^#(#neg(@x), #0()) -> c_56() 555.06/148.09 , #mult^#(#neg(@x), #neg(@y)) -> c_57(#natmult^#(@x, @y)) 555.06/148.09 , #natsub^#(@x, #0()) -> c_15() 555.06/148.09 , #natsub^#(#s(@x), #s(@y)) -> c_16(#natsub^#(@x, @y)) 555.06/148.09 , #and^#(#true(), #true()) -> c_45() 555.06/148.09 , #and^#(#true(), #false()) -> c_46() 555.06/148.09 , #and^#(#false(), #true()) -> c_47() 555.06/148.09 , #and^#(#false(), #false()) -> c_48() 555.06/148.09 , #natmult^#(#0(), @y) -> c_33() 555.06/148.09 , #natmult^#(#s(@x), @y) -> 555.06/148.09 c_34(#add^#(#pos(@y), #natmult(@x, @y)), #natmult^#(@x, @y)) 555.06/148.09 , #add^#(#pos(#s(#0())), @y) -> c_40(#succ^#(@y)) 555.06/148.09 , #add^#(#pos(#s(#s(@x))), @y) -> 555.06/148.09 c_41(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) 555.06/148.09 , #add^#(#0(), @y) -> c_42() 555.06/148.09 , #add^#(#neg(#s(#0())), @y) -> c_43(#pred^#(@y)) 555.06/148.09 , #add^#(#neg(#s(#s(@x))), @y) -> 555.06/148.09 c_44(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) 555.06/148.09 , #natdiv^#(#0(), #0()) -> c_35() 555.06/148.09 , #natdiv^#(#s(@x), #s(@y)) -> 555.06/148.09 c_36(#natdiv^#(#natsub(@x, @y), #s(@y)), #natsub^#(@x, @y)) 555.06/148.09 , #succ^#(#pos(#s(@x))) -> c_58() 555.06/148.09 , #succ^#(#0()) -> c_59() 555.06/148.09 , #succ^#(#neg(#s(#0()))) -> c_60() 555.06/148.09 , #succ^#(#neg(#s(#s(@x)))) -> c_61() 555.06/148.09 , #pred^#(#pos(#s(#0()))) -> c_71() 555.06/148.09 , #pred^#(#pos(#s(#s(@x)))) -> c_72() 555.06/148.09 , #pred^#(#0()) -> c_73() 555.06/148.09 , #pred^#(#neg(#s(@x))) -> c_74() } 555.06/148.09 Weak Trs: 555.06/148.09 { #equal(@x, @y) -> #eq(@x, @y) 555.06/148.09 , #natsub(@x, #0()) -> @x 555.06/148.09 , #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) 555.06/148.09 , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) 555.06/148.09 , #eq(#pos(@x), #0()) -> #false() 555.06/148.09 , #eq(#pos(@x), #neg(@y)) -> #false() 555.06/148.09 , #eq(nil(), nil()) -> #true() 555.06/148.09 , #eq(nil(), ::(@y_1, @y_2)) -> #false() 555.06/148.09 , #eq(::(@x_1, @x_2), nil()) -> #false() 555.06/148.09 , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> 555.06/148.09 #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) 555.06/148.09 , #eq(#0(), #pos(@y)) -> #false() 555.06/148.09 , #eq(#0(), #0()) -> #true() 555.06/148.09 , #eq(#0(), #neg(@y)) -> #false() 555.06/148.09 , #eq(#0(), #s(@y)) -> #false() 555.06/148.09 , #eq(#neg(@x), #pos(@y)) -> #false() 555.06/148.09 , #eq(#neg(@x), #0()) -> #false() 555.06/148.09 , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) 555.06/148.09 , #eq(#s(@x), #0()) -> #false() 555.06/148.09 , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) 555.06/148.09 , #natmult(#0(), @y) -> #0() 555.06/148.09 , #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) 555.06/148.09 , -(@x, @y) -> #sub(@x, @y) 555.06/148.09 , eratos(@l) -> eratos#1(@l) 555.06/148.09 , #natdiv(#0(), #0()) -> #divByZero() 555.06/148.09 , #natdiv(#s(@x), #s(@y)) -> #s(#natdiv(#natsub(@x, @y), #s(@y))) 555.06/148.09 , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) 555.06/148.09 , #sub(@x, #0()) -> @x 555.06/148.09 , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) 555.06/148.09 , #add(#pos(#s(#0())), @y) -> #succ(@y) 555.06/148.09 , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) 555.06/148.09 , #add(#0(), @y) -> @y 555.06/148.09 , #add(#neg(#s(#0())), @y) -> #pred(@y) 555.06/148.09 , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) 555.06/148.09 , div(@x, @y) -> #div(@x, @y) 555.06/148.09 , mod(@x, @y) -> -(@x, *(@x, div(@x, @y))) 555.06/148.09 , filter(@p, @l) -> filter#1(@l, @p) 555.06/148.09 , eratos#1(nil()) -> nil() 555.06/148.09 , eratos#1(::(@x, @xs)) -> ::(@x, eratos(filter(@x, @xs))) 555.06/148.09 , #and(#true(), #true()) -> #true() 555.06/148.09 , #and(#true(), #false()) -> #false() 555.06/148.09 , #and(#false(), #true()) -> #false() 555.06/148.09 , #and(#false(), #false()) -> #false() 555.06/148.09 , filter#3(#true(), @x, @xs') -> @xs' 555.06/148.09 , filter#3(#false(), @x, @xs') -> ::(@x, @xs') 555.06/148.09 , filter#1(nil(), @p) -> nil() 555.06/148.09 , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) 555.06/148.09 , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) 555.06/148.09 , #mult(#pos(@x), #0()) -> #0() 555.06/148.09 , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) 555.06/148.09 , #mult(#0(), #pos(@y)) -> #0() 555.06/148.09 , #mult(#0(), #0()) -> #0() 555.06/148.09 , #mult(#0(), #neg(@y)) -> #0() 555.06/148.09 , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) 555.06/148.09 , #mult(#neg(@x), #0()) -> #0() 555.06/148.09 , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) 555.06/148.09 , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) 555.06/148.09 , #succ(#0()) -> #pos(#s(#0())) 555.06/148.09 , #succ(#neg(#s(#0()))) -> #0() 555.06/148.09 , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) 555.06/148.09 , #div(#pos(@x), #pos(@y)) -> #pos(#natdiv(@x, @y)) 555.06/148.09 , #div(#pos(@x), #0()) -> #divByZero() 555.06/148.09 , #div(#pos(@x), #neg(@y)) -> #neg(#natdiv(@x, @y)) 555.06/148.09 , #div(#0(), #pos(@y)) -> #0() 555.06/148.09 , #div(#0(), #0()) -> #divByZero() 555.06/148.09 , #div(#0(), #neg(@y)) -> #0() 555.06/148.09 , #div(#neg(@x), #pos(@y)) -> #neg(#natdiv(@x, @y)) 555.06/148.09 , #div(#neg(@x), #0()) -> #divByZero() 555.06/148.09 , #div(#neg(@x), #neg(@y)) -> #pos(#natdiv(@x, @y)) 555.06/148.09 , *(@x, @y) -> #mult(@x, @y) 555.06/148.09 , filter#2(@xs', @p, @x) -> 555.06/148.09 filter#3(#equal(mod(@x, @p), #0()), @x, @xs') 555.06/148.09 , #pred(#pos(#s(#0()))) -> #0() 555.06/148.09 , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) 555.06/148.09 , #pred(#0()) -> #neg(#s(#0())) 555.06/148.09 , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) } 555.06/148.09 Obligation: 555.06/148.09 innermost runtime complexity 555.06/148.09 Answer: 555.06/148.09 YES(O(1),O(n^2)) 555.06/148.09 555.06/148.09 The following weak DPs constitute a sub-graph of the DG that is 555.06/148.09 closed under successors. The DPs are removed. 555.06/148.09 555.06/148.09 { #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) 555.06/148.09 , #eq^#(#pos(@x), #pos(@y)) -> c_17(#eq^#(@x, @y)) 555.06/148.09 , #eq^#(#pos(@x), #0()) -> c_18() 555.06/148.09 , #eq^#(#pos(@x), #neg(@y)) -> c_19() 555.06/148.09 , #eq^#(nil(), nil()) -> c_20() 555.06/148.09 , #eq^#(nil(), ::(@y_1, @y_2)) -> c_21() 555.06/148.09 , #eq^#(::(@x_1, @x_2), nil()) -> c_22() 555.06/148.09 , #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> 555.06/148.09 c_23(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), 555.06/148.09 #eq^#(@x_1, @y_1), 555.06/148.09 #eq^#(@x_2, @y_2)) 555.06/148.09 , #eq^#(#0(), #pos(@y)) -> c_24() 555.06/148.09 , #eq^#(#0(), #0()) -> c_25() 555.06/148.09 , #eq^#(#0(), #neg(@y)) -> c_26() 555.06/148.09 , #eq^#(#0(), #s(@y)) -> c_27() 555.06/148.09 , #eq^#(#neg(@x), #pos(@y)) -> c_28() 555.06/148.09 , #eq^#(#neg(@x), #0()) -> c_29() 555.06/148.09 , #eq^#(#neg(@x), #neg(@y)) -> c_30(#eq^#(@x, @y)) 555.06/148.09 , #eq^#(#s(@x), #0()) -> c_31() 555.06/148.09 , #eq^#(#s(@x), #s(@y)) -> c_32(#eq^#(@x, @y)) 555.06/148.09 , -^#(@x, @y) -> c_2(#sub^#(@x, @y)) 555.06/148.09 , #sub^#(@x, #pos(@y)) -> c_37(#add^#(@x, #neg(@y))) 555.06/148.09 , #sub^#(@x, #0()) -> c_38() 555.06/148.09 , #sub^#(@x, #neg(@y)) -> c_39(#add^#(@x, #pos(@y))) 555.06/148.09 , eratos#1^#(nil()) -> c_7() 555.06/148.09 , div^#(@x, @y) -> c_4(#div^#(@x, @y)) 555.06/148.09 , #div^#(#pos(@x), #pos(@y)) -> c_62(#natdiv^#(@x, @y)) 555.06/148.09 , #div^#(#pos(@x), #0()) -> c_63() 555.06/148.09 , #div^#(#pos(@x), #neg(@y)) -> c_64(#natdiv^#(@x, @y)) 555.06/148.09 , #div^#(#0(), #pos(@y)) -> c_65() 555.06/148.09 , #div^#(#0(), #0()) -> c_66() 555.06/148.09 , #div^#(#0(), #neg(@y)) -> c_67() 555.06/148.09 , #div^#(#neg(@x), #pos(@y)) -> c_68(#natdiv^#(@x, @y)) 555.06/148.09 , #div^#(#neg(@x), #0()) -> c_69() 555.06/148.09 , #div^#(#neg(@x), #neg(@y)) -> c_70(#natdiv^#(@x, @y)) 555.06/148.09 , mod^#(@x, @y) -> 555.06/148.09 c_5(-^#(@x, *(@x, div(@x, @y))), 555.06/148.09 *^#(@x, div(@x, @y)), 555.06/148.09 div^#(@x, @y)) 555.06/148.09 , *^#(@x, @y) -> c_13(#mult^#(@x, @y)) 555.06/148.09 , filter#1^#(nil(), @p) -> c_11() 555.06/148.09 , filter#3^#(#true(), @x, @xs') -> c_9() 555.06/148.09 , filter#3^#(#false(), @x, @xs') -> c_10() 555.06/148.09 , filter#2^#(@xs', @p, @x) -> 555.06/148.09 c_14(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'), 555.06/148.09 #equal^#(mod(@x, @p), #0()), 555.06/148.09 mod^#(@x, @p)) 555.06/148.09 , #mult^#(#pos(@x), #pos(@y)) -> c_49(#natmult^#(@x, @y)) 555.06/148.09 , #mult^#(#pos(@x), #0()) -> c_50() 555.06/148.09 , #mult^#(#pos(@x), #neg(@y)) -> c_51(#natmult^#(@x, @y)) 555.06/148.09 , #mult^#(#0(), #pos(@y)) -> c_52() 555.06/148.09 , #mult^#(#0(), #0()) -> c_53() 555.06/148.09 , #mult^#(#0(), #neg(@y)) -> c_54() 555.06/148.09 , #mult^#(#neg(@x), #pos(@y)) -> c_55(#natmult^#(@x, @y)) 555.06/148.09 , #mult^#(#neg(@x), #0()) -> c_56() 555.06/148.09 , #mult^#(#neg(@x), #neg(@y)) -> c_57(#natmult^#(@x, @y)) 555.06/148.09 , #natsub^#(@x, #0()) -> c_15() 555.06/148.09 , #natsub^#(#s(@x), #s(@y)) -> c_16(#natsub^#(@x, @y)) 555.06/148.09 , #and^#(#true(), #true()) -> c_45() 555.06/148.09 , #and^#(#true(), #false()) -> c_46() 555.06/148.09 , #and^#(#false(), #true()) -> c_47() 555.06/148.09 , #and^#(#false(), #false()) -> c_48() 555.06/148.09 , #natmult^#(#0(), @y) -> c_33() 555.06/148.09 , #natmult^#(#s(@x), @y) -> 555.06/148.09 c_34(#add^#(#pos(@y), #natmult(@x, @y)), #natmult^#(@x, @y)) 555.06/148.09 , #add^#(#pos(#s(#0())), @y) -> c_40(#succ^#(@y)) 555.06/148.09 , #add^#(#pos(#s(#s(@x))), @y) -> 555.06/148.09 c_41(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) 555.06/148.09 , #add^#(#0(), @y) -> c_42() 555.06/148.09 , #add^#(#neg(#s(#0())), @y) -> c_43(#pred^#(@y)) 555.06/148.09 , #add^#(#neg(#s(#s(@x))), @y) -> 555.06/148.09 c_44(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) 555.06/148.09 , #natdiv^#(#0(), #0()) -> c_35() 555.06/148.09 , #natdiv^#(#s(@x), #s(@y)) -> 555.06/148.09 c_36(#natdiv^#(#natsub(@x, @y), #s(@y)), #natsub^#(@x, @y)) 555.06/148.09 , #succ^#(#pos(#s(@x))) -> c_58() 555.06/148.09 , #succ^#(#0()) -> c_59() 555.06/148.09 , #succ^#(#neg(#s(#0()))) -> c_60() 555.06/148.09 , #succ^#(#neg(#s(#s(@x)))) -> c_61() 555.06/148.09 , #pred^#(#pos(#s(#0()))) -> c_71() 555.06/148.09 , #pred^#(#pos(#s(#s(@x)))) -> c_72() 555.06/148.09 , #pred^#(#0()) -> c_73() 555.06/148.09 , #pred^#(#neg(#s(@x))) -> c_74() } 555.06/148.09 555.06/148.09 We are left with following problem, upon which TcT provides the 555.06/148.09 certificate YES(O(1),O(n^2)). 555.06/148.09 555.06/148.09 Strict DPs: 555.06/148.09 { eratos^#(@l) -> c_3(eratos#1^#(@l)) 555.06/148.09 , eratos#1^#(::(@x, @xs)) -> 555.06/148.09 c_8(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) 555.06/148.09 , filter^#(@p, @l) -> c_6(filter#1^#(@l, @p)) 555.06/148.09 , filter#1^#(::(@x, @xs), @p) -> 555.06/148.09 c_12(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) } 555.06/148.09 Weak Trs: 555.06/148.09 { #equal(@x, @y) -> #eq(@x, @y) 555.06/148.09 , #natsub(@x, #0()) -> @x 555.06/148.09 , #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) 555.06/148.09 , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) 555.06/148.09 , #eq(#pos(@x), #0()) -> #false() 555.06/148.09 , #eq(#pos(@x), #neg(@y)) -> #false() 555.06/148.09 , #eq(nil(), nil()) -> #true() 555.06/148.09 , #eq(nil(), ::(@y_1, @y_2)) -> #false() 555.06/148.09 , #eq(::(@x_1, @x_2), nil()) -> #false() 555.06/148.09 , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> 555.06/148.09 #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) 555.06/148.09 , #eq(#0(), #pos(@y)) -> #false() 555.06/148.09 , #eq(#0(), #0()) -> #true() 555.06/148.09 , #eq(#0(), #neg(@y)) -> #false() 555.06/148.09 , #eq(#0(), #s(@y)) -> #false() 555.06/148.09 , #eq(#neg(@x), #pos(@y)) -> #false() 555.06/148.09 , #eq(#neg(@x), #0()) -> #false() 555.06/148.09 , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) 555.06/148.09 , #eq(#s(@x), #0()) -> #false() 555.06/148.09 , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) 555.06/148.09 , #natmult(#0(), @y) -> #0() 555.06/148.09 , #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) 555.06/148.09 , -(@x, @y) -> #sub(@x, @y) 555.06/148.09 , eratos(@l) -> eratos#1(@l) 555.06/148.09 , #natdiv(#0(), #0()) -> #divByZero() 555.06/148.09 , #natdiv(#s(@x), #s(@y)) -> #s(#natdiv(#natsub(@x, @y), #s(@y))) 555.06/148.09 , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) 555.06/148.09 , #sub(@x, #0()) -> @x 555.06/148.09 , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) 555.06/148.09 , #add(#pos(#s(#0())), @y) -> #succ(@y) 555.06/148.09 , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) 555.06/148.09 , #add(#0(), @y) -> @y 555.06/148.09 , #add(#neg(#s(#0())), @y) -> #pred(@y) 555.06/148.09 , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) 555.06/148.09 , div(@x, @y) -> #div(@x, @y) 555.06/148.09 , mod(@x, @y) -> -(@x, *(@x, div(@x, @y))) 555.06/148.09 , filter(@p, @l) -> filter#1(@l, @p) 555.06/148.09 , eratos#1(nil()) -> nil() 555.06/148.09 , eratos#1(::(@x, @xs)) -> ::(@x, eratos(filter(@x, @xs))) 555.06/148.09 , #and(#true(), #true()) -> #true() 555.06/148.09 , #and(#true(), #false()) -> #false() 555.06/148.09 , #and(#false(), #true()) -> #false() 555.06/148.09 , #and(#false(), #false()) -> #false() 555.06/148.09 , filter#3(#true(), @x, @xs') -> @xs' 555.06/148.09 , filter#3(#false(), @x, @xs') -> ::(@x, @xs') 555.06/148.09 , filter#1(nil(), @p) -> nil() 555.06/148.09 , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) 555.06/148.09 , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) 555.06/148.09 , #mult(#pos(@x), #0()) -> #0() 555.06/148.09 , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) 555.06/148.09 , #mult(#0(), #pos(@y)) -> #0() 555.06/148.09 , #mult(#0(), #0()) -> #0() 555.06/148.09 , #mult(#0(), #neg(@y)) -> #0() 555.06/148.09 , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) 555.06/148.09 , #mult(#neg(@x), #0()) -> #0() 555.06/148.09 , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) 555.06/148.09 , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) 555.06/148.09 , #succ(#0()) -> #pos(#s(#0())) 555.06/148.09 , #succ(#neg(#s(#0()))) -> #0() 555.06/148.09 , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) 555.06/148.09 , #div(#pos(@x), #pos(@y)) -> #pos(#natdiv(@x, @y)) 555.06/148.09 , #div(#pos(@x), #0()) -> #divByZero() 555.06/148.09 , #div(#pos(@x), #neg(@y)) -> #neg(#natdiv(@x, @y)) 555.06/148.09 , #div(#0(), #pos(@y)) -> #0() 555.06/148.09 , #div(#0(), #0()) -> #divByZero() 555.06/148.09 , #div(#0(), #neg(@y)) -> #0() 555.06/148.09 , #div(#neg(@x), #pos(@y)) -> #neg(#natdiv(@x, @y)) 555.06/148.09 , #div(#neg(@x), #0()) -> #divByZero() 555.06/148.09 , #div(#neg(@x), #neg(@y)) -> #pos(#natdiv(@x, @y)) 555.06/148.09 , *(@x, @y) -> #mult(@x, @y) 555.06/148.09 , filter#2(@xs', @p, @x) -> 555.06/148.09 filter#3(#equal(mod(@x, @p), #0()), @x, @xs') 555.06/148.09 , #pred(#pos(#s(#0()))) -> #0() 555.06/148.09 , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) 555.06/148.09 , #pred(#0()) -> #neg(#s(#0())) 555.06/148.09 , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) } 555.06/148.09 Obligation: 555.06/148.09 innermost runtime complexity 555.06/148.09 Answer: 555.06/148.09 YES(O(1),O(n^2)) 555.06/148.09 555.06/148.09 Due to missing edges in the dependency-graph, the right-hand sides 555.06/148.09 of following rules could be simplified: 555.06/148.09 555.06/148.09 { filter#1^#(::(@x, @xs), @p) -> 555.06/148.09 c_12(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) } 555.06/148.09 555.06/148.09 We are left with following problem, upon which TcT provides the 555.06/148.09 certificate YES(O(1),O(n^2)). 555.06/148.09 555.06/148.09 Strict DPs: 555.06/148.09 { eratos^#(@l) -> c_1(eratos#1^#(@l)) 555.06/148.09 , eratos#1^#(::(@x, @xs)) -> 555.06/148.09 c_2(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) 555.06/148.09 , filter^#(@p, @l) -> c_3(filter#1^#(@l, @p)) 555.06/148.09 , filter#1^#(::(@x, @xs), @p) -> c_4(filter^#(@p, @xs)) } 555.06/148.09 Weak Trs: 555.06/148.09 { #equal(@x, @y) -> #eq(@x, @y) 555.06/148.09 , #natsub(@x, #0()) -> @x 555.06/148.09 , #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) 555.06/148.09 , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) 555.06/148.09 , #eq(#pos(@x), #0()) -> #false() 555.06/148.09 , #eq(#pos(@x), #neg(@y)) -> #false() 555.06/148.09 , #eq(nil(), nil()) -> #true() 555.06/148.09 , #eq(nil(), ::(@y_1, @y_2)) -> #false() 555.06/148.09 , #eq(::(@x_1, @x_2), nil()) -> #false() 555.06/148.09 , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> 555.06/148.09 #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) 555.06/148.09 , #eq(#0(), #pos(@y)) -> #false() 555.35/148.10 , #eq(#0(), #0()) -> #true() 555.35/148.10 , #eq(#0(), #neg(@y)) -> #false() 555.35/148.10 , #eq(#0(), #s(@y)) -> #false() 555.35/148.10 , #eq(#neg(@x), #pos(@y)) -> #false() 555.35/148.10 , #eq(#neg(@x), #0()) -> #false() 555.35/148.10 , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) 555.35/148.10 , #eq(#s(@x), #0()) -> #false() 555.35/148.10 , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) 555.35/148.10 , #natmult(#0(), @y) -> #0() 555.35/148.10 , #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) 555.35/148.10 , -(@x, @y) -> #sub(@x, @y) 555.35/148.10 , eratos(@l) -> eratos#1(@l) 555.35/148.10 , #natdiv(#0(), #0()) -> #divByZero() 555.35/148.10 , #natdiv(#s(@x), #s(@y)) -> #s(#natdiv(#natsub(@x, @y), #s(@y))) 555.35/148.10 , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) 555.35/148.10 , #sub(@x, #0()) -> @x 555.35/148.10 , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) 555.35/148.10 , #add(#pos(#s(#0())), @y) -> #succ(@y) 555.35/148.10 , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) 555.35/148.10 , #add(#0(), @y) -> @y 555.35/148.10 , #add(#neg(#s(#0())), @y) -> #pred(@y) 555.35/148.10 , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) 555.35/148.10 , div(@x, @y) -> #div(@x, @y) 555.35/148.10 , mod(@x, @y) -> -(@x, *(@x, div(@x, @y))) 555.35/148.10 , filter(@p, @l) -> filter#1(@l, @p) 555.35/148.10 , eratos#1(nil()) -> nil() 555.35/148.10 , eratos#1(::(@x, @xs)) -> ::(@x, eratos(filter(@x, @xs))) 555.35/148.10 , #and(#true(), #true()) -> #true() 555.35/148.10 , #and(#true(), #false()) -> #false() 555.35/148.10 , #and(#false(), #true()) -> #false() 555.35/148.10 , #and(#false(), #false()) -> #false() 555.35/148.10 , filter#3(#true(), @x, @xs') -> @xs' 555.35/148.10 , filter#3(#false(), @x, @xs') -> ::(@x, @xs') 555.35/148.10 , filter#1(nil(), @p) -> nil() 555.35/148.10 , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) 555.35/148.10 , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) 555.35/148.10 , #mult(#pos(@x), #0()) -> #0() 555.35/148.10 , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) 555.35/148.10 , #mult(#0(), #pos(@y)) -> #0() 555.35/148.10 , #mult(#0(), #0()) -> #0() 555.35/148.10 , #mult(#0(), #neg(@y)) -> #0() 555.35/148.10 , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) 555.35/148.10 , #mult(#neg(@x), #0()) -> #0() 555.35/148.10 , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) 555.35/148.10 , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) 555.35/148.10 , #succ(#0()) -> #pos(#s(#0())) 555.35/148.10 , #succ(#neg(#s(#0()))) -> #0() 555.35/148.10 , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) 555.35/148.10 , #div(#pos(@x), #pos(@y)) -> #pos(#natdiv(@x, @y)) 555.35/148.10 , #div(#pos(@x), #0()) -> #divByZero() 555.35/148.10 , #div(#pos(@x), #neg(@y)) -> #neg(#natdiv(@x, @y)) 555.35/148.10 , #div(#0(), #pos(@y)) -> #0() 555.35/148.10 , #div(#0(), #0()) -> #divByZero() 555.35/148.10 , #div(#0(), #neg(@y)) -> #0() 555.35/148.10 , #div(#neg(@x), #pos(@y)) -> #neg(#natdiv(@x, @y)) 555.35/148.10 , #div(#neg(@x), #0()) -> #divByZero() 555.35/148.10 , #div(#neg(@x), #neg(@y)) -> #pos(#natdiv(@x, @y)) 555.35/148.10 , *(@x, @y) -> #mult(@x, @y) 555.35/148.10 , filter#2(@xs', @p, @x) -> 555.35/148.10 filter#3(#equal(mod(@x, @p), #0()), @x, @xs') 555.35/148.10 , #pred(#pos(#s(#0()))) -> #0() 555.35/148.10 , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) 555.35/148.10 , #pred(#0()) -> #neg(#s(#0())) 555.35/148.10 , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) } 555.35/148.10 Obligation: 555.35/148.10 innermost runtime complexity 555.35/148.10 Answer: 555.35/148.10 YES(O(1),O(n^2)) 555.35/148.10 555.35/148.10 We replace rewrite rules by usable rules: 555.35/148.10 555.35/148.10 Weak Usable Rules: 555.35/148.10 { #equal(@x, @y) -> #eq(@x, @y) 555.35/148.10 , #natsub(@x, #0()) -> @x 555.35/148.10 , #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) 555.35/148.10 , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) 555.35/148.10 , #eq(#pos(@x), #0()) -> #false() 555.35/148.10 , #eq(#pos(@x), #neg(@y)) -> #false() 555.35/148.10 , #eq(nil(), nil()) -> #true() 555.35/148.10 , #eq(nil(), ::(@y_1, @y_2)) -> #false() 555.35/148.10 , #eq(::(@x_1, @x_2), nil()) -> #false() 555.35/148.10 , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> 555.35/148.10 #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) 555.35/148.10 , #eq(#0(), #pos(@y)) -> #false() 555.35/148.10 , #eq(#0(), #0()) -> #true() 555.35/148.10 , #eq(#0(), #neg(@y)) -> #false() 555.35/148.10 , #eq(#0(), #s(@y)) -> #false() 555.35/148.10 , #eq(#neg(@x), #pos(@y)) -> #false() 555.35/148.10 , #eq(#neg(@x), #0()) -> #false() 555.35/148.10 , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) 555.35/148.10 , #eq(#s(@x), #0()) -> #false() 555.35/148.10 , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) 555.35/148.10 , #natmult(#0(), @y) -> #0() 555.35/148.10 , #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) 555.35/148.10 , -(@x, @y) -> #sub(@x, @y) 555.35/148.10 , #natdiv(#0(), #0()) -> #divByZero() 555.35/148.10 , #natdiv(#s(@x), #s(@y)) -> #s(#natdiv(#natsub(@x, @y), #s(@y))) 555.35/148.10 , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) 555.35/148.10 , #sub(@x, #0()) -> @x 555.35/148.10 , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) 555.35/148.10 , #add(#pos(#s(#0())), @y) -> #succ(@y) 555.35/148.10 , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) 555.35/148.10 , #add(#0(), @y) -> @y 555.35/148.10 , #add(#neg(#s(#0())), @y) -> #pred(@y) 555.35/148.10 , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) 555.35/148.10 , div(@x, @y) -> #div(@x, @y) 555.35/148.10 , mod(@x, @y) -> -(@x, *(@x, div(@x, @y))) 555.35/148.10 , filter(@p, @l) -> filter#1(@l, @p) 555.35/148.10 , #and(#true(), #true()) -> #true() 555.35/148.10 , #and(#true(), #false()) -> #false() 555.35/148.10 , #and(#false(), #true()) -> #false() 555.35/148.10 , #and(#false(), #false()) -> #false() 555.35/148.10 , filter#3(#true(), @x, @xs') -> @xs' 555.35/148.10 , filter#3(#false(), @x, @xs') -> ::(@x, @xs') 555.35/148.10 , filter#1(nil(), @p) -> nil() 555.35/148.10 , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) 555.35/148.10 , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) 555.35/148.10 , #mult(#pos(@x), #0()) -> #0() 555.35/148.10 , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) 555.35/148.10 , #mult(#0(), #pos(@y)) -> #0() 555.35/148.10 , #mult(#0(), #0()) -> #0() 555.35/148.10 , #mult(#0(), #neg(@y)) -> #0() 555.35/148.10 , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) 555.35/148.10 , #mult(#neg(@x), #0()) -> #0() 555.35/148.10 , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) 555.35/148.10 , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) 555.35/148.10 , #succ(#0()) -> #pos(#s(#0())) 555.35/148.10 , #succ(#neg(#s(#0()))) -> #0() 555.35/148.10 , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) 555.35/148.10 , #div(#pos(@x), #pos(@y)) -> #pos(#natdiv(@x, @y)) 555.35/148.10 , #div(#pos(@x), #0()) -> #divByZero() 555.35/148.10 , #div(#pos(@x), #neg(@y)) -> #neg(#natdiv(@x, @y)) 555.35/148.10 , #div(#0(), #pos(@y)) -> #0() 555.35/148.10 , #div(#0(), #0()) -> #divByZero() 555.35/148.10 , #div(#0(), #neg(@y)) -> #0() 555.35/148.10 , #div(#neg(@x), #pos(@y)) -> #neg(#natdiv(@x, @y)) 555.35/148.10 , #div(#neg(@x), #0()) -> #divByZero() 555.35/148.10 , #div(#neg(@x), #neg(@y)) -> #pos(#natdiv(@x, @y)) 555.35/148.10 , *(@x, @y) -> #mult(@x, @y) 555.35/148.10 , filter#2(@xs', @p, @x) -> 555.35/148.10 filter#3(#equal(mod(@x, @p), #0()), @x, @xs') 555.35/148.10 , #pred(#pos(#s(#0()))) -> #0() 555.35/148.10 , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) 555.35/148.10 , #pred(#0()) -> #neg(#s(#0())) 555.35/148.10 , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) } 555.35/148.10 555.35/148.10 We are left with following problem, upon which TcT provides the 555.35/148.10 certificate YES(O(1),O(n^2)). 555.35/148.10 555.35/148.10 Strict DPs: 555.35/148.10 { eratos^#(@l) -> c_1(eratos#1^#(@l)) 555.35/148.10 , eratos#1^#(::(@x, @xs)) -> 555.35/148.10 c_2(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) 555.35/148.10 , filter^#(@p, @l) -> c_3(filter#1^#(@l, @p)) 555.35/148.10 , filter#1^#(::(@x, @xs), @p) -> c_4(filter^#(@p, @xs)) } 555.35/148.10 Weak Trs: 555.35/148.10 { #equal(@x, @y) -> #eq(@x, @y) 555.35/148.10 , #natsub(@x, #0()) -> @x 555.35/148.10 , #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) 555.35/148.10 , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) 555.35/148.10 , #eq(#pos(@x), #0()) -> #false() 555.35/148.10 , #eq(#pos(@x), #neg(@y)) -> #false() 555.35/148.10 , #eq(nil(), nil()) -> #true() 555.35/148.10 , #eq(nil(), ::(@y_1, @y_2)) -> #false() 555.35/148.10 , #eq(::(@x_1, @x_2), nil()) -> #false() 555.35/148.10 , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> 555.35/148.10 #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) 555.35/148.10 , #eq(#0(), #pos(@y)) -> #false() 555.35/148.10 , #eq(#0(), #0()) -> #true() 555.35/148.10 , #eq(#0(), #neg(@y)) -> #false() 555.35/148.10 , #eq(#0(), #s(@y)) -> #false() 555.35/148.10 , #eq(#neg(@x), #pos(@y)) -> #false() 555.35/148.10 , #eq(#neg(@x), #0()) -> #false() 555.35/148.10 , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) 555.35/148.10 , #eq(#s(@x), #0()) -> #false() 555.35/148.10 , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) 555.35/148.10 , #natmult(#0(), @y) -> #0() 555.35/148.10 , #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) 555.35/148.10 , -(@x, @y) -> #sub(@x, @y) 555.35/148.10 , #natdiv(#0(), #0()) -> #divByZero() 555.35/148.10 , #natdiv(#s(@x), #s(@y)) -> #s(#natdiv(#natsub(@x, @y), #s(@y))) 555.35/148.10 , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) 555.35/148.10 , #sub(@x, #0()) -> @x 555.35/148.10 , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) 555.35/148.10 , #add(#pos(#s(#0())), @y) -> #succ(@y) 555.35/148.10 , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) 555.35/148.10 , #add(#0(), @y) -> @y 555.35/148.10 , #add(#neg(#s(#0())), @y) -> #pred(@y) 555.35/148.10 , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) 555.35/148.10 , div(@x, @y) -> #div(@x, @y) 555.35/148.10 , mod(@x, @y) -> -(@x, *(@x, div(@x, @y))) 555.35/148.10 , filter(@p, @l) -> filter#1(@l, @p) 555.35/148.10 , #and(#true(), #true()) -> #true() 555.35/148.10 , #and(#true(), #false()) -> #false() 555.35/148.10 , #and(#false(), #true()) -> #false() 555.35/148.10 , #and(#false(), #false()) -> #false() 555.35/148.10 , filter#3(#true(), @x, @xs') -> @xs' 555.35/148.10 , filter#3(#false(), @x, @xs') -> ::(@x, @xs') 555.35/148.10 , filter#1(nil(), @p) -> nil() 555.35/148.10 , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) 555.35/148.10 , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) 555.35/148.10 , #mult(#pos(@x), #0()) -> #0() 555.35/148.10 , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) 555.35/148.10 , #mult(#0(), #pos(@y)) -> #0() 555.35/148.10 , #mult(#0(), #0()) -> #0() 555.35/148.10 , #mult(#0(), #neg(@y)) -> #0() 555.35/148.10 , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) 555.35/148.10 , #mult(#neg(@x), #0()) -> #0() 555.35/148.10 , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) 555.35/148.10 , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) 555.35/148.10 , #succ(#0()) -> #pos(#s(#0())) 555.35/148.10 , #succ(#neg(#s(#0()))) -> #0() 555.35/148.10 , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) 555.35/148.10 , #div(#pos(@x), #pos(@y)) -> #pos(#natdiv(@x, @y)) 555.35/148.10 , #div(#pos(@x), #0()) -> #divByZero() 555.35/148.10 , #div(#pos(@x), #neg(@y)) -> #neg(#natdiv(@x, @y)) 555.35/148.10 , #div(#0(), #pos(@y)) -> #0() 555.35/148.10 , #div(#0(), #0()) -> #divByZero() 555.35/148.10 , #div(#0(), #neg(@y)) -> #0() 555.35/148.10 , #div(#neg(@x), #pos(@y)) -> #neg(#natdiv(@x, @y)) 555.35/148.10 , #div(#neg(@x), #0()) -> #divByZero() 555.35/148.10 , #div(#neg(@x), #neg(@y)) -> #pos(#natdiv(@x, @y)) 555.35/148.10 , *(@x, @y) -> #mult(@x, @y) 555.35/148.10 , filter#2(@xs', @p, @x) -> 555.35/148.10 filter#3(#equal(mod(@x, @p), #0()), @x, @xs') 555.35/148.10 , #pred(#pos(#s(#0()))) -> #0() 555.35/148.10 , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) 555.35/148.10 , #pred(#0()) -> #neg(#s(#0())) 555.35/148.10 , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) } 555.35/148.10 Obligation: 555.35/148.10 innermost runtime complexity 555.35/148.10 Answer: 555.35/148.10 YES(O(1),O(n^2)) 555.35/148.10 555.35/148.10 We use the processor 'matrix interpretation of dimension 2' to 555.35/148.10 orient following rules strictly. 555.35/148.10 555.35/148.10 DPs: 555.35/148.10 { 4: filter#1^#(::(@x, @xs), @p) -> c_4(filter^#(@p, @xs)) } 555.35/148.10 555.35/148.10 Sub-proof: 555.35/148.10 ---------- 555.35/148.10 The following argument positions are usable: 555.35/148.10 Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1}, 555.35/148.10 Uargs(c_4) = {1} 555.35/148.10 555.35/148.10 TcT has computed the following constructor-based matrix 555.35/148.10 interpretation satisfying not(EDA). 555.35/148.10 555.35/148.10 [#equal](x1, x2) = [0] 555.35/148.10 [0] 555.35/148.10 555.35/148.10 [#natsub](x1, x2) = [0] 555.35/148.10 [0] 555.35/148.10 555.35/148.10 [#eq](x1, x2) = [0] 555.35/148.10 [0] 555.35/148.10 555.35/148.10 [#natmult](x1, x2) = [0] 555.35/148.10 [0] 555.35/148.10 555.35/148.10 [-](x1, x2) = [0] 555.35/148.10 [0] 555.35/148.10 555.35/148.10 [#divByZero] = [7] 555.35/148.10 [0] 555.35/148.10 555.35/148.10 [#true] = [0] 555.35/148.10 [0] 555.35/148.10 555.35/148.10 [#natdiv](x1, x2) = [0] 555.35/148.10 [0] 555.35/148.10 555.35/148.10 [#sub](x1, x2) = [2 0] x1 + [0] 555.35/148.10 [3 2] [0] 555.35/148.10 555.35/148.10 [#add](x1, x2) = [0] 555.35/148.10 [0] 555.35/148.10 555.35/148.10 [#pos](x1) = [0] 555.35/148.10 [0] 555.35/148.10 555.35/148.10 [div](x1, x2) = [0] 555.35/148.10 [0] 555.35/148.10 555.35/148.10 [mod](x1, x2) = [0] 555.35/148.10 [0] 555.35/148.10 555.35/148.10 [filter](x1, x2) = [1 0] x2 + [0] 555.35/148.10 [0 1] [0] 555.35/148.10 555.35/148.10 [#and](x1, x2) = [0] 555.35/148.10 [0] 555.35/148.10 555.35/148.10 [nil] = [0] 555.35/148.10 [0] 555.35/148.10 555.35/148.10 [filter#3](x1, x2, x3) = [1 4] x3 + [0] 555.35/148.10 [0 1] [2] 555.35/148.10 555.35/148.10 [filter#1](x1, x2) = [1 0] x1 + [0] 555.35/148.10 [0 1] [0] 555.35/148.10 555.35/148.10 [#false] = [0] 555.35/148.10 [0] 555.35/148.10 555.35/148.10 [::](x1, x2) = [1 4] x2 + [0] 555.35/148.10 [0 1] [2] 555.35/148.10 555.35/148.10 [#mult](x1, x2) = [0] 555.35/148.10 [0] 555.35/148.10 555.35/148.10 [#succ](x1) = [0] 555.35/148.10 [0] 555.35/148.10 555.35/148.10 [#0] = [0] 555.35/148.10 [0] 555.35/148.10 555.35/148.10 [#div](x1, x2) = [0] 555.35/148.10 [0] 555.35/148.10 555.35/148.10 [*](x1, x2) = [0] 555.35/148.10 [0] 555.35/148.10 555.35/148.10 [#neg](x1) = [0] 555.35/148.10 [0] 555.35/148.10 555.35/148.10 [filter#2](x1, x2, x3) = [1 4] x1 + [0] 555.35/148.10 [0 1] [2] 555.35/148.10 555.35/148.10 [#pred](x1) = [0] 555.35/148.10 [0] 555.35/148.10 555.35/148.10 [#s](x1) = [0] 555.35/148.10 [0] 555.35/148.10 555.35/148.10 [eratos^#](x1) = [2 0] x1 + [0] 555.35/148.10 [0 0] [0] 555.35/148.10 555.35/148.10 [eratos#1^#](x1) = [2 0] x1 + [0] 555.35/148.10 [2 0] [4] 555.35/148.10 555.35/148.10 [filter^#](x1, x2) = [0 0] x1 + [0 1] x2 + [0] 555.35/148.10 [4 0] [4 4] [0] 555.35/148.10 555.35/148.10 [filter#1^#](x1, x2) = [0 1] x1 + [0] 555.35/148.10 [0 4] [0] 555.35/148.10 555.35/148.10 [c_1](x1) = [1 0] x1 + [0] 555.35/148.10 [0 0] [0] 555.35/148.10 555.35/148.10 [c_2](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 555.35/148.10 [0 0] [0 0] [3] 555.35/148.10 555.35/148.10 [c_3](x1) = [1 0] x1 + [0] 555.35/148.10 [0 0] [0] 555.35/148.10 555.35/148.10 [c_4](x1) = [1 0] x1 + [1] 555.35/148.10 [0 0] [7] 555.35/148.10 555.35/148.10 The order satisfies the following ordering constraints: 555.35/148.10 555.35/148.10 [#equal(@x, @y)] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#eq(@x, @y)] 555.35/148.10 555.35/148.10 [#natsub(@x, #0())] = [0] 555.35/148.10 [0] 555.35/148.10 ? [1 0] @x + [0] 555.35/148.10 [0 1] [0] 555.35/148.10 = [@x] 555.35/148.10 555.35/148.10 [#natsub(#s(@x), #s(@y))] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#natsub(@x, @y)] 555.35/148.10 555.35/148.10 [#eq(#pos(@x), #pos(@y))] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#eq(@x, @y)] 555.35/148.10 555.35/148.10 [#eq(#pos(@x), #0())] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#false()] 555.35/148.10 555.35/148.10 [#eq(#pos(@x), #neg(@y))] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#false()] 555.35/148.10 555.35/148.10 [#eq(nil(), nil())] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#true()] 555.35/148.10 555.35/148.10 [#eq(nil(), ::(@y_1, @y_2))] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#false()] 555.35/148.10 555.35/148.10 [#eq(::(@x_1, @x_2), nil())] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#false()] 555.35/148.10 555.35/148.10 [#eq(::(@x_1, @x_2), ::(@y_1, @y_2))] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))] 555.35/148.10 555.35/148.10 [#eq(#0(), #pos(@y))] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#false()] 555.35/148.10 555.35/148.10 [#eq(#0(), #0())] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#true()] 555.35/148.10 555.35/148.10 [#eq(#0(), #neg(@y))] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#false()] 555.35/148.10 555.35/148.10 [#eq(#0(), #s(@y))] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#false()] 555.35/148.10 555.35/148.10 [#eq(#neg(@x), #pos(@y))] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#false()] 555.35/148.10 555.35/148.10 [#eq(#neg(@x), #0())] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#false()] 555.35/148.10 555.35/148.10 [#eq(#neg(@x), #neg(@y))] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#eq(@x, @y)] 555.35/148.10 555.35/148.10 [#eq(#s(@x), #0())] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#false()] 555.35/148.10 555.35/148.10 [#eq(#s(@x), #s(@y))] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#eq(@x, @y)] 555.35/148.10 555.35/148.10 [#natmult(#0(), @y)] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#0()] 555.35/148.10 555.35/148.10 [#natmult(#s(@x), @y)] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#add(#pos(@y), #natmult(@x, @y))] 555.35/148.10 555.35/148.10 [-(@x, @y)] = [0] 555.35/148.10 [0] 555.35/148.10 ? [2 0] @x + [0] 555.35/148.10 [3 2] [0] 555.35/148.10 = [#sub(@x, @y)] 555.35/148.10 555.35/148.10 [#natdiv(#0(), #0())] = [0] 555.35/148.10 [0] 555.35/148.10 ? [7] 555.35/148.10 [0] 555.35/148.10 = [#divByZero()] 555.35/148.10 555.35/148.10 [#natdiv(#s(@x), #s(@y))] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#s(#natdiv(#natsub(@x, @y), #s(@y)))] 555.35/148.10 555.35/148.10 [#sub(@x, #pos(@y))] = [2 0] @x + [0] 555.35/148.10 [3 2] [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#add(@x, #neg(@y))] 555.35/148.10 555.35/148.10 [#sub(@x, #0())] = [2 0] @x + [0] 555.35/148.10 [3 2] [0] 555.35/148.10 >= [1 0] @x + [0] 555.35/148.10 [0 1] [0] 555.35/148.10 = [@x] 555.35/148.10 555.35/148.10 [#sub(@x, #neg(@y))] = [2 0] @x + [0] 555.35/148.10 [3 2] [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#add(@x, #pos(@y))] 555.35/148.10 555.35/148.10 [#add(#pos(#s(#0())), @y)] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#succ(@y)] 555.35/148.10 555.35/148.10 [#add(#pos(#s(#s(@x))), @y)] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#succ(#add(#pos(#s(@x)), @y))] 555.35/148.10 555.35/148.10 [#add(#0(), @y)] = [0] 555.35/148.10 [0] 555.35/148.10 ? [1 0] @y + [0] 555.35/148.10 [0 1] [0] 555.35/148.10 = [@y] 555.35/148.10 555.35/148.10 [#add(#neg(#s(#0())), @y)] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#pred(@y)] 555.35/148.10 555.35/148.10 [#add(#neg(#s(#s(@x))), @y)] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#pred(#add(#pos(#s(@x)), @y))] 555.35/148.10 555.35/148.10 [div(@x, @y)] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#div(@x, @y)] 555.35/148.10 555.35/148.10 [mod(@x, @y)] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [-(@x, *(@x, div(@x, @y)))] 555.35/148.10 555.35/148.10 [filter(@p, @l)] = [1 0] @l + [0] 555.35/148.10 [0 1] [0] 555.35/148.10 >= [1 0] @l + [0] 555.35/148.10 [0 1] [0] 555.35/148.10 = [filter#1(@l, @p)] 555.35/148.10 555.35/148.10 [#and(#true(), #true())] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#true()] 555.35/148.10 555.35/148.10 [#and(#true(), #false())] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#false()] 555.35/148.10 555.35/148.10 [#and(#false(), #true())] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#false()] 555.35/148.10 555.35/148.10 [#and(#false(), #false())] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#false()] 555.35/148.10 555.35/148.10 [filter#3(#true(), @x, @xs')] = [1 4] @xs' + [0] 555.35/148.10 [0 1] [2] 555.35/148.10 >= [1 0] @xs' + [0] 555.35/148.10 [0 1] [0] 555.35/148.10 = [@xs'] 555.35/148.10 555.35/148.10 [filter#3(#false(), @x, @xs')] = [1 4] @xs' + [0] 555.35/148.10 [0 1] [2] 555.35/148.10 >= [1 4] @xs' + [0] 555.35/148.10 [0 1] [2] 555.35/148.10 = [::(@x, @xs')] 555.35/148.10 555.35/148.10 [filter#1(nil(), @p)] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [nil()] 555.35/148.10 555.35/148.10 [filter#1(::(@x, @xs), @p)] = [1 4] @xs + [0] 555.35/148.10 [0 1] [2] 555.35/148.10 >= [1 4] @xs + [0] 555.35/148.10 [0 1] [2] 555.35/148.10 = [filter#2(filter(@p, @xs), @p, @x)] 555.35/148.10 555.35/148.10 [#mult(#pos(@x), #pos(@y))] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#pos(#natmult(@x, @y))] 555.35/148.10 555.35/148.10 [#mult(#pos(@x), #0())] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#0()] 555.35/148.10 555.35/148.10 [#mult(#pos(@x), #neg(@y))] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#neg(#natmult(@x, @y))] 555.35/148.10 555.35/148.10 [#mult(#0(), #pos(@y))] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#0()] 555.35/148.10 555.35/148.10 [#mult(#0(), #0())] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#0()] 555.35/148.10 555.35/148.10 [#mult(#0(), #neg(@y))] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#0()] 555.35/148.10 555.35/148.10 [#mult(#neg(@x), #pos(@y))] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#neg(#natmult(@x, @y))] 555.35/148.10 555.35/148.10 [#mult(#neg(@x), #0())] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#0()] 555.35/148.10 555.35/148.10 [#mult(#neg(@x), #neg(@y))] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#pos(#natmult(@x, @y))] 555.35/148.10 555.35/148.10 [#succ(#pos(#s(@x)))] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#pos(#s(#s(@x)))] 555.35/148.10 555.35/148.10 [#succ(#0())] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#pos(#s(#0()))] 555.35/148.10 555.35/148.10 [#succ(#neg(#s(#0())))] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#0()] 555.35/148.10 555.35/148.10 [#succ(#neg(#s(#s(@x))))] = [0] 555.35/148.10 [0] 555.35/148.10 >= [0] 555.35/148.10 [0] 555.35/148.10 = [#neg(#s(@x))] 555.35/148.10 555.35/148.10 [#div(#pos(@x), #pos(@y))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#pos(#natdiv(@x, @y))] 555.35/148.11 555.35/148.11 [#div(#pos(@x), #0())] = [0] 555.35/148.11 [0] 555.35/148.11 ? [7] 555.35/148.11 [0] 555.35/148.11 = [#divByZero()] 555.35/148.11 555.35/148.11 [#div(#pos(@x), #neg(@y))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#neg(#natdiv(@x, @y))] 555.35/148.11 555.35/148.11 [#div(#0(), #pos(@y))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#0()] 555.35/148.11 555.35/148.11 [#div(#0(), #0())] = [0] 555.35/148.11 [0] 555.35/148.11 ? [7] 555.35/148.11 [0] 555.35/148.11 = [#divByZero()] 555.35/148.11 555.35/148.11 [#div(#0(), #neg(@y))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#0()] 555.35/148.11 555.35/148.11 [#div(#neg(@x), #pos(@y))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#neg(#natdiv(@x, @y))] 555.35/148.11 555.35/148.11 [#div(#neg(@x), #0())] = [0] 555.35/148.11 [0] 555.35/148.11 ? [7] 555.35/148.11 [0] 555.35/148.11 = [#divByZero()] 555.35/148.11 555.35/148.11 [#div(#neg(@x), #neg(@y))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#pos(#natdiv(@x, @y))] 555.35/148.11 555.35/148.11 [*(@x, @y)] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#mult(@x, @y)] 555.35/148.11 555.35/148.11 [filter#2(@xs', @p, @x)] = [1 4] @xs' + [0] 555.35/148.11 [0 1] [2] 555.35/148.11 >= [1 4] @xs' + [0] 555.35/148.11 [0 1] [2] 555.35/148.11 = [filter#3(#equal(mod(@x, @p), #0()), @x, @xs')] 555.35/148.11 555.35/148.11 [#pred(#pos(#s(#0())))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#0()] 555.35/148.11 555.35/148.11 [#pred(#pos(#s(#s(@x))))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#pos(#s(@x))] 555.35/148.11 555.35/148.11 [#pred(#0())] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#neg(#s(#0()))] 555.35/148.11 555.35/148.11 [#pred(#neg(#s(@x)))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#neg(#s(#s(@x)))] 555.35/148.11 555.35/148.11 [eratos^#(@l)] = [2 0] @l + [0] 555.35/148.11 [0 0] [0] 555.35/148.11 >= [2 0] @l + [0] 555.35/148.11 [0 0] [0] 555.35/148.11 = [c_1(eratos#1^#(@l))] 555.35/148.11 555.35/148.11 [eratos#1^#(::(@x, @xs))] = [2 8] @xs + [0] 555.35/148.11 [2 8] [4] 555.35/148.11 >= [2 1] @xs + [0] 555.35/148.11 [0 0] [3] 555.35/148.11 = [c_2(eratos^#(filter(@x, @xs)), filter^#(@x, @xs))] 555.35/148.11 555.35/148.11 [filter^#(@p, @l)] = [0 1] @l + [0 0] @p + [0] 555.35/148.11 [4 4] [4 0] [0] 555.35/148.11 >= [0 1] @l + [0] 555.35/148.11 [0 0] [0] 555.35/148.11 = [c_3(filter#1^#(@l, @p))] 555.35/148.11 555.35/148.11 [filter#1^#(::(@x, @xs), @p)] = [0 1] @xs + [2] 555.35/148.11 [0 4] [8] 555.35/148.11 > [0 1] @xs + [1] 555.35/148.11 [0 0] [7] 555.35/148.11 = [c_4(filter^#(@p, @xs))] 555.35/148.11 555.35/148.11 555.35/148.11 The strictly oriented rules are moved into the weak component. 555.35/148.11 555.35/148.11 We are left with following problem, upon which TcT provides the 555.35/148.11 certificate YES(O(1),O(n^2)). 555.35/148.11 555.35/148.11 Strict DPs: 555.35/148.11 { eratos^#(@l) -> c_1(eratos#1^#(@l)) 555.35/148.11 , eratos#1^#(::(@x, @xs)) -> 555.35/148.11 c_2(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) 555.35/148.11 , filter^#(@p, @l) -> c_3(filter#1^#(@l, @p)) } 555.35/148.11 Weak DPs: { filter#1^#(::(@x, @xs), @p) -> c_4(filter^#(@p, @xs)) } 555.35/148.11 Weak Trs: 555.35/148.11 { #equal(@x, @y) -> #eq(@x, @y) 555.35/148.11 , #natsub(@x, #0()) -> @x 555.35/148.11 , #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) 555.35/148.11 , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) 555.35/148.11 , #eq(#pos(@x), #0()) -> #false() 555.35/148.11 , #eq(#pos(@x), #neg(@y)) -> #false() 555.35/148.11 , #eq(nil(), nil()) -> #true() 555.35/148.11 , #eq(nil(), ::(@y_1, @y_2)) -> #false() 555.35/148.11 , #eq(::(@x_1, @x_2), nil()) -> #false() 555.35/148.11 , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> 555.35/148.11 #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) 555.35/148.11 , #eq(#0(), #pos(@y)) -> #false() 555.35/148.11 , #eq(#0(), #0()) -> #true() 555.35/148.11 , #eq(#0(), #neg(@y)) -> #false() 555.35/148.11 , #eq(#0(), #s(@y)) -> #false() 555.35/148.11 , #eq(#neg(@x), #pos(@y)) -> #false() 555.35/148.11 , #eq(#neg(@x), #0()) -> #false() 555.35/148.11 , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) 555.35/148.11 , #eq(#s(@x), #0()) -> #false() 555.35/148.11 , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) 555.35/148.11 , #natmult(#0(), @y) -> #0() 555.35/148.11 , #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) 555.35/148.11 , -(@x, @y) -> #sub(@x, @y) 555.35/148.11 , #natdiv(#0(), #0()) -> #divByZero() 555.35/148.11 , #natdiv(#s(@x), #s(@y)) -> #s(#natdiv(#natsub(@x, @y), #s(@y))) 555.35/148.11 , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) 555.35/148.11 , #sub(@x, #0()) -> @x 555.35/148.11 , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) 555.35/148.11 , #add(#pos(#s(#0())), @y) -> #succ(@y) 555.35/148.11 , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) 555.35/148.11 , #add(#0(), @y) -> @y 555.35/148.11 , #add(#neg(#s(#0())), @y) -> #pred(@y) 555.35/148.11 , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) 555.35/148.11 , div(@x, @y) -> #div(@x, @y) 555.35/148.11 , mod(@x, @y) -> -(@x, *(@x, div(@x, @y))) 555.35/148.11 , filter(@p, @l) -> filter#1(@l, @p) 555.35/148.11 , #and(#true(), #true()) -> #true() 555.35/148.11 , #and(#true(), #false()) -> #false() 555.35/148.11 , #and(#false(), #true()) -> #false() 555.35/148.11 , #and(#false(), #false()) -> #false() 555.35/148.11 , filter#3(#true(), @x, @xs') -> @xs' 555.35/148.11 , filter#3(#false(), @x, @xs') -> ::(@x, @xs') 555.35/148.11 , filter#1(nil(), @p) -> nil() 555.35/148.11 , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) 555.35/148.11 , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) 555.35/148.11 , #mult(#pos(@x), #0()) -> #0() 555.35/148.11 , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) 555.35/148.11 , #mult(#0(), #pos(@y)) -> #0() 555.35/148.11 , #mult(#0(), #0()) -> #0() 555.35/148.11 , #mult(#0(), #neg(@y)) -> #0() 555.35/148.11 , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) 555.35/148.11 , #mult(#neg(@x), #0()) -> #0() 555.35/148.11 , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) 555.35/148.11 , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) 555.35/148.11 , #succ(#0()) -> #pos(#s(#0())) 555.35/148.11 , #succ(#neg(#s(#0()))) -> #0() 555.35/148.11 , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) 555.35/148.11 , #div(#pos(@x), #pos(@y)) -> #pos(#natdiv(@x, @y)) 555.35/148.11 , #div(#pos(@x), #0()) -> #divByZero() 555.35/148.11 , #div(#pos(@x), #neg(@y)) -> #neg(#natdiv(@x, @y)) 555.35/148.11 , #div(#0(), #pos(@y)) -> #0() 555.35/148.11 , #div(#0(), #0()) -> #divByZero() 555.35/148.11 , #div(#0(), #neg(@y)) -> #0() 555.35/148.11 , #div(#neg(@x), #pos(@y)) -> #neg(#natdiv(@x, @y)) 555.35/148.11 , #div(#neg(@x), #0()) -> #divByZero() 555.35/148.11 , #div(#neg(@x), #neg(@y)) -> #pos(#natdiv(@x, @y)) 555.35/148.11 , *(@x, @y) -> #mult(@x, @y) 555.35/148.11 , filter#2(@xs', @p, @x) -> 555.35/148.11 filter#3(#equal(mod(@x, @p), #0()), @x, @xs') 555.35/148.11 , #pred(#pos(#s(#0()))) -> #0() 555.35/148.11 , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) 555.35/148.11 , #pred(#0()) -> #neg(#s(#0())) 555.35/148.11 , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) } 555.35/148.11 Obligation: 555.35/148.11 innermost runtime complexity 555.35/148.11 Answer: 555.35/148.11 YES(O(1),O(n^2)) 555.35/148.11 555.35/148.11 We use the processor 'matrix interpretation of dimension 2' to 555.35/148.11 orient following rules strictly. 555.35/148.11 555.35/148.11 DPs: 555.35/148.11 { 3: filter^#(@p, @l) -> c_3(filter#1^#(@l, @p)) } 555.35/148.11 Trs: 555.35/148.11 { filter#3(#true(), @x, @xs') -> @xs' 555.35/148.11 , filter#1(nil(), @p) -> nil() } 555.35/148.11 555.35/148.11 Sub-proof: 555.35/148.11 ---------- 555.35/148.11 The following argument positions are usable: 555.35/148.11 Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1}, 555.35/148.11 Uargs(c_4) = {1} 555.35/148.11 555.35/148.11 TcT has computed the following constructor-based matrix 555.35/148.11 interpretation satisfying not(EDA). 555.35/148.11 555.35/148.11 [#equal](x1, x2) = [0] 555.35/148.11 [0] 555.35/148.11 555.35/148.11 [#natsub](x1, x2) = [0] 555.35/148.11 [0] 555.35/148.11 555.35/148.11 [#eq](x1, x2) = [0] 555.35/148.11 [0] 555.35/148.11 555.35/148.11 [#natmult](x1, x2) = [0] 555.35/148.11 [0] 555.35/148.11 555.35/148.11 [-](x1, x2) = [0] 555.35/148.11 [0] 555.35/148.11 555.35/148.11 [#divByZero] = [7] 555.35/148.11 [0] 555.35/148.11 555.35/148.11 [#true] = [0] 555.35/148.11 [0] 555.35/148.11 555.35/148.11 [#natdiv](x1, x2) = [0] 555.35/148.11 [0] 555.35/148.11 555.35/148.11 [#sub](x1, x2) = [3 0] x1 + [0] 555.35/148.11 [3 2] [0] 555.35/148.11 555.35/148.11 [#add](x1, x2) = [0] 555.35/148.11 [0] 555.35/148.11 555.35/148.11 [#pos](x1) = [0 1] x1 + [0] 555.35/148.11 [0 1] [0] 555.35/148.11 555.35/148.11 [div](x1, x2) = [0] 555.35/148.11 [0] 555.35/148.11 555.35/148.11 [mod](x1, x2) = [0] 555.35/148.11 [0] 555.35/148.11 555.35/148.11 [filter](x1, x2) = [1 0] x2 + [3] 555.35/148.11 [0 1] [0] 555.35/148.11 555.35/148.11 [#and](x1, x2) = [0] 555.35/148.11 [0] 555.35/148.11 555.35/148.11 [nil] = [0] 555.35/148.11 [0] 555.35/148.11 555.35/148.11 [filter#3](x1, x2, x3) = [1 4] x3 + [3] 555.35/148.11 [0 1] [1] 555.35/148.11 555.35/148.11 [filter#1](x1, x2) = [1 0] x1 + [3] 555.35/148.11 [0 1] [0] 555.35/148.11 555.35/148.11 [#false] = [0] 555.35/148.11 [0] 555.35/148.11 555.35/148.11 [::](x1, x2) = [1 4] x2 + [3] 555.35/148.11 [0 1] [1] 555.35/148.11 555.35/148.11 [#mult](x1, x2) = [0] 555.35/148.11 [0] 555.35/148.11 555.35/148.11 [#succ](x1) = [0] 555.35/148.11 [0] 555.35/148.11 555.35/148.11 [#0] = [0] 555.35/148.11 [0] 555.35/148.11 555.35/148.11 [#div](x1, x2) = [0] 555.35/148.11 [0] 555.35/148.11 555.35/148.11 [*](x1, x2) = [0] 555.35/148.11 [0] 555.35/148.11 555.35/148.11 [#neg](x1) = [0] 555.35/148.11 [0] 555.35/148.11 555.35/148.11 [filter#2](x1, x2, x3) = [1 4] x1 + [3] 555.35/148.11 [0 1] [1] 555.35/148.11 555.35/148.11 [#pred](x1) = [0] 555.35/148.11 [0] 555.35/148.11 555.35/148.11 [#s](x1) = [0] 555.35/148.11 [0] 555.35/148.11 555.35/148.11 [eratos^#](x1) = [2 2] x1 + [0] 555.35/148.11 [0 0] [0] 555.35/148.11 555.35/148.11 [eratos#1^#](x1) = [2 2] x1 + [0] 555.35/148.11 [0 4] [4] 555.35/148.11 555.35/148.11 [filter^#](x1, x2) = [0 0] x1 + [0 1] x2 + [2] 555.35/148.11 [0 4] [4 4] [0] 555.35/148.11 555.35/148.11 [filter#1^#](x1, x2) = [0 1] x1 + [1] 555.35/148.11 [0 0] [0] 555.35/148.11 555.35/148.11 [c_1](x1) = [1 0] x1 + [0] 555.35/148.11 [0 0] [0] 555.35/148.11 555.35/148.11 [c_2](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 555.35/148.11 [0 0] [0 0] [3] 555.35/148.11 555.35/148.11 [c_3](x1) = [1 0] x1 + [0] 555.35/148.11 [0 0] [0] 555.35/148.11 555.35/148.11 [c_4](x1) = [1 0] x1 + [0] 555.35/148.11 [0 0] [0] 555.35/148.11 555.35/148.11 The order satisfies the following ordering constraints: 555.35/148.11 555.35/148.11 [#equal(@x, @y)] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#eq(@x, @y)] 555.35/148.11 555.35/148.11 [#natsub(@x, #0())] = [0] 555.35/148.11 [0] 555.35/148.11 ? [1 0] @x + [0] 555.35/148.11 [0 1] [0] 555.35/148.11 = [@x] 555.35/148.11 555.35/148.11 [#natsub(#s(@x), #s(@y))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#natsub(@x, @y)] 555.35/148.11 555.35/148.11 [#eq(#pos(@x), #pos(@y))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#eq(@x, @y)] 555.35/148.11 555.35/148.11 [#eq(#pos(@x), #0())] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#false()] 555.35/148.11 555.35/148.11 [#eq(#pos(@x), #neg(@y))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#false()] 555.35/148.11 555.35/148.11 [#eq(nil(), nil())] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#true()] 555.35/148.11 555.35/148.11 [#eq(nil(), ::(@y_1, @y_2))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#false()] 555.35/148.11 555.35/148.11 [#eq(::(@x_1, @x_2), nil())] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#false()] 555.35/148.11 555.35/148.11 [#eq(::(@x_1, @x_2), ::(@y_1, @y_2))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))] 555.35/148.11 555.35/148.11 [#eq(#0(), #pos(@y))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#false()] 555.35/148.11 555.35/148.11 [#eq(#0(), #0())] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#true()] 555.35/148.11 555.35/148.11 [#eq(#0(), #neg(@y))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#false()] 555.35/148.11 555.35/148.11 [#eq(#0(), #s(@y))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#false()] 555.35/148.11 555.35/148.11 [#eq(#neg(@x), #pos(@y))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#false()] 555.35/148.11 555.35/148.11 [#eq(#neg(@x), #0())] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#false()] 555.35/148.11 555.35/148.11 [#eq(#neg(@x), #neg(@y))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#eq(@x, @y)] 555.35/148.11 555.35/148.11 [#eq(#s(@x), #0())] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#false()] 555.35/148.11 555.35/148.11 [#eq(#s(@x), #s(@y))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#eq(@x, @y)] 555.35/148.11 555.35/148.11 [#natmult(#0(), @y)] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#0()] 555.35/148.11 555.35/148.11 [#natmult(#s(@x), @y)] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#add(#pos(@y), #natmult(@x, @y))] 555.35/148.11 555.35/148.11 [-(@x, @y)] = [0] 555.35/148.11 [0] 555.35/148.11 ? [3 0] @x + [0] 555.35/148.11 [3 2] [0] 555.35/148.11 = [#sub(@x, @y)] 555.35/148.11 555.35/148.11 [#natdiv(#0(), #0())] = [0] 555.35/148.11 [0] 555.35/148.11 ? [7] 555.35/148.11 [0] 555.35/148.11 = [#divByZero()] 555.35/148.11 555.35/148.11 [#natdiv(#s(@x), #s(@y))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#s(#natdiv(#natsub(@x, @y), #s(@y)))] 555.35/148.11 555.35/148.11 [#sub(@x, #pos(@y))] = [3 0] @x + [0] 555.35/148.11 [3 2] [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#add(@x, #neg(@y))] 555.35/148.11 555.35/148.11 [#sub(@x, #0())] = [3 0] @x + [0] 555.35/148.11 [3 2] [0] 555.35/148.11 >= [1 0] @x + [0] 555.35/148.11 [0 1] [0] 555.35/148.11 = [@x] 555.35/148.11 555.35/148.11 [#sub(@x, #neg(@y))] = [3 0] @x + [0] 555.35/148.11 [3 2] [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#add(@x, #pos(@y))] 555.35/148.11 555.35/148.11 [#add(#pos(#s(#0())), @y)] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#succ(@y)] 555.35/148.11 555.35/148.11 [#add(#pos(#s(#s(@x))), @y)] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#succ(#add(#pos(#s(@x)), @y))] 555.35/148.11 555.35/148.11 [#add(#0(), @y)] = [0] 555.35/148.11 [0] 555.35/148.11 ? [1 0] @y + [0] 555.35/148.11 [0 1] [0] 555.35/148.11 = [@y] 555.35/148.11 555.35/148.11 [#add(#neg(#s(#0())), @y)] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#pred(@y)] 555.35/148.11 555.35/148.11 [#add(#neg(#s(#s(@x))), @y)] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#pred(#add(#pos(#s(@x)), @y))] 555.35/148.11 555.35/148.11 [div(@x, @y)] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#div(@x, @y)] 555.35/148.11 555.35/148.11 [mod(@x, @y)] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [-(@x, *(@x, div(@x, @y)))] 555.35/148.11 555.35/148.11 [filter(@p, @l)] = [1 0] @l + [3] 555.35/148.11 [0 1] [0] 555.35/148.11 >= [1 0] @l + [3] 555.35/148.11 [0 1] [0] 555.35/148.11 = [filter#1(@l, @p)] 555.35/148.11 555.35/148.11 [#and(#true(), #true())] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#true()] 555.35/148.11 555.35/148.11 [#and(#true(), #false())] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#false()] 555.35/148.11 555.35/148.11 [#and(#false(), #true())] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#false()] 555.35/148.11 555.35/148.11 [#and(#false(), #false())] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#false()] 555.35/148.11 555.35/148.11 [filter#3(#true(), @x, @xs')] = [1 4] @xs' + [3] 555.35/148.11 [0 1] [1] 555.35/148.11 > [1 0] @xs' + [0] 555.35/148.11 [0 1] [0] 555.35/148.11 = [@xs'] 555.35/148.11 555.35/148.11 [filter#3(#false(), @x, @xs')] = [1 4] @xs' + [3] 555.35/148.11 [0 1] [1] 555.35/148.11 >= [1 4] @xs' + [3] 555.35/148.11 [0 1] [1] 555.35/148.11 = [::(@x, @xs')] 555.35/148.11 555.35/148.11 [filter#1(nil(), @p)] = [3] 555.35/148.11 [0] 555.35/148.11 > [0] 555.35/148.11 [0] 555.35/148.11 = [nil()] 555.35/148.11 555.35/148.11 [filter#1(::(@x, @xs), @p)] = [1 4] @xs + [6] 555.35/148.11 [0 1] [1] 555.35/148.11 >= [1 4] @xs + [6] 555.35/148.11 [0 1] [1] 555.35/148.11 = [filter#2(filter(@p, @xs), @p, @x)] 555.35/148.11 555.35/148.11 [#mult(#pos(@x), #pos(@y))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#pos(#natmult(@x, @y))] 555.35/148.11 555.35/148.11 [#mult(#pos(@x), #0())] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#0()] 555.35/148.11 555.35/148.11 [#mult(#pos(@x), #neg(@y))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#neg(#natmult(@x, @y))] 555.35/148.11 555.35/148.11 [#mult(#0(), #pos(@y))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#0()] 555.35/148.11 555.35/148.11 [#mult(#0(), #0())] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#0()] 555.35/148.11 555.35/148.11 [#mult(#0(), #neg(@y))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#0()] 555.35/148.11 555.35/148.11 [#mult(#neg(@x), #pos(@y))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#neg(#natmult(@x, @y))] 555.35/148.11 555.35/148.11 [#mult(#neg(@x), #0())] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#0()] 555.35/148.11 555.35/148.11 [#mult(#neg(@x), #neg(@y))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#pos(#natmult(@x, @y))] 555.35/148.11 555.35/148.11 [#succ(#pos(#s(@x)))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#pos(#s(#s(@x)))] 555.35/148.11 555.35/148.11 [#succ(#0())] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#pos(#s(#0()))] 555.35/148.11 555.35/148.11 [#succ(#neg(#s(#0())))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#0()] 555.35/148.11 555.35/148.11 [#succ(#neg(#s(#s(@x))))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#neg(#s(@x))] 555.35/148.11 555.35/148.11 [#div(#pos(@x), #pos(@y))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#pos(#natdiv(@x, @y))] 555.35/148.11 555.35/148.11 [#div(#pos(@x), #0())] = [0] 555.35/148.11 [0] 555.35/148.11 ? [7] 555.35/148.11 [0] 555.35/148.11 = [#divByZero()] 555.35/148.11 555.35/148.11 [#div(#pos(@x), #neg(@y))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#neg(#natdiv(@x, @y))] 555.35/148.11 555.35/148.11 [#div(#0(), #pos(@y))] = [0] 555.35/148.11 [0] 555.35/148.11 >= [0] 555.35/148.11 [0] 555.35/148.11 = [#0()] 555.35/148.11 555.35/148.11 [#div(#0(), #0())] = [0] 555.35/148.11 [0] 555.35/148.11 ? [7] 555.35/148.11 [0] 555.35/148.11 = [#divByZero()] 555.35/148.11 555.35/148.11 [#div(#0(), #neg(@y))] = [0] 555.35/148.12 [0] 555.35/148.12 >= [0] 555.35/148.12 [0] 555.35/148.12 = [#0()] 555.35/148.12 555.35/148.12 [#div(#neg(@x), #pos(@y))] = [0] 555.35/148.12 [0] 555.35/148.12 >= [0] 555.35/148.12 [0] 555.35/148.12 = [#neg(#natdiv(@x, @y))] 555.35/148.12 555.35/148.12 [#div(#neg(@x), #0())] = [0] 555.35/148.12 [0] 555.35/148.12 ? [7] 555.35/148.12 [0] 555.35/148.12 = [#divByZero()] 555.35/148.12 555.35/148.12 [#div(#neg(@x), #neg(@y))] = [0] 555.35/148.12 [0] 555.35/148.12 >= [0] 555.35/148.12 [0] 555.35/148.12 = [#pos(#natdiv(@x, @y))] 555.35/148.12 555.35/148.12 [*(@x, @y)] = [0] 555.35/148.12 [0] 555.35/148.12 >= [0] 555.35/148.12 [0] 555.35/148.12 = [#mult(@x, @y)] 555.35/148.12 555.35/148.12 [filter#2(@xs', @p, @x)] = [1 4] @xs' + [3] 555.35/148.12 [0 1] [1] 555.35/148.12 >= [1 4] @xs' + [3] 555.35/148.12 [0 1] [1] 555.35/148.12 = [filter#3(#equal(mod(@x, @p), #0()), @x, @xs')] 555.35/148.12 555.35/148.12 [#pred(#pos(#s(#0())))] = [0] 555.35/148.12 [0] 555.35/148.12 >= [0] 555.35/148.12 [0] 555.35/148.12 = [#0()] 555.35/148.12 555.35/148.12 [#pred(#pos(#s(#s(@x))))] = [0] 555.35/148.12 [0] 555.35/148.12 >= [0] 555.35/148.12 [0] 555.35/148.12 = [#pos(#s(@x))] 555.35/148.12 555.35/148.12 [#pred(#0())] = [0] 555.35/148.12 [0] 555.35/148.12 >= [0] 555.35/148.12 [0] 555.35/148.12 = [#neg(#s(#0()))] 555.35/148.12 555.35/148.12 [#pred(#neg(#s(@x)))] = [0] 555.35/148.12 [0] 555.35/148.12 >= [0] 555.35/148.12 [0] 555.35/148.12 = [#neg(#s(#s(@x)))] 555.35/148.12 555.35/148.12 [eratos^#(@l)] = [2 2] @l + [0] 555.35/148.12 [0 0] [0] 555.35/148.12 >= [2 2] @l + [0] 555.35/148.12 [0 0] [0] 555.35/148.12 = [c_1(eratos#1^#(@l))] 555.35/148.12 555.35/148.12 [eratos#1^#(::(@x, @xs))] = [2 10] @xs + [8] 555.35/148.12 [0 4] [8] 555.35/148.12 >= [2 3] @xs + [8] 555.35/148.12 [0 0] [3] 555.35/148.12 = [c_2(eratos^#(filter(@x, @xs)), filter^#(@x, @xs))] 555.35/148.12 555.35/148.12 [filter^#(@p, @l)] = [0 1] @l + [0 0] @p + [2] 555.35/148.12 [4 4] [0 4] [0] 555.35/148.12 > [0 1] @l + [1] 555.35/148.12 [0 0] [0] 555.35/148.12 = [c_3(filter#1^#(@l, @p))] 555.35/148.12 555.35/148.12 [filter#1^#(::(@x, @xs), @p)] = [0 1] @xs + [2] 555.35/148.12 [0 0] [0] 555.35/148.12 >= [0 1] @xs + [2] 555.35/148.12 [0 0] [0] 555.35/148.12 = [c_4(filter^#(@p, @xs))] 555.35/148.12 555.35/148.12 555.35/148.12 We return to the main proof. Consider the set of all dependency 555.35/148.12 pairs 555.35/148.12 555.35/148.12 : 555.35/148.12 { 1: eratos^#(@l) -> c_1(eratos#1^#(@l)) 555.35/148.12 , 2: eratos#1^#(::(@x, @xs)) -> 555.35/148.12 c_2(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) 555.35/148.12 , 3: filter^#(@p, @l) -> c_3(filter#1^#(@l, @p)) 555.35/148.12 , 4: filter#1^#(::(@x, @xs), @p) -> c_4(filter^#(@p, @xs)) } 555.35/148.12 555.35/148.12 Processor 'matrix interpretation of dimension 2' induces the 555.35/148.12 complexity certificate YES(?,O(n^2)) on application of dependency 555.35/148.12 pairs {3}. These cover all (indirect) predecessors of dependency 555.35/148.12 pairs {3,4}, their number of application is equally bounded. The 555.35/148.12 dependency pairs are shifted into the weak component. 555.35/148.12 555.35/148.12 We are left with following problem, upon which TcT provides the 555.35/148.12 certificate YES(O(1),O(n^1)). 555.35/148.12 555.35/148.12 Strict DPs: 555.35/148.12 { eratos^#(@l) -> c_1(eratos#1^#(@l)) 555.35/148.12 , eratos#1^#(::(@x, @xs)) -> 555.35/148.12 c_2(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) } 555.35/148.12 Weak DPs: 555.35/148.12 { filter^#(@p, @l) -> c_3(filter#1^#(@l, @p)) 555.35/148.12 , filter#1^#(::(@x, @xs), @p) -> c_4(filter^#(@p, @xs)) } 555.35/148.12 Weak Trs: 555.35/148.12 { #equal(@x, @y) -> #eq(@x, @y) 555.35/148.12 , #natsub(@x, #0()) -> @x 555.35/148.12 , #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) 555.35/148.12 , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) 555.35/148.12 , #eq(#pos(@x), #0()) -> #false() 555.35/148.12 , #eq(#pos(@x), #neg(@y)) -> #false() 555.35/148.12 , #eq(nil(), nil()) -> #true() 555.35/148.12 , #eq(nil(), ::(@y_1, @y_2)) -> #false() 555.35/148.12 , #eq(::(@x_1, @x_2), nil()) -> #false() 555.35/148.12 , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> 555.35/148.12 #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) 555.35/148.12 , #eq(#0(), #pos(@y)) -> #false() 555.35/148.12 , #eq(#0(), #0()) -> #true() 555.35/148.12 , #eq(#0(), #neg(@y)) -> #false() 555.35/148.12 , #eq(#0(), #s(@y)) -> #false() 555.35/148.12 , #eq(#neg(@x), #pos(@y)) -> #false() 555.35/148.12 , #eq(#neg(@x), #0()) -> #false() 555.35/148.12 , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) 555.35/148.12 , #eq(#s(@x), #0()) -> #false() 555.35/148.12 , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) 555.35/148.12 , #natmult(#0(), @y) -> #0() 555.35/148.12 , #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) 555.35/148.12 , -(@x, @y) -> #sub(@x, @y) 555.35/148.12 , #natdiv(#0(), #0()) -> #divByZero() 555.35/148.12 , #natdiv(#s(@x), #s(@y)) -> #s(#natdiv(#natsub(@x, @y), #s(@y))) 555.35/148.12 , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) 555.35/148.12 , #sub(@x, #0()) -> @x 555.35/148.12 , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) 555.35/148.12 , #add(#pos(#s(#0())), @y) -> #succ(@y) 555.35/148.12 , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) 555.35/148.12 , #add(#0(), @y) -> @y 555.35/148.12 , #add(#neg(#s(#0())), @y) -> #pred(@y) 555.35/148.12 , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) 555.35/148.12 , div(@x, @y) -> #div(@x, @y) 555.35/148.12 , mod(@x, @y) -> -(@x, *(@x, div(@x, @y))) 555.35/148.12 , filter(@p, @l) -> filter#1(@l, @p) 555.35/148.12 , #and(#true(), #true()) -> #true() 555.35/148.12 , #and(#true(), #false()) -> #false() 555.35/148.12 , #and(#false(), #true()) -> #false() 555.35/148.12 , #and(#false(), #false()) -> #false() 555.35/148.12 , filter#3(#true(), @x, @xs') -> @xs' 555.35/148.12 , filter#3(#false(), @x, @xs') -> ::(@x, @xs') 555.35/148.12 , filter#1(nil(), @p) -> nil() 555.35/148.12 , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) 555.35/148.12 , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) 555.35/148.12 , #mult(#pos(@x), #0()) -> #0() 555.35/148.12 , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) 555.35/148.12 , #mult(#0(), #pos(@y)) -> #0() 555.35/148.12 , #mult(#0(), #0()) -> #0() 555.35/148.12 , #mult(#0(), #neg(@y)) -> #0() 555.35/148.12 , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) 555.35/148.12 , #mult(#neg(@x), #0()) -> #0() 555.35/148.12 , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) 555.35/148.12 , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) 555.35/148.12 , #succ(#0()) -> #pos(#s(#0())) 555.35/148.12 , #succ(#neg(#s(#0()))) -> #0() 555.35/148.12 , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) 555.35/148.12 , #div(#pos(@x), #pos(@y)) -> #pos(#natdiv(@x, @y)) 555.35/148.12 , #div(#pos(@x), #0()) -> #divByZero() 555.35/148.12 , #div(#pos(@x), #neg(@y)) -> #neg(#natdiv(@x, @y)) 555.35/148.12 , #div(#0(), #pos(@y)) -> #0() 555.35/148.12 , #div(#0(), #0()) -> #divByZero() 555.35/148.12 , #div(#0(), #neg(@y)) -> #0() 555.35/148.12 , #div(#neg(@x), #pos(@y)) -> #neg(#natdiv(@x, @y)) 555.35/148.12 , #div(#neg(@x), #0()) -> #divByZero() 555.35/148.12 , #div(#neg(@x), #neg(@y)) -> #pos(#natdiv(@x, @y)) 555.35/148.12 , *(@x, @y) -> #mult(@x, @y) 555.35/148.12 , filter#2(@xs', @p, @x) -> 555.35/148.12 filter#3(#equal(mod(@x, @p), #0()), @x, @xs') 555.35/148.12 , #pred(#pos(#s(#0()))) -> #0() 555.35/148.12 , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) 555.35/148.12 , #pred(#0()) -> #neg(#s(#0())) 555.35/148.12 , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) } 555.35/148.12 Obligation: 555.35/148.12 innermost runtime complexity 555.35/148.12 Answer: 555.35/148.12 YES(O(1),O(n^1)) 555.35/148.12 555.35/148.12 The following weak DPs constitute a sub-graph of the DG that is 555.35/148.12 closed under successors. The DPs are removed. 555.35/148.12 555.35/148.12 { filter^#(@p, @l) -> c_3(filter#1^#(@l, @p)) 555.35/148.12 , filter#1^#(::(@x, @xs), @p) -> c_4(filter^#(@p, @xs)) } 555.35/148.12 555.35/148.12 We are left with following problem, upon which TcT provides the 555.35/148.12 certificate YES(O(1),O(n^1)). 555.35/148.12 555.35/148.12 Strict DPs: 555.35/148.12 { eratos^#(@l) -> c_1(eratos#1^#(@l)) 555.35/148.12 , eratos#1^#(::(@x, @xs)) -> 555.35/148.12 c_2(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) } 555.35/148.12 Weak Trs: 555.35/148.12 { #equal(@x, @y) -> #eq(@x, @y) 555.35/148.12 , #natsub(@x, #0()) -> @x 555.35/148.12 , #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) 555.35/148.12 , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) 555.35/148.12 , #eq(#pos(@x), #0()) -> #false() 555.35/148.12 , #eq(#pos(@x), #neg(@y)) -> #false() 555.35/148.12 , #eq(nil(), nil()) -> #true() 555.35/148.12 , #eq(nil(), ::(@y_1, @y_2)) -> #false() 555.35/148.12 , #eq(::(@x_1, @x_2), nil()) -> #false() 555.35/148.12 , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> 555.35/148.12 #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) 555.35/148.12 , #eq(#0(), #pos(@y)) -> #false() 555.35/148.12 , #eq(#0(), #0()) -> #true() 555.35/148.12 , #eq(#0(), #neg(@y)) -> #false() 555.35/148.12 , #eq(#0(), #s(@y)) -> #false() 555.35/148.12 , #eq(#neg(@x), #pos(@y)) -> #false() 555.35/148.12 , #eq(#neg(@x), #0()) -> #false() 555.35/148.12 , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) 555.35/148.12 , #eq(#s(@x), #0()) -> #false() 555.35/148.12 , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) 555.35/148.12 , #natmult(#0(), @y) -> #0() 555.35/148.12 , #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) 555.35/148.12 , -(@x, @y) -> #sub(@x, @y) 555.35/148.12 , #natdiv(#0(), #0()) -> #divByZero() 555.35/148.12 , #natdiv(#s(@x), #s(@y)) -> #s(#natdiv(#natsub(@x, @y), #s(@y))) 555.35/148.12 , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) 555.35/148.12 , #sub(@x, #0()) -> @x 555.35/148.12 , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) 555.35/148.12 , #add(#pos(#s(#0())), @y) -> #succ(@y) 555.35/148.12 , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) 555.35/148.12 , #add(#0(), @y) -> @y 555.35/148.12 , #add(#neg(#s(#0())), @y) -> #pred(@y) 555.35/148.12 , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) 555.35/148.12 , div(@x, @y) -> #div(@x, @y) 555.35/148.12 , mod(@x, @y) -> -(@x, *(@x, div(@x, @y))) 555.35/148.12 , filter(@p, @l) -> filter#1(@l, @p) 555.35/148.12 , #and(#true(), #true()) -> #true() 555.35/148.12 , #and(#true(), #false()) -> #false() 555.35/148.12 , #and(#false(), #true()) -> #false() 555.35/148.12 , #and(#false(), #false()) -> #false() 555.35/148.12 , filter#3(#true(), @x, @xs') -> @xs' 555.35/148.12 , filter#3(#false(), @x, @xs') -> ::(@x, @xs') 555.35/148.12 , filter#1(nil(), @p) -> nil() 555.35/148.12 , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) 555.35/148.12 , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) 555.35/148.12 , #mult(#pos(@x), #0()) -> #0() 555.35/148.12 , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) 555.35/148.12 , #mult(#0(), #pos(@y)) -> #0() 555.35/148.12 , #mult(#0(), #0()) -> #0() 555.35/148.12 , #mult(#0(), #neg(@y)) -> #0() 555.35/148.12 , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) 555.35/148.12 , #mult(#neg(@x), #0()) -> #0() 555.35/148.12 , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) 555.35/148.12 , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) 555.35/148.12 , #succ(#0()) -> #pos(#s(#0())) 555.35/148.12 , #succ(#neg(#s(#0()))) -> #0() 555.35/148.12 , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) 555.35/148.12 , #div(#pos(@x), #pos(@y)) -> #pos(#natdiv(@x, @y)) 555.35/148.12 , #div(#pos(@x), #0()) -> #divByZero() 555.35/148.12 , #div(#pos(@x), #neg(@y)) -> #neg(#natdiv(@x, @y)) 555.35/148.12 , #div(#0(), #pos(@y)) -> #0() 555.35/148.12 , #div(#0(), #0()) -> #divByZero() 555.35/148.12 , #div(#0(), #neg(@y)) -> #0() 555.35/148.12 , #div(#neg(@x), #pos(@y)) -> #neg(#natdiv(@x, @y)) 555.35/148.12 , #div(#neg(@x), #0()) -> #divByZero() 555.35/148.12 , #div(#neg(@x), #neg(@y)) -> #pos(#natdiv(@x, @y)) 555.35/148.12 , *(@x, @y) -> #mult(@x, @y) 555.35/148.12 , filter#2(@xs', @p, @x) -> 555.35/148.12 filter#3(#equal(mod(@x, @p), #0()), @x, @xs') 555.35/148.12 , #pred(#pos(#s(#0()))) -> #0() 555.35/148.12 , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) 555.35/148.12 , #pred(#0()) -> #neg(#s(#0())) 555.35/148.12 , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) } 555.35/148.12 Obligation: 555.35/148.12 innermost runtime complexity 555.35/148.12 Answer: 555.35/148.12 YES(O(1),O(n^1)) 555.35/148.12 555.35/148.12 Due to missing edges in the dependency-graph, the right-hand sides 555.35/148.12 of following rules could be simplified: 555.35/148.12 555.35/148.12 { eratos#1^#(::(@x, @xs)) -> 555.35/148.12 c_2(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) } 555.35/148.12 555.35/148.12 We are left with following problem, upon which TcT provides the 555.35/148.12 certificate YES(O(1),O(n^1)). 555.35/148.12 555.35/148.12 Strict DPs: 555.35/148.12 { eratos^#(@l) -> c_1(eratos#1^#(@l)) 555.35/148.12 , eratos#1^#(::(@x, @xs)) -> c_2(eratos^#(filter(@x, @xs))) } 555.35/148.12 Weak Trs: 555.35/148.12 { #equal(@x, @y) -> #eq(@x, @y) 555.35/148.12 , #natsub(@x, #0()) -> @x 555.35/148.12 , #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) 555.35/148.12 , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) 555.35/148.12 , #eq(#pos(@x), #0()) -> #false() 555.35/148.12 , #eq(#pos(@x), #neg(@y)) -> #false() 555.35/148.12 , #eq(nil(), nil()) -> #true() 555.35/148.12 , #eq(nil(), ::(@y_1, @y_2)) -> #false() 555.35/148.12 , #eq(::(@x_1, @x_2), nil()) -> #false() 555.35/148.12 , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> 555.35/148.12 #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) 555.35/148.12 , #eq(#0(), #pos(@y)) -> #false() 555.35/148.12 , #eq(#0(), #0()) -> #true() 555.35/148.12 , #eq(#0(), #neg(@y)) -> #false() 555.35/148.12 , #eq(#0(), #s(@y)) -> #false() 555.35/148.12 , #eq(#neg(@x), #pos(@y)) -> #false() 555.35/148.12 , #eq(#neg(@x), #0()) -> #false() 555.35/148.12 , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) 555.35/148.12 , #eq(#s(@x), #0()) -> #false() 555.35/148.12 , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) 555.35/148.12 , #natmult(#0(), @y) -> #0() 555.35/148.12 , #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) 555.35/148.12 , -(@x, @y) -> #sub(@x, @y) 555.35/148.12 , #natdiv(#0(), #0()) -> #divByZero() 555.35/148.12 , #natdiv(#s(@x), #s(@y)) -> #s(#natdiv(#natsub(@x, @y), #s(@y))) 555.35/148.12 , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) 555.35/148.12 , #sub(@x, #0()) -> @x 555.35/148.12 , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) 555.35/148.12 , #add(#pos(#s(#0())), @y) -> #succ(@y) 555.35/148.12 , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) 555.35/148.12 , #add(#0(), @y) -> @y 555.35/148.12 , #add(#neg(#s(#0())), @y) -> #pred(@y) 555.35/148.12 , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) 555.35/148.12 , div(@x, @y) -> #div(@x, @y) 555.35/148.12 , mod(@x, @y) -> -(@x, *(@x, div(@x, @y))) 555.35/148.12 , filter(@p, @l) -> filter#1(@l, @p) 555.35/148.12 , #and(#true(), #true()) -> #true() 555.35/148.12 , #and(#true(), #false()) -> #false() 555.35/148.12 , #and(#false(), #true()) -> #false() 555.35/148.12 , #and(#false(), #false()) -> #false() 555.35/148.12 , filter#3(#true(), @x, @xs') -> @xs' 555.35/148.12 , filter#3(#false(), @x, @xs') -> ::(@x, @xs') 555.35/148.12 , filter#1(nil(), @p) -> nil() 555.35/148.12 , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) 555.35/148.12 , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) 555.35/148.12 , #mult(#pos(@x), #0()) -> #0() 555.35/148.12 , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) 555.35/148.12 , #mult(#0(), #pos(@y)) -> #0() 555.35/148.12 , #mult(#0(), #0()) -> #0() 555.35/148.12 , #mult(#0(), #neg(@y)) -> #0() 555.35/148.12 , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) 555.35/148.12 , #mult(#neg(@x), #0()) -> #0() 555.35/148.12 , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) 555.35/148.12 , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) 555.35/148.12 , #succ(#0()) -> #pos(#s(#0())) 555.35/148.12 , #succ(#neg(#s(#0()))) -> #0() 555.35/148.12 , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) 555.35/148.12 , #div(#pos(@x), #pos(@y)) -> #pos(#natdiv(@x, @y)) 555.35/148.12 , #div(#pos(@x), #0()) -> #divByZero() 555.35/148.12 , #div(#pos(@x), #neg(@y)) -> #neg(#natdiv(@x, @y)) 555.35/148.12 , #div(#0(), #pos(@y)) -> #0() 555.35/148.12 , #div(#0(), #0()) -> #divByZero() 555.35/148.12 , #div(#0(), #neg(@y)) -> #0() 555.35/148.12 , #div(#neg(@x), #pos(@y)) -> #neg(#natdiv(@x, @y)) 555.35/148.12 , #div(#neg(@x), #0()) -> #divByZero() 555.35/148.12 , #div(#neg(@x), #neg(@y)) -> #pos(#natdiv(@x, @y)) 555.35/148.12 , *(@x, @y) -> #mult(@x, @y) 555.35/148.12 , filter#2(@xs', @p, @x) -> 555.35/148.12 filter#3(#equal(mod(@x, @p), #0()), @x, @xs') 555.35/148.12 , #pred(#pos(#s(#0()))) -> #0() 555.35/148.12 , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) 555.35/148.12 , #pred(#0()) -> #neg(#s(#0())) 555.35/148.12 , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) } 555.35/148.12 Obligation: 555.35/148.12 innermost runtime complexity 555.35/148.12 Answer: 555.35/148.12 YES(O(1),O(n^1)) 555.35/148.12 555.35/148.12 We use the processor 'matrix interpretation of dimension 1' to 555.35/148.12 orient following rules strictly. 555.35/148.12 555.35/148.12 DPs: 555.35/148.12 { 2: eratos#1^#(::(@x, @xs)) -> c_2(eratos^#(filter(@x, @xs))) } 555.35/148.12 Trs: { filter#3(#true(), @x, @xs') -> @xs' } 555.35/148.12 555.35/148.12 Sub-proof: 555.35/148.12 ---------- 555.35/148.12 The following argument positions are usable: 555.35/148.12 Uargs(c_1) = {1}, Uargs(c_2) = {1} 555.35/148.12 555.35/148.12 TcT has computed the following constructor-based matrix 555.35/148.12 interpretation satisfying not(EDA). 555.35/148.12 555.35/148.12 [#equal](x1, x2) = [0] 555.35/148.12 555.35/148.12 [#natsub](x1, x2) = [0] 555.35/148.12 555.35/148.12 [#eq](x1, x2) = [0] 555.35/148.12 555.35/148.12 [#natmult](x1, x2) = [0] 555.35/148.12 555.35/148.12 [-](x1, x2) = [0] 555.35/148.12 555.35/148.12 [#divByZero] = [7] 555.35/148.12 555.35/148.12 [#true] = [0] 555.35/148.12 555.35/148.12 [#natdiv](x1, x2) = [0] 555.35/148.12 555.35/148.12 [#sub](x1, x2) = [3] x1 + [0] 555.35/148.12 555.35/148.12 [#add](x1, x2) = [0] 555.35/148.12 555.35/148.12 [#pos](x1) = [0] 555.35/148.12 555.35/148.12 [div](x1, x2) = [0] 555.35/148.12 555.35/148.12 [mod](x1, x2) = [0] 555.35/148.12 555.35/148.12 [filter](x1, x2) = [1] x2 + [0] 555.35/148.12 555.35/148.12 [#and](x1, x2) = [0] 555.35/148.12 555.35/148.12 [nil] = [0] 555.35/148.12 555.35/148.12 [filter#3](x1, x2, x3) = [1] x3 + [1] 555.35/148.12 555.35/148.12 [filter#1](x1, x2) = [1] x1 + [0] 555.35/148.12 555.35/148.12 [#false] = [0] 555.35/148.12 555.35/148.12 [::](x1, x2) = [1] x2 + [1] 555.35/148.12 555.35/148.12 [#mult](x1, x2) = [0] 555.35/148.12 555.35/148.12 [#succ](x1) = [0] 555.35/148.12 555.35/148.12 [#0] = [0] 555.35/148.12 555.35/148.12 [#div](x1, x2) = [0] 555.35/148.12 555.35/148.12 [*](x1, x2) = [0] 555.35/148.12 555.35/148.12 [#neg](x1) = [0] 555.35/148.12 555.35/148.12 [filter#2](x1, x2, x3) = [1] x1 + [1] 555.35/148.12 555.35/148.12 [#pred](x1) = [0] 555.35/148.12 555.35/148.12 [#s](x1) = [0] 555.35/148.12 555.35/148.12 [eratos^#](x1) = [1] x1 + [0] 555.35/148.12 555.35/148.12 [eratos#1^#](x1) = [1] x1 + [0] 555.35/148.12 555.35/148.12 [filter^#](x1, x2) = [7] x1 + [7] x2 + [0] 555.35/148.12 555.35/148.12 [filter#1^#](x1, x2) = [7] x1 + [7] x2 + [0] 555.35/148.12 555.35/148.12 [c_1](x1) = [7] x1 + [0] 555.35/148.12 555.35/148.12 [c_2](x1, x2) = [7] x1 + [7] x2 + [0] 555.35/148.12 555.35/148.12 [c_3](x1) = [7] x1 + [0] 555.35/148.12 555.35/148.12 [c_4](x1) = [7] x1 + [0] 555.35/148.12 555.35/148.12 [c] = [0] 555.35/148.12 555.35/148.12 [c_1](x1) = [1] x1 + [0] 555.35/148.12 555.35/148.12 [c_2](x1) = [1] x1 + [0] 555.35/148.12 555.35/148.12 The order satisfies the following ordering constraints: 555.35/148.12 555.35/148.12 [#equal(@x, @y)] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#eq(@x, @y)] 555.35/148.12 555.35/148.12 [#natsub(@x, #0())] = [0] 555.35/148.12 ? [1] @x + [0] 555.35/148.12 = [@x] 555.35/148.12 555.35/148.12 [#natsub(#s(@x), #s(@y))] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#natsub(@x, @y)] 555.35/148.12 555.35/148.12 [#eq(#pos(@x), #pos(@y))] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#eq(@x, @y)] 555.35/148.12 555.35/148.12 [#eq(#pos(@x), #0())] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#false()] 555.35/148.12 555.35/148.12 [#eq(#pos(@x), #neg(@y))] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#false()] 555.35/148.12 555.35/148.12 [#eq(nil(), nil())] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#true()] 555.35/148.12 555.35/148.12 [#eq(nil(), ::(@y_1, @y_2))] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#false()] 555.35/148.12 555.35/148.12 [#eq(::(@x_1, @x_2), nil())] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#false()] 555.35/148.12 555.35/148.12 [#eq(::(@x_1, @x_2), ::(@y_1, @y_2))] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))] 555.35/148.12 555.35/148.12 [#eq(#0(), #pos(@y))] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#false()] 555.35/148.12 555.35/148.12 [#eq(#0(), #0())] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#true()] 555.35/148.12 555.35/148.12 [#eq(#0(), #neg(@y))] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#false()] 555.35/148.12 555.35/148.12 [#eq(#0(), #s(@y))] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#false()] 555.35/148.12 555.35/148.12 [#eq(#neg(@x), #pos(@y))] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#false()] 555.35/148.12 555.35/148.12 [#eq(#neg(@x), #0())] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#false()] 555.35/148.12 555.35/148.12 [#eq(#neg(@x), #neg(@y))] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#eq(@x, @y)] 555.35/148.12 555.35/148.12 [#eq(#s(@x), #0())] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#false()] 555.35/148.12 555.35/148.12 [#eq(#s(@x), #s(@y))] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#eq(@x, @y)] 555.35/148.12 555.35/148.12 [#natmult(#0(), @y)] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#0()] 555.35/148.12 555.35/148.12 [#natmult(#s(@x), @y)] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#add(#pos(@y), #natmult(@x, @y))] 555.35/148.12 555.35/148.12 [-(@x, @y)] = [0] 555.35/148.12 ? [3] @x + [0] 555.35/148.12 = [#sub(@x, @y)] 555.35/148.12 555.35/148.12 [#natdiv(#0(), #0())] = [0] 555.35/148.12 ? [7] 555.35/148.12 = [#divByZero()] 555.35/148.12 555.35/148.12 [#natdiv(#s(@x), #s(@y))] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#s(#natdiv(#natsub(@x, @y), #s(@y)))] 555.35/148.12 555.35/148.12 [#sub(@x, #pos(@y))] = [3] @x + [0] 555.35/148.12 >= [0] 555.35/148.12 = [#add(@x, #neg(@y))] 555.35/148.12 555.35/148.12 [#sub(@x, #0())] = [3] @x + [0] 555.35/148.12 >= [1] @x + [0] 555.35/148.12 = [@x] 555.35/148.12 555.35/148.12 [#sub(@x, #neg(@y))] = [3] @x + [0] 555.35/148.12 >= [0] 555.35/148.12 = [#add(@x, #pos(@y))] 555.35/148.12 555.35/148.12 [#add(#pos(#s(#0())), @y)] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#succ(@y)] 555.35/148.12 555.35/148.12 [#add(#pos(#s(#s(@x))), @y)] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#succ(#add(#pos(#s(@x)), @y))] 555.35/148.12 555.35/148.12 [#add(#0(), @y)] = [0] 555.35/148.12 ? [1] @y + [0] 555.35/148.12 = [@y] 555.35/148.12 555.35/148.12 [#add(#neg(#s(#0())), @y)] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#pred(@y)] 555.35/148.12 555.35/148.12 [#add(#neg(#s(#s(@x))), @y)] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#pred(#add(#pos(#s(@x)), @y))] 555.35/148.12 555.35/148.12 [div(@x, @y)] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#div(@x, @y)] 555.35/148.12 555.35/148.12 [mod(@x, @y)] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [-(@x, *(@x, div(@x, @y)))] 555.35/148.12 555.35/148.12 [filter(@p, @l)] = [1] @l + [0] 555.35/148.12 >= [1] @l + [0] 555.35/148.12 = [filter#1(@l, @p)] 555.35/148.12 555.35/148.12 [#and(#true(), #true())] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#true()] 555.35/148.12 555.35/148.12 [#and(#true(), #false())] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#false()] 555.35/148.12 555.35/148.12 [#and(#false(), #true())] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#false()] 555.35/148.12 555.35/148.12 [#and(#false(), #false())] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#false()] 555.35/148.12 555.35/148.12 [filter#3(#true(), @x, @xs')] = [1] @xs' + [1] 555.35/148.12 > [1] @xs' + [0] 555.35/148.12 = [@xs'] 555.35/148.12 555.35/148.12 [filter#3(#false(), @x, @xs')] = [1] @xs' + [1] 555.35/148.12 >= [1] @xs' + [1] 555.35/148.12 = [::(@x, @xs')] 555.35/148.12 555.35/148.12 [filter#1(nil(), @p)] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [nil()] 555.35/148.12 555.35/148.12 [filter#1(::(@x, @xs), @p)] = [1] @xs + [1] 555.35/148.12 >= [1] @xs + [1] 555.35/148.12 = [filter#2(filter(@p, @xs), @p, @x)] 555.35/148.12 555.35/148.12 [#mult(#pos(@x), #pos(@y))] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#pos(#natmult(@x, @y))] 555.35/148.12 555.35/148.12 [#mult(#pos(@x), #0())] = [0] 555.35/148.12 >= [0] 555.35/148.12 = [#0()] 555.35/148.12 555.35/148.13 [#mult(#pos(@x), #neg(@y))] = [0] 555.35/148.13 >= [0] 555.35/148.13 = [#neg(#natmult(@x, @y))] 555.35/148.13 555.35/148.13 [#mult(#0(), #pos(@y))] = [0] 555.35/148.13 >= [0] 555.35/148.13 = [#0()] 555.35/148.13 555.35/148.13 [#mult(#0(), #0())] = [0] 555.35/148.13 >= [0] 555.35/148.13 = [#0()] 555.35/148.13 555.35/148.13 [#mult(#0(), #neg(@y))] = [0] 555.35/148.13 >= [0] 555.35/148.13 = [#0()] 555.35/148.13 555.35/148.13 [#mult(#neg(@x), #pos(@y))] = [0] 555.35/148.13 >= [0] 555.35/148.13 = [#neg(#natmult(@x, @y))] 555.35/148.13 555.35/148.13 [#mult(#neg(@x), #0())] = [0] 555.35/148.13 >= [0] 555.35/148.13 = [#0()] 555.35/148.13 555.35/148.13 [#mult(#neg(@x), #neg(@y))] = [0] 555.35/148.13 >= [0] 555.35/148.13 = [#pos(#natmult(@x, @y))] 555.35/148.13 555.35/148.13 [#succ(#pos(#s(@x)))] = [0] 555.35/148.13 >= [0] 555.35/148.13 = [#pos(#s(#s(@x)))] 555.35/148.13 555.35/148.13 [#succ(#0())] = [0] 555.35/148.13 >= [0] 555.35/148.13 = [#pos(#s(#0()))] 555.35/148.13 555.35/148.13 [#succ(#neg(#s(#0())))] = [0] 555.35/148.13 >= [0] 555.35/148.13 = [#0()] 555.35/148.13 555.35/148.13 [#succ(#neg(#s(#s(@x))))] = [0] 555.35/148.13 >= [0] 555.35/148.13 = [#neg(#s(@x))] 555.35/148.13 555.35/148.13 [#div(#pos(@x), #pos(@y))] = [0] 555.35/148.13 >= [0] 555.35/148.13 = [#pos(#natdiv(@x, @y))] 555.35/148.13 555.35/148.13 [#div(#pos(@x), #0())] = [0] 555.35/148.13 ? [7] 555.35/148.13 = [#divByZero()] 555.35/148.13 555.35/148.13 [#div(#pos(@x), #neg(@y))] = [0] 555.35/148.13 >= [0] 555.35/148.13 = [#neg(#natdiv(@x, @y))] 555.35/148.13 555.35/148.13 [#div(#0(), #pos(@y))] = [0] 555.35/148.13 >= [0] 555.35/148.13 = [#0()] 555.35/148.13 555.35/148.13 [#div(#0(), #0())] = [0] 555.35/148.13 ? [7] 555.35/148.13 = [#divByZero()] 555.35/148.13 555.35/148.13 [#div(#0(), #neg(@y))] = [0] 555.35/148.13 >= [0] 555.35/148.13 = [#0()] 555.35/148.13 555.35/148.13 [#div(#neg(@x), #pos(@y))] = [0] 555.35/148.13 >= [0] 555.35/148.13 = [#neg(#natdiv(@x, @y))] 555.35/148.13 555.35/148.13 [#div(#neg(@x), #0())] = [0] 555.35/148.13 ? [7] 555.35/148.13 = [#divByZero()] 555.35/148.13 555.35/148.13 [#div(#neg(@x), #neg(@y))] = [0] 555.35/148.13 >= [0] 555.35/148.13 = [#pos(#natdiv(@x, @y))] 555.35/148.13 555.35/148.13 [*(@x, @y)] = [0] 555.35/148.13 >= [0] 555.35/148.13 = [#mult(@x, @y)] 555.35/148.13 555.35/148.13 [filter#2(@xs', @p, @x)] = [1] @xs' + [1] 555.35/148.13 >= [1] @xs' + [1] 555.35/148.13 = [filter#3(#equal(mod(@x, @p), #0()), @x, @xs')] 555.35/148.13 555.35/148.13 [#pred(#pos(#s(#0())))] = [0] 555.35/148.13 >= [0] 555.35/148.13 = [#0()] 555.35/148.13 555.35/148.13 [#pred(#pos(#s(#s(@x))))] = [0] 555.35/148.13 >= [0] 555.35/148.13 = [#pos(#s(@x))] 555.35/148.13 555.35/148.13 [#pred(#0())] = [0] 555.35/148.13 >= [0] 555.35/148.13 = [#neg(#s(#0()))] 555.35/148.13 555.35/148.13 [#pred(#neg(#s(@x)))] = [0] 555.35/148.13 >= [0] 555.35/148.13 = [#neg(#s(#s(@x)))] 555.35/148.13 555.35/148.13 [eratos^#(@l)] = [1] @l + [0] 555.35/148.13 >= [1] @l + [0] 555.35/148.13 = [c_1(eratos#1^#(@l))] 555.35/148.13 555.35/148.13 [eratos#1^#(::(@x, @xs))] = [1] @xs + [1] 555.35/148.13 > [1] @xs + [0] 555.35/148.13 = [c_2(eratos^#(filter(@x, @xs)))] 555.35/148.13 555.35/148.13 555.35/148.13 We return to the main proof. Consider the set of all dependency 555.35/148.13 pairs 555.35/148.13 555.35/148.13 : 555.35/148.13 { 1: eratos^#(@l) -> c_1(eratos#1^#(@l)) 555.35/148.13 , 2: eratos#1^#(::(@x, @xs)) -> c_2(eratos^#(filter(@x, @xs))) } 555.35/148.13 555.35/148.13 Processor 'matrix interpretation of dimension 1' induces the 555.35/148.13 complexity certificate YES(?,O(n^1)) on application of dependency 555.35/148.13 pairs {2}. These cover all (indirect) predecessors of dependency 555.35/148.13 pairs {1,2}, their number of application is equally bounded. The 555.35/148.13 dependency pairs are shifted into the weak component. 555.35/148.13 555.35/148.13 We are left with following problem, upon which TcT provides the 555.35/148.13 certificate YES(O(1),O(1)). 555.35/148.13 555.35/148.13 Weak DPs: 555.35/148.13 { eratos^#(@l) -> c_1(eratos#1^#(@l)) 555.35/148.13 , eratos#1^#(::(@x, @xs)) -> c_2(eratos^#(filter(@x, @xs))) } 555.35/148.13 Weak Trs: 555.35/148.13 { #equal(@x, @y) -> #eq(@x, @y) 555.35/148.13 , #natsub(@x, #0()) -> @x 555.35/148.13 , #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) 555.35/148.13 , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) 555.35/148.13 , #eq(#pos(@x), #0()) -> #false() 555.35/148.13 , #eq(#pos(@x), #neg(@y)) -> #false() 555.35/148.13 , #eq(nil(), nil()) -> #true() 555.35/148.13 , #eq(nil(), ::(@y_1, @y_2)) -> #false() 555.35/148.13 , #eq(::(@x_1, @x_2), nil()) -> #false() 555.35/148.13 , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> 555.35/148.13 #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) 555.35/148.13 , #eq(#0(), #pos(@y)) -> #false() 555.35/148.13 , #eq(#0(), #0()) -> #true() 555.35/148.13 , #eq(#0(), #neg(@y)) -> #false() 555.35/148.13 , #eq(#0(), #s(@y)) -> #false() 555.35/148.13 , #eq(#neg(@x), #pos(@y)) -> #false() 555.35/148.13 , #eq(#neg(@x), #0()) -> #false() 555.35/148.13 , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) 555.35/148.13 , #eq(#s(@x), #0()) -> #false() 555.35/148.13 , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) 555.35/148.13 , #natmult(#0(), @y) -> #0() 555.35/148.13 , #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) 555.35/148.13 , -(@x, @y) -> #sub(@x, @y) 555.35/148.13 , #natdiv(#0(), #0()) -> #divByZero() 555.35/148.13 , #natdiv(#s(@x), #s(@y)) -> #s(#natdiv(#natsub(@x, @y), #s(@y))) 555.35/148.13 , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) 555.35/148.13 , #sub(@x, #0()) -> @x 555.35/148.13 , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) 555.35/148.13 , #add(#pos(#s(#0())), @y) -> #succ(@y) 555.35/148.13 , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) 555.35/148.13 , #add(#0(), @y) -> @y 555.35/148.13 , #add(#neg(#s(#0())), @y) -> #pred(@y) 555.35/148.13 , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) 555.35/148.13 , div(@x, @y) -> #div(@x, @y) 555.35/148.13 , mod(@x, @y) -> -(@x, *(@x, div(@x, @y))) 555.35/148.13 , filter(@p, @l) -> filter#1(@l, @p) 555.35/148.13 , #and(#true(), #true()) -> #true() 555.35/148.13 , #and(#true(), #false()) -> #false() 555.35/148.13 , #and(#false(), #true()) -> #false() 555.35/148.13 , #and(#false(), #false()) -> #false() 555.35/148.13 , filter#3(#true(), @x, @xs') -> @xs' 555.35/148.13 , filter#3(#false(), @x, @xs') -> ::(@x, @xs') 555.35/148.13 , filter#1(nil(), @p) -> nil() 555.35/148.13 , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) 555.35/148.13 , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) 555.35/148.13 , #mult(#pos(@x), #0()) -> #0() 555.35/148.13 , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) 555.35/148.13 , #mult(#0(), #pos(@y)) -> #0() 555.35/148.13 , #mult(#0(), #0()) -> #0() 555.35/148.13 , #mult(#0(), #neg(@y)) -> #0() 555.35/148.13 , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) 555.35/148.13 , #mult(#neg(@x), #0()) -> #0() 555.35/148.13 , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) 555.35/148.13 , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) 555.35/148.13 , #succ(#0()) -> #pos(#s(#0())) 555.35/148.13 , #succ(#neg(#s(#0()))) -> #0() 555.35/148.13 , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) 555.35/148.13 , #div(#pos(@x), #pos(@y)) -> #pos(#natdiv(@x, @y)) 555.35/148.13 , #div(#pos(@x), #0()) -> #divByZero() 555.35/148.13 , #div(#pos(@x), #neg(@y)) -> #neg(#natdiv(@x, @y)) 555.35/148.13 , #div(#0(), #pos(@y)) -> #0() 555.35/148.13 , #div(#0(), #0()) -> #divByZero() 555.35/148.13 , #div(#0(), #neg(@y)) -> #0() 555.35/148.13 , #div(#neg(@x), #pos(@y)) -> #neg(#natdiv(@x, @y)) 555.35/148.13 , #div(#neg(@x), #0()) -> #divByZero() 555.35/148.13 , #div(#neg(@x), #neg(@y)) -> #pos(#natdiv(@x, @y)) 555.35/148.13 , *(@x, @y) -> #mult(@x, @y) 555.35/148.13 , filter#2(@xs', @p, @x) -> 555.35/148.13 filter#3(#equal(mod(@x, @p), #0()), @x, @xs') 555.35/148.13 , #pred(#pos(#s(#0()))) -> #0() 555.35/148.13 , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) 555.35/148.13 , #pred(#0()) -> #neg(#s(#0())) 555.35/148.13 , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) } 555.35/148.13 Obligation: 555.35/148.13 innermost runtime complexity 555.35/148.13 Answer: 555.35/148.13 YES(O(1),O(1)) 555.35/148.13 555.35/148.13 The following weak DPs constitute a sub-graph of the DG that is 555.35/148.13 closed under successors. The DPs are removed. 555.35/148.13 555.35/148.13 { eratos^#(@l) -> c_1(eratos#1^#(@l)) 555.35/148.13 , eratos#1^#(::(@x, @xs)) -> c_2(eratos^#(filter(@x, @xs))) } 555.35/148.13 555.35/148.13 We are left with following problem, upon which TcT provides the 555.35/148.13 certificate YES(O(1),O(1)). 555.35/148.13 555.35/148.13 Weak Trs: 555.35/148.13 { #equal(@x, @y) -> #eq(@x, @y) 555.35/148.13 , #natsub(@x, #0()) -> @x 555.35/148.13 , #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) 555.35/148.13 , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) 555.35/148.13 , #eq(#pos(@x), #0()) -> #false() 555.35/148.13 , #eq(#pos(@x), #neg(@y)) -> #false() 555.35/148.13 , #eq(nil(), nil()) -> #true() 555.35/148.13 , #eq(nil(), ::(@y_1, @y_2)) -> #false() 555.35/148.13 , #eq(::(@x_1, @x_2), nil()) -> #false() 555.35/148.13 , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> 555.35/148.13 #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) 555.35/148.13 , #eq(#0(), #pos(@y)) -> #false() 555.35/148.13 , #eq(#0(), #0()) -> #true() 555.35/148.13 , #eq(#0(), #neg(@y)) -> #false() 555.35/148.13 , #eq(#0(), #s(@y)) -> #false() 555.35/148.13 , #eq(#neg(@x), #pos(@y)) -> #false() 555.35/148.13 , #eq(#neg(@x), #0()) -> #false() 555.35/148.13 , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) 555.35/148.13 , #eq(#s(@x), #0()) -> #false() 555.35/148.13 , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) 555.35/148.13 , #natmult(#0(), @y) -> #0() 555.35/148.13 , #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) 555.35/148.13 , -(@x, @y) -> #sub(@x, @y) 555.35/148.13 , #natdiv(#0(), #0()) -> #divByZero() 555.35/148.13 , #natdiv(#s(@x), #s(@y)) -> #s(#natdiv(#natsub(@x, @y), #s(@y))) 555.35/148.13 , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) 555.35/148.13 , #sub(@x, #0()) -> @x 555.35/148.13 , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) 555.35/148.13 , #add(#pos(#s(#0())), @y) -> #succ(@y) 555.35/148.13 , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) 555.35/148.13 , #add(#0(), @y) -> @y 555.35/148.13 , #add(#neg(#s(#0())), @y) -> #pred(@y) 555.35/148.13 , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) 555.35/148.13 , div(@x, @y) -> #div(@x, @y) 555.35/148.13 , mod(@x, @y) -> -(@x, *(@x, div(@x, @y))) 555.35/148.13 , filter(@p, @l) -> filter#1(@l, @p) 555.35/148.13 , #and(#true(), #true()) -> #true() 555.35/148.13 , #and(#true(), #false()) -> #false() 555.35/148.13 , #and(#false(), #true()) -> #false() 555.35/148.13 , #and(#false(), #false()) -> #false() 555.35/148.13 , filter#3(#true(), @x, @xs') -> @xs' 555.35/148.13 , filter#3(#false(), @x, @xs') -> ::(@x, @xs') 555.35/148.13 , filter#1(nil(), @p) -> nil() 555.35/148.13 , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) 555.35/148.13 , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) 555.35/148.13 , #mult(#pos(@x), #0()) -> #0() 555.35/148.13 , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) 555.35/148.13 , #mult(#0(), #pos(@y)) -> #0() 555.35/148.13 , #mult(#0(), #0()) -> #0() 555.35/148.13 , #mult(#0(), #neg(@y)) -> #0() 555.35/148.13 , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) 555.35/148.13 , #mult(#neg(@x), #0()) -> #0() 555.35/148.13 , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) 555.35/148.13 , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) 555.35/148.13 , #succ(#0()) -> #pos(#s(#0())) 555.35/148.13 , #succ(#neg(#s(#0()))) -> #0() 555.35/148.13 , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) 555.35/148.13 , #div(#pos(@x), #pos(@y)) -> #pos(#natdiv(@x, @y)) 555.35/148.13 , #div(#pos(@x), #0()) -> #divByZero() 555.35/148.13 , #div(#pos(@x), #neg(@y)) -> #neg(#natdiv(@x, @y)) 555.35/148.13 , #div(#0(), #pos(@y)) -> #0() 555.35/148.13 , #div(#0(), #0()) -> #divByZero() 555.35/148.13 , #div(#0(), #neg(@y)) -> #0() 555.35/148.13 , #div(#neg(@x), #pos(@y)) -> #neg(#natdiv(@x, @y)) 555.35/148.13 , #div(#neg(@x), #0()) -> #divByZero() 555.35/148.13 , #div(#neg(@x), #neg(@y)) -> #pos(#natdiv(@x, @y)) 555.35/148.13 , *(@x, @y) -> #mult(@x, @y) 555.35/148.13 , filter#2(@xs', @p, @x) -> 555.35/148.13 filter#3(#equal(mod(@x, @p), #0()), @x, @xs') 555.35/148.13 , #pred(#pos(#s(#0()))) -> #0() 555.35/148.13 , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) 555.35/148.13 , #pred(#0()) -> #neg(#s(#0())) 555.35/148.13 , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) } 555.35/148.13 Obligation: 555.35/148.13 innermost runtime complexity 555.35/148.13 Answer: 555.35/148.13 YES(O(1),O(1)) 555.35/148.13 555.35/148.13 No rule is usable, rules are removed from the input problem. 555.35/148.13 555.35/148.13 We are left with following problem, upon which TcT provides the 555.35/148.13 certificate YES(O(1),O(1)). 555.35/148.13 555.35/148.13 Rules: Empty 555.35/148.13 Obligation: 555.35/148.13 innermost runtime complexity 555.35/148.13 Answer: 555.35/148.13 YES(O(1),O(1)) 555.35/148.13 555.35/148.13 Empty rules are trivially bounded 555.35/148.13 555.35/148.13 Hurray, we answered YES(O(1),O(n^2)) 555.60/148.37 EOF