WORST_CASE(?,O(n^2)) * Step 1: DependencyPairs WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #equal(@x,@y) -> #eq(@x,@y) *(@x,@y) -> #mult(@x,@y) -(@x,@y) -> #sub(@x,@y) div(@x,@y) -> #div(@x,@y) eratos(@l) -> eratos#1(@l) eratos#1(::(@x,@xs)) -> ::(@x,eratos(filter(@x,@xs))) eratos#1(nil()) -> nil() filter(@p,@l) -> filter#1(@l,@p) filter#1(::(@x,@xs),@p) -> filter#2(filter(@p,@xs),@p,@x) filter#1(nil(),@p) -> nil() filter#2(@xs',@p,@x) -> filter#3(#equal(mod(@x,@p),#0()),@x,@xs') filter#3(#false(),@x,@xs') -> ::(@x,@xs') filter#3(#true(),@x,@xs') -> @xs' mod(@x,@y) -> -(@x,*(@x,div(@x,@y))) - Weak TRS: #add(#0(),@y) -> @y #add(#neg(#s(#0())),@y) -> #pred(@y) #add(#neg(#s(#s(@x))),@y) -> #pred(#add(#pos(#s(@x)),@y)) #add(#pos(#s(#0())),@y) -> #succ(@y) #add(#pos(#s(#s(@x))),@y) -> #succ(#add(#pos(#s(@x)),@y)) #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #div(#0(),#0()) -> #divByZero() #div(#0(),#neg(@y)) -> #0() #div(#0(),#pos(@y)) -> #0() #div(#neg(@x),#0()) -> #divByZero() #div(#neg(@x),#neg(@y)) -> #pos(#natdiv(@x,@y)) #div(#neg(@x),#pos(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#0()) -> #divByZero() #div(#pos(@x),#neg(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#pos(@y)) -> #pos(#natdiv(@x,@y)) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #mult(#0(),#0()) -> #0() #mult(#0(),#neg(@y)) -> #0() #mult(#0(),#pos(@y)) -> #0() #mult(#neg(@x),#0()) -> #0() #mult(#neg(@x),#neg(@y)) -> #pos(#natmult(@x,@y)) #mult(#neg(@x),#pos(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#0()) -> #0() #mult(#pos(@x),#neg(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#pos(@y)) -> #pos(#natmult(@x,@y)) #natdiv(#0(),#0()) -> #divByZero() #natdiv(#s(@x),#s(@y)) -> #s(#natdiv(#natsub(@x,@y),#s(@y))) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@y),#natmult(@x,@y)) #natsub(@x,#0()) -> @x #natsub(#s(@x),#s(@y)) -> #natsub(@x,@y) #pred(#0()) -> #neg(#s(#0())) #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) #pred(#pos(#s(#0()))) -> #0() #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) #sub(@x,#0()) -> @x #sub(@x,#neg(@y)) -> #add(@x,#pos(@y)) #sub(@x,#pos(@y)) -> #add(@x,#neg(@y)) #succ(#0()) -> #pos(#s(#0())) #succ(#neg(#s(#0()))) -> #0() #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) - Signature: {#add/2,#and/2,#div/2,#eq/2,#equal/2,#mult/2,#natdiv/2,#natmult/2,#natsub/2,#pred/1,#sub/2,#succ/1,*/2,-/2 ,div/2,eratos/1,eratos#1/1,filter/2,filter#1/2,filter#2/3,filter#3/3,mod/2} / {#0/0,#divByZero/0,#false/0 ,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add,#and,#div,#eq,#equal,#mult,#natdiv,#natmult,#natsub ,#pred,#sub,#succ,*,-,div,eratos,eratos#1,filter,filter#1,filter#2,filter#3,mod} and constructors {#0 ,#divByZero,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs #equal#(@x,@y) -> c_1(#eq#(@x,@y)) *#(@x,@y) -> c_2(#mult#(@x,@y)) -#(@x,@y) -> c_3(#sub#(@x,@y)) div#(@x,@y) -> c_4(#div#(@x,@y)) eratos#(@l) -> c_5(eratos#1#(@l)) eratos#1#(::(@x,@xs)) -> c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)) eratos#1#(nil()) -> c_7() filter#(@p,@l) -> c_8(filter#1#(@l,@p)) filter#1#(::(@x,@xs),@p) -> c_9(filter#2#(filter(@p,@xs),@p,@x),filter#(@p,@xs)) filter#1#(nil(),@p) -> c_10() filter#2#(@xs',@p,@x) -> c_11(filter#3#(#equal(mod(@x,@p),#0()),@x,@xs') ,#equal#(mod(@x,@p),#0()) ,mod#(@x,@p)) filter#3#(#false(),@x,@xs') -> c_12() filter#3#(#true(),@x,@xs') -> c_13() mod#(@x,@y) -> c_14(-#(@x,*(@x,div(@x,@y))),*#(@x,div(@x,@y)),div#(@x,@y)) Weak DPs #add#(#0(),@y) -> c_15() #add#(#neg(#s(#0())),@y) -> c_16(#pred#(@y)) #add#(#neg(#s(#s(@x))),@y) -> c_17(#pred#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) #add#(#pos(#s(#0())),@y) -> c_18(#succ#(@y)) #add#(#pos(#s(#s(@x))),@y) -> c_19(#succ#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) #and#(#false(),#false()) -> c_20() #and#(#false(),#true()) -> c_21() #and#(#true(),#false()) -> c_22() #and#(#true(),#true()) -> c_23() #div#(#0(),#0()) -> c_24() #div#(#0(),#neg(@y)) -> c_25() #div#(#0(),#pos(@y)) -> c_26() #div#(#neg(@x),#0()) -> c_27() #div#(#neg(@x),#neg(@y)) -> c_28(#natdiv#(@x,@y)) #div#(#neg(@x),#pos(@y)) -> c_29(#natdiv#(@x,@y)) #div#(#pos(@x),#0()) -> c_30() #div#(#pos(@x),#neg(@y)) -> c_31(#natdiv#(@x,@y)) #div#(#pos(@x),#pos(@y)) -> c_32(#natdiv#(@x,@y)) #eq#(#0(),#0()) -> c_33() #eq#(#0(),#neg(@y)) -> c_34() #eq#(#0(),#pos(@y)) -> c_35() #eq#(#0(),#s(@y)) -> c_36() #eq#(#neg(@x),#0()) -> c_37() #eq#(#neg(@x),#neg(@y)) -> c_38(#eq#(@x,@y)) #eq#(#neg(@x),#pos(@y)) -> c_39() #eq#(#pos(@x),#0()) -> c_40() #eq#(#pos(@x),#neg(@y)) -> c_41() #eq#(#pos(@x),#pos(@y)) -> c_42(#eq#(@x,@y)) #eq#(#s(@x),#0()) -> c_43() #eq#(#s(@x),#s(@y)) -> c_44(#eq#(@x,@y)) #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_45(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)) #eq#(::(@x_1,@x_2),nil()) -> c_46() #eq#(nil(),::(@y_1,@y_2)) -> c_47() #eq#(nil(),nil()) -> c_48() #mult#(#0(),#0()) -> c_49() #mult#(#0(),#neg(@y)) -> c_50() #mult#(#0(),#pos(@y)) -> c_51() #mult#(#neg(@x),#0()) -> c_52() #mult#(#neg(@x),#neg(@y)) -> c_53(#natmult#(@x,@y)) #mult#(#neg(@x),#pos(@y)) -> c_54(#natmult#(@x,@y)) #mult#(#pos(@x),#0()) -> c_55() #mult#(#pos(@x),#neg(@y)) -> c_56(#natmult#(@x,@y)) #mult#(#pos(@x),#pos(@y)) -> c_57(#natmult#(@x,@y)) #natdiv#(#0(),#0()) -> c_58() #natdiv#(#s(@x),#s(@y)) -> c_59(#natdiv#(#natsub(@x,@y),#s(@y)),#natsub#(@x,@y)) #natmult#(#0(),@y) -> c_60() #natmult#(#s(@x),@y) -> c_61(#add#(#pos(@y),#natmult(@x,@y)),#natmult#(@x,@y)) #natsub#(@x,#0()) -> c_62() #natsub#(#s(@x),#s(@y)) -> c_63(#natsub#(@x,@y)) #pred#(#0()) -> c_64() #pred#(#neg(#s(@x))) -> c_65() #pred#(#pos(#s(#0()))) -> c_66() #pred#(#pos(#s(#s(@x)))) -> c_67() #sub#(@x,#0()) -> c_68() #sub#(@x,#neg(@y)) -> c_69(#add#(@x,#pos(@y))) #sub#(@x,#pos(@y)) -> c_70(#add#(@x,#neg(@y))) #succ#(#0()) -> c_71() #succ#(#neg(#s(#0()))) -> c_72() #succ#(#neg(#s(#s(@x)))) -> c_73() #succ#(#pos(#s(@x))) -> c_74() and mark the set of starting terms. * Step 2: UsableRules WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: #equal#(@x,@y) -> c_1(#eq#(@x,@y)) *#(@x,@y) -> c_2(#mult#(@x,@y)) -#(@x,@y) -> c_3(#sub#(@x,@y)) div#(@x,@y) -> c_4(#div#(@x,@y)) eratos#(@l) -> c_5(eratos#1#(@l)) eratos#1#(::(@x,@xs)) -> c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)) eratos#1#(nil()) -> c_7() filter#(@p,@l) -> c_8(filter#1#(@l,@p)) filter#1#(::(@x,@xs),@p) -> c_9(filter#2#(filter(@p,@xs),@p,@x),filter#(@p,@xs)) filter#1#(nil(),@p) -> c_10() filter#2#(@xs',@p,@x) -> c_11(filter#3#(#equal(mod(@x,@p),#0()),@x,@xs') ,#equal#(mod(@x,@p),#0()) ,mod#(@x,@p)) filter#3#(#false(),@x,@xs') -> c_12() filter#3#(#true(),@x,@xs') -> c_13() mod#(@x,@y) -> c_14(-#(@x,*(@x,div(@x,@y))),*#(@x,div(@x,@y)),div#(@x,@y)) - Weak DPs: #add#(#0(),@y) -> c_15() #add#(#neg(#s(#0())),@y) -> c_16(#pred#(@y)) #add#(#neg(#s(#s(@x))),@y) -> c_17(#pred#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) #add#(#pos(#s(#0())),@y) -> c_18(#succ#(@y)) #add#(#pos(#s(#s(@x))),@y) -> c_19(#succ#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) #and#(#false(),#false()) -> c_20() #and#(#false(),#true()) -> c_21() #and#(#true(),#false()) -> c_22() #and#(#true(),#true()) -> c_23() #div#(#0(),#0()) -> c_24() #div#(#0(),#neg(@y)) -> c_25() #div#(#0(),#pos(@y)) -> c_26() #div#(#neg(@x),#0()) -> c_27() #div#(#neg(@x),#neg(@y)) -> c_28(#natdiv#(@x,@y)) #div#(#neg(@x),#pos(@y)) -> c_29(#natdiv#(@x,@y)) #div#(#pos(@x),#0()) -> c_30() #div#(#pos(@x),#neg(@y)) -> c_31(#natdiv#(@x,@y)) #div#(#pos(@x),#pos(@y)) -> c_32(#natdiv#(@x,@y)) #eq#(#0(),#0()) -> c_33() #eq#(#0(),#neg(@y)) -> c_34() #eq#(#0(),#pos(@y)) -> c_35() #eq#(#0(),#s(@y)) -> c_36() #eq#(#neg(@x),#0()) -> c_37() #eq#(#neg(@x),#neg(@y)) -> c_38(#eq#(@x,@y)) #eq#(#neg(@x),#pos(@y)) -> c_39() #eq#(#pos(@x),#0()) -> c_40() #eq#(#pos(@x),#neg(@y)) -> c_41() #eq#(#pos(@x),#pos(@y)) -> c_42(#eq#(@x,@y)) #eq#(#s(@x),#0()) -> c_43() #eq#(#s(@x),#s(@y)) -> c_44(#eq#(@x,@y)) #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_45(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)) #eq#(::(@x_1,@x_2),nil()) -> c_46() #eq#(nil(),::(@y_1,@y_2)) -> c_47() #eq#(nil(),nil()) -> c_48() #mult#(#0(),#0()) -> c_49() #mult#(#0(),#neg(@y)) -> c_50() #mult#(#0(),#pos(@y)) -> c_51() #mult#(#neg(@x),#0()) -> c_52() #mult#(#neg(@x),#neg(@y)) -> c_53(#natmult#(@x,@y)) #mult#(#neg(@x),#pos(@y)) -> c_54(#natmult#(@x,@y)) #mult#(#pos(@x),#0()) -> c_55() #mult#(#pos(@x),#neg(@y)) -> c_56(#natmult#(@x,@y)) #mult#(#pos(@x),#pos(@y)) -> c_57(#natmult#(@x,@y)) #natdiv#(#0(),#0()) -> c_58() #natdiv#(#s(@x),#s(@y)) -> c_59(#natdiv#(#natsub(@x,@y),#s(@y)),#natsub#(@x,@y)) #natmult#(#0(),@y) -> c_60() #natmult#(#s(@x),@y) -> c_61(#add#(#pos(@y),#natmult(@x,@y)),#natmult#(@x,@y)) #natsub#(@x,#0()) -> c_62() #natsub#(#s(@x),#s(@y)) -> c_63(#natsub#(@x,@y)) #pred#(#0()) -> c_64() #pred#(#neg(#s(@x))) -> c_65() #pred#(#pos(#s(#0()))) -> c_66() #pred#(#pos(#s(#s(@x)))) -> c_67() #sub#(@x,#0()) -> c_68() #sub#(@x,#neg(@y)) -> c_69(#add#(@x,#pos(@y))) #sub#(@x,#pos(@y)) -> c_70(#add#(@x,#neg(@y))) #succ#(#0()) -> c_71() #succ#(#neg(#s(#0()))) -> c_72() #succ#(#neg(#s(#s(@x)))) -> c_73() #succ#(#pos(#s(@x))) -> c_74() - Weak TRS: #add(#0(),@y) -> @y #add(#neg(#s(#0())),@y) -> #pred(@y) #add(#neg(#s(#s(@x))),@y) -> #pred(#add(#pos(#s(@x)),@y)) #add(#pos(#s(#0())),@y) -> #succ(@y) #add(#pos(#s(#s(@x))),@y) -> #succ(#add(#pos(#s(@x)),@y)) #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #div(#0(),#0()) -> #divByZero() #div(#0(),#neg(@y)) -> #0() #div(#0(),#pos(@y)) -> #0() #div(#neg(@x),#0()) -> #divByZero() #div(#neg(@x),#neg(@y)) -> #pos(#natdiv(@x,@y)) #div(#neg(@x),#pos(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#0()) -> #divByZero() #div(#pos(@x),#neg(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#pos(@y)) -> #pos(#natdiv(@x,@y)) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #mult(#0(),#0()) -> #0() #mult(#0(),#neg(@y)) -> #0() #mult(#0(),#pos(@y)) -> #0() #mult(#neg(@x),#0()) -> #0() #mult(#neg(@x),#neg(@y)) -> #pos(#natmult(@x,@y)) #mult(#neg(@x),#pos(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#0()) -> #0() #mult(#pos(@x),#neg(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#pos(@y)) -> #pos(#natmult(@x,@y)) #natdiv(#0(),#0()) -> #divByZero() #natdiv(#s(@x),#s(@y)) -> #s(#natdiv(#natsub(@x,@y),#s(@y))) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@y),#natmult(@x,@y)) #natsub(@x,#0()) -> @x #natsub(#s(@x),#s(@y)) -> #natsub(@x,@y) #pred(#0()) -> #neg(#s(#0())) #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) #pred(#pos(#s(#0()))) -> #0() #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) #sub(@x,#0()) -> @x #sub(@x,#neg(@y)) -> #add(@x,#pos(@y)) #sub(@x,#pos(@y)) -> #add(@x,#neg(@y)) #succ(#0()) -> #pos(#s(#0())) #succ(#neg(#s(#0()))) -> #0() #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) *(@x,@y) -> #mult(@x,@y) -(@x,@y) -> #sub(@x,@y) div(@x,@y) -> #div(@x,@y) eratos(@l) -> eratos#1(@l) eratos#1(::(@x,@xs)) -> ::(@x,eratos(filter(@x,@xs))) eratos#1(nil()) -> nil() filter(@p,@l) -> filter#1(@l,@p) filter#1(::(@x,@xs),@p) -> filter#2(filter(@p,@xs),@p,@x) filter#1(nil(),@p) -> nil() filter#2(@xs',@p,@x) -> filter#3(#equal(mod(@x,@p),#0()),@x,@xs') filter#3(#false(),@x,@xs') -> ::(@x,@xs') filter#3(#true(),@x,@xs') -> @xs' mod(@x,@y) -> -(@x,*(@x,div(@x,@y))) - Signature: {#add/2,#and/2,#div/2,#eq/2,#equal/2,#mult/2,#natdiv/2,#natmult/2,#natsub/2,#pred/1,#sub/2,#succ/1,*/2,-/2 ,div/2,eratos/1,eratos#1/1,filter/2,filter#1/2,filter#2/3,filter#3/3,mod/2,#add#/2,#and#/2,#div#/2,#eq#/2 ,#equal#/2,#mult#/2,#natdiv#/2,#natmult#/2,#natsub#/2,#pred#/1,#sub#/2,#succ#/1,*#/2,-#/2,div#/2,eratos#/1 ,eratos#1#/1,filter#/2,filter#1#/2,filter#2#/3,filter#3#/3,mod#/2} / {#0/0,#divByZero/0,#false/0,#neg/1 ,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/2,c_7/0,c_8/1,c_9/2,c_10/0,c_11/3,c_12/0 ,c_13/0,c_14/3,c_15/0,c_16/1,c_17/2,c_18/1,c_19/2,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0 ,c_28/1,c_29/1,c_30/0,c_31/1,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/1,c_39/0,c_40/0,c_41/0,c_42/1 ,c_43/0,c_44/1,c_45/3,c_46/0,c_47/0,c_48/0,c_49/0,c_50/0,c_51/0,c_52/0,c_53/1,c_54/1,c_55/0,c_56/1,c_57/1 ,c_58/0,c_59/2,c_60/0,c_61/2,c_62/0,c_63/1,c_64/0,c_65/0,c_66/0,c_67/0,c_68/0,c_69/1,c_70/1,c_71/0,c_72/0 ,c_73/0,c_74/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult# ,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3# ,mod#} and constructors {#0,#divByZero,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: #add(#0(),@y) -> @y #add(#neg(#s(#0())),@y) -> #pred(@y) #add(#neg(#s(#s(@x))),@y) -> #pred(#add(#pos(#s(@x)),@y)) #add(#pos(#s(#0())),@y) -> #succ(@y) #add(#pos(#s(#s(@x))),@y) -> #succ(#add(#pos(#s(@x)),@y)) #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #div(#0(),#0()) -> #divByZero() #div(#0(),#neg(@y)) -> #0() #div(#0(),#pos(@y)) -> #0() #div(#neg(@x),#0()) -> #divByZero() #div(#neg(@x),#neg(@y)) -> #pos(#natdiv(@x,@y)) #div(#neg(@x),#pos(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#0()) -> #divByZero() #div(#pos(@x),#neg(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#pos(@y)) -> #pos(#natdiv(@x,@y)) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #mult(#0(),#0()) -> #0() #mult(#0(),#neg(@y)) -> #0() #mult(#0(),#pos(@y)) -> #0() #mult(#neg(@x),#0()) -> #0() #mult(#neg(@x),#neg(@y)) -> #pos(#natmult(@x,@y)) #mult(#neg(@x),#pos(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#0()) -> #0() #mult(#pos(@x),#neg(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#pos(@y)) -> #pos(#natmult(@x,@y)) #natdiv(#0(),#0()) -> #divByZero() #natdiv(#s(@x),#s(@y)) -> #s(#natdiv(#natsub(@x,@y),#s(@y))) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@y),#natmult(@x,@y)) #natsub(@x,#0()) -> @x #natsub(#s(@x),#s(@y)) -> #natsub(@x,@y) #pred(#0()) -> #neg(#s(#0())) #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) #pred(#pos(#s(#0()))) -> #0() #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) #sub(@x,#0()) -> @x #sub(@x,#neg(@y)) -> #add(@x,#pos(@y)) #sub(@x,#pos(@y)) -> #add(@x,#neg(@y)) #succ(#0()) -> #pos(#s(#0())) #succ(#neg(#s(#0()))) -> #0() #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) *(@x,@y) -> #mult(@x,@y) -(@x,@y) -> #sub(@x,@y) div(@x,@y) -> #div(@x,@y) filter(@p,@l) -> filter#1(@l,@p) filter#1(::(@x,@xs),@p) -> filter#2(filter(@p,@xs),@p,@x) filter#1(nil(),@p) -> nil() filter#2(@xs',@p,@x) -> filter#3(#equal(mod(@x,@p),#0()),@x,@xs') filter#3(#false(),@x,@xs') -> ::(@x,@xs') filter#3(#true(),@x,@xs') -> @xs' mod(@x,@y) -> -(@x,*(@x,div(@x,@y))) #add#(#0(),@y) -> c_15() #add#(#neg(#s(#0())),@y) -> c_16(#pred#(@y)) #add#(#neg(#s(#s(@x))),@y) -> c_17(#pred#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) #add#(#pos(#s(#0())),@y) -> c_18(#succ#(@y)) #add#(#pos(#s(#s(@x))),@y) -> c_19(#succ#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) #and#(#false(),#false()) -> c_20() #and#(#false(),#true()) -> c_21() #and#(#true(),#false()) -> c_22() #and#(#true(),#true()) -> c_23() #div#(#0(),#0()) -> c_24() #div#(#0(),#neg(@y)) -> c_25() #div#(#0(),#pos(@y)) -> c_26() #div#(#neg(@x),#0()) -> c_27() #div#(#neg(@x),#neg(@y)) -> c_28(#natdiv#(@x,@y)) #div#(#neg(@x),#pos(@y)) -> c_29(#natdiv#(@x,@y)) #div#(#pos(@x),#0()) -> c_30() #div#(#pos(@x),#neg(@y)) -> c_31(#natdiv#(@x,@y)) #div#(#pos(@x),#pos(@y)) -> c_32(#natdiv#(@x,@y)) #eq#(#0(),#0()) -> c_33() #eq#(#0(),#neg(@y)) -> c_34() #eq#(#0(),#pos(@y)) -> c_35() #eq#(#0(),#s(@y)) -> c_36() #eq#(#neg(@x),#0()) -> c_37() #eq#(#neg(@x),#neg(@y)) -> c_38(#eq#(@x,@y)) #eq#(#neg(@x),#pos(@y)) -> c_39() #eq#(#pos(@x),#0()) -> c_40() #eq#(#pos(@x),#neg(@y)) -> c_41() #eq#(#pos(@x),#pos(@y)) -> c_42(#eq#(@x,@y)) #eq#(#s(@x),#0()) -> c_43() #eq#(#s(@x),#s(@y)) -> c_44(#eq#(@x,@y)) #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_45(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)) #eq#(::(@x_1,@x_2),nil()) -> c_46() #eq#(nil(),::(@y_1,@y_2)) -> c_47() #eq#(nil(),nil()) -> c_48() #equal#(@x,@y) -> c_1(#eq#(@x,@y)) #mult#(#0(),#0()) -> c_49() #mult#(#0(),#neg(@y)) -> c_50() #mult#(#0(),#pos(@y)) -> c_51() #mult#(#neg(@x),#0()) -> c_52() #mult#(#neg(@x),#neg(@y)) -> c_53(#natmult#(@x,@y)) #mult#(#neg(@x),#pos(@y)) -> c_54(#natmult#(@x,@y)) #mult#(#pos(@x),#0()) -> c_55() #mult#(#pos(@x),#neg(@y)) -> c_56(#natmult#(@x,@y)) #mult#(#pos(@x),#pos(@y)) -> c_57(#natmult#(@x,@y)) #natdiv#(#0(),#0()) -> c_58() #natdiv#(#s(@x),#s(@y)) -> c_59(#natdiv#(#natsub(@x,@y),#s(@y)),#natsub#(@x,@y)) #natmult#(#0(),@y) -> c_60() #natmult#(#s(@x),@y) -> c_61(#add#(#pos(@y),#natmult(@x,@y)),#natmult#(@x,@y)) #natsub#(@x,#0()) -> c_62() #natsub#(#s(@x),#s(@y)) -> c_63(#natsub#(@x,@y)) #pred#(#0()) -> c_64() #pred#(#neg(#s(@x))) -> c_65() #pred#(#pos(#s(#0()))) -> c_66() #pred#(#pos(#s(#s(@x)))) -> c_67() #sub#(@x,#0()) -> c_68() #sub#(@x,#neg(@y)) -> c_69(#add#(@x,#pos(@y))) #sub#(@x,#pos(@y)) -> c_70(#add#(@x,#neg(@y))) #succ#(#0()) -> c_71() #succ#(#neg(#s(#0()))) -> c_72() #succ#(#neg(#s(#s(@x)))) -> c_73() #succ#(#pos(#s(@x))) -> c_74() *#(@x,@y) -> c_2(#mult#(@x,@y)) -#(@x,@y) -> c_3(#sub#(@x,@y)) div#(@x,@y) -> c_4(#div#(@x,@y)) eratos#(@l) -> c_5(eratos#1#(@l)) eratos#1#(::(@x,@xs)) -> c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)) eratos#1#(nil()) -> c_7() filter#(@p,@l) -> c_8(filter#1#(@l,@p)) filter#1#(::(@x,@xs),@p) -> c_9(filter#2#(filter(@p,@xs),@p,@x),filter#(@p,@xs)) filter#1#(nil(),@p) -> c_10() filter#2#(@xs',@p,@x) -> c_11(filter#3#(#equal(mod(@x,@p),#0()),@x,@xs') ,#equal#(mod(@x,@p),#0()) ,mod#(@x,@p)) filter#3#(#false(),@x,@xs') -> c_12() filter#3#(#true(),@x,@xs') -> c_13() mod#(@x,@y) -> c_14(-#(@x,*(@x,div(@x,@y))),*#(@x,div(@x,@y)),div#(@x,@y)) * Step 3: PredecessorEstimation WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: #equal#(@x,@y) -> c_1(#eq#(@x,@y)) *#(@x,@y) -> c_2(#mult#(@x,@y)) -#(@x,@y) -> c_3(#sub#(@x,@y)) div#(@x,@y) -> c_4(#div#(@x,@y)) eratos#(@l) -> c_5(eratos#1#(@l)) eratos#1#(::(@x,@xs)) -> c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)) eratos#1#(nil()) -> c_7() filter#(@p,@l) -> c_8(filter#1#(@l,@p)) filter#1#(::(@x,@xs),@p) -> c_9(filter#2#(filter(@p,@xs),@p,@x),filter#(@p,@xs)) filter#1#(nil(),@p) -> c_10() filter#2#(@xs',@p,@x) -> c_11(filter#3#(#equal(mod(@x,@p),#0()),@x,@xs') ,#equal#(mod(@x,@p),#0()) ,mod#(@x,@p)) filter#3#(#false(),@x,@xs') -> c_12() filter#3#(#true(),@x,@xs') -> c_13() mod#(@x,@y) -> c_14(-#(@x,*(@x,div(@x,@y))),*#(@x,div(@x,@y)),div#(@x,@y)) - Weak DPs: #add#(#0(),@y) -> c_15() #add#(#neg(#s(#0())),@y) -> c_16(#pred#(@y)) #add#(#neg(#s(#s(@x))),@y) -> c_17(#pred#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) #add#(#pos(#s(#0())),@y) -> c_18(#succ#(@y)) #add#(#pos(#s(#s(@x))),@y) -> c_19(#succ#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) #and#(#false(),#false()) -> c_20() #and#(#false(),#true()) -> c_21() #and#(#true(),#false()) -> c_22() #and#(#true(),#true()) -> c_23() #div#(#0(),#0()) -> c_24() #div#(#0(),#neg(@y)) -> c_25() #div#(#0(),#pos(@y)) -> c_26() #div#(#neg(@x),#0()) -> c_27() #div#(#neg(@x),#neg(@y)) -> c_28(#natdiv#(@x,@y)) #div#(#neg(@x),#pos(@y)) -> c_29(#natdiv#(@x,@y)) #div#(#pos(@x),#0()) -> c_30() #div#(#pos(@x),#neg(@y)) -> c_31(#natdiv#(@x,@y)) #div#(#pos(@x),#pos(@y)) -> c_32(#natdiv#(@x,@y)) #eq#(#0(),#0()) -> c_33() #eq#(#0(),#neg(@y)) -> c_34() #eq#(#0(),#pos(@y)) -> c_35() #eq#(#0(),#s(@y)) -> c_36() #eq#(#neg(@x),#0()) -> c_37() #eq#(#neg(@x),#neg(@y)) -> c_38(#eq#(@x,@y)) #eq#(#neg(@x),#pos(@y)) -> c_39() #eq#(#pos(@x),#0()) -> c_40() #eq#(#pos(@x),#neg(@y)) -> c_41() #eq#(#pos(@x),#pos(@y)) -> c_42(#eq#(@x,@y)) #eq#(#s(@x),#0()) -> c_43() #eq#(#s(@x),#s(@y)) -> c_44(#eq#(@x,@y)) #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_45(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)) #eq#(::(@x_1,@x_2),nil()) -> c_46() #eq#(nil(),::(@y_1,@y_2)) -> c_47() #eq#(nil(),nil()) -> c_48() #mult#(#0(),#0()) -> c_49() #mult#(#0(),#neg(@y)) -> c_50() #mult#(#0(),#pos(@y)) -> c_51() #mult#(#neg(@x),#0()) -> c_52() #mult#(#neg(@x),#neg(@y)) -> c_53(#natmult#(@x,@y)) #mult#(#neg(@x),#pos(@y)) -> c_54(#natmult#(@x,@y)) #mult#(#pos(@x),#0()) -> c_55() #mult#(#pos(@x),#neg(@y)) -> c_56(#natmult#(@x,@y)) #mult#(#pos(@x),#pos(@y)) -> c_57(#natmult#(@x,@y)) #natdiv#(#0(),#0()) -> c_58() #natdiv#(#s(@x),#s(@y)) -> c_59(#natdiv#(#natsub(@x,@y),#s(@y)),#natsub#(@x,@y)) #natmult#(#0(),@y) -> c_60() #natmult#(#s(@x),@y) -> c_61(#add#(#pos(@y),#natmult(@x,@y)),#natmult#(@x,@y)) #natsub#(@x,#0()) -> c_62() #natsub#(#s(@x),#s(@y)) -> c_63(#natsub#(@x,@y)) #pred#(#0()) -> c_64() #pred#(#neg(#s(@x))) -> c_65() #pred#(#pos(#s(#0()))) -> c_66() #pred#(#pos(#s(#s(@x)))) -> c_67() #sub#(@x,#0()) -> c_68() #sub#(@x,#neg(@y)) -> c_69(#add#(@x,#pos(@y))) #sub#(@x,#pos(@y)) -> c_70(#add#(@x,#neg(@y))) #succ#(#0()) -> c_71() #succ#(#neg(#s(#0()))) -> c_72() #succ#(#neg(#s(#s(@x)))) -> c_73() #succ#(#pos(#s(@x))) -> c_74() - Weak TRS: #add(#0(),@y) -> @y #add(#neg(#s(#0())),@y) -> #pred(@y) #add(#neg(#s(#s(@x))),@y) -> #pred(#add(#pos(#s(@x)),@y)) #add(#pos(#s(#0())),@y) -> #succ(@y) #add(#pos(#s(#s(@x))),@y) -> #succ(#add(#pos(#s(@x)),@y)) #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #div(#0(),#0()) -> #divByZero() #div(#0(),#neg(@y)) -> #0() #div(#0(),#pos(@y)) -> #0() #div(#neg(@x),#0()) -> #divByZero() #div(#neg(@x),#neg(@y)) -> #pos(#natdiv(@x,@y)) #div(#neg(@x),#pos(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#0()) -> #divByZero() #div(#pos(@x),#neg(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#pos(@y)) -> #pos(#natdiv(@x,@y)) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #mult(#0(),#0()) -> #0() #mult(#0(),#neg(@y)) -> #0() #mult(#0(),#pos(@y)) -> #0() #mult(#neg(@x),#0()) -> #0() #mult(#neg(@x),#neg(@y)) -> #pos(#natmult(@x,@y)) #mult(#neg(@x),#pos(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#0()) -> #0() #mult(#pos(@x),#neg(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#pos(@y)) -> #pos(#natmult(@x,@y)) #natdiv(#0(),#0()) -> #divByZero() #natdiv(#s(@x),#s(@y)) -> #s(#natdiv(#natsub(@x,@y),#s(@y))) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@y),#natmult(@x,@y)) #natsub(@x,#0()) -> @x #natsub(#s(@x),#s(@y)) -> #natsub(@x,@y) #pred(#0()) -> #neg(#s(#0())) #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) #pred(#pos(#s(#0()))) -> #0() #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) #sub(@x,#0()) -> @x #sub(@x,#neg(@y)) -> #add(@x,#pos(@y)) #sub(@x,#pos(@y)) -> #add(@x,#neg(@y)) #succ(#0()) -> #pos(#s(#0())) #succ(#neg(#s(#0()))) -> #0() #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) *(@x,@y) -> #mult(@x,@y) -(@x,@y) -> #sub(@x,@y) div(@x,@y) -> #div(@x,@y) filter(@p,@l) -> filter#1(@l,@p) filter#1(::(@x,@xs),@p) -> filter#2(filter(@p,@xs),@p,@x) filter#1(nil(),@p) -> nil() filter#2(@xs',@p,@x) -> filter#3(#equal(mod(@x,@p),#0()),@x,@xs') filter#3(#false(),@x,@xs') -> ::(@x,@xs') filter#3(#true(),@x,@xs') -> @xs' mod(@x,@y) -> -(@x,*(@x,div(@x,@y))) - Signature: {#add/2,#and/2,#div/2,#eq/2,#equal/2,#mult/2,#natdiv/2,#natmult/2,#natsub/2,#pred/1,#sub/2,#succ/1,*/2,-/2 ,div/2,eratos/1,eratos#1/1,filter/2,filter#1/2,filter#2/3,filter#3/3,mod/2,#add#/2,#and#/2,#div#/2,#eq#/2 ,#equal#/2,#mult#/2,#natdiv#/2,#natmult#/2,#natsub#/2,#pred#/1,#sub#/2,#succ#/1,*#/2,-#/2,div#/2,eratos#/1 ,eratos#1#/1,filter#/2,filter#1#/2,filter#2#/3,filter#3#/3,mod#/2} / {#0/0,#divByZero/0,#false/0,#neg/1 ,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/2,c_7/0,c_8/1,c_9/2,c_10/0,c_11/3,c_12/0 ,c_13/0,c_14/3,c_15/0,c_16/1,c_17/2,c_18/1,c_19/2,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0 ,c_28/1,c_29/1,c_30/0,c_31/1,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/1,c_39/0,c_40/0,c_41/0,c_42/1 ,c_43/0,c_44/1,c_45/3,c_46/0,c_47/0,c_48/0,c_49/0,c_50/0,c_51/0,c_52/0,c_53/1,c_54/1,c_55/0,c_56/1,c_57/1 ,c_58/0,c_59/2,c_60/0,c_61/2,c_62/0,c_63/1,c_64/0,c_65/0,c_66/0,c_67/0,c_68/0,c_69/1,c_70/1,c_71/0,c_72/0 ,c_73/0,c_74/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult# ,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3# ,mod#} and constructors {#0,#divByZero,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,3,4,7,10,12,13} by application of Pre({1,2,3,4,7,10,12,13}) = {5,8,11,14}. Here rules are labelled as follows: 1: #equal#(@x,@y) -> c_1(#eq#(@x,@y)) 2: *#(@x,@y) -> c_2(#mult#(@x,@y)) 3: -#(@x,@y) -> c_3(#sub#(@x,@y)) 4: div#(@x,@y) -> c_4(#div#(@x,@y)) 5: eratos#(@l) -> c_5(eratos#1#(@l)) 6: eratos#1#(::(@x,@xs)) -> c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)) 7: eratos#1#(nil()) -> c_7() 8: filter#(@p,@l) -> c_8(filter#1#(@l,@p)) 9: filter#1#(::(@x,@xs),@p) -> c_9(filter#2#(filter(@p,@xs),@p,@x),filter#(@p,@xs)) 10: filter#1#(nil(),@p) -> c_10() 11: filter#2#(@xs',@p,@x) -> c_11(filter#3#(#equal(mod(@x,@p),#0()),@x,@xs') ,#equal#(mod(@x,@p),#0()) ,mod#(@x,@p)) 12: filter#3#(#false(),@x,@xs') -> c_12() 13: filter#3#(#true(),@x,@xs') -> c_13() 14: mod#(@x,@y) -> c_14(-#(@x,*(@x,div(@x,@y))),*#(@x,div(@x,@y)),div#(@x,@y)) 15: #add#(#0(),@y) -> c_15() 16: #add#(#neg(#s(#0())),@y) -> c_16(#pred#(@y)) 17: #add#(#neg(#s(#s(@x))),@y) -> c_17(#pred#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) 18: #add#(#pos(#s(#0())),@y) -> c_18(#succ#(@y)) 19: #add#(#pos(#s(#s(@x))),@y) -> c_19(#succ#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) 20: #and#(#false(),#false()) -> c_20() 21: #and#(#false(),#true()) -> c_21() 22: #and#(#true(),#false()) -> c_22() 23: #and#(#true(),#true()) -> c_23() 24: #div#(#0(),#0()) -> c_24() 25: #div#(#0(),#neg(@y)) -> c_25() 26: #div#(#0(),#pos(@y)) -> c_26() 27: #div#(#neg(@x),#0()) -> c_27() 28: #div#(#neg(@x),#neg(@y)) -> c_28(#natdiv#(@x,@y)) 29: #div#(#neg(@x),#pos(@y)) -> c_29(#natdiv#(@x,@y)) 30: #div#(#pos(@x),#0()) -> c_30() 31: #div#(#pos(@x),#neg(@y)) -> c_31(#natdiv#(@x,@y)) 32: #div#(#pos(@x),#pos(@y)) -> c_32(#natdiv#(@x,@y)) 33: #eq#(#0(),#0()) -> c_33() 34: #eq#(#0(),#neg(@y)) -> c_34() 35: #eq#(#0(),#pos(@y)) -> c_35() 36: #eq#(#0(),#s(@y)) -> c_36() 37: #eq#(#neg(@x),#0()) -> c_37() 38: #eq#(#neg(@x),#neg(@y)) -> c_38(#eq#(@x,@y)) 39: #eq#(#neg(@x),#pos(@y)) -> c_39() 40: #eq#(#pos(@x),#0()) -> c_40() 41: #eq#(#pos(@x),#neg(@y)) -> c_41() 42: #eq#(#pos(@x),#pos(@y)) -> c_42(#eq#(@x,@y)) 43: #eq#(#s(@x),#0()) -> c_43() 44: #eq#(#s(@x),#s(@y)) -> c_44(#eq#(@x,@y)) 45: #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_45(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)) 46: #eq#(::(@x_1,@x_2),nil()) -> c_46() 47: #eq#(nil(),::(@y_1,@y_2)) -> c_47() 48: #eq#(nil(),nil()) -> c_48() 49: #mult#(#0(),#0()) -> c_49() 50: #mult#(#0(),#neg(@y)) -> c_50() 51: #mult#(#0(),#pos(@y)) -> c_51() 52: #mult#(#neg(@x),#0()) -> c_52() 53: #mult#(#neg(@x),#neg(@y)) -> c_53(#natmult#(@x,@y)) 54: #mult#(#neg(@x),#pos(@y)) -> c_54(#natmult#(@x,@y)) 55: #mult#(#pos(@x),#0()) -> c_55() 56: #mult#(#pos(@x),#neg(@y)) -> c_56(#natmult#(@x,@y)) 57: #mult#(#pos(@x),#pos(@y)) -> c_57(#natmult#(@x,@y)) 58: #natdiv#(#0(),#0()) -> c_58() 59: #natdiv#(#s(@x),#s(@y)) -> c_59(#natdiv#(#natsub(@x,@y),#s(@y)),#natsub#(@x,@y)) 60: #natmult#(#0(),@y) -> c_60() 61: #natmult#(#s(@x),@y) -> c_61(#add#(#pos(@y),#natmult(@x,@y)),#natmult#(@x,@y)) 62: #natsub#(@x,#0()) -> c_62() 63: #natsub#(#s(@x),#s(@y)) -> c_63(#natsub#(@x,@y)) 64: #pred#(#0()) -> c_64() 65: #pred#(#neg(#s(@x))) -> c_65() 66: #pred#(#pos(#s(#0()))) -> c_66() 67: #pred#(#pos(#s(#s(@x)))) -> c_67() 68: #sub#(@x,#0()) -> c_68() 69: #sub#(@x,#neg(@y)) -> c_69(#add#(@x,#pos(@y))) 70: #sub#(@x,#pos(@y)) -> c_70(#add#(@x,#neg(@y))) 71: #succ#(#0()) -> c_71() 72: #succ#(#neg(#s(#0()))) -> c_72() 73: #succ#(#neg(#s(#s(@x)))) -> c_73() 74: #succ#(#pos(#s(@x))) -> c_74() * Step 4: PredecessorEstimation WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: eratos#(@l) -> c_5(eratos#1#(@l)) eratos#1#(::(@x,@xs)) -> c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)) filter#(@p,@l) -> c_8(filter#1#(@l,@p)) filter#1#(::(@x,@xs),@p) -> c_9(filter#2#(filter(@p,@xs),@p,@x),filter#(@p,@xs)) filter#2#(@xs',@p,@x) -> c_11(filter#3#(#equal(mod(@x,@p),#0()),@x,@xs') ,#equal#(mod(@x,@p),#0()) ,mod#(@x,@p)) mod#(@x,@y) -> c_14(-#(@x,*(@x,div(@x,@y))),*#(@x,div(@x,@y)),div#(@x,@y)) - Weak DPs: #add#(#0(),@y) -> c_15() #add#(#neg(#s(#0())),@y) -> c_16(#pred#(@y)) #add#(#neg(#s(#s(@x))),@y) -> c_17(#pred#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) #add#(#pos(#s(#0())),@y) -> c_18(#succ#(@y)) #add#(#pos(#s(#s(@x))),@y) -> c_19(#succ#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) #and#(#false(),#false()) -> c_20() #and#(#false(),#true()) -> c_21() #and#(#true(),#false()) -> c_22() #and#(#true(),#true()) -> c_23() #div#(#0(),#0()) -> c_24() #div#(#0(),#neg(@y)) -> c_25() #div#(#0(),#pos(@y)) -> c_26() #div#(#neg(@x),#0()) -> c_27() #div#(#neg(@x),#neg(@y)) -> c_28(#natdiv#(@x,@y)) #div#(#neg(@x),#pos(@y)) -> c_29(#natdiv#(@x,@y)) #div#(#pos(@x),#0()) -> c_30() #div#(#pos(@x),#neg(@y)) -> c_31(#natdiv#(@x,@y)) #div#(#pos(@x),#pos(@y)) -> c_32(#natdiv#(@x,@y)) #eq#(#0(),#0()) -> c_33() #eq#(#0(),#neg(@y)) -> c_34() #eq#(#0(),#pos(@y)) -> c_35() #eq#(#0(),#s(@y)) -> c_36() #eq#(#neg(@x),#0()) -> c_37() #eq#(#neg(@x),#neg(@y)) -> c_38(#eq#(@x,@y)) #eq#(#neg(@x),#pos(@y)) -> c_39() #eq#(#pos(@x),#0()) -> c_40() #eq#(#pos(@x),#neg(@y)) -> c_41() #eq#(#pos(@x),#pos(@y)) -> c_42(#eq#(@x,@y)) #eq#(#s(@x),#0()) -> c_43() #eq#(#s(@x),#s(@y)) -> c_44(#eq#(@x,@y)) #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_45(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)) #eq#(::(@x_1,@x_2),nil()) -> c_46() #eq#(nil(),::(@y_1,@y_2)) -> c_47() #eq#(nil(),nil()) -> c_48() #equal#(@x,@y) -> c_1(#eq#(@x,@y)) #mult#(#0(),#0()) -> c_49() #mult#(#0(),#neg(@y)) -> c_50() #mult#(#0(),#pos(@y)) -> c_51() #mult#(#neg(@x),#0()) -> c_52() #mult#(#neg(@x),#neg(@y)) -> c_53(#natmult#(@x,@y)) #mult#(#neg(@x),#pos(@y)) -> c_54(#natmult#(@x,@y)) #mult#(#pos(@x),#0()) -> c_55() #mult#(#pos(@x),#neg(@y)) -> c_56(#natmult#(@x,@y)) #mult#(#pos(@x),#pos(@y)) -> c_57(#natmult#(@x,@y)) #natdiv#(#0(),#0()) -> c_58() #natdiv#(#s(@x),#s(@y)) -> c_59(#natdiv#(#natsub(@x,@y),#s(@y)),#natsub#(@x,@y)) #natmult#(#0(),@y) -> c_60() #natmult#(#s(@x),@y) -> c_61(#add#(#pos(@y),#natmult(@x,@y)),#natmult#(@x,@y)) #natsub#(@x,#0()) -> c_62() #natsub#(#s(@x),#s(@y)) -> c_63(#natsub#(@x,@y)) #pred#(#0()) -> c_64() #pred#(#neg(#s(@x))) -> c_65() #pred#(#pos(#s(#0()))) -> c_66() #pred#(#pos(#s(#s(@x)))) -> c_67() #sub#(@x,#0()) -> c_68() #sub#(@x,#neg(@y)) -> c_69(#add#(@x,#pos(@y))) #sub#(@x,#pos(@y)) -> c_70(#add#(@x,#neg(@y))) #succ#(#0()) -> c_71() #succ#(#neg(#s(#0()))) -> c_72() #succ#(#neg(#s(#s(@x)))) -> c_73() #succ#(#pos(#s(@x))) -> c_74() *#(@x,@y) -> c_2(#mult#(@x,@y)) -#(@x,@y) -> c_3(#sub#(@x,@y)) div#(@x,@y) -> c_4(#div#(@x,@y)) eratos#1#(nil()) -> c_7() filter#1#(nil(),@p) -> c_10() filter#3#(#false(),@x,@xs') -> c_12() filter#3#(#true(),@x,@xs') -> c_13() - Weak TRS: #add(#0(),@y) -> @y #add(#neg(#s(#0())),@y) -> #pred(@y) #add(#neg(#s(#s(@x))),@y) -> #pred(#add(#pos(#s(@x)),@y)) #add(#pos(#s(#0())),@y) -> #succ(@y) #add(#pos(#s(#s(@x))),@y) -> #succ(#add(#pos(#s(@x)),@y)) #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #div(#0(),#0()) -> #divByZero() #div(#0(),#neg(@y)) -> #0() #div(#0(),#pos(@y)) -> #0() #div(#neg(@x),#0()) -> #divByZero() #div(#neg(@x),#neg(@y)) -> #pos(#natdiv(@x,@y)) #div(#neg(@x),#pos(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#0()) -> #divByZero() #div(#pos(@x),#neg(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#pos(@y)) -> #pos(#natdiv(@x,@y)) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #mult(#0(),#0()) -> #0() #mult(#0(),#neg(@y)) -> #0() #mult(#0(),#pos(@y)) -> #0() #mult(#neg(@x),#0()) -> #0() #mult(#neg(@x),#neg(@y)) -> #pos(#natmult(@x,@y)) #mult(#neg(@x),#pos(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#0()) -> #0() #mult(#pos(@x),#neg(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#pos(@y)) -> #pos(#natmult(@x,@y)) #natdiv(#0(),#0()) -> #divByZero() #natdiv(#s(@x),#s(@y)) -> #s(#natdiv(#natsub(@x,@y),#s(@y))) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@y),#natmult(@x,@y)) #natsub(@x,#0()) -> @x #natsub(#s(@x),#s(@y)) -> #natsub(@x,@y) #pred(#0()) -> #neg(#s(#0())) #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) #pred(#pos(#s(#0()))) -> #0() #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) #sub(@x,#0()) -> @x #sub(@x,#neg(@y)) -> #add(@x,#pos(@y)) #sub(@x,#pos(@y)) -> #add(@x,#neg(@y)) #succ(#0()) -> #pos(#s(#0())) #succ(#neg(#s(#0()))) -> #0() #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) *(@x,@y) -> #mult(@x,@y) -(@x,@y) -> #sub(@x,@y) div(@x,@y) -> #div(@x,@y) filter(@p,@l) -> filter#1(@l,@p) filter#1(::(@x,@xs),@p) -> filter#2(filter(@p,@xs),@p,@x) filter#1(nil(),@p) -> nil() filter#2(@xs',@p,@x) -> filter#3(#equal(mod(@x,@p),#0()),@x,@xs') filter#3(#false(),@x,@xs') -> ::(@x,@xs') filter#3(#true(),@x,@xs') -> @xs' mod(@x,@y) -> -(@x,*(@x,div(@x,@y))) - Signature: {#add/2,#and/2,#div/2,#eq/2,#equal/2,#mult/2,#natdiv/2,#natmult/2,#natsub/2,#pred/1,#sub/2,#succ/1,*/2,-/2 ,div/2,eratos/1,eratos#1/1,filter/2,filter#1/2,filter#2/3,filter#3/3,mod/2,#add#/2,#and#/2,#div#/2,#eq#/2 ,#equal#/2,#mult#/2,#natdiv#/2,#natmult#/2,#natsub#/2,#pred#/1,#sub#/2,#succ#/1,*#/2,-#/2,div#/2,eratos#/1 ,eratos#1#/1,filter#/2,filter#1#/2,filter#2#/3,filter#3#/3,mod#/2} / {#0/0,#divByZero/0,#false/0,#neg/1 ,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/2,c_7/0,c_8/1,c_9/2,c_10/0,c_11/3,c_12/0 ,c_13/0,c_14/3,c_15/0,c_16/1,c_17/2,c_18/1,c_19/2,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0 ,c_28/1,c_29/1,c_30/0,c_31/1,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/1,c_39/0,c_40/0,c_41/0,c_42/1 ,c_43/0,c_44/1,c_45/3,c_46/0,c_47/0,c_48/0,c_49/0,c_50/0,c_51/0,c_52/0,c_53/1,c_54/1,c_55/0,c_56/1,c_57/1 ,c_58/0,c_59/2,c_60/0,c_61/2,c_62/0,c_63/1,c_64/0,c_65/0,c_66/0,c_67/0,c_68/0,c_69/1,c_70/1,c_71/0,c_72/0 ,c_73/0,c_74/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult# ,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3# ,mod#} and constructors {#0,#divByZero,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {6} by application of Pre({6}) = {5}. Here rules are labelled as follows: 1: eratos#(@l) -> c_5(eratos#1#(@l)) 2: eratos#1#(::(@x,@xs)) -> c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)) 3: filter#(@p,@l) -> c_8(filter#1#(@l,@p)) 4: filter#1#(::(@x,@xs),@p) -> c_9(filter#2#(filter(@p,@xs),@p,@x),filter#(@p,@xs)) 5: filter#2#(@xs',@p,@x) -> c_11(filter#3#(#equal(mod(@x,@p),#0()),@x,@xs') ,#equal#(mod(@x,@p),#0()) ,mod#(@x,@p)) 6: mod#(@x,@y) -> c_14(-#(@x,*(@x,div(@x,@y))),*#(@x,div(@x,@y)),div#(@x,@y)) 7: #add#(#0(),@y) -> c_15() 8: #add#(#neg(#s(#0())),@y) -> c_16(#pred#(@y)) 9: #add#(#neg(#s(#s(@x))),@y) -> c_17(#pred#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) 10: #add#(#pos(#s(#0())),@y) -> c_18(#succ#(@y)) 11: #add#(#pos(#s(#s(@x))),@y) -> c_19(#succ#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) 12: #and#(#false(),#false()) -> c_20() 13: #and#(#false(),#true()) -> c_21() 14: #and#(#true(),#false()) -> c_22() 15: #and#(#true(),#true()) -> c_23() 16: #div#(#0(),#0()) -> c_24() 17: #div#(#0(),#neg(@y)) -> c_25() 18: #div#(#0(),#pos(@y)) -> c_26() 19: #div#(#neg(@x),#0()) -> c_27() 20: #div#(#neg(@x),#neg(@y)) -> c_28(#natdiv#(@x,@y)) 21: #div#(#neg(@x),#pos(@y)) -> c_29(#natdiv#(@x,@y)) 22: #div#(#pos(@x),#0()) -> c_30() 23: #div#(#pos(@x),#neg(@y)) -> c_31(#natdiv#(@x,@y)) 24: #div#(#pos(@x),#pos(@y)) -> c_32(#natdiv#(@x,@y)) 25: #eq#(#0(),#0()) -> c_33() 26: #eq#(#0(),#neg(@y)) -> c_34() 27: #eq#(#0(),#pos(@y)) -> c_35() 28: #eq#(#0(),#s(@y)) -> c_36() 29: #eq#(#neg(@x),#0()) -> c_37() 30: #eq#(#neg(@x),#neg(@y)) -> c_38(#eq#(@x,@y)) 31: #eq#(#neg(@x),#pos(@y)) -> c_39() 32: #eq#(#pos(@x),#0()) -> c_40() 33: #eq#(#pos(@x),#neg(@y)) -> c_41() 34: #eq#(#pos(@x),#pos(@y)) -> c_42(#eq#(@x,@y)) 35: #eq#(#s(@x),#0()) -> c_43() 36: #eq#(#s(@x),#s(@y)) -> c_44(#eq#(@x,@y)) 37: #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_45(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)) 38: #eq#(::(@x_1,@x_2),nil()) -> c_46() 39: #eq#(nil(),::(@y_1,@y_2)) -> c_47() 40: #eq#(nil(),nil()) -> c_48() 41: #equal#(@x,@y) -> c_1(#eq#(@x,@y)) 42: #mult#(#0(),#0()) -> c_49() 43: #mult#(#0(),#neg(@y)) -> c_50() 44: #mult#(#0(),#pos(@y)) -> c_51() 45: #mult#(#neg(@x),#0()) -> c_52() 46: #mult#(#neg(@x),#neg(@y)) -> c_53(#natmult#(@x,@y)) 47: #mult#(#neg(@x),#pos(@y)) -> c_54(#natmult#(@x,@y)) 48: #mult#(#pos(@x),#0()) -> c_55() 49: #mult#(#pos(@x),#neg(@y)) -> c_56(#natmult#(@x,@y)) 50: #mult#(#pos(@x),#pos(@y)) -> c_57(#natmult#(@x,@y)) 51: #natdiv#(#0(),#0()) -> c_58() 52: #natdiv#(#s(@x),#s(@y)) -> c_59(#natdiv#(#natsub(@x,@y),#s(@y)),#natsub#(@x,@y)) 53: #natmult#(#0(),@y) -> c_60() 54: #natmult#(#s(@x),@y) -> c_61(#add#(#pos(@y),#natmult(@x,@y)),#natmult#(@x,@y)) 55: #natsub#(@x,#0()) -> c_62() 56: #natsub#(#s(@x),#s(@y)) -> c_63(#natsub#(@x,@y)) 57: #pred#(#0()) -> c_64() 58: #pred#(#neg(#s(@x))) -> c_65() 59: #pred#(#pos(#s(#0()))) -> c_66() 60: #pred#(#pos(#s(#s(@x)))) -> c_67() 61: #sub#(@x,#0()) -> c_68() 62: #sub#(@x,#neg(@y)) -> c_69(#add#(@x,#pos(@y))) 63: #sub#(@x,#pos(@y)) -> c_70(#add#(@x,#neg(@y))) 64: #succ#(#0()) -> c_71() 65: #succ#(#neg(#s(#0()))) -> c_72() 66: #succ#(#neg(#s(#s(@x)))) -> c_73() 67: #succ#(#pos(#s(@x))) -> c_74() 68: *#(@x,@y) -> c_2(#mult#(@x,@y)) 69: -#(@x,@y) -> c_3(#sub#(@x,@y)) 70: div#(@x,@y) -> c_4(#div#(@x,@y)) 71: eratos#1#(nil()) -> c_7() 72: filter#1#(nil(),@p) -> c_10() 73: filter#3#(#false(),@x,@xs') -> c_12() 74: filter#3#(#true(),@x,@xs') -> c_13() * Step 5: PredecessorEstimation WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: eratos#(@l) -> c_5(eratos#1#(@l)) eratos#1#(::(@x,@xs)) -> c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)) filter#(@p,@l) -> c_8(filter#1#(@l,@p)) filter#1#(::(@x,@xs),@p) -> c_9(filter#2#(filter(@p,@xs),@p,@x),filter#(@p,@xs)) filter#2#(@xs',@p,@x) -> c_11(filter#3#(#equal(mod(@x,@p),#0()),@x,@xs') ,#equal#(mod(@x,@p),#0()) ,mod#(@x,@p)) - Weak DPs: #add#(#0(),@y) -> c_15() #add#(#neg(#s(#0())),@y) -> c_16(#pred#(@y)) #add#(#neg(#s(#s(@x))),@y) -> c_17(#pred#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) #add#(#pos(#s(#0())),@y) -> c_18(#succ#(@y)) #add#(#pos(#s(#s(@x))),@y) -> c_19(#succ#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) #and#(#false(),#false()) -> c_20() #and#(#false(),#true()) -> c_21() #and#(#true(),#false()) -> c_22() #and#(#true(),#true()) -> c_23() #div#(#0(),#0()) -> c_24() #div#(#0(),#neg(@y)) -> c_25() #div#(#0(),#pos(@y)) -> c_26() #div#(#neg(@x),#0()) -> c_27() #div#(#neg(@x),#neg(@y)) -> c_28(#natdiv#(@x,@y)) #div#(#neg(@x),#pos(@y)) -> c_29(#natdiv#(@x,@y)) #div#(#pos(@x),#0()) -> c_30() #div#(#pos(@x),#neg(@y)) -> c_31(#natdiv#(@x,@y)) #div#(#pos(@x),#pos(@y)) -> c_32(#natdiv#(@x,@y)) #eq#(#0(),#0()) -> c_33() #eq#(#0(),#neg(@y)) -> c_34() #eq#(#0(),#pos(@y)) -> c_35() #eq#(#0(),#s(@y)) -> c_36() #eq#(#neg(@x),#0()) -> c_37() #eq#(#neg(@x),#neg(@y)) -> c_38(#eq#(@x,@y)) #eq#(#neg(@x),#pos(@y)) -> c_39() #eq#(#pos(@x),#0()) -> c_40() #eq#(#pos(@x),#neg(@y)) -> c_41() #eq#(#pos(@x),#pos(@y)) -> c_42(#eq#(@x,@y)) #eq#(#s(@x),#0()) -> c_43() #eq#(#s(@x),#s(@y)) -> c_44(#eq#(@x,@y)) #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_45(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)) #eq#(::(@x_1,@x_2),nil()) -> c_46() #eq#(nil(),::(@y_1,@y_2)) -> c_47() #eq#(nil(),nil()) -> c_48() #equal#(@x,@y) -> c_1(#eq#(@x,@y)) #mult#(#0(),#0()) -> c_49() #mult#(#0(),#neg(@y)) -> c_50() #mult#(#0(),#pos(@y)) -> c_51() #mult#(#neg(@x),#0()) -> c_52() #mult#(#neg(@x),#neg(@y)) -> c_53(#natmult#(@x,@y)) #mult#(#neg(@x),#pos(@y)) -> c_54(#natmult#(@x,@y)) #mult#(#pos(@x),#0()) -> c_55() #mult#(#pos(@x),#neg(@y)) -> c_56(#natmult#(@x,@y)) #mult#(#pos(@x),#pos(@y)) -> c_57(#natmult#(@x,@y)) #natdiv#(#0(),#0()) -> c_58() #natdiv#(#s(@x),#s(@y)) -> c_59(#natdiv#(#natsub(@x,@y),#s(@y)),#natsub#(@x,@y)) #natmult#(#0(),@y) -> c_60() #natmult#(#s(@x),@y) -> c_61(#add#(#pos(@y),#natmult(@x,@y)),#natmult#(@x,@y)) #natsub#(@x,#0()) -> c_62() #natsub#(#s(@x),#s(@y)) -> c_63(#natsub#(@x,@y)) #pred#(#0()) -> c_64() #pred#(#neg(#s(@x))) -> c_65() #pred#(#pos(#s(#0()))) -> c_66() #pred#(#pos(#s(#s(@x)))) -> c_67() #sub#(@x,#0()) -> c_68() #sub#(@x,#neg(@y)) -> c_69(#add#(@x,#pos(@y))) #sub#(@x,#pos(@y)) -> c_70(#add#(@x,#neg(@y))) #succ#(#0()) -> c_71() #succ#(#neg(#s(#0()))) -> c_72() #succ#(#neg(#s(#s(@x)))) -> c_73() #succ#(#pos(#s(@x))) -> c_74() *#(@x,@y) -> c_2(#mult#(@x,@y)) -#(@x,@y) -> c_3(#sub#(@x,@y)) div#(@x,@y) -> c_4(#div#(@x,@y)) eratos#1#(nil()) -> c_7() filter#1#(nil(),@p) -> c_10() filter#3#(#false(),@x,@xs') -> c_12() filter#3#(#true(),@x,@xs') -> c_13() mod#(@x,@y) -> c_14(-#(@x,*(@x,div(@x,@y))),*#(@x,div(@x,@y)),div#(@x,@y)) - Weak TRS: #add(#0(),@y) -> @y #add(#neg(#s(#0())),@y) -> #pred(@y) #add(#neg(#s(#s(@x))),@y) -> #pred(#add(#pos(#s(@x)),@y)) #add(#pos(#s(#0())),@y) -> #succ(@y) #add(#pos(#s(#s(@x))),@y) -> #succ(#add(#pos(#s(@x)),@y)) #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #div(#0(),#0()) -> #divByZero() #div(#0(),#neg(@y)) -> #0() #div(#0(),#pos(@y)) -> #0() #div(#neg(@x),#0()) -> #divByZero() #div(#neg(@x),#neg(@y)) -> #pos(#natdiv(@x,@y)) #div(#neg(@x),#pos(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#0()) -> #divByZero() #div(#pos(@x),#neg(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#pos(@y)) -> #pos(#natdiv(@x,@y)) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #mult(#0(),#0()) -> #0() #mult(#0(),#neg(@y)) -> #0() #mult(#0(),#pos(@y)) -> #0() #mult(#neg(@x),#0()) -> #0() #mult(#neg(@x),#neg(@y)) -> #pos(#natmult(@x,@y)) #mult(#neg(@x),#pos(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#0()) -> #0() #mult(#pos(@x),#neg(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#pos(@y)) -> #pos(#natmult(@x,@y)) #natdiv(#0(),#0()) -> #divByZero() #natdiv(#s(@x),#s(@y)) -> #s(#natdiv(#natsub(@x,@y),#s(@y))) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@y),#natmult(@x,@y)) #natsub(@x,#0()) -> @x #natsub(#s(@x),#s(@y)) -> #natsub(@x,@y) #pred(#0()) -> #neg(#s(#0())) #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) #pred(#pos(#s(#0()))) -> #0() #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) #sub(@x,#0()) -> @x #sub(@x,#neg(@y)) -> #add(@x,#pos(@y)) #sub(@x,#pos(@y)) -> #add(@x,#neg(@y)) #succ(#0()) -> #pos(#s(#0())) #succ(#neg(#s(#0()))) -> #0() #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) *(@x,@y) -> #mult(@x,@y) -(@x,@y) -> #sub(@x,@y) div(@x,@y) -> #div(@x,@y) filter(@p,@l) -> filter#1(@l,@p) filter#1(::(@x,@xs),@p) -> filter#2(filter(@p,@xs),@p,@x) filter#1(nil(),@p) -> nil() filter#2(@xs',@p,@x) -> filter#3(#equal(mod(@x,@p),#0()),@x,@xs') filter#3(#false(),@x,@xs') -> ::(@x,@xs') filter#3(#true(),@x,@xs') -> @xs' mod(@x,@y) -> -(@x,*(@x,div(@x,@y))) - Signature: {#add/2,#and/2,#div/2,#eq/2,#equal/2,#mult/2,#natdiv/2,#natmult/2,#natsub/2,#pred/1,#sub/2,#succ/1,*/2,-/2 ,div/2,eratos/1,eratos#1/1,filter/2,filter#1/2,filter#2/3,filter#3/3,mod/2,#add#/2,#and#/2,#div#/2,#eq#/2 ,#equal#/2,#mult#/2,#natdiv#/2,#natmult#/2,#natsub#/2,#pred#/1,#sub#/2,#succ#/1,*#/2,-#/2,div#/2,eratos#/1 ,eratos#1#/1,filter#/2,filter#1#/2,filter#2#/3,filter#3#/3,mod#/2} / {#0/0,#divByZero/0,#false/0,#neg/1 ,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/2,c_7/0,c_8/1,c_9/2,c_10/0,c_11/3,c_12/0 ,c_13/0,c_14/3,c_15/0,c_16/1,c_17/2,c_18/1,c_19/2,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0 ,c_28/1,c_29/1,c_30/0,c_31/1,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/1,c_39/0,c_40/0,c_41/0,c_42/1 ,c_43/0,c_44/1,c_45/3,c_46/0,c_47/0,c_48/0,c_49/0,c_50/0,c_51/0,c_52/0,c_53/1,c_54/1,c_55/0,c_56/1,c_57/1 ,c_58/0,c_59/2,c_60/0,c_61/2,c_62/0,c_63/1,c_64/0,c_65/0,c_66/0,c_67/0,c_68/0,c_69/1,c_70/1,c_71/0,c_72/0 ,c_73/0,c_74/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult# ,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3# ,mod#} and constructors {#0,#divByZero,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {5} by application of Pre({5}) = {4}. Here rules are labelled as follows: 1: eratos#(@l) -> c_5(eratos#1#(@l)) 2: eratos#1#(::(@x,@xs)) -> c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)) 3: filter#(@p,@l) -> c_8(filter#1#(@l,@p)) 4: filter#1#(::(@x,@xs),@p) -> c_9(filter#2#(filter(@p,@xs),@p,@x),filter#(@p,@xs)) 5: filter#2#(@xs',@p,@x) -> c_11(filter#3#(#equal(mod(@x,@p),#0()),@x,@xs') ,#equal#(mod(@x,@p),#0()) ,mod#(@x,@p)) 6: #add#(#0(),@y) -> c_15() 7: #add#(#neg(#s(#0())),@y) -> c_16(#pred#(@y)) 8: #add#(#neg(#s(#s(@x))),@y) -> c_17(#pred#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) 9: #add#(#pos(#s(#0())),@y) -> c_18(#succ#(@y)) 10: #add#(#pos(#s(#s(@x))),@y) -> c_19(#succ#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) 11: #and#(#false(),#false()) -> c_20() 12: #and#(#false(),#true()) -> c_21() 13: #and#(#true(),#false()) -> c_22() 14: #and#(#true(),#true()) -> c_23() 15: #div#(#0(),#0()) -> c_24() 16: #div#(#0(),#neg(@y)) -> c_25() 17: #div#(#0(),#pos(@y)) -> c_26() 18: #div#(#neg(@x),#0()) -> c_27() 19: #div#(#neg(@x),#neg(@y)) -> c_28(#natdiv#(@x,@y)) 20: #div#(#neg(@x),#pos(@y)) -> c_29(#natdiv#(@x,@y)) 21: #div#(#pos(@x),#0()) -> c_30() 22: #div#(#pos(@x),#neg(@y)) -> c_31(#natdiv#(@x,@y)) 23: #div#(#pos(@x),#pos(@y)) -> c_32(#natdiv#(@x,@y)) 24: #eq#(#0(),#0()) -> c_33() 25: #eq#(#0(),#neg(@y)) -> c_34() 26: #eq#(#0(),#pos(@y)) -> c_35() 27: #eq#(#0(),#s(@y)) -> c_36() 28: #eq#(#neg(@x),#0()) -> c_37() 29: #eq#(#neg(@x),#neg(@y)) -> c_38(#eq#(@x,@y)) 30: #eq#(#neg(@x),#pos(@y)) -> c_39() 31: #eq#(#pos(@x),#0()) -> c_40() 32: #eq#(#pos(@x),#neg(@y)) -> c_41() 33: #eq#(#pos(@x),#pos(@y)) -> c_42(#eq#(@x,@y)) 34: #eq#(#s(@x),#0()) -> c_43() 35: #eq#(#s(@x),#s(@y)) -> c_44(#eq#(@x,@y)) 36: #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_45(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)) 37: #eq#(::(@x_1,@x_2),nil()) -> c_46() 38: #eq#(nil(),::(@y_1,@y_2)) -> c_47() 39: #eq#(nil(),nil()) -> c_48() 40: #equal#(@x,@y) -> c_1(#eq#(@x,@y)) 41: #mult#(#0(),#0()) -> c_49() 42: #mult#(#0(),#neg(@y)) -> c_50() 43: #mult#(#0(),#pos(@y)) -> c_51() 44: #mult#(#neg(@x),#0()) -> c_52() 45: #mult#(#neg(@x),#neg(@y)) -> c_53(#natmult#(@x,@y)) 46: #mult#(#neg(@x),#pos(@y)) -> c_54(#natmult#(@x,@y)) 47: #mult#(#pos(@x),#0()) -> c_55() 48: #mult#(#pos(@x),#neg(@y)) -> c_56(#natmult#(@x,@y)) 49: #mult#(#pos(@x),#pos(@y)) -> c_57(#natmult#(@x,@y)) 50: #natdiv#(#0(),#0()) -> c_58() 51: #natdiv#(#s(@x),#s(@y)) -> c_59(#natdiv#(#natsub(@x,@y),#s(@y)),#natsub#(@x,@y)) 52: #natmult#(#0(),@y) -> c_60() 53: #natmult#(#s(@x),@y) -> c_61(#add#(#pos(@y),#natmult(@x,@y)),#natmult#(@x,@y)) 54: #natsub#(@x,#0()) -> c_62() 55: #natsub#(#s(@x),#s(@y)) -> c_63(#natsub#(@x,@y)) 56: #pred#(#0()) -> c_64() 57: #pred#(#neg(#s(@x))) -> c_65() 58: #pred#(#pos(#s(#0()))) -> c_66() 59: #pred#(#pos(#s(#s(@x)))) -> c_67() 60: #sub#(@x,#0()) -> c_68() 61: #sub#(@x,#neg(@y)) -> c_69(#add#(@x,#pos(@y))) 62: #sub#(@x,#pos(@y)) -> c_70(#add#(@x,#neg(@y))) 63: #succ#(#0()) -> c_71() 64: #succ#(#neg(#s(#0()))) -> c_72() 65: #succ#(#neg(#s(#s(@x)))) -> c_73() 66: #succ#(#pos(#s(@x))) -> c_74() 67: *#(@x,@y) -> c_2(#mult#(@x,@y)) 68: -#(@x,@y) -> c_3(#sub#(@x,@y)) 69: div#(@x,@y) -> c_4(#div#(@x,@y)) 70: eratos#1#(nil()) -> c_7() 71: filter#1#(nil(),@p) -> c_10() 72: filter#3#(#false(),@x,@xs') -> c_12() 73: filter#3#(#true(),@x,@xs') -> c_13() 74: mod#(@x,@y) -> c_14(-#(@x,*(@x,div(@x,@y))),*#(@x,div(@x,@y)),div#(@x,@y)) * Step 6: RemoveWeakSuffixes WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: eratos#(@l) -> c_5(eratos#1#(@l)) eratos#1#(::(@x,@xs)) -> c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)) filter#(@p,@l) -> c_8(filter#1#(@l,@p)) filter#1#(::(@x,@xs),@p) -> c_9(filter#2#(filter(@p,@xs),@p,@x),filter#(@p,@xs)) - Weak DPs: #add#(#0(),@y) -> c_15() #add#(#neg(#s(#0())),@y) -> c_16(#pred#(@y)) #add#(#neg(#s(#s(@x))),@y) -> c_17(#pred#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) #add#(#pos(#s(#0())),@y) -> c_18(#succ#(@y)) #add#(#pos(#s(#s(@x))),@y) -> c_19(#succ#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) #and#(#false(),#false()) -> c_20() #and#(#false(),#true()) -> c_21() #and#(#true(),#false()) -> c_22() #and#(#true(),#true()) -> c_23() #div#(#0(),#0()) -> c_24() #div#(#0(),#neg(@y)) -> c_25() #div#(#0(),#pos(@y)) -> c_26() #div#(#neg(@x),#0()) -> c_27() #div#(#neg(@x),#neg(@y)) -> c_28(#natdiv#(@x,@y)) #div#(#neg(@x),#pos(@y)) -> c_29(#natdiv#(@x,@y)) #div#(#pos(@x),#0()) -> c_30() #div#(#pos(@x),#neg(@y)) -> c_31(#natdiv#(@x,@y)) #div#(#pos(@x),#pos(@y)) -> c_32(#natdiv#(@x,@y)) #eq#(#0(),#0()) -> c_33() #eq#(#0(),#neg(@y)) -> c_34() #eq#(#0(),#pos(@y)) -> c_35() #eq#(#0(),#s(@y)) -> c_36() #eq#(#neg(@x),#0()) -> c_37() #eq#(#neg(@x),#neg(@y)) -> c_38(#eq#(@x,@y)) #eq#(#neg(@x),#pos(@y)) -> c_39() #eq#(#pos(@x),#0()) -> c_40() #eq#(#pos(@x),#neg(@y)) -> c_41() #eq#(#pos(@x),#pos(@y)) -> c_42(#eq#(@x,@y)) #eq#(#s(@x),#0()) -> c_43() #eq#(#s(@x),#s(@y)) -> c_44(#eq#(@x,@y)) #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_45(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)) #eq#(::(@x_1,@x_2),nil()) -> c_46() #eq#(nil(),::(@y_1,@y_2)) -> c_47() #eq#(nil(),nil()) -> c_48() #equal#(@x,@y) -> c_1(#eq#(@x,@y)) #mult#(#0(),#0()) -> c_49() #mult#(#0(),#neg(@y)) -> c_50() #mult#(#0(),#pos(@y)) -> c_51() #mult#(#neg(@x),#0()) -> c_52() #mult#(#neg(@x),#neg(@y)) -> c_53(#natmult#(@x,@y)) #mult#(#neg(@x),#pos(@y)) -> c_54(#natmult#(@x,@y)) #mult#(#pos(@x),#0()) -> c_55() #mult#(#pos(@x),#neg(@y)) -> c_56(#natmult#(@x,@y)) #mult#(#pos(@x),#pos(@y)) -> c_57(#natmult#(@x,@y)) #natdiv#(#0(),#0()) -> c_58() #natdiv#(#s(@x),#s(@y)) -> c_59(#natdiv#(#natsub(@x,@y),#s(@y)),#natsub#(@x,@y)) #natmult#(#0(),@y) -> c_60() #natmult#(#s(@x),@y) -> c_61(#add#(#pos(@y),#natmult(@x,@y)),#natmult#(@x,@y)) #natsub#(@x,#0()) -> c_62() #natsub#(#s(@x),#s(@y)) -> c_63(#natsub#(@x,@y)) #pred#(#0()) -> c_64() #pred#(#neg(#s(@x))) -> c_65() #pred#(#pos(#s(#0()))) -> c_66() #pred#(#pos(#s(#s(@x)))) -> c_67() #sub#(@x,#0()) -> c_68() #sub#(@x,#neg(@y)) -> c_69(#add#(@x,#pos(@y))) #sub#(@x,#pos(@y)) -> c_70(#add#(@x,#neg(@y))) #succ#(#0()) -> c_71() #succ#(#neg(#s(#0()))) -> c_72() #succ#(#neg(#s(#s(@x)))) -> c_73() #succ#(#pos(#s(@x))) -> c_74() *#(@x,@y) -> c_2(#mult#(@x,@y)) -#(@x,@y) -> c_3(#sub#(@x,@y)) div#(@x,@y) -> c_4(#div#(@x,@y)) eratos#1#(nil()) -> c_7() filter#1#(nil(),@p) -> c_10() filter#2#(@xs',@p,@x) -> c_11(filter#3#(#equal(mod(@x,@p),#0()),@x,@xs') ,#equal#(mod(@x,@p),#0()) ,mod#(@x,@p)) filter#3#(#false(),@x,@xs') -> c_12() filter#3#(#true(),@x,@xs') -> c_13() mod#(@x,@y) -> c_14(-#(@x,*(@x,div(@x,@y))),*#(@x,div(@x,@y)),div#(@x,@y)) - Weak TRS: #add(#0(),@y) -> @y #add(#neg(#s(#0())),@y) -> #pred(@y) #add(#neg(#s(#s(@x))),@y) -> #pred(#add(#pos(#s(@x)),@y)) #add(#pos(#s(#0())),@y) -> #succ(@y) #add(#pos(#s(#s(@x))),@y) -> #succ(#add(#pos(#s(@x)),@y)) #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #div(#0(),#0()) -> #divByZero() #div(#0(),#neg(@y)) -> #0() #div(#0(),#pos(@y)) -> #0() #div(#neg(@x),#0()) -> #divByZero() #div(#neg(@x),#neg(@y)) -> #pos(#natdiv(@x,@y)) #div(#neg(@x),#pos(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#0()) -> #divByZero() #div(#pos(@x),#neg(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#pos(@y)) -> #pos(#natdiv(@x,@y)) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #mult(#0(),#0()) -> #0() #mult(#0(),#neg(@y)) -> #0() #mult(#0(),#pos(@y)) -> #0() #mult(#neg(@x),#0()) -> #0() #mult(#neg(@x),#neg(@y)) -> #pos(#natmult(@x,@y)) #mult(#neg(@x),#pos(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#0()) -> #0() #mult(#pos(@x),#neg(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#pos(@y)) -> #pos(#natmult(@x,@y)) #natdiv(#0(),#0()) -> #divByZero() #natdiv(#s(@x),#s(@y)) -> #s(#natdiv(#natsub(@x,@y),#s(@y))) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@y),#natmult(@x,@y)) #natsub(@x,#0()) -> @x #natsub(#s(@x),#s(@y)) -> #natsub(@x,@y) #pred(#0()) -> #neg(#s(#0())) #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) #pred(#pos(#s(#0()))) -> #0() #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) #sub(@x,#0()) -> @x #sub(@x,#neg(@y)) -> #add(@x,#pos(@y)) #sub(@x,#pos(@y)) -> #add(@x,#neg(@y)) #succ(#0()) -> #pos(#s(#0())) #succ(#neg(#s(#0()))) -> #0() #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) *(@x,@y) -> #mult(@x,@y) -(@x,@y) -> #sub(@x,@y) div(@x,@y) -> #div(@x,@y) filter(@p,@l) -> filter#1(@l,@p) filter#1(::(@x,@xs),@p) -> filter#2(filter(@p,@xs),@p,@x) filter#1(nil(),@p) -> nil() filter#2(@xs',@p,@x) -> filter#3(#equal(mod(@x,@p),#0()),@x,@xs') filter#3(#false(),@x,@xs') -> ::(@x,@xs') filter#3(#true(),@x,@xs') -> @xs' mod(@x,@y) -> -(@x,*(@x,div(@x,@y))) - Signature: {#add/2,#and/2,#div/2,#eq/2,#equal/2,#mult/2,#natdiv/2,#natmult/2,#natsub/2,#pred/1,#sub/2,#succ/1,*/2,-/2 ,div/2,eratos/1,eratos#1/1,filter/2,filter#1/2,filter#2/3,filter#3/3,mod/2,#add#/2,#and#/2,#div#/2,#eq#/2 ,#equal#/2,#mult#/2,#natdiv#/2,#natmult#/2,#natsub#/2,#pred#/1,#sub#/2,#succ#/1,*#/2,-#/2,div#/2,eratos#/1 ,eratos#1#/1,filter#/2,filter#1#/2,filter#2#/3,filter#3#/3,mod#/2} / {#0/0,#divByZero/0,#false/0,#neg/1 ,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/2,c_7/0,c_8/1,c_9/2,c_10/0,c_11/3,c_12/0 ,c_13/0,c_14/3,c_15/0,c_16/1,c_17/2,c_18/1,c_19/2,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0 ,c_28/1,c_29/1,c_30/0,c_31/1,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/1,c_39/0,c_40/0,c_41/0,c_42/1 ,c_43/0,c_44/1,c_45/3,c_46/0,c_47/0,c_48/0,c_49/0,c_50/0,c_51/0,c_52/0,c_53/1,c_54/1,c_55/0,c_56/1,c_57/1 ,c_58/0,c_59/2,c_60/0,c_61/2,c_62/0,c_63/1,c_64/0,c_65/0,c_66/0,c_67/0,c_68/0,c_69/1,c_70/1,c_71/0,c_72/0 ,c_73/0,c_74/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult# ,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3# ,mod#} and constructors {#0,#divByZero,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:eratos#(@l) -> c_5(eratos#1#(@l)) -->_1 eratos#1#(::(@x,@xs)) -> c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)):2 -->_1 eratos#1#(nil()) -> c_7():69 2:S:eratos#1#(::(@x,@xs)) -> c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)) -->_2 filter#(@p,@l) -> c_8(filter#1#(@l,@p)):3 -->_1 eratos#(@l) -> c_5(eratos#1#(@l)):1 3:S:filter#(@p,@l) -> c_8(filter#1#(@l,@p)) -->_1 filter#1#(::(@x,@xs),@p) -> c_9(filter#2#(filter(@p,@xs),@p,@x),filter#(@p,@xs)):4 -->_1 filter#1#(nil(),@p) -> c_10():70 4:S:filter#1#(::(@x,@xs),@p) -> c_9(filter#2#(filter(@p,@xs),@p,@x),filter#(@p,@xs)) -->_1 filter#2#(@xs',@p,@x) -> c_11(filter#3#(#equal(mod(@x,@p),#0()),@x,@xs') ,#equal#(mod(@x,@p),#0()) ,mod#(@x,@p)):71 -->_2 filter#(@p,@l) -> c_8(filter#1#(@l,@p)):3 5:W:#add#(#0(),@y) -> c_15() 6:W:#add#(#neg(#s(#0())),@y) -> c_16(#pred#(@y)) -->_1 #pred#(#pos(#s(#s(@x)))) -> c_67():58 -->_1 #pred#(#pos(#s(#0()))) -> c_66():57 -->_1 #pred#(#neg(#s(@x))) -> c_65():56 -->_1 #pred#(#0()) -> c_64():55 7:W:#add#(#neg(#s(#s(@x))),@y) -> c_17(#pred#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) -->_2 #add#(#pos(#s(#s(@x))),@y) -> c_19(#succ#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)):9 -->_2 #add#(#pos(#s(#0())),@y) -> c_18(#succ#(@y)):8 -->_1 #pred#(#pos(#s(#s(@x)))) -> c_67():58 -->_1 #pred#(#pos(#s(#0()))) -> c_66():57 -->_1 #pred#(#neg(#s(@x))) -> c_65():56 -->_1 #pred#(#0()) -> c_64():55 8:W:#add#(#pos(#s(#0())),@y) -> c_18(#succ#(@y)) -->_1 #succ#(#pos(#s(@x))) -> c_74():65 -->_1 #succ#(#neg(#s(#s(@x)))) -> c_73():64 -->_1 #succ#(#neg(#s(#0()))) -> c_72():63 -->_1 #succ#(#0()) -> c_71():62 9:W:#add#(#pos(#s(#s(@x))),@y) -> c_19(#succ#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) -->_1 #succ#(#pos(#s(@x))) -> c_74():65 -->_1 #succ#(#neg(#s(#s(@x)))) -> c_73():64 -->_1 #succ#(#neg(#s(#0()))) -> c_72():63 -->_1 #succ#(#0()) -> c_71():62 -->_2 #add#(#pos(#s(#s(@x))),@y) -> c_19(#succ#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)):9 -->_2 #add#(#pos(#s(#0())),@y) -> c_18(#succ#(@y)):8 10:W:#and#(#false(),#false()) -> c_20() 11:W:#and#(#false(),#true()) -> c_21() 12:W:#and#(#true(),#false()) -> c_22() 13:W:#and#(#true(),#true()) -> c_23() 14:W:#div#(#0(),#0()) -> c_24() 15:W:#div#(#0(),#neg(@y)) -> c_25() 16:W:#div#(#0(),#pos(@y)) -> c_26() 17:W:#div#(#neg(@x),#0()) -> c_27() 18:W:#div#(#neg(@x),#neg(@y)) -> c_28(#natdiv#(@x,@y)) -->_1 #natdiv#(#s(@x),#s(@y)) -> c_59(#natdiv#(#natsub(@x,@y),#s(@y)),#natsub#(@x,@y)):50 -->_1 #natdiv#(#0(),#0()) -> c_58():49 19:W:#div#(#neg(@x),#pos(@y)) -> c_29(#natdiv#(@x,@y)) -->_1 #natdiv#(#s(@x),#s(@y)) -> c_59(#natdiv#(#natsub(@x,@y),#s(@y)),#natsub#(@x,@y)):50 -->_1 #natdiv#(#0(),#0()) -> c_58():49 20:W:#div#(#pos(@x),#0()) -> c_30() 21:W:#div#(#pos(@x),#neg(@y)) -> c_31(#natdiv#(@x,@y)) -->_1 #natdiv#(#s(@x),#s(@y)) -> c_59(#natdiv#(#natsub(@x,@y),#s(@y)),#natsub#(@x,@y)):50 -->_1 #natdiv#(#0(),#0()) -> c_58():49 22:W:#div#(#pos(@x),#pos(@y)) -> c_32(#natdiv#(@x,@y)) -->_1 #natdiv#(#s(@x),#s(@y)) -> c_59(#natdiv#(#natsub(@x,@y),#s(@y)),#natsub#(@x,@y)):50 -->_1 #natdiv#(#0(),#0()) -> c_58():49 23:W:#eq#(#0(),#0()) -> c_33() 24:W:#eq#(#0(),#neg(@y)) -> c_34() 25:W:#eq#(#0(),#pos(@y)) -> c_35() 26:W:#eq#(#0(),#s(@y)) -> c_36() 27:W:#eq#(#neg(@x),#0()) -> c_37() 28:W:#eq#(#neg(@x),#neg(@y)) -> c_38(#eq#(@x,@y)) -->_1 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_45(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)):35 -->_1 #eq#(#s(@x),#s(@y)) -> c_44(#eq#(@x,@y)):34 -->_1 #eq#(#pos(@x),#pos(@y)) -> c_42(#eq#(@x,@y)):32 -->_1 #eq#(nil(),nil()) -> c_48():38 -->_1 #eq#(nil(),::(@y_1,@y_2)) -> c_47():37 -->_1 #eq#(::(@x_1,@x_2),nil()) -> c_46():36 -->_1 #eq#(#s(@x),#0()) -> c_43():33 -->_1 #eq#(#pos(@x),#neg(@y)) -> c_41():31 -->_1 #eq#(#pos(@x),#0()) -> c_40():30 -->_1 #eq#(#neg(@x),#pos(@y)) -> c_39():29 -->_1 #eq#(#neg(@x),#neg(@y)) -> c_38(#eq#(@x,@y)):28 -->_1 #eq#(#neg(@x),#0()) -> c_37():27 -->_1 #eq#(#0(),#s(@y)) -> c_36():26 -->_1 #eq#(#0(),#pos(@y)) -> c_35():25 -->_1 #eq#(#0(),#neg(@y)) -> c_34():24 -->_1 #eq#(#0(),#0()) -> c_33():23 29:W:#eq#(#neg(@x),#pos(@y)) -> c_39() 30:W:#eq#(#pos(@x),#0()) -> c_40() 31:W:#eq#(#pos(@x),#neg(@y)) -> c_41() 32:W:#eq#(#pos(@x),#pos(@y)) -> c_42(#eq#(@x,@y)) -->_1 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_45(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)):35 -->_1 #eq#(#s(@x),#s(@y)) -> c_44(#eq#(@x,@y)):34 -->_1 #eq#(nil(),nil()) -> c_48():38 -->_1 #eq#(nil(),::(@y_1,@y_2)) -> c_47():37 -->_1 #eq#(::(@x_1,@x_2),nil()) -> c_46():36 -->_1 #eq#(#s(@x),#0()) -> c_43():33 -->_1 #eq#(#pos(@x),#pos(@y)) -> c_42(#eq#(@x,@y)):32 -->_1 #eq#(#pos(@x),#neg(@y)) -> c_41():31 -->_1 #eq#(#pos(@x),#0()) -> c_40():30 -->_1 #eq#(#neg(@x),#pos(@y)) -> c_39():29 -->_1 #eq#(#neg(@x),#neg(@y)) -> c_38(#eq#(@x,@y)):28 -->_1 #eq#(#neg(@x),#0()) -> c_37():27 -->_1 #eq#(#0(),#s(@y)) -> c_36():26 -->_1 #eq#(#0(),#pos(@y)) -> c_35():25 -->_1 #eq#(#0(),#neg(@y)) -> c_34():24 -->_1 #eq#(#0(),#0()) -> c_33():23 33:W:#eq#(#s(@x),#0()) -> c_43() 34:W:#eq#(#s(@x),#s(@y)) -> c_44(#eq#(@x,@y)) -->_1 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_45(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)):35 -->_1 #eq#(nil(),nil()) -> c_48():38 -->_1 #eq#(nil(),::(@y_1,@y_2)) -> c_47():37 -->_1 #eq#(::(@x_1,@x_2),nil()) -> c_46():36 -->_1 #eq#(#s(@x),#s(@y)) -> c_44(#eq#(@x,@y)):34 -->_1 #eq#(#s(@x),#0()) -> c_43():33 -->_1 #eq#(#pos(@x),#pos(@y)) -> c_42(#eq#(@x,@y)):32 -->_1 #eq#(#pos(@x),#neg(@y)) -> c_41():31 -->_1 #eq#(#pos(@x),#0()) -> c_40():30 -->_1 #eq#(#neg(@x),#pos(@y)) -> c_39():29 -->_1 #eq#(#neg(@x),#neg(@y)) -> c_38(#eq#(@x,@y)):28 -->_1 #eq#(#neg(@x),#0()) -> c_37():27 -->_1 #eq#(#0(),#s(@y)) -> c_36():26 -->_1 #eq#(#0(),#pos(@y)) -> c_35():25 -->_1 #eq#(#0(),#neg(@y)) -> c_34():24 -->_1 #eq#(#0(),#0()) -> c_33():23 35:W:#eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_45(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)) -->_3 #eq#(nil(),nil()) -> c_48():38 -->_2 #eq#(nil(),nil()) -> c_48():38 -->_3 #eq#(nil(),::(@y_1,@y_2)) -> c_47():37 -->_2 #eq#(nil(),::(@y_1,@y_2)) -> c_47():37 -->_3 #eq#(::(@x_1,@x_2),nil()) -> c_46():36 -->_2 #eq#(::(@x_1,@x_2),nil()) -> c_46():36 -->_3 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_45(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)):35 -->_2 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_45(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)):35 -->_3 #eq#(#s(@x),#s(@y)) -> c_44(#eq#(@x,@y)):34 -->_2 #eq#(#s(@x),#s(@y)) -> c_44(#eq#(@x,@y)):34 -->_3 #eq#(#s(@x),#0()) -> c_43():33 -->_2 #eq#(#s(@x),#0()) -> c_43():33 -->_3 #eq#(#pos(@x),#pos(@y)) -> c_42(#eq#(@x,@y)):32 -->_2 #eq#(#pos(@x),#pos(@y)) -> c_42(#eq#(@x,@y)):32 -->_3 #eq#(#pos(@x),#neg(@y)) -> c_41():31 -->_2 #eq#(#pos(@x),#neg(@y)) -> c_41():31 -->_3 #eq#(#pos(@x),#0()) -> c_40():30 -->_2 #eq#(#pos(@x),#0()) -> c_40():30 -->_3 #eq#(#neg(@x),#pos(@y)) -> c_39():29 -->_2 #eq#(#neg(@x),#pos(@y)) -> c_39():29 -->_3 #eq#(#neg(@x),#neg(@y)) -> c_38(#eq#(@x,@y)):28 -->_2 #eq#(#neg(@x),#neg(@y)) -> c_38(#eq#(@x,@y)):28 -->_3 #eq#(#neg(@x),#0()) -> c_37():27 -->_2 #eq#(#neg(@x),#0()) -> c_37():27 -->_3 #eq#(#0(),#s(@y)) -> c_36():26 -->_2 #eq#(#0(),#s(@y)) -> c_36():26 -->_3 #eq#(#0(),#pos(@y)) -> c_35():25 -->_2 #eq#(#0(),#pos(@y)) -> c_35():25 -->_3 #eq#(#0(),#neg(@y)) -> c_34():24 -->_2 #eq#(#0(),#neg(@y)) -> c_34():24 -->_3 #eq#(#0(),#0()) -> c_33():23 -->_2 #eq#(#0(),#0()) -> c_33():23 -->_1 #and#(#true(),#true()) -> c_23():13 -->_1 #and#(#true(),#false()) -> c_22():12 -->_1 #and#(#false(),#true()) -> c_21():11 -->_1 #and#(#false(),#false()) -> c_20():10 36:W:#eq#(::(@x_1,@x_2),nil()) -> c_46() 37:W:#eq#(nil(),::(@y_1,@y_2)) -> c_47() 38:W:#eq#(nil(),nil()) -> c_48() 39:W:#equal#(@x,@y) -> c_1(#eq#(@x,@y)) -->_1 #eq#(nil(),nil()) -> c_48():38 -->_1 #eq#(nil(),::(@y_1,@y_2)) -> c_47():37 -->_1 #eq#(::(@x_1,@x_2),nil()) -> c_46():36 -->_1 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_45(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)):35 -->_1 #eq#(#s(@x),#s(@y)) -> c_44(#eq#(@x,@y)):34 -->_1 #eq#(#s(@x),#0()) -> c_43():33 -->_1 #eq#(#pos(@x),#pos(@y)) -> c_42(#eq#(@x,@y)):32 -->_1 #eq#(#pos(@x),#neg(@y)) -> c_41():31 -->_1 #eq#(#pos(@x),#0()) -> c_40():30 -->_1 #eq#(#neg(@x),#pos(@y)) -> c_39():29 -->_1 #eq#(#neg(@x),#neg(@y)) -> c_38(#eq#(@x,@y)):28 -->_1 #eq#(#neg(@x),#0()) -> c_37():27 -->_1 #eq#(#0(),#s(@y)) -> c_36():26 -->_1 #eq#(#0(),#pos(@y)) -> c_35():25 -->_1 #eq#(#0(),#neg(@y)) -> c_34():24 -->_1 #eq#(#0(),#0()) -> c_33():23 40:W:#mult#(#0(),#0()) -> c_49() 41:W:#mult#(#0(),#neg(@y)) -> c_50() 42:W:#mult#(#0(),#pos(@y)) -> c_51() 43:W:#mult#(#neg(@x),#0()) -> c_52() 44:W:#mult#(#neg(@x),#neg(@y)) -> c_53(#natmult#(@x,@y)) -->_1 #natmult#(#s(@x),@y) -> c_61(#add#(#pos(@y),#natmult(@x,@y)),#natmult#(@x,@y)):52 -->_1 #natmult#(#0(),@y) -> c_60():51 45:W:#mult#(#neg(@x),#pos(@y)) -> c_54(#natmult#(@x,@y)) -->_1 #natmult#(#s(@x),@y) -> c_61(#add#(#pos(@y),#natmult(@x,@y)),#natmult#(@x,@y)):52 -->_1 #natmult#(#0(),@y) -> c_60():51 46:W:#mult#(#pos(@x),#0()) -> c_55() 47:W:#mult#(#pos(@x),#neg(@y)) -> c_56(#natmult#(@x,@y)) -->_1 #natmult#(#s(@x),@y) -> c_61(#add#(#pos(@y),#natmult(@x,@y)),#natmult#(@x,@y)):52 -->_1 #natmult#(#0(),@y) -> c_60():51 48:W:#mult#(#pos(@x),#pos(@y)) -> c_57(#natmult#(@x,@y)) -->_1 #natmult#(#s(@x),@y) -> c_61(#add#(#pos(@y),#natmult(@x,@y)),#natmult#(@x,@y)):52 -->_1 #natmult#(#0(),@y) -> c_60():51 49:W:#natdiv#(#0(),#0()) -> c_58() 50:W:#natdiv#(#s(@x),#s(@y)) -> c_59(#natdiv#(#natsub(@x,@y),#s(@y)),#natsub#(@x,@y)) -->_2 #natsub#(#s(@x),#s(@y)) -> c_63(#natsub#(@x,@y)):54 -->_2 #natsub#(@x,#0()) -> c_62():53 -->_1 #natdiv#(#s(@x),#s(@y)) -> c_59(#natdiv#(#natsub(@x,@y),#s(@y)),#natsub#(@x,@y)):50 51:W:#natmult#(#0(),@y) -> c_60() 52:W:#natmult#(#s(@x),@y) -> c_61(#add#(#pos(@y),#natmult(@x,@y)),#natmult#(@x,@y)) -->_2 #natmult#(#s(@x),@y) -> c_61(#add#(#pos(@y),#natmult(@x,@y)),#natmult#(@x,@y)):52 -->_2 #natmult#(#0(),@y) -> c_60():51 -->_1 #add#(#pos(#s(#s(@x))),@y) -> c_19(#succ#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)):9 -->_1 #add#(#pos(#s(#0())),@y) -> c_18(#succ#(@y)):8 53:W:#natsub#(@x,#0()) -> c_62() 54:W:#natsub#(#s(@x),#s(@y)) -> c_63(#natsub#(@x,@y)) -->_1 #natsub#(#s(@x),#s(@y)) -> c_63(#natsub#(@x,@y)):54 -->_1 #natsub#(@x,#0()) -> c_62():53 55:W:#pred#(#0()) -> c_64() 56:W:#pred#(#neg(#s(@x))) -> c_65() 57:W:#pred#(#pos(#s(#0()))) -> c_66() 58:W:#pred#(#pos(#s(#s(@x)))) -> c_67() 59:W:#sub#(@x,#0()) -> c_68() 60:W:#sub#(@x,#neg(@y)) -> c_69(#add#(@x,#pos(@y))) -->_1 #add#(#pos(#s(#s(@x))),@y) -> c_19(#succ#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)):9 -->_1 #add#(#pos(#s(#0())),@y) -> c_18(#succ#(@y)):8 -->_1 #add#(#neg(#s(#s(@x))),@y) -> c_17(#pred#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)):7 -->_1 #add#(#neg(#s(#0())),@y) -> c_16(#pred#(@y)):6 -->_1 #add#(#0(),@y) -> c_15():5 61:W:#sub#(@x,#pos(@y)) -> c_70(#add#(@x,#neg(@y))) -->_1 #add#(#pos(#s(#s(@x))),@y) -> c_19(#succ#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)):9 -->_1 #add#(#pos(#s(#0())),@y) -> c_18(#succ#(@y)):8 -->_1 #add#(#neg(#s(#s(@x))),@y) -> c_17(#pred#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)):7 -->_1 #add#(#neg(#s(#0())),@y) -> c_16(#pred#(@y)):6 -->_1 #add#(#0(),@y) -> c_15():5 62:W:#succ#(#0()) -> c_71() 63:W:#succ#(#neg(#s(#0()))) -> c_72() 64:W:#succ#(#neg(#s(#s(@x)))) -> c_73() 65:W:#succ#(#pos(#s(@x))) -> c_74() 66:W:*#(@x,@y) -> c_2(#mult#(@x,@y)) -->_1 #mult#(#pos(@x),#pos(@y)) -> c_57(#natmult#(@x,@y)):48 -->_1 #mult#(#pos(@x),#neg(@y)) -> c_56(#natmult#(@x,@y)):47 -->_1 #mult#(#pos(@x),#0()) -> c_55():46 -->_1 #mult#(#neg(@x),#pos(@y)) -> c_54(#natmult#(@x,@y)):45 -->_1 #mult#(#neg(@x),#neg(@y)) -> c_53(#natmult#(@x,@y)):44 -->_1 #mult#(#neg(@x),#0()) -> c_52():43 -->_1 #mult#(#0(),#pos(@y)) -> c_51():42 -->_1 #mult#(#0(),#neg(@y)) -> c_50():41 -->_1 #mult#(#0(),#0()) -> c_49():40 67:W:-#(@x,@y) -> c_3(#sub#(@x,@y)) -->_1 #sub#(@x,#pos(@y)) -> c_70(#add#(@x,#neg(@y))):61 -->_1 #sub#(@x,#neg(@y)) -> c_69(#add#(@x,#pos(@y))):60 -->_1 #sub#(@x,#0()) -> c_68():59 68:W:div#(@x,@y) -> c_4(#div#(@x,@y)) -->_1 #div#(#pos(@x),#pos(@y)) -> c_32(#natdiv#(@x,@y)):22 -->_1 #div#(#pos(@x),#neg(@y)) -> c_31(#natdiv#(@x,@y)):21 -->_1 #div#(#pos(@x),#0()) -> c_30():20 -->_1 #div#(#neg(@x),#pos(@y)) -> c_29(#natdiv#(@x,@y)):19 -->_1 #div#(#neg(@x),#neg(@y)) -> c_28(#natdiv#(@x,@y)):18 -->_1 #div#(#neg(@x),#0()) -> c_27():17 -->_1 #div#(#0(),#pos(@y)) -> c_26():16 -->_1 #div#(#0(),#neg(@y)) -> c_25():15 -->_1 #div#(#0(),#0()) -> c_24():14 69:W:eratos#1#(nil()) -> c_7() 70:W:filter#1#(nil(),@p) -> c_10() 71:W:filter#2#(@xs',@p,@x) -> c_11(filter#3#(#equal(mod(@x,@p),#0()),@x,@xs') ,#equal#(mod(@x,@p),#0()) ,mod#(@x,@p)) -->_3 mod#(@x,@y) -> c_14(-#(@x,*(@x,div(@x,@y))),*#(@x,div(@x,@y)),div#(@x,@y)):74 -->_1 filter#3#(#true(),@x,@xs') -> c_13():73 -->_1 filter#3#(#false(),@x,@xs') -> c_12():72 -->_2 #equal#(@x,@y) -> c_1(#eq#(@x,@y)):39 72:W:filter#3#(#false(),@x,@xs') -> c_12() 73:W:filter#3#(#true(),@x,@xs') -> c_13() 74:W:mod#(@x,@y) -> c_14(-#(@x,*(@x,div(@x,@y))),*#(@x,div(@x,@y)),div#(@x,@y)) -->_3 div#(@x,@y) -> c_4(#div#(@x,@y)):68 -->_1 -#(@x,@y) -> c_3(#sub#(@x,@y)):67 -->_2 *#(@x,@y) -> c_2(#mult#(@x,@y)):66 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 69: eratos#1#(nil()) -> c_7() 70: filter#1#(nil(),@p) -> c_10() 71: filter#2#(@xs',@p,@x) -> c_11(filter#3#(#equal(mod(@x,@p),#0()),@x,@xs') ,#equal#(mod(@x,@p),#0()) ,mod#(@x,@p)) 39: #equal#(@x,@y) -> c_1(#eq#(@x,@y)) 35: #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_45(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)) 34: #eq#(#s(@x),#s(@y)) -> c_44(#eq#(@x,@y)) 32: #eq#(#pos(@x),#pos(@y)) -> c_42(#eq#(@x,@y)) 28: #eq#(#neg(@x),#neg(@y)) -> c_38(#eq#(@x,@y)) 10: #and#(#false(),#false()) -> c_20() 11: #and#(#false(),#true()) -> c_21() 12: #and#(#true(),#false()) -> c_22() 13: #and#(#true(),#true()) -> c_23() 23: #eq#(#0(),#0()) -> c_33() 24: #eq#(#0(),#neg(@y)) -> c_34() 25: #eq#(#0(),#pos(@y)) -> c_35() 26: #eq#(#0(),#s(@y)) -> c_36() 27: #eq#(#neg(@x),#0()) -> c_37() 29: #eq#(#neg(@x),#pos(@y)) -> c_39() 30: #eq#(#pos(@x),#0()) -> c_40() 31: #eq#(#pos(@x),#neg(@y)) -> c_41() 33: #eq#(#s(@x),#0()) -> c_43() 36: #eq#(::(@x_1,@x_2),nil()) -> c_46() 37: #eq#(nil(),::(@y_1,@y_2)) -> c_47() 38: #eq#(nil(),nil()) -> c_48() 72: filter#3#(#false(),@x,@xs') -> c_12() 73: filter#3#(#true(),@x,@xs') -> c_13() 74: mod#(@x,@y) -> c_14(-#(@x,*(@x,div(@x,@y))),*#(@x,div(@x,@y)),div#(@x,@y)) 66: *#(@x,@y) -> c_2(#mult#(@x,@y)) 40: #mult#(#0(),#0()) -> c_49() 41: #mult#(#0(),#neg(@y)) -> c_50() 42: #mult#(#0(),#pos(@y)) -> c_51() 43: #mult#(#neg(@x),#0()) -> c_52() 44: #mult#(#neg(@x),#neg(@y)) -> c_53(#natmult#(@x,@y)) 45: #mult#(#neg(@x),#pos(@y)) -> c_54(#natmult#(@x,@y)) 46: #mult#(#pos(@x),#0()) -> c_55() 47: #mult#(#pos(@x),#neg(@y)) -> c_56(#natmult#(@x,@y)) 48: #mult#(#pos(@x),#pos(@y)) -> c_57(#natmult#(@x,@y)) 52: #natmult#(#s(@x),@y) -> c_61(#add#(#pos(@y),#natmult(@x,@y)),#natmult#(@x,@y)) 51: #natmult#(#0(),@y) -> c_60() 67: -#(@x,@y) -> c_3(#sub#(@x,@y)) 59: #sub#(@x,#0()) -> c_68() 60: #sub#(@x,#neg(@y)) -> c_69(#add#(@x,#pos(@y))) 61: #sub#(@x,#pos(@y)) -> c_70(#add#(@x,#neg(@y))) 5: #add#(#0(),@y) -> c_15() 6: #add#(#neg(#s(#0())),@y) -> c_16(#pred#(@y)) 7: #add#(#neg(#s(#s(@x))),@y) -> c_17(#pred#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) 55: #pred#(#0()) -> c_64() 56: #pred#(#neg(#s(@x))) -> c_65() 57: #pred#(#pos(#s(#0()))) -> c_66() 58: #pred#(#pos(#s(#s(@x)))) -> c_67() 9: #add#(#pos(#s(#s(@x))),@y) -> c_19(#succ#(#add(#pos(#s(@x)),@y)),#add#(#pos(#s(@x)),@y)) 8: #add#(#pos(#s(#0())),@y) -> c_18(#succ#(@y)) 62: #succ#(#0()) -> c_71() 63: #succ#(#neg(#s(#0()))) -> c_72() 64: #succ#(#neg(#s(#s(@x)))) -> c_73() 65: #succ#(#pos(#s(@x))) -> c_74() 68: div#(@x,@y) -> c_4(#div#(@x,@y)) 14: #div#(#0(),#0()) -> c_24() 15: #div#(#0(),#neg(@y)) -> c_25() 16: #div#(#0(),#pos(@y)) -> c_26() 17: #div#(#neg(@x),#0()) -> c_27() 18: #div#(#neg(@x),#neg(@y)) -> c_28(#natdiv#(@x,@y)) 19: #div#(#neg(@x),#pos(@y)) -> c_29(#natdiv#(@x,@y)) 20: #div#(#pos(@x),#0()) -> c_30() 21: #div#(#pos(@x),#neg(@y)) -> c_31(#natdiv#(@x,@y)) 22: #div#(#pos(@x),#pos(@y)) -> c_32(#natdiv#(@x,@y)) 49: #natdiv#(#0(),#0()) -> c_58() 50: #natdiv#(#s(@x),#s(@y)) -> c_59(#natdiv#(#natsub(@x,@y),#s(@y)),#natsub#(@x,@y)) 54: #natsub#(#s(@x),#s(@y)) -> c_63(#natsub#(@x,@y)) 53: #natsub#(@x,#0()) -> c_62() * Step 7: SimplifyRHS WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: eratos#(@l) -> c_5(eratos#1#(@l)) eratos#1#(::(@x,@xs)) -> c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)) filter#(@p,@l) -> c_8(filter#1#(@l,@p)) filter#1#(::(@x,@xs),@p) -> c_9(filter#2#(filter(@p,@xs),@p,@x),filter#(@p,@xs)) - Weak TRS: #add(#0(),@y) -> @y #add(#neg(#s(#0())),@y) -> #pred(@y) #add(#neg(#s(#s(@x))),@y) -> #pred(#add(#pos(#s(@x)),@y)) #add(#pos(#s(#0())),@y) -> #succ(@y) #add(#pos(#s(#s(@x))),@y) -> #succ(#add(#pos(#s(@x)),@y)) #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #div(#0(),#0()) -> #divByZero() #div(#0(),#neg(@y)) -> #0() #div(#0(),#pos(@y)) -> #0() #div(#neg(@x),#0()) -> #divByZero() #div(#neg(@x),#neg(@y)) -> #pos(#natdiv(@x,@y)) #div(#neg(@x),#pos(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#0()) -> #divByZero() #div(#pos(@x),#neg(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#pos(@y)) -> #pos(#natdiv(@x,@y)) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #mult(#0(),#0()) -> #0() #mult(#0(),#neg(@y)) -> #0() #mult(#0(),#pos(@y)) -> #0() #mult(#neg(@x),#0()) -> #0() #mult(#neg(@x),#neg(@y)) -> #pos(#natmult(@x,@y)) #mult(#neg(@x),#pos(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#0()) -> #0() #mult(#pos(@x),#neg(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#pos(@y)) -> #pos(#natmult(@x,@y)) #natdiv(#0(),#0()) -> #divByZero() #natdiv(#s(@x),#s(@y)) -> #s(#natdiv(#natsub(@x,@y),#s(@y))) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@y),#natmult(@x,@y)) #natsub(@x,#0()) -> @x #natsub(#s(@x),#s(@y)) -> #natsub(@x,@y) #pred(#0()) -> #neg(#s(#0())) #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) #pred(#pos(#s(#0()))) -> #0() #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) #sub(@x,#0()) -> @x #sub(@x,#neg(@y)) -> #add(@x,#pos(@y)) #sub(@x,#pos(@y)) -> #add(@x,#neg(@y)) #succ(#0()) -> #pos(#s(#0())) #succ(#neg(#s(#0()))) -> #0() #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) *(@x,@y) -> #mult(@x,@y) -(@x,@y) -> #sub(@x,@y) div(@x,@y) -> #div(@x,@y) filter(@p,@l) -> filter#1(@l,@p) filter#1(::(@x,@xs),@p) -> filter#2(filter(@p,@xs),@p,@x) filter#1(nil(),@p) -> nil() filter#2(@xs',@p,@x) -> filter#3(#equal(mod(@x,@p),#0()),@x,@xs') filter#3(#false(),@x,@xs') -> ::(@x,@xs') filter#3(#true(),@x,@xs') -> @xs' mod(@x,@y) -> -(@x,*(@x,div(@x,@y))) - Signature: {#add/2,#and/2,#div/2,#eq/2,#equal/2,#mult/2,#natdiv/2,#natmult/2,#natsub/2,#pred/1,#sub/2,#succ/1,*/2,-/2 ,div/2,eratos/1,eratos#1/1,filter/2,filter#1/2,filter#2/3,filter#3/3,mod/2,#add#/2,#and#/2,#div#/2,#eq#/2 ,#equal#/2,#mult#/2,#natdiv#/2,#natmult#/2,#natsub#/2,#pred#/1,#sub#/2,#succ#/1,*#/2,-#/2,div#/2,eratos#/1 ,eratos#1#/1,filter#/2,filter#1#/2,filter#2#/3,filter#3#/3,mod#/2} / {#0/0,#divByZero/0,#false/0,#neg/1 ,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/2,c_7/0,c_8/1,c_9/2,c_10/0,c_11/3,c_12/0 ,c_13/0,c_14/3,c_15/0,c_16/1,c_17/2,c_18/1,c_19/2,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0 ,c_28/1,c_29/1,c_30/0,c_31/1,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/1,c_39/0,c_40/0,c_41/0,c_42/1 ,c_43/0,c_44/1,c_45/3,c_46/0,c_47/0,c_48/0,c_49/0,c_50/0,c_51/0,c_52/0,c_53/1,c_54/1,c_55/0,c_56/1,c_57/1 ,c_58/0,c_59/2,c_60/0,c_61/2,c_62/0,c_63/1,c_64/0,c_65/0,c_66/0,c_67/0,c_68/0,c_69/1,c_70/1,c_71/0,c_72/0 ,c_73/0,c_74/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult# ,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3# ,mod#} and constructors {#0,#divByZero,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:eratos#(@l) -> c_5(eratos#1#(@l)) -->_1 eratos#1#(::(@x,@xs)) -> c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)):2 2:S:eratos#1#(::(@x,@xs)) -> c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)) -->_2 filter#(@p,@l) -> c_8(filter#1#(@l,@p)):3 -->_1 eratos#(@l) -> c_5(eratos#1#(@l)):1 3:S:filter#(@p,@l) -> c_8(filter#1#(@l,@p)) -->_1 filter#1#(::(@x,@xs),@p) -> c_9(filter#2#(filter(@p,@xs),@p,@x),filter#(@p,@xs)):4 4:S:filter#1#(::(@x,@xs),@p) -> c_9(filter#2#(filter(@p,@xs),@p,@x),filter#(@p,@xs)) -->_2 filter#(@p,@l) -> c_8(filter#1#(@l,@p)):3 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: filter#1#(::(@x,@xs),@p) -> c_9(filter#(@p,@xs)) * Step 8: PredecessorEstimationCP WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: eratos#(@l) -> c_5(eratos#1#(@l)) eratos#1#(::(@x,@xs)) -> c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)) filter#(@p,@l) -> c_8(filter#1#(@l,@p)) filter#1#(::(@x,@xs),@p) -> c_9(filter#(@p,@xs)) - Weak TRS: #add(#0(),@y) -> @y #add(#neg(#s(#0())),@y) -> #pred(@y) #add(#neg(#s(#s(@x))),@y) -> #pred(#add(#pos(#s(@x)),@y)) #add(#pos(#s(#0())),@y) -> #succ(@y) #add(#pos(#s(#s(@x))),@y) -> #succ(#add(#pos(#s(@x)),@y)) #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #div(#0(),#0()) -> #divByZero() #div(#0(),#neg(@y)) -> #0() #div(#0(),#pos(@y)) -> #0() #div(#neg(@x),#0()) -> #divByZero() #div(#neg(@x),#neg(@y)) -> #pos(#natdiv(@x,@y)) #div(#neg(@x),#pos(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#0()) -> #divByZero() #div(#pos(@x),#neg(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#pos(@y)) -> #pos(#natdiv(@x,@y)) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #mult(#0(),#0()) -> #0() #mult(#0(),#neg(@y)) -> #0() #mult(#0(),#pos(@y)) -> #0() #mult(#neg(@x),#0()) -> #0() #mult(#neg(@x),#neg(@y)) -> #pos(#natmult(@x,@y)) #mult(#neg(@x),#pos(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#0()) -> #0() #mult(#pos(@x),#neg(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#pos(@y)) -> #pos(#natmult(@x,@y)) #natdiv(#0(),#0()) -> #divByZero() #natdiv(#s(@x),#s(@y)) -> #s(#natdiv(#natsub(@x,@y),#s(@y))) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@y),#natmult(@x,@y)) #natsub(@x,#0()) -> @x #natsub(#s(@x),#s(@y)) -> #natsub(@x,@y) #pred(#0()) -> #neg(#s(#0())) #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) #pred(#pos(#s(#0()))) -> #0() #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) #sub(@x,#0()) -> @x #sub(@x,#neg(@y)) -> #add(@x,#pos(@y)) #sub(@x,#pos(@y)) -> #add(@x,#neg(@y)) #succ(#0()) -> #pos(#s(#0())) #succ(#neg(#s(#0()))) -> #0() #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) *(@x,@y) -> #mult(@x,@y) -(@x,@y) -> #sub(@x,@y) div(@x,@y) -> #div(@x,@y) filter(@p,@l) -> filter#1(@l,@p) filter#1(::(@x,@xs),@p) -> filter#2(filter(@p,@xs),@p,@x) filter#1(nil(),@p) -> nil() filter#2(@xs',@p,@x) -> filter#3(#equal(mod(@x,@p),#0()),@x,@xs') filter#3(#false(),@x,@xs') -> ::(@x,@xs') filter#3(#true(),@x,@xs') -> @xs' mod(@x,@y) -> -(@x,*(@x,div(@x,@y))) - Signature: {#add/2,#and/2,#div/2,#eq/2,#equal/2,#mult/2,#natdiv/2,#natmult/2,#natsub/2,#pred/1,#sub/2,#succ/1,*/2,-/2 ,div/2,eratos/1,eratos#1/1,filter/2,filter#1/2,filter#2/3,filter#3/3,mod/2,#add#/2,#and#/2,#div#/2,#eq#/2 ,#equal#/2,#mult#/2,#natdiv#/2,#natmult#/2,#natsub#/2,#pred#/1,#sub#/2,#succ#/1,*#/2,-#/2,div#/2,eratos#/1 ,eratos#1#/1,filter#/2,filter#1#/2,filter#2#/3,filter#3#/3,mod#/2} / {#0/0,#divByZero/0,#false/0,#neg/1 ,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/3,c_12/0 ,c_13/0,c_14/3,c_15/0,c_16/1,c_17/2,c_18/1,c_19/2,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0 ,c_28/1,c_29/1,c_30/0,c_31/1,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/1,c_39/0,c_40/0,c_41/0,c_42/1 ,c_43/0,c_44/1,c_45/3,c_46/0,c_47/0,c_48/0,c_49/0,c_50/0,c_51/0,c_52/0,c_53/1,c_54/1,c_55/0,c_56/1,c_57/1 ,c_58/0,c_59/2,c_60/0,c_61/2,c_62/0,c_63/1,c_64/0,c_65/0,c_66/0,c_67/0,c_68/0,c_69/1,c_70/1,c_71/0,c_72/0 ,c_73/0,c_74/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult# ,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3# ,mod#} and constructors {#0,#divByZero,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 4: filter#1#(::(@x,@xs),@p) -> c_9(filter#(@p,@xs)) The strictly oriented rules are moved into the weak component. ** Step 8.a:1: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: eratos#(@l) -> c_5(eratos#1#(@l)) eratos#1#(::(@x,@xs)) -> c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)) filter#(@p,@l) -> c_8(filter#1#(@l,@p)) filter#1#(::(@x,@xs),@p) -> c_9(filter#(@p,@xs)) - Weak TRS: #add(#0(),@y) -> @y #add(#neg(#s(#0())),@y) -> #pred(@y) #add(#neg(#s(#s(@x))),@y) -> #pred(#add(#pos(#s(@x)),@y)) #add(#pos(#s(#0())),@y) -> #succ(@y) #add(#pos(#s(#s(@x))),@y) -> #succ(#add(#pos(#s(@x)),@y)) #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #div(#0(),#0()) -> #divByZero() #div(#0(),#neg(@y)) -> #0() #div(#0(),#pos(@y)) -> #0() #div(#neg(@x),#0()) -> #divByZero() #div(#neg(@x),#neg(@y)) -> #pos(#natdiv(@x,@y)) #div(#neg(@x),#pos(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#0()) -> #divByZero() #div(#pos(@x),#neg(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#pos(@y)) -> #pos(#natdiv(@x,@y)) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #mult(#0(),#0()) -> #0() #mult(#0(),#neg(@y)) -> #0() #mult(#0(),#pos(@y)) -> #0() #mult(#neg(@x),#0()) -> #0() #mult(#neg(@x),#neg(@y)) -> #pos(#natmult(@x,@y)) #mult(#neg(@x),#pos(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#0()) -> #0() #mult(#pos(@x),#neg(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#pos(@y)) -> #pos(#natmult(@x,@y)) #natdiv(#0(),#0()) -> #divByZero() #natdiv(#s(@x),#s(@y)) -> #s(#natdiv(#natsub(@x,@y),#s(@y))) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@y),#natmult(@x,@y)) #natsub(@x,#0()) -> @x #natsub(#s(@x),#s(@y)) -> #natsub(@x,@y) #pred(#0()) -> #neg(#s(#0())) #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) #pred(#pos(#s(#0()))) -> #0() #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) #sub(@x,#0()) -> @x #sub(@x,#neg(@y)) -> #add(@x,#pos(@y)) #sub(@x,#pos(@y)) -> #add(@x,#neg(@y)) #succ(#0()) -> #pos(#s(#0())) #succ(#neg(#s(#0()))) -> #0() #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) *(@x,@y) -> #mult(@x,@y) -(@x,@y) -> #sub(@x,@y) div(@x,@y) -> #div(@x,@y) filter(@p,@l) -> filter#1(@l,@p) filter#1(::(@x,@xs),@p) -> filter#2(filter(@p,@xs),@p,@x) filter#1(nil(),@p) -> nil() filter#2(@xs',@p,@x) -> filter#3(#equal(mod(@x,@p),#0()),@x,@xs') filter#3(#false(),@x,@xs') -> ::(@x,@xs') filter#3(#true(),@x,@xs') -> @xs' mod(@x,@y) -> -(@x,*(@x,div(@x,@y))) - Signature: {#add/2,#and/2,#div/2,#eq/2,#equal/2,#mult/2,#natdiv/2,#natmult/2,#natsub/2,#pred/1,#sub/2,#succ/1,*/2,-/2 ,div/2,eratos/1,eratos#1/1,filter/2,filter#1/2,filter#2/3,filter#3/3,mod/2,#add#/2,#and#/2,#div#/2,#eq#/2 ,#equal#/2,#mult#/2,#natdiv#/2,#natmult#/2,#natsub#/2,#pred#/1,#sub#/2,#succ#/1,*#/2,-#/2,div#/2,eratos#/1 ,eratos#1#/1,filter#/2,filter#1#/2,filter#2#/3,filter#3#/3,mod#/2} / {#0/0,#divByZero/0,#false/0,#neg/1 ,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/3,c_12/0 ,c_13/0,c_14/3,c_15/0,c_16/1,c_17/2,c_18/1,c_19/2,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0 ,c_28/1,c_29/1,c_30/0,c_31/1,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/1,c_39/0,c_40/0,c_41/0,c_42/1 ,c_43/0,c_44/1,c_45/3,c_46/0,c_47/0,c_48/0,c_49/0,c_50/0,c_51/0,c_52/0,c_53/1,c_54/1,c_55/0,c_56/1,c_57/1 ,c_58/0,c_59/2,c_60/0,c_61/2,c_62/0,c_63/1,c_64/0,c_65/0,c_66/0,c_67/0,c_68/0,c_69/1,c_70/1,c_71/0,c_72/0 ,c_73/0,c_74/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult# ,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3# ,mod#} and constructors {#0,#divByZero,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_5) = {1}, uargs(c_6) = {1,2}, uargs(c_8) = {1}, uargs(c_9) = {1} Following symbols are considered usable: {filter,filter#1,filter#2,filter#3,#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult#,#natsub# ,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3#,mod#} TcT has computed the following interpretation: p(#0) = [1] [1] p(#add) = [0] [1] p(#and) = [0 0] x1 + [0 1] x2 + [1] [1 1] [0 0] [1] p(#div) = [1 0] x1 + [1] [0 0] [0] p(#divByZero) = [0] [0] p(#eq) = [0] [0] p(#equal) = [0 0] x1 + [1 0] x2 + [1] [1 0] [0 1] [1] p(#false) = [0] [0] p(#mult) = [0 0] x1 + [1] [0 1] [0] p(#natdiv) = [0 0] x1 + [0 0] x2 + [1] [1 1] [0 1] [0] p(#natmult) = [0 1] x1 + [0] [0 1] [1] p(#natsub) = [1 1] x2 + [1] [1 0] [1] p(#neg) = [0] [0] p(#pos) = [0] [0] p(#pred) = [0] [1] p(#s) = [0] [0] p(#sub) = [1 0] x2 + [1] [0 0] [0] p(#succ) = [0] [1] p(#true) = [1] [1] p(*) = [1 1] x1 + [1 1] x2 + [1] [0 1] [0 1] [1] p(-) = [0 1] x1 + [1 0] x2 + [0] [0 0] [0 1] [0] p(::) = [1 0] x1 + [1 1] x2 + [0] [0 1] [0 1] [1] p(div) = [0 0] x1 + [1 0] x2 + [1] [0 1] [1 0] [1] p(eratos) = [0] [0] p(eratos#1) = [0] [0] p(filter) = [1 0] x2 + [0] [0 1] [0] p(filter#1) = [1 0] x1 + [0] [0 1] [0] p(filter#2) = [1 1] x1 + [1 0] x3 + [0] [0 1] [0 1] [1] p(filter#3) = [1 0] x2 + [1 1] x3 + [0] [0 1] [0 1] [1] p(mod) = [1] [0] p(nil) = [0] [0] p(#add#) = [0] [0] p(#and#) = [0] [0] p(#div#) = [0] [0] p(#eq#) = [0] [0] p(#equal#) = [0] [0] p(#mult#) = [0] [0] p(#natdiv#) = [0] [0] p(#natmult#) = [0] [0] p(#natsub#) = [0] [0] p(#pred#) = [0] [0] p(#sub#) = [0] [0] p(#succ#) = [0] [0] p(*#) = [0] [0] p(-#) = [0] [0] p(div#) = [0] [0] p(eratos#) = [1 1] x1 + [1] [0 0] [0] p(eratos#1#) = [1 1] x1 + [1] [0 0] [1] p(filter#) = [0 1] x2 + [0] [0 0] [1] p(filter#1#) = [0 1] x1 + [0] [0 0] [1] p(filter#2#) = [0] [0] p(filter#3#) = [0] [0] p(mod#) = [0] [0] p(c_1) = [0] [0] p(c_2) = [0] [0] p(c_3) = [0] [0] p(c_4) = [0] [0] p(c_5) = [1 0] x1 + [0] [0 0] [0] p(c_6) = [1 0] x1 + [1 0] x2 + [1] [0 0] [0 1] [0] p(c_7) = [0] [0] p(c_8) = [1 0] x1 + [0] [0 0] [0] p(c_9) = [1 0] x1 + [0] [0 0] [0] p(c_10) = [0] [0] p(c_11) = [0] [0] p(c_12) = [0] [0] p(c_13) = [0] [0] p(c_14) = [0] [0] p(c_15) = [0] [0] p(c_16) = [0] [0] p(c_17) = [0] [0] p(c_18) = [0] [0] p(c_19) = [0] [0] p(c_20) = [0] [0] p(c_21) = [0] [0] p(c_22) = [0] [0] p(c_23) = [0] [0] p(c_24) = [0] [0] p(c_25) = [0] [0] p(c_26) = [0] [0] p(c_27) = [0] [0] p(c_28) = [0] [0] p(c_29) = [0] [0] p(c_30) = [0] [0] p(c_31) = [0] [0] p(c_32) = [0] [0] p(c_33) = [0] [0] p(c_34) = [0] [0] p(c_35) = [0] [0] p(c_36) = [0] [0] p(c_37) = [0] [0] p(c_38) = [0] [0] p(c_39) = [0] [0] p(c_40) = [0] [0] p(c_41) = [0] [0] p(c_42) = [0] [0] p(c_43) = [0] [0] p(c_44) = [0] [0] p(c_45) = [0] [0] p(c_46) = [0] [0] p(c_47) = [0] [0] p(c_48) = [0] [0] p(c_49) = [0] [0] p(c_50) = [0] [0] p(c_51) = [0] [0] p(c_52) = [0] [0] p(c_53) = [0] [0] p(c_54) = [0] [0] p(c_55) = [0] [0] p(c_56) = [0] [0] p(c_57) = [0] [0] p(c_58) = [0] [0] p(c_59) = [0] [0] p(c_60) = [0] [0] p(c_61) = [0] [0] p(c_62) = [0] [0] p(c_63) = [0] [0] p(c_64) = [0] [0] p(c_65) = [0] [0] p(c_66) = [0] [0] p(c_67) = [0] [0] p(c_68) = [0] [0] p(c_69) = [0] [0] p(c_70) = [0] [0] p(c_71) = [0] [0] p(c_72) = [0] [0] p(c_73) = [0] [0] p(c_74) = [0] [0] Following rules are strictly oriented: filter#1#(::(@x,@xs),@p) = [0 1] @x + [0 1] @xs + [1] [0 0] [0 0] [1] > [0 1] @xs + [0] [0 0] [0] = c_9(filter#(@p,@xs)) Following rules are (at-least) weakly oriented: eratos#(@l) = [1 1] @l + [1] [0 0] [0] >= [1 1] @l + [1] [0 0] [0] = c_5(eratos#1#(@l)) eratos#1#(::(@x,@xs)) = [1 1] @x + [1 2] @xs + [2] [0 0] [0 0] [1] >= [1 2] @xs + [2] [0 0] [1] = c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)) filter#(@p,@l) = [0 1] @l + [0] [0 0] [1] >= [0 1] @l + [0] [0 0] [0] = c_8(filter#1#(@l,@p)) filter(@p,@l) = [1 0] @l + [0] [0 1] [0] >= [1 0] @l + [0] [0 1] [0] = filter#1(@l,@p) filter#1(::(@x,@xs),@p) = [1 0] @x + [1 1] @xs + [0] [0 1] [0 1] [1] >= [1 0] @x + [1 1] @xs + [0] [0 1] [0 1] [1] = filter#2(filter(@p,@xs),@p,@x) filter#1(nil(),@p) = [0] [0] >= [0] [0] = nil() filter#2(@xs',@p,@x) = [1 0] @x + [1 1] @xs' + [0] [0 1] [0 1] [1] >= [1 0] @x + [1 1] @xs' + [0] [0 1] [0 1] [1] = filter#3(#equal(mod(@x,@p),#0()),@x,@xs') filter#3(#false(),@x,@xs') = [1 0] @x + [1 1] @xs' + [0] [0 1] [0 1] [1] >= [1 0] @x + [1 1] @xs' + [0] [0 1] [0 1] [1] = ::(@x,@xs') filter#3(#true(),@x,@xs') = [1 0] @x + [1 1] @xs' + [0] [0 1] [0 1] [1] >= [1 0] @xs' + [0] [0 1] [0] = @xs' ** Step 8.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: eratos#(@l) -> c_5(eratos#1#(@l)) eratos#1#(::(@x,@xs)) -> c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)) filter#(@p,@l) -> c_8(filter#1#(@l,@p)) - Weak DPs: filter#1#(::(@x,@xs),@p) -> c_9(filter#(@p,@xs)) - Weak TRS: #add(#0(),@y) -> @y #add(#neg(#s(#0())),@y) -> #pred(@y) #add(#neg(#s(#s(@x))),@y) -> #pred(#add(#pos(#s(@x)),@y)) #add(#pos(#s(#0())),@y) -> #succ(@y) #add(#pos(#s(#s(@x))),@y) -> #succ(#add(#pos(#s(@x)),@y)) #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #div(#0(),#0()) -> #divByZero() #div(#0(),#neg(@y)) -> #0() #div(#0(),#pos(@y)) -> #0() #div(#neg(@x),#0()) -> #divByZero() #div(#neg(@x),#neg(@y)) -> #pos(#natdiv(@x,@y)) #div(#neg(@x),#pos(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#0()) -> #divByZero() #div(#pos(@x),#neg(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#pos(@y)) -> #pos(#natdiv(@x,@y)) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #mult(#0(),#0()) -> #0() #mult(#0(),#neg(@y)) -> #0() #mult(#0(),#pos(@y)) -> #0() #mult(#neg(@x),#0()) -> #0() #mult(#neg(@x),#neg(@y)) -> #pos(#natmult(@x,@y)) #mult(#neg(@x),#pos(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#0()) -> #0() #mult(#pos(@x),#neg(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#pos(@y)) -> #pos(#natmult(@x,@y)) #natdiv(#0(),#0()) -> #divByZero() #natdiv(#s(@x),#s(@y)) -> #s(#natdiv(#natsub(@x,@y),#s(@y))) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@y),#natmult(@x,@y)) #natsub(@x,#0()) -> @x #natsub(#s(@x),#s(@y)) -> #natsub(@x,@y) #pred(#0()) -> #neg(#s(#0())) #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) #pred(#pos(#s(#0()))) -> #0() #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) #sub(@x,#0()) -> @x #sub(@x,#neg(@y)) -> #add(@x,#pos(@y)) #sub(@x,#pos(@y)) -> #add(@x,#neg(@y)) #succ(#0()) -> #pos(#s(#0())) #succ(#neg(#s(#0()))) -> #0() #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) *(@x,@y) -> #mult(@x,@y) -(@x,@y) -> #sub(@x,@y) div(@x,@y) -> #div(@x,@y) filter(@p,@l) -> filter#1(@l,@p) filter#1(::(@x,@xs),@p) -> filter#2(filter(@p,@xs),@p,@x) filter#1(nil(),@p) -> nil() filter#2(@xs',@p,@x) -> filter#3(#equal(mod(@x,@p),#0()),@x,@xs') filter#3(#false(),@x,@xs') -> ::(@x,@xs') filter#3(#true(),@x,@xs') -> @xs' mod(@x,@y) -> -(@x,*(@x,div(@x,@y))) - Signature: {#add/2,#and/2,#div/2,#eq/2,#equal/2,#mult/2,#natdiv/2,#natmult/2,#natsub/2,#pred/1,#sub/2,#succ/1,*/2,-/2 ,div/2,eratos/1,eratos#1/1,filter/2,filter#1/2,filter#2/3,filter#3/3,mod/2,#add#/2,#and#/2,#div#/2,#eq#/2 ,#equal#/2,#mult#/2,#natdiv#/2,#natmult#/2,#natsub#/2,#pred#/1,#sub#/2,#succ#/1,*#/2,-#/2,div#/2,eratos#/1 ,eratos#1#/1,filter#/2,filter#1#/2,filter#2#/3,filter#3#/3,mod#/2} / {#0/0,#divByZero/0,#false/0,#neg/1 ,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/3,c_12/0 ,c_13/0,c_14/3,c_15/0,c_16/1,c_17/2,c_18/1,c_19/2,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0 ,c_28/1,c_29/1,c_30/0,c_31/1,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/1,c_39/0,c_40/0,c_41/0,c_42/1 ,c_43/0,c_44/1,c_45/3,c_46/0,c_47/0,c_48/0,c_49/0,c_50/0,c_51/0,c_52/0,c_53/1,c_54/1,c_55/0,c_56/1,c_57/1 ,c_58/0,c_59/2,c_60/0,c_61/2,c_62/0,c_63/1,c_64/0,c_65/0,c_66/0,c_67/0,c_68/0,c_69/1,c_70/1,c_71/0,c_72/0 ,c_73/0,c_74/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult# ,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3# ,mod#} and constructors {#0,#divByZero,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () ** Step 8.b:1: PredecessorEstimationCP WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: eratos#(@l) -> c_5(eratos#1#(@l)) eratos#1#(::(@x,@xs)) -> c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)) filter#(@p,@l) -> c_8(filter#1#(@l,@p)) - Weak DPs: filter#1#(::(@x,@xs),@p) -> c_9(filter#(@p,@xs)) - Weak TRS: #add(#0(),@y) -> @y #add(#neg(#s(#0())),@y) -> #pred(@y) #add(#neg(#s(#s(@x))),@y) -> #pred(#add(#pos(#s(@x)),@y)) #add(#pos(#s(#0())),@y) -> #succ(@y) #add(#pos(#s(#s(@x))),@y) -> #succ(#add(#pos(#s(@x)),@y)) #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #div(#0(),#0()) -> #divByZero() #div(#0(),#neg(@y)) -> #0() #div(#0(),#pos(@y)) -> #0() #div(#neg(@x),#0()) -> #divByZero() #div(#neg(@x),#neg(@y)) -> #pos(#natdiv(@x,@y)) #div(#neg(@x),#pos(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#0()) -> #divByZero() #div(#pos(@x),#neg(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#pos(@y)) -> #pos(#natdiv(@x,@y)) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #mult(#0(),#0()) -> #0() #mult(#0(),#neg(@y)) -> #0() #mult(#0(),#pos(@y)) -> #0() #mult(#neg(@x),#0()) -> #0() #mult(#neg(@x),#neg(@y)) -> #pos(#natmult(@x,@y)) #mult(#neg(@x),#pos(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#0()) -> #0() #mult(#pos(@x),#neg(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#pos(@y)) -> #pos(#natmult(@x,@y)) #natdiv(#0(),#0()) -> #divByZero() #natdiv(#s(@x),#s(@y)) -> #s(#natdiv(#natsub(@x,@y),#s(@y))) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@y),#natmult(@x,@y)) #natsub(@x,#0()) -> @x #natsub(#s(@x),#s(@y)) -> #natsub(@x,@y) #pred(#0()) -> #neg(#s(#0())) #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) #pred(#pos(#s(#0()))) -> #0() #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) #sub(@x,#0()) -> @x #sub(@x,#neg(@y)) -> #add(@x,#pos(@y)) #sub(@x,#pos(@y)) -> #add(@x,#neg(@y)) #succ(#0()) -> #pos(#s(#0())) #succ(#neg(#s(#0()))) -> #0() #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) *(@x,@y) -> #mult(@x,@y) -(@x,@y) -> #sub(@x,@y) div(@x,@y) -> #div(@x,@y) filter(@p,@l) -> filter#1(@l,@p) filter#1(::(@x,@xs),@p) -> filter#2(filter(@p,@xs),@p,@x) filter#1(nil(),@p) -> nil() filter#2(@xs',@p,@x) -> filter#3(#equal(mod(@x,@p),#0()),@x,@xs') filter#3(#false(),@x,@xs') -> ::(@x,@xs') filter#3(#true(),@x,@xs') -> @xs' mod(@x,@y) -> -(@x,*(@x,div(@x,@y))) - Signature: {#add/2,#and/2,#div/2,#eq/2,#equal/2,#mult/2,#natdiv/2,#natmult/2,#natsub/2,#pred/1,#sub/2,#succ/1,*/2,-/2 ,div/2,eratos/1,eratos#1/1,filter/2,filter#1/2,filter#2/3,filter#3/3,mod/2,#add#/2,#and#/2,#div#/2,#eq#/2 ,#equal#/2,#mult#/2,#natdiv#/2,#natmult#/2,#natsub#/2,#pred#/1,#sub#/2,#succ#/1,*#/2,-#/2,div#/2,eratos#/1 ,eratos#1#/1,filter#/2,filter#1#/2,filter#2#/3,filter#3#/3,mod#/2} / {#0/0,#divByZero/0,#false/0,#neg/1 ,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/3,c_12/0 ,c_13/0,c_14/3,c_15/0,c_16/1,c_17/2,c_18/1,c_19/2,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0 ,c_28/1,c_29/1,c_30/0,c_31/1,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/1,c_39/0,c_40/0,c_41/0,c_42/1 ,c_43/0,c_44/1,c_45/3,c_46/0,c_47/0,c_48/0,c_49/0,c_50/0,c_51/0,c_52/0,c_53/1,c_54/1,c_55/0,c_56/1,c_57/1 ,c_58/0,c_59/2,c_60/0,c_61/2,c_62/0,c_63/1,c_64/0,c_65/0,c_66/0,c_67/0,c_68/0,c_69/1,c_70/1,c_71/0,c_72/0 ,c_73/0,c_74/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult# ,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3# ,mod#} and constructors {#0,#divByZero,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: eratos#(@l) -> c_5(eratos#1#(@l)) Consider the set of all dependency pairs 1: eratos#(@l) -> c_5(eratos#1#(@l)) 2: eratos#1#(::(@x,@xs)) -> c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)) 3: filter#(@p,@l) -> c_8(filter#1#(@l,@p)) 4: filter#1#(::(@x,@xs),@p) -> c_9(filter#(@p,@xs)) Processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^1)) SPACE(?,?)on application of the dependency pairs {1} These cover all (indirect) predecessors of dependency pairs {1,2} their number of applications is equally bounded. The dependency pairs are shifted into the weak component. *** Step 8.b:1.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: eratos#(@l) -> c_5(eratos#1#(@l)) eratos#1#(::(@x,@xs)) -> c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)) filter#(@p,@l) -> c_8(filter#1#(@l,@p)) - Weak DPs: filter#1#(::(@x,@xs),@p) -> c_9(filter#(@p,@xs)) - Weak TRS: #add(#0(),@y) -> @y #add(#neg(#s(#0())),@y) -> #pred(@y) #add(#neg(#s(#s(@x))),@y) -> #pred(#add(#pos(#s(@x)),@y)) #add(#pos(#s(#0())),@y) -> #succ(@y) #add(#pos(#s(#s(@x))),@y) -> #succ(#add(#pos(#s(@x)),@y)) #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #div(#0(),#0()) -> #divByZero() #div(#0(),#neg(@y)) -> #0() #div(#0(),#pos(@y)) -> #0() #div(#neg(@x),#0()) -> #divByZero() #div(#neg(@x),#neg(@y)) -> #pos(#natdiv(@x,@y)) #div(#neg(@x),#pos(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#0()) -> #divByZero() #div(#pos(@x),#neg(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#pos(@y)) -> #pos(#natdiv(@x,@y)) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #mult(#0(),#0()) -> #0() #mult(#0(),#neg(@y)) -> #0() #mult(#0(),#pos(@y)) -> #0() #mult(#neg(@x),#0()) -> #0() #mult(#neg(@x),#neg(@y)) -> #pos(#natmult(@x,@y)) #mult(#neg(@x),#pos(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#0()) -> #0() #mult(#pos(@x),#neg(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#pos(@y)) -> #pos(#natmult(@x,@y)) #natdiv(#0(),#0()) -> #divByZero() #natdiv(#s(@x),#s(@y)) -> #s(#natdiv(#natsub(@x,@y),#s(@y))) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@y),#natmult(@x,@y)) #natsub(@x,#0()) -> @x #natsub(#s(@x),#s(@y)) -> #natsub(@x,@y) #pred(#0()) -> #neg(#s(#0())) #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) #pred(#pos(#s(#0()))) -> #0() #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) #sub(@x,#0()) -> @x #sub(@x,#neg(@y)) -> #add(@x,#pos(@y)) #sub(@x,#pos(@y)) -> #add(@x,#neg(@y)) #succ(#0()) -> #pos(#s(#0())) #succ(#neg(#s(#0()))) -> #0() #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) *(@x,@y) -> #mult(@x,@y) -(@x,@y) -> #sub(@x,@y) div(@x,@y) -> #div(@x,@y) filter(@p,@l) -> filter#1(@l,@p) filter#1(::(@x,@xs),@p) -> filter#2(filter(@p,@xs),@p,@x) filter#1(nil(),@p) -> nil() filter#2(@xs',@p,@x) -> filter#3(#equal(mod(@x,@p),#0()),@x,@xs') filter#3(#false(),@x,@xs') -> ::(@x,@xs') filter#3(#true(),@x,@xs') -> @xs' mod(@x,@y) -> -(@x,*(@x,div(@x,@y))) - Signature: {#add/2,#and/2,#div/2,#eq/2,#equal/2,#mult/2,#natdiv/2,#natmult/2,#natsub/2,#pred/1,#sub/2,#succ/1,*/2,-/2 ,div/2,eratos/1,eratos#1/1,filter/2,filter#1/2,filter#2/3,filter#3/3,mod/2,#add#/2,#and#/2,#div#/2,#eq#/2 ,#equal#/2,#mult#/2,#natdiv#/2,#natmult#/2,#natsub#/2,#pred#/1,#sub#/2,#succ#/1,*#/2,-#/2,div#/2,eratos#/1 ,eratos#1#/1,filter#/2,filter#1#/2,filter#2#/3,filter#3#/3,mod#/2} / {#0/0,#divByZero/0,#false/0,#neg/1 ,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/3,c_12/0 ,c_13/0,c_14/3,c_15/0,c_16/1,c_17/2,c_18/1,c_19/2,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0 ,c_28/1,c_29/1,c_30/0,c_31/1,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/1,c_39/0,c_40/0,c_41/0,c_42/1 ,c_43/0,c_44/1,c_45/3,c_46/0,c_47/0,c_48/0,c_49/0,c_50/0,c_51/0,c_52/0,c_53/1,c_54/1,c_55/0,c_56/1,c_57/1 ,c_58/0,c_59/2,c_60/0,c_61/2,c_62/0,c_63/1,c_64/0,c_65/0,c_66/0,c_67/0,c_68/0,c_69/1,c_70/1,c_71/0,c_72/0 ,c_73/0,c_74/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult# ,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3# ,mod#} and constructors {#0,#divByZero,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_5) = {1}, uargs(c_6) = {1,2}, uargs(c_8) = {1}, uargs(c_9) = {1} Following symbols are considered usable: {filter,filter#1,filter#2,filter#3,#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult#,#natsub# ,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3#,mod#} TcT has computed the following interpretation: p(#0) = [0] p(#add) = [0] p(#and) = [0] p(#div) = [0] p(#divByZero) = [0] p(#eq) = [4] x1 + [0] p(#equal) = [1] x1 + [0] p(#false) = [0] p(#mult) = [0] p(#natdiv) = [7] p(#natmult) = [4] x1 + [0] p(#natsub) = [0] p(#neg) = [0] p(#pos) = [1] x1 + [1] p(#pred) = [0] p(#s) = [1] p(#sub) = [0] p(#succ) = [0] p(#true) = [0] p(*) = [0] p(-) = [0] p(::) = [1] x2 + [1] p(div) = [0] p(eratos) = [0] p(eratos#1) = [0] p(filter) = [1] x2 + [0] p(filter#1) = [1] x1 + [0] p(filter#2) = [1] x1 + [1] p(filter#3) = [1] x3 + [1] p(mod) = [0] p(nil) = [0] p(#add#) = [0] p(#and#) = [0] p(#div#) = [0] p(#eq#) = [0] p(#equal#) = [0] p(#mult#) = [0] p(#natdiv#) = [0] p(#natmult#) = [0] p(#natsub#) = [0] p(#pred#) = [0] p(#sub#) = [0] p(#succ#) = [0] p(*#) = [0] p(-#) = [0] p(div#) = [1] x2 + [0] p(eratos#) = [1] x1 + [4] p(eratos#1#) = [1] x1 + [3] p(filter#) = [0] p(filter#1#) = [0] p(filter#2#) = [0] p(filter#3#) = [0] p(mod#) = [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [1] x1 + [0] p(c_6) = [1] x1 + [4] x2 + [0] p(c_7) = [0] p(c_8) = [4] x1 + [0] p(c_9) = [2] x1 + [0] p(c_10) = [0] p(c_11) = [4] x1 + [1] x3 + [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [2] x1 + [4] x2 + [0] p(c_15) = [0] p(c_16) = [1] x1 + [0] p(c_17) = [1] x1 + [4] x2 + [0] p(c_18) = [0] p(c_19) = [1] x1 + [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [0] p(c_28) = [1] x1 + [0] p(c_29) = [0] p(c_30) = [0] p(c_31) = [0] p(c_32) = [2] x1 + [0] p(c_33) = [0] p(c_34) = [0] p(c_35) = [0] p(c_36) = [0] p(c_37) = [0] p(c_38) = [0] p(c_39) = [0] p(c_40) = [0] p(c_41) = [0] p(c_42) = [0] p(c_43) = [0] p(c_44) = [0] p(c_45) = [1] x1 + [1] x3 + [0] p(c_46) = [0] p(c_47) = [0] p(c_48) = [0] p(c_49) = [0] p(c_50) = [0] p(c_51) = [0] p(c_52) = [0] p(c_53) = [0] p(c_54) = [2] x1 + [0] p(c_55) = [0] p(c_56) = [1] x1 + [0] p(c_57) = [0] p(c_58) = [0] p(c_59) = [1] x1 + [0] p(c_60) = [0] p(c_61) = [1] x2 + [0] p(c_62) = [0] p(c_63) = [1] x1 + [0] p(c_64) = [0] p(c_65) = [0] p(c_66) = [0] p(c_67) = [0] p(c_68) = [0] p(c_69) = [0] p(c_70) = [1] x1 + [0] p(c_71) = [0] p(c_72) = [0] p(c_73) = [0] p(c_74) = [0] Following rules are strictly oriented: eratos#(@l) = [1] @l + [4] > [1] @l + [3] = c_5(eratos#1#(@l)) Following rules are (at-least) weakly oriented: eratos#1#(::(@x,@xs)) = [1] @xs + [4] >= [1] @xs + [4] = c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)) filter#(@p,@l) = [0] >= [0] = c_8(filter#1#(@l,@p)) filter#1#(::(@x,@xs),@p) = [0] >= [0] = c_9(filter#(@p,@xs)) filter(@p,@l) = [1] @l + [0] >= [1] @l + [0] = filter#1(@l,@p) filter#1(::(@x,@xs),@p) = [1] @xs + [1] >= [1] @xs + [1] = filter#2(filter(@p,@xs),@p,@x) filter#1(nil(),@p) = [0] >= [0] = nil() filter#2(@xs',@p,@x) = [1] @xs' + [1] >= [1] @xs' + [1] = filter#3(#equal(mod(@x,@p),#0()),@x,@xs') filter#3(#false(),@x,@xs') = [1] @xs' + [1] >= [1] @xs' + [1] = ::(@x,@xs') filter#3(#true(),@x,@xs') = [1] @xs' + [1] >= [1] @xs' + [0] = @xs' *** Step 8.b:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: eratos#1#(::(@x,@xs)) -> c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)) filter#(@p,@l) -> c_8(filter#1#(@l,@p)) - Weak DPs: eratos#(@l) -> c_5(eratos#1#(@l)) filter#1#(::(@x,@xs),@p) -> c_9(filter#(@p,@xs)) - Weak TRS: #add(#0(),@y) -> @y #add(#neg(#s(#0())),@y) -> #pred(@y) #add(#neg(#s(#s(@x))),@y) -> #pred(#add(#pos(#s(@x)),@y)) #add(#pos(#s(#0())),@y) -> #succ(@y) #add(#pos(#s(#s(@x))),@y) -> #succ(#add(#pos(#s(@x)),@y)) #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #div(#0(),#0()) -> #divByZero() #div(#0(),#neg(@y)) -> #0() #div(#0(),#pos(@y)) -> #0() #div(#neg(@x),#0()) -> #divByZero() #div(#neg(@x),#neg(@y)) -> #pos(#natdiv(@x,@y)) #div(#neg(@x),#pos(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#0()) -> #divByZero() #div(#pos(@x),#neg(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#pos(@y)) -> #pos(#natdiv(@x,@y)) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #mult(#0(),#0()) -> #0() #mult(#0(),#neg(@y)) -> #0() #mult(#0(),#pos(@y)) -> #0() #mult(#neg(@x),#0()) -> #0() #mult(#neg(@x),#neg(@y)) -> #pos(#natmult(@x,@y)) #mult(#neg(@x),#pos(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#0()) -> #0() #mult(#pos(@x),#neg(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#pos(@y)) -> #pos(#natmult(@x,@y)) #natdiv(#0(),#0()) -> #divByZero() #natdiv(#s(@x),#s(@y)) -> #s(#natdiv(#natsub(@x,@y),#s(@y))) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@y),#natmult(@x,@y)) #natsub(@x,#0()) -> @x #natsub(#s(@x),#s(@y)) -> #natsub(@x,@y) #pred(#0()) -> #neg(#s(#0())) #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) #pred(#pos(#s(#0()))) -> #0() #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) #sub(@x,#0()) -> @x #sub(@x,#neg(@y)) -> #add(@x,#pos(@y)) #sub(@x,#pos(@y)) -> #add(@x,#neg(@y)) #succ(#0()) -> #pos(#s(#0())) #succ(#neg(#s(#0()))) -> #0() #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) *(@x,@y) -> #mult(@x,@y) -(@x,@y) -> #sub(@x,@y) div(@x,@y) -> #div(@x,@y) filter(@p,@l) -> filter#1(@l,@p) filter#1(::(@x,@xs),@p) -> filter#2(filter(@p,@xs),@p,@x) filter#1(nil(),@p) -> nil() filter#2(@xs',@p,@x) -> filter#3(#equal(mod(@x,@p),#0()),@x,@xs') filter#3(#false(),@x,@xs') -> ::(@x,@xs') filter#3(#true(),@x,@xs') -> @xs' mod(@x,@y) -> -(@x,*(@x,div(@x,@y))) - Signature: {#add/2,#and/2,#div/2,#eq/2,#equal/2,#mult/2,#natdiv/2,#natmult/2,#natsub/2,#pred/1,#sub/2,#succ/1,*/2,-/2 ,div/2,eratos/1,eratos#1/1,filter/2,filter#1/2,filter#2/3,filter#3/3,mod/2,#add#/2,#and#/2,#div#/2,#eq#/2 ,#equal#/2,#mult#/2,#natdiv#/2,#natmult#/2,#natsub#/2,#pred#/1,#sub#/2,#succ#/1,*#/2,-#/2,div#/2,eratos#/1 ,eratos#1#/1,filter#/2,filter#1#/2,filter#2#/3,filter#3#/3,mod#/2} / {#0/0,#divByZero/0,#false/0,#neg/1 ,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/3,c_12/0 ,c_13/0,c_14/3,c_15/0,c_16/1,c_17/2,c_18/1,c_19/2,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0 ,c_28/1,c_29/1,c_30/0,c_31/1,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/1,c_39/0,c_40/0,c_41/0,c_42/1 ,c_43/0,c_44/1,c_45/3,c_46/0,c_47/0,c_48/0,c_49/0,c_50/0,c_51/0,c_52/0,c_53/1,c_54/1,c_55/0,c_56/1,c_57/1 ,c_58/0,c_59/2,c_60/0,c_61/2,c_62/0,c_63/1,c_64/0,c_65/0,c_66/0,c_67/0,c_68/0,c_69/1,c_70/1,c_71/0,c_72/0 ,c_73/0,c_74/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult# ,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3# ,mod#} and constructors {#0,#divByZero,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () *** Step 8.b:1.b:1: PredecessorEstimationCP WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: filter#(@p,@l) -> c_8(filter#1#(@l,@p)) - Weak DPs: eratos#(@l) -> c_5(eratos#1#(@l)) eratos#1#(::(@x,@xs)) -> c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)) filter#1#(::(@x,@xs),@p) -> c_9(filter#(@p,@xs)) - Weak TRS: #add(#0(),@y) -> @y #add(#neg(#s(#0())),@y) -> #pred(@y) #add(#neg(#s(#s(@x))),@y) -> #pred(#add(#pos(#s(@x)),@y)) #add(#pos(#s(#0())),@y) -> #succ(@y) #add(#pos(#s(#s(@x))),@y) -> #succ(#add(#pos(#s(@x)),@y)) #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #div(#0(),#0()) -> #divByZero() #div(#0(),#neg(@y)) -> #0() #div(#0(),#pos(@y)) -> #0() #div(#neg(@x),#0()) -> #divByZero() #div(#neg(@x),#neg(@y)) -> #pos(#natdiv(@x,@y)) #div(#neg(@x),#pos(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#0()) -> #divByZero() #div(#pos(@x),#neg(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#pos(@y)) -> #pos(#natdiv(@x,@y)) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #mult(#0(),#0()) -> #0() #mult(#0(),#neg(@y)) -> #0() #mult(#0(),#pos(@y)) -> #0() #mult(#neg(@x),#0()) -> #0() #mult(#neg(@x),#neg(@y)) -> #pos(#natmult(@x,@y)) #mult(#neg(@x),#pos(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#0()) -> #0() #mult(#pos(@x),#neg(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#pos(@y)) -> #pos(#natmult(@x,@y)) #natdiv(#0(),#0()) -> #divByZero() #natdiv(#s(@x),#s(@y)) -> #s(#natdiv(#natsub(@x,@y),#s(@y))) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@y),#natmult(@x,@y)) #natsub(@x,#0()) -> @x #natsub(#s(@x),#s(@y)) -> #natsub(@x,@y) #pred(#0()) -> #neg(#s(#0())) #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) #pred(#pos(#s(#0()))) -> #0() #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) #sub(@x,#0()) -> @x #sub(@x,#neg(@y)) -> #add(@x,#pos(@y)) #sub(@x,#pos(@y)) -> #add(@x,#neg(@y)) #succ(#0()) -> #pos(#s(#0())) #succ(#neg(#s(#0()))) -> #0() #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) *(@x,@y) -> #mult(@x,@y) -(@x,@y) -> #sub(@x,@y) div(@x,@y) -> #div(@x,@y) filter(@p,@l) -> filter#1(@l,@p) filter#1(::(@x,@xs),@p) -> filter#2(filter(@p,@xs),@p,@x) filter#1(nil(),@p) -> nil() filter#2(@xs',@p,@x) -> filter#3(#equal(mod(@x,@p),#0()),@x,@xs') filter#3(#false(),@x,@xs') -> ::(@x,@xs') filter#3(#true(),@x,@xs') -> @xs' mod(@x,@y) -> -(@x,*(@x,div(@x,@y))) - Signature: {#add/2,#and/2,#div/2,#eq/2,#equal/2,#mult/2,#natdiv/2,#natmult/2,#natsub/2,#pred/1,#sub/2,#succ/1,*/2,-/2 ,div/2,eratos/1,eratos#1/1,filter/2,filter#1/2,filter#2/3,filter#3/3,mod/2,#add#/2,#and#/2,#div#/2,#eq#/2 ,#equal#/2,#mult#/2,#natdiv#/2,#natmult#/2,#natsub#/2,#pred#/1,#sub#/2,#succ#/1,*#/2,-#/2,div#/2,eratos#/1 ,eratos#1#/1,filter#/2,filter#1#/2,filter#2#/3,filter#3#/3,mod#/2} / {#0/0,#divByZero/0,#false/0,#neg/1 ,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/3,c_12/0 ,c_13/0,c_14/3,c_15/0,c_16/1,c_17/2,c_18/1,c_19/2,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0 ,c_28/1,c_29/1,c_30/0,c_31/1,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/1,c_39/0,c_40/0,c_41/0,c_42/1 ,c_43/0,c_44/1,c_45/3,c_46/0,c_47/0,c_48/0,c_49/0,c_50/0,c_51/0,c_52/0,c_53/1,c_54/1,c_55/0,c_56/1,c_57/1 ,c_58/0,c_59/2,c_60/0,c_61/2,c_62/0,c_63/1,c_64/0,c_65/0,c_66/0,c_67/0,c_68/0,c_69/1,c_70/1,c_71/0,c_72/0 ,c_73/0,c_74/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult# ,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3# ,mod#} and constructors {#0,#divByZero,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: filter#(@p,@l) -> c_8(filter#1#(@l,@p)) Consider the set of all dependency pairs 1: filter#(@p,@l) -> c_8(filter#1#(@l,@p)) 2: eratos#(@l) -> c_5(eratos#1#(@l)) 3: eratos#1#(::(@x,@xs)) -> c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)) 4: filter#1#(::(@x,@xs),@p) -> c_9(filter#(@p,@xs)) Processor NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^2)) SPACE(?,?)on application of the dependency pairs {1} These cover all (indirect) predecessors of dependency pairs {1,4} their number of applications is equally bounded. The dependency pairs are shifted into the weak component. **** Step 8.b:1.b:1.a:1: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: filter#(@p,@l) -> c_8(filter#1#(@l,@p)) - Weak DPs: eratos#(@l) -> c_5(eratos#1#(@l)) eratos#1#(::(@x,@xs)) -> c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)) filter#1#(::(@x,@xs),@p) -> c_9(filter#(@p,@xs)) - Weak TRS: #add(#0(),@y) -> @y #add(#neg(#s(#0())),@y) -> #pred(@y) #add(#neg(#s(#s(@x))),@y) -> #pred(#add(#pos(#s(@x)),@y)) #add(#pos(#s(#0())),@y) -> #succ(@y) #add(#pos(#s(#s(@x))),@y) -> #succ(#add(#pos(#s(@x)),@y)) #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #div(#0(),#0()) -> #divByZero() #div(#0(),#neg(@y)) -> #0() #div(#0(),#pos(@y)) -> #0() #div(#neg(@x),#0()) -> #divByZero() #div(#neg(@x),#neg(@y)) -> #pos(#natdiv(@x,@y)) #div(#neg(@x),#pos(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#0()) -> #divByZero() #div(#pos(@x),#neg(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#pos(@y)) -> #pos(#natdiv(@x,@y)) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #mult(#0(),#0()) -> #0() #mult(#0(),#neg(@y)) -> #0() #mult(#0(),#pos(@y)) -> #0() #mult(#neg(@x),#0()) -> #0() #mult(#neg(@x),#neg(@y)) -> #pos(#natmult(@x,@y)) #mult(#neg(@x),#pos(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#0()) -> #0() #mult(#pos(@x),#neg(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#pos(@y)) -> #pos(#natmult(@x,@y)) #natdiv(#0(),#0()) -> #divByZero() #natdiv(#s(@x),#s(@y)) -> #s(#natdiv(#natsub(@x,@y),#s(@y))) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@y),#natmult(@x,@y)) #natsub(@x,#0()) -> @x #natsub(#s(@x),#s(@y)) -> #natsub(@x,@y) #pred(#0()) -> #neg(#s(#0())) #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) #pred(#pos(#s(#0()))) -> #0() #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) #sub(@x,#0()) -> @x #sub(@x,#neg(@y)) -> #add(@x,#pos(@y)) #sub(@x,#pos(@y)) -> #add(@x,#neg(@y)) #succ(#0()) -> #pos(#s(#0())) #succ(#neg(#s(#0()))) -> #0() #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) *(@x,@y) -> #mult(@x,@y) -(@x,@y) -> #sub(@x,@y) div(@x,@y) -> #div(@x,@y) filter(@p,@l) -> filter#1(@l,@p) filter#1(::(@x,@xs),@p) -> filter#2(filter(@p,@xs),@p,@x) filter#1(nil(),@p) -> nil() filter#2(@xs',@p,@x) -> filter#3(#equal(mod(@x,@p),#0()),@x,@xs') filter#3(#false(),@x,@xs') -> ::(@x,@xs') filter#3(#true(),@x,@xs') -> @xs' mod(@x,@y) -> -(@x,*(@x,div(@x,@y))) - Signature: {#add/2,#and/2,#div/2,#eq/2,#equal/2,#mult/2,#natdiv/2,#natmult/2,#natsub/2,#pred/1,#sub/2,#succ/1,*/2,-/2 ,div/2,eratos/1,eratos#1/1,filter/2,filter#1/2,filter#2/3,filter#3/3,mod/2,#add#/2,#and#/2,#div#/2,#eq#/2 ,#equal#/2,#mult#/2,#natdiv#/2,#natmult#/2,#natsub#/2,#pred#/1,#sub#/2,#succ#/1,*#/2,-#/2,div#/2,eratos#/1 ,eratos#1#/1,filter#/2,filter#1#/2,filter#2#/3,filter#3#/3,mod#/2} / {#0/0,#divByZero/0,#false/0,#neg/1 ,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/3,c_12/0 ,c_13/0,c_14/3,c_15/0,c_16/1,c_17/2,c_18/1,c_19/2,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0 ,c_28/1,c_29/1,c_30/0,c_31/1,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/1,c_39/0,c_40/0,c_41/0,c_42/1 ,c_43/0,c_44/1,c_45/3,c_46/0,c_47/0,c_48/0,c_49/0,c_50/0,c_51/0,c_52/0,c_53/1,c_54/1,c_55/0,c_56/1,c_57/1 ,c_58/0,c_59/2,c_60/0,c_61/2,c_62/0,c_63/1,c_64/0,c_65/0,c_66/0,c_67/0,c_68/0,c_69/1,c_70/1,c_71/0,c_72/0 ,c_73/0,c_74/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult# ,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3# ,mod#} and constructors {#0,#divByZero,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_5) = {1}, uargs(c_6) = {1,2}, uargs(c_8) = {1}, uargs(c_9) = {1} Following symbols are considered usable: {filter,filter#1,filter#2,filter#3,#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult#,#natsub# ,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3#,mod#} TcT has computed the following interpretation: p(#0) = [1] [0] p(#add) = [0] [0] p(#and) = [0] [0] p(#div) = [0 0] x1 + [0] [1 0] [1] p(#divByZero) = [0] [0] p(#eq) = [0 0] x1 + [0] [1 0] [0] p(#equal) = [1 0] x2 + [1] [0 0] [1] p(#false) = [0] [0] p(#mult) = [0] [0] p(#natdiv) = [1 0] x2 + [1] [0 0] [1] p(#natmult) = [1] [0] p(#natsub) = [0 0] x2 + [0] [1 0] [1] p(#neg) = [0] [0] p(#pos) = [0] [0] p(#pred) = [0] [0] p(#s) = [0] [0] p(#sub) = [0] [0] p(#succ) = [0 0] x1 + [0] [1 0] [1] p(#true) = [0] [0] p(*) = [1] [0] p(-) = [0 1] x1 + [1] [0 0] [0] p(::) = [0 0] x1 + [1 1] x2 + [0] [0 1] [0 1] [1] p(div) = [0] [0] p(eratos) = [0] [0] p(eratos#1) = [0] [0] p(filter) = [1 0] x2 + [0] [0 1] [0] p(filter#1) = [1 0] x1 + [0] [0 1] [0] p(filter#2) = [1 1] x1 + [0 0] x3 + [0] [0 1] [0 1] [1] p(filter#3) = [0 0] x2 + [1 1] x3 + [0] [0 1] [0 1] [1] p(mod) = [0] [0] p(nil) = [0] [0] p(#add#) = [0] [0] p(#and#) = [0] [0] p(#div#) = [0] [0] p(#eq#) = [0] [0] p(#equal#) = [0] [0] p(#mult#) = [0] [0] p(#natdiv#) = [0] [0] p(#natmult#) = [0] [0] p(#natsub#) = [0] [0] p(#pred#) = [0] [0] p(#sub#) = [0] [0] p(#succ#) = [0] [0] p(*#) = [0] [0] p(-#) = [0] [0] p(div#) = [0] [0] p(eratos#) = [1 1] x1 + [0] [0 0] [0] p(eratos#1#) = [1 1] x1 + [0] [1 0] [0] p(filter#) = [0 1] x2 + [1] [0 0] [0] p(filter#1#) = [0 1] x1 + [0 0] x2 + [0] [0 1] [1 1] [1] p(filter#2#) = [0] [0] p(filter#3#) = [0] [0] p(mod#) = [0] [0] p(c_1) = [0] [0] p(c_2) = [0] [0] p(c_3) = [0] [0] p(c_4) = [0] [0] p(c_5) = [1 0] x1 + [0] [0 0] [0] p(c_6) = [1 0] x1 + [1 0] x2 + [0] [1 0] [0 0] [0] p(c_7) = [0] [0] p(c_8) = [1 0] x1 + [0] [0 0] [0] p(c_9) = [1 0] x1 + [0] [0 0] [0] p(c_10) = [0] [0] p(c_11) = [0] [0] p(c_12) = [0] [0] p(c_13) = [0] [0] p(c_14) = [0] [0] p(c_15) = [0] [0] p(c_16) = [0] [0] p(c_17) = [0] [0] p(c_18) = [0] [0] p(c_19) = [0] [0] p(c_20) = [0] [0] p(c_21) = [0] [0] p(c_22) = [0] [0] p(c_23) = [0] [0] p(c_24) = [0] [0] p(c_25) = [0] [0] p(c_26) = [0] [0] p(c_27) = [0] [0] p(c_28) = [0] [0] p(c_29) = [0] [0] p(c_30) = [0] [0] p(c_31) = [0] [0] p(c_32) = [0] [0] p(c_33) = [0] [0] p(c_34) = [0] [0] p(c_35) = [0] [0] p(c_36) = [0] [0] p(c_37) = [0] [0] p(c_38) = [0] [0] p(c_39) = [0] [0] p(c_40) = [0] [0] p(c_41) = [0] [0] p(c_42) = [0] [0] p(c_43) = [0] [0] p(c_44) = [0] [0] p(c_45) = [0] [0] p(c_46) = [0] [0] p(c_47) = [0] [0] p(c_48) = [0] [0] p(c_49) = [0] [0] p(c_50) = [0] [0] p(c_51) = [0] [0] p(c_52) = [0] [0] p(c_53) = [0] [0] p(c_54) = [0] [0] p(c_55) = [0] [0] p(c_56) = [0] [0] p(c_57) = [0] [0] p(c_58) = [0] [0] p(c_59) = [0] [0] p(c_60) = [0] [0] p(c_61) = [0] [0] p(c_62) = [0] [0] p(c_63) = [0] [0] p(c_64) = [0] [0] p(c_65) = [0] [0] p(c_66) = [0] [0] p(c_67) = [0] [0] p(c_68) = [0] [0] p(c_69) = [0] [0] p(c_70) = [0] [0] p(c_71) = [0] [0] p(c_72) = [0] [0] p(c_73) = [0] [0] p(c_74) = [0] [0] Following rules are strictly oriented: filter#(@p,@l) = [0 1] @l + [1] [0 0] [0] > [0 1] @l + [0] [0 0] [0] = c_8(filter#1#(@l,@p)) Following rules are (at-least) weakly oriented: eratos#(@l) = [1 1] @l + [0] [0 0] [0] >= [1 1] @l + [0] [0 0] [0] = c_5(eratos#1#(@l)) eratos#1#(::(@x,@xs)) = [0 1] @x + [1 2] @xs + [1] [0 0] [1 1] [0] >= [1 2] @xs + [1] [1 1] [0] = c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)) filter#1#(::(@x,@xs),@p) = [0 0] @p + [0 1] @x + [0 1] @xs + [1] [1 1] [0 1] [0 1] [2] >= [0 1] @xs + [1] [0 0] [0] = c_9(filter#(@p,@xs)) filter(@p,@l) = [1 0] @l + [0] [0 1] [0] >= [1 0] @l + [0] [0 1] [0] = filter#1(@l,@p) filter#1(::(@x,@xs),@p) = [0 0] @x + [1 1] @xs + [0] [0 1] [0 1] [1] >= [0 0] @x + [1 1] @xs + [0] [0 1] [0 1] [1] = filter#2(filter(@p,@xs),@p,@x) filter#1(nil(),@p) = [0] [0] >= [0] [0] = nil() filter#2(@xs',@p,@x) = [0 0] @x + [1 1] @xs' + [0] [0 1] [0 1] [1] >= [0 0] @x + [1 1] @xs' + [0] [0 1] [0 1] [1] = filter#3(#equal(mod(@x,@p),#0()),@x,@xs') filter#3(#false(),@x,@xs') = [0 0] @x + [1 1] @xs' + [0] [0 1] [0 1] [1] >= [0 0] @x + [1 1] @xs' + [0] [0 1] [0 1] [1] = ::(@x,@xs') filter#3(#true(),@x,@xs') = [0 0] @x + [1 1] @xs' + [0] [0 1] [0 1] [1] >= [1 0] @xs' + [0] [0 1] [0] = @xs' **** Step 8.b:1.b:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: eratos#(@l) -> c_5(eratos#1#(@l)) eratos#1#(::(@x,@xs)) -> c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)) filter#(@p,@l) -> c_8(filter#1#(@l,@p)) filter#1#(::(@x,@xs),@p) -> c_9(filter#(@p,@xs)) - Weak TRS: #add(#0(),@y) -> @y #add(#neg(#s(#0())),@y) -> #pred(@y) #add(#neg(#s(#s(@x))),@y) -> #pred(#add(#pos(#s(@x)),@y)) #add(#pos(#s(#0())),@y) -> #succ(@y) #add(#pos(#s(#s(@x))),@y) -> #succ(#add(#pos(#s(@x)),@y)) #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #div(#0(),#0()) -> #divByZero() #div(#0(),#neg(@y)) -> #0() #div(#0(),#pos(@y)) -> #0() #div(#neg(@x),#0()) -> #divByZero() #div(#neg(@x),#neg(@y)) -> #pos(#natdiv(@x,@y)) #div(#neg(@x),#pos(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#0()) -> #divByZero() #div(#pos(@x),#neg(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#pos(@y)) -> #pos(#natdiv(@x,@y)) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #mult(#0(),#0()) -> #0() #mult(#0(),#neg(@y)) -> #0() #mult(#0(),#pos(@y)) -> #0() #mult(#neg(@x),#0()) -> #0() #mult(#neg(@x),#neg(@y)) -> #pos(#natmult(@x,@y)) #mult(#neg(@x),#pos(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#0()) -> #0() #mult(#pos(@x),#neg(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#pos(@y)) -> #pos(#natmult(@x,@y)) #natdiv(#0(),#0()) -> #divByZero() #natdiv(#s(@x),#s(@y)) -> #s(#natdiv(#natsub(@x,@y),#s(@y))) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@y),#natmult(@x,@y)) #natsub(@x,#0()) -> @x #natsub(#s(@x),#s(@y)) -> #natsub(@x,@y) #pred(#0()) -> #neg(#s(#0())) #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) #pred(#pos(#s(#0()))) -> #0() #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) #sub(@x,#0()) -> @x #sub(@x,#neg(@y)) -> #add(@x,#pos(@y)) #sub(@x,#pos(@y)) -> #add(@x,#neg(@y)) #succ(#0()) -> #pos(#s(#0())) #succ(#neg(#s(#0()))) -> #0() #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) *(@x,@y) -> #mult(@x,@y) -(@x,@y) -> #sub(@x,@y) div(@x,@y) -> #div(@x,@y) filter(@p,@l) -> filter#1(@l,@p) filter#1(::(@x,@xs),@p) -> filter#2(filter(@p,@xs),@p,@x) filter#1(nil(),@p) -> nil() filter#2(@xs',@p,@x) -> filter#3(#equal(mod(@x,@p),#0()),@x,@xs') filter#3(#false(),@x,@xs') -> ::(@x,@xs') filter#3(#true(),@x,@xs') -> @xs' mod(@x,@y) -> -(@x,*(@x,div(@x,@y))) - Signature: {#add/2,#and/2,#div/2,#eq/2,#equal/2,#mult/2,#natdiv/2,#natmult/2,#natsub/2,#pred/1,#sub/2,#succ/1,*/2,-/2 ,div/2,eratos/1,eratos#1/1,filter/2,filter#1/2,filter#2/3,filter#3/3,mod/2,#add#/2,#and#/2,#div#/2,#eq#/2 ,#equal#/2,#mult#/2,#natdiv#/2,#natmult#/2,#natsub#/2,#pred#/1,#sub#/2,#succ#/1,*#/2,-#/2,div#/2,eratos#/1 ,eratos#1#/1,filter#/2,filter#1#/2,filter#2#/3,filter#3#/3,mod#/2} / {#0/0,#divByZero/0,#false/0,#neg/1 ,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/3,c_12/0 ,c_13/0,c_14/3,c_15/0,c_16/1,c_17/2,c_18/1,c_19/2,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0 ,c_28/1,c_29/1,c_30/0,c_31/1,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/1,c_39/0,c_40/0,c_41/0,c_42/1 ,c_43/0,c_44/1,c_45/3,c_46/0,c_47/0,c_48/0,c_49/0,c_50/0,c_51/0,c_52/0,c_53/1,c_54/1,c_55/0,c_56/1,c_57/1 ,c_58/0,c_59/2,c_60/0,c_61/2,c_62/0,c_63/1,c_64/0,c_65/0,c_66/0,c_67/0,c_68/0,c_69/1,c_70/1,c_71/0,c_72/0 ,c_73/0,c_74/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult# ,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3# ,mod#} and constructors {#0,#divByZero,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () **** Step 8.b:1.b:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: eratos#(@l) -> c_5(eratos#1#(@l)) eratos#1#(::(@x,@xs)) -> c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)) filter#(@p,@l) -> c_8(filter#1#(@l,@p)) filter#1#(::(@x,@xs),@p) -> c_9(filter#(@p,@xs)) - Weak TRS: #add(#0(),@y) -> @y #add(#neg(#s(#0())),@y) -> #pred(@y) #add(#neg(#s(#s(@x))),@y) -> #pred(#add(#pos(#s(@x)),@y)) #add(#pos(#s(#0())),@y) -> #succ(@y) #add(#pos(#s(#s(@x))),@y) -> #succ(#add(#pos(#s(@x)),@y)) #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #div(#0(),#0()) -> #divByZero() #div(#0(),#neg(@y)) -> #0() #div(#0(),#pos(@y)) -> #0() #div(#neg(@x),#0()) -> #divByZero() #div(#neg(@x),#neg(@y)) -> #pos(#natdiv(@x,@y)) #div(#neg(@x),#pos(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#0()) -> #divByZero() #div(#pos(@x),#neg(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#pos(@y)) -> #pos(#natdiv(@x,@y)) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #mult(#0(),#0()) -> #0() #mult(#0(),#neg(@y)) -> #0() #mult(#0(),#pos(@y)) -> #0() #mult(#neg(@x),#0()) -> #0() #mult(#neg(@x),#neg(@y)) -> #pos(#natmult(@x,@y)) #mult(#neg(@x),#pos(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#0()) -> #0() #mult(#pos(@x),#neg(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#pos(@y)) -> #pos(#natmult(@x,@y)) #natdiv(#0(),#0()) -> #divByZero() #natdiv(#s(@x),#s(@y)) -> #s(#natdiv(#natsub(@x,@y),#s(@y))) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@y),#natmult(@x,@y)) #natsub(@x,#0()) -> @x #natsub(#s(@x),#s(@y)) -> #natsub(@x,@y) #pred(#0()) -> #neg(#s(#0())) #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) #pred(#pos(#s(#0()))) -> #0() #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) #sub(@x,#0()) -> @x #sub(@x,#neg(@y)) -> #add(@x,#pos(@y)) #sub(@x,#pos(@y)) -> #add(@x,#neg(@y)) #succ(#0()) -> #pos(#s(#0())) #succ(#neg(#s(#0()))) -> #0() #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) *(@x,@y) -> #mult(@x,@y) -(@x,@y) -> #sub(@x,@y) div(@x,@y) -> #div(@x,@y) filter(@p,@l) -> filter#1(@l,@p) filter#1(::(@x,@xs),@p) -> filter#2(filter(@p,@xs),@p,@x) filter#1(nil(),@p) -> nil() filter#2(@xs',@p,@x) -> filter#3(#equal(mod(@x,@p),#0()),@x,@xs') filter#3(#false(),@x,@xs') -> ::(@x,@xs') filter#3(#true(),@x,@xs') -> @xs' mod(@x,@y) -> -(@x,*(@x,div(@x,@y))) - Signature: {#add/2,#and/2,#div/2,#eq/2,#equal/2,#mult/2,#natdiv/2,#natmult/2,#natsub/2,#pred/1,#sub/2,#succ/1,*/2,-/2 ,div/2,eratos/1,eratos#1/1,filter/2,filter#1/2,filter#2/3,filter#3/3,mod/2,#add#/2,#and#/2,#div#/2,#eq#/2 ,#equal#/2,#mult#/2,#natdiv#/2,#natmult#/2,#natsub#/2,#pred#/1,#sub#/2,#succ#/1,*#/2,-#/2,div#/2,eratos#/1 ,eratos#1#/1,filter#/2,filter#1#/2,filter#2#/3,filter#3#/3,mod#/2} / {#0/0,#divByZero/0,#false/0,#neg/1 ,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/3,c_12/0 ,c_13/0,c_14/3,c_15/0,c_16/1,c_17/2,c_18/1,c_19/2,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0 ,c_28/1,c_29/1,c_30/0,c_31/1,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/1,c_39/0,c_40/0,c_41/0,c_42/1 ,c_43/0,c_44/1,c_45/3,c_46/0,c_47/0,c_48/0,c_49/0,c_50/0,c_51/0,c_52/0,c_53/1,c_54/1,c_55/0,c_56/1,c_57/1 ,c_58/0,c_59/2,c_60/0,c_61/2,c_62/0,c_63/1,c_64/0,c_65/0,c_66/0,c_67/0,c_68/0,c_69/1,c_70/1,c_71/0,c_72/0 ,c_73/0,c_74/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult# ,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3# ,mod#} and constructors {#0,#divByZero,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:eratos#(@l) -> c_5(eratos#1#(@l)) -->_1 eratos#1#(::(@x,@xs)) -> c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)):2 2:W:eratos#1#(::(@x,@xs)) -> c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)) -->_2 filter#(@p,@l) -> c_8(filter#1#(@l,@p)):3 -->_1 eratos#(@l) -> c_5(eratos#1#(@l)):1 3:W:filter#(@p,@l) -> c_8(filter#1#(@l,@p)) -->_1 filter#1#(::(@x,@xs),@p) -> c_9(filter#(@p,@xs)):4 4:W:filter#1#(::(@x,@xs),@p) -> c_9(filter#(@p,@xs)) -->_1 filter#(@p,@l) -> c_8(filter#1#(@l,@p)):3 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: eratos#(@l) -> c_5(eratos#1#(@l)) 2: eratos#1#(::(@x,@xs)) -> c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs)) 3: filter#(@p,@l) -> c_8(filter#1#(@l,@p)) 4: filter#1#(::(@x,@xs),@p) -> c_9(filter#(@p,@xs)) **** Step 8.b:1.b:1.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: #add(#0(),@y) -> @y #add(#neg(#s(#0())),@y) -> #pred(@y) #add(#neg(#s(#s(@x))),@y) -> #pred(#add(#pos(#s(@x)),@y)) #add(#pos(#s(#0())),@y) -> #succ(@y) #add(#pos(#s(#s(@x))),@y) -> #succ(#add(#pos(#s(@x)),@y)) #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #div(#0(),#0()) -> #divByZero() #div(#0(),#neg(@y)) -> #0() #div(#0(),#pos(@y)) -> #0() #div(#neg(@x),#0()) -> #divByZero() #div(#neg(@x),#neg(@y)) -> #pos(#natdiv(@x,@y)) #div(#neg(@x),#pos(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#0()) -> #divByZero() #div(#pos(@x),#neg(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#pos(@y)) -> #pos(#natdiv(@x,@y)) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #mult(#0(),#0()) -> #0() #mult(#0(),#neg(@y)) -> #0() #mult(#0(),#pos(@y)) -> #0() #mult(#neg(@x),#0()) -> #0() #mult(#neg(@x),#neg(@y)) -> #pos(#natmult(@x,@y)) #mult(#neg(@x),#pos(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#0()) -> #0() #mult(#pos(@x),#neg(@y)) -> #neg(#natmult(@x,@y)) #mult(#pos(@x),#pos(@y)) -> #pos(#natmult(@x,@y)) #natdiv(#0(),#0()) -> #divByZero() #natdiv(#s(@x),#s(@y)) -> #s(#natdiv(#natsub(@x,@y),#s(@y))) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@y),#natmult(@x,@y)) #natsub(@x,#0()) -> @x #natsub(#s(@x),#s(@y)) -> #natsub(@x,@y) #pred(#0()) -> #neg(#s(#0())) #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) #pred(#pos(#s(#0()))) -> #0() #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) #sub(@x,#0()) -> @x #sub(@x,#neg(@y)) -> #add(@x,#pos(@y)) #sub(@x,#pos(@y)) -> #add(@x,#neg(@y)) #succ(#0()) -> #pos(#s(#0())) #succ(#neg(#s(#0()))) -> #0() #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) *(@x,@y) -> #mult(@x,@y) -(@x,@y) -> #sub(@x,@y) div(@x,@y) -> #div(@x,@y) filter(@p,@l) -> filter#1(@l,@p) filter#1(::(@x,@xs),@p) -> filter#2(filter(@p,@xs),@p,@x) filter#1(nil(),@p) -> nil() filter#2(@xs',@p,@x) -> filter#3(#equal(mod(@x,@p),#0()),@x,@xs') filter#3(#false(),@x,@xs') -> ::(@x,@xs') filter#3(#true(),@x,@xs') -> @xs' mod(@x,@y) -> -(@x,*(@x,div(@x,@y))) - Signature: {#add/2,#and/2,#div/2,#eq/2,#equal/2,#mult/2,#natdiv/2,#natmult/2,#natsub/2,#pred/1,#sub/2,#succ/1,*/2,-/2 ,div/2,eratos/1,eratos#1/1,filter/2,filter#1/2,filter#2/3,filter#3/3,mod/2,#add#/2,#and#/2,#div#/2,#eq#/2 ,#equal#/2,#mult#/2,#natdiv#/2,#natmult#/2,#natsub#/2,#pred#/1,#sub#/2,#succ#/1,*#/2,-#/2,div#/2,eratos#/1 ,eratos#1#/1,filter#/2,filter#1#/2,filter#2#/3,filter#3#/3,mod#/2} / {#0/0,#divByZero/0,#false/0,#neg/1 ,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/2,c_7/0,c_8/1,c_9/1,c_10/0,c_11/3,c_12/0 ,c_13/0,c_14/3,c_15/0,c_16/1,c_17/2,c_18/1,c_19/2,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0 ,c_28/1,c_29/1,c_30/0,c_31/1,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/1,c_39/0,c_40/0,c_41/0,c_42/1 ,c_43/0,c_44/1,c_45/3,c_46/0,c_47/0,c_48/0,c_49/0,c_50/0,c_51/0,c_52/0,c_53/1,c_54/1,c_55/0,c_56/1,c_57/1 ,c_58/0,c_59/2,c_60/0,c_61/2,c_62/0,c_63/1,c_64/0,c_65/0,c_66/0,c_67/0,c_68/0,c_69/1,c_70/1,c_71/0,c_72/0 ,c_73/0,c_74/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult# ,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3# ,mod#} and constructors {#0,#divByZero,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^2))