0 CpxRelTRS
↳1 RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID), 9 ms)
↳4 CpxWeightedTrs
↳5 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳6 CpxTypedWeightedTrs
↳7 CompletionProof (UPPER BOUND(ID), 0 ms)
↳8 CpxTypedWeightedCompleteTrs
↳9 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 36 ms)
↳10 CpxRNTS
↳11 CompleteCoflocoProof (⇔, 2309 ms)
↳12 BOUNDS(1, n^2)
#equal(@x, @y) → #eq(@x, @y)
*(@x, @y) → #mult(@x, @y)
-(@x, @y) → #sub(@x, @y)
div(@x, @y) → #div(@x, @y)
eratos(@l) → eratos#1(@l)
eratos#1(::(@x, @xs)) → ::(@x, eratos(filter(@x, @xs)))
eratos#1(nil) → nil
filter(@p, @l) → filter#1(@l, @p)
filter#1(::(@x, @xs), @p) → filter#2(filter(@p, @xs), @p, @x)
filter#1(nil, @p) → nil
filter#2(@xs', @p, @x) → filter#3(#equal(mod(@x, @p), #0), @x, @xs')
filter#3(#false, @x, @xs') → ::(@x, @xs')
filter#3(#true, @x, @xs') → @xs'
mod(@x, @y) → -(@x, *(@x, div(@x, @y)))
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#div(#0, #0) → #divByZero
#div(#0, #neg(@y)) → #0
#div(#0, #pos(@y)) → #0
#div(#neg(@x), #0) → #divByZero
#div(#neg(@x), #neg(@y)) → #pos(#natdiv(@x, @y))
#div(#neg(@x), #pos(@y)) → #neg(#natdiv(@x, @y))
#div(#pos(@x), #0) → #divByZero
#div(#pos(@x), #neg(@y)) → #neg(#natdiv(@x, @y))
#div(#pos(@x), #pos(@y)) → #pos(#natdiv(@x, @y))
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), nil) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, nil) → #true
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natdiv(#0, #0) → #divByZero
#natdiv(#s(@x), #s(@y)) → #s(#natdiv(#natsub(@x, @y), #s(@y)))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#natsub(@x, #0) → @x
#natsub(#s(@x), #s(@y)) → #natsub(@x, @y)
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#sub(@x, #0) → @x
#sub(@x, #neg(@y)) → #add(@x, #pos(@y))
#sub(@x, #pos(@y)) → #add(@x, #neg(@y))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))
#equal(@x, @y) → #eq(@x, @y) [1]
*(@x, @y) → #mult(@x, @y) [1]
-(@x, @y) → #sub(@x, @y) [1]
div(@x, @y) → #div(@x, @y) [1]
eratos(@l) → eratos#1(@l) [1]
eratos#1(::(@x, @xs)) → ::(@x, eratos(filter(@x, @xs))) [1]
eratos#1(nil) → nil [1]
filter(@p, @l) → filter#1(@l, @p) [1]
filter#1(::(@x, @xs), @p) → filter#2(filter(@p, @xs), @p, @x) [1]
filter#1(nil, @p) → nil [1]
filter#2(@xs', @p, @x) → filter#3(#equal(mod(@x, @p), #0), @x, @xs') [1]
filter#3(#false, @x, @xs') → ::(@x, @xs') [1]
filter#3(#true, @x, @xs') → @xs' [1]
mod(@x, @y) → -(@x, *(@x, div(@x, @y))) [1]
#add(#0, @y) → @y [0]
#add(#neg(#s(#0)), @y) → #pred(@y) [0]
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y)) [0]
#add(#pos(#s(#0)), @y) → #succ(@y) [0]
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y)) [0]
#and(#false, #false) → #false [0]
#and(#false, #true) → #false [0]
#and(#true, #false) → #false [0]
#and(#true, #true) → #true [0]
#div(#0, #0) → #divByZero [0]
#div(#0, #neg(@y)) → #0 [0]
#div(#0, #pos(@y)) → #0 [0]
#div(#neg(@x), #0) → #divByZero [0]
#div(#neg(@x), #neg(@y)) → #pos(#natdiv(@x, @y)) [0]
#div(#neg(@x), #pos(@y)) → #neg(#natdiv(@x, @y)) [0]
#div(#pos(@x), #0) → #divByZero [0]
#div(#pos(@x), #neg(@y)) → #neg(#natdiv(@x, @y)) [0]
#div(#pos(@x), #pos(@y)) → #pos(#natdiv(@x, @y)) [0]
#eq(#0, #0) → #true [0]
#eq(#0, #neg(@y)) → #false [0]
#eq(#0, #pos(@y)) → #false [0]
#eq(#0, #s(@y)) → #false [0]
#eq(#neg(@x), #0) → #false [0]
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y) [0]
#eq(#neg(@x), #pos(@y)) → #false [0]
#eq(#pos(@x), #0) → #false [0]
#eq(#pos(@x), #neg(@y)) → #false [0]
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y) [0]
#eq(#s(@x), #0) → #false [0]
#eq(#s(@x), #s(@y)) → #eq(@x, @y) [0]
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) [0]
#eq(::(@x_1, @x_2), nil) → #false [0]
#eq(nil, ::(@y_1, @y_2)) → #false [0]
#eq(nil, nil) → #true [0]
#mult(#0, #0) → #0 [0]
#mult(#0, #neg(@y)) → #0 [0]
#mult(#0, #pos(@y)) → #0 [0]
#mult(#neg(@x), #0) → #0 [0]
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y)) [0]
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y)) [0]
#mult(#pos(@x), #0) → #0 [0]
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y)) [0]
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y)) [0]
#natdiv(#0, #0) → #divByZero [0]
#natdiv(#s(@x), #s(@y)) → #s(#natdiv(#natsub(@x, @y), #s(@y))) [0]
#natmult(#0, @y) → #0 [0]
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y)) [0]
#natsub(@x, #0) → @x [0]
#natsub(#s(@x), #s(@y)) → #natsub(@x, @y) [0]
#pred(#0) → #neg(#s(#0)) [0]
#pred(#neg(#s(@x))) → #neg(#s(#s(@x))) [0]
#pred(#pos(#s(#0))) → #0 [0]
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x)) [0]
#sub(@x, #0) → @x [0]
#sub(@x, #neg(@y)) → #add(@x, #pos(@y)) [0]
#sub(@x, #pos(@y)) → #add(@x, #neg(@y)) [0]
#succ(#0) → #pos(#s(#0)) [0]
#succ(#neg(#s(#0))) → #0 [0]
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x)) [0]
#succ(#pos(#s(@x))) → #pos(#s(#s(@x))) [0]
| * => times |
| - => minus |
#equal(@x, @y) → #eq(@x, @y) [1]
times(@x, @y) → #mult(@x, @y) [1]
minus(@x, @y) → #sub(@x, @y) [1]
div(@x, @y) → #div(@x, @y) [1]
eratos(@l) → eratos#1(@l) [1]
eratos#1(::(@x, @xs)) → ::(@x, eratos(filter(@x, @xs))) [1]
eratos#1(nil) → nil [1]
filter(@p, @l) → filter#1(@l, @p) [1]
filter#1(::(@x, @xs), @p) → filter#2(filter(@p, @xs), @p, @x) [1]
filter#1(nil, @p) → nil [1]
filter#2(@xs', @p, @x) → filter#3(#equal(mod(@x, @p), #0), @x, @xs') [1]
filter#3(#false, @x, @xs') → ::(@x, @xs') [1]
filter#3(#true, @x, @xs') → @xs' [1]
mod(@x, @y) → minus(@x, times(@x, div(@x, @y))) [1]
#add(#0, @y) → @y [0]
#add(#neg(#s(#0)), @y) → #pred(@y) [0]
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y)) [0]
#add(#pos(#s(#0)), @y) → #succ(@y) [0]
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y)) [0]
#and(#false, #false) → #false [0]
#and(#false, #true) → #false [0]
#and(#true, #false) → #false [0]
#and(#true, #true) → #true [0]
#div(#0, #0) → #divByZero [0]
#div(#0, #neg(@y)) → #0 [0]
#div(#0, #pos(@y)) → #0 [0]
#div(#neg(@x), #0) → #divByZero [0]
#div(#neg(@x), #neg(@y)) → #pos(#natdiv(@x, @y)) [0]
#div(#neg(@x), #pos(@y)) → #neg(#natdiv(@x, @y)) [0]
#div(#pos(@x), #0) → #divByZero [0]
#div(#pos(@x), #neg(@y)) → #neg(#natdiv(@x, @y)) [0]
#div(#pos(@x), #pos(@y)) → #pos(#natdiv(@x, @y)) [0]
#eq(#0, #0) → #true [0]
#eq(#0, #neg(@y)) → #false [0]
#eq(#0, #pos(@y)) → #false [0]
#eq(#0, #s(@y)) → #false [0]
#eq(#neg(@x), #0) → #false [0]
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y) [0]
#eq(#neg(@x), #pos(@y)) → #false [0]
#eq(#pos(@x), #0) → #false [0]
#eq(#pos(@x), #neg(@y)) → #false [0]
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y) [0]
#eq(#s(@x), #0) → #false [0]
#eq(#s(@x), #s(@y)) → #eq(@x, @y) [0]
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) [0]
#eq(::(@x_1, @x_2), nil) → #false [0]
#eq(nil, ::(@y_1, @y_2)) → #false [0]
#eq(nil, nil) → #true [0]
#mult(#0, #0) → #0 [0]
#mult(#0, #neg(@y)) → #0 [0]
#mult(#0, #pos(@y)) → #0 [0]
#mult(#neg(@x), #0) → #0 [0]
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y)) [0]
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y)) [0]
#mult(#pos(@x), #0) → #0 [0]
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y)) [0]
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y)) [0]
#natdiv(#0, #0) → #divByZero [0]
#natdiv(#s(@x), #s(@y)) → #s(#natdiv(#natsub(@x, @y), #s(@y))) [0]
#natmult(#0, @y) → #0 [0]
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y)) [0]
#natsub(@x, #0) → @x [0]
#natsub(#s(@x), #s(@y)) → #natsub(@x, @y) [0]
#pred(#0) → #neg(#s(#0)) [0]
#pred(#neg(#s(@x))) → #neg(#s(#s(@x))) [0]
#pred(#pos(#s(#0))) → #0 [0]
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x)) [0]
#sub(@x, #0) → @x [0]
#sub(@x, #neg(@y)) → #add(@x, #pos(@y)) [0]
#sub(@x, #pos(@y)) → #add(@x, #neg(@y)) [0]
#succ(#0) → #pos(#s(#0)) [0]
#succ(#neg(#s(#0))) → #0 [0]
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x)) [0]
#succ(#pos(#s(@x))) → #pos(#s(#s(@x))) [0]
#equal(@x, @y) → #eq(@x, @y) [1]
times(@x, @y) → #mult(@x, @y) [1]
minus(@x, @y) → #sub(@x, @y) [1]
div(@x, @y) → #div(@x, @y) [1]
eratos(@l) → eratos#1(@l) [1]
eratos#1(::(@x, @xs)) → ::(@x, eratos(filter(@x, @xs))) [1]
eratos#1(nil) → nil [1]
filter(@p, @l) → filter#1(@l, @p) [1]
filter#1(::(@x, @xs), @p) → filter#2(filter(@p, @xs), @p, @x) [1]
filter#1(nil, @p) → nil [1]
filter#2(@xs', @p, @x) → filter#3(#equal(mod(@x, @p), #0), @x, @xs') [1]
filter#3(#false, @x, @xs') → ::(@x, @xs') [1]
filter#3(#true, @x, @xs') → @xs' [1]
mod(@x, @y) → minus(@x, times(@x, div(@x, @y))) [1]
#add(#0, @y) → @y [0]
#add(#neg(#s(#0)), @y) → #pred(@y) [0]
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y)) [0]
#add(#pos(#s(#0)), @y) → #succ(@y) [0]
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y)) [0]
#and(#false, #false) → #false [0]
#and(#false, #true) → #false [0]
#and(#true, #false) → #false [0]
#and(#true, #true) → #true [0]
#div(#0, #0) → #divByZero [0]
#div(#0, #neg(@y)) → #0 [0]
#div(#0, #pos(@y)) → #0 [0]
#div(#neg(@x), #0) → #divByZero [0]
#div(#neg(@x), #neg(@y)) → #pos(#natdiv(@x, @y)) [0]
#div(#neg(@x), #pos(@y)) → #neg(#natdiv(@x, @y)) [0]
#div(#pos(@x), #0) → #divByZero [0]
#div(#pos(@x), #neg(@y)) → #neg(#natdiv(@x, @y)) [0]
#div(#pos(@x), #pos(@y)) → #pos(#natdiv(@x, @y)) [0]
#eq(#0, #0) → #true [0]
#eq(#0, #neg(@y)) → #false [0]
#eq(#0, #pos(@y)) → #false [0]
#eq(#0, #s(@y)) → #false [0]
#eq(#neg(@x), #0) → #false [0]
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y) [0]
#eq(#neg(@x), #pos(@y)) → #false [0]
#eq(#pos(@x), #0) → #false [0]
#eq(#pos(@x), #neg(@y)) → #false [0]
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y) [0]
#eq(#s(@x), #0) → #false [0]
#eq(#s(@x), #s(@y)) → #eq(@x, @y) [0]
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) [0]
#eq(::(@x_1, @x_2), nil) → #false [0]
#eq(nil, ::(@y_1, @y_2)) → #false [0]
#eq(nil, nil) → #true [0]
#mult(#0, #0) → #0 [0]
#mult(#0, #neg(@y)) → #0 [0]
#mult(#0, #pos(@y)) → #0 [0]
#mult(#neg(@x), #0) → #0 [0]
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y)) [0]
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y)) [0]
#mult(#pos(@x), #0) → #0 [0]
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y)) [0]
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y)) [0]
#natdiv(#0, #0) → #divByZero [0]
#natdiv(#s(@x), #s(@y)) → #s(#natdiv(#natsub(@x, @y), #s(@y))) [0]
#natmult(#0, @y) → #0 [0]
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y)) [0]
#natsub(@x, #0) → @x [0]
#natsub(#s(@x), #s(@y)) → #natsub(@x, @y) [0]
#pred(#0) → #neg(#s(#0)) [0]
#pred(#neg(#s(@x))) → #neg(#s(#s(@x))) [0]
#pred(#pos(#s(#0))) → #0 [0]
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x)) [0]
#sub(@x, #0) → @x [0]
#sub(@x, #neg(@y)) → #add(@x, #pos(@y)) [0]
#sub(@x, #pos(@y)) → #add(@x, #neg(@y)) [0]
#succ(#0) → #pos(#s(#0)) [0]
#succ(#neg(#s(#0))) → #0 [0]
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x)) [0]
#succ(#pos(#s(@x))) → #pos(#s(#s(@x))) [0]
| #equal :: :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero → #false:#true #eq :: :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero → #false:#true times :: :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero #mult :: :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero minus :: :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero #sub :: :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero div :: :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero #div :: :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero eratos :: :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero eratos#1 :: :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero :: :: :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero filter :: :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero nil :: :::nil:#0:#s:#neg:#pos:#divByZero filter#1 :: :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero filter#2 :: :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero filter#3 :: #false:#true → :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero mod :: :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero #0 :: :::nil:#0:#s:#neg:#pos:#divByZero #false :: #false:#true #true :: #false:#true #add :: :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero #neg :: :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero #s :: :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero #pred :: :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero #pos :: :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero #succ :: :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero #and :: #false:#true → #false:#true → #false:#true #divByZero :: :::nil:#0:#s:#neg:#pos:#divByZero #natdiv :: :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero #natmult :: :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero #natsub :: :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero → :::nil:#0:#s:#neg:#pos:#divByZero |
#add(v0, v1) → null_#add [0]
#and(v0, v1) → null_#and [0]
#div(v0, v1) → null_#div [0]
#eq(v0, v1) → null_#eq [0]
#mult(v0, v1) → null_#mult [0]
#natdiv(v0, v1) → null_#natdiv [0]
#natmult(v0, v1) → null_#natmult [0]
#natsub(v0, v1) → null_#natsub [0]
#pred(v0) → null_#pred [0]
#sub(v0, v1) → null_#sub [0]
#succ(v0) → null_#succ [0]
eratos#1(v0) → null_eratos#1 [0]
filter#1(v0, v1) → null_filter#1 [0]
filter#3(v0, v1, v2) → null_filter#3 [0]
null_#add, null_#and, null_#div, null_#eq, null_#mult, null_#natdiv, null_#natmult, null_#natsub, null_#pred, null_#sub, null_#succ, null_eratos#1, null_filter#1, null_filter#3
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
nil => 2
#0 => 0
#false => 1
#true => 2
#divByZero => 1
null_#add => 0
null_#and => 0
null_#div => 0
null_#eq => 0
null_#mult => 0
null_#natdiv => 0
null_#natmult => 0
null_#natsub => 0
null_#pred => 0
null_#sub => 0
null_#succ => 0
null_eratos#1 => 0
null_filter#1 => 0
null_filter#3 => 0
#add(z, z') -{ 0 }→ @y :|: z' = @y, z = 0, @y >= 0
#add(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
#add(z, z') -{ 0 }→ #succ(@y) :|: z = 1 + (1 + 0), z' = @y, @y >= 0
#add(z, z') -{ 0 }→ #succ(#add(1 + (1 + @x), @y)) :|: @x >= 0, z' = @y, z = 1 + (1 + (1 + @x)), @y >= 0
#add(z, z') -{ 0 }→ #pred(@y) :|: z = 1 + (1 + 0), z' = @y, @y >= 0
#add(z, z') -{ 0 }→ #pred(#add(1 + (1 + @x), @y)) :|: @x >= 0, z' = @y, z = 1 + (1 + (1 + @x)), @y >= 0
#and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
#and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
#and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
#and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
#and(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
#div(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
#div(z, z') -{ 0 }→ 1 :|: @x >= 0, z = 1 + @x, z' = 0
#div(z, z') -{ 0 }→ 0 :|: z = 0, z' = 1 + @y, @y >= 0
#div(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
#div(z, z') -{ 0 }→ 1 + #natdiv(@x, @y) :|: @x >= 0, z = 1 + @x, z' = 1 + @y, @y >= 0
#eq(z, z') -{ 0 }→ 2 :|: z = 0, z' = 0
#eq(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
#eq(z, z') -{ 0 }→ 1 :|: z = 0, z' = 1 + @y, @y >= 0
#eq(z, z') -{ 0 }→ 1 :|: @x >= 0, z = 1 + @x, z' = 0
#eq(z, z') -{ 0 }→ 1 :|: @x >= 0, z = 1 + @x, z' = 1 + @y, @y >= 0
#eq(z, z') -{ 0 }→ 1 :|: @x_1 >= 0, z' = 2, z = 1 + @x_1 + @x_2, @x_2 >= 0
#eq(z, z') -{ 0 }→ 1 :|: z = 2, @y_1 >= 0, @y_2 >= 0, z' = 1 + @y_1 + @y_2
#eq(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
#eq(z, z') -{ 0 }→ #eq(@x, @y) :|: @x >= 0, z = 1 + @x, z' = 1 + @y, @y >= 0
#eq(z, z') -{ 0 }→ #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) :|: @x_1 >= 0, z = 1 + @x_1 + @x_2, @y_1 >= 0, @x_2 >= 0, @y_2 >= 0, z' = 1 + @y_1 + @y_2
#equal(z, z') -{ 1 }→ #eq(@x, @y) :|: z = @x, @x >= 0, z' = @y, @y >= 0
#mult(z, z') -{ 0 }→ 0 :|: z = 0, z' = 0
#mult(z, z') -{ 0 }→ 0 :|: z = 0, z' = 1 + @y, @y >= 0
#mult(z, z') -{ 0 }→ 0 :|: @x >= 0, z = 1 + @x, z' = 0
#mult(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
#mult(z, z') -{ 0 }→ 1 + #natmult(@x, @y) :|: @x >= 0, z = 1 + @x, z' = 1 + @y, @y >= 0
#natdiv(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
#natdiv(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
#natdiv(z, z') -{ 0 }→ 1 + #natdiv(#natsub(@x, @y), 1 + @y) :|: @x >= 0, z = 1 + @x, z' = 1 + @y, @y >= 0
#natmult(z, z') -{ 0 }→ 0 :|: z' = @y, z = 0, @y >= 0
#natmult(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
#natmult(z, z') -{ 0 }→ #add(1 + @y, #natmult(@x, @y)) :|: @x >= 0, z = 1 + @x, z' = @y, @y >= 0
#natsub(z, z') -{ 0 }→ @x :|: z = @x, @x >= 0, z' = 0
#natsub(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
#natsub(z, z') -{ 0 }→ #natsub(@x, @y) :|: @x >= 0, z = 1 + @x, z' = 1 + @y, @y >= 0
#pred(z) -{ 0 }→ 0 :|: z = 1 + (1 + 0)
#pred(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
#pred(z) -{ 0 }→ 1 + (1 + @x) :|: @x >= 0, z = 1 + (1 + (1 + @x))
#pred(z) -{ 0 }→ 1 + (1 + 0) :|: z = 0
#pred(z) -{ 0 }→ 1 + (1 + (1 + @x)) :|: @x >= 0, z = 1 + (1 + @x)
#sub(z, z') -{ 0 }→ @x :|: z = @x, @x >= 0, z' = 0
#sub(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
#sub(z, z') -{ 0 }→ #add(@x, 1 + @y) :|: z = @x, @x >= 0, z' = 1 + @y, @y >= 0
#succ(z) -{ 0 }→ 0 :|: z = 1 + (1 + 0)
#succ(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
#succ(z) -{ 0 }→ 1 + (1 + @x) :|: @x >= 0, z = 1 + (1 + (1 + @x))
#succ(z) -{ 0 }→ 1 + (1 + 0) :|: z = 0
#succ(z) -{ 0 }→ 1 + (1 + (1 + @x)) :|: @x >= 0, z = 1 + (1 + @x)
div(z, z') -{ 1 }→ #div(@x, @y) :|: z = @x, @x >= 0, z' = @y, @y >= 0
eratos(z) -{ 1 }→ eratos#1(@l) :|: z = @l, @l >= 0
eratos#1(z) -{ 1 }→ 2 :|: z = 2
eratos#1(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
eratos#1(z) -{ 1 }→ 1 + @x + eratos(filter(@x, @xs)) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0
filter(z, z') -{ 1 }→ filter#1(@l, @p) :|: z = @p, @p >= 0, @l >= 0, z' = @l
filter#1(z, z') -{ 1 }→ filter#2(filter(@p, @xs), @p, @x) :|: @p >= 0, @x >= 0, z = 1 + @x + @xs, @xs >= 0, z' = @p
filter#1(z, z') -{ 1 }→ 2 :|: z = 2, @p >= 0, z' = @p
filter#1(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
filter#2(z, z', z'') -{ 1 }→ filter#3(#equal(mod(@x, @p), 0), @x, @xs') :|: @p >= 0, @x >= 0, @xs' >= 0, z = @xs', z'' = @x, z' = @p
filter#3(z, z', z'') -{ 1 }→ @xs' :|: z = 2, z'' = @xs', @x >= 0, @xs' >= 0, z' = @x
filter#3(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
filter#3(z, z', z'') -{ 1 }→ 1 + @x + @xs' :|: z'' = @xs', @x >= 0, @xs' >= 0, z = 1, z' = @x
minus(z, z') -{ 1 }→ #sub(@x, @y) :|: z = @x, @x >= 0, z' = @y, @y >= 0
mod(z, z') -{ 1 }→ minus(@x, times(@x, div(@x, @y))) :|: z = @x, @x >= 0, z' = @y, @y >= 0
times(z, z') -{ 1 }→ #mult(@x, @y) :|: z = @x, @x >= 0, z' = @y, @y >= 0
| eq(start(V, V1, V19),0,[fun(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V19),0,[times(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V19),0,[minus(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V19),0,[div(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V19),0,[eratos(V, Out)],[V >= 0]). eq(start(V, V1, V19),0,[fun5(V, Out)],[V >= 0]). eq(start(V, V1, V19),0,[filter(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V19),0,[fun6(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V19),0,[fun7(V, V1, V19, Out)],[V >= 0,V1 >= 0,V19 >= 0]). eq(start(V, V1, V19),0,[fun8(V, V1, V19, Out)],[V >= 0,V1 >= 0,V19 >= 0]). eq(start(V, V1, V19),0,[mod(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V19),0,[fun9(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V19),0,[fun12(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V19),0,[fun4(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V19),0,[fun1(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V19),0,[fun2(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V19),0,[fun13(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V19),0,[fun14(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V19),0,[fun15(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V19),0,[fun10(V, Out)],[V >= 0]). eq(start(V, V1, V19),0,[fun3(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V19),0,[fun11(V, Out)],[V >= 0]). eq(fun(V, V1, Out),1,[fun1(V2, V3, Ret)],[Out = Ret,V = V2,V2 >= 0,V1 = V3,V3 >= 0]). eq(times(V, V1, Out),1,[fun2(V4, V5, Ret1)],[Out = Ret1,V = V4,V4 >= 0,V1 = V5,V5 >= 0]). eq(minus(V, V1, Out),1,[fun3(V6, V7, Ret2)],[Out = Ret2,V = V6,V6 >= 0,V1 = V7,V7 >= 0]). eq(div(V, V1, Out),1,[fun4(V8, V9, Ret3)],[Out = Ret3,V = V8,V8 >= 0,V1 = V9,V9 >= 0]). eq(eratos(V, Out),1,[fun5(V10, Ret4)],[Out = Ret4,V = V10,V10 >= 0]). eq(fun5(V, Out),1,[filter(V11, V12, Ret10),eratos(Ret10, Ret11)],[Out = 1 + Ret11 + V11,V11 >= 0,V = 1 + V11 + V12,V12 >= 0]). eq(fun5(V, Out),1,[],[Out = 2,V = 2]). eq(filter(V, V1, Out),1,[fun6(V13, V14, Ret5)],[Out = Ret5,V = V14,V14 >= 0,V13 >= 0,V1 = V13]). eq(fun6(V, V1, Out),1,[filter(V15, V16, Ret0),fun7(Ret0, V15, V17, Ret6)],[Out = Ret6,V15 >= 0,V17 >= 0,V = 1 + V16 + V17,V16 >= 0,V1 = V15]). eq(fun6(V, V1, Out),1,[],[Out = 2,V = 2,V18 >= 0,V1 = V18]). eq(fun7(V, V1, V19, Out),1,[mod(V20, V21, Ret00),fun(Ret00, 0, Ret01),fun8(Ret01, V20, V22, Ret7)],[Out = Ret7,V21 >= 0,V20 >= 0,V22 >= 0,V = V22,V19 = V20,V1 = V21]). eq(fun8(V, V1, V19, Out),1,[],[Out = 1 + V23 + V24,V19 = V24,V23 >= 0,V24 >= 0,V = 1,V1 = V23]). eq(fun8(V, V1, V19, Out),1,[],[Out = V25,V = 2,V19 = V25,V26 >= 0,V25 >= 0,V1 = V26]). eq(mod(V, V1, Out),1,[div(V27, V28, Ret111),times(V27, Ret111, Ret12),minus(V27, Ret12, Ret8)],[Out = Ret8,V = V27,V27 >= 0,V1 = V28,V28 >= 0]). eq(fun9(V, V1, Out),0,[],[Out = V29,V1 = V29,V = 0,V29 >= 0]). eq(fun9(V, V1, Out),0,[fun10(V30, Ret9)],[Out = Ret9,V = 2,V1 = V30,V30 >= 0]). eq(fun9(V, V1, Out),0,[fun9(1 + (1 + V31), V32, Ret02),fun10(Ret02, Ret13)],[Out = Ret13,V31 >= 0,V1 = V32,V = 3 + V31,V32 >= 0]). eq(fun9(V, V1, Out),0,[fun11(V33, Ret14)],[Out = Ret14,V = 2,V1 = V33,V33 >= 0]). eq(fun9(V, V1, Out),0,[fun9(1 + (1 + V34), V35, Ret03),fun11(Ret03, Ret15)],[Out = Ret15,V34 >= 0,V1 = V35,V = 3 + V34,V35 >= 0]). eq(fun12(V, V1, Out),0,[],[Out = 1,V = 1,V1 = 1]). eq(fun12(V, V1, Out),0,[],[Out = 1,V1 = 2,V = 1]). eq(fun12(V, V1, Out),0,[],[Out = 1,V = 2,V1 = 1]). eq(fun12(V, V1, Out),0,[],[Out = 2,V = 2,V1 = 2]). eq(fun4(V, V1, Out),0,[],[Out = 1,V = 0,V1 = 0]). eq(fun4(V, V1, Out),0,[],[Out = 0,V = 0,V1 = 1 + V36,V36 >= 0]). eq(fun4(V, V1, Out),0,[],[Out = 1,V37 >= 0,V = 1 + V37,V1 = 0]). eq(fun4(V, V1, Out),0,[fun13(V38, V39, Ret16)],[Out = 1 + Ret16,V38 >= 0,V = 1 + V38,V1 = 1 + V39,V39 >= 0]). eq(fun1(V, V1, Out),0,[],[Out = 2,V = 0,V1 = 0]). eq(fun1(V, V1, Out),0,[],[Out = 1,V = 0,V1 = 1 + V40,V40 >= 0]). eq(fun1(V, V1, Out),0,[],[Out = 1,V41 >= 0,V = 1 + V41,V1 = 0]). eq(fun1(V, V1, Out),0,[fun1(V42, V43, Ret17)],[Out = Ret17,V42 >= 0,V = 1 + V42,V1 = 1 + V43,V43 >= 0]). eq(fun1(V, V1, Out),0,[],[Out = 1,V44 >= 0,V = 1 + V44,V1 = 1 + V45,V45 >= 0]). eq(fun1(V, V1, Out),0,[fun1(V46, V47, Ret04),fun1(V48, V49, Ret18),fun12(Ret04, Ret18, Ret19)],[Out = Ret19,V46 >= 0,V = 1 + V46 + V48,V47 >= 0,V48 >= 0,V49 >= 0,V1 = 1 + V47 + V49]). eq(fun1(V, V1, Out),0,[],[Out = 1,V50 >= 0,V1 = 2,V = 1 + V50 + V51,V51 >= 0]). eq(fun1(V, V1, Out),0,[],[Out = 1,V = 2,V52 >= 0,V53 >= 0,V1 = 1 + V52 + V53]). eq(fun1(V, V1, Out),0,[],[Out = 2,V = 2,V1 = 2]). eq(fun2(V, V1, Out),0,[],[Out = 0,V = 0,V1 = 0]). eq(fun2(V, V1, Out),0,[],[Out = 0,V = 0,V1 = 1 + V54,V54 >= 0]). eq(fun2(V, V1, Out),0,[],[Out = 0,V55 >= 0,V = 1 + V55,V1 = 0]). eq(fun2(V, V1, Out),0,[fun14(V56, V57, Ret110)],[Out = 1 + Ret110,V56 >= 0,V = 1 + V56,V1 = 1 + V57,V57 >= 0]). eq(fun13(V, V1, Out),0,[],[Out = 1,V = 0,V1 = 0]). eq(fun13(V, V1, Out),0,[fun15(V58, V59, Ret101),fun13(Ret101, 1 + V59, Ret112)],[Out = 1 + Ret112,V58 >= 0,V = 1 + V58,V1 = 1 + V59,V59 >= 0]). eq(fun14(V, V1, Out),0,[],[Out = 0,V1 = V60,V = 0,V60 >= 0]). eq(fun14(V, V1, Out),0,[fun14(V62, V61, Ret113),fun9(1 + V61, Ret113, Ret20)],[Out = Ret20,V62 >= 0,V = 1 + V62,V1 = V61,V61 >= 0]). eq(fun15(V, V1, Out),0,[],[Out = V63,V = V63,V63 >= 0,V1 = 0]). eq(fun15(V, V1, Out),0,[fun15(V64, V65, Ret21)],[Out = Ret21,V64 >= 0,V = 1 + V64,V1 = 1 + V65,V65 >= 0]). eq(fun10(V, Out),0,[],[Out = 2,V = 0]). eq(fun10(V, Out),0,[],[Out = 3 + V66,V66 >= 0,V = 2 + V66]). eq(fun10(V, Out),0,[],[Out = 0,V = 2]). eq(fun10(V, Out),0,[],[Out = 2 + V67,V67 >= 0,V = 3 + V67]). eq(fun3(V, V1, Out),0,[],[Out = V68,V = V68,V68 >= 0,V1 = 0]). eq(fun3(V, V1, Out),0,[fun9(V69, 1 + V70, Ret22)],[Out = Ret22,V = V69,V69 >= 0,V1 = 1 + V70,V70 >= 0]). eq(fun11(V, Out),0,[],[Out = 2,V = 0]). eq(fun11(V, Out),0,[],[Out = 0,V = 2]). eq(fun11(V, Out),0,[],[Out = 2 + V71,V71 >= 0,V = 3 + V71]). eq(fun11(V, Out),0,[],[Out = 3 + V72,V72 >= 0,V = 2 + V72]). eq(fun9(V, V1, Out),0,[],[Out = 0,V73 >= 0,V74 >= 0,V = V73,V1 = V74]). eq(fun12(V, V1, Out),0,[],[Out = 0,V75 >= 0,V76 >= 0,V = V75,V1 = V76]). eq(fun4(V, V1, Out),0,[],[Out = 0,V77 >= 0,V78 >= 0,V = V77,V1 = V78]). eq(fun1(V, V1, Out),0,[],[Out = 0,V79 >= 0,V80 >= 0,V = V79,V1 = V80]). eq(fun2(V, V1, Out),0,[],[Out = 0,V81 >= 0,V82 >= 0,V = V81,V1 = V82]). eq(fun13(V, V1, Out),0,[],[Out = 0,V83 >= 0,V84 >= 0,V = V83,V1 = V84]). eq(fun14(V, V1, Out),0,[],[Out = 0,V85 >= 0,V86 >= 0,V = V85,V1 = V86]). eq(fun15(V, V1, Out),0,[],[Out = 0,V87 >= 0,V88 >= 0,V = V87,V1 = V88]). eq(fun10(V, Out),0,[],[Out = 0,V89 >= 0,V = V89]). eq(fun3(V, V1, Out),0,[],[Out = 0,V90 >= 0,V91 >= 0,V = V90,V1 = V91]). eq(fun11(V, Out),0,[],[Out = 0,V92 >= 0,V = V92]). eq(fun5(V, Out),0,[],[Out = 0,V93 >= 0,V = V93]). eq(fun6(V, V1, Out),0,[],[Out = 0,V94 >= 0,V95 >= 0,V = V94,V1 = V95]). eq(fun8(V, V1, V19, Out),0,[],[Out = 0,V96 >= 0,V19 = V97,V98 >= 0,V = V96,V1 = V98,V97 >= 0]). input_output_vars(fun(V,V1,Out),[V,V1],[Out]). input_output_vars(times(V,V1,Out),[V,V1],[Out]). input_output_vars(minus(V,V1,Out),[V,V1],[Out]). input_output_vars(div(V,V1,Out),[V,V1],[Out]). input_output_vars(eratos(V,Out),[V],[Out]). input_output_vars(fun5(V,Out),[V],[Out]). input_output_vars(filter(V,V1,Out),[V,V1],[Out]). input_output_vars(fun6(V,V1,Out),[V,V1],[Out]). input_output_vars(fun7(V,V1,V19,Out),[V,V1,V19],[Out]). input_output_vars(fun8(V,V1,V19,Out),[V,V1,V19],[Out]). input_output_vars(mod(V,V1,Out),[V,V1],[Out]). input_output_vars(fun9(V,V1,Out),[V,V1],[Out]). input_output_vars(fun12(V,V1,Out),[V,V1],[Out]). input_output_vars(fun4(V,V1,Out),[V,V1],[Out]). input_output_vars(fun1(V,V1,Out),[V,V1],[Out]). input_output_vars(fun2(V,V1,Out),[V,V1],[Out]). input_output_vars(fun13(V,V1,Out),[V,V1],[Out]). input_output_vars(fun14(V,V1,Out),[V,V1],[Out]). input_output_vars(fun15(V,V1,Out),[V,V1],[Out]). input_output_vars(fun10(V,Out),[V],[Out]). input_output_vars(fun3(V,V1,Out),[V,V1],[Out]). input_output_vars(fun11(V,Out),[V],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. recursive : [fun15/3]
1. recursive : [fun13/3]
2. non_recursive : [fun4/3]
3. non_recursive : [ (div)/3]
4. non_recursive : [fun12/3]
5. recursive [non_tail,multiple] : [fun1/3]
6. non_recursive : [fun/3]
7. non_recursive : [fun8/4]
8. non_recursive : [fun10/2]
9. non_recursive : [fun11/2]
10. recursive [non_tail] : [fun9/3]
11. non_recursive : [fun3/3]
12. non_recursive : [minus/3]
13. recursive [non_tail] : [fun14/3]
14. non_recursive : [fun2/3]
15. non_recursive : [times/3]
16. non_recursive : [ (mod)/3]
17. non_recursive : [fun7/4]
18. recursive [non_tail] : [filter/3,fun6/3]
19. recursive : [eratos/2,fun5/2]
20. non_recursive : [start/3]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into fun15/3
1. SCC is partially evaluated into fun13/3
2. SCC is partially evaluated into fun4/3
3. SCC is completely evaluated into other SCCs
4. SCC is partially evaluated into fun12/3
5. SCC is partially evaluated into fun1/3
6. SCC is completely evaluated into other SCCs
7. SCC is partially evaluated into fun8/4
8. SCC is partially evaluated into fun10/2
9. SCC is partially evaluated into fun11/2
10. SCC is partially evaluated into fun9/3
11. SCC is partially evaluated into fun3/3
12. SCC is completely evaluated into other SCCs
13. SCC is partially evaluated into fun14/3
14. SCC is partially evaluated into fun2/3
15. SCC is completely evaluated into other SCCs
16. SCC is partially evaluated into (mod)/3
17. SCC is partially evaluated into fun7/4
18. SCC is partially evaluated into filter/3
19. SCC is partially evaluated into fun5/2
20. SCC is partially evaluated into start/3
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations fun15/3
* CE 74 is refined into CE [83]
* CE 72 is refined into CE [84]
* CE 73 is refined into CE [85]
### Cost equations --> "Loop" of fun15/3
* CEs [85] --> Loop 56
* CEs [83] --> Loop 57
* CEs [84] --> Loop 58
### Ranking functions of CR fun15(V,V1,Out)
* RF of phase [56]: [V,V1]
#### Partial ranking functions of CR fun15(V,V1,Out)
* Partial RF of phase [56]:
- RF of loop [56:1]:
V
V1
### Specialization of cost equations fun13/3
* CE 69 is refined into CE [86]
* CE 67 is refined into CE [87]
* CE 68 is refined into CE [88,89,90]
### Cost equations --> "Loop" of fun13/3
* CEs [90] --> Loop 59
* CEs [89] --> Loop 60
* CEs [88] --> Loop 61
* CEs [86] --> Loop 62
* CEs [87] --> Loop 63
### Ranking functions of CR fun13(V,V1,Out)
* RF of phase [59]: [V-1,V-V1+1]
* RF of phase [61]: [V]
#### Partial ranking functions of CR fun13(V,V1,Out)
* Partial RF of phase [59]:
- RF of loop [59:1]:
V-1
V-V1+1
* Partial RF of phase [61]:
- RF of loop [61:1]:
V
### Specialization of cost equations fun4/3
* CE 51 is refined into CE [91,92,93,94,95,96]
* CE 49 is refined into CE [97]
* CE 50 is refined into CE [98]
* CE 48 is refined into CE [99]
### Cost equations --> "Loop" of fun4/3
* CEs [96] --> Loop 64
* CEs [95] --> Loop 65
* CEs [94] --> Loop 66
* CEs [93] --> Loop 67
* CEs [97] --> Loop 68
* CEs [92] --> Loop 69
* CEs [98] --> Loop 70
* CEs [91] --> Loop 71
* CEs [99] --> Loop 72
### Ranking functions of CR fun4(V,V1,Out)
#### Partial ranking functions of CR fun4(V,V1,Out)
### Specialization of cost equations fun12/3
* CE 66 is refined into CE [100]
* CE 65 is refined into CE [101]
* CE 64 is refined into CE [102]
* CE 63 is refined into CE [103]
* CE 62 is refined into CE [104]
### Cost equations --> "Loop" of fun12/3
* CEs [100] --> Loop 73
* CEs [101] --> Loop 74
* CEs [102] --> Loop 75
* CEs [103] --> Loop 76
* CEs [104] --> Loop 77
### Ranking functions of CR fun12(V,V1,Out)
#### Partial ranking functions of CR fun12(V,V1,Out)
### Specialization of cost equations fun1/3
* CE 37 is refined into CE [105]
* CE 40 is refined into CE [106]
* CE 35 is refined into CE [107]
* CE 39 is refined into CE [108]
* CE 34 is refined into CE [109]
* CE 33 is refined into CE [110]
* CE 38 is refined into CE [111,112,113,114,115]
* CE 36 is refined into CE [116]
### Cost equations --> "Loop" of fun1/3
* CEs [116] --> Loop 78
* CEs [114] --> Loop 79
* CEs [113] --> Loop 80
* CEs [112] --> Loop 81
* CEs [111] --> Loop 82
* CEs [115] --> Loop 83
* CEs [105] --> Loop 84
* CEs [106] --> Loop 85
* CEs [107] --> Loop 86
* CEs [108] --> Loop 87
* CEs [109] --> Loop 88
* CEs [110] --> Loop 89
### Ranking functions of CR fun1(V,V1,Out)
* RF of phase [78,79,80,81,82,83]: [V,V1]
#### Partial ranking functions of CR fun1(V,V1,Out)
* Partial RF of phase [78,79,80,81,82,83]:
- RF of loop [78:1,79:1,79:2,80:1,80:2,81:1,81:2,82:1,82:2,83:1,83:2]:
V
V1
### Specialization of cost equations fun8/4
* CE 54 is refined into CE [117]
* CE 53 is refined into CE [118]
* CE 52 is refined into CE [119]
### Cost equations --> "Loop" of fun8/4
* CEs [117] --> Loop 90
* CEs [118] --> Loop 91
* CEs [119] --> Loop 92
### Ranking functions of CR fun8(V,V1,V19,Out)
#### Partial ranking functions of CR fun8(V,V1,V19,Out)
### Specialization of cost equations fun10/2
* CE 78 is refined into CE [120]
* CE 76 is refined into CE [121]
* CE 77 is refined into CE [122]
* CE 75 is refined into CE [123]
### Cost equations --> "Loop" of fun10/2
* CEs [120] --> Loop 93
* CEs [121] --> Loop 94
* CEs [122] --> Loop 95
* CEs [123] --> Loop 96
### Ranking functions of CR fun10(V,Out)
#### Partial ranking functions of CR fun10(V,Out)
### Specialization of cost equations fun11/2
* CE 81 is refined into CE [124]
* CE 82 is refined into CE [125]
* CE 80 is refined into CE [126]
* CE 79 is refined into CE [127]
### Cost equations --> "Loop" of fun11/2
* CEs [124] --> Loop 97
* CEs [125] --> Loop 98
* CEs [126] --> Loop 99
* CEs [127] --> Loop 100
### Ranking functions of CR fun11(V,Out)
#### Partial ranking functions of CR fun11(V,Out)
### Specialization of cost equations fun9/3
* CE 61 is refined into CE [128]
* CE 57 is refined into CE [129,130,131,132]
* CE 59 is refined into CE [133,134,135,136]
* CE 56 is refined into CE [137]
* CE 58 is refined into CE [138,139,140,141]
* CE 60 is refined into CE [142,143,144,145]
### Cost equations --> "Loop" of fun9/3
* CEs [140,144] --> Loop 101
* CEs [141,145] --> Loop 102
* CEs [138,142] --> Loop 103
* CEs [139,143] --> Loop 104
* CEs [132,136] --> Loop 105
* CEs [131,135] --> Loop 106
* CEs [128,130,134] --> Loop 107
* CEs [129,133] --> Loop 108
* CEs [137] --> Loop 109
### Ranking functions of CR fun9(V,V1,Out)
* RF of phase [101,102,103,104]: [V-2]
#### Partial ranking functions of CR fun9(V,V1,Out)
* Partial RF of phase [101,102,103,104]:
- RF of loop [101:1,102:1,103:1,104:1]:
V-2
### Specialization of cost equations fun3/3
* CE 46 is refined into CE [146,147,148,149,150,151]
* CE 47 is refined into CE [152]
* CE 45 is refined into CE [153]
### Cost equations --> "Loop" of fun3/3
* CEs [151] --> Loop 110
* CEs [150] --> Loop 111
* CEs [149,152] --> Loop 112
* CEs [153] --> Loop 113
* CEs [148] --> Loop 114
* CEs [147] --> Loop 115
* CEs [146] --> Loop 116
### Ranking functions of CR fun3(V,V1,Out)
#### Partial ranking functions of CR fun3(V,V1,Out)
### Specialization of cost equations fun14/3
* CE 70 is refined into CE [154]
* CE 71 is refined into CE [155,156,157,158,159,160,161]
### Cost equations --> "Loop" of fun14/3
* CEs [161] --> Loop 117
* CEs [160] --> Loop 118
* CEs [158] --> Loop 119
* CEs [159] --> Loop 120
* CEs [156] --> Loop 121
* CEs [157] --> Loop 122
* CEs [155] --> Loop 123
* CEs [154] --> Loop 124
### Ranking functions of CR fun14(V,V1,Out)
* RF of phase [117,118,119,120,121,122,123]: [V]
#### Partial ranking functions of CR fun14(V,V1,Out)
* Partial RF of phase [117,118,119,120,121,122,123]:
- RF of loop [117:1,118:1,119:1,120:1,121:1,122:1,123:1]:
V
### Specialization of cost equations fun2/3
* CE 44 is refined into CE [162,163]
* CE 43 is refined into CE [164]
* CE 41 is refined into CE [165]
* CE 42 is refined into CE [166]
### Cost equations --> "Loop" of fun2/3
* CEs [163] --> Loop 125
* CEs [162] --> Loop 126
* CEs [164] --> Loop 127
* CEs [165,166] --> Loop 128
### Ranking functions of CR fun2(V,V1,Out)
#### Partial ranking functions of CR fun2(V,V1,Out)
### Specialization of cost equations (mod)/3
* CE 55 is refined into CE [167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200,201,202,203,204,205,206,207,208,209,210,211,212,213,214,215,216,217,218,219,220,221,222,223]
### Cost equations --> "Loop" of (mod)/3
* CEs [184,188,189,195,199,200,204,208,209,213,215,216,220,222,223] --> Loop 129
* CEs [181] --> Loop 130
* CEs [182,183,187] --> Loop 131
* CEs [175,179,180] --> Loop 132
* CEs [172] --> Loop 133
* CEs [173,174,178] --> Loop 134
* CEs [185,186,196,197,205,206] --> Loop 135
* CEs [176,177] --> Loop 136
* CEs [169,190,192,201,210,217] --> Loop 137
* CEs [170,171] --> Loop 138
* CEs [167,168,191,193,194,198,202,203,207,211,212,214,218,219,221] --> Loop 139
### Ranking functions of CR mod(V,V1,Out)
#### Partial ranking functions of CR mod(V,V1,Out)
### Specialization of cost equations fun7/4
* CE 32 is refined into CE [224,225,226,227,228,229,230,231,232,233,234,235,236,237,238,239,240,241,242,243,244,245,246,247,248,249,250,251,252,253,254,255,256]
### Cost equations --> "Loop" of fun7/4
* CEs [230] --> Loop 140
* CEs [231,232] --> Loop 141
* CEs [236] --> Loop 142
* CEs [237] --> Loop 143
* CEs [249] --> Loop 144
* CEs [246] --> Loop 145
* CEs [247,248,250,251] --> Loop 146
* CEs [243] --> Loop 147
* CEs [224,233,241,252] --> Loop 148
* CEs [227,238,254] --> Loop 149
* CEs [225,226,228,229,234,235,239,240,242,244,245,253,255,256] --> Loop 150
### Ranking functions of CR fun7(V,V1,V19,Out)
#### Partial ranking functions of CR fun7(V,V1,V19,Out)
### Specialization of cost equations filter/3
* CE 31 is refined into CE [257,258,259,260,261,262,263,264]
* CE 29 is refined into CE [265]
* CE 30 is refined into CE [266]
### Cost equations --> "Loop" of filter/3
* CEs [265] --> Loop 151
* CEs [266] --> Loop 152
* CEs [259,262] --> Loop 153
* CEs [264] --> Loop 154
* CEs [261] --> Loop 155
* CEs [258,263] --> Loop 156
* CEs [257,260] --> Loop 157
### Ranking functions of CR filter(V,V1,Out)
* RF of phase [153,154,155,156,157]: [V1]
#### Partial ranking functions of CR filter(V,V1,Out)
* Partial RF of phase [153,154,155,156,157]:
- RF of loop [153:1,155:1,156:1]:
V1
- RF of loop [154:1]:
V1/3-2/3
- RF of loop [157:1]:
V1-1
### Specialization of cost equations fun5/2
* CE 28 is refined into CE [267]
* CE 27 is refined into CE [268]
* CE 26 is refined into CE [269,270,271]
### Cost equations --> "Loop" of fun5/2
* CEs [269,271] --> Loop 158
* CEs [270] --> Loop 159
* CEs [267] --> Loop 160
* CEs [268] --> Loop 161
### Ranking functions of CR fun5(V,Out)
* RF of phase [158]: [V-1]
#### Partial ranking functions of CR fun5(V,Out)
* Partial RF of phase [158]:
- RF of loop [158:1]:
V-1
### Specialization of cost equations start/3
* CE 2 is refined into CE [272,273]
* CE 3 is refined into CE [274]
* CE 4 is refined into CE [275]
* CE 5 is refined into CE [276,277,278,279,280,281,282,283,284,285,286,287,288,289,290,291,292,293,294,295,296,297,298,299]
* CE 6 is refined into CE [300,301,302,303,304,305]
* CE 7 is refined into CE [306,307,308]
* CE 8 is refined into CE [309,310,311,312,313,314,315]
* CE 9 is refined into CE [316,317,318,319,320,321,322,323,324]
* CE 10 is refined into CE [325,326]
* CE 11 is refined into CE [327,328,329]
* CE 12 is refined into CE [330,331,332,333,334,335,336,337]
* CE 13 is refined into CE [338,339,340]
* CE 14 is refined into CE [341,342,343,344,345,346,347,348,349]
* CE 15 is refined into CE [350,351,352,353,354,355,356,357]
* CE 16 is refined into CE [358,359,360,361,362]
* CE 17 is refined into CE [363,364,365,366,367,368,369,370,371]
* CE 18 is refined into CE [372,373,374,375,376,377]
* CE 19 is refined into CE [378,379,380]
* CE 20 is refined into CE [381,382,383,384,385,386]
* CE 21 is refined into CE [387,388]
* CE 22 is refined into CE [389,390,391]
* CE 23 is refined into CE [392,393,394,395]
* CE 24 is refined into CE [396,397,398,399,400,401,402]
* CE 25 is refined into CE [403,404,405,406]
### Cost equations --> "Loop" of start/3
* CEs [336,337] --> Loop 162
* CEs [334,335] --> Loop 163
* CEs [333] --> Loop 164
* CEs [303,312,318,344,346,354,365,375,389,399] --> Loop 165
* CEs [279,287,295,319,347,348,361,366] --> Loop 166
* CEs [360] --> Loop 167
* CEs [275,310,311,339,342,343,351,352,353,397,398] --> Loop 168
* CEs [338] --> Loop 169
* CEs [359] --> Loop 170
* CEs [317,358,364,382] --> Loop 171
* CEs [272,273,274,276,277,278,280,281,282,283,284,285,286,288,289,290,291,292,293,294,296,297,298,299,300,301,302,304,305,306,307,308,309,313,314,315,316,320,321,322,323,324,325,326,327,328,329,330,331,332,340,341,345,349,350,355,356,357,362,363,367,368,369,370,371,372,373,374,376,377,378,379,380,381,383,384,385,386,387,388,390,391,392,393,394,395,396,400,401,402,403,404,405,406] --> Loop 172
### Ranking functions of CR start(V,V1,V19)
#### Partial ranking functions of CR start(V,V1,V19)
Computing Bounds
=====================================
#### Cost of chains of fun15(V,V1,Out):
* Chain [[56],58]: 0
with precondition: [V=Out+V1,V1>=1,V>=V1]
* Chain [[56],57]: 0
with precondition: [Out=0,V>=1,V1>=1]
* Chain [58]: 0
with precondition: [V1=0,V=Out,V>=0]
* Chain [57]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of fun13(V,V1,Out):
* Chain [[61],62]: 0
with precondition: [V1=1,Out>=1,V>=Out]
* Chain [[61],60,62]: 0
with precondition: [V1=1,Out>=2,V>=Out]
* Chain [[59],62]: 0
with precondition: [V1>=2,Out>=1,V+2>=2*Out+V1]
* Chain [[59],60,62]: 0
with precondition: [V1>=2,Out>=2,V+3>=2*Out+V1]
* Chain [63]: 0
with precondition: [V=0,V1=0,Out=1]
* Chain [62]: 0
with precondition: [Out=0,V>=0,V1>=0]
* Chain [60,62]: 0
with precondition: [Out=1,V>=1,V1>=1]
#### Cost of chains of fun4(V,V1,Out):
* Chain [72]: 0
with precondition: [V=0,V1=0,Out=1]
* Chain [71]: 0
with precondition: [V=1,V1=1,Out=2]
* Chain [70]: 0
with precondition: [V1=0,Out=1,V>=1]
* Chain [69]: 0
with precondition: [V1=2,Out>=2,V>=Out]
* Chain [68]: 0
with precondition: [Out=0,V>=0,V1>=0]
* Chain [67]: 0
with precondition: [Out=1,V>=1,V1>=1]
* Chain [66]: 0
with precondition: [Out=2,V>=2,V1>=2]
* Chain [65]: 0
with precondition: [V1>=3,Out>=2,V+4>=2*Out+V1]
* Chain [64]: 0
with precondition: [V1>=3,Out>=3,V+5>=2*Out+V1]
#### Cost of chains of fun12(V,V1,Out):
* Chain [77]: 0
with precondition: [V=1,V1=1,Out=1]
* Chain [76]: 0
with precondition: [V=1,V1=2,Out=1]
* Chain [75]: 0
with precondition: [V=2,V1=1,Out=1]
* Chain [74]: 0
with precondition: [V=2,V1=2,Out=2]
* Chain [73]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of fun1(V,V1,Out):
* Chain [89]: 0
with precondition: [V=0,V1=0,Out=2]
* Chain [88]: 0
with precondition: [V=0,Out=1,V1>=1]
* Chain [87]: 0
with precondition: [V=2,V1=2,Out=2]
* Chain [86]: 0
with precondition: [V1=0,Out=1,V>=1]
* Chain [85]: 0
with precondition: [Out=0,V>=0,V1>=0]
* Chain [84]: 0
with precondition: [Out=1,V>=1,V1>=1]
* Chain [multiple([78,79,80,81,82,83],[[89],[88],[87],[86],[85],[84]])]: 0
with precondition: [2>=Out,V>=1,V1>=1,Out>=0]
#### Cost of chains of fun8(V,V1,V19,Out):
* Chain [92]: 1
with precondition: [V=1,V1+V19+1=Out,V1>=0,V19>=0]
* Chain [91]: 1
with precondition: [V=2,V19=Out,V1>=0,V19>=0]
* Chain [90]: 0
with precondition: [Out=0,V>=0,V1>=0,V19>=0]
#### Cost of chains of fun10(V,Out):
* Chain [96]: 0
with precondition: [V=0,Out=2]
* Chain [95]: 0
with precondition: [Out=0,V>=0]
* Chain [94]: 0
with precondition: [V+1=Out,V>=2]
* Chain [93]: 0
with precondition: [V=Out+1,V>=3]
#### Cost of chains of fun11(V,Out):
* Chain [100]: 0
with precondition: [V=0,Out=2]
* Chain [99]: 0
with precondition: [Out=0,V>=0]
* Chain [98]: 0
with precondition: [V+1=Out,V>=2]
* Chain [97]: 0
with precondition: [V=Out+1,V>=3]
#### Cost of chains of fun9(V,V1,Out):
* Chain [[101,102,103,104],108]: 0
with precondition: [V1=0,V>=3,Out>=0,V>=Out]
* Chain [[101,102,103,104],107]: 0
with precondition: [V>=3,V1>=0,Out>=0,V>=Out+1]
* Chain [[101,102,103,104],106]: 0
with precondition: [V>=3,V1>=2,Out>=0,V+V1>=Out+1]
* Chain [[101,102,103,104],105]: 0
with precondition: [V>=3,V1>=3,Out>=0,V+V1>=Out+3]
* Chain [109]: 0
with precondition: [V=0,V1=Out,V1>=0]
* Chain [108]: 0
with precondition: [V=2,V1=0,Out=2]
* Chain [107]: 0
with precondition: [Out=0,V>=0,V1>=0]
* Chain [106]: 0
with precondition: [V=2,V1+1=Out,V1>=2]
* Chain [105]: 0
with precondition: [V=2,V1=Out+1,V1>=3]
#### Cost of chains of fun3(V,V1,Out):
* Chain [116]: 0
with precondition: [V=0,V1=Out,V1>=1]
* Chain [115]: 0
with precondition: [V=2,V1+1=Out,V1>=2]
* Chain [114]: 0
with precondition: [V=2,V1=Out+1,V1>=3]
* Chain [113]: 0
with precondition: [V1=0,V=Out,V>=0]
* Chain [112]: 0
with precondition: [Out=0,V>=0,V1>=0]
* Chain [111]: 0
with precondition: [V>=3,V1>=1,Out>=0,V>=Out+1]
* Chain [110]: 0
with precondition: [V>=3,V1>=2,Out>=0,V+V1>=Out+1]
#### Cost of chains of fun14(V,V1,Out):
* Chain [[117,118,119,120,121,122,123],124]: 0
with precondition: [V>=1,V1>=0,Out>=0]
* Chain [124]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of fun2(V,V1,Out):
* Chain [128]: 0
with precondition: [Out=0,V>=0,V1>=0]
* Chain [127]: 0
with precondition: [V1=0,Out=0,V>=1]
* Chain [126]: 0
with precondition: [Out=1,V>=1,V1>=1]
* Chain [125]: 0
with precondition: [V>=2,V1>=1,Out>=1]
#### Cost of chains of mod(V,V1,Out):
* Chain [139]: 4
with precondition: [Out=0,V>=0,V1>=0]
* Chain [138]: 4
with precondition: [V=1,V1=1,Out=0]
* Chain [137]: 4
with precondition: [V=Out,V>=0,V1>=0]
* Chain [136]: 4
with precondition: [V=2,V1=0,Out>=2]
* Chain [135]: 4
with precondition: [V=2,V1>=1,Out>=2]
* Chain [134]: 4
with precondition: [V1=0,Out=0,V>=1]
* Chain [133]: 4
with precondition: [V1=0,V=Out,V>=1]
* Chain [132]: 4
with precondition: [V1=0,V>=3,Out>=0]
* Chain [131]: 4
with precondition: [V1=2,Out=0,V>=2]
* Chain [130]: 4
with precondition: [V1=2,V=Out,V>=2]
* Chain [129]: 4
with precondition: [V>=3,V1>=1,Out>=0]
#### Cost of chains of fun7(V,V1,V19,Out):
* Chain [150]: 6
with precondition: [Out=0,V>=0,V1>=0,V19>=0]
* Chain [149]: 7
with precondition: [V+V19+1=Out,V>=0,V1>=0,V19>=1]
* Chain [148]: 7
with precondition: [V=Out,V>=0,V1>=0,V19>=0]
* Chain [147]: 7
with precondition: [V1=0,V+V19+1=Out,V>=0,V19>=3]
* Chain [146]: 6
with precondition: [V1=2,Out=0,V>=0,V19>=2]
* Chain [145]: 7
with precondition: [V1=2,V=Out,V>=0,V19>=2]
* Chain [144]: 7
with precondition: [V1=2,V+V19+1=Out,V>=0,V19>=2]
* Chain [143]: 6
with precondition: [V19=0,Out=0,V>=0,V1>=0]
* Chain [142]: 7
with precondition: [V19=0,V=Out,V>=0,V1>=0]
* Chain [141]: 6
with precondition: [V19=2,Out=0,V>=0,V1>=1]
* Chain [140]: 7
with precondition: [V19=2,V+3=Out,V>=0,V1>=1]
#### Cost of chains of filter(V,V1,Out):
* Chain [[153,154,155,156,157],152]: 34*it(153)+9*it(154)+2
Such that:it(154) =< V1/3
aux(22) =< V1
it(153) =< aux(22)
it(154) =< aux(22)
with precondition: [V>=0,V1>=3,Out>=0,V1>=Out,2*V1>=Out+4]
* Chain [[153,154,155,156,157],151]: 34*it(153)+9*it(154)+1
Such that:it(154) =< V1/3
aux(23) =< V1
it(153) =< aux(23)
it(154) =< aux(23)
with precondition: [V>=0,Out>=0,V1>=Out,2*V1>=Out+2]
* Chain [152]: 2
with precondition: [V1=2,Out=2,V>=0]
* Chain [151]: 1
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of fun5(V,Out):
* Chain [[158],161]: 4*it(158)+18*s(14)+68*s(15)+1
Such that:aux(29) =< V
it(158) =< aux(29)
aux(27) =< it(158)*aux(29)
s(17) =< aux(27)* (1/3)
s(14) =< s(17)
s(15) =< aux(27)
s(14) =< aux(27)
with precondition: [Out>=3,V>=Out]
* Chain [[158],160]: 4*it(158)+18*s(14)+68*s(15)+0
Such that:aux(30) =< V
it(158) =< aux(30)
aux(27) =< it(158)*aux(30)
s(17) =< aux(27)* (1/3)
s(14) =< s(17)
s(15) =< aux(27)
s(14) =< aux(27)
with precondition: [Out>=1,V>=Out+1]
* Chain [[158],159,160]: 4*it(158)+18*s(14)+68*s(15)+3
Such that:aux(31) =< V
it(158) =< aux(31)
aux(27) =< it(158)*aux(31)
s(17) =< aux(27)* (1/3)
s(14) =< s(17)
s(15) =< aux(27)
s(14) =< aux(27)
with precondition: [Out>=2,V>=Out,2*V>=Out+3]
* Chain [161]: 1
with precondition: [V=2,Out=2]
* Chain [160]: 0
with precondition: [Out=0,V>=0]
* Chain [159,160]: 3
with precondition: [Out>=1,V>=Out]
#### Cost of chains of start(V,V1,V19):
* Chain [172]: 500*s(37)+108*s(40)+408*s(41)+126*s(43)+18*s(91)+68*s(92)+10
Such that:aux(33) =< V
aux(34) =< V/3
aux(35) =< V1
aux(36) =< V1/3
s(43) =< aux(34)
s(91) =< aux(36)
s(37) =< aux(33)
s(38) =< s(37)*aux(33)
s(39) =< s(38)* (1/3)
s(40) =< s(39)
s(41) =< s(38)
s(40) =< s(38)
s(43) =< aux(33)
s(92) =< aux(35)
s(91) =< aux(35)
with precondition: [V>=0]
* Chain [171]: 1
with precondition: [V1=1,V>=1]
* Chain [170]: 0
with precondition: [V=1,V1=2]
* Chain [169]: 1
with precondition: [V=1,V1>=0,V19>=0]
* Chain [168]: 4
with precondition: [V=2,V1>=0]
* Chain [167]: 0
with precondition: [V=2,V1=1]
* Chain [166]: 18*s(97)+68*s(98)+10
Such that:aux(37) =< V
aux(38) =< V/3
s(97) =< aux(38)
s(98) =< aux(37)
s(97) =< aux(37)
with precondition: [V1=2,V>=2]
* Chain [165]: 4
with precondition: [V1=0,V>=0]
* Chain [164]: 7
with precondition: [V1=2,V>=0,V19>=2]
* Chain [163]: 7
with precondition: [V19=0,V>=0,V1>=0]
* Chain [162]: 7
with precondition: [V19=2,V>=0,V1>=1]
Closed-form bounds of start(V,V1,V19):
-------------------------------------
* Chain [172] with precondition: [V>=0]
- Upper bound: 500*V+10+444*V*V+nat(V1)*68+42*V+nat(V1/3)*18
- Complexity: n^2
* Chain [171] with precondition: [V1=1,V>=1]
- Upper bound: 1
- Complexity: constant
* Chain [170] with precondition: [V=1,V1=2]
- Upper bound: 0
- Complexity: constant
* Chain [169] with precondition: [V=1,V1>=0,V19>=0]
- Upper bound: 1
- Complexity: constant
* Chain [168] with precondition: [V=2,V1>=0]
- Upper bound: 4
- Complexity: constant
* Chain [167] with precondition: [V=2,V1=1]
- Upper bound: 0
- Complexity: constant
* Chain [166] with precondition: [V1=2,V>=2]
- Upper bound: 74*V+10
- Complexity: n
* Chain [165] with precondition: [V1=0,V>=0]
- Upper bound: 4
- Complexity: constant
* Chain [164] with precondition: [V1=2,V>=0,V19>=2]
- Upper bound: 7
- Complexity: constant
* Chain [163] with precondition: [V19=0,V>=0,V1>=0]
- Upper bound: 7
- Complexity: constant
* Chain [162] with precondition: [V19=2,V>=0,V1>=1]
- Upper bound: 7
- Complexity: constant
### Maximum cost of start(V,V1,V19): max([7,444*V*V+432*V+nat(V1)*68+36*V+nat(V1/3)*18+ (74*V+10)])
Asymptotic class: n^2
* Total analysis performed in 2080 ms.