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