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