*** 1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
#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 DP Rules:
Weak TRS 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()
#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
basic terms: {#add,#and,#div,#eq,#equal,#mult,#natdiv,#natmult,#natsub,#pred,#sub,#succ,*,-,div,eratos,eratos#1,filter,filter#1,filter#2,filter#3,mod}/{#0,#divByZero,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
DependencyPairs {dpKind_ = DT}
Proof:
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.
*** 1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
#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))
Strict TRS Rules:
Weak DP Rules:
#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 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)
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
basic terms: {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult#,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3#,mod#}/{#0,#divByZero,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
UsableRules
Proof:
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))
*** 1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
#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))
Strict TRS Rules:
Weak DP Rules:
#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 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)))
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
basic terms: {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult#,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3#,mod#}/{#0,#divByZero,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
Proof:
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()
*** 1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
#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 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)))
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
basic terms: {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult#,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3#,mod#}/{#0,#divByZero,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
Proof:
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()
*** 1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
#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 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)))
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
basic terms: {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult#,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3#,mod#}/{#0,#divByZero,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
Proof:
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))
*** 1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
#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 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)))
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
basic terms: {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult#,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3#,mod#}/{#0,#divByZero,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
RemoveWeakSuffixes
Proof:
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()
*** 1.1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
Weak TRS 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)))
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
basic terms: {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult#,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3#,mod#}/{#0,#divByZero,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
SimplifyRHS
Proof:
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))
*** 1.1.1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
Weak TRS 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)))
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
basic terms: {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult#,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3#,mod#}/{#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, greedy = NoGreedy}}
Proof:
We first use the processor NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} 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.
*** 1.1.1.1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
Weak TRS 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)))
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
basic terms: {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult#,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3#,mod#}/{#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 any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
Proof:
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]
[1]
p(#add) = [0 1] x2 + [0]
[1 0] [1]
p(#and) = [0 0] x1 + [1 1] x2 + [1]
[1 1] [1 0] [0]
p(#div) = [1 1] x1 + [1]
[1 0] [0]
p(#divByZero) = [0]
[0]
p(#eq) = [1 0] x1 + [0]
[0 0] [0]
p(#equal) = [0 0] x2 + [1]
[0 1] [0]
p(#false) = [0]
[0]
p(#mult) = [0 1] x1 + [1 0] x2 + [1]
[0 0] [0 0] [0]
p(#natdiv) = [0 0] x1 + [0]
[1 1] [1]
p(#natmult) = [0 1] x1 + [1]
[0 0] [1]
p(#natsub) = [0 0] x2 + [0]
[0 1] [1]
p(#neg) = [0 1] x1 + [0]
[0 0] [0]
p(#pos) = [0]
[0]
p(#pred) = [0]
[1]
p(#s) = [0]
[0]
p(#sub) = [0]
[0]
p(#succ) = [0]
[0]
p(#true) = [1]
[1]
p(*) = [1 0] x2 + [1]
[1 1] [1]
p(-) = [0 0] x1 + [0 0] x2 + [0]
[1 0] [0 1] [0]
p(::) = [1 1] x2 + [0]
[0 1] [1]
p(div) = [0 1] x1 + [1]
[1 1] [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 1] [1]
p(filter#3) = [1 1] x3 + [0]
[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 0] x1 + [0]
[0 1] [1]
p(eratos#1#) = [1 0] x1 + [0]
[0 1] [1]
p(filter#) = [0 1] x2 + [0]
[1 0] [0]
p(filter#1#) = [0 1] x1 + [0]
[1 0] [0]
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]
[0 1] [0 0] [1]
p(c_7) = [0]
[0]
p(c_8) = [1 0] x1 + [0]
[0 1] [0]
p(c_9) = [1 0] x1 + [0]
[0 1] [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] @xs + [1]
[1 1] [0]
> [0 1] @xs + [0]
[1 0] [0]
= c_9(filter#(@p,@xs))
Following rules are (at-least) weakly oriented:
eratos#(@l) = [1 0] @l + [0]
[0 1] [1]
>= [1 0] @l + [0]
[0 0] [0]
= c_5(eratos#1#(@l))
eratos#1#(::(@x,@xs)) = [1 1] @xs + [0]
[0 1] [2]
>= [1 1] @xs + [0]
[0 1] [2]
= c_6(eratos#(filter(@x,@xs))
,filter#(@x,@xs))
filter#(@p,@l) = [0 1] @l + [0]
[1 0] [0]
>= [0 1] @l + [0]
[1 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 1] @xs + [0]
[0 1] [1]
>= [1 1] @xs + [0]
[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 1] @xs' + [0]
[0 1] [1]
>= [1 1] @xs' + [0]
[0 1] [1]
= filter#3(#equal(mod(@x,@p),#0())
,@x
,@xs')
filter#3(#false(),@x,@xs') = [1 1] @xs' + [0]
[0 1] [1]
>= [1 1] @xs' + [0]
[0 1] [1]
= ::(@x,@xs')
filter#3(#true(),@x,@xs') = [1 1] @xs' + [0]
[0 1] [1]
>= [1 0] @xs' + [0]
[0 1] [0]
= @xs'
*** 1.1.1.1.1.1.1.1.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
filter#1#(::(@x,@xs),@p) -> c_9(filter#(@p,@xs))
Weak TRS 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)))
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
basic terms: {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult#,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3#,mod#}/{#0,#divByZero,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.1.1.1.2 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
filter#1#(::(@x,@xs),@p) -> c_9(filter#(@p,@xs))
Weak TRS 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)))
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
basic terms: {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult#,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3#,mod#}/{#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, greedy = NoGreedy}}
Proof:
We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} 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, greedy = NoGreedy}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.
*** 1.1.1.1.1.1.1.1.2.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
filter#1#(::(@x,@xs),@p) -> c_9(filter#(@p,@xs))
Weak TRS 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)))
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
basic terms: {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult#,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3#,mod#}/{#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 any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
Proof:
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) = [2]
p(#add) = [1] x1 + [1] x2 + [7]
p(#and) = [2] x1 + [6] x2 + [5]
p(#div) = [1] x1 + [0]
p(#divByZero) = [1]
p(#eq) = [0]
p(#equal) = [1] x2 + [2]
p(#false) = [0]
p(#mult) = [3]
p(#natdiv) = [3]
p(#natmult) = [4] x1 + [2] x2 + [0]
p(#natsub) = [2] x2 + [3]
p(#neg) = [0]
p(#pos) = [5]
p(#pred) = [4]
p(#s) = [1]
p(#sub) = [2] x2 + [1]
p(#succ) = [6]
p(#true) = [1]
p(*) = [6] x1 + [1] x2 + [0]
p(-) = [1] x2 + [6]
p(::) = [1] x2 + [4]
p(div) = [7] x1 + [4] x2 + [5]
p(eratos) = [0]
p(eratos#1) = [0]
p(filter) = [1] x2 + [1]
p(filter#1) = [1] x1 + [1]
p(filter#2) = [1] x1 + [4]
p(filter#3) = [1] x3 + [4]
p(mod) = [4] x2 + [4]
p(nil) = [0]
p(#add#) = [0]
p(#and#) = [2] x2 + [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#) = [0]
p(eratos#) = [1] x1 + [7]
p(eratos#1#) = [1] x1 + [4]
p(filter#) = [0]
p(filter#1#) = [0]
p(filter#2#) = [0]
p(filter#3#) = [1] x2 + [0]
p(mod#) = [0]
p(c_1) = [0]
p(c_2) = [0]
p(c_3) = [0]
p(c_4) = [4] x1 + [0]
p(c_5) = [1] x1 + [0]
p(c_6) = [1] x1 + [1] x2 + [0]
p(c_7) = [0]
p(c_8) = [4] x1 + [0]
p(c_9) = [4] x1 + [0]
p(c_10) = [0]
p(c_11) = [1] x1 + [1] x2 + [1] x3 + [0]
p(c_12) = [0]
p(c_13) = [0]
p(c_14) = [2] x1 + [0]
p(c_15) = [0]
p(c_16) = [1] x1 + [0]
p(c_17) = [1] x2 + [0]
p(c_18) = [0]
p(c_19) = [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) = [1]
p(c_27) = [0]
p(c_28) = [2] x1 + [0]
p(c_29) = [0]
p(c_30) = [0]
p(c_31) = [0]
p(c_32) = [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) = [4] 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) = [2]
p(c_53) = [2] x1 + [0]
p(c_54) = [1] x1 + [0]
p(c_55) = [0]
p(c_56) = [0]
p(c_57) = [2] x1 + [0]
p(c_58) = [0]
p(c_59) = [1] x1 + [1] x2 + [0]
p(c_60) = [0]
p(c_61) = [4] x1 + [1] x2 + [0]
p(c_62) = [0]
p(c_63) = [2] x1 + [0]
p(c_64) = [0]
p(c_65) = [2]
p(c_66) = [0]
p(c_67) = [0]
p(c_68) = [0]
p(c_69) = [1] x1 + [0]
p(c_70) = [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 + [7]
> [1] @l + [4]
= c_5(eratos#1#(@l))
Following rules are (at-least) weakly oriented:
eratos#1#(::(@x,@xs)) = [1] @xs + [8]
>= [1] @xs + [8]
= 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 + [1]
>= [1] @l + [1]
= filter#1(@l,@p)
filter#1(::(@x,@xs),@p) = [1] @xs + [5]
>= [1] @xs + [5]
= filter#2(filter(@p,@xs),@p,@x)
filter#1(nil(),@p) = [1]
>= [0]
= nil()
filter#2(@xs',@p,@x) = [1] @xs' + [4]
>= [1] @xs' + [4]
= filter#3(#equal(mod(@x,@p),#0())
,@x
,@xs')
filter#3(#false(),@x,@xs') = [1] @xs' + [4]
>= [1] @xs' + [4]
= ::(@x,@xs')
filter#3(#true(),@x,@xs') = [1] @xs' + [4]
>= [1] @xs' + [0]
= @xs'
*** 1.1.1.1.1.1.1.1.2.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
eratos#1#(::(@x,@xs)) -> c_6(eratos#(filter(@x,@xs)),filter#(@x,@xs))
filter#(@p,@l) -> c_8(filter#1#(@l,@p))
Strict TRS Rules:
Weak DP Rules:
eratos#(@l) -> c_5(eratos#1#(@l))
filter#1#(::(@x,@xs),@p) -> c_9(filter#(@p,@xs))
Weak TRS 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)))
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
basic terms: {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult#,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3#,mod#}/{#0,#divByZero,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.1.1.1.2.2 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
filter#(@p,@l) -> c_8(filter#1#(@l,@p))
Strict TRS Rules:
Weak DP Rules:
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 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)))
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
basic terms: {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult#,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3#,mod#}/{#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, greedy = NoGreedy}}
Proof:
We first use the processor NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} 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, greedy = NoGreedy}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.
*** 1.1.1.1.1.1.1.1.2.2.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
filter#(@p,@l) -> c_8(filter#1#(@l,@p))
Strict TRS Rules:
Weak DP Rules:
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 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)))
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
basic terms: {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult#,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3#,mod#}/{#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 any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
Proof:
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]
[0]
p(#add) = [0 0] x1 + [0]
[1 0] [0]
p(#and) = [0]
[0]
p(#div) = [1 0] x1 + [0 0] x2 + [1]
[1 0] [1 0] [0]
p(#divByZero) = [0]
[0]
p(#eq) = [0]
[0]
p(#equal) = [1 1] x1 + [1]
[1 1] [1]
p(#false) = [0]
[0]
p(#mult) = [1 0] x1 + [0 0] x2 + [0]
[1 0] [1 0] [0]
p(#natdiv) = [0 0] x2 + [1]
[1 0] [0]
p(#natmult) = [0 0] x1 + [0 0] x2 + [1]
[1 0] [1 0] [1]
p(#natsub) = [0]
[0]
p(#neg) = [0]
[0]
p(#pos) = [1 1] x1 + [1]
[0 0] [0]
p(#pred) = [0]
[1]
p(#s) = [1 0] x1 + [1]
[0 0] [0]
p(#sub) = [0]
[0]
p(#succ) = [0]
[0]
p(#true) = [0]
[0]
p(*) = [0 0] x1 + [0 1] x2 + [0]
[1 0] [1 0] [1]
p(-) = [0 1] x2 + [0]
[0 0] [0]
p(::) = [1 1] x1 + [1 1] x2 + [0]
[0 0] [0 1] [1]
p(div) = [1 0] x1 + [0 0] x2 + [0]
[0 0] [0 1] [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 + [1 1] x3 + [0]
[0 1] [0 0] [1]
p(filter#3) = [1 1] x2 + [1 1] x3 + [0]
[0 0] [0 1] [1]
p(mod) = [0 1] x1 + [1]
[1 0] [1]
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 1] [0]
p(eratos#1#) = [1 1] x1 + [0]
[0 0] [0]
p(filter#) = [0 0] x1 + [0 1] x2 + [1]
[1 1] [0 0] [0]
p(filter#1#) = [0 1] x1 + [0]
[0 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 1] x2 + [0]
[0 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]
[1 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 + [0 0] @p + [1]
[0 0] [1 1] [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 1] [0]
>= [1 1] @l + [0]
[0 0] [0]
= c_5(eratos#1#(@l))
eratos#1#(::(@x,@xs)) = [1 1] @x + [1 2] @xs + [1]
[0 0] [0 0] [0]
>= [1 1] @x + [1 2] @xs + [1]
[0 0] [0 0] [0]
= c_6(eratos#(filter(@x,@xs))
,filter#(@x,@xs))
filter#1#(::(@x,@xs),@p) = [0 1] @xs + [1]
[0 1] [2]
>= [0 1] @xs + [1]
[0 1] [1]
= 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) = [1 1] @x + [1 1] @xs + [0]
[0 0] [0 1] [1]
>= [1 1] @x + [1 1] @xs + [0]
[0 0] [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 1] @x + [1 1] @xs' + [0]
[0 0] [0 1] [1]
>= [1 1] @x + [1 1] @xs' + [0]
[0 0] [0 1] [1]
= filter#3(#equal(mod(@x,@p),#0())
,@x
,@xs')
filter#3(#false(),@x,@xs') = [1 1] @x + [1 1] @xs' + [0]
[0 0] [0 1] [1]
>= [1 1] @x + [1 1] @xs' + [0]
[0 0] [0 1] [1]
= ::(@x,@xs')
filter#3(#true(),@x,@xs') = [1 1] @x + [1 1] @xs' + [0]
[0 0] [0 1] [1]
>= [1 0] @xs' + [0]
[0 1] [0]
= @xs'
*** 1.1.1.1.1.1.1.1.2.2.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
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 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)))
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
basic terms: {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult#,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3#,mod#}/{#0,#divByZero,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.1.1.1.2.2.2 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
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 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)))
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
basic terms: {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult#,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3#,mod#}/{#0,#divByZero,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
RemoveWeakSuffixes
Proof:
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))
*** 1.1.1.1.1.1.1.1.2.2.2.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS 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)))
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
basic terms: {#add#,#and#,#div#,#eq#,#equal#,#mult#,#natdiv#,#natmult#,#natsub#,#pred#,#sub#,#succ#,*#,-#,div#,eratos#,eratos#1#,filter#,filter#1#,filter#2#,filter#3#,mod#}/{#0,#divByZero,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).