YES(?,POLY) * Step 1: FromIts WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f0(A,B,C,D,E) -> f1(A,B,C,D,E) True (1,1) 1. f1(A,B,C,D,E) -> f1(A,1 + B,C,D,E) [A >= 1 + B] (?,1) 2. f1(A,B,C,D,E) -> f2(A,B,B,D,E) [B >= A] (?,1) 3. f2(A,B,C,D,E) -> f2(A,B,-1 + C,D,E) [B + -1*C >= 0 && -1*A + B >= 0 && C >= 1] (?,1) 4. f2(A,B,C,D,E) -> f3(A,B,C,C,E) [B + -1*C >= 0 && -1*A + B >= 0 && 0 >= C] (?,1) 5. f3(A,B,C,D,E) -> f3(A,B,C,1 + D,E) [B + -1*D >= 0 && -1*C + D >= 0 && -1*C >= 0 && B + -1*C >= 0 && -1*A + B >= 0 && A >= 1 + D] (?,1) 6. f3(A,B,C,D,E) -> f4(A,B,C,D,D) [B + -1*D >= 0 && -1*C + D >= 0 && -1*C >= 0 && B + -1*C >= 0 && -1*A + B >= 0 && D >= A] (?,1) 7. f4(A,B,C,D,E) -> f4(A,B,C,D,-1 + E) [D + -1*E >= 0 (?,1) && B + -1*E >= 0 && -1*C + E >= 0 && B + -1*D >= 0 && -1*C + D >= 0 && -1*A + D >= 0 && -1*C >= 0 && B + -1*C >= 0 && -1*A + B >= 0 && E >= 1] Signature: {(f0,5);(f1,5);(f2,5);(f3,5);(f4,5)} Flow Graph: [0->{1,2},1->{1,2},2->{3,4},3->{3,4},4->{5,6},5->{5,6},6->{7},7->{7}] + Applied Processor: FromIts + Details: () * Step 2: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: f0(A,B,C,D,E) -> f1(A,B,C,D,E) True f1(A,B,C,D,E) -> f1(A,1 + B,C,D,E) [A >= 1 + B] f1(A,B,C,D,E) -> f2(A,B,B,D,E) [B >= A] f2(A,B,C,D,E) -> f2(A,B,-1 + C,D,E) [B + -1*C >= 0 && -1*A + B >= 0 && C >= 1] f2(A,B,C,D,E) -> f3(A,B,C,C,E) [B + -1*C >= 0 && -1*A + B >= 0 && 0 >= C] f3(A,B,C,D,E) -> f3(A,B,C,1 + D,E) [B + -1*D >= 0 && -1*C + D >= 0 && -1*C >= 0 && B + -1*C >= 0 && -1*A + B >= 0 && A >= 1 + D] f3(A,B,C,D,E) -> f4(A,B,C,D,D) [B + -1*D >= 0 && -1*C + D >= 0 && -1*C >= 0 && B + -1*C >= 0 && -1*A + B >= 0 && D >= A] f4(A,B,C,D,E) -> f4(A,B,C,D,-1 + E) [D + -1*E >= 0 && B + -1*E >= 0 && -1*C + E >= 0 && B + -1*D >= 0 && -1*C + D >= 0 && -1*A + D >= 0 && -1*C >= 0 && B + -1*C >= 0 && -1*A + B >= 0 && E >= 1] Signature: {(f0,5);(f1,5);(f2,5);(f3,5);(f4,5)} Rule Graph: [0->{1,2},1->{1,2},2->{3,4},3->{3,4},4->{5,6},5->{5,6},6->{7},7->{7}] + Applied Processor: AddSinks + Details: () * Step 3: Unfold WORST_CASE(?,POLY) + Considered Problem: Rules: f0(A,B,C,D,E) -> f1(A,B,C,D,E) True f1(A,B,C,D,E) -> f1(A,1 + B,C,D,E) [A >= 1 + B] f1(A,B,C,D,E) -> f2(A,B,B,D,E) [B >= A] f2(A,B,C,D,E) -> f2(A,B,-1 + C,D,E) [B + -1*C >= 0 && -1*A + B >= 0 && C >= 1] f2(A,B,C,D,E) -> f3(A,B,C,C,E) [B + -1*C >= 0 && -1*A + B >= 0 && 0 >= C] f3(A,B,C,D,E) -> f3(A,B,C,1 + D,E) [B + -1*D >= 0 && -1*C + D >= 0 && -1*C >= 0 && B + -1*C >= 0 && -1*A + B >= 0 && A >= 1 + D] f3(A,B,C,D,E) -> f4(A,B,C,D,D) [B + -1*D >= 0 && -1*C + D >= 0 && -1*C >= 0 && B + -1*C >= 0 && -1*A + B >= 0 && D >= A] f4(A,B,C,D,E) -> f4(A,B,C,D,-1 + E) [D + -1*E >= 0 && B + -1*E >= 0 && -1*C + E >= 0 && B + -1*D >= 0 && -1*C + D >= 0 && -1*A + D >= 0 && -1*C >= 0 && B + -1*C >= 0 && -1*A + B >= 0 && E >= 1] f4(A,B,C,D,E) -> exitus616(A,B,C,D,E) True Signature: {(exitus616,5);(f0,5);(f1,5);(f2,5);(f3,5);(f4,5)} Rule Graph: [0->{1,2},1->{1,2},2->{3,4},3->{3,4},4->{5,6},5->{5,6},6->{7},7->{7,8}] + Applied Processor: Unfold + Details: () * Step 4: Decompose WORST_CASE(?,POLY) + Considered Problem: Rules: f0.0(A,B,C,D,E) -> f1.1(A,B,C,D,E) True f0.0(A,B,C,D,E) -> f1.2(A,B,C,D,E) True f1.1(A,B,C,D,E) -> f1.1(A,1 + B,C,D,E) [A >= 1 + B] f1.1(A,B,C,D,E) -> f1.2(A,1 + B,C,D,E) [A >= 1 + B] f1.2(A,B,C,D,E) -> f2.3(A,B,B,D,E) [B >= A] f1.2(A,B,C,D,E) -> f2.4(A,B,B,D,E) [B >= A] f2.3(A,B,C,D,E) -> f2.3(A,B,-1 + C,D,E) [B + -1*C >= 0 && -1*A + B >= 0 && C >= 1] f2.3(A,B,C,D,E) -> f2.4(A,B,-1 + C,D,E) [B + -1*C >= 0 && -1*A + B >= 0 && C >= 1] f2.4(A,B,C,D,E) -> f3.5(A,B,C,C,E) [B + -1*C >= 0 && -1*A + B >= 0 && 0 >= C] f2.4(A,B,C,D,E) -> f3.6(A,B,C,C,E) [B + -1*C >= 0 && -1*A + B >= 0 && 0 >= C] f3.5(A,B,C,D,E) -> f3.5(A,B,C,1 + D,E) [B + -1*D >= 0 && -1*C + D >= 0 && -1*C >= 0 && B + -1*C >= 0 && -1*A + B >= 0 && A >= 1 + D] f3.5(A,B,C,D,E) -> f3.6(A,B,C,1 + D,E) [B + -1*D >= 0 && -1*C + D >= 0 && -1*C >= 0 && B + -1*C >= 0 && -1*A + B >= 0 && A >= 1 + D] f3.6(A,B,C,D,E) -> f4.7(A,B,C,D,D) [B + -1*D >= 0 && -1*C + D >= 0 && -1*C >= 0 && B + -1*C >= 0 && -1*A + B >= 0 && D >= A] f4.7(A,B,C,D,E) -> f4.7(A,B,C,D,-1 + E) [D + -1*E >= 0 && B + -1*E >= 0 && -1*C + E >= 0 && B + -1*D >= 0 && -1*C + D >= 0 && -1*A + D >= 0 && -1*C >= 0 && B + -1*C >= 0 && -1*A + B >= 0 && E >= 1] f4.7(A,B,C,D,E) -> f4.8(A,B,C,D,-1 + E) [D + -1*E >= 0 && B + -1*E >= 0 && -1*C + E >= 0 && B + -1*D >= 0 && -1*C + D >= 0 && -1*A + D >= 0 && -1*C >= 0 && B + -1*C >= 0 && -1*A + B >= 0 && E >= 1] f4.8(A,B,C,D,E) -> exitus616.9(A,B,C,D,E) True Signature: {(exitus616.9,5);(f0.0,5);(f1.1,5);(f1.2,5);(f2.3,5);(f2.4,5);(f3.5,5);(f3.6,5);(f4.7,5);(f4.8,5)} Rule Graph: [0->{2,3},1->{4,5},2->{2,3},3->{4,5},4->{6,7},5->{8,9},6->{6,7},7->{8,9},8->{10,11},9->{12},10->{10,11} ,11->{12},12->{13,14},13->{13,14},14->{15},15->{}] + 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] | +- p:[2] c: [2] | +- p:[6] c: [6] | +- p:[10] c: [10] | `- p:[13] c: [13] * Step 5: AbstractSize WORST_CASE(?,POLY) + Considered Problem: (Rules: f0.0(A,B,C,D,E) -> f1.1(A,B,C,D,E) True f0.0(A,B,C,D,E) -> f1.2(A,B,C,D,E) True f1.1(A,B,C,D,E) -> f1.1(A,1 + B,C,D,E) [A >= 1 + B] f1.1(A,B,C,D,E) -> f1.2(A,1 + B,C,D,E) [A >= 1 + B] f1.2(A,B,C,D,E) -> f2.3(A,B,B,D,E) [B >= A] f1.2(A,B,C,D,E) -> f2.4(A,B,B,D,E) [B >= A] f2.3(A,B,C,D,E) -> f2.3(A,B,-1 + C,D,E) [B + -1*C >= 0 && -1*A + B >= 0 && C >= 1] f2.3(A,B,C,D,E) -> f2.4(A,B,-1 + C,D,E) [B + -1*C >= 0 && -1*A + B >= 0 && C >= 1] f2.4(A,B,C,D,E) -> f3.5(A,B,C,C,E) [B + -1*C >= 0 && -1*A + B >= 0 && 0 >= C] f2.4(A,B,C,D,E) -> f3.6(A,B,C,C,E) [B + -1*C >= 0 && -1*A + B >= 0 && 0 >= C] f3.5(A,B,C,D,E) -> f3.5(A,B,C,1 + D,E) [B + -1*D >= 0 && -1*C + D >= 0 && -1*C >= 0 && B + -1*C >= 0 && -1*A + B >= 0 && A >= 1 + D] f3.5(A,B,C,D,E) -> f3.6(A,B,C,1 + D,E) [B + -1*D >= 0 && -1*C + D >= 0 && -1*C >= 0 && B + -1*C >= 0 && -1*A + B >= 0 && A >= 1 + D] f3.6(A,B,C,D,E) -> f4.7(A,B,C,D,D) [B + -1*D >= 0 && -1*C + D >= 0 && -1*C >= 0 && B + -1*C >= 0 && -1*A + B >= 0 && D >= A] f4.7(A,B,C,D,E) -> f4.7(A,B,C,D,-1 + E) [D + -1*E >= 0 && B + -1*E >= 0 && -1*C + E >= 0 && B + -1*D >= 0 && -1*C + D >= 0 && -1*A + D >= 0 && -1*C >= 0 && B + -1*C >= 0 && -1*A + B >= 0 && E >= 1] f4.7(A,B,C,D,E) -> f4.8(A,B,C,D,-1 + E) [D + -1*E >= 0 && B + -1*E >= 0 && -1*C + E >= 0 && B + -1*D >= 0 && -1*C + D >= 0 && -1*A + D >= 0 && -1*C >= 0 && B + -1*C >= 0 && -1*A + B >= 0 && E >= 1] f4.8(A,B,C,D,E) -> exitus616.9(A,B,C,D,E) True Signature: {(exitus616.9,5);(f0.0,5);(f1.1,5);(f1.2,5);(f2.3,5);(f2.4,5);(f3.5,5);(f3.6,5);(f4.7,5);(f4.8,5)} Rule Graph: [0->{2,3},1->{4,5},2->{2,3},3->{4,5},4->{6,7},5->{8,9},6->{6,7},7->{8,9},8->{10,11},9->{12},10->{10,11} ,11->{12},12->{13,14},13->{13,14},14->{15},15->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15] | +- p:[2] c: [2] | +- p:[6] c: [6] | +- p:[10] c: [10] | `- p:[13] c: [13]) + Applied Processor: AbstractSize Minimize + Details: () * Step 6: AbstractFlow WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,C,D,E,0.0,0.1,0.2,0.3] f0.0 ~> f1.1 [A <= A, B <= B, C <= C, D <= D, E <= E] f0.0 ~> f1.2 [A <= A, B <= B, C <= C, D <= D, E <= E] f1.1 ~> f1.1 [A <= A, B <= A + B, C <= C, D <= D, E <= E] f1.1 ~> f1.2 [A <= A, B <= A + B, C <= C, D <= D, E <= E] f1.2 ~> f2.3 [A <= A, B <= B, C <= B, D <= D, E <= E] f1.2 ~> f2.4 [A <= A, B <= B, C <= B, D <= D, E <= E] f2.3 ~> f2.3 [A <= A, B <= B, C <= C, D <= D, E <= E] f2.3 ~> f2.4 [A <= A, B <= B, C <= C, D <= D, E <= E] f2.4 ~> f3.5 [A <= A, B <= B, C <= C, D <= C, E <= E] f2.4 ~> f3.6 [A <= A, B <= B, C <= C, D <= C, E <= E] f3.5 ~> f3.5 [A <= A, B <= B, C <= C, D <= B + D, E <= E] f3.5 ~> f3.6 [A <= A, B <= B, C <= C, D <= B + D, E <= E] f3.6 ~> f4.7 [A <= A, B <= B, C <= C, D <= D, E <= D] f4.7 ~> f4.7 [A <= A, B <= B, C <= C, D <= D, E <= D] f4.7 ~> f4.8 [A <= A, B <= B, C <= C, D <= D, E <= D] f4.8 ~> exitus616.9 [A <= A, B <= B, C <= C, D <= D, E <= E] + Loop: [0.0 <= K + A + B] f1.1 ~> f1.1 [A <= A, B <= A + B, C <= C, D <= D, E <= E] + Loop: [0.1 <= K + C] f2.3 ~> f2.3 [A <= A, B <= B, C <= C, D <= D, E <= E] + Loop: [0.2 <= K + A + D] f3.5 ~> f3.5 [A <= A, B <= B, C <= C, D <= B + D, E <= E] + Loop: [0.3 <= K + E] f4.7 ~> f4.7 [A <= A, B <= B, C <= C, D <= D, E <= D] + Applied Processor: AbstractFlow + Details: () * Step 7: Lare WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,E,0.0,0.1,0.2,0.3] f0.0 ~> f1.1 [] f0.0 ~> f1.2 [] f1.1 ~> f1.1 [A ~+> B,B ~+> B] f1.1 ~> f1.2 [A ~+> B,B ~+> B] f1.2 ~> f2.3 [B ~=> C] f1.2 ~> f2.4 [B ~=> C] f2.3 ~> f2.3 [] f2.3 ~> f2.4 [] f2.4 ~> f3.5 [C ~=> D] f2.4 ~> f3.6 [C ~=> D] f3.5 ~> f3.5 [B ~+> D,D ~+> D] f3.5 ~> f3.6 [B ~+> D,D ~+> D] f3.6 ~> f4.7 [D ~=> E] f4.7 ~> f4.7 [D ~=> E] f4.7 ~> f4.8 [D ~=> E] f4.8 ~> exitus616.9 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~+> 0.0] f1.1 ~> f1.1 [A ~+> B,B ~+> B] + Loop: [C ~+> 0.1,K ~+> 0.1] f2.3 ~> f2.3 [] + Loop: [A ~+> 0.2,D ~+> 0.2,K ~+> 0.2] f3.5 ~> f3.5 [B ~+> D,D ~+> D] + Loop: [E ~+> 0.3,K ~+> 0.3] f4.7 ~> f4.7 [D ~=> E] + Applied Processor: Lare + Details: f0.0 ~> exitus616.9 [B ~=> C ,B ~=> D ,B ~=> E ,A ~+> B ,A ~+> C ,A ~+> D ,A ~+> E ,A ~+> 0.0 ,A ~+> 0.1 ,A ~+> 0.2 ,A ~+> 0.3 ,A ~+> tick ,B ~+> B ,B ~+> C ,B ~+> D ,B ~+> E ,B ~+> 0.0 ,B ~+> 0.1 ,B ~+> 0.2 ,B ~+> 0.3 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> 0.2 ,K ~+> 0.3 ,K ~+> tick ,A ~*> B ,A ~*> C ,A ~*> D ,A ~*> E ,A ~*> 0.1 ,A ~*> 0.2 ,A ~*> 0.3 ,A ~*> tick ,B ~*> B ,B ~*> C ,B ~*> D ,B ~*> E ,B ~*> 0.1 ,B ~*> 0.2 ,B ~*> 0.3 ,B ~*> tick ,K ~*> B ,K ~*> C ,K ~*> D ,K ~*> E ,K ~*> 0.1 ,K ~*> 0.2 ,K ~*> 0.3 ,K ~*> tick] + f1.1> [A ~+> B ,A ~+> 0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> tick ,A ~*> B ,B ~*> B ,K ~*> B] + f2.3> [C ~+> 0.1,C ~+> tick,tick ~+> tick,K ~+> 0.1,K ~+> tick] + f3.5> [A ~+> 0.2 ,A ~+> tick ,B ~+> D ,D ~+> D ,D ~+> 0.2 ,D ~+> tick ,tick ~+> tick ,K ~+> 0.2 ,K ~+> tick ,A ~*> D ,B ~*> D ,D ~*> D ,K ~*> D] + f4.7> [D ~=> E,E ~+> 0.3,E ~+> tick,tick ~+> tick,K ~+> 0.3,K ~+> tick] YES(?,POLY)