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