YES(?,O(n^1)) * Step 1: UnsatRules WORST_CASE(?,O(n^1)) + 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(?,O(n^1)) + 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: AddSinks WORST_CASE(?,O(n^1)) + 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: AddSinks + Details: () * Step 4: UnsatPaths WORST_CASE(?,O(n^1)) + 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) 19. f2(A,B) -> exitus616(A,B) True (?,1) Signature: {(exitus616,2);(f0,2);(f2,2)} Flow Graph: [0->{4,6,9,11,13,15,16,18,19},1->{4,6,9,11,13,15,16,18,19},2->{4,6,9,11,13,15,16,18,19},3->{4,6,9,11,13,15 ,16,18,19},4->{4,6,9,11,13,15,16,18,19},6->{4,6,9,11,13,15,16,18,19},9->{4,6,9,11,13,15,16,18,19},11->{4,6,9 ,11,13,15,16,18,19},13->{4,6,9,11,13,15,16,18,19},15->{4,6,9,11,13,15,16,18,19},16->{4,6,9,11,13,15,16,18 ,19},18->{4,6,9,11,13,15,16,18,19},19->{}] + 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 5: LooptreeTransformer WORST_CASE(?,O(n^1)) + 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) 19. f2(A,B) -> exitus616(A,B) True (?,1) Signature: {(exitus616,2);(f0,2);(f2,2)} Flow Graph: [0->{4,16,19},1->{6,9,19},2->{13,18,19},3->{11,15,19},4->{4,19},6->{6,9,19},9->{9,19},11->{11,15,19} ,13->{13,18,19},15->{15,19},16->{4,16,19},18->{18,19},19->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,6,9,11,13,15,16,18,19] | +- p:[11] c: [11] | +- p:[15] c: [15] | +- p:[13] c: [13] | +- p:[18] c: [18] | +- p:[6] c: [6] | +- p:[9] c: [9] | +- p:[16] c: [16] | `- p:[4] c: [4] * Step 6: SizeAbstraction WORST_CASE(?,O(n^1)) + 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) 19. f2(A,B) -> exitus616(A,B) True (?,1) Signature: {(exitus616,2);(f0,2);(f2,2)} Flow Graph: [0->{4,16,19},1->{6,9,19},2->{13,18,19},3->{11,15,19},4->{4,19},6->{6,9,19},9->{9,19},11->{11,15,19} ,13->{13,18,19},15->{15,19},16->{4,16,19},18->{18,19},19->{}] ,We construct a looptree: P: [0,1,2,3,4,6,9,11,13,15,16,18,19] | +- p:[11] c: [11] | +- p:[15] c: [15] | +- p:[13] c: [13] | +- p:[18] c: [18] | +- p:[6] c: [6] | +- p:[9] c: [9] | +- p:[16] c: [16] | `- p:[4] c: [4]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 7: FlowAbstraction WORST_CASE(?,O(n^1)) + Considered Problem: Program: Domain: [A,B,0.0,0.1,0.2,0.3,0.4,0.5,0.6,0.7] f0 ~> f2 [A <= A, B <= B] f0 ~> f2 [A <= A, B <= B] f0 ~> f2 [A <= A, B <= B] f0 ~> f2 [A <= A, B <= B] f2 ~> f2 [A <= A, B <= B] f2 ~> f2 [A <= A, B <= A] f2 ~> f2 [A <= B, B <= B] f2 ~> f2 [A <= B, B <= B] f2 ~> f2 [A <= A, B <= A] f2 ~> f2 [A <= A, B <= B] f2 ~> f2 [A <= B, B <= B] f2 ~> f2 [A <= B, B <= B] f2 ~> exitus616 [A <= A, B <= B] + Loop: [0.0 <= A + B] f2 ~> f2 [A <= B, B <= B] + Loop: [0.1 <= A + B] f2 ~> f2 [A <= A, B <= B] + Loop: [0.2 <= A + B] f2 ~> f2 [A <= A, B <= A] + Loop: [0.3 <= A] f2 ~> f2 [A <= B, B <= B] + Loop: [0.4 <= A + B] f2 ~> f2 [A <= A, B <= A] + Loop: [0.5 <= A + B] f2 ~> f2 [A <= B, B <= B] + Loop: [0.6 <= A + B] f2 ~> f2 [A <= B, B <= B] + Loop: [0.7 <= B] f2 ~> f2 [A <= A, B <= B] + Applied Processor: FlowAbstraction + Details: () * Step 8: LareProcessor WORST_CASE(?,O(n^1)) + 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 ~> f2 [] f0 ~> f2 [] f0 ~> f2 [] f0 ~> f2 [] f2 ~> f2 [] f2 ~> f2 [A ~=> B] f2 ~> f2 [B ~=> A] f2 ~> f2 [B ~=> A] f2 ~> f2 [A ~=> B] f2 ~> f2 [] f2 ~> f2 [B ~=> A] f2 ~> f2 [B ~=> A] f2 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0] f2 ~> f2 [B ~=> A] + Loop: [A ~+> 0.1,B ~+> 0.1] f2 ~> f2 [] + Loop: [A ~+> 0.2,B ~+> 0.2] f2 ~> f2 [A ~=> B] + Loop: [A ~=> 0.3] f2 ~> f2 [B ~=> A] + Loop: [A ~+> 0.4,B ~+> 0.4] f2 ~> f2 [A ~=> B] + Loop: [A ~+> 0.5,B ~+> 0.5] f2 ~> f2 [B ~=> A] + Loop: [A ~+> 0.6,B ~+> 0.6] f2 ~> f2 [B ~=> A] + Loop: [B ~=> 0.7] f2 ~> f2 [] + Applied Processor: LareProcessor + Details: f0 ~> exitus616 [A ~=> B ,A ~=> 0.3 ,B ~=> A ,B ~=> 0.7 ,A ~+> 0.0 ,A ~+> 0.1 ,A ~+> 0.2 ,A ~+> 0.4 ,A ~+> 0.5 ,A ~+> 0.6 ,A ~+> tick ,B ~+> 0.0 ,B ~+> 0.1 ,B ~+> 0.2 ,B ~+> 0.4 ,B ~+> 0.5 ,B ~+> 0.6 ,B ~+> tick ,tick ~+> tick] + f2> [B ~=> A,A ~+> 0.0,A ~+> tick,B ~+> 0.0,B ~+> tick,tick ~+> tick] + f2> [A ~+> 0.1,A ~+> tick,B ~+> 0.1,B ~+> tick,tick ~+> tick] + f2> [A ~=> B,A ~+> 0.2,A ~+> tick,B ~+> 0.2,B ~+> tick,tick ~+> tick] + f2> [A ~=> 0.3,B ~=> A,A ~+> tick,tick ~+> tick] + f2> [A ~=> B,A ~+> 0.4,A ~+> tick,B ~+> 0.4,B ~+> tick,tick ~+> tick] + f2> [B ~=> A,A ~+> 0.5,A ~+> tick,B ~+> 0.5,B ~+> tick,tick ~+> tick] + f2> [B ~=> A,A ~+> 0.6,A ~+> tick,B ~+> 0.6,B ~+> tick,tick ~+> tick] + f2> [B ~=> 0.7,B ~+> tick,tick ~+> tick] YES(?,O(n^1))