WORST_CASE(?,O(n^1)) * Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalspeedpldi4start(A,B) -> evalspeedpldi4entryin(A,B) True (1,1) 1. evalspeedpldi4entryin(A,B) -> evalspeedpldi4returnin(A,B) [0 >= A] (?,1) 2. evalspeedpldi4entryin(A,B) -> evalspeedpldi4returnin(A,B) [A >= B] (?,1) 3. evalspeedpldi4entryin(A,B) -> evalspeedpldi4bb5in(A,B) [A >= 1 && B >= 1 + A] (?,1) 4. evalspeedpldi4bb5in(A,B) -> evalspeedpldi4bb2in(A,B) [B >= 1] (?,1) 5. evalspeedpldi4bb5in(A,B) -> evalspeedpldi4returnin(A,B) [0 >= B] (?,1) 6. evalspeedpldi4bb2in(A,B) -> evalspeedpldi4bb3in(A,B) [A >= 1 + B] (?,1) 7. evalspeedpldi4bb2in(A,B) -> evalspeedpldi4bb4in(A,B) [B >= A] (?,1) 8. evalspeedpldi4bb3in(A,B) -> evalspeedpldi4bb5in(A,-1 + B) True (?,1) 9. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb5in(A,-1*A + B) True (?,1) 10. evalspeedpldi4returnin(A,B) -> evalspeedpldi4stop(A,B) True (?,1) Signature: {(evalspeedpldi4bb2in,2) ;(evalspeedpldi4bb3in,2) ;(evalspeedpldi4bb4in,2) ;(evalspeedpldi4bb5in,2) ;(evalspeedpldi4entryin,2) ;(evalspeedpldi4returnin,2) ;(evalspeedpldi4start,2) ;(evalspeedpldi4stop,2)} Flow Graph: [0->{1,2,3},1->{10},2->{10},3->{4,5},4->{6,7},5->{10},6->{8},7->{9},8->{4,5},9->{4,5},10->{}] + 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>, B, .= 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>, 1 + B, .+ 1) (< 9,0,A>, A, .= 0) (< 9,0,B>, A + B, .* 0) (<10,0,A>, A, .= 0) (<10,0,B>, B, .= 0) * Step 2: SizeboundsProc WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalspeedpldi4start(A,B) -> evalspeedpldi4entryin(A,B) True (1,1) 1. evalspeedpldi4entryin(A,B) -> evalspeedpldi4returnin(A,B) [0 >= A] (?,1) 2. evalspeedpldi4entryin(A,B) -> evalspeedpldi4returnin(A,B) [A >= B] (?,1) 3. evalspeedpldi4entryin(A,B) -> evalspeedpldi4bb5in(A,B) [A >= 1 && B >= 1 + A] (?,1) 4. evalspeedpldi4bb5in(A,B) -> evalspeedpldi4bb2in(A,B) [B >= 1] (?,1) 5. evalspeedpldi4bb5in(A,B) -> evalspeedpldi4returnin(A,B) [0 >= B] (?,1) 6. evalspeedpldi4bb2in(A,B) -> evalspeedpldi4bb3in(A,B) [A >= 1 + B] (?,1) 7. evalspeedpldi4bb2in(A,B) -> evalspeedpldi4bb4in(A,B) [B >= A] (?,1) 8. evalspeedpldi4bb3in(A,B) -> evalspeedpldi4bb5in(A,-1 + B) True (?,1) 9. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb5in(A,-1*A + B) True (?,1) 10. evalspeedpldi4returnin(A,B) -> evalspeedpldi4stop(A,B) True (?,1) Signature: {(evalspeedpldi4bb2in,2) ;(evalspeedpldi4bb3in,2) ;(evalspeedpldi4bb4in,2) ;(evalspeedpldi4bb5in,2) ;(evalspeedpldi4entryin,2) ;(evalspeedpldi4returnin,2) ;(evalspeedpldi4start,2) ;(evalspeedpldi4stop,2)} Flow Graph: [0->{1,2,3},1->{10},2->{10},3->{4,5},4->{6,7},5->{10},6->{8},7->{9},8->{4,5},9->{4,5},10->{}] 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>, ?) + 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>, A) (< 2,0,B>, B) (< 3,0,A>, A) (< 3,0,B>, B) (< 4,0,A>, A) (< 4,0,B>, ?) (< 5,0,A>, A) (< 5,0,B>, ?) (< 6,0,A>, A) (< 6,0,B>, A) (< 7,0,A>, A) (< 7,0,B>, ?) (< 8,0,A>, A) (< 8,0,B>, A) (< 9,0,A>, A) (< 9,0,B>, ?) (<10,0,A>, A) (<10,0,B>, ?) * Step 3: UnsatPaths WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalspeedpldi4start(A,B) -> evalspeedpldi4entryin(A,B) True (1,1) 1. evalspeedpldi4entryin(A,B) -> evalspeedpldi4returnin(A,B) [0 >= A] (?,1) 2. evalspeedpldi4entryin(A,B) -> evalspeedpldi4returnin(A,B) [A >= B] (?,1) 3. evalspeedpldi4entryin(A,B) -> evalspeedpldi4bb5in(A,B) [A >= 1 && B >= 1 + A] (?,1) 4. evalspeedpldi4bb5in(A,B) -> evalspeedpldi4bb2in(A,B) [B >= 1] (?,1) 5. evalspeedpldi4bb5in(A,B) -> evalspeedpldi4returnin(A,B) [0 >= B] (?,1) 6. evalspeedpldi4bb2in(A,B) -> evalspeedpldi4bb3in(A,B) [A >= 1 + B] (?,1) 7. evalspeedpldi4bb2in(A,B) -> evalspeedpldi4bb4in(A,B) [B >= A] (?,1) 8. evalspeedpldi4bb3in(A,B) -> evalspeedpldi4bb5in(A,-1 + B) True (?,1) 9. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb5in(A,-1*A + B) True (?,1) 10. evalspeedpldi4returnin(A,B) -> evalspeedpldi4stop(A,B) True (?,1) Signature: {(evalspeedpldi4bb2in,2) ;(evalspeedpldi4bb3in,2) ;(evalspeedpldi4bb4in,2) ;(evalspeedpldi4bb5in,2) ;(evalspeedpldi4entryin,2) ;(evalspeedpldi4returnin,2) ;(evalspeedpldi4start,2) ;(evalspeedpldi4stop,2)} Flow Graph: [0->{1,2,3},1->{10},2->{10},3->{4,5},4->{6,7},5->{10},6->{8},7->{9},8->{4,5},9->{4,5},10->{}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 1,0,A>, A) (< 1,0,B>, B) (< 2,0,A>, A) (< 2,0,B>, B) (< 3,0,A>, A) (< 3,0,B>, B) (< 4,0,A>, A) (< 4,0,B>, ?) (< 5,0,A>, A) (< 5,0,B>, ?) (< 6,0,A>, A) (< 6,0,B>, A) (< 7,0,A>, A) (< 7,0,B>, ?) (< 8,0,A>, A) (< 8,0,B>, A) (< 9,0,A>, A) (< 9,0,B>, ?) (<10,0,A>, A) (<10,0,B>, ?) + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(3,5)] * Step 4: LeafRules WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalspeedpldi4start(A,B) -> evalspeedpldi4entryin(A,B) True (1,1) 1. evalspeedpldi4entryin(A,B) -> evalspeedpldi4returnin(A,B) [0 >= A] (?,1) 2. evalspeedpldi4entryin(A,B) -> evalspeedpldi4returnin(A,B) [A >= B] (?,1) 3. evalspeedpldi4entryin(A,B) -> evalspeedpldi4bb5in(A,B) [A >= 1 && B >= 1 + A] (?,1) 4. evalspeedpldi4bb5in(A,B) -> evalspeedpldi4bb2in(A,B) [B >= 1] (?,1) 5. evalspeedpldi4bb5in(A,B) -> evalspeedpldi4returnin(A,B) [0 >= B] (?,1) 6. evalspeedpldi4bb2in(A,B) -> evalspeedpldi4bb3in(A,B) [A >= 1 + B] (?,1) 7. evalspeedpldi4bb2in(A,B) -> evalspeedpldi4bb4in(A,B) [B >= A] (?,1) 8. evalspeedpldi4bb3in(A,B) -> evalspeedpldi4bb5in(A,-1 + B) True (?,1) 9. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb5in(A,-1*A + B) True (?,1) 10. evalspeedpldi4returnin(A,B) -> evalspeedpldi4stop(A,B) True (?,1) Signature: {(evalspeedpldi4bb2in,2) ;(evalspeedpldi4bb3in,2) ;(evalspeedpldi4bb4in,2) ;(evalspeedpldi4bb5in,2) ;(evalspeedpldi4entryin,2) ;(evalspeedpldi4returnin,2) ;(evalspeedpldi4start,2) ;(evalspeedpldi4stop,2)} Flow Graph: [0->{1,2,3},1->{10},2->{10},3->{4},4->{6,7},5->{10},6->{8},7->{9},8->{4,5},9->{4,5},10->{}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 1,0,A>, A) (< 1,0,B>, B) (< 2,0,A>, A) (< 2,0,B>, B) (< 3,0,A>, A) (< 3,0,B>, B) (< 4,0,A>, A) (< 4,0,B>, ?) (< 5,0,A>, A) (< 5,0,B>, ?) (< 6,0,A>, A) (< 6,0,B>, A) (< 7,0,A>, A) (< 7,0,B>, ?) (< 8,0,A>, A) (< 8,0,B>, A) (< 9,0,A>, A) (< 9,0,B>, ?) (<10,0,A>, A) (<10,0,B>, ?) + Applied Processor: LeafRules + Details: The following transitions are estimated by its predecessors and are removed [1,2,5,10] * Step 5: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalspeedpldi4start(A,B) -> evalspeedpldi4entryin(A,B) True (1,1) 3. evalspeedpldi4entryin(A,B) -> evalspeedpldi4bb5in(A,B) [A >= 1 && B >= 1 + A] (?,1) 4. evalspeedpldi4bb5in(A,B) -> evalspeedpldi4bb2in(A,B) [B >= 1] (?,1) 6. evalspeedpldi4bb2in(A,B) -> evalspeedpldi4bb3in(A,B) [A >= 1 + B] (?,1) 7. evalspeedpldi4bb2in(A,B) -> evalspeedpldi4bb4in(A,B) [B >= A] (?,1) 8. evalspeedpldi4bb3in(A,B) -> evalspeedpldi4bb5in(A,-1 + B) True (?,1) 9. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb5in(A,-1*A + B) True (?,1) Signature: {(evalspeedpldi4bb2in,2) ;(evalspeedpldi4bb3in,2) ;(evalspeedpldi4bb4in,2) ;(evalspeedpldi4bb5in,2) ;(evalspeedpldi4entryin,2) ;(evalspeedpldi4returnin,2) ;(evalspeedpldi4start,2) ;(evalspeedpldi4stop,2)} Flow Graph: [0->{3},3->{4},4->{6,7},6->{8},7->{9},8->{4},9->{4}] Sizebounds: (<0,0,A>, A) (<0,0,B>, B) (<3,0,A>, A) (<3,0,B>, B) (<4,0,A>, A) (<4,0,B>, ?) (<6,0,A>, A) (<6,0,B>, A) (<7,0,A>, A) (<7,0,B>, ?) (<8,0,A>, A) (<8,0,B>, A) (<9,0,A>, A) (<9,0,B>, ?) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(evalspeedpldi4bb2in) = 1 p(evalspeedpldi4bb3in) = 1 p(evalspeedpldi4bb4in) = 1 p(evalspeedpldi4bb5in) = 1 p(evalspeedpldi4entryin) = 2 p(evalspeedpldi4start) = 2 The following rules are strictly oriented: [A >= 1 && B >= 1 + A] ==> evalspeedpldi4entryin(A,B) = 2 > 1 = evalspeedpldi4bb5in(A,B) The following rules are weakly oriented: True ==> evalspeedpldi4start(A,B) = 2 >= 2 = evalspeedpldi4entryin(A,B) [B >= 1] ==> evalspeedpldi4bb5in(A,B) = 1 >= 1 = evalspeedpldi4bb2in(A,B) [A >= 1 + B] ==> evalspeedpldi4bb2in(A,B) = 1 >= 1 = evalspeedpldi4bb3in(A,B) [B >= A] ==> evalspeedpldi4bb2in(A,B) = 1 >= 1 = evalspeedpldi4bb4in(A,B) True ==> evalspeedpldi4bb3in(A,B) = 1 >= 1 = evalspeedpldi4bb5in(A,-1 + B) True ==> evalspeedpldi4bb4in(A,B) = 1 >= 1 = evalspeedpldi4bb5in(A,-1*A + B) * Step 6: ChainProcessor WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalspeedpldi4start(A,B) -> evalspeedpldi4entryin(A,B) True (1,1) 3. evalspeedpldi4entryin(A,B) -> evalspeedpldi4bb5in(A,B) [A >= 1 && B >= 1 + A] (2,1) 4. evalspeedpldi4bb5in(A,B) -> evalspeedpldi4bb2in(A,B) [B >= 1] (?,1) 6. evalspeedpldi4bb2in(A,B) -> evalspeedpldi4bb3in(A,B) [A >= 1 + B] (?,1) 7. evalspeedpldi4bb2in(A,B) -> evalspeedpldi4bb4in(A,B) [B >= A] (?,1) 8. evalspeedpldi4bb3in(A,B) -> evalspeedpldi4bb5in(A,-1 + B) True (?,1) 9. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb5in(A,-1*A + B) True (?,1) Signature: {(evalspeedpldi4bb2in,2) ;(evalspeedpldi4bb3in,2) ;(evalspeedpldi4bb4in,2) ;(evalspeedpldi4bb5in,2) ;(evalspeedpldi4entryin,2) ;(evalspeedpldi4returnin,2) ;(evalspeedpldi4start,2) ;(evalspeedpldi4stop,2)} Flow Graph: [0->{3},3->{4},4->{6,7},6->{8},7->{9},8->{4},9->{4}] Sizebounds: (<0,0,A>, A) (<0,0,B>, B) (<3,0,A>, A) (<3,0,B>, B) (<4,0,A>, A) (<4,0,B>, ?) (<6,0,A>, A) (<6,0,B>, A) (<7,0,A>, A) (<7,0,B>, ?) (<8,0,A>, A) (<8,0,B>, A) (<9,0,A>, A) (<9,0,B>, ?) + Applied Processor: ChainProcessor False [0,3,4,6,7,8,9] + Details: We chained rule 0 to obtain the rules [10] . * Step 7: UnreachableRules WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 3. evalspeedpldi4entryin(A,B) -> evalspeedpldi4bb5in(A,B) [A >= 1 && B >= 1 + A] (2,1) 4. evalspeedpldi4bb5in(A,B) -> evalspeedpldi4bb2in(A,B) [B >= 1] (?,1) 6. evalspeedpldi4bb2in(A,B) -> evalspeedpldi4bb3in(A,B) [A >= 1 + B] (?,1) 7. evalspeedpldi4bb2in(A,B) -> evalspeedpldi4bb4in(A,B) [B >= A] (?,1) 8. evalspeedpldi4bb3in(A,B) -> evalspeedpldi4bb5in(A,-1 + B) True (?,1) 9. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb5in(A,-1*A + B) True (?,1) 10. evalspeedpldi4start(A,B) -> evalspeedpldi4bb5in(A,B) [A >= 1 && B >= 1 + A] (1,2) Signature: {(evalspeedpldi4bb2in,2) ;(evalspeedpldi4bb3in,2) ;(evalspeedpldi4bb4in,2) ;(evalspeedpldi4bb5in,2) ;(evalspeedpldi4entryin,2) ;(evalspeedpldi4returnin,2) ;(evalspeedpldi4start,2) ;(evalspeedpldi4stop,2)} Flow Graph: [3->{4},4->{6,7},6->{8},7->{9},8->{4},9->{4},10->{4}] Sizebounds: (< 3,0,A>, A) (< 3,0,B>, B) (< 4,0,A>, A) (< 4,0,B>, ?) (< 6,0,A>, A) (< 6,0,B>, A) (< 7,0,A>, A) (< 7,0,B>, ?) (< 8,0,A>, A) (< 8,0,B>, A) (< 9,0,A>, A) (< 9,0,B>, ?) (<10,0,A>, A) (<10,0,B>, B) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [3] * Step 8: ChainProcessor WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 4. evalspeedpldi4bb5in(A,B) -> evalspeedpldi4bb2in(A,B) [B >= 1] (?,1) 6. evalspeedpldi4bb2in(A,B) -> evalspeedpldi4bb3in(A,B) [A >= 1 + B] (?,1) 7. evalspeedpldi4bb2in(A,B) -> evalspeedpldi4bb4in(A,B) [B >= A] (?,1) 8. evalspeedpldi4bb3in(A,B) -> evalspeedpldi4bb5in(A,-1 + B) True (?,1) 9. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb5in(A,-1*A + B) True (?,1) 10. evalspeedpldi4start(A,B) -> evalspeedpldi4bb5in(A,B) [A >= 1 && B >= 1 + A] (1,2) Signature: {(evalspeedpldi4bb2in,2) ;(evalspeedpldi4bb3in,2) ;(evalspeedpldi4bb4in,2) ;(evalspeedpldi4bb5in,2) ;(evalspeedpldi4entryin,2) ;(evalspeedpldi4returnin,2) ;(evalspeedpldi4start,2) ;(evalspeedpldi4stop,2)} Flow Graph: [4->{6,7},6->{8},7->{9},8->{4},9->{4},10->{4}] Sizebounds: (< 4,0,A>, A) (< 4,0,B>, ?) (< 6,0,A>, A) (< 6,0,B>, A) (< 7,0,A>, A) (< 7,0,B>, ?) (< 8,0,A>, A) (< 8,0,B>, A) (< 9,0,A>, A) (< 9,0,B>, ?) (<10,0,A>, A) (<10,0,B>, B) + Applied Processor: ChainProcessor False [4,6,7,8,9,10] + Details: We chained rule 4 to obtain the rules [11,12] . * Step 9: UnreachableRules WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 6. evalspeedpldi4bb2in(A,B) -> evalspeedpldi4bb3in(A,B) [A >= 1 + B] (?,1) 7. evalspeedpldi4bb2in(A,B) -> evalspeedpldi4bb4in(A,B) [B >= A] (?,1) 8. evalspeedpldi4bb3in(A,B) -> evalspeedpldi4bb5in(A,-1 + B) True (?,1) 9. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb5in(A,-1*A + B) True (?,1) 10. evalspeedpldi4start(A,B) -> evalspeedpldi4bb5in(A,B) [A >= 1 && B >= 1 + A] (1,2) 11. evalspeedpldi4bb5in(A,B) -> evalspeedpldi4bb3in(A,B) [B >= 1 && A >= 1 + B] (?,2) 12. evalspeedpldi4bb5in(A,B) -> evalspeedpldi4bb4in(A,B) [B >= 1 && B >= A] (?,2) Signature: {(evalspeedpldi4bb2in,2) ;(evalspeedpldi4bb3in,2) ;(evalspeedpldi4bb4in,2) ;(evalspeedpldi4bb5in,2) ;(evalspeedpldi4entryin,2) ;(evalspeedpldi4returnin,2) ;(evalspeedpldi4start,2) ;(evalspeedpldi4stop,2)} Flow Graph: [6->{8},7->{9},8->{11,12},9->{11,12},10->{11,12},11->{8},12->{9}] Sizebounds: (< 6,0,A>, A) (< 6,0,B>, A) (< 7,0,A>, A) (< 7,0,B>, ?) (< 8,0,A>, A) (< 8,0,B>, A) (< 9,0,A>, A) (< 9,0,B>, ?) (<10,0,A>, A) (<10,0,B>, B) (<11,0,A>, A) (<11,0,B>, A) (<12,0,A>, A) (<12,0,B>, ?) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [6,7] * Step 10: ChainProcessor WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 8. evalspeedpldi4bb3in(A,B) -> evalspeedpldi4bb5in(A,-1 + B) True (?,1) 9. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb5in(A,-1*A + B) True (?,1) 10. evalspeedpldi4start(A,B) -> evalspeedpldi4bb5in(A,B) [A >= 1 && B >= 1 + A] (1,2) 11. evalspeedpldi4bb5in(A,B) -> evalspeedpldi4bb3in(A,B) [B >= 1 && A >= 1 + B] (?,2) 12. evalspeedpldi4bb5in(A,B) -> evalspeedpldi4bb4in(A,B) [B >= 1 && B >= A] (?,2) Signature: {(evalspeedpldi4bb2in,2) ;(evalspeedpldi4bb3in,2) ;(evalspeedpldi4bb4in,2) ;(evalspeedpldi4bb5in,2) ;(evalspeedpldi4entryin,2) ;(evalspeedpldi4returnin,2) ;(evalspeedpldi4start,2) ;(evalspeedpldi4stop,2)} Flow Graph: [8->{11,12},9->{11,12},10->{11,12},11->{8},12->{9}] Sizebounds: (< 8,0,A>, A) (< 8,0,B>, A) (< 9,0,A>, A) (< 9,0,B>, ?) (<10,0,A>, A) (<10,0,B>, B) (<11,0,A>, A) (<11,0,B>, A) (<12,0,A>, A) (<12,0,B>, ?) + Applied Processor: ChainProcessor False [8,9,10,11,12] + Details: We chained rule 8 to obtain the rules [13,14] . * Step 11: ChainProcessor WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 9. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb5in(A,-1*A + B) True (?,1) 10. evalspeedpldi4start(A,B) -> evalspeedpldi4bb5in(A,B) [A >= 1 && B >= 1 + A] (1,2) 11. evalspeedpldi4bb5in(A,B) -> evalspeedpldi4bb3in(A,B) [B >= 1 && A >= 1 + B] (?,2) 12. evalspeedpldi4bb5in(A,B) -> evalspeedpldi4bb4in(A,B) [B >= 1 && B >= A] (?,2) 13. evalspeedpldi4bb3in(A,B) -> evalspeedpldi4bb3in(A,-1 + B) [-1 + B >= 1 && A >= B] (?,3) 14. evalspeedpldi4bb3in(A,B) -> evalspeedpldi4bb4in(A,-1 + B) [-1 + B >= 1 && -1 + B >= A] (?,3) Signature: {(evalspeedpldi4bb2in,2) ;(evalspeedpldi4bb3in,2) ;(evalspeedpldi4bb4in,2) ;(evalspeedpldi4bb5in,2) ;(evalspeedpldi4entryin,2) ;(evalspeedpldi4returnin,2) ;(evalspeedpldi4start,2) ;(evalspeedpldi4stop,2)} Flow Graph: [9->{11,12},10->{11,12},11->{13,14},12->{9},13->{13,14},14->{9}] Sizebounds: (< 9,0,A>, A) (< 9,0,B>, ?) (<10,0,A>, A) (<10,0,B>, B) (<11,0,A>, A) (<11,0,B>, A) (<12,0,A>, A) (<12,0,B>, ?) (<13,0,A>, A) (<13,0,B>, A) (<14,0,A>, A) (<14,0,B>, ?) + Applied Processor: ChainProcessor False [9,10,11,12,13,14] + Details: We chained rule 9 to obtain the rules [15,16] . * Step 12: ChainProcessor WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 10. evalspeedpldi4start(A,B) -> evalspeedpldi4bb5in(A,B) [A >= 1 && B >= 1 + A] (1,2) 11. evalspeedpldi4bb5in(A,B) -> evalspeedpldi4bb3in(A,B) [B >= 1 && A >= 1 + B] (?,2) 12. evalspeedpldi4bb5in(A,B) -> evalspeedpldi4bb4in(A,B) [B >= 1 && B >= A] (?,2) 13. evalspeedpldi4bb3in(A,B) -> evalspeedpldi4bb3in(A,-1 + B) [-1 + B >= 1 && A >= B] (?,3) 14. evalspeedpldi4bb3in(A,B) -> evalspeedpldi4bb4in(A,-1 + B) [-1 + B >= 1 && -1 + B >= A] (?,3) 15. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb3in(A,-1*A + B) [-1*A + B >= 1 && A >= 1 + -1*A + B] (?,3) 16. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb4in(A,-1*A + B) [-1*A + B >= 1 && -1*A + B >= A] (?,3) Signature: {(evalspeedpldi4bb2in,2) ;(evalspeedpldi4bb3in,2) ;(evalspeedpldi4bb4in,2) ;(evalspeedpldi4bb5in,2) ;(evalspeedpldi4entryin,2) ;(evalspeedpldi4returnin,2) ;(evalspeedpldi4start,2) ;(evalspeedpldi4stop,2)} Flow Graph: [10->{11,12},11->{13,14},12->{15,16},13->{13,14},14->{15,16},15->{13,14},16->{15,16}] Sizebounds: (<10,0,A>, A) (<10,0,B>, B) (<11,0,A>, A) (<11,0,B>, A) (<12,0,A>, A) (<12,0,B>, ?) (<13,0,A>, A) (<13,0,B>, A) (<14,0,A>, A) (<14,0,B>, ?) (<15,0,A>, A) (<15,0,B>, A) (<16,0,A>, A) (<16,0,B>, ?) + Applied Processor: ChainProcessor False [10,11,12,13,14,15,16] + Details: We chained rule 10 to obtain the rules [17,18] . * Step 13: UnreachableRules WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 11. evalspeedpldi4bb5in(A,B) -> evalspeedpldi4bb3in(A,B) [B >= 1 && A >= 1 + B] (?,2) 12. evalspeedpldi4bb5in(A,B) -> evalspeedpldi4bb4in(A,B) [B >= 1 && B >= A] (?,2) 13. evalspeedpldi4bb3in(A,B) -> evalspeedpldi4bb3in(A,-1 + B) [-1 + B >= 1 && A >= B] (?,3) 14. evalspeedpldi4bb3in(A,B) -> evalspeedpldi4bb4in(A,-1 + B) [-1 + B >= 1 && -1 + B >= A] (?,3) 15. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb3in(A,-1*A + B) [-1*A + B >= 1 && A >= 1 + -1*A + B] (?,3) 16. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb4in(A,-1*A + B) [-1*A + B >= 1 && -1*A + B >= A] (?,3) 17. evalspeedpldi4start(A,B) -> evalspeedpldi4bb3in(A,B) [A >= 1 && B >= 1 + A && B >= 1 && A >= 1 + B] (1,4) 18. evalspeedpldi4start(A,B) -> evalspeedpldi4bb4in(A,B) [A >= 1 && B >= 1 + A && B >= 1 && B >= A] (1,4) Signature: {(evalspeedpldi4bb2in,2) ;(evalspeedpldi4bb3in,2) ;(evalspeedpldi4bb4in,2) ;(evalspeedpldi4bb5in,2) ;(evalspeedpldi4entryin,2) ;(evalspeedpldi4returnin,2) ;(evalspeedpldi4start,2) ;(evalspeedpldi4stop,2)} Flow Graph: [11->{13,14},12->{15,16},13->{13,14},14->{15,16},15->{13,14},16->{15,16},17->{13,14},18->{15,16}] Sizebounds: (<11,0,A>, A) (<11,0,B>, A) (<12,0,A>, A) (<12,0,B>, ?) (<13,0,A>, A) (<13,0,B>, A) (<14,0,A>, A) (<14,0,B>, ?) (<15,0,A>, A) (<15,0,B>, A) (<16,0,A>, A) (<16,0,B>, ?) (<17,0,A>, A) (<17,0,B>, A) (<18,0,A>, A) (<18,0,B>, ?) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [11,12] * Step 14: UnsatPaths WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 13. evalspeedpldi4bb3in(A,B) -> evalspeedpldi4bb3in(A,-1 + B) [-1 + B >= 1 && A >= B] (?,3) 14. evalspeedpldi4bb3in(A,B) -> evalspeedpldi4bb4in(A,-1 + B) [-1 + B >= 1 && -1 + B >= A] (?,3) 15. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb3in(A,-1*A + B) [-1*A + B >= 1 && A >= 1 + -1*A + B] (?,3) 16. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb4in(A,-1*A + B) [-1*A + B >= 1 && -1*A + B >= A] (?,3) 17. evalspeedpldi4start(A,B) -> evalspeedpldi4bb3in(A,B) [A >= 1 && B >= 1 + A && B >= 1 && A >= 1 + B] (1,4) 18. evalspeedpldi4start(A,B) -> evalspeedpldi4bb4in(A,B) [A >= 1 && B >= 1 + A && B >= 1 && B >= A] (1,4) Signature: {(evalspeedpldi4bb2in,2) ;(evalspeedpldi4bb3in,2) ;(evalspeedpldi4bb4in,2) ;(evalspeedpldi4bb5in,2) ;(evalspeedpldi4entryin,2) ;(evalspeedpldi4returnin,2) ;(evalspeedpldi4start,2) ;(evalspeedpldi4stop,2)} Flow Graph: [13->{13,14},14->{15,16},15->{13,14},16->{15,16},17->{13,14},18->{15,16}] Sizebounds: (<13,0,A>, A) (<13,0,B>, A) (<14,0,A>, A) (<14,0,B>, ?) (<15,0,A>, A) (<15,0,B>, A) (<16,0,A>, A) (<16,0,B>, ?) (<17,0,A>, A) (<17,0,B>, A) (<18,0,A>, A) (<18,0,B>, ?) + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(13,14),(15,14),(17,13),(17,14)] * Step 15: UnreachableRules WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 13. evalspeedpldi4bb3in(A,B) -> evalspeedpldi4bb3in(A,-1 + B) [-1 + B >= 1 && A >= B] (?,3) 14. evalspeedpldi4bb3in(A,B) -> evalspeedpldi4bb4in(A,-1 + B) [-1 + B >= 1 && -1 + B >= A] (?,3) 15. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb3in(A,-1*A + B) [-1*A + B >= 1 && A >= 1 + -1*A + B] (?,3) 16. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb4in(A,-1*A + B) [-1*A + B >= 1 && -1*A + B >= A] (?,3) 17. evalspeedpldi4start(A,B) -> evalspeedpldi4bb3in(A,B) [A >= 1 && B >= 1 + A && B >= 1 && A >= 1 + B] (1,4) 18. evalspeedpldi4start(A,B) -> evalspeedpldi4bb4in(A,B) [A >= 1 && B >= 1 + A && B >= 1 && B >= A] (1,4) Signature: {(evalspeedpldi4bb2in,2) ;(evalspeedpldi4bb3in,2) ;(evalspeedpldi4bb4in,2) ;(evalspeedpldi4bb5in,2) ;(evalspeedpldi4entryin,2) ;(evalspeedpldi4returnin,2) ;(evalspeedpldi4start,2) ;(evalspeedpldi4stop,2)} Flow Graph: [13->{13},14->{15,16},15->{13},16->{15,16},17->{},18->{15,16}] Sizebounds: (<13,0,A>, A) (<13,0,B>, A) (<14,0,A>, A) (<14,0,B>, ?) (<15,0,A>, A) (<15,0,B>, A) (<16,0,A>, A) (<16,0,B>, ?) (<17,0,A>, A) (<17,0,B>, A) (<18,0,A>, A) (<18,0,B>, ?) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [14] * Step 16: LocalSizeboundsProc WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 13. evalspeedpldi4bb3in(A,B) -> evalspeedpldi4bb3in(A,-1 + B) [-1 + B >= 1 && A >= B] (?,3) 15. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb3in(A,-1*A + B) [-1*A + B >= 1 && A >= 1 + -1*A + B] (?,3) 16. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb4in(A,-1*A + B) [-1*A + B >= 1 && -1*A + B >= A] (?,3) 17. evalspeedpldi4start(A,B) -> evalspeedpldi4bb3in(A,B) [A >= 1 && B >= 1 + A && B >= 1 && A >= 1 + B] (1,4) 18. evalspeedpldi4start(A,B) -> evalspeedpldi4bb4in(A,B) [A >= 1 && B >= 1 + A && B >= 1 && B >= A] (1,4) Signature: {(evalspeedpldi4bb2in,2) ;(evalspeedpldi4bb3in,2) ;(evalspeedpldi4bb4in,2) ;(evalspeedpldi4bb5in,2) ;(evalspeedpldi4entryin,2) ;(evalspeedpldi4returnin,2) ;(evalspeedpldi4start,2) ;(evalspeedpldi4stop,2)} Flow Graph: [13->{13},15->{13},16->{15,16},17->{},18->{15,16}] Sizebounds: (<13,0,A>, A) (<13,0,B>, A) (<15,0,A>, A) (<15,0,B>, A) (<16,0,A>, A) (<16,0,B>, ?) (<17,0,A>, A) (<17,0,B>, A) (<18,0,A>, A) (<18,0,B>, ?) + Applied Processor: LocalSizeboundsProc + Details: LocalSizebounds generated; rvgraph (<13,0,A>, A, .= 0) (<13,0,B>, 1 + B, .+ 1) (<15,0,A>, A, .= 0) (<15,0,B>, A + B, .* 0) (<16,0,A>, A, .= 0) (<16,0,B>, A + B, .* 0) (<17,0,A>, A, .= 0) (<17,0,B>, B, .= 0) (<18,0,A>, A, .= 0) (<18,0,B>, B, .= 0) * Step 17: SizeboundsProc WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 13. evalspeedpldi4bb3in(A,B) -> evalspeedpldi4bb3in(A,-1 + B) [-1 + B >= 1 && A >= B] (?,3) 15. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb3in(A,-1*A + B) [-1*A + B >= 1 && A >= 1 + -1*A + B] (?,3) 16. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb4in(A,-1*A + B) [-1*A + B >= 1 && -1*A + B >= A] (?,3) 17. evalspeedpldi4start(A,B) -> evalspeedpldi4bb3in(A,B) [A >= 1 && B >= 1 + A && B >= 1 && A >= 1 + B] (1,4) 18. evalspeedpldi4start(A,B) -> evalspeedpldi4bb4in(A,B) [A >= 1 && B >= 1 + A && B >= 1 && B >= A] (1,4) Signature: {(evalspeedpldi4bb2in,2) ;(evalspeedpldi4bb3in,2) ;(evalspeedpldi4bb4in,2) ;(evalspeedpldi4bb5in,2) ;(evalspeedpldi4entryin,2) ;(evalspeedpldi4returnin,2) ;(evalspeedpldi4start,2) ;(evalspeedpldi4stop,2)} Flow Graph: [13->{13},15->{13},16->{15,16},17->{},18->{15,16}] Sizebounds: (<13,0,A>, ?) (<13,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: SizeboundsProc + Details: Sizebounds computed: (<13,0,A>, A) (<13,0,B>, A) (<15,0,A>, A) (<15,0,B>, ?) (<16,0,A>, A) (<16,0,B>, ?) (<17,0,A>, A) (<17,0,B>, B) (<18,0,A>, A) (<18,0,B>, B) * Step 18: LocationConstraintsProc WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 13. evalspeedpldi4bb3in(A,B) -> evalspeedpldi4bb3in(A,-1 + B) [-1 + B >= 1 && A >= B] (?,3) 15. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb3in(A,-1*A + B) [-1*A + B >= 1 && A >= 1 + -1*A + B] (?,3) 16. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb4in(A,-1*A + B) [-1*A + B >= 1 && -1*A + B >= A] (?,3) 17. evalspeedpldi4start(A,B) -> evalspeedpldi4bb3in(A,B) [A >= 1 && B >= 1 + A && B >= 1 && A >= 1 + B] (1,4) 18. evalspeedpldi4start(A,B) -> evalspeedpldi4bb4in(A,B) [A >= 1 && B >= 1 + A && B >= 1 && B >= A] (1,4) Signature: {(evalspeedpldi4bb2in,2) ;(evalspeedpldi4bb3in,2) ;(evalspeedpldi4bb4in,2) ;(evalspeedpldi4bb5in,2) ;(evalspeedpldi4entryin,2) ;(evalspeedpldi4returnin,2) ;(evalspeedpldi4start,2) ;(evalspeedpldi4stop,2)} Flow Graph: [13->{13},15->{13},16->{15,16},17->{},18->{15,16}] Sizebounds: (<13,0,A>, A) (<13,0,B>, A) (<15,0,A>, A) (<15,0,B>, ?) (<16,0,A>, A) (<16,0,B>, ?) (<17,0,A>, A) (<17,0,B>, B) (<18,0,A>, A) (<18,0,B>, B) + Applied Processor: LocationConstraintsProc + Details: We computed the location constraints 13 : [A >= 1 + B && False] 15 : [A >= 1] 16 : [B >= A && A >= 1] 17 : True 18 : True . * Step 19: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 13. evalspeedpldi4bb3in(A,B) -> evalspeedpldi4bb3in(A,-1 + B) [-1 + B >= 1 && A >= B] (?,3) 15. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb3in(A,-1*A + B) [-1*A + B >= 1 && A >= 1 + -1*A + B] (?,3) 16. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb4in(A,-1*A + B) [-1*A + B >= 1 && -1*A + B >= A] (?,3) 17. evalspeedpldi4start(A,B) -> evalspeedpldi4bb3in(A,B) [A >= 1 && B >= 1 + A && B >= 1 && A >= 1 + B] (1,4) 18. evalspeedpldi4start(A,B) -> evalspeedpldi4bb4in(A,B) [A >= 1 && B >= 1 + A && B >= 1 && B >= A] (1,4) Signature: {(evalspeedpldi4bb2in,2) ;(evalspeedpldi4bb3in,2) ;(evalspeedpldi4bb4in,2) ;(evalspeedpldi4bb5in,2) ;(evalspeedpldi4entryin,2) ;(evalspeedpldi4returnin,2) ;(evalspeedpldi4start,2) ;(evalspeedpldi4stop,2)} Flow Graph: [13->{13},15->{13},16->{15,16},17->{},18->{15,16}] Sizebounds: (<13,0,A>, A) (<13,0,B>, A) (<15,0,A>, A) (<15,0,B>, ?) (<16,0,A>, A) (<16,0,B>, ?) (<17,0,A>, A) (<17,0,B>, B) (<18,0,A>, A) (<18,0,B>, B) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Constant} + Details: We apply a polynomial interpretation of shape constant: p(evalspeedpldi4bb3in) = 0 p(evalspeedpldi4bb4in) = 1 p(evalspeedpldi4start) = 1 The following rules are strictly oriented: [-1*A + B >= 1 && A >= 1 + -1*A + B] ==> evalspeedpldi4bb4in(A,B) = 1 > 0 = evalspeedpldi4bb3in(A,-1*A + B) The following rules are weakly oriented: [-1 + B >= 1 && A >= B] ==> evalspeedpldi4bb3in(A,B) = 0 >= 0 = evalspeedpldi4bb3in(A,-1 + B) [-1*A + B >= 1 && -1*A + B >= A] ==> evalspeedpldi4bb4in(A,B) = 1 >= 1 = evalspeedpldi4bb4in(A,-1*A + B) [A >= 1 && B >= 1 + A && B >= 1 && A >= 1 + B] ==> evalspeedpldi4start(A,B) = 1 >= 0 = evalspeedpldi4bb3in(A,B) [A >= 1 && B >= 1 + A && B >= 1 && B >= A] ==> evalspeedpldi4start(A,B) = 1 >= 1 = evalspeedpldi4bb4in(A,B) * Step 20: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 13. evalspeedpldi4bb3in(A,B) -> evalspeedpldi4bb3in(A,-1 + B) [-1 + B >= 1 && A >= B] (?,3) 15. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb3in(A,-1*A + B) [-1*A + B >= 1 && A >= 1 + -1*A + B] (1,3) 16. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb4in(A,-1*A + B) [-1*A + B >= 1 && -1*A + B >= A] (?,3) 17. evalspeedpldi4start(A,B) -> evalspeedpldi4bb3in(A,B) [A >= 1 && B >= 1 + A && B >= 1 && A >= 1 + B] (1,4) 18. evalspeedpldi4start(A,B) -> evalspeedpldi4bb4in(A,B) [A >= 1 && B >= 1 + A && B >= 1 && B >= A] (1,4) Signature: {(evalspeedpldi4bb2in,2) ;(evalspeedpldi4bb3in,2) ;(evalspeedpldi4bb4in,2) ;(evalspeedpldi4bb5in,2) ;(evalspeedpldi4entryin,2) ;(evalspeedpldi4returnin,2) ;(evalspeedpldi4start,2) ;(evalspeedpldi4stop,2)} Flow Graph: [13->{13},15->{13},16->{15,16},17->{},18->{15,16}] Sizebounds: (<13,0,A>, A) (<13,0,B>, A) (<15,0,A>, A) (<15,0,B>, ?) (<16,0,A>, A) (<16,0,B>, ?) (<17,0,A>, A) (<17,0,B>, B) (<18,0,A>, A) (<18,0,B>, B) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(evalspeedpldi4bb3in) = 0 p(evalspeedpldi4bb4in) = -1*x1 + x2 p(evalspeedpldi4start) = x2 The following rules are strictly oriented: [-1*A + B >= 1 && A >= 1 + -1*A + B] ==> evalspeedpldi4bb4in(A,B) = -1*A + B > 0 = evalspeedpldi4bb3in(A,-1*A + B) [-1*A + B >= 1 && -1*A + B >= A] ==> evalspeedpldi4bb4in(A,B) = -1*A + B > -2*A + B = evalspeedpldi4bb4in(A,-1*A + B) [A >= 1 && B >= 1 + A && B >= 1 && A >= 1 + B] ==> evalspeedpldi4start(A,B) = B > 0 = evalspeedpldi4bb3in(A,B) [A >= 1 && B >= 1 + A && B >= 1 && B >= A] ==> evalspeedpldi4start(A,B) = B > -1*A + B = evalspeedpldi4bb4in(A,B) The following rules are weakly oriented: [-1 + B >= 1 && A >= B] ==> evalspeedpldi4bb3in(A,B) = 0 >= 0 = evalspeedpldi4bb3in(A,-1 + B) * Step 21: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 13. evalspeedpldi4bb3in(A,B) -> evalspeedpldi4bb3in(A,-1 + B) [-1 + B >= 1 && A >= B] (?,3) 15. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb3in(A,-1*A + B) [-1*A + B >= 1 && A >= 1 + -1*A + B] (1,3) 16. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb4in(A,-1*A + B) [-1*A + B >= 1 && -1*A + B >= A] (B,3) 17. evalspeedpldi4start(A,B) -> evalspeedpldi4bb3in(A,B) [A >= 1 && B >= 1 + A && B >= 1 && A >= 1 + B] (1,4) 18. evalspeedpldi4start(A,B) -> evalspeedpldi4bb4in(A,B) [A >= 1 && B >= 1 + A && B >= 1 && B >= A] (1,4) Signature: {(evalspeedpldi4bb2in,2) ;(evalspeedpldi4bb3in,2) ;(evalspeedpldi4bb4in,2) ;(evalspeedpldi4bb5in,2) ;(evalspeedpldi4entryin,2) ;(evalspeedpldi4returnin,2) ;(evalspeedpldi4start,2) ;(evalspeedpldi4stop,2)} Flow Graph: [13->{13},15->{13},16->{15,16},17->{},18->{15,16}] Sizebounds: (<13,0,A>, A) (<13,0,B>, A) (<15,0,A>, A) (<15,0,B>, ?) (<16,0,A>, A) (<16,0,B>, ?) (<17,0,A>, A) (<17,0,B>, B) (<18,0,A>, A) (<18,0,B>, B) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(evalspeedpldi4bb3in) = -1 + x2 p(evalspeedpldi4bb4in) = -1*x1 + x2 p(evalspeedpldi4start) = x2 The following rules are strictly oriented: [-1 + B >= 1 && A >= B] ==> evalspeedpldi4bb3in(A,B) = -1 + B > -2 + B = evalspeedpldi4bb3in(A,-1 + B) [-1*A + B >= 1 && A >= 1 + -1*A + B] ==> evalspeedpldi4bb4in(A,B) = -1*A + B > -1 + -1*A + B = evalspeedpldi4bb3in(A,-1*A + B) [-1*A + B >= 1 && -1*A + B >= A] ==> evalspeedpldi4bb4in(A,B) = -1*A + B > -2*A + B = evalspeedpldi4bb4in(A,-1*A + B) [A >= 1 && B >= 1 + A && B >= 1 && A >= 1 + B] ==> evalspeedpldi4start(A,B) = B > -1 + B = evalspeedpldi4bb3in(A,B) [A >= 1 && B >= 1 + A && B >= 1 && B >= A] ==> evalspeedpldi4start(A,B) = B > -1*A + B = evalspeedpldi4bb4in(A,B) The following rules are weakly oriented: * Step 22: LoopRecurrenceProcessor WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 13. evalspeedpldi4bb3in(A,B) -> evalspeedpldi4bb3in(A,-1 + B) [-1 + B >= 1 && A >= B] (B,3) 15. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb3in(A,-1*A + B) [-1*A + B >= 1 && A >= 1 + -1*A + B] (1,3) 16. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb4in(A,-1*A + B) [-1*A + B >= 1 && -1*A + B >= A] (B,3) 17. evalspeedpldi4start(A,B) -> evalspeedpldi4bb3in(A,B) [A >= 1 && B >= 1 + A && B >= 1 && A >= 1 + B] (1,4) 18. evalspeedpldi4start(A,B) -> evalspeedpldi4bb4in(A,B) [A >= 1 && B >= 1 + A && B >= 1 && B >= A] (1,4) Signature: {(evalspeedpldi4bb2in,2) ;(evalspeedpldi4bb3in,2) ;(evalspeedpldi4bb4in,2) ;(evalspeedpldi4bb5in,2) ;(evalspeedpldi4entryin,2) ;(evalspeedpldi4returnin,2) ;(evalspeedpldi4start,2) ;(evalspeedpldi4stop,2)} Flow Graph: [13->{13},15->{13},16->{15,16},17->{},18->{15,16}] Sizebounds: (<13,0,A>, A) (<13,0,B>, A) (<15,0,A>, A) (<15,0,B>, ?) (<16,0,A>, A) (<16,0,B>, ?) (<17,0,A>, A) (<17,0,B>, B) (<18,0,A>, A) (<18,0,B>, B) + Applied Processor: LoopRecurrenceProcessor [13] + Details: Applying the recurrence pattern linear * f to the expression B yields the solution B . * Step 23: UnsatPaths WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 13. evalspeedpldi4bb3in(A,B) -> evalspeedpldi4bb3in(A,-1 + B) [-1 + B >= 1 && A >= B] (B,3) 15. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb3in(A,-1*A + B) [-1*A + B >= 1 && A >= 1 + -1*A + B] (1,3) 16. evalspeedpldi4bb4in(A,B) -> evalspeedpldi4bb4in(A,-1*A + B) [-1*A + B >= 1 && -1*A + B >= A] (B,3) 17. evalspeedpldi4start(A,B) -> evalspeedpldi4bb3in(A,B) [A >= 1 && B >= 1 + A && B >= 1 && A >= 1 + B] (1,4) 18. evalspeedpldi4start(A,B) -> evalspeedpldi4bb4in(A,B) [A >= 1 && B >= 1 + A && B >= 1 && B >= A] (1,4) Signature: {(evalspeedpldi4bb2in,2) ;(evalspeedpldi4bb3in,2) ;(evalspeedpldi4bb4in,2) ;(evalspeedpldi4bb5in,2) ;(evalspeedpldi4entryin,2) ;(evalspeedpldi4returnin,2) ;(evalspeedpldi4start,2) ;(evalspeedpldi4stop,2)} Flow Graph: [13->{13},15->{13},16->{15,16},17->{},18->{15,16}] Sizebounds: (<13,0,A>, A) (<13,0,B>, A) (<15,0,A>, A) (<15,0,B>, ?) (<16,0,A>, A) (<16,0,B>, ?) (<17,0,A>, A) (<17,0,B>, B) (<18,0,A>, A) (<18,0,B>, B) + Applied Processor: UnsatPaths + Details: The problem is already solved. WORST_CASE(?,O(n^1))