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