WORST_CASE(?,O(n^1)) * Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalSimpleSingle2start(A,B,C,D) -> evalSimpleSingle2entryin(A,B,C,D) True (1,1) 1. evalSimpleSingle2entryin(A,B,C,D) -> evalSimpleSingle2bb4in(0,0,C,D) True (?,1) 2. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [0 >= 1 + E] (?,1) 3. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [E >= 1] (?,1) 4. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2returnin(A,B,C,D) True (?,1) 5. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb1in(A,B,C,D) [C >= 1 + B] (?,1) 6. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb2in(A,B,C,D) [B >= C] (?,1) 7. evalSimpleSingle2bb1in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True (?,1) 8. evalSimpleSingle2bb2in(A,B,C,D) -> evalSimpleSingle2bb3in(A,B,C,D) [D >= 1 + A] (?,1) 9. evalSimpleSingle2bb2in(A,B,C,D) -> evalSimpleSingle2returnin(A,B,C,D) [A >= D] (?,1) 10. evalSimpleSingle2bb3in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True (?,1) 11. evalSimpleSingle2returnin(A,B,C,D) -> evalSimpleSingle2stop(A,B,C,D) True (?,1) Signature: {(evalSimpleSingle2bb1in,4) ;(evalSimpleSingle2bb2in,4) ;(evalSimpleSingle2bb3in,4) ;(evalSimpleSingle2bb4in,4) ;(evalSimpleSingle2bbin,4) ;(evalSimpleSingle2entryin,4) ;(evalSimpleSingle2returnin,4) ;(evalSimpleSingle2start,4) ;(evalSimpleSingle2stop,4)} Flow Graph: [0->{1},1->{2,3,4},2->{5,6},3->{5,6},4->{11},5->{7},6->{8,9},7->{2,3,4},8->{10},9->{11},10->{2,3,4} ,11->{}] + Applied Processor: LocalSizeboundsProc + Details: LocalSizebounds generated; rvgraph (< 0,0,A>, A, .= 0) (< 0,0,B>, B, .= 0) (< 0,0,C>, C, .= 0) (< 0,0,D>, D, .= 0) (< 1,0,A>, 0, .= 0) (< 1,0,B>, 0, .= 0) (< 1,0,C>, C, .= 0) (< 1,0,D>, D, .= 0) (< 2,0,A>, A, .= 0) (< 2,0,B>, B, .= 0) (< 2,0,C>, C, .= 0) (< 2,0,D>, D, .= 0) (< 3,0,A>, A, .= 0) (< 3,0,B>, B, .= 0) (< 3,0,C>, C, .= 0) (< 3,0,D>, D, .= 0) (< 4,0,A>, A, .= 0) (< 4,0,B>, B, .= 0) (< 4,0,C>, C, .= 0) (< 4,0,D>, D, .= 0) (< 5,0,A>, A, .= 0) (< 5,0,B>, B, .= 0) (< 5,0,C>, C, .= 0) (< 5,0,D>, D, .= 0) (< 6,0,A>, A, .= 0) (< 6,0,B>, B, .= 0) (< 6,0,C>, C, .= 0) (< 6,0,D>, D, .= 0) (< 7,0,A>, 1 + A, .+ 1) (< 7,0,B>, 1 + B, .+ 1) (< 7,0,C>, C, .= 0) (< 7,0,D>, D, .= 0) (< 8,0,A>, A, .= 0) (< 8,0,B>, B, .= 0) (< 8,0,C>, C, .= 0) (< 8,0,D>, D, .= 0) (< 9,0,A>, A, .= 0) (< 9,0,B>, B, .= 0) (< 9,0,C>, C, .= 0) (< 9,0,D>, D, .= 0) (<10,0,A>, 1 + A, .+ 1) (<10,0,B>, 1 + B, .+ 1) (<10,0,C>, C, .= 0) (<10,0,D>, D, .= 0) (<11,0,A>, A, .= 0) (<11,0,B>, B, .= 0) (<11,0,C>, C, .= 0) (<11,0,D>, D, .= 0) * Step 2: SizeboundsProc WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalSimpleSingle2start(A,B,C,D) -> evalSimpleSingle2entryin(A,B,C,D) True (1,1) 1. evalSimpleSingle2entryin(A,B,C,D) -> evalSimpleSingle2bb4in(0,0,C,D) True (?,1) 2. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [0 >= 1 + E] (?,1) 3. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [E >= 1] (?,1) 4. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2returnin(A,B,C,D) True (?,1) 5. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb1in(A,B,C,D) [C >= 1 + B] (?,1) 6. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb2in(A,B,C,D) [B >= C] (?,1) 7. evalSimpleSingle2bb1in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True (?,1) 8. evalSimpleSingle2bb2in(A,B,C,D) -> evalSimpleSingle2bb3in(A,B,C,D) [D >= 1 + A] (?,1) 9. evalSimpleSingle2bb2in(A,B,C,D) -> evalSimpleSingle2returnin(A,B,C,D) [A >= D] (?,1) 10. evalSimpleSingle2bb3in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True (?,1) 11. evalSimpleSingle2returnin(A,B,C,D) -> evalSimpleSingle2stop(A,B,C,D) True (?,1) Signature: {(evalSimpleSingle2bb1in,4) ;(evalSimpleSingle2bb2in,4) ;(evalSimpleSingle2bb3in,4) ;(evalSimpleSingle2bb4in,4) ;(evalSimpleSingle2bbin,4) ;(evalSimpleSingle2entryin,4) ;(evalSimpleSingle2returnin,4) ;(evalSimpleSingle2start,4) ;(evalSimpleSingle2stop,4)} Flow Graph: [0->{1},1->{2,3,4},2->{5,6},3->{5,6},4->{11},5->{7},6->{8,9},7->{2,3,4},8->{10},9->{11},10->{2,3,4} ,11->{}] Sizebounds: (< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?) (< 0,0,D>, ?) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?) (< 1,0,D>, ?) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?) (<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) + Applied Processor: SizeboundsProc + Details: Sizebounds computed: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 1,0,A>, 0) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, D) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, C) (< 2,0,D>, D) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, D) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, C) (< 4,0,D>, D) (< 5,0,A>, ?) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, D) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, D) (< 7,0,A>, ?) (< 7,0,B>, C) (< 7,0,C>, C) (< 7,0,D>, D) (< 8,0,A>, D) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, D) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, C) (< 9,0,D>, D) (<10,0,A>, D) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, D) (<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, C) (<11,0,D>, D) * Step 3: LeafRules WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalSimpleSingle2start(A,B,C,D) -> evalSimpleSingle2entryin(A,B,C,D) True (1,1) 1. evalSimpleSingle2entryin(A,B,C,D) -> evalSimpleSingle2bb4in(0,0,C,D) True (?,1) 2. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [0 >= 1 + E] (?,1) 3. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [E >= 1] (?,1) 4. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2returnin(A,B,C,D) True (?,1) 5. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb1in(A,B,C,D) [C >= 1 + B] (?,1) 6. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb2in(A,B,C,D) [B >= C] (?,1) 7. evalSimpleSingle2bb1in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True (?,1) 8. evalSimpleSingle2bb2in(A,B,C,D) -> evalSimpleSingle2bb3in(A,B,C,D) [D >= 1 + A] (?,1) 9. evalSimpleSingle2bb2in(A,B,C,D) -> evalSimpleSingle2returnin(A,B,C,D) [A >= D] (?,1) 10. evalSimpleSingle2bb3in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True (?,1) 11. evalSimpleSingle2returnin(A,B,C,D) -> evalSimpleSingle2stop(A,B,C,D) True (?,1) Signature: {(evalSimpleSingle2bb1in,4) ;(evalSimpleSingle2bb2in,4) ;(evalSimpleSingle2bb3in,4) ;(evalSimpleSingle2bb4in,4) ;(evalSimpleSingle2bbin,4) ;(evalSimpleSingle2entryin,4) ;(evalSimpleSingle2returnin,4) ;(evalSimpleSingle2start,4) ;(evalSimpleSingle2stop,4)} Flow Graph: [0->{1},1->{2,3,4},2->{5,6},3->{5,6},4->{11},5->{7},6->{8,9},7->{2,3,4},8->{10},9->{11},10->{2,3,4} ,11->{}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 1,0,A>, 0) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, D) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, C) (< 2,0,D>, D) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, D) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, C) (< 4,0,D>, D) (< 5,0,A>, ?) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, D) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, D) (< 7,0,A>, ?) (< 7,0,B>, C) (< 7,0,C>, C) (< 7,0,D>, D) (< 8,0,A>, D) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, D) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, C) (< 9,0,D>, D) (<10,0,A>, D) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, D) (<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, C) (<11,0,D>, D) + Applied Processor: LeafRules + Details: The following transitions are estimated by its predecessors and are removed [4,9,11] * Step 4: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalSimpleSingle2start(A,B,C,D) -> evalSimpleSingle2entryin(A,B,C,D) True (1,1) 1. evalSimpleSingle2entryin(A,B,C,D) -> evalSimpleSingle2bb4in(0,0,C,D) True (?,1) 2. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [0 >= 1 + E] (?,1) 3. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [E >= 1] (?,1) 5. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb1in(A,B,C,D) [C >= 1 + B] (?,1) 6. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb2in(A,B,C,D) [B >= C] (?,1) 7. evalSimpleSingle2bb1in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True (?,1) 8. evalSimpleSingle2bb2in(A,B,C,D) -> evalSimpleSingle2bb3in(A,B,C,D) [D >= 1 + A] (?,1) 10. evalSimpleSingle2bb3in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True (?,1) Signature: {(evalSimpleSingle2bb1in,4) ;(evalSimpleSingle2bb2in,4) ;(evalSimpleSingle2bb3in,4) ;(evalSimpleSingle2bb4in,4) ;(evalSimpleSingle2bbin,4) ;(evalSimpleSingle2entryin,4) ;(evalSimpleSingle2returnin,4) ;(evalSimpleSingle2start,4) ;(evalSimpleSingle2stop,4)} Flow Graph: [0->{1},1->{2,3},2->{5,6},3->{5,6},5->{7},6->{8},7->{2,3},8->{10},10->{2,3}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 1,0,A>, 0) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, D) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, C) (< 2,0,D>, D) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, D) (< 5,0,A>, ?) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, D) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, D) (< 7,0,A>, ?) (< 7,0,B>, C) (< 7,0,C>, C) (< 7,0,D>, D) (< 8,0,A>, D) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, D) (<10,0,A>, D) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, D) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(evalSimpleSingle2bb1in) = 1 + -1*x1 + x4 p(evalSimpleSingle2bb2in) = 2 + -1*x1 + x4 p(evalSimpleSingle2bb3in) = 1 + -1*x1 + x4 p(evalSimpleSingle2bb4in) = 2 + -1*x1 + x4 p(evalSimpleSingle2bbin) = 2 + -1*x1 + x4 p(evalSimpleSingle2entryin) = 2 + x4 p(evalSimpleSingle2start) = 2 + x4 The following rules are strictly oriented: [D >= 1 + A] ==> evalSimpleSingle2bb2in(A,B,C,D) = 2 + -1*A + D > 1 + -1*A + D = evalSimpleSingle2bb3in(A,B,C,D) The following rules are weakly oriented: True ==> evalSimpleSingle2start(A,B,C,D) = 2 + D >= 2 + D = evalSimpleSingle2entryin(A,B,C,D) True ==> evalSimpleSingle2entryin(A,B,C,D) = 2 + D >= 2 + D = evalSimpleSingle2bb4in(0,0,C,D) [0 >= 1 + E] ==> evalSimpleSingle2bb4in(A,B,C,D) = 2 + -1*A + D >= 2 + -1*A + D = evalSimpleSingle2bbin(A,B,C,D) [E >= 1] ==> evalSimpleSingle2bb4in(A,B,C,D) = 2 + -1*A + D >= 2 + -1*A + D = evalSimpleSingle2bbin(A,B,C,D) [C >= 1 + B] ==> evalSimpleSingle2bbin(A,B,C,D) = 2 + -1*A + D >= 1 + -1*A + D = evalSimpleSingle2bb1in(A,B,C,D) [B >= C] ==> evalSimpleSingle2bbin(A,B,C,D) = 2 + -1*A + D >= 2 + -1*A + D = evalSimpleSingle2bb2in(A,B,C,D) True ==> evalSimpleSingle2bb1in(A,B,C,D) = 1 + -1*A + D >= 1 + -1*A + D = evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True ==> evalSimpleSingle2bb3in(A,B,C,D) = 1 + -1*A + D >= 1 + -1*A + D = evalSimpleSingle2bb4in(1 + A,1 + B,C,D) * Step 5: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalSimpleSingle2start(A,B,C,D) -> evalSimpleSingle2entryin(A,B,C,D) True (1,1) 1. evalSimpleSingle2entryin(A,B,C,D) -> evalSimpleSingle2bb4in(0,0,C,D) True (?,1) 2. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [0 >= 1 + E] (?,1) 3. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [E >= 1] (?,1) 5. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb1in(A,B,C,D) [C >= 1 + B] (?,1) 6. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb2in(A,B,C,D) [B >= C] (?,1) 7. evalSimpleSingle2bb1in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True (?,1) 8. evalSimpleSingle2bb2in(A,B,C,D) -> evalSimpleSingle2bb3in(A,B,C,D) [D >= 1 + A] (2 + D,1) 10. evalSimpleSingle2bb3in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True (?,1) Signature: {(evalSimpleSingle2bb1in,4) ;(evalSimpleSingle2bb2in,4) ;(evalSimpleSingle2bb3in,4) ;(evalSimpleSingle2bb4in,4) ;(evalSimpleSingle2bbin,4) ;(evalSimpleSingle2entryin,4) ;(evalSimpleSingle2returnin,4) ;(evalSimpleSingle2start,4) ;(evalSimpleSingle2stop,4)} Flow Graph: [0->{1},1->{2,3},2->{5,6},3->{5,6},5->{7},6->{8},7->{2,3},8->{10},10->{2,3}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 1,0,A>, 0) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, D) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, C) (< 2,0,D>, D) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, D) (< 5,0,A>, ?) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, D) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, D) (< 7,0,A>, ?) (< 7,0,B>, C) (< 7,0,C>, C) (< 7,0,D>, D) (< 8,0,A>, D) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, D) (<10,0,A>, D) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, D) + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 6: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalSimpleSingle2start(A,B,C,D) -> evalSimpleSingle2entryin(A,B,C,D) True (1,1) 1. evalSimpleSingle2entryin(A,B,C,D) -> evalSimpleSingle2bb4in(0,0,C,D) True (1,1) 2. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [0 >= 1 + E] (?,1) 3. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [E >= 1] (?,1) 5. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb1in(A,B,C,D) [C >= 1 + B] (?,1) 6. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb2in(A,B,C,D) [B >= C] (?,1) 7. evalSimpleSingle2bb1in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True (?,1) 8. evalSimpleSingle2bb2in(A,B,C,D) -> evalSimpleSingle2bb3in(A,B,C,D) [D >= 1 + A] (2 + D,1) 10. evalSimpleSingle2bb3in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True (2 + D,1) Signature: {(evalSimpleSingle2bb1in,4) ;(evalSimpleSingle2bb2in,4) ;(evalSimpleSingle2bb3in,4) ;(evalSimpleSingle2bb4in,4) ;(evalSimpleSingle2bbin,4) ;(evalSimpleSingle2entryin,4) ;(evalSimpleSingle2returnin,4) ;(evalSimpleSingle2start,4) ;(evalSimpleSingle2stop,4)} Flow Graph: [0->{1},1->{2,3},2->{5,6},3->{5,6},5->{7},6->{8},7->{2,3},8->{10},10->{2,3}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 1,0,A>, 0) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, D) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, C) (< 2,0,D>, D) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, D) (< 5,0,A>, ?) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, D) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, D) (< 7,0,A>, ?) (< 7,0,B>, C) (< 7,0,C>, C) (< 7,0,D>, D) (< 8,0,A>, D) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, D) (<10,0,A>, D) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, D) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(evalSimpleSingle2bb1in) = 1 + -1*x2 + x3 p(evalSimpleSingle2bb2in) = 1 + -1*x2 + x3 p(evalSimpleSingle2bb3in) = 1 + -1*x2 + x3 p(evalSimpleSingle2bb4in) = 2 + -1*x2 + x3 p(evalSimpleSingle2bbin) = 2 + -1*x2 + x3 p(evalSimpleSingle2entryin) = 2 + x3 p(evalSimpleSingle2start) = 2 + x3 The following rules are strictly oriented: [C >= 1 + B] ==> evalSimpleSingle2bbin(A,B,C,D) = 2 + -1*B + C > 1 + -1*B + C = evalSimpleSingle2bb1in(A,B,C,D) The following rules are weakly oriented: True ==> evalSimpleSingle2start(A,B,C,D) = 2 + C >= 2 + C = evalSimpleSingle2entryin(A,B,C,D) True ==> evalSimpleSingle2entryin(A,B,C,D) = 2 + C >= 2 + C = evalSimpleSingle2bb4in(0,0,C,D) [0 >= 1 + E] ==> evalSimpleSingle2bb4in(A,B,C,D) = 2 + -1*B + C >= 2 + -1*B + C = evalSimpleSingle2bbin(A,B,C,D) [E >= 1] ==> evalSimpleSingle2bb4in(A,B,C,D) = 2 + -1*B + C >= 2 + -1*B + C = evalSimpleSingle2bbin(A,B,C,D) [B >= C] ==> evalSimpleSingle2bbin(A,B,C,D) = 2 + -1*B + C >= 1 + -1*B + C = evalSimpleSingle2bb2in(A,B,C,D) True ==> evalSimpleSingle2bb1in(A,B,C,D) = 1 + -1*B + C >= 1 + -1*B + C = evalSimpleSingle2bb4in(1 + A,1 + B,C,D) [D >= 1 + A] ==> evalSimpleSingle2bb2in(A,B,C,D) = 1 + -1*B + C >= 1 + -1*B + C = evalSimpleSingle2bb3in(A,B,C,D) True ==> evalSimpleSingle2bb3in(A,B,C,D) = 1 + -1*B + C >= 1 + -1*B + C = evalSimpleSingle2bb4in(1 + A,1 + B,C,D) * Step 7: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalSimpleSingle2start(A,B,C,D) -> evalSimpleSingle2entryin(A,B,C,D) True (1,1) 1. evalSimpleSingle2entryin(A,B,C,D) -> evalSimpleSingle2bb4in(0,0,C,D) True (1,1) 2. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [0 >= 1 + E] (?,1) 3. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [E >= 1] (?,1) 5. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb1in(A,B,C,D) [C >= 1 + B] (2 + C,1) 6. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb2in(A,B,C,D) [B >= C] (?,1) 7. evalSimpleSingle2bb1in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True (?,1) 8. evalSimpleSingle2bb2in(A,B,C,D) -> evalSimpleSingle2bb3in(A,B,C,D) [D >= 1 + A] (2 + D,1) 10. evalSimpleSingle2bb3in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True (2 + D,1) Signature: {(evalSimpleSingle2bb1in,4) ;(evalSimpleSingle2bb2in,4) ;(evalSimpleSingle2bb3in,4) ;(evalSimpleSingle2bb4in,4) ;(evalSimpleSingle2bbin,4) ;(evalSimpleSingle2entryin,4) ;(evalSimpleSingle2returnin,4) ;(evalSimpleSingle2start,4) ;(evalSimpleSingle2stop,4)} Flow Graph: [0->{1},1->{2,3},2->{5,6},3->{5,6},5->{7},6->{8},7->{2,3},8->{10},10->{2,3}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 1,0,A>, 0) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, D) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, C) (< 2,0,D>, D) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, D) (< 5,0,A>, ?) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, D) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, D) (< 7,0,A>, ?) (< 7,0,B>, C) (< 7,0,C>, C) (< 7,0,D>, D) (< 8,0,A>, D) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, D) (<10,0,A>, D) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, D) + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 8: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalSimpleSingle2start(A,B,C,D) -> evalSimpleSingle2entryin(A,B,C,D) True (1,1) 1. evalSimpleSingle2entryin(A,B,C,D) -> evalSimpleSingle2bb4in(0,0,C,D) True (1,1) 2. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [0 >= 1 + E] (?,1) 3. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [E >= 1] (5 + C + D,1) 5. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb1in(A,B,C,D) [C >= 1 + B] (2 + C,1) 6. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb2in(A,B,C,D) [B >= C] (?,1) 7. evalSimpleSingle2bb1in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True (2 + C,1) 8. evalSimpleSingle2bb2in(A,B,C,D) -> evalSimpleSingle2bb3in(A,B,C,D) [D >= 1 + A] (2 + D,1) 10. evalSimpleSingle2bb3in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True (2 + D,1) Signature: {(evalSimpleSingle2bb1in,4) ;(evalSimpleSingle2bb2in,4) ;(evalSimpleSingle2bb3in,4) ;(evalSimpleSingle2bb4in,4) ;(evalSimpleSingle2bbin,4) ;(evalSimpleSingle2entryin,4) ;(evalSimpleSingle2returnin,4) ;(evalSimpleSingle2start,4) ;(evalSimpleSingle2stop,4)} Flow Graph: [0->{1},1->{2,3},2->{5,6},3->{5,6},5->{7},6->{8},7->{2,3},8->{10},10->{2,3}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 1,0,A>, 0) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, D) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, C) (< 2,0,D>, D) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, D) (< 5,0,A>, ?) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, D) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, D) (< 7,0,A>, ?) (< 7,0,B>, C) (< 7,0,C>, C) (< 7,0,D>, D) (< 8,0,A>, D) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, D) (<10,0,A>, D) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, D) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [2,7,5,3,10,6], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(evalSimpleSingle2bb1in) = 1 p(evalSimpleSingle2bb2in) = 0 p(evalSimpleSingle2bb3in) = 1 p(evalSimpleSingle2bb4in) = 1 p(evalSimpleSingle2bbin) = 1 The following rules are strictly oriented: [B >= C] ==> evalSimpleSingle2bbin(A,B,C,D) = 1 > 0 = evalSimpleSingle2bb2in(A,B,C,D) The following rules are weakly oriented: [0 >= 1 + E] ==> evalSimpleSingle2bb4in(A,B,C,D) = 1 >= 1 = evalSimpleSingle2bbin(A,B,C,D) [E >= 1] ==> evalSimpleSingle2bb4in(A,B,C,D) = 1 >= 1 = evalSimpleSingle2bbin(A,B,C,D) [C >= 1 + B] ==> evalSimpleSingle2bbin(A,B,C,D) = 1 >= 1 = evalSimpleSingle2bb1in(A,B,C,D) True ==> evalSimpleSingle2bb1in(A,B,C,D) = 1 >= 1 = evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True ==> evalSimpleSingle2bb3in(A,B,C,D) = 1 >= 1 = evalSimpleSingle2bb4in(1 + A,1 + B,C,D) We use the following global sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 1,0,A>, 0) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, D) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, C) (< 2,0,D>, D) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, D) (< 5,0,A>, ?) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, D) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, D) (< 7,0,A>, ?) (< 7,0,B>, C) (< 7,0,C>, C) (< 7,0,D>, D) (< 8,0,A>, D) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, D) (<10,0,A>, D) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, D) * Step 9: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalSimpleSingle2start(A,B,C,D) -> evalSimpleSingle2entryin(A,B,C,D) True (1,1) 1. evalSimpleSingle2entryin(A,B,C,D) -> evalSimpleSingle2bb4in(0,0,C,D) True (1,1) 2. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [0 >= 1 + E] (?,1) 3. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [E >= 1] (5 + C + D,1) 5. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb1in(A,B,C,D) [C >= 1 + B] (2 + C,1) 6. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb2in(A,B,C,D) [B >= C] (3 + D,1) 7. evalSimpleSingle2bb1in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True (2 + C,1) 8. evalSimpleSingle2bb2in(A,B,C,D) -> evalSimpleSingle2bb3in(A,B,C,D) [D >= 1 + A] (2 + D,1) 10. evalSimpleSingle2bb3in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True (2 + D,1) Signature: {(evalSimpleSingle2bb1in,4) ;(evalSimpleSingle2bb2in,4) ;(evalSimpleSingle2bb3in,4) ;(evalSimpleSingle2bb4in,4) ;(evalSimpleSingle2bbin,4) ;(evalSimpleSingle2entryin,4) ;(evalSimpleSingle2returnin,4) ;(evalSimpleSingle2start,4) ;(evalSimpleSingle2stop,4)} Flow Graph: [0->{1},1->{2,3},2->{5,6},3->{5,6},5->{7},6->{8},7->{2,3},8->{10},10->{2,3}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 1,0,A>, 0) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, D) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, C) (< 2,0,D>, D) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, D) (< 5,0,A>, ?) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, D) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, D) (< 7,0,A>, ?) (< 7,0,B>, C) (< 7,0,C>, C) (< 7,0,D>, D) (< 8,0,A>, D) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, D) (<10,0,A>, D) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, D) + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 10: LocalSizeboundsProc WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalSimpleSingle2start(A,B,C,D) -> evalSimpleSingle2entryin(A,B,C,D) True (1,1) 1. evalSimpleSingle2entryin(A,B,C,D) -> evalSimpleSingle2bb4in(0,0,C,D) True (1,1) 2. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [0 >= 1 + E] (5 + C + D,1) 3. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [E >= 1] (5 + C + D,1) 5. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb1in(A,B,C,D) [C >= 1 + B] (2 + C,1) 6. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb2in(A,B,C,D) [B >= C] (3 + D,1) 7. evalSimpleSingle2bb1in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True (2 + C,1) 8. evalSimpleSingle2bb2in(A,B,C,D) -> evalSimpleSingle2bb3in(A,B,C,D) [D >= 1 + A] (2 + D,1) 10. evalSimpleSingle2bb3in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True (2 + D,1) Signature: {(evalSimpleSingle2bb1in,4) ;(evalSimpleSingle2bb2in,4) ;(evalSimpleSingle2bb3in,4) ;(evalSimpleSingle2bb4in,4) ;(evalSimpleSingle2bbin,4) ;(evalSimpleSingle2entryin,4) ;(evalSimpleSingle2returnin,4) ;(evalSimpleSingle2start,4) ;(evalSimpleSingle2stop,4)} Flow Graph: [0->{1},1->{2,3},2->{5,6},3->{5,6},5->{7},6->{8},7->{2,3},8->{10},10->{2,3}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 1,0,A>, 0) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, D) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, C) (< 2,0,D>, D) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, D) (< 5,0,A>, ?) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, D) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, D) (< 7,0,A>, ?) (< 7,0,B>, C) (< 7,0,C>, C) (< 7,0,D>, D) (< 8,0,A>, D) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, D) (<10,0,A>, D) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, D) + Applied Processor: LocalSizeboundsProc + Details: The problem is already solved. WORST_CASE(?,O(n^1))