YES(?,POLY) * Step 1: UnsatRules WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f0(A,B) -> f2(A,B) [A >= 1 && B >= 1] (1,1) 1. f0(A,B) -> f2(A,B) [A >= 1 && 0 >= 1 + B] (1,1) 2. f0(A,B) -> f2(A,B) [0 >= 1 + A && B >= 1] (1,1) 3. f0(A,B) -> f2(A,B) [0 >= 1 + A && 0 >= 1 + B] (1,1) 4. f2(A,B) -> f2(A,-1 + B) [A >= B && B >= 2 && A >= 1 && A + B >= 2] (?,1) 5. f2(A,B) -> f2(A,-1 + B) [A >= B && B >= 2 && 0 >= 1 + A && A + B >= 2] (?,1) 6. f2(A,B) -> f2(A,-1 + B) [A >= B && 0 >= B && A >= 1 && A + B >= 2] (?,1) 7. f2(A,B) -> f2(A,-1 + B) [A >= B && 0 >= B && 0 >= 1 + A && A + B >= 2] (?,1) 8. f2(A,B) -> f2(-1 + A,B) [1 >= A + B && A >= 1 + B && A >= 2 && B >= 1] (?,1) 9. f2(A,B) -> f2(-1 + A,B) [1 >= A + B && A >= 1 + B && A >= 2 && 0 >= 1 + B] (?,1) 10. f2(A,B) -> f2(-1 + A,B) [1 >= A + B && A >= 1 + B && 0 >= A && B >= 1] (?,1) 11. f2(A,B) -> f2(-1 + A,B) [1 >= A + B && A >= 1 + B && 0 >= A && 0 >= 1 + B] (?,1) 12. f2(A,B) -> f2(A,1 + B) [B >= A && B >= 0 && A >= 1 && 0 >= 1 + A + B] (?,1) 13. f2(A,B) -> f2(A,1 + B) [B >= A && B >= 0 && 0 >= 1 + A && 0 >= 1 + A + B] (?,1) 14. f2(A,B) -> f2(A,1 + B) [B >= A && 0 >= 2 + B && A >= 1 && 0 >= 1 + A + B] (?,1) 15. f2(A,B) -> f2(A,1 + B) [B >= A && 0 >= 2 + B && 0 >= 1 + A && 0 >= 1 + A + B] (?,1) 16. f2(A,B) -> f2(1 + A,B) [A + B >= 0 && B >= 1 + A && A >= 0 && B >= 1] (?,1) 17. f2(A,B) -> f2(1 + A,B) [A + B >= 0 && B >= 1 + A && A >= 0 && 0 >= 1 + B] (?,1) 18. f2(A,B) -> f2(1 + A,B) [A + B >= 0 && B >= 1 + A && 0 >= 2 + A && B >= 1] (?,1) 19. f2(A,B) -> f2(1 + A,B) [A + B >= 0 && B >= 1 + A && 0 >= 2 + A && 0 >= 1 + B] (?,1) Signature: {(f0,2);(f2,2)} Flow Graph: [0->{4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19},1->{4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19},2->{4,5,6,7 ,8,9,10,11,12,13,14,15,16,17,18,19},3->{4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19},4->{4,5,6,7,8,9,10,11,12 ,13,14,15,16,17,18,19},5->{4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19},6->{4,5,6,7,8,9,10,11,12,13,14,15,16 ,17,18,19},7->{4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19},8->{4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19} ,9->{4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19},10->{4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19},11->{4,5,6,7 ,8,9,10,11,12,13,14,15,16,17,18,19},12->{4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19},13->{4,5,6,7,8,9,10,11 ,12,13,14,15,16,17,18,19},14->{4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19},15->{4,5,6,7,8,9,10,11,12,13,14,15 ,16,17,18,19},16->{4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19},17->{4,5,6,7,8,9,10,11,12,13,14,15,16,17,18 ,19},18->{4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19},19->{4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19}] + Applied Processor: UnsatRules + Details: Following transitions have unsatisfiable constraints and are removed: [5,7,8,10,12,14,17,19] * Step 2: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f0(A,B) -> f2(A,B) [A >= 1 && B >= 1] (1,1) 1. f0(A,B) -> f2(A,B) [A >= 1 && 0 >= 1 + B] (1,1) 2. f0(A,B) -> f2(A,B) [0 >= 1 + A && B >= 1] (1,1) 3. f0(A,B) -> f2(A,B) [0 >= 1 + A && 0 >= 1 + B] (1,1) 4. f2(A,B) -> f2(A,-1 + B) [A >= B && B >= 2 && A >= 1 && A + B >= 2] (?,1) 6. f2(A,B) -> f2(A,-1 + B) [A >= B && 0 >= B && A >= 1 && A + B >= 2] (?,1) 9. f2(A,B) -> f2(-1 + A,B) [1 >= A + B && A >= 1 + B && A >= 2 && 0 >= 1 + B] (?,1) 11. f2(A,B) -> f2(-1 + A,B) [1 >= A + B && A >= 1 + B && 0 >= A && 0 >= 1 + B] (?,1) 13. f2(A,B) -> f2(A,1 + B) [B >= A && B >= 0 && 0 >= 1 + A && 0 >= 1 + A + B] (?,1) 15. f2(A,B) -> f2(A,1 + B) [B >= A && 0 >= 2 + B && 0 >= 1 + A && 0 >= 1 + A + B] (?,1) 16. f2(A,B) -> f2(1 + A,B) [A + B >= 0 && B >= 1 + A && A >= 0 && B >= 1] (?,1) 18. f2(A,B) -> f2(1 + A,B) [A + B >= 0 && B >= 1 + A && 0 >= 2 + A && B >= 1] (?,1) Signature: {(f0,2);(f2,2)} Flow Graph: [0->{4,6,9,11,13,15,16,18},1->{4,6,9,11,13,15,16,18},2->{4,6,9,11,13,15,16,18},3->{4,6,9,11,13,15,16,18} ,4->{4,6,9,11,13,15,16,18},6->{4,6,9,11,13,15,16,18},9->{4,6,9,11,13,15,16,18},11->{4,6,9,11,13,15,16,18} ,13->{4,6,9,11,13,15,16,18},15->{4,6,9,11,13,15,16,18},16->{4,6,9,11,13,15,16,18},18->{4,6,9,11,13,15,16 ,18}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,6) ,(0,9) ,(0,11) ,(0,13) ,(0,15) ,(0,18) ,(1,4) ,(1,11) ,(1,13) ,(1,15) ,(1,16) ,(1,18) ,(2,4) ,(2,6) ,(2,9) ,(2,11) ,(2,15) ,(2,16) ,(3,4) ,(3,6) ,(3,9) ,(3,13) ,(3,16) ,(3,18) ,(4,6) ,(4,9) ,(4,11) ,(4,13) ,(4,15) ,(4,16) ,(4,18) ,(6,4) ,(6,11) ,(6,13) ,(6,15) ,(6,16) ,(6,18) ,(9,4) ,(9,6) ,(9,11) ,(9,13) ,(9,15) ,(9,16) ,(9,18) ,(11,4) ,(11,6) ,(11,9) ,(11,13) ,(11,16) ,(11,18) ,(13,4) ,(13,6) ,(13,9) ,(13,11) ,(13,15) ,(13,16) ,(15,4) ,(15,6) ,(15,9) ,(15,11) ,(15,13) ,(15,16) ,(15,18) ,(16,6) ,(16,9) ,(16,11) ,(16,13) ,(16,15) ,(16,18) ,(18,4) ,(18,6) ,(18,9) ,(18,11) ,(18,13) ,(18,15) ,(18,16)] * Step 3: FromIts WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f0(A,B) -> f2(A,B) [A >= 1 && B >= 1] (1,1) 1. f0(A,B) -> f2(A,B) [A >= 1 && 0 >= 1 + B] (1,1) 2. f0(A,B) -> f2(A,B) [0 >= 1 + A && B >= 1] (1,1) 3. f0(A,B) -> f2(A,B) [0 >= 1 + A && 0 >= 1 + B] (1,1) 4. f2(A,B) -> f2(A,-1 + B) [A >= B && B >= 2 && A >= 1 && A + B >= 2] (?,1) 6. f2(A,B) -> f2(A,-1 + B) [A >= B && 0 >= B && A >= 1 && A + B >= 2] (?,1) 9. f2(A,B) -> f2(-1 + A,B) [1 >= A + B && A >= 1 + B && A >= 2 && 0 >= 1 + B] (?,1) 11. f2(A,B) -> f2(-1 + A,B) [1 >= A + B && A >= 1 + B && 0 >= A && 0 >= 1 + B] (?,1) 13. f2(A,B) -> f2(A,1 + B) [B >= A && B >= 0 && 0 >= 1 + A && 0 >= 1 + A + B] (?,1) 15. f2(A,B) -> f2(A,1 + B) [B >= A && 0 >= 2 + B && 0 >= 1 + A && 0 >= 1 + A + B] (?,1) 16. f2(A,B) -> f2(1 + A,B) [A + B >= 0 && B >= 1 + A && A >= 0 && B >= 1] (?,1) 18. f2(A,B) -> f2(1 + A,B) [A + B >= 0 && B >= 1 + A && 0 >= 2 + A && B >= 1] (?,1) Signature: {(f0,2);(f2,2)} Flow Graph: [0->{4,16},1->{6,9},2->{13,18},3->{11,15},4->{4},6->{6,9},9->{9},11->{11,15},13->{13,18},15->{15},16->{4 ,16},18->{18}] + Applied Processor: FromIts + Details: () * Step 4: Unfold WORST_CASE(?,POLY) + Considered Problem: Rules: f0(A,B) -> f2(A,B) [A >= 1 && B >= 1] f0(A,B) -> f2(A,B) [A >= 1 && 0 >= 1 + B] f0(A,B) -> f2(A,B) [0 >= 1 + A && B >= 1] f0(A,B) -> f2(A,B) [0 >= 1 + A && 0 >= 1 + B] f2(A,B) -> f2(A,-1 + B) [A >= B && B >= 2 && A >= 1 && A + B >= 2] f2(A,B) -> f2(A,-1 + B) [A >= B && 0 >= B && A >= 1 && A + B >= 2] f2(A,B) -> f2(-1 + A,B) [1 >= A + B && A >= 1 + B && A >= 2 && 0 >= 1 + B] f2(A,B) -> f2(-1 + A,B) [1 >= A + B && A >= 1 + B && 0 >= A && 0 >= 1 + B] f2(A,B) -> f2(A,1 + B) [B >= A && B >= 0 && 0 >= 1 + A && 0 >= 1 + A + B] f2(A,B) -> f2(A,1 + B) [B >= A && 0 >= 2 + B && 0 >= 1 + A && 0 >= 1 + A + B] f2(A,B) -> f2(1 + A,B) [A + B >= 0 && B >= 1 + A && A >= 0 && B >= 1] f2(A,B) -> f2(1 + A,B) [A + B >= 0 && B >= 1 + A && 0 >= 2 + A && B >= 1] Signature: {(f0,2);(f2,2)} Rule Graph: [0->{4,16},1->{6,9},2->{13,18},3->{11,15},4->{4},6->{6,9},9->{9},11->{11,15},13->{13,18},15->{15},16->{4 ,16},18->{18}] + Applied Processor: Unfold + Details: () * Step 5: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: f0.0(A,B) -> f2.4(A,B) [A >= 1 && B >= 1] f0.0(A,B) -> f2.16(A,B) [A >= 1 && B >= 1] f0.1(A,B) -> f2.6(A,B) [A >= 1 && 0 >= 1 + B] f0.1(A,B) -> f2.9(A,B) [A >= 1 && 0 >= 1 + B] f0.2(A,B) -> f2.13(A,B) [0 >= 1 + A && B >= 1] f0.2(A,B) -> f2.18(A,B) [0 >= 1 + A && B >= 1] f0.3(A,B) -> f2.11(A,B) [0 >= 1 + A && 0 >= 1 + B] f0.3(A,B) -> f2.15(A,B) [0 >= 1 + A && 0 >= 1 + B] f2.4(A,B) -> f2.4(A,-1 + B) [A >= B && B >= 2 && A >= 1 && A + B >= 2] f2.6(A,B) -> f2.6(A,-1 + B) [A >= B && 0 >= B && A >= 1 && A + B >= 2] f2.6(A,B) -> f2.9(A,-1 + B) [A >= B && 0 >= B && A >= 1 && A + B >= 2] f2.9(A,B) -> f2.9(-1 + A,B) [1 >= A + B && A >= 1 + B && A >= 2 && 0 >= 1 + B] f2.11(A,B) -> f2.11(-1 + A,B) [1 >= A + B && A >= 1 + B && 0 >= A && 0 >= 1 + B] f2.11(A,B) -> f2.15(-1 + A,B) [1 >= A + B && A >= 1 + B && 0 >= A && 0 >= 1 + B] f2.13(A,B) -> f2.13(A,1 + B) [B >= A && B >= 0 && 0 >= 1 + A && 0 >= 1 + A + B] f2.13(A,B) -> f2.18(A,1 + B) [B >= A && B >= 0 && 0 >= 1 + A && 0 >= 1 + A + B] f2.15(A,B) -> f2.15(A,1 + B) [B >= A && 0 >= 2 + B && 0 >= 1 + A && 0 >= 1 + A + B] f2.16(A,B) -> f2.4(1 + A,B) [A + B >= 0 && B >= 1 + A && A >= 0 && B >= 1] f2.16(A,B) -> f2.16(1 + A,B) [A + B >= 0 && B >= 1 + A && A >= 0 && B >= 1] f2.18(A,B) -> f2.18(1 + A,B) [A + B >= 0 && B >= 1 + A && 0 >= 2 + A && B >= 1] Signature: {(f0.0,2) ;(f0.1,2) ;(f0.2,2) ;(f0.3,2) ;(f2.11,2) ;(f2.13,2) ;(f2.15,2) ;(f2.16,2) ;(f2.18,2) ;(f2.4,2) ;(f2.6,2) ;(f2.9,2)} Rule Graph: [0->{8},1->{17,18},2->{9,10},3->{11},4->{14,15},5->{19},6->{12,13},7->{16},8->{8},9->{9,10},10->{11} ,11->{11},12->{12,13},13->{16},14->{14,15},15->{19},16->{16},17->{8},18->{17,18},19->{19}] + Applied Processor: AddSinks + Details: () * Step 6: Decompose WORST_CASE(?,POLY) + Considered Problem: Rules: f0.0(A,B) -> f2.4(A,B) [A >= 1 && B >= 1] f0.0(A,B) -> f2.16(A,B) [A >= 1 && B >= 1] f0.1(A,B) -> f2.6(A,B) [A >= 1 && 0 >= 1 + B] f0.1(A,B) -> f2.9(A,B) [A >= 1 && 0 >= 1 + B] f0.2(A,B) -> f2.13(A,B) [0 >= 1 + A && B >= 1] f0.2(A,B) -> f2.18(A,B) [0 >= 1 + A && B >= 1] f0.3(A,B) -> f2.11(A,B) [0 >= 1 + A && 0 >= 1 + B] f0.3(A,B) -> f2.15(A,B) [0 >= 1 + A && 0 >= 1 + B] f2.4(A,B) -> f2.4(A,-1 + B) [A >= B && B >= 2 && A >= 1 && A + B >= 2] f2.6(A,B) -> f2.6(A,-1 + B) [A >= B && 0 >= B && A >= 1 && A + B >= 2] f2.6(A,B) -> f2.9(A,-1 + B) [A >= B && 0 >= B && A >= 1 && A + B >= 2] f2.9(A,B) -> f2.9(-1 + A,B) [1 >= A + B && A >= 1 + B && A >= 2 && 0 >= 1 + B] f2.11(A,B) -> f2.11(-1 + A,B) [1 >= A + B && A >= 1 + B && 0 >= A && 0 >= 1 + B] f2.11(A,B) -> f2.15(-1 + A,B) [1 >= A + B && A >= 1 + B && 0 >= A && 0 >= 1 + B] f2.13(A,B) -> f2.13(A,1 + B) [B >= A && B >= 0 && 0 >= 1 + A && 0 >= 1 + A + B] f2.13(A,B) -> f2.18(A,1 + B) [B >= A && B >= 0 && 0 >= 1 + A && 0 >= 1 + A + B] f2.15(A,B) -> f2.15(A,1 + B) [B >= A && 0 >= 2 + B && 0 >= 1 + A && 0 >= 1 + A + B] f2.16(A,B) -> f2.4(1 + A,B) [A + B >= 0 && B >= 1 + A && A >= 0 && B >= 1] f2.16(A,B) -> f2.16(1 + A,B) [A + B >= 0 && B >= 1 + A && A >= 0 && B >= 1] f2.18(A,B) -> f2.18(1 + A,B) [A + B >= 0 && B >= 1 + A && 0 >= 2 + A && B >= 1] f2.15(A,B) -> exitus616(A,B) True f2.15(A,B) -> exitus616(A,B) True f2.18(A,B) -> exitus616(A,B) True f2.18(A,B) -> exitus616(A,B) True f2.9(A,B) -> exitus616(A,B) True f2.9(A,B) -> exitus616(A,B) True f2.4(A,B) -> exitus616(A,B) True f2.4(A,B) -> exitus616(A,B) True Signature: {(exitus616,2) ;(f0.0,2) ;(f0.1,2) ;(f0.2,2) ;(f0.3,2) ;(f2.11,2) ;(f2.13,2) ;(f2.15,2) ;(f2.16,2) ;(f2.18,2) ;(f2.4,2) ;(f2.6,2) ;(f2.9,2)} Rule Graph: [0->{8},1->{17,18},2->{9,10},3->{11},4->{14,15},5->{19},6->{12,13},7->{16},8->{8,26,27},9->{9,10},10->{11} ,11->{11,24,25},12->{12,13},13->{16},14->{14,15},15->{19},16->{16,20,21},17->{8},18->{17,18},19->{19,22,23}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27] | +- p:[12] c: [12] | +- p:[16] c: [16] | +- p:[14] c: [14] | +- p:[19] c: [19] | +- p:[9] c: [9] | +- p:[11] c: [11] | +- p:[18] c: [18] | `- p:[8] c: [8] * Step 7: AbstractSize WORST_CASE(?,POLY) + Considered Problem: (Rules: f0.0(A,B) -> f2.4(A,B) [A >= 1 && B >= 1] f0.0(A,B) -> f2.16(A,B) [A >= 1 && B >= 1] f0.1(A,B) -> f2.6(A,B) [A >= 1 && 0 >= 1 + B] f0.1(A,B) -> f2.9(A,B) [A >= 1 && 0 >= 1 + B] f0.2(A,B) -> f2.13(A,B) [0 >= 1 + A && B >= 1] f0.2(A,B) -> f2.18(A,B) [0 >= 1 + A && B >= 1] f0.3(A,B) -> f2.11(A,B) [0 >= 1 + A && 0 >= 1 + B] f0.3(A,B) -> f2.15(A,B) [0 >= 1 + A && 0 >= 1 + B] f2.4(A,B) -> f2.4(A,-1 + B) [A >= B && B >= 2 && A >= 1 && A + B >= 2] f2.6(A,B) -> f2.6(A,-1 + B) [A >= B && 0 >= B && A >= 1 && A + B >= 2] f2.6(A,B) -> f2.9(A,-1 + B) [A >= B && 0 >= B && A >= 1 && A + B >= 2] f2.9(A,B) -> f2.9(-1 + A,B) [1 >= A + B && A >= 1 + B && A >= 2 && 0 >= 1 + B] f2.11(A,B) -> f2.11(-1 + A,B) [1 >= A + B && A >= 1 + B && 0 >= A && 0 >= 1 + B] f2.11(A,B) -> f2.15(-1 + A,B) [1 >= A + B && A >= 1 + B && 0 >= A && 0 >= 1 + B] f2.13(A,B) -> f2.13(A,1 + B) [B >= A && B >= 0 && 0 >= 1 + A && 0 >= 1 + A + B] f2.13(A,B) -> f2.18(A,1 + B) [B >= A && B >= 0 && 0 >= 1 + A && 0 >= 1 + A + B] f2.15(A,B) -> f2.15(A,1 + B) [B >= A && 0 >= 2 + B && 0 >= 1 + A && 0 >= 1 + A + B] f2.16(A,B) -> f2.4(1 + A,B) [A + B >= 0 && B >= 1 + A && A >= 0 && B >= 1] f2.16(A,B) -> f2.16(1 + A,B) [A + B >= 0 && B >= 1 + A && A >= 0 && B >= 1] f2.18(A,B) -> f2.18(1 + A,B) [A + B >= 0 && B >= 1 + A && 0 >= 2 + A && B >= 1] f2.15(A,B) -> exitus616(A,B) True f2.15(A,B) -> exitus616(A,B) True f2.18(A,B) -> exitus616(A,B) True f2.18(A,B) -> exitus616(A,B) True f2.9(A,B) -> exitus616(A,B) True f2.9(A,B) -> exitus616(A,B) True f2.4(A,B) -> exitus616(A,B) True f2.4(A,B) -> exitus616(A,B) True Signature: {(exitus616,2) ;(f0.0,2) ;(f0.1,2) ;(f0.2,2) ;(f0.3,2) ;(f2.11,2) ;(f2.13,2) ;(f2.15,2) ;(f2.16,2) ;(f2.18,2) ;(f2.4,2) ;(f2.6,2) ;(f2.9,2)} Rule Graph: [0->{8},1->{17,18},2->{9,10},3->{11},4->{14,15},5->{19},6->{12,13},7->{16},8->{8,26,27},9->{9,10},10->{11} ,11->{11,24,25},12->{12,13},13->{16},14->{14,15},15->{19},16->{16,20,21},17->{8},18->{17,18},19->{19,22,23}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27] | +- p:[12] c: [12] | +- p:[16] c: [16] | +- p:[14] c: [14] | +- p:[19] c: [19] | +- p:[9] c: [9] | +- p:[11] c: [11] | +- p:[18] c: [18] | `- p:[8] c: [8]) + Applied Processor: AbstractSize Minimize + Details: () * Step 8: AbstractFlow WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,0.0,0.1,0.2,0.3,0.4,0.5,0.6,0.7] f0.0 ~> f2.4 [A <= A, B <= B] f0.0 ~> f2.16 [A <= A, B <= B] f0.1 ~> f2.6 [A <= A, B <= B] f0.1 ~> f2.9 [A <= A, B <= B] f0.2 ~> f2.13 [A <= A, B <= B] f0.2 ~> f2.18 [A <= A, B <= B] f0.3 ~> f2.11 [A <= A, B <= B] f0.3 ~> f2.15 [A <= A, B <= B] f2.4 ~> f2.4 [A <= A, B <= B] f2.6 ~> f2.6 [A <= A, B <= A] f2.6 ~> f2.9 [A <= A, B <= A] f2.9 ~> f2.9 [A <= B, B <= B] f2.11 ~> f2.11 [A <= B, B <= B] f2.11 ~> f2.15 [A <= B, B <= B] f2.13 ~> f2.13 [A <= A, B <= A] f2.13 ~> f2.18 [A <= A, B <= A] f2.15 ~> f2.15 [A <= A, B <= B] f2.16 ~> f2.4 [A <= B, B <= B] f2.16 ~> f2.16 [A <= B, B <= B] f2.18 ~> f2.18 [A <= B, B <= B] f2.15 ~> exitus616 [A <= A, B <= B] f2.15 ~> exitus616 [A <= A, B <= B] f2.18 ~> exitus616 [A <= A, B <= B] f2.18 ~> exitus616 [A <= A, B <= B] f2.9 ~> exitus616 [A <= A, B <= B] f2.9 ~> exitus616 [A <= A, B <= B] f2.4 ~> exitus616 [A <= A, B <= B] f2.4 ~> exitus616 [A <= A, B <= B] + Loop: [0.0 <= K + A + B] f2.11 ~> f2.11 [A <= B, B <= B] + Loop: [0.1 <= K + A + B] f2.15 ~> f2.15 [A <= A, B <= B] + Loop: [0.2 <= K + A + B] f2.13 ~> f2.13 [A <= A, B <= A] + Loop: [0.3 <= 2*K + A] f2.18 ~> f2.18 [A <= B, B <= B] + Loop: [0.4 <= 2*K + A + B] f2.6 ~> f2.6 [A <= A, B <= A] + Loop: [0.5 <= 2*K + A] f2.9 ~> f2.9 [A <= B, B <= B] + Loop: [0.6 <= K + A + B] f2.16 ~> f2.16 [A <= B, B <= B] + Loop: [0.7 <= 2*K + A + B] f2.4 ~> f2.4 [A <= A, B <= B] + Applied Processor: AbstractFlow + Details: () * Step 9: Lare WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,A,B,0.0,0.1,0.2,0.3,0.4,0.5,0.6,0.7] f0.0 ~> f2.4 [] f0.0 ~> f2.16 [] f0.1 ~> f2.6 [] f0.1 ~> f2.9 [] f0.2 ~> f2.13 [] f0.2 ~> f2.18 [] f0.3 ~> f2.11 [] f0.3 ~> f2.15 [] f2.4 ~> f2.4 [] f2.6 ~> f2.6 [A ~=> B] f2.6 ~> f2.9 [A ~=> B] f2.9 ~> f2.9 [B ~=> A] f2.11 ~> f2.11 [B ~=> A] f2.11 ~> f2.15 [B ~=> A] f2.13 ~> f2.13 [A ~=> B] f2.13 ~> f2.18 [A ~=> B] f2.15 ~> f2.15 [] f2.16 ~> f2.4 [B ~=> A] f2.16 ~> f2.16 [B ~=> A] f2.18 ~> f2.18 [B ~=> A] f2.15 ~> exitus616 [] f2.15 ~> exitus616 [] f2.18 ~> exitus616 [] f2.18 ~> exitus616 [] f2.9 ~> exitus616 [] f2.9 ~> exitus616 [] f2.4 ~> exitus616 [] f2.4 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~+> 0.0] f2.11 ~> f2.11 [B ~=> A] + Loop: [A ~+> 0.1,B ~+> 0.1,K ~+> 0.1] f2.15 ~> f2.15 [] + Loop: [A ~+> 0.2,B ~+> 0.2,K ~+> 0.2] f2.13 ~> f2.13 [A ~=> B] + Loop: [A ~+> 0.3,K ~*> 0.3] f2.18 ~> f2.18 [B ~=> A] + Loop: [A ~+> 0.4,B ~+> 0.4,K ~*> 0.4] f2.6 ~> f2.6 [A ~=> B] + Loop: [A ~+> 0.5,K ~*> 0.5] f2.9 ~> f2.9 [B ~=> A] + Loop: [A ~+> 0.6,B ~+> 0.6,K ~+> 0.6] f2.16 ~> f2.16 [B ~=> A] + Loop: [A ~+> 0.7,B ~+> 0.7,K ~*> 0.7] f2.4 ~> f2.4 [] + Applied Processor: Lare + Details: f0.3 ~> exitus616 [B ~=> A ,A ~+> 0.0 ,A ~+> 0.1 ,A ~+> tick ,B ~+> 0.0 ,B ~+> 0.1 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> tick ,B ~*> 0.1 ,B ~*> tick ,K ~*> tick] f0.1 ~> exitus616 [A ~=> B ,B ~=> A ,A ~+> 0.4 ,A ~+> 0.5 ,A ~+> tick ,B ~+> 0.4 ,B ~+> tick ,tick ~+> tick ,A ~*> tick ,K ~*> 0.4 ,K ~*> 0.5 ,K ~*> tick] f0.0 ~> exitus616 [B ~=> A ,A ~+> 0.6 ,A ~+> 0.7 ,A ~+> tick ,B ~+> 0.6 ,B ~+> 0.7 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.6 ,K ~+> tick ,B ~*> 0.7 ,B ~*> tick ,K ~*> 0.7 ,K ~*> tick] f0.2 ~> exitus616 [A ~=> B ,B ~=> A ,A ~+> 0.2 ,A ~+> 0.3 ,A ~+> tick ,B ~+> 0.2 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.2 ,K ~+> tick ,A ~*> tick ,K ~*> 0.3 ,K ~*> tick] + f2.11> [B ~=> A,A ~+> 0.0,A ~+> tick,B ~+> 0.0,B ~+> tick,tick ~+> tick,K ~+> 0.0,K ~+> tick] + f2.15> [A ~+> 0.1,A ~+> tick,B ~+> 0.1,B ~+> tick,tick ~+> tick,K ~+> 0.1,K ~+> tick] + f2.13> [A ~=> B,A ~+> 0.2,A ~+> tick,B ~+> 0.2,B ~+> tick,tick ~+> tick,K ~+> 0.2,K ~+> tick] + f2.18> [B ~=> A,A ~+> 0.3,A ~+> tick,tick ~+> tick,K ~*> 0.3,K ~*> tick] + f2.6> [A ~=> B,A ~+> 0.4,A ~+> tick,B ~+> 0.4,B ~+> tick,tick ~+> tick,K ~*> 0.4,K ~*> tick] + f2.9> [B ~=> A,A ~+> 0.5,A ~+> tick,tick ~+> tick,K ~*> 0.5,K ~*> tick] + f2.16> [B ~=> A,A ~+> 0.6,A ~+> tick,B ~+> 0.6,B ~+> tick,tick ~+> tick,K ~+> 0.6,K ~+> tick] + f2.4> [A ~+> 0.7,A ~+> tick,B ~+> 0.7,B ~+> tick,tick ~+> tick,K ~*> 0.7,K ~*> tick] YES(?,POLY)