YES(?,POLY) * Step 1: ArgumentFilter WORST_CASE(?,POLY) + Considered Problem: Rules: 0. eval1(A,B,C,D) -> eval2(-1 + A,B,C,D) [A >= 2] (1,1) 1. eval1(A,B,C,D) -> eval2(A,-1 + B,C,D) [1 >= A] (1,1) 2. eval2(A,B,C,D) -> eval3(A,B,A,2*A) [B >= 2] (?,1) 3. eval3(A,B,C,D) -> eval4(A,B,C,D) [-2 + B >= 0 && B >= D && B >= 1 + D] (?,1) 4. eval3(A,B,C,D) -> eval4(A,B,C,1 + D) [-2 + B >= 0 && B >= D && B >= 1 + D] (?,1) 5. eval3(A,B,C,D) -> eval3(A,B,D,2*D) [-2 + B >= 0 && B >= D && B >= 1 + D && D >= 1] (?,1) 6. eval3(A,B,C,D) -> eval3(A,B,1 + D,2 + 2*D) [-2 + B >= 0 && B >= D && B >= 1 + D && D >= 1] (?,1) 7. eval3(A,B,C,D) -> eval4(A,B,C,D) [-2 + B >= 0 && B = D] (?,1) 8. eval3(A,B,C,D) -> eval3(A,B,D,2*D) [-2 + B >= 0 && D >= 1 && B = D] (?,1) 9. eval4(A,B,C,D) -> eval2(-1 + A,B,C,D) [B + -1*D >= 0 && -2 + B >= 0 && A >= 2 && A >= 1 && B >= 2] (?,1) 10. eval4(A,B,C,D) -> eval2(A,-1 + B,C,D) [B + -1*D >= 0 && -2 + B >= 0 && B >= 2 && A = 1] (?,1) Signature: {(eval1,4);(eval2,4);(eval3,4);(eval4,4)} Flow Graph: [0->{2},1->{2},2->{3,4,5,6,7,8},3->{9,10},4->{9,10},5->{3,4,5,6,7,8},6->{3,4,5,6,7,8},7->{9,10},8->{3,4,5 ,6,7,8},9->{2},10->{2}] + Applied Processor: ArgumentFilter [2] + Details: We remove following argument positions: [2]. * Step 2: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. eval1(A,B,D) -> eval2(-1 + A,B,D) [A >= 2] (1,1) 1. eval1(A,B,D) -> eval2(A,-1 + B,D) [1 >= A] (1,1) 2. eval2(A,B,D) -> eval3(A,B,2*A) [B >= 2] (?,1) 3. eval3(A,B,D) -> eval4(A,B,D) [-2 + B >= 0 && B >= D && B >= 1 + D] (?,1) 4. eval3(A,B,D) -> eval4(A,B,1 + D) [-2 + B >= 0 && B >= D && B >= 1 + D] (?,1) 5. eval3(A,B,D) -> eval3(A,B,2*D) [-2 + B >= 0 && B >= D && B >= 1 + D && D >= 1] (?,1) 6. eval3(A,B,D) -> eval3(A,B,2 + 2*D) [-2 + B >= 0 && B >= D && B >= 1 + D && D >= 1] (?,1) 7. eval3(A,B,D) -> eval4(A,B,D) [-2 + B >= 0 && B = D] (?,1) 8. eval3(A,B,D) -> eval3(A,B,2*D) [-2 + B >= 0 && D >= 1 && B = D] (?,1) 9. eval4(A,B,D) -> eval2(-1 + A,B,D) [B + -1*D >= 0 && -2 + B >= 0 && A >= 2 && A >= 1 && B >= 2] (?,1) 10. eval4(A,B,D) -> eval2(A,-1 + B,D) [B + -1*D >= 0 && -2 + B >= 0 && B >= 2 && A = 1] (?,1) Signature: {(eval1,4);(eval2,4);(eval3,4);(eval4,4)} Flow Graph: [0->{2},1->{2},2->{3,4,5,6,7,8},3->{9,10},4->{9,10},5->{3,4,5,6,7,8},6->{3,4,5,6,7,8},7->{9,10},8->{3,4,5 ,6,7,8},9->{2},10->{2}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(8,3),(8,4),(8,5),(8,6),(8,7),(8,8)] * Step 3: FromIts WORST_CASE(?,POLY) + Considered Problem: Rules: 0. eval1(A,B,D) -> eval2(-1 + A,B,D) [A >= 2] (1,1) 1. eval1(A,B,D) -> eval2(A,-1 + B,D) [1 >= A] (1,1) 2. eval2(A,B,D) -> eval3(A,B,2*A) [B >= 2] (?,1) 3. eval3(A,B,D) -> eval4(A,B,D) [-2 + B >= 0 && B >= D && B >= 1 + D] (?,1) 4. eval3(A,B,D) -> eval4(A,B,1 + D) [-2 + B >= 0 && B >= D && B >= 1 + D] (?,1) 5. eval3(A,B,D) -> eval3(A,B,2*D) [-2 + B >= 0 && B >= D && B >= 1 + D && D >= 1] (?,1) 6. eval3(A,B,D) -> eval3(A,B,2 + 2*D) [-2 + B >= 0 && B >= D && B >= 1 + D && D >= 1] (?,1) 7. eval3(A,B,D) -> eval4(A,B,D) [-2 + B >= 0 && B = D] (?,1) 8. eval3(A,B,D) -> eval3(A,B,2*D) [-2 + B >= 0 && D >= 1 && B = D] (?,1) 9. eval4(A,B,D) -> eval2(-1 + A,B,D) [B + -1*D >= 0 && -2 + B >= 0 && A >= 2 && A >= 1 && B >= 2] (?,1) 10. eval4(A,B,D) -> eval2(A,-1 + B,D) [B + -1*D >= 0 && -2 + B >= 0 && B >= 2 && A = 1] (?,1) Signature: {(eval1,4);(eval2,4);(eval3,4);(eval4,4)} Flow Graph: [0->{2},1->{2},2->{3,4,5,6,7,8},3->{9,10},4->{9,10},5->{3,4,5,6,7,8},6->{3,4,5,6,7,8},7->{9,10},8->{} ,9->{2},10->{2}] + Applied Processor: FromIts + Details: () * Step 4: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: eval1(A,B,D) -> eval2(-1 + A,B,D) [A >= 2] eval1(A,B,D) -> eval2(A,-1 + B,D) [1 >= A] eval2(A,B,D) -> eval3(A,B,2*A) [B >= 2] eval3(A,B,D) -> eval4(A,B,D) [-2 + B >= 0 && B >= D && B >= 1 + D] eval3(A,B,D) -> eval4(A,B,1 + D) [-2 + B >= 0 && B >= D && B >= 1 + D] eval3(A,B,D) -> eval3(A,B,2*D) [-2 + B >= 0 && B >= D && B >= 1 + D && D >= 1] eval3(A,B,D) -> eval3(A,B,2 + 2*D) [-2 + B >= 0 && B >= D && B >= 1 + D && D >= 1] eval3(A,B,D) -> eval4(A,B,D) [-2 + B >= 0 && B = D] eval3(A,B,D) -> eval3(A,B,2*D) [-2 + B >= 0 && D >= 1 && B = D] eval4(A,B,D) -> eval2(-1 + A,B,D) [B + -1*D >= 0 && -2 + B >= 0 && A >= 2 && A >= 1 && B >= 2] eval4(A,B,D) -> eval2(A,-1 + B,D) [B + -1*D >= 0 && -2 + B >= 0 && B >= 2 && A = 1] Signature: {(eval1,4);(eval2,4);(eval3,4);(eval4,4)} Rule Graph: [0->{2},1->{2},2->{3,4,5,6,7,8},3->{9,10},4->{9,10},5->{3,4,5,6,7,8},6->{3,4,5,6,7,8},7->{9,10},8->{} ,9->{2},10->{2}] + Applied Processor: AddSinks + Details: () * Step 5: Decompose WORST_CASE(?,POLY) + Considered Problem: Rules: eval1(A,B,D) -> eval2(-1 + A,B,D) [A >= 2] eval1(A,B,D) -> eval2(A,-1 + B,D) [1 >= A] eval2(A,B,D) -> eval3(A,B,2*A) [B >= 2] eval3(A,B,D) -> eval4(A,B,D) [-2 + B >= 0 && B >= D && B >= 1 + D] eval3(A,B,D) -> eval4(A,B,1 + D) [-2 + B >= 0 && B >= D && B >= 1 + D] eval3(A,B,D) -> eval3(A,B,2*D) [-2 + B >= 0 && B >= D && B >= 1 + D && D >= 1] eval3(A,B,D) -> eval3(A,B,2 + 2*D) [-2 + B >= 0 && B >= D && B >= 1 + D && D >= 1] eval3(A,B,D) -> eval4(A,B,D) [-2 + B >= 0 && B = D] eval3(A,B,D) -> eval3(A,B,2*D) [-2 + B >= 0 && D >= 1 && B = D] eval4(A,B,D) -> eval2(-1 + A,B,D) [B + -1*D >= 0 && -2 + B >= 0 && A >= 2 && A >= 1 && B >= 2] eval4(A,B,D) -> eval2(A,-1 + B,D) [B + -1*D >= 0 && -2 + B >= 0 && B >= 2 && A = 1] eval3(A,B,D) -> exitus616(A,B,D) True eval3(A,B,D) -> exitus616(A,B,D) True Signature: {(eval1,4);(eval2,4);(eval3,4);(eval4,4);(exitus616,3)} Rule Graph: [0->{2},1->{2},2->{3,4,5,6,7,8},3->{9,10},4->{9,10},5->{3,4,5,6,7,8},6->{3,4,5,6,7,8},7->{9,10},8->{11,12} ,9->{2},10->{2}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12] | `- p:[2,9,3,5,6,4,7,10] c: [2,3,4,7,9,10] | `- p:[5,6] c: [5,6] * Step 6: AbstractSize WORST_CASE(?,POLY) + Considered Problem: (Rules: eval1(A,B,D) -> eval2(-1 + A,B,D) [A >= 2] eval1(A,B,D) -> eval2(A,-1 + B,D) [1 >= A] eval2(A,B,D) -> eval3(A,B,2*A) [B >= 2] eval3(A,B,D) -> eval4(A,B,D) [-2 + B >= 0 && B >= D && B >= 1 + D] eval3(A,B,D) -> eval4(A,B,1 + D) [-2 + B >= 0 && B >= D && B >= 1 + D] eval3(A,B,D) -> eval3(A,B,2*D) [-2 + B >= 0 && B >= D && B >= 1 + D && D >= 1] eval3(A,B,D) -> eval3(A,B,2 + 2*D) [-2 + B >= 0 && B >= D && B >= 1 + D && D >= 1] eval3(A,B,D) -> eval4(A,B,D) [-2 + B >= 0 && B = D] eval3(A,B,D) -> eval3(A,B,2*D) [-2 + B >= 0 && D >= 1 && B = D] eval4(A,B,D) -> eval2(-1 + A,B,D) [B + -1*D >= 0 && -2 + B >= 0 && A >= 2 && A >= 1 && B >= 2] eval4(A,B,D) -> eval2(A,-1 + B,D) [B + -1*D >= 0 && -2 + B >= 0 && B >= 2 && A = 1] eval3(A,B,D) -> exitus616(A,B,D) True eval3(A,B,D) -> exitus616(A,B,D) True Signature: {(eval1,4);(eval2,4);(eval3,4);(eval4,4);(exitus616,3)} Rule Graph: [0->{2},1->{2},2->{3,4,5,6,7,8},3->{9,10},4->{9,10},5->{3,4,5,6,7,8},6->{3,4,5,6,7,8},7->{9,10},8->{11,12} ,9->{2},10->{2}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12] | `- p:[2,9,3,5,6,4,7,10] c: [2,3,4,7,9,10] | `- p:[5,6] c: [5,6]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: AbstractFlow WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,D,0.0,0.0.0] eval1 ~> eval2 [A <= A, B <= B, D <= D] eval1 ~> eval2 [A <= A, B <= K + B, D <= D] eval2 ~> eval3 [A <= A, B <= B, D <= 2*A] eval3 ~> eval4 [A <= A, B <= B, D <= D] eval3 ~> eval4 [A <= A, B <= B, D <= B + D] eval3 ~> eval3 [A <= A, B <= B, D <= B + D] eval3 ~> eval3 [A <= A, B <= B, D <= K + B + D] eval3 ~> eval4 [A <= A, B <= B, D <= D] eval3 ~> eval3 [A <= A, B <= B, D <= B + D] eval4 ~> eval2 [A <= A, B <= B, D <= D] eval4 ~> eval2 [A <= A, B <= B, D <= D] eval3 ~> exitus616 [A <= A, B <= B, D <= D] eval3 ~> exitus616 [A <= A, B <= B, D <= D] + Loop: [0.0 <= A + B] eval2 ~> eval3 [A <= A, B <= B, D <= 2*A] eval4 ~> eval2 [A <= A, B <= B, D <= D] eval3 ~> eval4 [A <= A, B <= B, D <= D] eval3 ~> eval3 [A <= A, B <= B, D <= B + D] eval3 ~> eval3 [A <= A, B <= B, D <= K + B + D] eval3 ~> eval4 [A <= A, B <= B, D <= B + D] eval3 ~> eval4 [A <= A, B <= B, D <= D] eval4 ~> eval2 [A <= A, B <= B, D <= D] + Loop: [0.0.0 <= K + B + D] eval3 ~> eval3 [A <= A, B <= B, D <= B + D] eval3 ~> eval3 [A <= A, B <= B, D <= K + B + D] + Applied Processor: AbstractFlow + Details: () * Step 8: Lare WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,A,B,D,0.0,0.0.0] eval1 ~> eval2 [] eval1 ~> eval2 [B ~+> B,K ~+> B] eval2 ~> eval3 [A ~*> D] eval3 ~> eval4 [] eval3 ~> eval4 [B ~+> D,D ~+> D] eval3 ~> eval3 [B ~+> D,D ~+> D] eval3 ~> eval3 [B ~+> D,D ~+> D,K ~+> D] eval3 ~> eval4 [] eval3 ~> eval3 [B ~+> D,D ~+> D] eval4 ~> eval2 [] eval4 ~> eval2 [] eval3 ~> exitus616 [] eval3 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0] eval2 ~> eval3 [A ~*> D] eval4 ~> eval2 [] eval3 ~> eval4 [] eval3 ~> eval3 [B ~+> D,D ~+> D] eval3 ~> eval3 [B ~+> D,D ~+> D,K ~+> D] eval3 ~> eval4 [B ~+> D,D ~+> D] eval3 ~> eval4 [] eval4 ~> eval2 [] + Loop: [B ~+> 0.0.0,D ~+> 0.0.0,K ~+> 0.0.0] eval3 ~> eval3 [B ~+> D,D ~+> D] eval3 ~> eval3 [B ~+> D,D ~+> D,K ~+> D] + Applied Processor: Lare + Details: eval1 ~> exitus616 [A ~+> 0.0 ,A ~+> tick ,B ~+> B ,B ~+> D ,B ~+> 0.0 ,B ~+> 0.0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> D ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> D ,B ~*> 0.0.0 ,B ~*> tick ,K ~*> D ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> D ,B ~^> D ,K ~^> D] + eval3> [A ~+> 0.0 ,A ~+> tick ,B ~+> D ,B ~+> 0.0 ,B ~+> 0.0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> D ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> D ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> D ,B ~*> 0.0.0 ,B ~*> tick ,K ~*> D ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> D ,B ~^> D] + eval3> [B ~+> D ,B ~+> 0.0.0 ,B ~+> tick ,D ~+> D ,D ~+> 0.0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> D ,K ~+> 0.0.0 ,K ~+> tick ,B ~*> D ,D ~*> D ,K ~*> D] YES(?,POLY)