0 CpxRelTRS
↳1 RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxWeightedTrs
↳5 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳6 CpxTypedWeightedTrs
↳7 CompletionProof (UPPER BOUND(ID), 21 ms)
↳8 CpxTypedWeightedCompleteTrs
↳9 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)
↳10 CpxRNTS
↳11 CompleteCoflocoProof (⇔, 4929 ms)
↳12 BOUNDS(1, n^2)
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#equal(@x, @y) → #eq(@x, @y)
#greater(@x, @y) → #ckgt(#compare(@x, @y))
+(@x, @y) → #add(@x, @y)
firstline(@l) → firstline#1(@l)
firstline#1(::(@x, @xs)) → ::(#abs(#0), firstline(@xs))
firstline#1(nil) → nil
lcs(@l1, @l2) → lcs#1(lcstable(@l1, @l2))
lcs#1(@m) → lcs#2(@m)
lcs#2(::(@l1, @_@2)) → lcs#3(@l1)
lcs#2(nil) → #abs(#0)
lcs#3(::(@len, @_@1)) → @len
lcs#3(nil) → #abs(#0)
lcstable(@l1, @l2) → lcstable#1(@l1, @l2)
lcstable#1(::(@x, @xs), @l2) → lcstable#2(lcstable(@xs, @l2), @l2, @x)
lcstable#1(nil, @l2) → ::(firstline(@l2), nil)
lcstable#2(@m, @l2, @x) → lcstable#3(@m, @l2, @x)
lcstable#3(::(@l, @ls), @l2, @x) → ::(newline(@x, @l, @l2), ::(@l, @ls))
lcstable#3(nil, @l2, @x) → nil
max(@a, @b) → max#1(#greater(@a, @b), @a, @b)
max#1(#false, @a, @b) → @b
max#1(#true, @a, @b) → @a
newline(@y, @lastline, @l) → newline#1(@l, @lastline, @y)
newline#1(::(@x, @xs), @lastline, @y) → newline#2(@lastline, @x, @xs, @y)
newline#1(nil, @lastline, @y) → nil
newline#2(::(@belowVal, @lastline'), @x, @xs, @y) → newline#3(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y)
newline#2(nil, @x, @xs, @y) → nil
newline#3(@nl, @belowVal, @lastline', @x, @y) → newline#4(right(@nl), @belowVal, @lastline', @nl, @x, @y)
newline#4(@rightVal, @belowVal, @lastline', @nl, @x, @y) → newline#5(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y)
newline#5(@diagVal, @belowVal, @nl, @rightVal, @x, @y) → newline#6(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl)
newline#6(@elem, @nl) → ::(@elem, @nl)
newline#7(#false, @belowVal, @diagVal, @rightVal) → max(@belowVal, @rightVal)
newline#7(#true, @belowVal, @diagVal, @rightVal) → +(@diagVal, #pos(#s(#0)))
right(@l) → right#1(@l)
right#1(::(@x, @xs)) → @x
right#1(nil) → #abs(#0)
#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
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@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
#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))
#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)))
#abs(#0) → #0 [1]
#abs(#neg(@x)) → #pos(@x) [1]
#abs(#pos(@x)) → #pos(@x) [1]
#abs(#s(@x)) → #pos(#s(@x)) [1]
#equal(@x, @y) → #eq(@x, @y) [1]
#greater(@x, @y) → #ckgt(#compare(@x, @y)) [1]
+(@x, @y) → #add(@x, @y) [1]
firstline(@l) → firstline#1(@l) [1]
firstline#1(::(@x, @xs)) → ::(#abs(#0), firstline(@xs)) [1]
firstline#1(nil) → nil [1]
lcs(@l1, @l2) → lcs#1(lcstable(@l1, @l2)) [1]
lcs#1(@m) → lcs#2(@m) [1]
lcs#2(::(@l1, @_@2)) → lcs#3(@l1) [1]
lcs#2(nil) → #abs(#0) [1]
lcs#3(::(@len, @_@1)) → @len [1]
lcs#3(nil) → #abs(#0) [1]
lcstable(@l1, @l2) → lcstable#1(@l1, @l2) [1]
lcstable#1(::(@x, @xs), @l2) → lcstable#2(lcstable(@xs, @l2), @l2, @x) [1]
lcstable#1(nil, @l2) → ::(firstline(@l2), nil) [1]
lcstable#2(@m, @l2, @x) → lcstable#3(@m, @l2, @x) [1]
lcstable#3(::(@l, @ls), @l2, @x) → ::(newline(@x, @l, @l2), ::(@l, @ls)) [1]
lcstable#3(nil, @l2, @x) → nil [1]
max(@a, @b) → max#1(#greater(@a, @b), @a, @b) [1]
max#1(#false, @a, @b) → @b [1]
max#1(#true, @a, @b) → @a [1]
newline(@y, @lastline, @l) → newline#1(@l, @lastline, @y) [1]
newline#1(::(@x, @xs), @lastline, @y) → newline#2(@lastline, @x, @xs, @y) [1]
newline#1(nil, @lastline, @y) → nil [1]
newline#2(::(@belowVal, @lastline'), @x, @xs, @y) → newline#3(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y) [1]
newline#2(nil, @x, @xs, @y) → nil [1]
newline#3(@nl, @belowVal, @lastline', @x, @y) → newline#4(right(@nl), @belowVal, @lastline', @nl, @x, @y) [1]
newline#4(@rightVal, @belowVal, @lastline', @nl, @x, @y) → newline#5(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y) [1]
newline#5(@diagVal, @belowVal, @nl, @rightVal, @x, @y) → newline#6(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl) [1]
newline#6(@elem, @nl) → ::(@elem, @nl) [1]
newline#7(#false, @belowVal, @diagVal, @rightVal) → max(@belowVal, @rightVal) [1]
newline#7(#true, @belowVal, @diagVal, @rightVal) → +(@diagVal, #pos(#s(#0))) [1]
right(@l) → right#1(@l) [1]
right#1(::(@x, @xs)) → @x [1]
right#1(nil) → #abs(#0) [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]
#ckgt(#EQ) → #false [0]
#ckgt(#GT) → #true [0]
#ckgt(#LT) → #false [0]
#compare(#0, #0) → #EQ [0]
#compare(#0, #neg(@y)) → #GT [0]
#compare(#0, #pos(@y)) → #LT [0]
#compare(#0, #s(@y)) → #LT [0]
#compare(#neg(@x), #0) → #LT [0]
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x) [0]
#compare(#neg(@x), #pos(@y)) → #LT [0]
#compare(#pos(@x), #0) → #GT [0]
#compare(#pos(@x), #neg(@y)) → #GT [0]
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y) [0]
#compare(#s(@x), #0) → #GT [0]
#compare(#s(@x), #s(@y)) → #compare(@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]
#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]
#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]
| + => plus |
#abs(#0) → #0 [1]
#abs(#neg(@x)) → #pos(@x) [1]
#abs(#pos(@x)) → #pos(@x) [1]
#abs(#s(@x)) → #pos(#s(@x)) [1]
#equal(@x, @y) → #eq(@x, @y) [1]
#greater(@x, @y) → #ckgt(#compare(@x, @y)) [1]
plus(@x, @y) → #add(@x, @y) [1]
firstline(@l) → firstline#1(@l) [1]
firstline#1(::(@x, @xs)) → ::(#abs(#0), firstline(@xs)) [1]
firstline#1(nil) → nil [1]
lcs(@l1, @l2) → lcs#1(lcstable(@l1, @l2)) [1]
lcs#1(@m) → lcs#2(@m) [1]
lcs#2(::(@l1, @_@2)) → lcs#3(@l1) [1]
lcs#2(nil) → #abs(#0) [1]
lcs#3(::(@len, @_@1)) → @len [1]
lcs#3(nil) → #abs(#0) [1]
lcstable(@l1, @l2) → lcstable#1(@l1, @l2) [1]
lcstable#1(::(@x, @xs), @l2) → lcstable#2(lcstable(@xs, @l2), @l2, @x) [1]
lcstable#1(nil, @l2) → ::(firstline(@l2), nil) [1]
lcstable#2(@m, @l2, @x) → lcstable#3(@m, @l2, @x) [1]
lcstable#3(::(@l, @ls), @l2, @x) → ::(newline(@x, @l, @l2), ::(@l, @ls)) [1]
lcstable#3(nil, @l2, @x) → nil [1]
max(@a, @b) → max#1(#greater(@a, @b), @a, @b) [1]
max#1(#false, @a, @b) → @b [1]
max#1(#true, @a, @b) → @a [1]
newline(@y, @lastline, @l) → newline#1(@l, @lastline, @y) [1]
newline#1(::(@x, @xs), @lastline, @y) → newline#2(@lastline, @x, @xs, @y) [1]
newline#1(nil, @lastline, @y) → nil [1]
newline#2(::(@belowVal, @lastline'), @x, @xs, @y) → newline#3(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y) [1]
newline#2(nil, @x, @xs, @y) → nil [1]
newline#3(@nl, @belowVal, @lastline', @x, @y) → newline#4(right(@nl), @belowVal, @lastline', @nl, @x, @y) [1]
newline#4(@rightVal, @belowVal, @lastline', @nl, @x, @y) → newline#5(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y) [1]
newline#5(@diagVal, @belowVal, @nl, @rightVal, @x, @y) → newline#6(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl) [1]
newline#6(@elem, @nl) → ::(@elem, @nl) [1]
newline#7(#false, @belowVal, @diagVal, @rightVal) → max(@belowVal, @rightVal) [1]
newline#7(#true, @belowVal, @diagVal, @rightVal) → plus(@diagVal, #pos(#s(#0))) [1]
right(@l) → right#1(@l) [1]
right#1(::(@x, @xs)) → @x [1]
right#1(nil) → #abs(#0) [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]
#ckgt(#EQ) → #false [0]
#ckgt(#GT) → #true [0]
#ckgt(#LT) → #false [0]
#compare(#0, #0) → #EQ [0]
#compare(#0, #neg(@y)) → #GT [0]
#compare(#0, #pos(@y)) → #LT [0]
#compare(#0, #s(@y)) → #LT [0]
#compare(#neg(@x), #0) → #LT [0]
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x) [0]
#compare(#neg(@x), #pos(@y)) → #LT [0]
#compare(#pos(@x), #0) → #GT [0]
#compare(#pos(@x), #neg(@y)) → #GT [0]
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y) [0]
#compare(#s(@x), #0) → #GT [0]
#compare(#s(@x), #s(@y)) → #compare(@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]
#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]
#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]
#abs(#0) → #0 [1]
#abs(#neg(@x)) → #pos(@x) [1]
#abs(#pos(@x)) → #pos(@x) [1]
#abs(#s(@x)) → #pos(#s(@x)) [1]
#equal(@x, @y) → #eq(@x, @y) [1]
#greater(@x, @y) → #ckgt(#compare(@x, @y)) [1]
plus(@x, @y) → #add(@x, @y) [1]
firstline(@l) → firstline#1(@l) [1]
firstline#1(::(@x, @xs)) → ::(#abs(#0), firstline(@xs)) [1]
firstline#1(nil) → nil [1]
lcs(@l1, @l2) → lcs#1(lcstable(@l1, @l2)) [1]
lcs#1(@m) → lcs#2(@m) [1]
lcs#2(::(@l1, @_@2)) → lcs#3(@l1) [1]
lcs#2(nil) → #abs(#0) [1]
lcs#3(::(@len, @_@1)) → @len [1]
lcs#3(nil) → #abs(#0) [1]
lcstable(@l1, @l2) → lcstable#1(@l1, @l2) [1]
lcstable#1(::(@x, @xs), @l2) → lcstable#2(lcstable(@xs, @l2), @l2, @x) [1]
lcstable#1(nil, @l2) → ::(firstline(@l2), nil) [1]
lcstable#2(@m, @l2, @x) → lcstable#3(@m, @l2, @x) [1]
lcstable#3(::(@l, @ls), @l2, @x) → ::(newline(@x, @l, @l2), ::(@l, @ls)) [1]
lcstable#3(nil, @l2, @x) → nil [1]
max(@a, @b) → max#1(#greater(@a, @b), @a, @b) [1]
max#1(#false, @a, @b) → @b [1]
max#1(#true, @a, @b) → @a [1]
newline(@y, @lastline, @l) → newline#1(@l, @lastline, @y) [1]
newline#1(::(@x, @xs), @lastline, @y) → newline#2(@lastline, @x, @xs, @y) [1]
newline#1(nil, @lastline, @y) → nil [1]
newline#2(::(@belowVal, @lastline'), @x, @xs, @y) → newline#3(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y) [1]
newline#2(nil, @x, @xs, @y) → nil [1]
newline#3(@nl, @belowVal, @lastline', @x, @y) → newline#4(right(@nl), @belowVal, @lastline', @nl, @x, @y) [1]
newline#4(@rightVal, @belowVal, @lastline', @nl, @x, @y) → newline#5(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y) [1]
newline#5(@diagVal, @belowVal, @nl, @rightVal, @x, @y) → newline#6(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl) [1]
newline#6(@elem, @nl) → ::(@elem, @nl) [1]
newline#7(#false, @belowVal, @diagVal, @rightVal) → max(@belowVal, @rightVal) [1]
newline#7(#true, @belowVal, @diagVal, @rightVal) → plus(@diagVal, #pos(#s(#0))) [1]
right(@l) → right#1(@l) [1]
right#1(::(@x, @xs)) → @x [1]
right#1(nil) → #abs(#0) [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]
#ckgt(#EQ) → #false [0]
#ckgt(#GT) → #true [0]
#ckgt(#LT) → #false [0]
#compare(#0, #0) → #EQ [0]
#compare(#0, #neg(@y)) → #GT [0]
#compare(#0, #pos(@y)) → #LT [0]
#compare(#0, #s(@y)) → #LT [0]
#compare(#neg(@x), #0) → #LT [0]
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x) [0]
#compare(#neg(@x), #pos(@y)) → #LT [0]
#compare(#pos(@x), #0) → #GT [0]
#compare(#pos(@x), #neg(@y)) → #GT [0]
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y) [0]
#compare(#s(@x), #0) → #GT [0]
#compare(#s(@x), #s(@y)) → #compare(@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]
#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]
#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]
| #abs :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil #0 :: #0:#neg:#pos:#s::::nil #neg :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil #pos :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil #s :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil #equal :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #false:#true #eq :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #false:#true #greater :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #false:#true #ckgt :: #EQ:#GT:#LT → #false:#true #compare :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #EQ:#GT:#LT plus :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil #add :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil firstline :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil firstline#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil :: :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil nil :: #0:#neg:#pos:#s::::nil lcs :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil lcs#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil lcstable :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil lcs#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil lcs#3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil lcstable#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil lcstable#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil lcstable#3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil newline :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil max :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil max#1 :: #false:#true → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil #false :: #false:#true #true :: #false:#true newline#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil newline#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil newline#3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil newline#4 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil right :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil newline#5 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil newline#6 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil newline#7 :: #false:#true → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil right#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil #pred :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil #succ :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil #and :: #false:#true → #false:#true → #false:#true #EQ :: #EQ:#GT:#LT #GT :: #EQ:#GT:#LT #LT :: #EQ:#GT:#LT |
#add(v0, v1) → null_#add [0]
#and(v0, v1) → null_#and [0]
#ckgt(v0) → null_#ckgt [0]
#compare(v0, v1) → null_#compare [0]
#eq(v0, v1) → null_#eq [0]
#pred(v0) → null_#pred [0]
#succ(v0) → null_#succ [0]
#abs(v0) → null_#abs [0]
firstline#1(v0) → null_firstline#1 [0]
lcs#2(v0) → null_lcs#2 [0]
lcs#3(v0) → null_lcs#3 [0]
lcstable#1(v0, v1) → null_lcstable#1 [0]
lcstable#3(v0, v1, v2) → null_lcstable#3 [0]
max#1(v0, v1, v2) → null_max#1 [0]
newline#1(v0, v1, v2) → null_newline#1 [0]
newline#2(v0, v1, v2, v3) → null_newline#2 [0]
newline#7(v0, v1, v2, v3) → null_newline#7 [0]
right#1(v0) → null_right#1 [0]
null_#add, null_#and, null_#ckgt, null_#compare, null_#eq, null_#pred, null_#succ, null_#abs, null_firstline#1, null_lcs#2, null_lcs#3, null_lcstable#1, null_lcstable#3, null_max#1, null_newline#1, null_newline#2, null_newline#7, null_right#1
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
#0 => 0
nil => 1
#false => 1
#true => 2
#EQ => 1
#GT => 2
#LT => 3
null_#add => 0
null_#and => 0
null_#ckgt => 0
null_#compare => 0
null_#eq => 0
null_#pred => 0
null_#succ => 0
null_#abs => 0
null_firstline#1 => 0
null_lcs#2 => 0
null_lcs#3 => 0
null_lcstable#1 => 0
null_lcstable#3 => 0
null_max#1 => 0
null_newline#1 => 0
null_newline#2 => 0
null_newline#7 => 0
null_right#1 => 0
#abs(z) -{ 1 }→ 0 :|: z = 0
#abs(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
#abs(z) -{ 1 }→ 1 + @x :|: @x >= 0, z = 1 + @x
#abs(z) -{ 1 }→ 1 + (1 + @x) :|: @x >= 0, z = 1 + @x
#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
#ckgt(z) -{ 0 }→ 2 :|: z = 2
#ckgt(z) -{ 0 }→ 1 :|: z = 1
#ckgt(z) -{ 0 }→ 1 :|: z = 3
#ckgt(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
#compare(z, z') -{ 0 }→ 3 :|: z = 0, z' = 1 + @y, @y >= 0
#compare(z, z') -{ 0 }→ 3 :|: @x >= 0, z = 1 + @x, z' = 0
#compare(z, z') -{ 0 }→ 3 :|: @x >= 0, z = 1 + @x, z' = 1 + @y, @y >= 0
#compare(z, z') -{ 0 }→ 2 :|: z = 0, z' = 1 + @y, @y >= 0
#compare(z, z') -{ 0 }→ 2 :|: @x >= 0, z = 1 + @x, z' = 0
#compare(z, z') -{ 0 }→ 2 :|: @x >= 0, z = 1 + @x, z' = 1 + @y, @y >= 0
#compare(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
#compare(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
#compare(z, z') -{ 0 }→ #compare(@x, @y) :|: @x >= 0, z = 1 + @x, z' = 1 + @y, @y >= 0
#compare(z, z') -{ 0 }→ #compare(@y, @x) :|: @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 = 1, z' = 1
#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 = 1 + @x_1 + @x_2, @x_2 >= 0, z' = 1
#eq(z, z') -{ 0 }→ 1 :|: z = 1, @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
#greater(z, z') -{ 1 }→ #ckgt(#compare(@x, @y)) :|: z = @x, @x >= 0, z' = @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)
#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)
firstline(z) -{ 1 }→ firstline#1(@l) :|: z = @l, @l >= 0
firstline#1(z) -{ 1 }→ 1 :|: z = 1
firstline#1(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
firstline#1(z) -{ 1 }→ 1 + #abs(0) + firstline(@xs) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0
lcs(z, z') -{ 1 }→ lcs#1(lcstable(@l1, @l2)) :|: @l1 >= 0, z' = @l2, @l2 >= 0, z = @l1
lcs#1(z) -{ 1 }→ lcs#2(@m) :|: @m >= 0, z = @m
lcs#2(z) -{ 1 }→ lcs#3(@l1) :|: z = 1 + @l1 + @_@2, @l1 >= 0, @_@2 >= 0
lcs#2(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
lcs#2(z) -{ 1 }→ #abs(0) :|: z = 1
lcs#3(z) -{ 1 }→ @len :|: @_@1 >= 0, z = 1 + @len + @_@1, @len >= 0
lcs#3(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
lcs#3(z) -{ 1 }→ #abs(0) :|: z = 1
lcstable(z, z') -{ 1 }→ lcstable#1(@l1, @l2) :|: @l1 >= 0, z' = @l2, @l2 >= 0, z = @l1
lcstable#1(z, z') -{ 1 }→ lcstable#2(lcstable(@xs, @l2), @l2, @x) :|: z' = @l2, @x >= 0, z = 1 + @x + @xs, @l2 >= 0, @xs >= 0
lcstable#1(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
lcstable#1(z, z') -{ 1 }→ 1 + firstline(@l2) + 1 :|: z' = @l2, z = 1, @l2 >= 0
lcstable#2(z, z', z'') -{ 1 }→ lcstable#3(@m, @l2, @x) :|: @m >= 0, z' = @l2, @x >= 0, @l2 >= 0, z = @m, z'' = @x
lcstable#3(z, z', z'') -{ 1 }→ 1 :|: z' = @l2, @x >= 0, z = 1, @l2 >= 0, z'' = @x
lcstable#3(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
lcstable#3(z, z', z'') -{ 1 }→ 1 + newline(@x, @l, @l2) + (1 + @l + @ls) :|: z = 1 + @l + @ls, @ls >= 0, @l >= 0, z' = @l2, @x >= 0, @l2 >= 0, z'' = @x
max(z, z') -{ 1 }→ max#1(#greater(@a, @b), @a, @b) :|: @a >= 0, z = @a, z' = @b, @b >= 0
max#1(z, z', z'') -{ 1 }→ @a :|: z = 2, @a >= 0, z' = @a, @b >= 0, z'' = @b
max#1(z, z', z'') -{ 1 }→ @b :|: @a >= 0, z = 1, z' = @a, @b >= 0, z'' = @b
max#1(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
newline(z, z', z'') -{ 1 }→ newline#1(@l, @lastline, @y) :|: @l >= 0, z'' = @l, @lastline >= 0, z' = @lastline, z = @y, @y >= 0
newline#1(z, z', z'') -{ 1 }→ newline#2(@lastline, @x, @xs, @y) :|: @x >= 0, z = 1 + @x + @xs, @lastline >= 0, z' = @lastline, @xs >= 0, @y >= 0, z'' = @y
newline#1(z, z', z'') -{ 1 }→ 1 :|: @lastline >= 0, z = 1, z' = @lastline, @y >= 0, z'' = @y
newline#1(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
newline#2(z, z', z'', z1) -{ 1 }→ newline#3(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y) :|: @lastline' >= 0, @x >= 0, z1 = @y, z = 1 + @belowVal + @lastline', @xs >= 0, @y >= 0, z' = @x, z'' = @xs, @belowVal >= 0
newline#2(z, z', z'', z1) -{ 1 }→ 1 :|: @x >= 0, z = 1, z1 = @y, @xs >= 0, @y >= 0, z' = @x, z'' = @xs
newline#2(z, z', z'', z1) -{ 0 }→ 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
newline#3(z, z', z'', z1, z2) -{ 1 }→ newline#4(right(@nl), @belowVal, @lastline', @nl, @x, @y) :|: z'' = @lastline', z1 = @x, @lastline' >= 0, @x >= 0, z = @nl, z2 = @y, z' = @belowVal, @y >= 0, @nl >= 0, @belowVal >= 0
newline#4(z, z', z'', z1, z2, z3) -{ 1 }→ newline#5(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y) :|: z'' = @lastline', @lastline' >= 0, @x >= 0, @rightVal >= 0, z1 = @nl, z2 = @x, z = @rightVal, z' = @belowVal, z3 = @y, @y >= 0, @belowVal >= 0, @nl >= 0
newline#5(z, z', z'', z1, z2, z3) -{ 1 }→ newline#6(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl) :|: z = @diagVal, @x >= 0, @rightVal >= 0, z2 = @x, z' = @belowVal, z3 = @y, z'' = @nl, z1 = @rightVal, @diagVal >= 0, @y >= 0, @belowVal >= 0, @nl >= 0
newline#6(z, z') -{ 1 }→ 1 + @elem + @nl :|: @elem >= 0, z' = @nl, @nl >= 0, z = @elem
newline#7(z, z', z'', z1) -{ 1 }→ plus(@diagVal, 1 + (1 + 0)) :|: z = 2, @rightVal >= 0, z' = @belowVal, z1 = @rightVal, @diagVal >= 0, z'' = @diagVal, @belowVal >= 0
newline#7(z, z', z'', z1) -{ 1 }→ max(@belowVal, @rightVal) :|: @rightVal >= 0, z = 1, z' = @belowVal, z1 = @rightVal, @diagVal >= 0, z'' = @diagVal, @belowVal >= 0
newline#7(z, z', z'', z1) -{ 0 }→ 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
plus(z, z') -{ 1 }→ #add(@x, @y) :|: z = @x, @x >= 0, z' = @y, @y >= 0
right(z) -{ 1 }→ right#1(@l) :|: z = @l, @l >= 0
right#1(z) -{ 1 }→ @x :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0
right#1(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
right#1(z) -{ 1 }→ #abs(0) :|: z = 1
| eq(start(V, V3, V26, V51, V60, V66),0,[fun(V, Out)],[V >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[fun1(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[fun3(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[plus(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[firstline(V, Out)],[V >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[fun7(V, Out)],[V >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[lcs(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[fun8(V, Out)],[V >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[fun9(V, Out)],[V >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[fun10(V, Out)],[V >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[lcstable(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[fun11(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[fun12(V, V3, V26, Out)],[V >= 0,V3 >= 0,V26 >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[fun13(V, V3, V26, Out)],[V >= 0,V3 >= 0,V26 >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[max(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[fun14(V, V3, V26, Out)],[V >= 0,V3 >= 0,V26 >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[newline(V, V3, V26, Out)],[V >= 0,V3 >= 0,V26 >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[fun15(V, V3, V26, Out)],[V >= 0,V3 >= 0,V26 >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[fun16(V, V3, V26, V51, Out)],[V >= 0,V3 >= 0,V26 >= 0,V51 >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[fun17(V, V3, V26, V51, V60, Out)],[V >= 0,V3 >= 0,V26 >= 0,V51 >= 0,V60 >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[fun18(V, V3, V26, V51, V60, V66, Out)],[V >= 0,V3 >= 0,V26 >= 0,V51 >= 0,V60 >= 0,V66 >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[fun19(V, V3, V26, V51, V60, V66, Out)],[V >= 0,V3 >= 0,V26 >= 0,V51 >= 0,V60 >= 0,V66 >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[fun20(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[fun21(V, V3, V26, V51, Out)],[V >= 0,V3 >= 0,V26 >= 0,V51 >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[right(V, Out)],[V >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[fun22(V, Out)],[V >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[fun6(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[fun25(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[fun4(V, Out)],[V >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[fun5(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[fun2(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[fun23(V, Out)],[V >= 0]). eq(start(V, V3, V26, V51, V60, V66),0,[fun24(V, Out)],[V >= 0]). eq(fun(V, Out),1,[],[Out = 0,V = 0]). eq(fun(V, Out),1,[],[Out = 1 + V1,V1 >= 0,V = 1 + V1]). eq(fun(V, Out),1,[],[Out = 2 + V2,V2 >= 0,V = 1 + V2]). eq(fun1(V, V3, Out),1,[fun2(V4, V5, Ret)],[Out = Ret,V = V4,V4 >= 0,V3 = V5,V5 >= 0]). eq(fun3(V, V3, Out),1,[fun5(V6, V7, Ret0),fun4(Ret0, Ret1)],[Out = Ret1,V = V6,V6 >= 0,V3 = V7,V7 >= 0]). eq(plus(V, V3, Out),1,[fun6(V8, V9, Ret2)],[Out = Ret2,V = V8,V8 >= 0,V3 = V9,V9 >= 0]). eq(firstline(V, Out),1,[fun7(V10, Ret3)],[Out = Ret3,V = V10,V10 >= 0]). eq(fun7(V, Out),1,[fun(0, Ret01),firstline(V11, Ret11)],[Out = 1 + Ret01 + Ret11,V12 >= 0,V = 1 + V11 + V12,V11 >= 0]). eq(fun7(V, Out),1,[],[Out = 1,V = 1]). eq(lcs(V, V3, Out),1,[lcstable(V13, V14, Ret02),fun8(Ret02, Ret4)],[Out = Ret4,V13 >= 0,V3 = V14,V14 >= 0,V = V13]). eq(fun8(V, Out),1,[fun9(V15, Ret5)],[Out = Ret5,V15 >= 0,V = V15]). eq(fun9(V, Out),1,[fun10(V16, Ret6)],[Out = Ret6,V = 1 + V16 + V17,V16 >= 0,V17 >= 0]). eq(fun9(V, Out),1,[fun(0, Ret7)],[Out = Ret7,V = 1]). eq(fun10(V, Out),1,[],[Out = V18,V19 >= 0,V = 1 + V18 + V19,V18 >= 0]). eq(fun10(V, Out),1,[fun(0, Ret8)],[Out = Ret8,V = 1]). eq(lcstable(V, V3, Out),1,[fun11(V20, V21, Ret9)],[Out = Ret9,V20 >= 0,V3 = V21,V21 >= 0,V = V20]). eq(fun11(V, V3, Out),1,[lcstable(V22, V23, Ret03),fun12(Ret03, V23, V24, Ret10)],[Out = Ret10,V3 = V23,V24 >= 0,V = 1 + V22 + V24,V23 >= 0,V22 >= 0]). eq(fun11(V, V3, Out),1,[firstline(V25, Ret011)],[Out = 2 + Ret011,V3 = V25,V = 1,V25 >= 0]). eq(fun12(V, V3, V26, Out),1,[fun13(V27, V28, V29, Ret12)],[Out = Ret12,V27 >= 0,V3 = V28,V29 >= 0,V28 >= 0,V = V27,V26 = V29]). eq(fun13(V, V3, V26, Out),1,[newline(V30, V31, V32, Ret012)],[Out = 2 + Ret012 + V31 + V33,V = 1 + V31 + V33,V33 >= 0,V31 >= 0,V3 = V32,V30 >= 0,V32 >= 0,V26 = V30]). eq(fun13(V, V3, V26, Out),1,[],[Out = 1,V3 = V34,V35 >= 0,V = 1,V34 >= 0,V26 = V35]). eq(max(V, V3, Out),1,[fun3(V36, V37, Ret04),fun14(Ret04, V36, V37, Ret13)],[Out = Ret13,V36 >= 0,V = V36,V3 = V37,V37 >= 0]). eq(fun14(V, V3, V26, Out),1,[],[Out = V38,V39 >= 0,V = 1,V3 = V39,V38 >= 0,V26 = V38]). eq(fun14(V, V3, V26, Out),1,[],[Out = V40,V = 2,V40 >= 0,V3 = V40,V41 >= 0,V26 = V41]). eq(newline(V, V3, V26, Out),1,[fun15(V42, V43, V44, Ret14)],[Out = Ret14,V42 >= 0,V26 = V42,V43 >= 0,V3 = V43,V = V44,V44 >= 0]). eq(fun15(V, V3, V26, Out),1,[fun16(V45, V46, V47, V48, Ret15)],[Out = Ret15,V46 >= 0,V = 1 + V46 + V47,V45 >= 0,V3 = V45,V47 >= 0,V48 >= 0,V26 = V48]). eq(fun15(V, V3, V26, Out),1,[],[Out = 1,V49 >= 0,V = 1,V3 = V49,V50 >= 0,V26 = V50]). eq(fun16(V, V3, V26, V51, Out),1,[newline(V52, V53, V54, Ret05),fun17(Ret05, V55, V53, V56, V52, Ret16)],[Out = Ret16,V53 >= 0,V56 >= 0,V51 = V52,V = 1 + V53 + V55,V54 >= 0,V52 >= 0,V3 = V56,V26 = V54,V55 >= 0]). eq(fun16(V, V3, V26, V51, Out),1,[],[Out = 1,V57 >= 0,V = 1,V51 = V58,V59 >= 0,V58 >= 0,V3 = V57,V26 = V59]). eq(fun17(V, V3, V26, V51, V60, Out),1,[right(V61, Ret06),fun18(Ret06, V62, V63, V61, V64, V65, Ret17)],[Out = Ret17,V26 = V63,V51 = V64,V63 >= 0,V64 >= 0,V = V61,V60 = V65,V3 = V62,V65 >= 0,V61 >= 0,V62 >= 0]). eq(fun18(V, V3, V26, V51, V60, V66, Out),1,[right(V67, Ret07),fun19(Ret07, V68, V69, V70, V71, V72, Ret18)],[Out = Ret18,V26 = V67,V67 >= 0,V71 >= 0,V70 >= 0,V51 = V69,V60 = V71,V = V70,V3 = V68,V66 = V72,V72 >= 0,V68 >= 0,V69 >= 0]). eq(fun19(V, V3, V26, V51, V60, V66, Out),1,[fun1(V73, V74, Ret00),fun21(Ret00, V75, V76, V77, Ret08),fun20(Ret08, V78, Ret19)],[Out = Ret19,V = V76,V73 >= 0,V77 >= 0,V60 = V73,V3 = V75,V66 = V74,V26 = V78,V51 = V77,V76 >= 0,V74 >= 0,V75 >= 0,V78 >= 0]). eq(fun20(V, V3, Out),1,[],[Out = 1 + V79 + V80,V79 >= 0,V3 = V80,V80 >= 0,V = V79]). eq(fun21(V, V3, V26, V51, Out),1,[max(V81, V82, Ret20)],[Out = Ret20,V82 >= 0,V = 1,V3 = V81,V51 = V82,V83 >= 0,V26 = V83,V81 >= 0]). eq(fun21(V, V3, V26, V51, Out),1,[plus(V84, 1 + (1 + 0), Ret21)],[Out = Ret21,V = 2,V85 >= 0,V3 = V86,V51 = V85,V84 >= 0,V26 = V84,V86 >= 0]). eq(right(V, Out),1,[fun22(V87, Ret22)],[Out = Ret22,V = V87,V87 >= 0]). eq(fun22(V, Out),1,[],[Out = V88,V88 >= 0,V = 1 + V88 + V89,V89 >= 0]). eq(fun22(V, Out),1,[fun(0, Ret23)],[Out = Ret23,V = 1]). eq(fun6(V, V3, Out),0,[],[Out = V90,V3 = V90,V = 0,V90 >= 0]). eq(fun6(V, V3, Out),0,[fun23(V91, Ret24)],[Out = Ret24,V = 2,V3 = V91,V91 >= 0]). eq(fun6(V, V3, Out),0,[fun6(1 + (1 + V92), V93, Ret09),fun23(Ret09, Ret25)],[Out = Ret25,V92 >= 0,V3 = V93,V = 3 + V92,V93 >= 0]). eq(fun6(V, V3, Out),0,[fun24(V94, Ret26)],[Out = Ret26,V = 2,V3 = V94,V94 >= 0]). eq(fun6(V, V3, Out),0,[fun6(1 + (1 + V95), V96, Ret010),fun24(Ret010, Ret27)],[Out = Ret27,V95 >= 0,V3 = V96,V = 3 + V95,V96 >= 0]). eq(fun25(V, V3, Out),0,[],[Out = 1,V = 1,V3 = 1]). eq(fun25(V, V3, Out),0,[],[Out = 1,V3 = 2,V = 1]). eq(fun25(V, V3, Out),0,[],[Out = 1,V = 2,V3 = 1]). eq(fun25(V, V3, Out),0,[],[Out = 2,V = 2,V3 = 2]). eq(fun4(V, Out),0,[],[Out = 1,V = 1]). eq(fun4(V, Out),0,[],[Out = 2,V = 2]). eq(fun4(V, Out),0,[],[Out = 1,V = 3]). eq(fun5(V, V3, Out),0,[],[Out = 1,V = 0,V3 = 0]). eq(fun5(V, V3, Out),0,[],[Out = 2,V = 0,V3 = 1 + V97,V97 >= 0]). eq(fun5(V, V3, Out),0,[],[Out = 3,V = 0,V3 = 1 + V98,V98 >= 0]). eq(fun5(V, V3, Out),0,[],[Out = 3,V99 >= 0,V = 1 + V99,V3 = 0]). eq(fun5(V, V3, Out),0,[fun5(V100, V101, Ret28)],[Out = Ret28,V101 >= 0,V = 1 + V101,V3 = 1 + V100,V100 >= 0]). eq(fun5(V, V3, Out),0,[],[Out = 3,V102 >= 0,V = 1 + V102,V3 = 1 + V103,V103 >= 0]). eq(fun5(V, V3, Out),0,[],[Out = 2,V104 >= 0,V = 1 + V104,V3 = 0]). eq(fun5(V, V3, Out),0,[],[Out = 2,V105 >= 0,V = 1 + V105,V3 = 1 + V106,V106 >= 0]). eq(fun5(V, V3, Out),0,[fun5(V107, V108, Ret29)],[Out = Ret29,V107 >= 0,V = 1 + V107,V3 = 1 + V108,V108 >= 0]). eq(fun2(V, V3, Out),0,[],[Out = 2,V = 0,V3 = 0]). eq(fun2(V, V3, Out),0,[],[Out = 1,V = 0,V3 = 1 + V109,V109 >= 0]). eq(fun2(V, V3, Out),0,[],[Out = 1,V110 >= 0,V = 1 + V110,V3 = 0]). eq(fun2(V, V3, Out),0,[fun2(V111, V112, Ret30)],[Out = Ret30,V111 >= 0,V = 1 + V111,V3 = 1 + V112,V112 >= 0]). eq(fun2(V, V3, Out),0,[],[Out = 1,V113 >= 0,V = 1 + V113,V3 = 1 + V114,V114 >= 0]). eq(fun2(V, V3, Out),0,[fun2(V115, V116, Ret013),fun2(V117, V118, Ret110),fun25(Ret013, Ret110, Ret31)],[Out = Ret31,V115 >= 0,V = 1 + V115 + V117,V116 >= 0,V117 >= 0,V118 >= 0,V3 = 1 + V116 + V118]). eq(fun2(V, V3, Out),0,[],[Out = 1,V119 >= 0,V = 1 + V119 + V120,V120 >= 0,V3 = 1]). eq(fun2(V, V3, Out),0,[],[Out = 1,V = 1,V121 >= 0,V122 >= 0,V3 = 1 + V121 + V122]). eq(fun2(V, V3, Out),0,[],[Out = 2,V = 1,V3 = 1]). eq(fun23(V, Out),0,[],[Out = 2,V = 0]). eq(fun23(V, Out),0,[],[Out = 3 + V123,V123 >= 0,V = 2 + V123]). eq(fun23(V, Out),0,[],[Out = 0,V = 2]). eq(fun23(V, Out),0,[],[Out = 2 + V124,V124 >= 0,V = 3 + V124]). eq(fun24(V, Out),0,[],[Out = 2,V = 0]). eq(fun24(V, Out),0,[],[Out = 0,V = 2]). eq(fun24(V, Out),0,[],[Out = 2 + V125,V125 >= 0,V = 3 + V125]). eq(fun24(V, Out),0,[],[Out = 3 + V126,V126 >= 0,V = 2 + V126]). eq(fun6(V, V3, Out),0,[],[Out = 0,V127 >= 0,V128 >= 0,V = V127,V3 = V128]). eq(fun25(V, V3, Out),0,[],[Out = 0,V129 >= 0,V130 >= 0,V = V129,V3 = V130]). eq(fun4(V, Out),0,[],[Out = 0,V131 >= 0,V = V131]). eq(fun5(V, V3, Out),0,[],[Out = 0,V132 >= 0,V133 >= 0,V = V132,V3 = V133]). eq(fun2(V, V3, Out),0,[],[Out = 0,V134 >= 0,V135 >= 0,V = V134,V3 = V135]). eq(fun23(V, Out),0,[],[Out = 0,V136 >= 0,V = V136]). eq(fun24(V, Out),0,[],[Out = 0,V137 >= 0,V = V137]). eq(fun(V, Out),0,[],[Out = 0,V138 >= 0,V = V138]). eq(fun7(V, Out),0,[],[Out = 0,V139 >= 0,V = V139]). eq(fun9(V, Out),0,[],[Out = 0,V140 >= 0,V = V140]). eq(fun10(V, Out),0,[],[Out = 0,V141 >= 0,V = V141]). eq(fun11(V, V3, Out),0,[],[Out = 0,V142 >= 0,V143 >= 0,V = V142,V3 = V143]). eq(fun13(V, V3, V26, Out),0,[],[Out = 0,V144 >= 0,V26 = V145,V146 >= 0,V = V144,V3 = V146,V145 >= 0]). eq(fun14(V, V3, V26, Out),0,[],[Out = 0,V147 >= 0,V26 = V148,V149 >= 0,V = V147,V3 = V149,V148 >= 0]). eq(fun15(V, V3, V26, Out),0,[],[Out = 0,V150 >= 0,V26 = V151,V152 >= 0,V = V150,V3 = V152,V151 >= 0]). eq(fun16(V, V3, V26, V51, Out),0,[],[Out = 0,V51 = V153,V154 >= 0,V26 = V155,V156 >= 0,V = V154,V3 = V156,V155 >= 0,V153 >= 0]). eq(fun21(V, V3, V26, V51, Out),0,[],[Out = 0,V51 = V157,V158 >= 0,V26 = V159,V160 >= 0,V = V158,V3 = V160,V159 >= 0,V157 >= 0]). eq(fun22(V, Out),0,[],[Out = 0,V161 >= 0,V = V161]). input_output_vars(fun(V,Out),[V],[Out]). input_output_vars(fun1(V,V3,Out),[V,V3],[Out]). input_output_vars(fun3(V,V3,Out),[V,V3],[Out]). input_output_vars(plus(V,V3,Out),[V,V3],[Out]). input_output_vars(firstline(V,Out),[V],[Out]). input_output_vars(fun7(V,Out),[V],[Out]). input_output_vars(lcs(V,V3,Out),[V,V3],[Out]). input_output_vars(fun8(V,Out),[V],[Out]). input_output_vars(fun9(V,Out),[V],[Out]). input_output_vars(fun10(V,Out),[V],[Out]). input_output_vars(lcstable(V,V3,Out),[V,V3],[Out]). input_output_vars(fun11(V,V3,Out),[V,V3],[Out]). input_output_vars(fun12(V,V3,V26,Out),[V,V3,V26],[Out]). input_output_vars(fun13(V,V3,V26,Out),[V,V3,V26],[Out]). input_output_vars(max(V,V3,Out),[V,V3],[Out]). input_output_vars(fun14(V,V3,V26,Out),[V,V3,V26],[Out]). input_output_vars(newline(V,V3,V26,Out),[V,V3,V26],[Out]). input_output_vars(fun15(V,V3,V26,Out),[V,V3,V26],[Out]). input_output_vars(fun16(V,V3,V26,V51,Out),[V,V3,V26,V51],[Out]). input_output_vars(fun17(V,V3,V26,V51,V60,Out),[V,V3,V26,V51,V60],[Out]). input_output_vars(fun18(V,V3,V26,V51,V60,V66,Out),[V,V3,V26,V51,V60,V66],[Out]). input_output_vars(fun19(V,V3,V26,V51,V60,V66,Out),[V,V3,V26,V51,V60,V66],[Out]). input_output_vars(fun20(V,V3,Out),[V,V3],[Out]). input_output_vars(fun21(V,V3,V26,V51,Out),[V,V3,V26,V51],[Out]). input_output_vars(right(V,Out),[V],[Out]). input_output_vars(fun22(V,Out),[V],[Out]). input_output_vars(fun6(V,V3,Out),[V,V3],[Out]). input_output_vars(fun25(V,V3,Out),[V,V3],[Out]). input_output_vars(fun4(V,Out),[V],[Out]). input_output_vars(fun5(V,V3,Out),[V,V3],[Out]). input_output_vars(fun2(V,V3,Out),[V,V3],[Out]). input_output_vars(fun23(V,Out),[V],[Out]). input_output_vars(fun24(V,Out),[V],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. non_recursive : [fun/2]
1. recursive : [firstline/2,fun7/2]
2. non_recursive : [fun25/3]
3. recursive [non_tail,multiple] : [fun2/3]
4. non_recursive : [fun1/3]
5. non_recursive : [fun10/2]
6. non_recursive : [fun20/3]
7. non_recursive : [fun14/4]
8. non_recursive : [fun4/2]
9. recursive : [fun5/3]
10. non_recursive : [fun3/3]
11. non_recursive : [max/3]
12. non_recursive : [fun23/2]
13. non_recursive : [fun24/2]
14. recursive [non_tail] : [fun6/3]
15. non_recursive : [plus/3]
16. non_recursive : [fun21/5]
17. non_recursive : [fun19/7]
18. non_recursive : [fun22/2]
19. non_recursive : [right/2]
20. non_recursive : [fun18/7]
21. non_recursive : [fun17/6]
22. recursive [non_tail] : [fun15/4,fun16/5,newline/4]
23. non_recursive : [fun13/4]
24. non_recursive : [fun12/4]
25. recursive [non_tail] : [fun11/3,lcstable/3]
26. non_recursive : [fun9/2]
27. non_recursive : [fun8/2]
28. non_recursive : [lcs/3]
29. non_recursive : [start/6]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into fun/2
1. SCC is partially evaluated into firstline/2
2. SCC is partially evaluated into fun25/3
3. SCC is partially evaluated into fun2/3
4. SCC is completely evaluated into other SCCs
5. SCC is partially evaluated into fun10/2
6. SCC is completely evaluated into other SCCs
7. SCC is partially evaluated into fun14/4
8. SCC is partially evaluated into fun4/2
9. SCC is partially evaluated into fun5/3
10. SCC is partially evaluated into fun3/3
11. SCC is partially evaluated into max/3
12. SCC is partially evaluated into fun23/2
13. SCC is partially evaluated into fun24/2
14. SCC is partially evaluated into fun6/3
15. SCC is completely evaluated into other SCCs
16. SCC is partially evaluated into fun21/5
17. SCC is partially evaluated into fun19/7
18. SCC is partially evaluated into fun22/2
19. SCC is completely evaluated into other SCCs
20. SCC is partially evaluated into fun18/7
21. SCC is partially evaluated into fun17/6
22. SCC is partially evaluated into newline/4
23. SCC is partially evaluated into fun13/4
24. SCC is completely evaluated into other SCCs
25. SCC is partially evaluated into lcstable/3
26. SCC is partially evaluated into fun9/2
27. SCC is completely evaluated into other SCCs
28. SCC is partially evaluated into lcs/3
29. SCC is partially evaluated into start/6
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations fun/2
* CE 55 is refined into CE [119]
* CE 56 is refined into CE [120]
* CE 54 is refined into CE [121]
* CE 57 is refined into CE [122]
### Cost equations --> "Loop" of fun/2
* CEs [119] --> Loop 77
* CEs [120] --> Loop 78
* CEs [121,122] --> Loop 79
### Ranking functions of CR fun(V,Out)
#### Partial ranking functions of CR fun(V,Out)
### Specialization of cost equations firstline/2
* CE 41 is refined into CE [123]
* CE 39 is refined into CE [124]
* CE 40 is refined into CE [125]
### Cost equations --> "Loop" of firstline/2
* CEs [124] --> Loop 80
* CEs [125] --> Loop 81
* CEs [123] --> Loop 82
### Ranking functions of CR firstline(V,Out)
* RF of phase [82]: [V]
#### Partial ranking functions of CR firstline(V,Out)
* Partial RF of phase [82]:
- RF of loop [82:1]:
V
### Specialization of cost equations fun25/3
* CE 96 is refined into CE [126]
* CE 95 is refined into CE [127]
* CE 94 is refined into CE [128]
* CE 93 is refined into CE [129]
* CE 92 is refined into CE [130]
### Cost equations --> "Loop" of fun25/3
* CEs [126] --> Loop 83
* CEs [127] --> Loop 84
* CEs [128] --> Loop 85
* CEs [129] --> Loop 86
* CEs [130] --> Loop 87
### Ranking functions of CR fun25(V,V3,Out)
#### Partial ranking functions of CR fun25(V,V3,Out)
### Specialization of cost equations fun2/3
* CE 62 is refined into CE [131]
* CE 65 is refined into CE [132]
* CE 60 is refined into CE [133]
* CE 64 is refined into CE [134]
* CE 59 is refined into CE [135]
* CE 58 is refined into CE [136]
* CE 63 is refined into CE [137,138,139,140,141]
* CE 61 is refined into CE [142]
### Cost equations --> "Loop" of fun2/3
* CEs [142] --> Loop 88
* CEs [140] --> Loop 89
* CEs [139] --> Loop 90
* CEs [138] --> Loop 91
* CEs [137] --> Loop 92
* CEs [141] --> Loop 93
* CEs [131] --> Loop 94
* CEs [132] --> Loop 95
* CEs [133] --> Loop 96
* CEs [134] --> Loop 97
* CEs [135] --> Loop 98
* CEs [136] --> Loop 99
### Ranking functions of CR fun2(V,V3,Out)
* RF of phase [88,89,90,91,92,93]: [V,V3]
#### Partial ranking functions of CR fun2(V,V3,Out)
* Partial RF of phase [88,89,90,91,92,93]:
- RF of loop [88:1,89:1,89:2,90:1,90:2,91:1,91:2,92:1,92:2,93:1,93:2]:
V
V3
### Specialization of cost equations fun10/2
* CE 77 is refined into CE [143]
* CE 79 is refined into CE [144]
* CE 78 is refined into CE [145]
### Cost equations --> "Loop" of fun10/2
* CEs [143] --> Loop 100
* CEs [144,145] --> Loop 101
### Ranking functions of CR fun10(V,Out)
#### Partial ranking functions of CR fun10(V,Out)
### Specialization of cost equations fun14/4
* CE 83 is refined into CE [146]
* CE 82 is refined into CE [147]
* CE 81 is refined into CE [148]
### Cost equations --> "Loop" of fun14/4
* CEs [146] --> Loop 102
* CEs [147] --> Loop 103
* CEs [148] --> Loop 104
### Ranking functions of CR fun14(V,V3,V26,Out)
#### Partial ranking functions of CR fun14(V,V3,V26,Out)
### Specialization of cost equations fun4/2
* CE 100 is refined into CE [149]
* CE 99 is refined into CE [150]
* CE 98 is refined into CE [151]
* CE 97 is refined into CE [152]
### Cost equations --> "Loop" of fun4/2
* CEs [149] --> Loop 105
* CEs [150] --> Loop 106
* CEs [151] --> Loop 107
* CEs [152] --> Loop 108
### Ranking functions of CR fun4(V,Out)
#### Partial ranking functions of CR fun4(V,Out)
### Specialization of cost equations fun5/3
* CE 106 is refined into CE [153]
* CE 108 is refined into CE [154]
* CE 110 is refined into CE [155]
* CE 104 is refined into CE [156]
* CE 107 is refined into CE [157]
* CE 103 is refined into CE [158]
* CE 102 is refined into CE [159]
* CE 101 is refined into CE [160]
* CE 105 is refined into CE [161]
* CE 109 is refined into CE [162]
### Cost equations --> "Loop" of fun5/3
* CEs [161] --> Loop 109
* CEs [162] --> Loop 110
* CEs [153] --> Loop 111
* CEs [154] --> Loop 112
* CEs [155] --> Loop 113
* CEs [156] --> Loop 114
* CEs [157] --> Loop 115
* CEs [158] --> Loop 116
* CEs [159] --> Loop 117
* CEs [160] --> Loop 118
### Ranking functions of CR fun5(V,V3,Out)
* RF of phase [109,110]: [V/2+V3/2-1/2]
#### Partial ranking functions of CR fun5(V,V3,Out)
* Partial RF of phase [109,110]:
- RF of loop [109:1]:
V/2+V3/2-1/2
- RF of loop [110:1]:
V depends on loops [109:1]
V3 depends on loops [109:1]
### Specialization of cost equations fun3/3
* CE 66 is refined into CE [163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179]
### Cost equations --> "Loop" of fun3/3
* CEs [176] --> Loop 119
* CEs [174,178] --> Loop 120
* CEs [175] --> Loop 121
* CEs [169] --> Loop 122
* CEs [171] --> Loop 123
* CEs [170,172] --> Loop 124
* CEs [165] --> Loop 125
* CEs [167] --> Loop 126
* CEs [166,168] --> Loop 127
* CEs [163] --> Loop 128
* CEs [164,173,177,179] --> Loop 129
### Ranking functions of CR fun3(V,V3,Out)
#### Partial ranking functions of CR fun3(V,V3,Out)
### Specialization of cost equations max/3
* CE 80 is refined into CE [180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196]
### Cost equations --> "Loop" of max/3
* CEs [193] --> Loop 130
* CEs [195] --> Loop 131
* CEs [192] --> Loop 132
* CEs [190] --> Loop 133
* CEs [187,188,189,191] --> Loop 134
* CEs [183] --> Loop 135
* CEs [184,185,186] --> Loop 136
* CEs [180,181,182,194,196] --> Loop 137
### Ranking functions of CR max(V,V3,Out)
#### Partial ranking functions of CR max(V,V3,Out)
### Specialization of cost equations fun23/2
* CE 114 is refined into CE [197]
* CE 112 is refined into CE [198]
* CE 113 is refined into CE [199]
* CE 111 is refined into CE [200]
### Cost equations --> "Loop" of fun23/2
* CEs [197] --> Loop 138
* CEs [198] --> Loop 139
* CEs [199] --> Loop 140
* CEs [200] --> Loop 141
### Ranking functions of CR fun23(V,Out)
#### Partial ranking functions of CR fun23(V,Out)
### Specialization of cost equations fun24/2
* CE 117 is refined into CE [201]
* CE 118 is refined into CE [202]
* CE 116 is refined into CE [203]
* CE 115 is refined into CE [204]
### Cost equations --> "Loop" of fun24/2
* CEs [201] --> Loop 142
* CEs [202] --> Loop 143
* CEs [203] --> Loop 144
* CEs [204] --> Loop 145
### Ranking functions of CR fun24(V,Out)
#### Partial ranking functions of CR fun24(V,Out)
### Specialization of cost equations fun6/3
* CE 72 is refined into CE [205]
* CE 68 is refined into CE [206,207,208,209]
* CE 70 is refined into CE [210,211,212,213]
* CE 67 is refined into CE [214]
* CE 69 is refined into CE [215,216,217,218]
* CE 71 is refined into CE [219,220,221,222]
### Cost equations --> "Loop" of fun6/3
* CEs [217,221] --> Loop 146
* CEs [218,222] --> Loop 147
* CEs [215,219] --> Loop 148
* CEs [216,220] --> Loop 149
* CEs [209,213] --> Loop 150
* CEs [208,212] --> Loop 151
* CEs [205,207,211] --> Loop 152
* CEs [206,210] --> Loop 153
* CEs [214] --> Loop 154
### Ranking functions of CR fun6(V,V3,Out)
* RF of phase [146,147,148,149]: [V-2]
#### Partial ranking functions of CR fun6(V,V3,Out)
* Partial RF of phase [146,147,148,149]:
- RF of loop [146:1,147:1,148:1,149:1]:
V-2
### Specialization of cost equations fun21/5
* CE 88 is refined into CE [223]
* CE 87 is refined into CE [224,225,226,227,228]
* CE 86 is refined into CE [229,230,231,232,233,234,235]
### Cost equations --> "Loop" of fun21/5
* CEs [227,228] --> Loop 155
* CEs [226] --> Loop 156
* CEs [225] --> Loop 157
* CEs [224] --> Loop 158
* CEs [235] --> Loop 159
* CEs [234] --> Loop 160
* CEs [233] --> Loop 161
* CEs [232] --> Loop 162
* CEs [223,229,231] --> Loop 163
* CEs [230] --> Loop 164
### Ranking functions of CR fun21(V,V3,V26,V51,Out)
#### Partial ranking functions of CR fun21(V,V3,V26,V51,Out)
### Specialization of cost equations fun19/7
* CE 85 is refined into CE [236,237,238,239,240,241,242,243,244,245,246,247,248,249,250,251,252,253,254,255,256,257,258,259,260,261,262,263,264,265]
### Cost equations --> "Loop" of fun19/7
* CEs [254] --> Loop 165
* CEs [250,265] --> Loop 166
* CEs [249,264] --> Loop 167
* CEs [259] --> Loop 168
* CEs [258] --> Loop 169
* CEs [257] --> Loop 170
* CEs [245] --> Loop 171
* CEs [244] --> Loop 172
* CEs [243] --> Loop 173
* CEs [240] --> Loop 174
* CEs [236,239,248,253,260,263] --> Loop 175
* CEs [247,262] --> Loop 176
* CEs [256] --> Loop 177
* CEs [242] --> Loop 178
* CEs [246,261] --> Loop 179
* CEs [255] --> Loop 180
* CEs [241] --> Loop 181
* CEs [252] --> Loop 182
* CEs [238] --> Loop 183
* CEs [251] --> Loop 184
* CEs [237] --> Loop 185
### Ranking functions of CR fun19(V,V3,V26,V51,V60,V66,Out)
#### Partial ranking functions of CR fun19(V,V3,V26,V51,V60,V66,Out)
### Specialization of cost equations fun22/2
* CE 89 is refined into CE [266]
* CE 91 is refined into CE [267]
* CE 90 is refined into CE [268]
### Cost equations --> "Loop" of fun22/2
* CEs [266] --> Loop 186
* CEs [267,268] --> Loop 187
### Ranking functions of CR fun22(V,Out)
#### Partial ranking functions of CR fun22(V,Out)
### Specialization of cost equations fun18/7
* CE 84 is refined into CE [269,270,271,272,273,274,275,276,277,278,279,280,281,282,283,284,285,286,287,288,289,290,291,292,293,294,295,296,297,298,299,300,301,302,303,304]
### Cost equations --> "Loop" of fun18/7
* CEs [304] --> Loop 188
* CEs [283,302] --> Loop 189
* CEs [284,303] --> Loop 190
* CEs [288] --> Loop 191
* CEs [270,286] --> Loop 192
* CEs [281,300] --> Loop 193
* CEs [282,301] --> Loop 194
* CEs [277,280,296,299] --> Loop 195
* CEs [278,297] --> Loop 196
* CEs [279,298] --> Loop 197
* CEs [295] --> Loop 198
* CEs [287] --> Loop 199
* CEs [269,285] --> Loop 200
* CEs [273,291] --> Loop 201
* CEs [272,290] --> Loop 202
* CEs [271,289] --> Loop 203
* CEs [276,294] --> Loop 204
* CEs [275,293] --> Loop 205
* CEs [274,292] --> Loop 206
### Ranking functions of CR fun18(V,V3,V26,V51,V60,V66,Out)
#### Partial ranking functions of CR fun18(V,V3,V26,V51,V60,V66,Out)
### Specialization of cost equations fun17/6
* CE 53 is refined into CE [305,306,307,308,309,310,311,312,313,314,315,316,317,318,319,320,321,322,323,324,325,326,327,328,329,330,331,332,333]
### Cost equations --> "Loop" of fun17/6
* CEs [331] --> Loop 207
* CEs [314,333] --> Loop 208
* CEs [307,317,332] --> Loop 209
* CEs [311,328] --> Loop 210
* CEs [312,329] --> Loop 211
* CEs [313,330] --> Loop 212
* CEs [326] --> Loop 213
* CEs [306,316,327] --> Loop 214
* CEs [324] --> Loop 215
* CEs [305,315,325] --> Loop 216
* CEs [310,323] --> Loop 217
* CEs [308,321] --> Loop 218
* CEs [309,322] --> Loop 219
* CEs [320] --> Loop 220
* CEs [319] --> Loop 221
* CEs [318] --> Loop 222
### Ranking functions of CR fun17(V,V3,V26,V51,V60,Out)
#### Partial ranking functions of CR fun17(V,V3,V26,V51,V60,Out)
### Specialization of cost equations newline/4
* CE 48 is refined into CE [334]
* CE 51 is refined into CE [335]
* CE 52 is refined into CE [336]
* CE 49 is refined into CE [337]
* CE 50 is refined into CE [338,339,340,341,342,343,344,345,346,347,348,349,350,351,352,353]
### Cost equations --> "Loop" of newline/4
* CEs [352] --> Loop 223
* CEs [353] --> Loop 224
* CEs [351] --> Loop 225
* CEs [348] --> Loop 226
* CEs [349] --> Loop 227
* CEs [350] --> Loop 228
* CEs [345] --> Loop 229
* CEs [344] --> Loop 230
* CEs [340] --> Loop 231
* CEs [338] --> Loop 232
* CEs [347] --> Loop 233
* CEs [346] --> Loop 234
* CEs [343] --> Loop 235
* CEs [341] --> Loop 236
* CEs [342] --> Loop 237
* CEs [339] --> Loop 238
* CEs [334,335] --> Loop 239
* CEs [336] --> Loop 240
* CEs [337] --> Loop 241
### Ranking functions of CR newline(V,V3,V26,Out)
* RF of phase [223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238]: [V3,V26]
#### Partial ranking functions of CR newline(V,V3,V26,Out)
* Partial RF of phase [223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238]:
- RF of loop [223:1,224:1,225:1,226:1,227:1,231:1,238:1]:
V26/2-1/2
- RF of loop [223:1,235:1]:
V3-4
- RF of loop [224:1,225:1,229:1,230:1]:
V3/2-1/2
- RF of loop [226:1,236:1]:
V3-3
- RF of loop [227:1,228:1,231:1,232:1,237:1,238:1]:
V3
- RF of loop [228:1,229:1,230:1,232:1,235:1,236:1,237:1]:
V26
- RF of loop [233:1,234:1]:
V3-1
V26-1
### Specialization of cost equations fun13/4
* CE 47 is refined into CE [354]
* CE 45 is refined into CE [355,356,357]
* CE 46 is refined into CE [358]
### Cost equations --> "Loop" of fun13/4
* CEs [355] --> Loop 242
* CEs [357] --> Loop 243
* CEs [354] --> Loop 244
* CEs [356] --> Loop 245
* CEs [358] --> Loop 246
### Ranking functions of CR fun13(V,V3,V26,Out)
#### Partial ranking functions of CR fun13(V,V3,V26,Out)
### Specialization of cost equations lcstable/3
* CE 44 is refined into CE [359,360,361,362,363]
* CE 42 is refined into CE [364]
* CE 43 is refined into CE [365,366]
### Cost equations --> "Loop" of lcstable/3
* CEs [364] --> Loop 247
* CEs [365] --> Loop 248
* CEs [366] --> Loop 249
* CEs [363] --> Loop 250
* CEs [362] --> Loop 251
* CEs [359] --> Loop 252
* CEs [361] --> Loop 253
* CEs [360] --> Loop 254
### Ranking functions of CR lcstable(V,V3,Out)
* RF of phase [250,251,254]: [V]
* RF of phase [252]: [V]
* RF of phase [253]: [V]
#### Partial ranking functions of CR lcstable(V,V3,Out)
* Partial RF of phase [250,251,254]:
- RF of loop [250:1,251:1,254:1]:
V
* Partial RF of phase [252]:
- RF of loop [252:1]:
V
* Partial RF of phase [253]:
- RF of loop [253:1]:
V
### Specialization of cost equations fun9/2
* CE 76 is refined into CE [367]
* CE 74 is refined into CE [368,369]
* CE 75 is refined into CE [370]
### Cost equations --> "Loop" of fun9/2
* CEs [369] --> Loop 255
* CEs [367,368,370] --> Loop 256
### Ranking functions of CR fun9(V,Out)
#### Partial ranking functions of CR fun9(V,Out)
### Specialization of cost equations lcs/3
* CE 73 is refined into CE [371,372,373,374,375,376,377]
### Cost equations --> "Loop" of lcs/3
* CEs [377] --> Loop 257
* CEs [374] --> Loop 258
* CEs [371,372,373,375,376] --> Loop 259
### Ranking functions of CR lcs(V,V3,Out)
#### Partial ranking functions of CR lcs(V,V3,Out)
### Specialization of cost equations start/6
* CE 6 is refined into CE [378]
* CE 2 is refined into CE [379]
* CE 3 is refined into CE [380,381]
* CE 4 is refined into CE [382,383,384,385,386,387,388,389,390,391,392,393,394]
* CE 5 is refined into CE [395]
* CE 7 is refined into CE [396,397,398,399,400,401,402,403,404,405,406,407,408,409,410,411,412,413,414,415,416,417,418,419,420,421,422,423,424,425,426,427,428,429,430,431]
* CE 8 is refined into CE [432,433,434,435,436,437,438,439,440,441,442,443,444,445,446,447,448,449,450,451,452,453,454,455,456,457,458,459,460,461,462,463,464,465,466,467]
* CE 9 is refined into CE [468]
* CE 10 is refined into CE [469,470]
* CE 11 is refined into CE [471,472,473]
* CE 12 is refined into CE [474,475,476,477,478,479]
* CE 13 is refined into CE [480,481,482,483,484,485,486,487,488,489]
* CE 14 is refined into CE [490,491,492,493,494,495,496,497]
* CE 15 is refined into CE [498,499]
* CE 16 is refined into CE [500,501,502]
* CE 17 is refined into CE [503,504]
* CE 18 is refined into CE [505,506]
* CE 19 is refined into CE [507,508]
* CE 20 is refined into CE [509,510,511,512]
* CE 21 is refined into CE [513,514,515,516,517]
* CE 22 is refined into CE [518,519,520,521,522]
* CE 23 is refined into CE [523,524,525,526,527,528,529]
* CE 24 is refined into CE [530,531,532]
* CE 25 is refined into CE [533,534,535]
* CE 26 is refined into CE [536,537,538,539,540,541,542,543,544,545,546,547,548,549,550,551]
* CE 27 is refined into CE [552,553,554,555,556,557,558,559,560,561,562,563,564,565,566,567,568,569,570]
* CE 28 is refined into CE [571,572,573,574,575,576,577,578,579,580,581,582,583,584,585,586,587,588,589,590]
* CE 29 is refined into CE [591,592,593,594,595,596,597,598,599]
* CE 30 is refined into CE [600,601]
* CE 31 is refined into CE [602,603]
* CE 32 is refined into CE [604,605,606,607,608,609,610,611]
* CE 33 is refined into CE [612,613,614,615,616]
* CE 34 is refined into CE [617,618,619,620]
* CE 35 is refined into CE [621,622,623,624,625,626,627,628,629]
* CE 36 is refined into CE [630,631,632,633,634,635]
* CE 37 is refined into CE [636,637,638,639]
* CE 38 is refined into CE [640,641,642,643]
### Cost equations --> "Loop" of start/6
* CEs [487,527,627] --> Loop 260
* CEs [561,562] --> Loop 261
* CEs [544,545,583,584] --> Loop 262
* CEs [558,559,560,581] --> Loop 263
* CEs [542,579,580] --> Loop 264
* CEs [539,540,541,578] --> Loop 265
* CEs [433,440,441,452,462,543] --> Loop 266
* CEs [397,399,400,401,404,405,416,422,423,424,426] --> Loop 267
* CEs [382,386,391] --> Loop 268
* CEs [378,514,519] --> Loop 269
* CEs [577] --> Loop 270
* CEs [556] --> Loop 271
* CEs [563,564,576,585,586,587] --> Loop 272
* CEs [537] --> Loop 273
* CEs [555] --> Loop 274
* CEs [575] --> Loop 275
* CEs [451,453,454,455,456,457,534] --> Loop 276
* CEs [432,435,436,437,438,439,448,449,450,458,459,460,461,477,484,485,486,494,525,526,536,538,557,608,624,625,633] --> Loop 277
* CEs [619] --> Loop 278
* CEs [412,413,414,415,491,492,493,531,573,574,596,597,598,599,605,606,607,614,615,618] --> Loop 279
* CEs [380,381,468,500,509,510,513,518,530,591,592,594,595,612,613,617] --> Loop 280
* CEs [379,383,384,385,387,388,389,390,392,393,394,395,396,398,402,403,406,407,408,409,410,411,417,418,419,420,421,425,427,428,429,430,431,434,442,443,444,445,446,447,463,464,465,466,467,469,470,471,472,473,474,475,476,478,479,480,481,482,483,488,489,490,495,496,497,498,499,501,502,503,504,505,506,507,508,511,512,515,516,517,520,521,522,523,524,528,529,532,533,535,546,547,548,549,550,551,552,553,554,565,566,567,568,569,570,571,572,582,588,589,590,593,600,601,602,603,604,609,610,611,616,620,621,622,623,626,628,629,630,631,632,634,635,636,637,638,639,640,641,642,643] --> Loop 281
### Ranking functions of CR start(V,V3,V26,V51,V60,V66)
#### Partial ranking functions of CR start(V,V3,V26,V51,V60,V66)
Computing Bounds
=====================================
#### Cost of chains of fun(V,Out):
* Chain [79]: 1
with precondition: [Out=0,V>=0]
* Chain [78]: 1
with precondition: [V+1=Out,V>=1]
* Chain [77]: 1
with precondition: [V=Out,V>=1]
#### Cost of chains of firstline(V,Out):
* Chain [[82],81]: 3*it(82)+2
Such that:it(82) =< V
with precondition: [Out>=2,V>=Out]
* Chain [[82],80]: 3*it(82)+1
Such that:it(82) =< V
with precondition: [Out>=1,V>=Out]
* Chain [81]: 2
with precondition: [V=1,Out=1]
* Chain [80]: 1
with precondition: [Out=0,V>=0]
#### Cost of chains of fun25(V,V3,Out):
* Chain [87]: 0
with precondition: [V=1,V3=1,Out=1]
* Chain [86]: 0
with precondition: [V=1,V3=2,Out=1]
* Chain [85]: 0
with precondition: [V=2,V3=1,Out=1]
* Chain [84]: 0
with precondition: [V=2,V3=2,Out=2]
* Chain [83]: 0
with precondition: [Out=0,V>=0,V3>=0]
#### Cost of chains of fun2(V,V3,Out):
* Chain [99]: 0
with precondition: [V=0,V3=0,Out=2]
* Chain [98]: 0
with precondition: [V=0,Out=1,V3>=1]
* Chain [97]: 0
with precondition: [V=1,V3=1,Out=2]
* Chain [96]: 0
with precondition: [V3=0,Out=1,V>=1]
* Chain [95]: 0
with precondition: [Out=0,V>=0,V3>=0]
* Chain [94]: 0
with precondition: [Out=1,V>=1,V3>=1]
* Chain [multiple([88,89,90,91,92,93],[[99],[98],[97],[96],[95],[94]])]: 0
with precondition: [2>=Out,V>=1,V3>=1,Out>=0]
#### Cost of chains of fun10(V,Out):
* Chain [101]: 2
with precondition: [Out=0,V>=0]
* Chain [100]: 1
with precondition: [Out>=0,V>=Out+1]
#### Cost of chains of fun14(V,V3,V26,Out):
* Chain [104]: 1
with precondition: [V=1,V26=Out,V3>=0,V26>=0]
* Chain [103]: 1
with precondition: [V=2,V3=Out,V3>=0,V26>=0]
* Chain [102]: 0
with precondition: [Out=0,V>=0,V3>=0,V26>=0]
#### Cost of chains of fun4(V,Out):
* Chain [108]: 0
with precondition: [V=1,Out=1]
* Chain [107]: 0
with precondition: [V=2,Out=2]
* Chain [106]: 0
with precondition: [V=3,Out=1]
* Chain [105]: 0
with precondition: [Out=0,V>=0]
#### Cost of chains of fun5(V,V3,Out):
* Chain [[109,110],118]: 0
with precondition: [Out=1,V3=V,V3>=1]
* Chain [[109,110],117]: 0
with precondition: [Out=2,V>=1,V3>=1,V+V3>=3]
* Chain [[109,110],116]: 0
with precondition: [Out=3,V>=1,V3>=1,V+V3>=3]
* Chain [[109,110],115]: 0
with precondition: [Out=2,V>=1,V3>=1,V+V3>=3]
* Chain [[109,110],114]: 0
with precondition: [Out=3,V>=1,V3>=1,V+V3>=3]
* Chain [[109,110],113]: 0
with precondition: [Out=0,V>=1,V3>=1]
* Chain [[109,110],112]: 0
with precondition: [Out=2,V>=2,V3>=2]
* Chain [[109,110],111]: 0
with precondition: [Out=3,V>=2,V3>=2]
* Chain [118]: 0
with precondition: [V=0,V3=0,Out=1]
* Chain [117]: 0
with precondition: [V=0,Out=2,V3>=1]
* Chain [116]: 0
with precondition: [V=0,Out=3,V3>=1]
* Chain [115]: 0
with precondition: [V3=0,Out=2,V>=1]
* Chain [114]: 0
with precondition: [V3=0,Out=3,V>=1]
* Chain [113]: 0
with precondition: [Out=0,V>=0,V3>=0]
* Chain [112]: 0
with precondition: [Out=2,V>=1,V3>=1]
* Chain [111]: 0
with precondition: [Out=3,V>=1,V3>=1]
#### Cost of chains of fun3(V,V3,Out):
* Chain [129]: 1
with precondition: [Out=0,V>=0,V3>=0]
* Chain [128]: 1
with precondition: [V=0,V3=0,Out=1]
* Chain [127]: 1
with precondition: [V=0,Out=0,V3>=1]
* Chain [126]: 1
with precondition: [V=0,Out=1,V3>=1]
* Chain [125]: 1
with precondition: [V=0,Out=2,V3>=1]
* Chain [124]: 1
with precondition: [V3=0,Out=0,V>=1]
* Chain [123]: 1
with precondition: [V3=0,Out=1,V>=1]
* Chain [122]: 1
with precondition: [V3=0,Out=2,V>=1]
* Chain [121]: 1
with precondition: [Out=0,V=V3,V>=1]
* Chain [120]: 1
with precondition: [Out=1,V>=1,V3>=1]
* Chain [119]: 1
with precondition: [Out=2,V>=1,V3>=1]
#### Cost of chains of max(V,V3,Out):
* Chain [137]: 3
with precondition: [Out=0,V>=0,V3>=0]
* Chain [136]: 3
with precondition: [V=0,Out=0,V3>=1]
* Chain [135]: 3
with precondition: [V=0,V3=Out,V3>=1]
* Chain [134]: 3
with precondition: [V3=0,Out=0,V>=1]
* Chain [133]: 3
with precondition: [V3=0,V=Out,V>=1]
* Chain [132]: 2
with precondition: [Out=0,V=V3,V>=1]
* Chain [131]: 3
with precondition: [V=Out,V>=1,V3>=1]
* Chain [130]: 3
with precondition: [V3=Out,V>=1,V3>=1]
#### Cost of chains of fun23(V,Out):
* Chain [141]: 0
with precondition: [V=0,Out=2]
* Chain [140]: 0
with precondition: [Out=0,V>=0]
* Chain [139]: 0
with precondition: [V+1=Out,V>=2]
* Chain [138]: 0
with precondition: [V=Out+1,V>=3]
#### Cost of chains of fun24(V,Out):
* Chain [145]: 0
with precondition: [V=0,Out=2]
* Chain [144]: 0
with precondition: [Out=0,V>=0]
* Chain [143]: 0
with precondition: [V+1=Out,V>=2]
* Chain [142]: 0
with precondition: [V=Out+1,V>=3]
#### Cost of chains of fun6(V,V3,Out):
* Chain [[146,147,148,149],153]: 0
with precondition: [V3=0,V>=3,Out>=0,V>=Out]
* Chain [[146,147,148,149],152]: 0
with precondition: [V>=3,V3>=0,Out>=0,V>=Out+1]
* Chain [[146,147,148,149],151]: 0
with precondition: [V>=3,V3>=2,Out>=0,V+V3>=Out+1]
* Chain [[146,147,148,149],150]: 0
with precondition: [V>=3,V3>=3,Out>=0,V+V3>=Out+3]
* Chain [154]: 0
with precondition: [V=0,V3=Out,V3>=0]
* Chain [153]: 0
with precondition: [V=2,V3=0,Out=2]
* Chain [152]: 0
with precondition: [Out=0,V>=0,V3>=0]
* Chain [151]: 0
with precondition: [V=2,V3+1=Out,V3>=2]
* Chain [150]: 0
with precondition: [V=2,V3=Out+1,V3>=3]
#### Cost of chains of fun21(V,V3,V26,V51,Out):
* Chain [164]: 4
with precondition: [V=1,V3=0,V51=Out,V26>=0,V51>=1]
* Chain [163]: 4
with precondition: [Out=0,V>=0,V3>=0,V26>=0,V51>=0]
* Chain [162]: 4
with precondition: [V=1,V51=0,V3=Out,V3>=1,V26>=0]
* Chain [161]: 3
with precondition: [V=1,Out=0,V3=V51,V3>=1,V26>=0]
* Chain [160]: 4
with precondition: [V=1,V3=Out,V3>=1,V26>=0,V51>=1]
* Chain [159]: 4
with precondition: [V=1,V51=Out,V3>=1,V26>=0,V51>=1]
* Chain [158]: 2
with precondition: [V=2,V26=0,Out=2,V3>=0,V51>=0]
* Chain [157]: 2
with precondition: [V=2,V26=2,Out=3,V3>=0,V51>=0]
* Chain [156]: 2
with precondition: [V=2,Out=0,V3>=0,V26>=0,V51>=0]
* Chain [155]: 2
with precondition: [V=2,V3>=0,V26>=3,V51>=0,Out>=0,V26+1>=Out]
#### Cost of chains of fun19(V,V3,V26,V51,V60,V66,Out):
* Chain [185]: 5
with precondition: [V=0,V60=0,V66=0,V26+3=Out,V3>=0,V26>=0,V51>=0]
* Chain [184]: 5
with precondition: [V=0,V26+3=Out,V3>=0,V26>=0,V51>=0,V60>=1,V66>=1]
* Chain [183]: 5
with precondition: [V=2,V60=0,V66=0,V26+4=Out,V3>=0,V26>=0,V51>=0]
* Chain [182]: 5
with precondition: [V=2,V26+4=Out,V3>=0,V26>=0,V51>=0,V60>=1,V66>=1]
* Chain [181]: 7
with precondition: [V3=0,V60=0,V26+V51+1=Out,V>=0,V26>=0,V51>=1,V66>=1]
* Chain [180]: 7
with precondition: [V3=0,V66=0,V26+V51+1=Out,V>=0,V26>=0,V51>=1,V60>=1]
* Chain [179]: 7
with precondition: [V3=0,V26+V51+1=Out,V>=0,V26>=0,V51>=1,V60>=1,V66>=1]
* Chain [178]: 7
with precondition: [V51=0,V60=0,V3+V26+1=Out,V>=0,V3>=1,V26>=0,V66>=1]
* Chain [177]: 7
with precondition: [V51=0,V66=0,V3+V26+1=Out,V>=0,V3>=1,V26>=0,V60>=1]
* Chain [176]: 7
with precondition: [V51=0,V3+V26+1=Out,V>=0,V3>=1,V26>=0,V60>=1,V66>=1]
* Chain [175]: 7
with precondition: [V26+1=Out,V>=0,V3>=0,V26>=0,V51>=0,V60>=0,V66>=0]
* Chain [174]: 5
with precondition: [V60=0,V66=0,V>=3,V3>=0,V26>=0,V51>=0,Out>=V26+1,V+V26+2>=Out]
* Chain [173]: 7
with precondition: [V60=0,V26+1=Out,V>=0,V3>=0,V26>=0,V51>=0,V66>=1]
* Chain [172]: 7
with precondition: [V60=0,V3+V26+1=Out,V>=0,V3>=1,V26>=0,V51>=1,V66>=1]
* Chain [171]: 7
with precondition: [V60=0,V26+V51+1=Out,V>=0,V3>=1,V26>=0,V51>=1,V66>=1]
* Chain [170]: 7
with precondition: [V66=0,V26+1=Out,V>=0,V3>=0,V26>=0,V51>=0,V60>=1]
* Chain [169]: 7
with precondition: [V66=0,V3+V26+1=Out,V>=0,V3>=1,V26>=0,V51>=1,V60>=1]
* Chain [168]: 7
with precondition: [V66=0,V26+V51+1=Out,V>=0,V3>=1,V26>=0,V51>=1,V60>=1]
* Chain [167]: 7
with precondition: [V3+V26+1=Out,V>=0,V3>=1,V26>=0,V51>=1,V60>=1,V66>=1]
* Chain [166]: 7
with precondition: [V26+V51+1=Out,V>=0,V3>=1,V26>=0,V51>=1,V60>=1,V66>=1]
* Chain [165]: 5
with precondition: [V>=3,V3>=0,V26>=0,V51>=0,V60>=1,V66>=1,Out>=V26+1,V+V26+2>=Out]
#### Cost of chains of fun22(V,Out):
* Chain [187]: 2
with precondition: [Out=0,V>=0]
* Chain [186]: 1
with precondition: [Out>=0,V>=Out+1]
#### Cost of chains of fun18(V,V3,V26,V51,V60,V66,Out):
* Chain [206]: 11
with precondition: [V=0,V60=0,V3+V51+1=Out,V3>=1,V26>=0,V51>=0,V66>=1]
* Chain [205]: 11
with precondition: [V=0,V66=0,V3+V51+1=Out,V3>=1,V26>=0,V51>=0,V60>=1]
* Chain [204]: 11
with precondition: [V=0,V3+V51+1=Out,V3>=1,V26>=0,V51>=0,V60>=1,V66>=1]
* Chain [203]: 11
with precondition: [V3=0,V60=0,V+V51+1=Out,V>=1,V26>=0,V51>=0,V66>=1]
* Chain [202]: 11
with precondition: [V3=0,V66=0,V+V51+1=Out,V>=1,V26>=0,V51>=0,V60>=1]
* Chain [201]: 11
with precondition: [V3=0,V+V51+1=Out,V>=1,V26>=0,V51>=0,V60>=1,V66>=1]
* Chain [200]: 9
with precondition: [V60=0,V66=0,V51+3=Out,V>=0,V3>=0,V26>=0,V51>=0]
* Chain [199]: 8
with precondition: [V60=0,V66=0,V51+4=Out,V>=0,V3>=0,V26>=3,V51>=0]
* Chain [198]: 8
with precondition: [V60=0,V66=0,V>=0,V3>=0,V26>=4,V51>=0,Out>=V51+1,V26+V51+1>=Out]
* Chain [197]: 11
with precondition: [V60=0,V+V51+1=Out,V>=1,V3>=1,V26>=0,V51>=0,V66>=1]
* Chain [196]: 11
with precondition: [V60=0,V3+V51+1=Out,V>=1,V3>=1,V26>=0,V51>=0,V66>=1]
* Chain [195]: 11
with precondition: [V51+1=Out,V>=0,V3>=0,V26>=0,V51>=0,V60>=0,V66>=0]
* Chain [194]: 11
with precondition: [V66=0,V+V51+1=Out,V>=1,V3>=1,V26>=0,V51>=0,V60>=1]
* Chain [193]: 11
with precondition: [V66=0,V3+V51+1=Out,V>=1,V3>=1,V26>=0,V51>=0,V60>=1]
* Chain [192]: 9
with precondition: [V51+3=Out,V>=0,V3>=0,V26>=0,V51>=0,V60>=1,V66>=1]
* Chain [191]: 8
with precondition: [V51+4=Out,V>=0,V3>=0,V26>=3,V51>=0,V60>=1,V66>=1]
* Chain [190]: 11
with precondition: [V+V51+1=Out,V>=1,V3>=1,V26>=0,V51>=0,V60>=1,V66>=1]
* Chain [189]: 11
with precondition: [V3+V51+1=Out,V>=1,V3>=1,V26>=0,V51>=0,V60>=1,V66>=1]
* Chain [188]: 8
with precondition: [V>=0,V3>=0,V26>=4,V51>=0,V60>=1,V66>=1,Out>=V51+1,V26+V51+1>=Out]
#### Cost of chains of fun17(V,V3,V26,V51,V60,Out):
* Chain [222]: 14
with precondition: [V3=0,V51=0,V26>=0,V60>=1,Out>=V+2,2*V>=Out]
* Chain [221]: 14
with precondition: [V3=0,V60=0,V26>=0,V51>=1,Out>=V+2,2*V>=Out]
* Chain [220]: 14
with precondition: [V3=0,V26>=0,V51>=1,V60>=1,Out>=V+2,2*V>=Out]
* Chain [219]: 13
with precondition: [V51=0,V60=0,V+3=Out,V>=0,V3>=0,V26>=0]
* Chain [218]: 12
with precondition: [V51=0,V60=0,V+4=Out,V>=0,V3>=0,V26>=3]
* Chain [217]: 12
with precondition: [V51=0,V60=0,V>=0,V3>=0,V26>=4,Out>=V+1,V+V26+1>=Out]
* Chain [216]: 15
with precondition: [V51=0,V+V3+1=Out,V>=0,V3>=1,V26>=0,V60>=1]
* Chain [215]: 14
with precondition: [V51=0,V3>=1,V26>=0,V60>=1,Out>=V+2,2*V>=Out]
* Chain [214]: 15
with precondition: [V60=0,V+V3+1=Out,V>=0,V3>=1,V26>=0,V51>=1]
* Chain [213]: 14
with precondition: [V60=0,V3>=1,V26>=0,V51>=1,Out>=V+2,2*V>=Out]
* Chain [212]: 15
with precondition: [V+1=Out,V>=0,V3>=0,V26>=0,V51>=0,V60>=0]
* Chain [211]: 13
with precondition: [V+3=Out,V>=0,V3>=0,V26>=0,V51>=1,V60>=1]
* Chain [210]: 12
with precondition: [V+4=Out,V>=0,V3>=0,V26>=3,V51>=1,V60>=1]
* Chain [209]: 15
with precondition: [V+V3+1=Out,V>=0,V3>=1,V26>=0,V51>=1,V60>=1]
* Chain [208]: 12
with precondition: [V>=0,V3>=0,V26>=4,V51>=1,V60>=1,Out>=V+1,V+V26+1>=Out]
* Chain [207]: 14
with precondition: [V3>=1,V26>=0,V51>=1,V60>=1,Out>=V+2,2*V>=Out]
#### Cost of chains of newline(V,V3,V26,Out):
* Chain [[223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238],241]: 80*it(223)+70*it(224)+81*it(228)+35*it(229)+3
Such that:aux(42) =< V3
aux(43) =< V3/2
aux(44) =< V26
aux(45) =< V26/2
it(223) =< aux(42)
it(224) =< aux(42)
it(228) =< aux(42)
it(229) =< aux(42)
it(224) =< aux(43)
it(229) =< aux(43)
it(223) =< aux(44)
it(224) =< aux(44)
it(228) =< aux(44)
it(229) =< aux(44)
it(223) =< aux(45)
it(224) =< aux(45)
with precondition: [V>=0,V3>=2,V26>=2,Out>=2]
* Chain [[223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238],240]: 80*it(223)+70*it(224)+81*it(228)+35*it(229)+2
Such that:aux(46) =< V3
aux(47) =< V3/2
aux(48) =< V26
aux(49) =< V26/2
it(223) =< aux(46)
it(224) =< aux(46)
it(228) =< aux(46)
it(229) =< aux(46)
it(224) =< aux(47)
it(229) =< aux(47)
it(223) =< aux(48)
it(224) =< aux(48)
it(228) =< aux(48)
it(229) =< aux(48)
it(223) =< aux(49)
it(224) =< aux(49)
with precondition: [V>=0,V3>=1,V26>=2,Out>=2]
* Chain [[223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238],239]: 80*it(223)+70*it(224)+81*it(228)+35*it(229)+2
Such that:aux(50) =< V3
aux(51) =< V3/2
aux(52) =< V26
aux(53) =< V26/2
it(223) =< aux(50)
it(224) =< aux(50)
it(228) =< aux(50)
it(229) =< aux(50)
it(224) =< aux(51)
it(229) =< aux(51)
it(223) =< aux(52)
it(224) =< aux(52)
it(228) =< aux(52)
it(229) =< aux(52)
it(223) =< aux(53)
it(224) =< aux(53)
with precondition: [V>=0,V3>=1,V26>=1,Out>=1]
* Chain [241]: 3
with precondition: [V3=1,Out=1,V>=0,V26>=1]
* Chain [240]: 2
with precondition: [V26=1,Out=1,V>=0,V3>=0]
* Chain [239]: 2
with precondition: [Out=0,V>=0,V3>=0,V26>=0]
#### Cost of chains of fun13(V,V3,V26,Out):
* Chain [246]: 1
with precondition: [V=1,Out=1,V3>=0,V26>=0]
* Chain [245]: 3
with precondition: [V3=1,V+2=Out,V>=1,V26>=0]
* Chain [244]: 0
with precondition: [Out=0,V>=0,V3>=0,V26>=0]
* Chain [243]: 3
with precondition: [V+1=Out,V>=1,V3>=0,V26>=0]
* Chain [242]: 240*s(31)+210*s(32)+243*s(33)+105*s(34)+4
Such that:s(27) =< V
s(28) =< V/2
s(29) =< V3
s(30) =< V3/2
s(31) =< s(27)
s(32) =< s(27)
s(33) =< s(27)
s(34) =< s(27)
s(32) =< s(28)
s(34) =< s(28)
s(31) =< s(29)
s(32) =< s(29)
s(33) =< s(29)
s(34) =< s(29)
s(31) =< s(30)
s(32) =< s(30)
with precondition: [V>=2,V3>=1,V26>=0,Out>=V+2]
#### Cost of chains of lcstable(V,V3,Out):
* Chain [[253],[250,251,254],249]: 22*it(250)+450*s(49)+348*s(51)+3
Such that:aux(58) =< V3
aux(63) =< V
it(250) =< aux(63)
aux(59) =< it(250)*aux(58)
s(53) =< aux(59)* (1/2)
s(49) =< aux(59)
s(51) =< aux(59)
s(49) =< s(53)
with precondition: [Out=0,V>=3,V3>=0]
* Chain [[253],[250,251,254],248]: 22*it(250)+450*s(49)+348*s(51)+6*s(56)+4
Such that:aux(65) =< V3
aux(66) =< V
it(250) =< aux(66)
s(56) =< aux(65)
aux(59) =< it(250)*aux(65)
s(53) =< aux(59)* (1/2)
s(49) =< aux(59)
s(51) =< aux(59)
s(49) =< s(53)
with precondition: [Out=0,V>=3,V3>=1]
* Chain [[253],249]: 3*it(253)+3
Such that:it(253) =< V
with precondition: [Out=0,V>=2,V3>=0]
* Chain [[253],248]: 3*it(253)+6*s(56)+4
Such that:it(253) =< V
s(55) =< V3
s(56) =< s(55)
with precondition: [Out=0,V>=2,V3>=1]
* Chain [[253],247]: 3*it(253)+1
Such that:it(253) =< V
with precondition: [Out=0,V>=1,V3>=0]
* Chain [[250,251,254],249]: 19*it(250)+450*s(49)+348*s(51)+3
Such that:aux(58) =< V3
aux(62) =< V
it(250) =< aux(62)
aux(59) =< it(250)*aux(58)
s(53) =< aux(59)* (1/2)
s(49) =< aux(59)
s(51) =< aux(59)
s(49) =< s(53)
with precondition: [V>=2,V3>=0,Out>=3]
* Chain [[250,251,254],248]: 19*it(250)+450*s(49)+348*s(51)+6*s(56)+4
Such that:aux(64) =< V
aux(65) =< V3
s(56) =< aux(65)
it(250) =< aux(64)
aux(59) =< it(250)*aux(65)
s(53) =< aux(59)* (1/2)
s(49) =< aux(59)
s(51) =< aux(59)
s(49) =< s(53)
with precondition: [V>=2,V3>=1,Out>=4]
* Chain [249]: 3
with precondition: [V=1,Out=2,V3>=0]
* Chain [248]: 6*s(56)+4
Such that:s(55) =< V3
s(56) =< s(55)
with precondition: [V=1,Out>=3,V3+2>=Out]
* Chain [247]: 1
with precondition: [Out=0,V>=0,V3>=0]
#### Cost of chains of fun9(V,Out):
* Chain [256]: 3
with precondition: [Out=0,V>=0]
* Chain [255]: 2
with precondition: [Out>=0,V>=Out+2]
#### Cost of chains of lcs(V,V3,Out):
* Chain [259]: 24*s(93)+91*s(96)+1800*s(100)+1392*s(101)+9
Such that:aux(71) =< V
aux(72) =< V3
s(96) =< aux(71)
s(93) =< aux(72)
s(98) =< s(96)*aux(72)
s(99) =< s(98)* (1/2)
s(100) =< s(98)
s(101) =< s(98)
s(100) =< s(99)
with precondition: [Out=0,V>=0,V3>=0]
* Chain [258]: 6*s(111)+8
Such that:s(110) =< V3
s(111) =< s(110)
with precondition: [V=1,V3>=1,Out>=0,V3>=Out]
* Chain [257]: 6*s(114)+38*s(115)+900*s(118)+696*s(119)+8
Such that:s(112) =< V
s(113) =< V3
s(114) =< s(113)
s(115) =< s(112)
s(116) =< s(115)*s(113)
s(117) =< s(116)* (1/2)
s(118) =< s(116)
s(119) =< s(116)
s(118) =< s(117)
with precondition: [V>=2,V3>=0,Out>=0]
#### Cost of chains of start(V,V3,V26,V51,V60,V66):
* Chain [281]: 240*s(124)+210*s(125)+243*s(126)+105*s(127)+444*s(129)+240*s(138)+210*s(139)+243*s(140)+105*s(141)+399*s(144)+8100*s(148)+6264*s(149)+450*s(178)+2610*s(186)+2520*s(187)+2916*s(188)+1530*s(189)+1680*s(266)+1470*s(267)+1701*s(268)+735*s(269)+240*s(374)+210*s(375)+243*s(376)+105*s(377)+20
Such that:s(121) =< 1
s(120) =< 2
s(134) =< V3+2
s(135) =< V3/2+1
aux(75) =< V
aux(76) =< V/2
aux(77) =< V3
aux(78) =< V3/2
aux(79) =< V26
aux(80) =< V26/2
s(124) =< s(120)
s(125) =< s(120)
s(126) =< s(120)
s(127) =< s(120)
s(125) =< s(121)
s(127) =< s(121)
s(124) =< aux(77)
s(125) =< aux(77)
s(126) =< aux(77)
s(127) =< aux(77)
s(124) =< aux(78)
s(125) =< aux(78)
s(144) =< aux(75)
s(129) =< aux(77)
s(146) =< s(144)*aux(77)
s(147) =< s(146)* (1/2)
s(148) =< s(146)
s(149) =< s(146)
s(148) =< s(147)
s(178) =< aux(77)
s(178) =< aux(78)
s(186) =< aux(77)
s(187) =< aux(77)
s(188) =< aux(77)
s(189) =< aux(77)
s(187) =< aux(78)
s(189) =< aux(78)
s(186) =< aux(75)
s(187) =< aux(75)
s(188) =< aux(75)
s(189) =< aux(75)
s(186) =< aux(76)
s(187) =< aux(76)
s(266) =< aux(75)
s(267) =< aux(75)
s(268) =< aux(75)
s(269) =< aux(75)
s(267) =< aux(76)
s(269) =< aux(76)
s(266) =< aux(79)
s(267) =< aux(79)
s(268) =< aux(79)
s(269) =< aux(79)
s(266) =< aux(80)
s(267) =< aux(80)
s(374) =< aux(77)
s(375) =< aux(77)
s(376) =< aux(77)
s(377) =< aux(77)
s(375) =< aux(78)
s(377) =< aux(78)
s(374) =< aux(79)
s(375) =< aux(79)
s(376) =< aux(79)
s(377) =< aux(79)
s(374) =< aux(80)
s(375) =< aux(80)
s(138) =< s(134)
s(139) =< s(134)
s(140) =< s(134)
s(141) =< s(134)
s(139) =< s(135)
s(141) =< s(135)
s(138) =< aux(77)
s(139) =< aux(77)
s(140) =< aux(77)
s(141) =< aux(77)
s(138) =< aux(78)
s(139) =< aux(78)
with precondition: [V>=0]
* Chain [280]: 18*s(379)+8
Such that:aux(81) =< V3
s(379) =< aux(81)
with precondition: [V=1]
* Chain [279]: 19
with precondition: [V=2]
* Chain [278]: 0
with precondition: [V=3]
* Chain [277]: 1440*s(388)+1260*s(389)+1458*s(390)+630*s(391)+19
Such that:aux(82) =< V
aux(83) =< V/2
aux(84) =< V26
aux(85) =< V26/2
s(388) =< aux(82)
s(389) =< aux(82)
s(390) =< aux(82)
s(391) =< aux(82)
s(389) =< aux(83)
s(391) =< aux(83)
s(388) =< aux(84)
s(389) =< aux(84)
s(390) =< aux(84)
s(391) =< aux(84)
s(388) =< aux(85)
s(389) =< aux(85)
with precondition: [V3=0,V>=1]
* Chain [276]: 18
with precondition: [V26=1,V>=0,V3>=0]
* Chain [275]: 7
with precondition: [V3=0,V60=0,V>=0,V26>=0,V51>=1,V66>=1]
* Chain [274]: 11
with precondition: [V3=0,V60=0,V>=1,V26>=0,V51>=0,V66>=1]
* Chain [273]: 14
with precondition: [V3=0,V60=0,V>=2,V26>=0,V51>=1]
* Chain [272]: 11
with precondition: [V66=0,V>=0,V3>=0,V26>=0,V51>=0,V60>=1]
* Chain [271]: 11
with precondition: [V3=0,V66=0,V>=1,V26>=0,V51>=0,V60>=1]
* Chain [270]: 7
with precondition: [V3=0,V>=0,V26>=0,V51>=1,V60>=1,V66>=1]
* Chain [269]: 4
with precondition: [V3=1,V>=1,V26>=0]
* Chain [268]: 12*s(433)+38*s(437)+900*s(440)+696*s(441)+9
Such that:s(434) =< V
aux(86) =< 1
s(433) =< aux(86)
s(437) =< s(434)
s(438) =< s(437)*aux(86)
s(439) =< s(438)* (1/2)
s(440) =< s(438)
s(441) =< s(438)
s(440) =< s(439)
with precondition: [V3=1,V>=2]
* Chain [267]: 1440*s(446)+1260*s(447)+1458*s(448)+630*s(449)+20
Such that:aux(87) =< V
aux(88) =< V/2
aux(89) =< V3
aux(90) =< V3/2
s(446) =< aux(89)
s(447) =< aux(89)
s(448) =< aux(89)
s(449) =< aux(89)
s(447) =< aux(90)
s(449) =< aux(90)
s(446) =< aux(87)
s(447) =< aux(87)
s(448) =< aux(87)
s(449) =< aux(87)
s(446) =< aux(88)
s(447) =< aux(88)
with precondition: [V26=0,V>=1,V3>=1]
* Chain [266]: 720*s(494)+630*s(495)+729*s(496)+315*s(497)+19
Such that:aux(91) =< V
aux(92) =< V/2
aux(93) =< V26
aux(94) =< V26/2
s(494) =< aux(91)
s(495) =< aux(91)
s(496) =< aux(91)
s(497) =< aux(91)
s(495) =< aux(92)
s(497) =< aux(92)
s(494) =< aux(93)
s(495) =< aux(93)
s(496) =< aux(93)
s(497) =< aux(93)
s(494) =< aux(94)
s(495) =< aux(94)
with precondition: [V51=0,V>=2,V3>=1,V26>=0]
* Chain [265]: 13
with precondition: [V51=0,V60=0,V>=0,V3>=0,V26>=0]
* Chain [264]: 15
with precondition: [V51=0,V>=0,V3>=1,V26>=0,V60>=1]
* Chain [263]: 9
with precondition: [V60=0,V66=0,V>=0,V3>=0,V26>=0,V51>=0]
* Chain [262]: 15
with precondition: [V60=0,V>=0,V3>=1,V26>=0,V51>=1]
* Chain [261]: 11
with precondition: [V60=0,V>=1,V3>=1,V26>=0,V51>=0,V66>=1]
* Chain [260]: 2
with precondition: [V=V3,V>=1]
Closed-form bounds of start(V,V3,V26,V51,V60,V66):
-------------------------------------
* Chain [281] with precondition: [V>=0]
- Upper bound: 5985*V+1616+nat(V3)*11268+nat(V3)*14364*V+nat(V3+2)*798
- Complexity: n^2
* Chain [280] with precondition: [V=1]
- Upper bound: nat(V3)*18+8
- Complexity: n
* Chain [279] with precondition: [V=2]
- Upper bound: 19
- Complexity: constant
* Chain [278] with precondition: [V=3]
- Upper bound: 0
- Complexity: constant
* Chain [277] with precondition: [V3=0,V>=1]
- Upper bound: 4788*V+19
- Complexity: n
* Chain [276] with precondition: [V26=1,V>=0,V3>=0]
- Upper bound: 18
- Complexity: constant
* Chain [275] with precondition: [V3=0,V60=0,V>=0,V26>=0,V51>=1,V66>=1]
- Upper bound: 7
- Complexity: constant
* Chain [274] with precondition: [V3=0,V60=0,V>=1,V26>=0,V51>=0,V66>=1]
- Upper bound: 11
- Complexity: constant
* Chain [273] with precondition: [V3=0,V60=0,V>=2,V26>=0,V51>=1]
- Upper bound: 14
- Complexity: constant
* Chain [272] with precondition: [V66=0,V>=0,V3>=0,V26>=0,V51>=0,V60>=1]
- Upper bound: 11
- Complexity: constant
* Chain [271] with precondition: [V3=0,V66=0,V>=1,V26>=0,V51>=0,V60>=1]
- Upper bound: 11
- Complexity: constant
* Chain [270] with precondition: [V3=0,V>=0,V26>=0,V51>=1,V60>=1,V66>=1]
- Upper bound: 7
- Complexity: constant
* Chain [269] with precondition: [V3=1,V>=1,V26>=0]
- Upper bound: 4
- Complexity: constant
* Chain [268] with precondition: [V3=1,V>=2]
- Upper bound: 1634*V+21
- Complexity: n
* Chain [267] with precondition: [V26=0,V>=1,V3>=1]
- Upper bound: 4788*V3+20
- Complexity: n
* Chain [266] with precondition: [V51=0,V>=2,V3>=1,V26>=0]
- Upper bound: 2394*V+19
- Complexity: n
* Chain [265] with precondition: [V51=0,V60=0,V>=0,V3>=0,V26>=0]
- Upper bound: 13
- Complexity: constant
* Chain [264] with precondition: [V51=0,V>=0,V3>=1,V26>=0,V60>=1]
- Upper bound: 15
- Complexity: constant
* Chain [263] with precondition: [V60=0,V66=0,V>=0,V3>=0,V26>=0,V51>=0]
- Upper bound: 9
- Complexity: constant
* Chain [262] with precondition: [V60=0,V>=0,V3>=1,V26>=0,V51>=1]
- Upper bound: 15
- Complexity: constant
* Chain [261] with precondition: [V60=0,V>=1,V3>=1,V26>=0,V51>=0,V66>=1]
- Upper bound: 11
- Complexity: constant
* Chain [260] with precondition: [V=V3,V>=1]
- Upper bound: 2
- Complexity: constant
### Maximum cost of start(V,V3,V26,V51,V60,V66): max([max([19,nat(V3)*4770+12+ (nat(V3)*18+8)]),1634*V+19+max([2,1197*V+1597+nat(V3)*11268+nat(V3)*14364*V+nat(V3+2)*798+2394*V+760*V])])
Asymptotic class: n^2
* Total analysis performed in 4382 ms.