WORST_CASE(?,O(n^2)) * Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. evalsipmabubblestart(A,B) -> evalsipmabubbleentryin(A,B) True (1,1) 1. evalsipmabubbleentryin(A,B) -> evalsipmabubblebb6in(A,B) True (?,1) 2. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb4in(A,0) [A >= 0] (?,1) 3. evalsipmabubblebb6in(A,B) -> evalsipmabubblereturnin(A,B) [0 >= 1 + A] (?,1) 4. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb1in(A,B) [A >= 1 + B] (?,1) 5. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb5in(A,B) [B >= A] (?,1) 6. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb2in(A,B) [C >= 1 + D] (?,1) 7. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [D >= C] (?,1) 8. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb3in(A,B) True (?,1) 9. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,1) 10. evalsipmabubblebb5in(A,B) -> evalsipmabubblebb6in(-1 + A,B) True (?,1) 11. evalsipmabubblereturnin(A,B) -> evalsipmabubblestop(A,B) True (?,1) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [0->{1},1->{2,3},2->{4,5},3->{11},4->{6,7},5->{10},6->{8},7->{9},8->{9},9->{4,5},10->{2,3},11->{}] + Applied Processor: LocalSizeboundsProc + Details: LocalSizebounds generated; rvgraph (< 0,0,A>, A, .= 0) (< 0,0,B>, B, .= 0) (< 1,0,A>, A, .= 0) (< 1,0,B>, B, .= 0) (< 2,0,A>, A, .= 0) (< 2,0,B>, 0, .= 0) (< 3,0,A>, A, .= 0) (< 3,0,B>, B, .= 0) (< 4,0,A>, A, .= 0) (< 4,0,B>, B, .= 0) (< 5,0,A>, A, .= 0) (< 5,0,B>, B, .= 0) (< 6,0,A>, A, .= 0) (< 6,0,B>, B, .= 0) (< 7,0,A>, A, .= 0) (< 7,0,B>, B, .= 0) (< 8,0,A>, A, .= 0) (< 8,0,B>, B, .= 0) (< 9,0,A>, A, .= 0) (< 9,0,B>, 1 + B, .+ 1) (<10,0,A>, 1 + A, .+ 1) (<10,0,B>, B, .= 0) (<11,0,A>, A, .= 0) (<11,0,B>, B, .= 0) * Step 2: SizeboundsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. evalsipmabubblestart(A,B) -> evalsipmabubbleentryin(A,B) True (1,1) 1. evalsipmabubbleentryin(A,B) -> evalsipmabubblebb6in(A,B) True (?,1) 2. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb4in(A,0) [A >= 0] (?,1) 3. evalsipmabubblebb6in(A,B) -> evalsipmabubblereturnin(A,B) [0 >= 1 + A] (?,1) 4. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb1in(A,B) [A >= 1 + B] (?,1) 5. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb5in(A,B) [B >= A] (?,1) 6. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb2in(A,B) [C >= 1 + D] (?,1) 7. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [D >= C] (?,1) 8. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb3in(A,B) True (?,1) 9. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,1) 10. evalsipmabubblebb5in(A,B) -> evalsipmabubblebb6in(-1 + A,B) True (?,1) 11. evalsipmabubblereturnin(A,B) -> evalsipmabubblestop(A,B) True (?,1) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [0->{1},1->{2,3},2->{4,5},3->{11},4->{6,7},5->{10},6->{8},7->{9},8->{9},9->{4,5},10->{2,3},11->{}] Sizebounds: (< 0,0,A>, ?) (< 0,0,B>, ?) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 7,0,A>, ?) (< 7,0,B>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (<10,0,A>, ?) (<10,0,B>, ?) (<11,0,A>, ?) (<11,0,B>, ?) + Applied Processor: SizeboundsProc + Details: Sizebounds computed: (< 0,0,A>, A) (< 0,0,B>, B) (< 1,0,A>, A) (< 1,0,B>, B) (< 2,0,A>, ?) (< 2,0,B>, 0) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 7,0,A>, ?) (< 7,0,B>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (<10,0,A>, ?) (<10,0,B>, ?) (<11,0,A>, ?) (<11,0,B>, ?) * Step 3: LeafRules WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. evalsipmabubblestart(A,B) -> evalsipmabubbleentryin(A,B) True (1,1) 1. evalsipmabubbleentryin(A,B) -> evalsipmabubblebb6in(A,B) True (?,1) 2. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb4in(A,0) [A >= 0] (?,1) 3. evalsipmabubblebb6in(A,B) -> evalsipmabubblereturnin(A,B) [0 >= 1 + A] (?,1) 4. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb1in(A,B) [A >= 1 + B] (?,1) 5. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb5in(A,B) [B >= A] (?,1) 6. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb2in(A,B) [C >= 1 + D] (?,1) 7. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [D >= C] (?,1) 8. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb3in(A,B) True (?,1) 9. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,1) 10. evalsipmabubblebb5in(A,B) -> evalsipmabubblebb6in(-1 + A,B) True (?,1) 11. evalsipmabubblereturnin(A,B) -> evalsipmabubblestop(A,B) True (?,1) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [0->{1},1->{2,3},2->{4,5},3->{11},4->{6,7},5->{10},6->{8},7->{9},8->{9},9->{4,5},10->{2,3},11->{}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 1,0,A>, A) (< 1,0,B>, B) (< 2,0,A>, ?) (< 2,0,B>, 0) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 7,0,A>, ?) (< 7,0,B>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (<10,0,A>, ?) (<10,0,B>, ?) (<11,0,A>, ?) (<11,0,B>, ?) + Applied Processor: LeafRules + Details: The following transitions are estimated by its predecessors and are removed [3,11] * Step 4: PolyRank WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. evalsipmabubblestart(A,B) -> evalsipmabubbleentryin(A,B) True (1,1) 1. evalsipmabubbleentryin(A,B) -> evalsipmabubblebb6in(A,B) True (?,1) 2. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb4in(A,0) [A >= 0] (?,1) 4. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb1in(A,B) [A >= 1 + B] (?,1) 5. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb5in(A,B) [B >= A] (?,1) 6. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb2in(A,B) [C >= 1 + D] (?,1) 7. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [D >= C] (?,1) 8. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb3in(A,B) True (?,1) 9. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,1) 10. evalsipmabubblebb5in(A,B) -> evalsipmabubblebb6in(-1 + A,B) True (?,1) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [0->{1},1->{2},2->{4,5},4->{6,7},5->{10},6->{8},7->{9},8->{9},9->{4,5},10->{2}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 1,0,A>, A) (< 1,0,B>, B) (< 2,0,A>, ?) (< 2,0,B>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 7,0,A>, ?) (< 7,0,B>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (<10,0,A>, ?) (<10,0,B>, ?) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(evalsipmabubblebb1in) = 1 + x1 p(evalsipmabubblebb2in) = 1 + x1 p(evalsipmabubblebb3in) = 1 + x1 p(evalsipmabubblebb4in) = 1 + x1 p(evalsipmabubblebb5in) = 1 + x1 p(evalsipmabubblebb6in) = 2 + x1 p(evalsipmabubbleentryin) = 2 + x1 p(evalsipmabubblestart) = 2 + x1 The following rules are strictly oriented: [A >= 0] ==> evalsipmabubblebb6in(A,B) = 2 + A > 1 + A = evalsipmabubblebb4in(A,0) The following rules are weakly oriented: True ==> evalsipmabubblestart(A,B) = 2 + A >= 2 + A = evalsipmabubbleentryin(A,B) True ==> evalsipmabubbleentryin(A,B) = 2 + A >= 2 + A = evalsipmabubblebb6in(A,B) [A >= 1 + B] ==> evalsipmabubblebb4in(A,B) = 1 + A >= 1 + A = evalsipmabubblebb1in(A,B) [B >= A] ==> evalsipmabubblebb4in(A,B) = 1 + A >= 1 + A = evalsipmabubblebb5in(A,B) [C >= 1 + D] ==> evalsipmabubblebb1in(A,B) = 1 + A >= 1 + A = evalsipmabubblebb2in(A,B) [D >= C] ==> evalsipmabubblebb1in(A,B) = 1 + A >= 1 + A = evalsipmabubblebb3in(A,B) True ==> evalsipmabubblebb2in(A,B) = 1 + A >= 1 + A = evalsipmabubblebb3in(A,B) True ==> evalsipmabubblebb3in(A,B) = 1 + A >= 1 + A = evalsipmabubblebb4in(A,1 + B) True ==> evalsipmabubblebb5in(A,B) = 1 + A >= 1 + A = evalsipmabubblebb6in(-1 + A,B) * Step 5: KnowledgePropagation WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. evalsipmabubblestart(A,B) -> evalsipmabubbleentryin(A,B) True (1,1) 1. evalsipmabubbleentryin(A,B) -> evalsipmabubblebb6in(A,B) True (?,1) 2. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb4in(A,0) [A >= 0] (2 + A,1) 4. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb1in(A,B) [A >= 1 + B] (?,1) 5. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb5in(A,B) [B >= A] (?,1) 6. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb2in(A,B) [C >= 1 + D] (?,1) 7. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [D >= C] (?,1) 8. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb3in(A,B) True (?,1) 9. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,1) 10. evalsipmabubblebb5in(A,B) -> evalsipmabubblebb6in(-1 + A,B) True (?,1) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [0->{1},1->{2},2->{4,5},4->{6,7},5->{10},6->{8},7->{9},8->{9},9->{4,5},10->{2}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 1,0,A>, A) (< 1,0,B>, B) (< 2,0,A>, ?) (< 2,0,B>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 7,0,A>, ?) (< 7,0,B>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (<10,0,A>, ?) (<10,0,B>, ?) + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 6: PolyRank WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. evalsipmabubblestart(A,B) -> evalsipmabubbleentryin(A,B) True (1,1) 1. evalsipmabubbleentryin(A,B) -> evalsipmabubblebb6in(A,B) True (1,1) 2. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb4in(A,0) [A >= 0] (2 + A,1) 4. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb1in(A,B) [A >= 1 + B] (?,1) 5. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb5in(A,B) [B >= A] (?,1) 6. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb2in(A,B) [C >= 1 + D] (?,1) 7. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [D >= C] (?,1) 8. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb3in(A,B) True (?,1) 9. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,1) 10. evalsipmabubblebb5in(A,B) -> evalsipmabubblebb6in(-1 + A,B) True (?,1) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [0->{1},1->{2},2->{4,5},4->{6,7},5->{10},6->{8},7->{9},8->{9},9->{4,5},10->{2}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 1,0,A>, A) (< 1,0,B>, B) (< 2,0,A>, ?) (< 2,0,B>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 7,0,A>, ?) (< 7,0,B>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (<10,0,A>, ?) (<10,0,B>, ?) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [10,5,9,7,4,8,6], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(evalsipmabubblebb1in) = 1 p(evalsipmabubblebb2in) = 1 p(evalsipmabubblebb3in) = 1 p(evalsipmabubblebb4in) = 1 p(evalsipmabubblebb5in) = 1 p(evalsipmabubblebb6in) = 0 The following rules are strictly oriented: True ==> evalsipmabubblebb5in(A,B) = 1 > 0 = evalsipmabubblebb6in(-1 + A,B) The following rules are weakly oriented: [A >= 1 + B] ==> evalsipmabubblebb4in(A,B) = 1 >= 1 = evalsipmabubblebb1in(A,B) [B >= A] ==> evalsipmabubblebb4in(A,B) = 1 >= 1 = evalsipmabubblebb5in(A,B) [C >= 1 + D] ==> evalsipmabubblebb1in(A,B) = 1 >= 1 = evalsipmabubblebb2in(A,B) [D >= C] ==> evalsipmabubblebb1in(A,B) = 1 >= 1 = evalsipmabubblebb3in(A,B) True ==> evalsipmabubblebb2in(A,B) = 1 >= 1 = evalsipmabubblebb3in(A,B) True ==> evalsipmabubblebb3in(A,B) = 1 >= 1 = evalsipmabubblebb4in(A,1 + B) We use the following global sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 1,0,A>, A) (< 1,0,B>, B) (< 2,0,A>, ?) (< 2,0,B>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 7,0,A>, ?) (< 7,0,B>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (<10,0,A>, ?) (<10,0,B>, ?) * Step 7: PolyRank WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. evalsipmabubblestart(A,B) -> evalsipmabubbleentryin(A,B) True (1,1) 1. evalsipmabubbleentryin(A,B) -> evalsipmabubblebb6in(A,B) True (1,1) 2. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb4in(A,0) [A >= 0] (2 + A,1) 4. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb1in(A,B) [A >= 1 + B] (?,1) 5. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb5in(A,B) [B >= A] (?,1) 6. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb2in(A,B) [C >= 1 + D] (?,1) 7. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [D >= C] (?,1) 8. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb3in(A,B) True (?,1) 9. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,1) 10. evalsipmabubblebb5in(A,B) -> evalsipmabubblebb6in(-1 + A,B) True (2 + A,1) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [0->{1},1->{2},2->{4,5},4->{6,7},5->{10},6->{8},7->{9},8->{9},9->{4,5},10->{2}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 1,0,A>, A) (< 1,0,B>, B) (< 2,0,A>, ?) (< 2,0,B>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 7,0,A>, ?) (< 7,0,B>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (<10,0,A>, ?) (<10,0,B>, ?) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [2,5,9,7,4,8,6], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(evalsipmabubblebb1in) = 1 p(evalsipmabubblebb2in) = 1 p(evalsipmabubblebb3in) = 1 p(evalsipmabubblebb4in) = 1 p(evalsipmabubblebb5in) = 0 p(evalsipmabubblebb6in) = 1 The following rules are strictly oriented: [B >= A] ==> evalsipmabubblebb4in(A,B) = 1 > 0 = evalsipmabubblebb5in(A,B) The following rules are weakly oriented: [A >= 0] ==> evalsipmabubblebb6in(A,B) = 1 >= 1 = evalsipmabubblebb4in(A,0) [A >= 1 + B] ==> evalsipmabubblebb4in(A,B) = 1 >= 1 = evalsipmabubblebb1in(A,B) [C >= 1 + D] ==> evalsipmabubblebb1in(A,B) = 1 >= 1 = evalsipmabubblebb2in(A,B) [D >= C] ==> evalsipmabubblebb1in(A,B) = 1 >= 1 = evalsipmabubblebb3in(A,B) True ==> evalsipmabubblebb2in(A,B) = 1 >= 1 = evalsipmabubblebb3in(A,B) True ==> evalsipmabubblebb3in(A,B) = 1 >= 1 = evalsipmabubblebb4in(A,1 + B) We use the following global sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 1,0,A>, A) (< 1,0,B>, B) (< 2,0,A>, ?) (< 2,0,B>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 7,0,A>, ?) (< 7,0,B>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (<10,0,A>, ?) (<10,0,B>, ?) * Step 8: ChainProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. evalsipmabubblestart(A,B) -> evalsipmabubbleentryin(A,B) True (1,1) 1. evalsipmabubbleentryin(A,B) -> evalsipmabubblebb6in(A,B) True (1,1) 2. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb4in(A,0) [A >= 0] (2 + A,1) 4. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb1in(A,B) [A >= 1 + B] (?,1) 5. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb5in(A,B) [B >= A] (3 + A,1) 6. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb2in(A,B) [C >= 1 + D] (?,1) 7. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [D >= C] (?,1) 8. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb3in(A,B) True (?,1) 9. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,1) 10. evalsipmabubblebb5in(A,B) -> evalsipmabubblebb6in(-1 + A,B) True (2 + A,1) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [0->{1},1->{2},2->{4,5},4->{6,7},5->{10},6->{8},7->{9},8->{9},9->{4,5},10->{2}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 1,0,A>, A) (< 1,0,B>, B) (< 2,0,A>, ?) (< 2,0,B>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 7,0,A>, ?) (< 7,0,B>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (<10,0,A>, ?) (<10,0,B>, ?) + Applied Processor: ChainProcessor False [0,1,2,4,5,6,7,8,9,10] + Details: We chained rule 0 to obtain the rules [11] . * Step 9: UnreachableRules WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 1. evalsipmabubbleentryin(A,B) -> evalsipmabubblebb6in(A,B) True (1,1) 2. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb4in(A,0) [A >= 0] (2 + A,1) 4. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb1in(A,B) [A >= 1 + B] (?,1) 5. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb5in(A,B) [B >= A] (3 + A,1) 6. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb2in(A,B) [C >= 1 + D] (?,1) 7. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [D >= C] (?,1) 8. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb3in(A,B) True (?,1) 9. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,1) 10. evalsipmabubblebb5in(A,B) -> evalsipmabubblebb6in(-1 + A,B) True (2 + A,1) 11. evalsipmabubblestart(A,B) -> evalsipmabubblebb6in(A,B) True (1,2) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [1->{2},2->{4,5},4->{6,7},5->{10},6->{8},7->{9},8->{9},9->{4,5},10->{2},11->{2}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, B) (< 2,0,A>, ?) (< 2,0,B>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 7,0,A>, ?) (< 7,0,B>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (<10,0,A>, ?) (<10,0,B>, ?) (<11,0,A>, A) (<11,0,B>, B) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [1] * Step 10: ChainProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 2. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb4in(A,0) [A >= 0] (2 + A,1) 4. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb1in(A,B) [A >= 1 + B] (?,1) 5. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb5in(A,B) [B >= A] (3 + A,1) 6. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb2in(A,B) [C >= 1 + D] (?,1) 7. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [D >= C] (?,1) 8. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb3in(A,B) True (?,1) 9. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,1) 10. evalsipmabubblebb5in(A,B) -> evalsipmabubblebb6in(-1 + A,B) True (2 + A,1) 11. evalsipmabubblestart(A,B) -> evalsipmabubblebb6in(A,B) True (1,2) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [2->{4,5},4->{6,7},5->{10},6->{8},7->{9},8->{9},9->{4,5},10->{2},11->{2}] Sizebounds: (< 2,0,A>, ?) (< 2,0,B>, 0) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 7,0,A>, ?) (< 7,0,B>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (<10,0,A>, ?) (<10,0,B>, ?) (<11,0,A>, A) (<11,0,B>, B) + Applied Processor: ChainProcessor False [2,4,5,6,7,8,9,10,11] + Details: We chained rule 2 to obtain the rules [12,13] . * Step 11: ChainProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 4. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb1in(A,B) [A >= 1 + B] (?,1) 5. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb5in(A,B) [B >= A] (3 + A,1) 6. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb2in(A,B) [C >= 1 + D] (?,1) 7. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [D >= C] (?,1) 8. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb3in(A,B) True (?,1) 9. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,1) 10. evalsipmabubblebb5in(A,B) -> evalsipmabubblebb6in(-1 + A,B) True (2 + A,1) 11. evalsipmabubblestart(A,B) -> evalsipmabubblebb6in(A,B) True (1,2) 12. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (2 + A,2) 13. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb5in(A,0) [A >= 0 && 0 >= A] (2 + A,2) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [4->{6,7},5->{10},6->{8},7->{9},8->{9},9->{4,5},10->{12,13},11->{12,13},12->{6,7},13->{10}] Sizebounds: (< 4,0,A>, ?) (< 4,0,B>, ?) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 7,0,A>, ?) (< 7,0,B>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (<10,0,A>, ?) (<10,0,B>, ?) (<11,0,A>, A) (<11,0,B>, B) (<12,0,A>, ?) (<12,0,B>, ?) (<13,0,A>, ?) (<13,0,B>, ?) + Applied Processor: ChainProcessor False [4,5,6,7,8,9,10,11,12,13] + Details: We chained rule 4 to obtain the rules [14,15] . * Step 12: ChainProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 5. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb5in(A,B) [B >= A] (3 + A,1) 6. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb2in(A,B) [C >= 1 + D] (?,1) 7. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [D >= C] (?,1) 8. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb3in(A,B) True (?,1) 9. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,1) 10. evalsipmabubblebb5in(A,B) -> evalsipmabubblebb6in(-1 + A,B) True (2 + A,1) 11. evalsipmabubblestart(A,B) -> evalsipmabubblebb6in(A,B) True (1,2) 12. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (2 + A,2) 13. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb5in(A,0) [A >= 0 && 0 >= A] (2 + A,2) 14. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb2in(A,B) [A >= 1 + B && C$ >= 1 + D$] (?,2) 15. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb3in(A,B) [A >= 1 + B && D$ >= C$] (?,2) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [5->{10},6->{8},7->{9},8->{9},9->{5,14,15},10->{12,13},11->{12,13},12->{6,7},13->{10},14->{8},15->{9}] Sizebounds: (< 5,0,A>, ?) (< 5,0,B>, ?) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 7,0,A>, ?) (< 7,0,B>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (<10,0,A>, ?) (<10,0,B>, ?) (<11,0,A>, A) (<11,0,B>, B) (<12,0,A>, ?) (<12,0,B>, ?) (<13,0,A>, ?) (<13,0,B>, ?) (<14,0,A>, ?) (<14,0,B>, ?) (<15,0,A>, ?) (<15,0,B>, ?) + Applied Processor: ChainProcessor False [5,6,7,8,9,10,11,12,13,14,15] + Details: We chained rule 5 to obtain the rules [16] . * Step 13: ChainProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 6. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb2in(A,B) [C >= 1 + D] (?,1) 7. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [D >= C] (?,1) 8. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb3in(A,B) True (?,1) 9. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,1) 10. evalsipmabubblebb5in(A,B) -> evalsipmabubblebb6in(-1 + A,B) True (2 + A,1) 11. evalsipmabubblestart(A,B) -> evalsipmabubblebb6in(A,B) True (1,2) 12. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (2 + A,2) 13. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb5in(A,0) [A >= 0 && 0 >= A] (2 + A,2) 14. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb2in(A,B) [A >= 1 + B && C$ >= 1 + D$] (?,2) 15. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb3in(A,B) [A >= 1 + B && D$ >= C$] (?,2) 16. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb6in(-1 + A,B) [B >= A] (3 + A,2) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [6->{8},7->{9},8->{9},9->{14,15,16},10->{12,13},11->{12,13},12->{6,7},13->{10},14->{8},15->{9},16->{12 ,13}] Sizebounds: (< 6,0,A>, ?) (< 6,0,B>, ?) (< 7,0,A>, ?) (< 7,0,B>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (<10,0,A>, ?) (<10,0,B>, ?) (<11,0,A>, A) (<11,0,B>, B) (<12,0,A>, ?) (<12,0,B>, ?) (<13,0,A>, ?) (<13,0,B>, ?) (<14,0,A>, ?) (<14,0,B>, ?) (<15,0,A>, ?) (<15,0,B>, ?) (<16,0,A>, ?) (<16,0,B>, ?) + Applied Processor: ChainProcessor False [6,7,8,9,10,11,12,13,14,15,16] + Details: We chained rule 6 to obtain the rules [17] . * Step 14: ChainProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 7. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [D >= C] (?,1) 8. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb3in(A,B) True (?,1) 9. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,1) 10. evalsipmabubblebb5in(A,B) -> evalsipmabubblebb6in(-1 + A,B) True (2 + A,1) 11. evalsipmabubblestart(A,B) -> evalsipmabubblebb6in(A,B) True (1,2) 12. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (2 + A,2) 13. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb5in(A,0) [A >= 0 && 0 >= A] (2 + A,2) 14. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb2in(A,B) [A >= 1 + B && C$ >= 1 + D$] (?,2) 15. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb3in(A,B) [A >= 1 + B && D$ >= C$] (?,2) 16. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb6in(-1 + A,B) [B >= A] (3 + A,2) 17. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [C >= 1 + D] (?,2) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [7->{9},8->{9},9->{14,15,16},10->{12,13},11->{12,13},12->{7,17},13->{10},14->{8},15->{9},16->{12,13} ,17->{9}] Sizebounds: (< 7,0,A>, ?) (< 7,0,B>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (<10,0,A>, ?) (<10,0,B>, ?) (<11,0,A>, A) (<11,0,B>, B) (<12,0,A>, ?) (<12,0,B>, ?) (<13,0,A>, ?) (<13,0,B>, ?) (<14,0,A>, ?) (<14,0,B>, ?) (<15,0,A>, ?) (<15,0,B>, ?) (<16,0,A>, ?) (<16,0,B>, ?) (<17,0,A>, ?) (<17,0,B>, ?) + Applied Processor: ChainProcessor False [7,8,9,10,11,12,13,14,15,16,17] + Details: We chained rule 7 to obtain the rules [18] . * Step 15: ChainProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 8. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb3in(A,B) True (?,1) 9. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,1) 10. evalsipmabubblebb5in(A,B) -> evalsipmabubblebb6in(-1 + A,B) True (2 + A,1) 11. evalsipmabubblestart(A,B) -> evalsipmabubblebb6in(A,B) True (1,2) 12. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (2 + A,2) 13. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb5in(A,0) [A >= 0 && 0 >= A] (2 + A,2) 14. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb2in(A,B) [A >= 1 + B && C$ >= 1 + D$] (?,2) 15. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb3in(A,B) [A >= 1 + B && D$ >= C$] (?,2) 16. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb6in(-1 + A,B) [B >= A] (3 + A,2) 17. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [C >= 1 + D] (?,2) 18. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb4in(A,1 + B) [D >= C] (?,2) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [8->{9},9->{14,15,16},10->{12,13},11->{12,13},12->{17,18},13->{10},14->{8},15->{9},16->{12,13},17->{9} ,18->{14,15,16}] Sizebounds: (< 8,0,A>, ?) (< 8,0,B>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (<10,0,A>, ?) (<10,0,B>, ?) (<11,0,A>, A) (<11,0,B>, B) (<12,0,A>, ?) (<12,0,B>, ?) (<13,0,A>, ?) (<13,0,B>, ?) (<14,0,A>, ?) (<14,0,B>, ?) (<15,0,A>, ?) (<15,0,B>, ?) (<16,0,A>, ?) (<16,0,B>, ?) (<17,0,A>, ?) (<17,0,B>, ?) (<18,0,A>, ?) (<18,0,B>, ?) + Applied Processor: ChainProcessor False [8,9,10,11,12,13,14,15,16,17,18] + Details: We chained rule 8 to obtain the rules [19] . * Step 16: ChainProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 9. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,1) 10. evalsipmabubblebb5in(A,B) -> evalsipmabubblebb6in(-1 + A,B) True (2 + A,1) 11. evalsipmabubblestart(A,B) -> evalsipmabubblebb6in(A,B) True (1,2) 12. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (2 + A,2) 13. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb5in(A,0) [A >= 0 && 0 >= A] (2 + A,2) 14. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb2in(A,B) [A >= 1 + B && C$ >= 1 + D$] (?,2) 15. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb3in(A,B) [A >= 1 + B && D$ >= C$] (?,2) 16. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb6in(-1 + A,B) [B >= A] (3 + A,2) 17. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [C >= 1 + D] (?,2) 18. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb4in(A,1 + B) [D >= C] (?,2) 19. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,2) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [9->{14,15,16},10->{12,13},11->{12,13},12->{17,18},13->{10},14->{19},15->{9},16->{12,13},17->{9},18->{14 ,15,16},19->{14,15,16}] Sizebounds: (< 9,0,A>, ?) (< 9,0,B>, ?) (<10,0,A>, ?) (<10,0,B>, ?) (<11,0,A>, A) (<11,0,B>, B) (<12,0,A>, ?) (<12,0,B>, ?) (<13,0,A>, ?) (<13,0,B>, ?) (<14,0,A>, ?) (<14,0,B>, ?) (<15,0,A>, ?) (<15,0,B>, ?) (<16,0,A>, ?) (<16,0,B>, ?) (<17,0,A>, ?) (<17,0,B>, ?) (<18,0,A>, ?) (<18,0,B>, ?) (<19,0,A>, ?) (<19,0,B>, ?) + Applied Processor: ChainProcessor False [9,10,11,12,13,14,15,16,17,18,19] + Details: We chained rule 9 to obtain the rules [20,21,22] . * Step 17: ChainProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 10. evalsipmabubblebb5in(A,B) -> evalsipmabubblebb6in(-1 + A,B) True (2 + A,1) 11. evalsipmabubblestart(A,B) -> evalsipmabubblebb6in(A,B) True (1,2) 12. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (2 + A,2) 13. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb5in(A,0) [A >= 0 && 0 >= A] (2 + A,2) 14. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb2in(A,B) [A >= 1 + B && C$ >= 1 + D$] (?,2) 15. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb3in(A,B) [A >= 1 + B && D$ >= C$] (?,2) 16. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb6in(-1 + A,B) [B >= A] (3 + A,2) 17. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [C >= 1 + D] (?,2) 18. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb4in(A,1 + B) [D >= C] (?,2) 19. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,2) 20. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb2in(A,1 + B) [A >= 2 + B && C$$ >= 1 + D$$] (?,3) 21. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb3in(A,1 + B) [A >= 2 + B && D$$ >= C$$] (?,3) 22. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb6in(-1 + A,1 + B) [1 + B >= A] (?,3) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [10->{12,13},11->{12,13},12->{17,18},13->{10},14->{19},15->{20,21,22},16->{12,13},17->{20,21,22},18->{14 ,15,16},19->{14,15,16},20->{19},21->{20,21,22},22->{12,13}] Sizebounds: (<10,0,A>, ?) (<10,0,B>, ?) (<11,0,A>, A) (<11,0,B>, B) (<12,0,A>, ?) (<12,0,B>, ?) (<13,0,A>, ?) (<13,0,B>, ?) (<14,0,A>, ?) (<14,0,B>, ?) (<15,0,A>, ?) (<15,0,B>, ?) (<16,0,A>, ?) (<16,0,B>, ?) (<17,0,A>, ?) (<17,0,B>, ?) (<18,0,A>, ?) (<18,0,B>, ?) (<19,0,A>, ?) (<19,0,B>, ?) (<20,0,A>, ?) (<20,0,B>, ?) (<21,0,A>, ?) (<21,0,B>, ?) (<22,0,A>, ?) (<22,0,B>, ?) + Applied Processor: ChainProcessor False [10,11,12,13,14,15,16,17,18,19,20,21,22] + Details: We chained rule 10 to obtain the rules [23,24] . * Step 18: ChainProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 11. evalsipmabubblestart(A,B) -> evalsipmabubblebb6in(A,B) True (1,2) 12. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (2 + A,2) 13. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb5in(A,0) [A >= 0 && 0 >= A] (2 + A,2) 14. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb2in(A,B) [A >= 1 + B && C$ >= 1 + D$] (?,2) 15. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb3in(A,B) [A >= 1 + B && D$ >= C$] (?,2) 16. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb6in(-1 + A,B) [B >= A] (3 + A,2) 17. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [C >= 1 + D] (?,2) 18. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb4in(A,1 + B) [D >= C] (?,2) 19. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,2) 20. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb2in(A,1 + B) [A >= 2 + B && C$$ >= 1 + D$$] (?,3) 21. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb3in(A,1 + B) [A >= 2 + B && D$$ >= C$$] (?,3) 22. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb6in(-1 + A,1 + B) [1 + B >= A] (?,3) 23. evalsipmabubblebb5in(A,B) -> evalsipmabubblebb1in(-1 + A,0) [-1 + A >= 0 && -1 + A >= 1] (2 + A,3) 24. evalsipmabubblebb5in(A,B) -> evalsipmabubblebb5in(-1 + A,0) [-1 + A >= 0 && 0 >= -1 + A] (2 + A,3) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [11->{12,13},12->{17,18},13->{23,24},14->{19},15->{20,21,22},16->{12,13},17->{20,21,22},18->{14,15,16} ,19->{14,15,16},20->{19},21->{20,21,22},22->{12,13},23->{17,18},24->{23,24}] Sizebounds: (<11,0,A>, A) (<11,0,B>, B) (<12,0,A>, ?) (<12,0,B>, ?) (<13,0,A>, ?) (<13,0,B>, ?) (<14,0,A>, ?) (<14,0,B>, ?) (<15,0,A>, ?) (<15,0,B>, ?) (<16,0,A>, ?) (<16,0,B>, ?) (<17,0,A>, ?) (<17,0,B>, ?) (<18,0,A>, ?) (<18,0,B>, ?) (<19,0,A>, ?) (<19,0,B>, ?) (<20,0,A>, ?) (<20,0,B>, ?) (<21,0,A>, ?) (<21,0,B>, ?) (<22,0,A>, ?) (<22,0,B>, ?) (<23,0,A>, ?) (<23,0,B>, ?) (<24,0,A>, ?) (<24,0,B>, ?) + Applied Processor: ChainProcessor False [11,12,13,14,15,16,17,18,19,20,21,22,23,24] + Details: We chained rule 11 to obtain the rules [25,26] . * Step 19: UnsatPaths WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 12. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (2 + A,2) 13. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb5in(A,0) [A >= 0 && 0 >= A] (2 + A,2) 14. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb2in(A,B) [A >= 1 + B && C$ >= 1 + D$] (?,2) 15. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb3in(A,B) [A >= 1 + B && D$ >= C$] (?,2) 16. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb6in(-1 + A,B) [B >= A] (3 + A,2) 17. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [C >= 1 + D] (?,2) 18. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb4in(A,1 + B) [D >= C] (?,2) 19. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,2) 20. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb2in(A,1 + B) [A >= 2 + B && C$$ >= 1 + D$$] (?,3) 21. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb3in(A,1 + B) [A >= 2 + B && D$$ >= C$$] (?,3) 22. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb6in(-1 + A,1 + B) [1 + B >= A] (?,3) 23. evalsipmabubblebb5in(A,B) -> evalsipmabubblebb1in(-1 + A,0) [-1 + A >= 0 && -1 + A >= 1] (2 + A,3) 24. evalsipmabubblebb5in(A,B) -> evalsipmabubblebb5in(-1 + A,0) [-1 + A >= 0 && 0 >= -1 + A] (2 + A,3) 25. evalsipmabubblestart(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (1,4) 26. evalsipmabubblestart(A,B) -> evalsipmabubblebb5in(A,0) [A >= 0 && 0 >= A] (1,4) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [12->{17,18},13->{23,24},14->{19},15->{20,21,22},16->{12,13},17->{20,21,22},18->{14,15,16},19->{14,15,16} ,20->{19},21->{20,21,22},22->{12,13},23->{17,18},24->{23,24},25->{17,18},26->{23,24}] Sizebounds: (<12,0,A>, ?) (<12,0,B>, ?) (<13,0,A>, ?) (<13,0,B>, ?) (<14,0,A>, ?) (<14,0,B>, ?) (<15,0,A>, ?) (<15,0,B>, ?) (<16,0,A>, ?) (<16,0,B>, ?) (<17,0,A>, ?) (<17,0,B>, ?) (<18,0,A>, ?) (<18,0,B>, ?) (<19,0,A>, ?) (<19,0,B>, ?) (<20,0,A>, ?) (<20,0,B>, ?) (<21,0,A>, ?) (<21,0,B>, ?) (<22,0,A>, ?) (<22,0,B>, ?) (<23,0,A>, ?) (<23,0,B>, ?) (<24,0,A>, ?) (<24,0,B>, ?) (<25,0,A>, ?) (<25,0,B>, ?) (<26,0,A>, ?) (<26,0,B>, ?) + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(13,23),(13,24),(24,23),(24,24),(26,23),(26,24)] * Step 20: UnreachableRules WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 12. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (2 + A,2) 13. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb5in(A,0) [A >= 0 && 0 >= A] (2 + A,2) 14. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb2in(A,B) [A >= 1 + B && C$ >= 1 + D$] (?,2) 15. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb3in(A,B) [A >= 1 + B && D$ >= C$] (?,2) 16. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb6in(-1 + A,B) [B >= A] (3 + A,2) 17. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [C >= 1 + D] (?,2) 18. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb4in(A,1 + B) [D >= C] (?,2) 19. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,2) 20. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb2in(A,1 + B) [A >= 2 + B && C$$ >= 1 + D$$] (?,3) 21. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb3in(A,1 + B) [A >= 2 + B && D$$ >= C$$] (?,3) 22. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb6in(-1 + A,1 + B) [1 + B >= A] (?,3) 23. evalsipmabubblebb5in(A,B) -> evalsipmabubblebb1in(-1 + A,0) [-1 + A >= 0 && -1 + A >= 1] (2 + A,3) 24. evalsipmabubblebb5in(A,B) -> evalsipmabubblebb5in(-1 + A,0) [-1 + A >= 0 && 0 >= -1 + A] (2 + A,3) 25. evalsipmabubblestart(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (1,4) 26. evalsipmabubblestart(A,B) -> evalsipmabubblebb5in(A,0) [A >= 0 && 0 >= A] (1,4) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [12->{17,18},13->{},14->{19},15->{20,21,22},16->{12,13},17->{20,21,22},18->{14,15,16},19->{14,15,16} ,20->{19},21->{20,21,22},22->{12,13},23->{17,18},24->{},25->{17,18},26->{}] Sizebounds: (<12,0,A>, ?) (<12,0,B>, ?) (<13,0,A>, ?) (<13,0,B>, ?) (<14,0,A>, ?) (<14,0,B>, ?) (<15,0,A>, ?) (<15,0,B>, ?) (<16,0,A>, ?) (<16,0,B>, ?) (<17,0,A>, ?) (<17,0,B>, ?) (<18,0,A>, ?) (<18,0,B>, ?) (<19,0,A>, ?) (<19,0,B>, ?) (<20,0,A>, ?) (<20,0,B>, ?) (<21,0,A>, ?) (<21,0,B>, ?) (<22,0,A>, ?) (<22,0,B>, ?) (<23,0,A>, ?) (<23,0,B>, ?) (<24,0,A>, ?) (<24,0,B>, ?) (<25,0,A>, ?) (<25,0,B>, ?) (<26,0,A>, ?) (<26,0,B>, ?) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [23,24] * Step 21: LeafRules WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 12. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (2 + A,2) 13. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb5in(A,0) [A >= 0 && 0 >= A] (2 + A,2) 14. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb2in(A,B) [A >= 1 + B && C$ >= 1 + D$] (?,2) 15. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb3in(A,B) [A >= 1 + B && D$ >= C$] (?,2) 16. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb6in(-1 + A,B) [B >= A] (3 + A,2) 17. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [C >= 1 + D] (?,2) 18. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb4in(A,1 + B) [D >= C] (?,2) 19. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,2) 20. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb2in(A,1 + B) [A >= 2 + B && C$$ >= 1 + D$$] (?,3) 21. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb3in(A,1 + B) [A >= 2 + B && D$$ >= C$$] (?,3) 22. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb6in(-1 + A,1 + B) [1 + B >= A] (?,3) 25. evalsipmabubblestart(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (1,4) 26. evalsipmabubblestart(A,B) -> evalsipmabubblebb5in(A,0) [A >= 0 && 0 >= A] (1,4) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [12->{17,18},13->{},14->{19},15->{20,21,22},16->{12,13},17->{20,21,22},18->{14,15,16},19->{14,15,16} ,20->{19},21->{20,21,22},22->{12,13},25->{17,18},26->{}] Sizebounds: (<12,0,A>, ?) (<12,0,B>, ?) (<13,0,A>, ?) (<13,0,B>, ?) (<14,0,A>, ?) (<14,0,B>, ?) (<15,0,A>, ?) (<15,0,B>, ?) (<16,0,A>, ?) (<16,0,B>, ?) (<17,0,A>, ?) (<17,0,B>, ?) (<18,0,A>, ?) (<18,0,B>, ?) (<19,0,A>, ?) (<19,0,B>, ?) (<20,0,A>, ?) (<20,0,B>, ?) (<21,0,A>, ?) (<21,0,B>, ?) (<22,0,A>, ?) (<22,0,B>, ?) (<25,0,A>, ?) (<25,0,B>, ?) (<26,0,A>, ?) (<26,0,B>, ?) + Applied Processor: LeafRules + Details: The following transitions are estimated by its predecessors and are removed [13] * Step 22: LocalSizeboundsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 12. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (2 + A,2) 14. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb2in(A,B) [A >= 1 + B && C$ >= 1 + D$] (?,2) 15. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb3in(A,B) [A >= 1 + B && D$ >= C$] (?,2) 16. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb6in(-1 + A,B) [B >= A] (3 + A,2) 17. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [C >= 1 + D] (?,2) 18. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb4in(A,1 + B) [D >= C] (?,2) 19. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,2) 20. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb2in(A,1 + B) [A >= 2 + B && C$$ >= 1 + D$$] (?,3) 21. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb3in(A,1 + B) [A >= 2 + B && D$$ >= C$$] (?,3) 22. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb6in(-1 + A,1 + B) [1 + B >= A] (?,3) 25. evalsipmabubblestart(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (1,4) 26. evalsipmabubblestart(A,B) -> evalsipmabubblebb5in(A,0) [A >= 0 && 0 >= A] (1,4) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [12->{17,18},14->{19},15->{20,21,22},16->{12},17->{20,21,22},18->{14,15,16},19->{14,15,16},20->{19} ,21->{20,21,22},22->{12},25->{17,18},26->{}] Sizebounds: (<12,0,A>, ?) (<12,0,B>, ?) (<14,0,A>, ?) (<14,0,B>, ?) (<15,0,A>, ?) (<15,0,B>, ?) (<16,0,A>, ?) (<16,0,B>, ?) (<17,0,A>, ?) (<17,0,B>, ?) (<18,0,A>, ?) (<18,0,B>, ?) (<19,0,A>, ?) (<19,0,B>, ?) (<20,0,A>, ?) (<20,0,B>, ?) (<21,0,A>, ?) (<21,0,B>, ?) (<22,0,A>, ?) (<22,0,B>, ?) (<25,0,A>, ?) (<25,0,B>, ?) (<26,0,A>, ?) (<26,0,B>, ?) + Applied Processor: LocalSizeboundsProc + Details: LocalSizebounds generated; rvgraph (<12,0,A>, A, .= 0) (<12,0,B>, 0, .= 0) (<14,0,A>, A, .= 0) (<14,0,B>, B, .= 0) (<15,0,A>, A, .= 0) (<15,0,B>, B, .= 0) (<16,0,A>, 1 + A, .+ 1) (<16,0,B>, B, .= 0) (<17,0,A>, A, .= 0) (<17,0,B>, B, .= 0) (<18,0,A>, A, .= 0) (<18,0,B>, 1 + B, .+ 1) (<19,0,A>, A, .= 0) (<19,0,B>, 1 + B, .+ 1) (<20,0,A>, A, .= 0) (<20,0,B>, 1 + B, .+ 1) (<21,0,A>, A, .= 0) (<21,0,B>, 1 + B, .+ 1) (<22,0,A>, 1 + A, .+ 1) (<22,0,B>, 1 + B, .+ 1) (<25,0,A>, A, .= 0) (<25,0,B>, 0, .= 0) (<26,0,A>, A, .= 0) (<26,0,B>, 0, .= 0) * Step 23: SizeboundsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 12. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (2 + A,2) 14. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb2in(A,B) [A >= 1 + B && C$ >= 1 + D$] (?,2) 15. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb3in(A,B) [A >= 1 + B && D$ >= C$] (?,2) 16. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb6in(-1 + A,B) [B >= A] (3 + A,2) 17. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [C >= 1 + D] (?,2) 18. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb4in(A,1 + B) [D >= C] (?,2) 19. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,2) 20. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb2in(A,1 + B) [A >= 2 + B && C$$ >= 1 + D$$] (?,3) 21. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb3in(A,1 + B) [A >= 2 + B && D$$ >= C$$] (?,3) 22. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb6in(-1 + A,1 + B) [1 + B >= A] (?,3) 25. evalsipmabubblestart(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (1,4) 26. evalsipmabubblestart(A,B) -> evalsipmabubblebb5in(A,0) [A >= 0 && 0 >= A] (1,4) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [12->{17,18},14->{19},15->{20,21,22},16->{12},17->{20,21,22},18->{14,15,16},19->{14,15,16},20->{19} ,21->{20,21,22},22->{12},25->{17,18},26->{}] Sizebounds: (<12,0,A>, ?) (<12,0,B>, ?) (<14,0,A>, ?) (<14,0,B>, ?) (<15,0,A>, ?) (<15,0,B>, ?) (<16,0,A>, ?) (<16,0,B>, ?) (<17,0,A>, ?) (<17,0,B>, ?) (<18,0,A>, ?) (<18,0,B>, ?) (<19,0,A>, ?) (<19,0,B>, ?) (<20,0,A>, ?) (<20,0,B>, ?) (<21,0,A>, ?) (<21,0,B>, ?) (<22,0,A>, ?) (<22,0,B>, ?) (<25,0,A>, ?) (<25,0,B>, ?) (<26,0,A>, ?) (<26,0,B>, ?) + Applied Processor: SizeboundsProc + Details: Sizebounds computed: (<12,0,A>, ?) (<12,0,B>, 0) (<14,0,A>, ?) (<14,0,B>, ?) (<15,0,A>, ?) (<15,0,B>, ?) (<16,0,A>, ?) (<16,0,B>, ?) (<17,0,A>, ?) (<17,0,B>, 0) (<18,0,A>, ?) (<18,0,B>, 1) (<19,0,A>, ?) (<19,0,B>, ?) (<20,0,A>, ?) (<20,0,B>, ?) (<21,0,A>, ?) (<21,0,B>, ?) (<22,0,A>, ?) (<22,0,B>, ?) (<25,0,A>, A) (<25,0,B>, 0) (<26,0,A>, A) (<26,0,B>, 0) * Step 24: LocationConstraintsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 12. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (2 + A,2) 14. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb2in(A,B) [A >= 1 + B && C$ >= 1 + D$] (?,2) 15. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb3in(A,B) [A >= 1 + B && D$ >= C$] (?,2) 16. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb6in(-1 + A,B) [B >= A] (3 + A,2) 17. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [C >= 1 + D] (?,2) 18. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb4in(A,1 + B) [D >= C] (?,2) 19. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,2) 20. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb2in(A,1 + B) [A >= 2 + B && C$$ >= 1 + D$$] (?,3) 21. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb3in(A,1 + B) [A >= 2 + B && D$$ >= C$$] (?,3) 22. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb6in(-1 + A,1 + B) [1 + B >= A] (?,3) 25. evalsipmabubblestart(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (1,4) 26. evalsipmabubblestart(A,B) -> evalsipmabubblebb5in(A,0) [A >= 0 && 0 >= A] (1,4) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [12->{17,18},14->{19},15->{20,21,22},16->{12},17->{20,21,22},18->{14,15,16},19->{14,15,16},20->{19} ,21->{20,21,22},22->{12},25->{17,18},26->{}] Sizebounds: (<12,0,A>, ?) (<12,0,B>, 0) (<14,0,A>, ?) (<14,0,B>, ?) (<15,0,A>, ?) (<15,0,B>, ?) (<16,0,A>, ?) (<16,0,B>, ?) (<17,0,A>, ?) (<17,0,B>, 0) (<18,0,A>, ?) (<18,0,B>, 1) (<19,0,A>, ?) (<19,0,B>, ?) (<20,0,A>, ?) (<20,0,B>, ?) (<21,0,A>, ?) (<21,0,B>, ?) (<22,0,A>, ?) (<22,0,B>, ?) (<25,0,A>, A) (<25,0,B>, 0) (<26,0,A>, A) (<26,0,B>, 0) + Applied Processor: LocationConstraintsProc + Details: We computed the location constraints 12 : True 14 : True 15 : True 16 : True 17 : [A >= 0] 18 : [A >= 0] 19 : [A >= 1 + B] 20 : True 21 : True 22 : True 25 : True 26 : True . * Step 25: PolyRank WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 12. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (2 + A,2) 14. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb2in(A,B) [A >= 1 + B && C$ >= 1 + D$] (?,2) 15. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb3in(A,B) [A >= 1 + B && D$ >= C$] (?,2) 16. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb6in(-1 + A,B) [B >= A] (3 + A,2) 17. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [C >= 1 + D] (?,2) 18. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb4in(A,1 + B) [D >= C] (?,2) 19. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,2) 20. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb2in(A,1 + B) [A >= 2 + B && C$$ >= 1 + D$$] (?,3) 21. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb3in(A,1 + B) [A >= 2 + B && D$$ >= C$$] (?,3) 22. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb6in(-1 + A,1 + B) [1 + B >= A] (?,3) 25. evalsipmabubblestart(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (1,4) 26. evalsipmabubblestart(A,B) -> evalsipmabubblebb5in(A,0) [A >= 0 && 0 >= A] (1,4) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [12->{17,18},14->{19},15->{20,21,22},16->{12},17->{20,21,22},18->{14,15,16},19->{14,15,16},20->{19} ,21->{20,21,22},22->{12},25->{17,18},26->{}] Sizebounds: (<12,0,A>, ?) (<12,0,B>, 0) (<14,0,A>, ?) (<14,0,B>, ?) (<15,0,A>, ?) (<15,0,B>, ?) (<16,0,A>, ?) (<16,0,B>, ?) (<17,0,A>, ?) (<17,0,B>, 0) (<18,0,A>, ?) (<18,0,B>, 1) (<19,0,A>, ?) (<19,0,B>, ?) (<20,0,A>, ?) (<20,0,B>, ?) (<21,0,A>, ?) (<21,0,B>, ?) (<22,0,A>, ?) (<22,0,B>, ?) (<25,0,A>, A) (<25,0,B>, 0) (<26,0,A>, A) (<26,0,B>, 0) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [16,18,19,14,20,15,17,21,22], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(evalsipmabubblebb1in) = 1 p(evalsipmabubblebb2in) = 1 p(evalsipmabubblebb3in) = 1 p(evalsipmabubblebb4in) = 1 p(evalsipmabubblebb6in) = 0 The following rules are strictly oriented: [B >= A] ==> evalsipmabubblebb4in(A,B) = 1 > 0 = evalsipmabubblebb6in(-1 + A,B) [1 + B >= A] ==> evalsipmabubblebb3in(A,B) = 1 > 0 = evalsipmabubblebb6in(-1 + A,1 + B) The following rules are weakly oriented: [A >= 1 + B && C$ >= 1 + D$] ==> evalsipmabubblebb4in(A,B) = 1 >= 1 = evalsipmabubblebb2in(A,B) [A >= 1 + B && D$ >= C$] ==> evalsipmabubblebb4in(A,B) = 1 >= 1 = evalsipmabubblebb3in(A,B) [C >= 1 + D] ==> evalsipmabubblebb1in(A,B) = 1 >= 1 = evalsipmabubblebb3in(A,B) [D >= C] ==> evalsipmabubblebb1in(A,B) = 1 >= 1 = evalsipmabubblebb4in(A,1 + B) True ==> evalsipmabubblebb2in(A,B) = 1 >= 1 = evalsipmabubblebb4in(A,1 + B) [A >= 2 + B && C$$ >= 1 + D$$] ==> evalsipmabubblebb3in(A,B) = 1 >= 1 = evalsipmabubblebb2in(A,1 + B) [A >= 2 + B && D$$ >= C$$] ==> evalsipmabubblebb3in(A,B) = 1 >= 1 = evalsipmabubblebb3in(A,1 + B) We use the following global sizebounds: (<12,0,A>, ?) (<12,0,B>, 0) (<14,0,A>, ?) (<14,0,B>, ?) (<15,0,A>, ?) (<15,0,B>, ?) (<16,0,A>, ?) (<16,0,B>, ?) (<17,0,A>, ?) (<17,0,B>, 0) (<18,0,A>, ?) (<18,0,B>, 1) (<19,0,A>, ?) (<19,0,B>, ?) (<20,0,A>, ?) (<20,0,B>, ?) (<21,0,A>, ?) (<21,0,B>, ?) (<22,0,A>, ?) (<22,0,B>, ?) (<25,0,A>, A) (<25,0,B>, 0) (<26,0,A>, A) (<26,0,B>, 0) * Step 26: KnowledgePropagation WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 12. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (2 + A,2) 14. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb2in(A,B) [A >= 1 + B && C$ >= 1 + D$] (?,2) 15. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb3in(A,B) [A >= 1 + B && D$ >= C$] (?,2) 16. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb6in(-1 + A,B) [B >= A] (3 + A,2) 17. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [C >= 1 + D] (?,2) 18. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb4in(A,1 + B) [D >= C] (?,2) 19. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,2) 20. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb2in(A,1 + B) [A >= 2 + B && C$$ >= 1 + D$$] (?,3) 21. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb3in(A,1 + B) [A >= 2 + B && D$$ >= C$$] (?,3) 22. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb6in(-1 + A,1 + B) [1 + B >= A] (3 + A,3) 25. evalsipmabubblestart(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (1,4) 26. evalsipmabubblestart(A,B) -> evalsipmabubblebb5in(A,0) [A >= 0 && 0 >= A] (1,4) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [12->{17,18},14->{19},15->{20,21,22},16->{12},17->{20,21,22},18->{14,15,16},19->{14,15,16},20->{19} ,21->{20,21,22},22->{12},25->{17,18},26->{}] Sizebounds: (<12,0,A>, ?) (<12,0,B>, 0) (<14,0,A>, ?) (<14,0,B>, ?) (<15,0,A>, ?) (<15,0,B>, ?) (<16,0,A>, ?) (<16,0,B>, ?) (<17,0,A>, ?) (<17,0,B>, 0) (<18,0,A>, ?) (<18,0,B>, 1) (<19,0,A>, ?) (<19,0,B>, ?) (<20,0,A>, ?) (<20,0,B>, ?) (<21,0,A>, ?) (<21,0,B>, ?) (<22,0,A>, ?) (<22,0,B>, ?) (<25,0,A>, A) (<25,0,B>, 0) (<26,0,A>, A) (<26,0,B>, 0) + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 27: SizeboundsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 12. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (2 + A,2) 14. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb2in(A,B) [A >= 1 + B && C$ >= 1 + D$] (?,2) 15. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb3in(A,B) [A >= 1 + B && D$ >= C$] (?,2) 16. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb6in(-1 + A,B) [B >= A] (3 + A,2) 17. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [C >= 1 + D] (3 + A,2) 18. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb4in(A,1 + B) [D >= C] (3 + A,2) 19. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,2) 20. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb2in(A,1 + B) [A >= 2 + B && C$$ >= 1 + D$$] (?,3) 21. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb3in(A,1 + B) [A >= 2 + B && D$$ >= C$$] (?,3) 22. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb6in(-1 + A,1 + B) [1 + B >= A] (3 + A,3) 25. evalsipmabubblestart(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (1,4) 26. evalsipmabubblestart(A,B) -> evalsipmabubblebb5in(A,0) [A >= 0 && 0 >= A] (1,4) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [12->{17,18},14->{19},15->{20,21,22},16->{12},17->{20,21,22},18->{14,15,16},19->{14,15,16},20->{19} ,21->{20,21,22},22->{12},25->{17,18},26->{}] Sizebounds: (<12,0,A>, ?) (<12,0,B>, 0) (<14,0,A>, ?) (<14,0,B>, ?) (<15,0,A>, ?) (<15,0,B>, ?) (<16,0,A>, ?) (<16,0,B>, ?) (<17,0,A>, ?) (<17,0,B>, 0) (<18,0,A>, ?) (<18,0,B>, 1) (<19,0,A>, ?) (<19,0,B>, ?) (<20,0,A>, ?) (<20,0,B>, ?) (<21,0,A>, ?) (<21,0,B>, ?) (<22,0,A>, ?) (<22,0,B>, ?) (<25,0,A>, A) (<25,0,B>, 0) (<26,0,A>, A) (<26,0,B>, 0) + Applied Processor: SizeboundsProc + Details: Sizebounds computed: (<12,0,A>, 6 + 3*A) (<12,0,B>, 0) (<14,0,A>, 6 + 3*A) (<14,0,B>, 6 + 3*A) (<15,0,A>, 6 + 3*A) (<15,0,B>, 6 + 3*A) (<16,0,A>, 6 + 3*A) (<16,0,B>, 6 + 3*A) (<17,0,A>, 6 + 3*A) (<17,0,B>, 0) (<18,0,A>, 6 + 3*A) (<18,0,B>, 1) (<19,0,A>, 6 + 3*A) (<19,0,B>, 6 + 3*A) (<20,0,A>, 6 + 3*A) (<20,0,B>, 6 + 3*A) (<21,0,A>, 6 + 3*A) (<21,0,B>, 6 + 3*A) (<22,0,A>, 6 + 3*A) (<22,0,B>, 7 + 3*A) (<25,0,A>, A) (<25,0,B>, 0) (<26,0,A>, A) (<26,0,B>, 0) * Step 28: PolyRank WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 12. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (2 + A,2) 14. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb2in(A,B) [A >= 1 + B && C$ >= 1 + D$] (?,2) 15. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb3in(A,B) [A >= 1 + B && D$ >= C$] (?,2) 16. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb6in(-1 + A,B) [B >= A] (3 + A,2) 17. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [C >= 1 + D] (3 + A,2) 18. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb4in(A,1 + B) [D >= C] (3 + A,2) 19. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,2) 20. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb2in(A,1 + B) [A >= 2 + B && C$$ >= 1 + D$$] (?,3) 21. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb3in(A,1 + B) [A >= 2 + B && D$$ >= C$$] (?,3) 22. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb6in(-1 + A,1 + B) [1 + B >= A] (3 + A,3) 25. evalsipmabubblestart(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (1,4) 26. evalsipmabubblestart(A,B) -> evalsipmabubblebb5in(A,0) [A >= 0 && 0 >= A] (1,4) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [12->{17,18},14->{19},15->{20,21,22},16->{12},17->{20,21,22},18->{14,15,16},19->{14,15,16},20->{19} ,21->{20,21,22},22->{12},25->{17,18},26->{}] Sizebounds: (<12,0,A>, 6 + 3*A) (<12,0,B>, 0) (<14,0,A>, 6 + 3*A) (<14,0,B>, 6 + 3*A) (<15,0,A>, 6 + 3*A) (<15,0,B>, 6 + 3*A) (<16,0,A>, 6 + 3*A) (<16,0,B>, 6 + 3*A) (<17,0,A>, 6 + 3*A) (<17,0,B>, 0) (<18,0,A>, 6 + 3*A) (<18,0,B>, 1) (<19,0,A>, 6 + 3*A) (<19,0,B>, 6 + 3*A) (<20,0,A>, 6 + 3*A) (<20,0,B>, 6 + 3*A) (<21,0,A>, 6 + 3*A) (<21,0,B>, 6 + 3*A) (<22,0,A>, 6 + 3*A) (<22,0,B>, 7 + 3*A) (<25,0,A>, A) (<25,0,B>, 0) (<26,0,A>, A) (<26,0,B>, 0) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [16,18,19,14,20,15,17,21,22], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(evalsipmabubblebb1in) = x1 + -1*x2 p(evalsipmabubblebb2in) = -2 + x1 + -1*x2 p(evalsipmabubblebb3in) = -1 + x1 + -1*x2 p(evalsipmabubblebb4in) = -1 + x1 + -1*x2 p(evalsipmabubblebb6in) = x1 + -1*x2 The following rules are strictly oriented: [A >= 2 + B && D$$ >= C$$] ==> evalsipmabubblebb3in(A,B) = -1 + A + -1*B > -2 + A + -1*B = evalsipmabubblebb3in(A,1 + B) The following rules are weakly oriented: [A >= 1 + B && C$ >= 1 + D$] ==> evalsipmabubblebb4in(A,B) = -1 + A + -1*B >= -2 + A + -1*B = evalsipmabubblebb2in(A,B) [A >= 1 + B && D$ >= C$] ==> evalsipmabubblebb4in(A,B) = -1 + A + -1*B >= -1 + A + -1*B = evalsipmabubblebb3in(A,B) [B >= A] ==> evalsipmabubblebb4in(A,B) = -1 + A + -1*B >= -1 + A + -1*B = evalsipmabubblebb6in(-1 + A,B) [C >= 1 + D] ==> evalsipmabubblebb1in(A,B) = A + -1*B >= -1 + A + -1*B = evalsipmabubblebb3in(A,B) [D >= C] ==> evalsipmabubblebb1in(A,B) = A + -1*B >= -2 + A + -1*B = evalsipmabubblebb4in(A,1 + B) True ==> evalsipmabubblebb2in(A,B) = -2 + A + -1*B >= -2 + A + -1*B = evalsipmabubblebb4in(A,1 + B) [A >= 2 + B && C$$ >= 1 + D$$] ==> evalsipmabubblebb3in(A,B) = -1 + A + -1*B >= -3 + A + -1*B = evalsipmabubblebb2in(A,1 + B) [1 + B >= A] ==> evalsipmabubblebb3in(A,B) = -1 + A + -1*B >= -2 + A + -1*B = evalsipmabubblebb6in(-1 + A,1 + B) We use the following global sizebounds: (<12,0,A>, 6 + 3*A) (<12,0,B>, 0) (<14,0,A>, 6 + 3*A) (<14,0,B>, 6 + 3*A) (<15,0,A>, 6 + 3*A) (<15,0,B>, 6 + 3*A) (<16,0,A>, 6 + 3*A) (<16,0,B>, 6 + 3*A) (<17,0,A>, 6 + 3*A) (<17,0,B>, 0) (<18,0,A>, 6 + 3*A) (<18,0,B>, 1) (<19,0,A>, 6 + 3*A) (<19,0,B>, 6 + 3*A) (<20,0,A>, 6 + 3*A) (<20,0,B>, 6 + 3*A) (<21,0,A>, 6 + 3*A) (<21,0,B>, 6 + 3*A) (<22,0,A>, 6 + 3*A) (<22,0,B>, 7 + 3*A) (<25,0,A>, A) (<25,0,B>, 0) (<26,0,A>, A) (<26,0,B>, 0) * Step 29: PolyRank WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 12. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (2 + A,2) 14. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb2in(A,B) [A >= 1 + B && C$ >= 1 + D$] (?,2) 15. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb3in(A,B) [A >= 1 + B && D$ >= C$] (?,2) 16. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb6in(-1 + A,B) [B >= A] (3 + A,2) 17. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [C >= 1 + D] (3 + A,2) 18. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb4in(A,1 + B) [D >= C] (3 + A,2) 19. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,2) 20. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb2in(A,1 + B) [A >= 2 + B && C$$ >= 1 + D$$] (?,3) 21. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb3in(A,1 + B) [A >= 2 + B && D$$ >= C$$] (12 + 13*A + 3*A^2,3) 22. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb6in(-1 + A,1 + B) [1 + B >= A] (3 + A,3) 25. evalsipmabubblestart(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (1,4) 26. evalsipmabubblestart(A,B) -> evalsipmabubblebb5in(A,0) [A >= 0 && 0 >= A] (1,4) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [12->{17,18},14->{19},15->{20,21,22},16->{12},17->{20,21,22},18->{14,15,16},19->{14,15,16},20->{19} ,21->{20,21,22},22->{12},25->{17,18},26->{}] Sizebounds: (<12,0,A>, 6 + 3*A) (<12,0,B>, 0) (<14,0,A>, 6 + 3*A) (<14,0,B>, 6 + 3*A) (<15,0,A>, 6 + 3*A) (<15,0,B>, 6 + 3*A) (<16,0,A>, 6 + 3*A) (<16,0,B>, 6 + 3*A) (<17,0,A>, 6 + 3*A) (<17,0,B>, 0) (<18,0,A>, 6 + 3*A) (<18,0,B>, 1) (<19,0,A>, 6 + 3*A) (<19,0,B>, 6 + 3*A) (<20,0,A>, 6 + 3*A) (<20,0,B>, 6 + 3*A) (<21,0,A>, 6 + 3*A) (<21,0,B>, 6 + 3*A) (<22,0,A>, 6 + 3*A) (<22,0,B>, 7 + 3*A) (<25,0,A>, A) (<25,0,B>, 0) (<26,0,A>, A) (<26,0,B>, 0) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [16,18,19,14,20,15,17,21,22], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(evalsipmabubblebb1in) = x1 + -1*x2 p(evalsipmabubblebb2in) = -2 + x1 + -1*x2 p(evalsipmabubblebb3in) = -1 + x1 + -1*x2 p(evalsipmabubblebb4in) = -1 + x1 + -1*x2 p(evalsipmabubblebb6in) = x1 + -1*x2 The following rules are strictly oriented: [A >= 2 + B && C$$ >= 1 + D$$] ==> evalsipmabubblebb3in(A,B) = -1 + A + -1*B > -3 + A + -1*B = evalsipmabubblebb2in(A,1 + B) [A >= 2 + B && D$$ >= C$$] ==> evalsipmabubblebb3in(A,B) = -1 + A + -1*B > -2 + A + -1*B = evalsipmabubblebb3in(A,1 + B) The following rules are weakly oriented: [A >= 1 + B && C$ >= 1 + D$] ==> evalsipmabubblebb4in(A,B) = -1 + A + -1*B >= -2 + A + -1*B = evalsipmabubblebb2in(A,B) [A >= 1 + B && D$ >= C$] ==> evalsipmabubblebb4in(A,B) = -1 + A + -1*B >= -1 + A + -1*B = evalsipmabubblebb3in(A,B) [B >= A] ==> evalsipmabubblebb4in(A,B) = -1 + A + -1*B >= -1 + A + -1*B = evalsipmabubblebb6in(-1 + A,B) [C >= 1 + D] ==> evalsipmabubblebb1in(A,B) = A + -1*B >= -1 + A + -1*B = evalsipmabubblebb3in(A,B) [D >= C] ==> evalsipmabubblebb1in(A,B) = A + -1*B >= -2 + A + -1*B = evalsipmabubblebb4in(A,1 + B) True ==> evalsipmabubblebb2in(A,B) = -2 + A + -1*B >= -2 + A + -1*B = evalsipmabubblebb4in(A,1 + B) [1 + B >= A] ==> evalsipmabubblebb3in(A,B) = -1 + A + -1*B >= -2 + A + -1*B = evalsipmabubblebb6in(-1 + A,1 + B) We use the following global sizebounds: (<12,0,A>, 6 + 3*A) (<12,0,B>, 0) (<14,0,A>, 6 + 3*A) (<14,0,B>, 6 + 3*A) (<15,0,A>, 6 + 3*A) (<15,0,B>, 6 + 3*A) (<16,0,A>, 6 + 3*A) (<16,0,B>, 6 + 3*A) (<17,0,A>, 6 + 3*A) (<17,0,B>, 0) (<18,0,A>, 6 + 3*A) (<18,0,B>, 1) (<19,0,A>, 6 + 3*A) (<19,0,B>, 6 + 3*A) (<20,0,A>, 6 + 3*A) (<20,0,B>, 6 + 3*A) (<21,0,A>, 6 + 3*A) (<21,0,B>, 6 + 3*A) (<22,0,A>, 6 + 3*A) (<22,0,B>, 7 + 3*A) (<25,0,A>, A) (<25,0,B>, 0) (<26,0,A>, A) (<26,0,B>, 0) * Step 30: PolyRank WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 12. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (2 + A,2) 14. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb2in(A,B) [A >= 1 + B && C$ >= 1 + D$] (?,2) 15. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb3in(A,B) [A >= 1 + B && D$ >= C$] (?,2) 16. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb6in(-1 + A,B) [B >= A] (3 + A,2) 17. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [C >= 1 + D] (3 + A,2) 18. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb4in(A,1 + B) [D >= C] (3 + A,2) 19. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,2) 20. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb2in(A,1 + B) [A >= 2 + B && C$$ >= 1 + D$$] (12 + 13*A + 3*A^2,3) 21. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb3in(A,1 + B) [A >= 2 + B && D$$ >= C$$] (12 + 13*A + 3*A^2,3) 22. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb6in(-1 + A,1 + B) [1 + B >= A] (3 + A,3) 25. evalsipmabubblestart(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (1,4) 26. evalsipmabubblestart(A,B) -> evalsipmabubblebb5in(A,0) [A >= 0 && 0 >= A] (1,4) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [12->{17,18},14->{19},15->{20,21,22},16->{12},17->{20,21,22},18->{14,15,16},19->{14,15,16},20->{19} ,21->{20,21,22},22->{12},25->{17,18},26->{}] Sizebounds: (<12,0,A>, 6 + 3*A) (<12,0,B>, 0) (<14,0,A>, 6 + 3*A) (<14,0,B>, 6 + 3*A) (<15,0,A>, 6 + 3*A) (<15,0,B>, 6 + 3*A) (<16,0,A>, 6 + 3*A) (<16,0,B>, 6 + 3*A) (<17,0,A>, 6 + 3*A) (<17,0,B>, 0) (<18,0,A>, 6 + 3*A) (<18,0,B>, 1) (<19,0,A>, 6 + 3*A) (<19,0,B>, 6 + 3*A) (<20,0,A>, 6 + 3*A) (<20,0,B>, 6 + 3*A) (<21,0,A>, 6 + 3*A) (<21,0,B>, 6 + 3*A) (<22,0,A>, 6 + 3*A) (<22,0,B>, 7 + 3*A) (<25,0,A>, A) (<25,0,B>, 0) (<26,0,A>, A) (<26,0,B>, 0) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [16,18,19,14,20,15,17,21,22], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(evalsipmabubblebb1in) = 1 + x1 + -1*x2 p(evalsipmabubblebb2in) = 1 + x1 + -1*x2 p(evalsipmabubblebb3in) = x1 + -1*x2 p(evalsipmabubblebb4in) = 2 + x1 + -1*x2 p(evalsipmabubblebb6in) = 2 + x1 + -1*x2 The following rules are strictly oriented: [A >= 1 + B && C$ >= 1 + D$] ==> evalsipmabubblebb4in(A,B) = 2 + A + -1*B > 1 + A + -1*B = evalsipmabubblebb2in(A,B) [A >= 1 + B && D$ >= C$] ==> evalsipmabubblebb4in(A,B) = 2 + A + -1*B > A + -1*B = evalsipmabubblebb3in(A,B) [A >= 2 + B && D$$ >= C$$] ==> evalsipmabubblebb3in(A,B) = A + -1*B > -1 + A + -1*B = evalsipmabubblebb3in(A,1 + B) The following rules are weakly oriented: [B >= A] ==> evalsipmabubblebb4in(A,B) = 2 + A + -1*B >= 1 + A + -1*B = evalsipmabubblebb6in(-1 + A,B) [C >= 1 + D] ==> evalsipmabubblebb1in(A,B) = 1 + A + -1*B >= A + -1*B = evalsipmabubblebb3in(A,B) [D >= C] ==> evalsipmabubblebb1in(A,B) = 1 + A + -1*B >= 1 + A + -1*B = evalsipmabubblebb4in(A,1 + B) True ==> evalsipmabubblebb2in(A,B) = 1 + A + -1*B >= 1 + A + -1*B = evalsipmabubblebb4in(A,1 + B) [A >= 2 + B && C$$ >= 1 + D$$] ==> evalsipmabubblebb3in(A,B) = A + -1*B >= A + -1*B = evalsipmabubblebb2in(A,1 + B) [1 + B >= A] ==> evalsipmabubblebb3in(A,B) = A + -1*B >= A + -1*B = evalsipmabubblebb6in(-1 + A,1 + B) We use the following global sizebounds: (<12,0,A>, 6 + 3*A) (<12,0,B>, 0) (<14,0,A>, 6 + 3*A) (<14,0,B>, 6 + 3*A) (<15,0,A>, 6 + 3*A) (<15,0,B>, 6 + 3*A) (<16,0,A>, 6 + 3*A) (<16,0,B>, 6 + 3*A) (<17,0,A>, 6 + 3*A) (<17,0,B>, 0) (<18,0,A>, 6 + 3*A) (<18,0,B>, 1) (<19,0,A>, 6 + 3*A) (<19,0,B>, 6 + 3*A) (<20,0,A>, 6 + 3*A) (<20,0,B>, 6 + 3*A) (<21,0,A>, 6 + 3*A) (<21,0,B>, 6 + 3*A) (<22,0,A>, 6 + 3*A) (<22,0,B>, 7 + 3*A) (<25,0,A>, A) (<25,0,B>, 0) (<26,0,A>, A) (<26,0,B>, 0) * Step 31: KnowledgePropagation WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 12. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (2 + A,2) 14. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb2in(A,B) [A >= 1 + B && C$ >= 1 + D$] (15 + 14*A + 3*A^2,2) 15. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb3in(A,B) [A >= 1 + B && D$ >= C$] (15 + 14*A + 3*A^2,2) 16. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb6in(-1 + A,B) [B >= A] (3 + A,2) 17. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [C >= 1 + D] (3 + A,2) 18. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb4in(A,1 + B) [D >= C] (3 + A,2) 19. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (?,2) 20. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb2in(A,1 + B) [A >= 2 + B && C$$ >= 1 + D$$] (12 + 13*A + 3*A^2,3) 21. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb3in(A,1 + B) [A >= 2 + B && D$$ >= C$$] (12 + 13*A + 3*A^2,3) 22. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb6in(-1 + A,1 + B) [1 + B >= A] (3 + A,3) 25. evalsipmabubblestart(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (1,4) 26. evalsipmabubblestart(A,B) -> evalsipmabubblebb5in(A,0) [A >= 0 && 0 >= A] (1,4) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [12->{17,18},14->{19},15->{20,21,22},16->{12},17->{20,21,22},18->{14,15,16},19->{14,15,16},20->{19} ,21->{20,21,22},22->{12},25->{17,18},26->{}] Sizebounds: (<12,0,A>, 6 + 3*A) (<12,0,B>, 0) (<14,0,A>, 6 + 3*A) (<14,0,B>, 6 + 3*A) (<15,0,A>, 6 + 3*A) (<15,0,B>, 6 + 3*A) (<16,0,A>, 6 + 3*A) (<16,0,B>, 6 + 3*A) (<17,0,A>, 6 + 3*A) (<17,0,B>, 0) (<18,0,A>, 6 + 3*A) (<18,0,B>, 1) (<19,0,A>, 6 + 3*A) (<19,0,B>, 6 + 3*A) (<20,0,A>, 6 + 3*A) (<20,0,B>, 6 + 3*A) (<21,0,A>, 6 + 3*A) (<21,0,B>, 6 + 3*A) (<22,0,A>, 6 + 3*A) (<22,0,B>, 7 + 3*A) (<25,0,A>, A) (<25,0,B>, 0) (<26,0,A>, A) (<26,0,B>, 0) + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 32: SizeboundsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 12. evalsipmabubblebb6in(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (2 + A,2) 14. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb2in(A,B) [A >= 1 + B && C$ >= 1 + D$] (15 + 14*A + 3*A^2,2) 15. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb3in(A,B) [A >= 1 + B && D$ >= C$] (15 + 14*A + 3*A^2,2) 16. evalsipmabubblebb4in(A,B) -> evalsipmabubblebb6in(-1 + A,B) [B >= A] (3 + A,2) 17. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb3in(A,B) [C >= 1 + D] (3 + A,2) 18. evalsipmabubblebb1in(A,B) -> evalsipmabubblebb4in(A,1 + B) [D >= C] (3 + A,2) 19. evalsipmabubblebb2in(A,B) -> evalsipmabubblebb4in(A,1 + B) True (27 + 27*A + 6*A^2,2) 20. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb2in(A,1 + B) [A >= 2 + B && C$$ >= 1 + D$$] (12 + 13*A + 3*A^2,3) 21. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb3in(A,1 + B) [A >= 2 + B && D$$ >= C$$] (12 + 13*A + 3*A^2,3) 22. evalsipmabubblebb3in(A,B) -> evalsipmabubblebb6in(-1 + A,1 + B) [1 + B >= A] (3 + A,3) 25. evalsipmabubblestart(A,B) -> evalsipmabubblebb1in(A,0) [A >= 0 && A >= 1] (1,4) 26. evalsipmabubblestart(A,B) -> evalsipmabubblebb5in(A,0) [A >= 0 && 0 >= A] (1,4) Signature: {(evalsipmabubblebb1in,2) ;(evalsipmabubblebb2in,2) ;(evalsipmabubblebb3in,2) ;(evalsipmabubblebb4in,2) ;(evalsipmabubblebb5in,2) ;(evalsipmabubblebb6in,2) ;(evalsipmabubbleentryin,2) ;(evalsipmabubblereturnin,2) ;(evalsipmabubblestart,2) ;(evalsipmabubblestop,2)} Flow Graph: [12->{17,18},14->{19},15->{20,21,22},16->{12},17->{20,21,22},18->{14,15,16},19->{14,15,16},20->{19} ,21->{20,21,22},22->{12},25->{17,18},26->{}] Sizebounds: (<12,0,A>, 6 + 3*A) (<12,0,B>, 0) (<14,0,A>, 6 + 3*A) (<14,0,B>, 6 + 3*A) (<15,0,A>, 6 + 3*A) (<15,0,B>, 6 + 3*A) (<16,0,A>, 6 + 3*A) (<16,0,B>, 6 + 3*A) (<17,0,A>, 6 + 3*A) (<17,0,B>, 0) (<18,0,A>, 6 + 3*A) (<18,0,B>, 1) (<19,0,A>, 6 + 3*A) (<19,0,B>, 6 + 3*A) (<20,0,A>, 6 + 3*A) (<20,0,B>, 6 + 3*A) (<21,0,A>, 6 + 3*A) (<21,0,B>, 6 + 3*A) (<22,0,A>, 6 + 3*A) (<22,0,B>, 7 + 3*A) (<25,0,A>, A) (<25,0,B>, 0) (<26,0,A>, A) (<26,0,B>, 0) + Applied Processor: SizeboundsProc + Details: The problem is already solved. WORST_CASE(?,O(n^2))