YES(?,POLY) * Step 1: TrivialSCCs WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J) -> f17(0,K,L,0,E,F,G,H,I,J) True (1,1) 1. f17(A,B,C,D,E,F,G,H,I,J) -> f17(A,B,C,1 + D,E,F,G,H,I,J) [D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && E >= 1 + D] (?,1) 2. f27(A,B,C,D,E,F,G,H,I,J) -> f27(A,B,C,D,E,-1 + F,G,H,I,J) [-1 + E + -1*F >= 0 (?,1) && -1 + D + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && F >= 0] 3. f37(A,B,C,D,E,F,G,H,I,J) -> f37(A,B,C,D,E,F,1 + G,H,I,J) [D + -1*G >= 0 (?,1) && G >= 0 && -1 + -1*F + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && -1 + -1*A + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && E >= 1 + G] 4. f45(A,B,C,D,E,F,G,H,I,J) -> f45(1 + A,B,C,D,E,F,G,H,I,J) [D + -1*G >= 0 (?,1) && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && E >= 1 + A] 5. f55(A,B,C,D,E,F,G,H,I,J) -> f55(A,B,C,D,E,F,G,1 + H,I,J) [G + -1*H >= 0 (?,1) && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && D + H >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && E >= 1 + H] 6. f65(A,B,C,D,E,F,G,H,I,J) -> f65(A,B,C,D,E,F,G,H,-1 + I,J) [-1 + H + -1*I >= 0 (?,1) && -1 + G + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && I >= 0] 7. f75(A,B,C,D,E,F,G,H,I,J) -> f75(A,B,C,D,E,F,G,H,I,1 + J) [-1 + -1*I >= 0 (?,1) && -1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -2 + -1*F + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + -1*I + J >= 0 && -1 + A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && H + J >= 0 && H + -1*J >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && G + J >= 0 && G + -1*J >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + -1*F + J >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && D + J >= 0 && D + -1*J >= 0 && A + D >= 0 && -1*A + D >= 0 && A + -1*J >= 0 && J >= 0 && A + J >= 0 && A >= 0 && E >= 1 + J] 8. f83(A,B,C,D,E,F,G,H,I,J) -> f83(-1 + A,B,C,D,E,F,G,H,I,J) [-1 + -1*I >= 0 (?,1) && -1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -2 + -1*F + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + -1*I + J >= 0 && A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && H + J >= 0 && H + -1*J >= 0 && -1 + -1*A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && G + J >= 0 && G + -1*J >= 0 && -1 + -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + -1*F + J >= 0 && A + -1*F >= 0 && D + -1*E >= 0 && -1*E + J >= 0 && -1 + -1*A + E >= 0 && D >= 0 && D + J >= 0 && D + -1*J >= 0 && -1 + -1*A + D >= 0 && J >= 0 && -1 + -1*A + J >= 0 && A >= 0] 9. f83(A,B,C,D,E,F,G,H,I,J) -> f93(A,B,C,D,E,F,G,H,I,J) [-1 + -1*I >= 0 (?,1) && -1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -2 + -1*F + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + -1*I + J >= 0 && A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && H + J >= 0 && H + -1*J >= 0 && -1 + -1*A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && G + J >= 0 && G + -1*J >= 0 && -1 + -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + -1*F + J >= 0 && A + -1*F >= 0 && D + -1*E >= 0 && -1*E + J >= 0 && -1 + -1*A + E >= 0 && D >= 0 && D + J >= 0 && D + -1*J >= 0 && -1 + -1*A + D >= 0 && J >= 0 && -1 + -1*A + J >= 0 && 0 >= 1 + A] 10. f75(A,B,C,D,E,F,G,H,I,J) -> f83(-1 + E,B,C,D,E,F,G,H,I,J) [-1 + -1*I >= 0 (?,1) && -1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -2 + -1*F + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + -1*I + J >= 0 && -1 + A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && H + J >= 0 && H + -1*J >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && G + J >= 0 && G + -1*J >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + -1*F + J >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && D + J >= 0 && D + -1*J >= 0 && A + D >= 0 && -1*A + D >= 0 && A + -1*J >= 0 && J >= 0 && A + J >= 0 && A >= 0 && J >= E] 11. f65(A,B,C,D,E,F,G,H,I,J) -> f75(A,B,C,D,E,F,G,H,I,0) [-1 + H + -1*I >= 0 (?,1) && -1 + G + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && 0 >= 1 + I] 12. f55(A,B,C,D,E,F,G,H,I,J) -> f65(A,B,C,D,E,F,G,H,-1 + E,J) [G + -1*H >= 0 (?,1) && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && D + H >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && H >= E] 13. f45(A,B,C,D,E,F,G,H,I,J) -> f55(A,B,C,D,E,F,G,0,I,J) [D + -1*G >= 0 (?,1) && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && A >= E] 14. f37(A,B,C,D,E,F,G,H,I,J) -> f45(0,B,C,D,E,F,G,H,I,J) [D + -1*G >= 0 (?,1) && G >= 0 && -1 + -1*F + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && -1 + -1*A + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && G >= E] 15. f27(A,B,C,D,E,F,G,H,I,J) -> f37(A,B,C,D,E,F,0,H,I,J) [-1 + E + -1*F >= 0 (?,1) && -1 + D + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 0 >= 1 + F] 16. f17(A,B,C,D,E,F,G,H,I,J) -> f27(A,B,C,D,E,-1 + E,G,H,I,J) [D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && D >= E] (?,1) Signature: {(f0,10);(f17,10);(f27,10);(f37,10);(f45,10);(f55,10);(f65,10);(f75,10);(f83,10);(f93,10)} Flow Graph: [0->{1,16},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8,9},9->{},10->{8,9} ,11->{7,10},12->{6,11},13->{5,12},14->{4,13},15->{3,14},16->{2,15}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J) -> f17(0,K,L,0,E,F,G,H,I,J) True (1,1) 1. f17(A,B,C,D,E,F,G,H,I,J) -> f17(A,B,C,1 + D,E,F,G,H,I,J) [D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && E >= 1 + D] (?,1) 2. f27(A,B,C,D,E,F,G,H,I,J) -> f27(A,B,C,D,E,-1 + F,G,H,I,J) [-1 + E + -1*F >= 0 (?,1) && -1 + D + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && F >= 0] 3. f37(A,B,C,D,E,F,G,H,I,J) -> f37(A,B,C,D,E,F,1 + G,H,I,J) [D + -1*G >= 0 (?,1) && G >= 0 && -1 + -1*F + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && -1 + -1*A + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && E >= 1 + G] 4. f45(A,B,C,D,E,F,G,H,I,J) -> f45(1 + A,B,C,D,E,F,G,H,I,J) [D + -1*G >= 0 (?,1) && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && E >= 1 + A] 5. f55(A,B,C,D,E,F,G,H,I,J) -> f55(A,B,C,D,E,F,G,1 + H,I,J) [G + -1*H >= 0 (?,1) && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && D + H >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && E >= 1 + H] 6. f65(A,B,C,D,E,F,G,H,I,J) -> f65(A,B,C,D,E,F,G,H,-1 + I,J) [-1 + H + -1*I >= 0 (?,1) && -1 + G + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && I >= 0] 7. f75(A,B,C,D,E,F,G,H,I,J) -> f75(A,B,C,D,E,F,G,H,I,1 + J) [-1 + -1*I >= 0 (?,1) && -1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -2 + -1*F + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + -1*I + J >= 0 && -1 + A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && H + J >= 0 && H + -1*J >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && G + J >= 0 && G + -1*J >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + -1*F + J >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && D + J >= 0 && D + -1*J >= 0 && A + D >= 0 && -1*A + D >= 0 && A + -1*J >= 0 && J >= 0 && A + J >= 0 && A >= 0 && E >= 1 + J] 8. f83(A,B,C,D,E,F,G,H,I,J) -> f83(-1 + A,B,C,D,E,F,G,H,I,J) [-1 + -1*I >= 0 (?,1) && -1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -2 + -1*F + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + -1*I + J >= 0 && A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && H + J >= 0 && H + -1*J >= 0 && -1 + -1*A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && G + J >= 0 && G + -1*J >= 0 && -1 + -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + -1*F + J >= 0 && A + -1*F >= 0 && D + -1*E >= 0 && -1*E + J >= 0 && -1 + -1*A + E >= 0 && D >= 0 && D + J >= 0 && D + -1*J >= 0 && -1 + -1*A + D >= 0 && J >= 0 && -1 + -1*A + J >= 0 && A >= 0] 9. f83(A,B,C,D,E,F,G,H,I,J) -> f93(A,B,C,D,E,F,G,H,I,J) [-1 + -1*I >= 0 (1,1) && -1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -2 + -1*F + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + -1*I + J >= 0 && A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && H + J >= 0 && H + -1*J >= 0 && -1 + -1*A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && G + J >= 0 && G + -1*J >= 0 && -1 + -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + -1*F + J >= 0 && A + -1*F >= 0 && D + -1*E >= 0 && -1*E + J >= 0 && -1 + -1*A + E >= 0 && D >= 0 && D + J >= 0 && D + -1*J >= 0 && -1 + -1*A + D >= 0 && J >= 0 && -1 + -1*A + J >= 0 && 0 >= 1 + A] 10. f75(A,B,C,D,E,F,G,H,I,J) -> f83(-1 + E,B,C,D,E,F,G,H,I,J) [-1 + -1*I >= 0 (1,1) && -1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -2 + -1*F + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + -1*I + J >= 0 && -1 + A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && H + J >= 0 && H + -1*J >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && G + J >= 0 && G + -1*J >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + -1*F + J >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && D + J >= 0 && D + -1*J >= 0 && A + D >= 0 && -1*A + D >= 0 && A + -1*J >= 0 && J >= 0 && A + J >= 0 && A >= 0 && J >= E] 11. f65(A,B,C,D,E,F,G,H,I,J) -> f75(A,B,C,D,E,F,G,H,I,0) [-1 + H + -1*I >= 0 (1,1) && -1 + G + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && 0 >= 1 + I] 12. f55(A,B,C,D,E,F,G,H,I,J) -> f65(A,B,C,D,E,F,G,H,-1 + E,J) [G + -1*H >= 0 (1,1) && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && D + H >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && H >= E] 13. f45(A,B,C,D,E,F,G,H,I,J) -> f55(A,B,C,D,E,F,G,0,I,J) [D + -1*G >= 0 (1,1) && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && A >= E] 14. f37(A,B,C,D,E,F,G,H,I,J) -> f45(0,B,C,D,E,F,G,H,I,J) [D + -1*G >= 0 (1,1) && G >= 0 && -1 + -1*F + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && -1 + -1*A + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && G >= E] 15. f27(A,B,C,D,E,F,G,H,I,J) -> f37(A,B,C,D,E,F,0,H,I,J) [-1 + E + -1*F >= 0 (1,1) && -1 + D + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 0 >= 1 + F] 16. f17(A,B,C,D,E,F,G,H,I,J) -> f27(A,B,C,D,E,-1 + E,G,H,I,J) [D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && D >= E] (1,1) Signature: {(f0,10);(f17,10);(f27,10);(f37,10);(f45,10);(f55,10);(f65,10);(f75,10);(f83,10);(f93,10)} Flow Graph: [0->{1,16},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8,9},9->{},10->{8,9} ,11->{7,10},12->{6,11},13->{5,12},14->{4,13},15->{3,14},16->{2,15}] + Applied Processor: AddSinks + Details: () * Step 3: LooptreeTransformer WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J) -> f17(0,K,L,0,E,F,G,H,I,J) True (1,1) 1. f17(A,B,C,D,E,F,G,H,I,J) -> f17(A,B,C,1 + D,E,F,G,H,I,J) [D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && E >= 1 + D] (?,1) 2. f27(A,B,C,D,E,F,G,H,I,J) -> f27(A,B,C,D,E,-1 + F,G,H,I,J) [-1 + E + -1*F >= 0 (?,1) && -1 + D + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && F >= 0] 3. f37(A,B,C,D,E,F,G,H,I,J) -> f37(A,B,C,D,E,F,1 + G,H,I,J) [D + -1*G >= 0 (?,1) && G >= 0 && -1 + -1*F + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && -1 + -1*A + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && E >= 1 + G] 4. f45(A,B,C,D,E,F,G,H,I,J) -> f45(1 + A,B,C,D,E,F,G,H,I,J) [D + -1*G >= 0 (?,1) && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && E >= 1 + A] 5. f55(A,B,C,D,E,F,G,H,I,J) -> f55(A,B,C,D,E,F,G,1 + H,I,J) [G + -1*H >= 0 (?,1) && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && D + H >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && E >= 1 + H] 6. f65(A,B,C,D,E,F,G,H,I,J) -> f65(A,B,C,D,E,F,G,H,-1 + I,J) [-1 + H + -1*I >= 0 (?,1) && -1 + G + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && I >= 0] 7. f75(A,B,C,D,E,F,G,H,I,J) -> f75(A,B,C,D,E,F,G,H,I,1 + J) [-1 + -1*I >= 0 (?,1) && -1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -2 + -1*F + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + -1*I + J >= 0 && -1 + A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && H + J >= 0 && H + -1*J >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && G + J >= 0 && G + -1*J >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + -1*F + J >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && D + J >= 0 && D + -1*J >= 0 && A + D >= 0 && -1*A + D >= 0 && A + -1*J >= 0 && J >= 0 && A + J >= 0 && A >= 0 && E >= 1 + J] 8. f83(A,B,C,D,E,F,G,H,I,J) -> f83(-1 + A,B,C,D,E,F,G,H,I,J) [-1 + -1*I >= 0 (?,1) && -1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -2 + -1*F + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + -1*I + J >= 0 && A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && H + J >= 0 && H + -1*J >= 0 && -1 + -1*A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && G + J >= 0 && G + -1*J >= 0 && -1 + -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + -1*F + J >= 0 && A + -1*F >= 0 && D + -1*E >= 0 && -1*E + J >= 0 && -1 + -1*A + E >= 0 && D >= 0 && D + J >= 0 && D + -1*J >= 0 && -1 + -1*A + D >= 0 && J >= 0 && -1 + -1*A + J >= 0 && A >= 0] 9. f83(A,B,C,D,E,F,G,H,I,J) -> f93(A,B,C,D,E,F,G,H,I,J) [-1 + -1*I >= 0 (?,1) && -1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -2 + -1*F + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + -1*I + J >= 0 && A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && H + J >= 0 && H + -1*J >= 0 && -1 + -1*A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && G + J >= 0 && G + -1*J >= 0 && -1 + -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + -1*F + J >= 0 && A + -1*F >= 0 && D + -1*E >= 0 && -1*E + J >= 0 && -1 + -1*A + E >= 0 && D >= 0 && D + J >= 0 && D + -1*J >= 0 && -1 + -1*A + D >= 0 && J >= 0 && -1 + -1*A + J >= 0 && 0 >= 1 + A] 10. f75(A,B,C,D,E,F,G,H,I,J) -> f83(-1 + E,B,C,D,E,F,G,H,I,J) [-1 + -1*I >= 0 (?,1) && -1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -2 + -1*F + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + -1*I + J >= 0 && -1 + A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && H + J >= 0 && H + -1*J >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && G + J >= 0 && G + -1*J >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + -1*F + J >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && D + J >= 0 && D + -1*J >= 0 && A + D >= 0 && -1*A + D >= 0 && A + -1*J >= 0 && J >= 0 && A + J >= 0 && A >= 0 && J >= E] 11. f65(A,B,C,D,E,F,G,H,I,J) -> f75(A,B,C,D,E,F,G,H,I,0) [-1 + H + -1*I >= 0 (?,1) && -1 + G + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && 0 >= 1 + I] 12. f55(A,B,C,D,E,F,G,H,I,J) -> f65(A,B,C,D,E,F,G,H,-1 + E,J) [G + -1*H >= 0 (?,1) && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && D + H >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && H >= E] 13. f45(A,B,C,D,E,F,G,H,I,J) -> f55(A,B,C,D,E,F,G,0,I,J) [D + -1*G >= 0 (?,1) && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && A >= E] 14. f37(A,B,C,D,E,F,G,H,I,J) -> f45(0,B,C,D,E,F,G,H,I,J) [D + -1*G >= 0 (?,1) && G >= 0 && -1 + -1*F + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && -1 + -1*A + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && G >= E] 15. f27(A,B,C,D,E,F,G,H,I,J) -> f37(A,B,C,D,E,F,0,H,I,J) [-1 + E + -1*F >= 0 (?,1) && -1 + D + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 0 >= 1 + F] 16. f17(A,B,C,D,E,F,G,H,I,J) -> f27(A,B,C,D,E,-1 + E,G,H,I,J) [D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && D >= E] (?,1) 17. f83(A,B,C,D,E,F,G,H,I,J) -> exitus616(A,B,C,D,E,F,G,H,I,J) True (?,1) Signature: {(exitus616,10);(f0,10);(f17,10);(f27,10);(f37,10);(f45,10);(f55,10);(f65,10);(f75,10);(f83,10);(f93,10)} Flow Graph: [0->{1,16},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8,9,17},9->{},10->{8 ,9,17},11->{7,10},12->{6,11},13->{5,12},14->{4,13},15->{3,14},16->{2,15},17->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17] | +- p:[1] c: [1] | +- p:[2] c: [2] | +- p:[3] c: [3] | +- p:[4] c: [4] | +- p:[5] c: [5] | +- p:[6] c: [6] | +- p:[7] c: [7] | `- p:[8] c: [8] * Step 4: SizeAbstraction WORST_CASE(?,POLY) + Considered Problem: (Rules: 0. f0(A,B,C,D,E,F,G,H,I,J) -> f17(0,K,L,0,E,F,G,H,I,J) True (1,1) 1. f17(A,B,C,D,E,F,G,H,I,J) -> f17(A,B,C,1 + D,E,F,G,H,I,J) [D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && E >= 1 + D] (?,1) 2. f27(A,B,C,D,E,F,G,H,I,J) -> f27(A,B,C,D,E,-1 + F,G,H,I,J) [-1 + E + -1*F >= 0 (?,1) && -1 + D + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && F >= 0] 3. f37(A,B,C,D,E,F,G,H,I,J) -> f37(A,B,C,D,E,F,1 + G,H,I,J) [D + -1*G >= 0 (?,1) && G >= 0 && -1 + -1*F + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && -1 + -1*A + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && E >= 1 + G] 4. f45(A,B,C,D,E,F,G,H,I,J) -> f45(1 + A,B,C,D,E,F,G,H,I,J) [D + -1*G >= 0 (?,1) && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && E >= 1 + A] 5. f55(A,B,C,D,E,F,G,H,I,J) -> f55(A,B,C,D,E,F,G,1 + H,I,J) [G + -1*H >= 0 (?,1) && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && D + H >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && E >= 1 + H] 6. f65(A,B,C,D,E,F,G,H,I,J) -> f65(A,B,C,D,E,F,G,H,-1 + I,J) [-1 + H + -1*I >= 0 (?,1) && -1 + G + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && I >= 0] 7. f75(A,B,C,D,E,F,G,H,I,J) -> f75(A,B,C,D,E,F,G,H,I,1 + J) [-1 + -1*I >= 0 (?,1) && -1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -2 + -1*F + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + -1*I + J >= 0 && -1 + A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && H + J >= 0 && H + -1*J >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && G + J >= 0 && G + -1*J >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + -1*F + J >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && D + J >= 0 && D + -1*J >= 0 && A + D >= 0 && -1*A + D >= 0 && A + -1*J >= 0 && J >= 0 && A + J >= 0 && A >= 0 && E >= 1 + J] 8. f83(A,B,C,D,E,F,G,H,I,J) -> f83(-1 + A,B,C,D,E,F,G,H,I,J) [-1 + -1*I >= 0 (?,1) && -1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -2 + -1*F + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + -1*I + J >= 0 && A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && H + J >= 0 && H + -1*J >= 0 && -1 + -1*A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && G + J >= 0 && G + -1*J >= 0 && -1 + -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + -1*F + J >= 0 && A + -1*F >= 0 && D + -1*E >= 0 && -1*E + J >= 0 && -1 + -1*A + E >= 0 && D >= 0 && D + J >= 0 && D + -1*J >= 0 && -1 + -1*A + D >= 0 && J >= 0 && -1 + -1*A + J >= 0 && A >= 0] 9. f83(A,B,C,D,E,F,G,H,I,J) -> f93(A,B,C,D,E,F,G,H,I,J) [-1 + -1*I >= 0 (?,1) && -1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -2 + -1*F + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + -1*I + J >= 0 && A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && H + J >= 0 && H + -1*J >= 0 && -1 + -1*A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && G + J >= 0 && G + -1*J >= 0 && -1 + -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + -1*F + J >= 0 && A + -1*F >= 0 && D + -1*E >= 0 && -1*E + J >= 0 && -1 + -1*A + E >= 0 && D >= 0 && D + J >= 0 && D + -1*J >= 0 && -1 + -1*A + D >= 0 && J >= 0 && -1 + -1*A + J >= 0 && 0 >= 1 + A] 10. f75(A,B,C,D,E,F,G,H,I,J) -> f83(-1 + E,B,C,D,E,F,G,H,I,J) [-1 + -1*I >= 0 (?,1) && -1 + H + -1*I >= 0 && -1 + G + -1*I >= 0 && -2 + -1*F + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + -1*I + J >= 0 && -1 + A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && H + J >= 0 && H + -1*J >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && G + J >= 0 && G + -1*J >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + -1*F + J >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && D + J >= 0 && D + -1*J >= 0 && A + D >= 0 && -1*A + D >= 0 && A + -1*J >= 0 && J >= 0 && A + J >= 0 && A >= 0 && J >= E] 11. f65(A,B,C,D,E,F,G,H,I,J) -> f75(A,B,C,D,E,F,G,H,I,0) [-1 + H + -1*I >= 0 (?,1) && -1 + G + -1*I >= 0 && -1 + E + -1*I >= 0 && -1 + D + -1*I >= 0 && -1 + A + -1*I >= 0 && -1*F + I >= 0 && G + -1*H >= 0 && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && -1*E + H >= 0 && D + H >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && 0 >= 1 + I] 12. f55(A,B,C,D,E,F,G,H,I,J) -> f65(A,B,C,D,E,F,G,H,-1 + E,J) [G + -1*H >= 0 (?,1) && D + -1*H >= 0 && A + -1*H >= 0 && H >= 0 && G + H >= 0 && -1 + -1*F + H >= 0 && D + H >= 0 && A + H >= 0 && D + -1*G >= 0 && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && A + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && H >= E] 13. f45(A,B,C,D,E,F,G,H,I,J) -> f55(A,B,C,D,E,F,G,0,I,J) [D + -1*G >= 0 (?,1) && G >= 0 && -1 + -1*F + G >= 0 && -1*E + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && A >= 0 && A >= E] 14. f37(A,B,C,D,E,F,G,H,I,J) -> f45(0,B,C,D,E,F,G,H,I,J) [D + -1*G >= 0 (?,1) && G >= 0 && -1 + -1*F + G >= 0 && D + G >= 0 && A + G >= 0 && -1*A + G >= 0 && -1 + -1*F >= 0 && -1 + E + -1*F >= 0 && -1 + D + -1*F >= 0 && -1 + A + -1*F >= 0 && -1 + -1*A + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && G >= E] 15. f27(A,B,C,D,E,F,G,H,I,J) -> f37(A,B,C,D,E,F,0,H,I,J) [-1 + E + -1*F >= 0 (?,1) && -1 + D + -1*F >= 0 && D + -1*E >= 0 && D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 0 >= 1 + F] 16. f17(A,B,C,D,E,F,G,H,I,J) -> f27(A,B,C,D,E,-1 + E,G,H,I,J) [D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && D >= E] (?,1) 17. f83(A,B,C,D,E,F,G,H,I,J) -> exitus616(A,B,C,D,E,F,G,H,I,J) True (?,1) Signature: {(exitus616,10);(f0,10);(f17,10);(f27,10);(f37,10);(f45,10);(f55,10);(f65,10);(f75,10);(f83,10);(f93,10)} Flow Graph: [0->{1,16},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8,9,17},9->{},10->{8 ,9,17},11->{7,10},12->{6,11},13->{5,12},14->{4,13},15->{3,14},16->{2,15},17->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17] | +- p:[1] c: [1] | +- p:[2] c: [2] | +- p:[3] c: [3] | +- p:[4] c: [4] | +- p:[5] c: [5] | +- p:[6] c: [6] | +- p:[7] c: [7] | `- p:[8] c: [8]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 5: FlowAbstraction WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,C,D,E,F,G,H,I,J,0.0,0.1,0.2,0.3,0.4,0.5,0.6,0.7] f0 ~> f17 [A <= 0*K, B <= unknown, C <= unknown, D <= 0*K, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] f17 ~> f17 [A <= A, B <= B, C <= C, D <= E, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] f27 ~> f27 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= E, G <= G, H <= H, I <= I, J <= J] f37 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= D, H <= H, I <= I, J <= J] f45 ~> f45 [A <= G, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] f55 ~> f55 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= D, I <= I, J <= J] f65 ~> f65 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= E, J <= J] f75 ~> f75 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= G] f83 ~> f83 [A <= H, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] f83 ~> f93 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] f75 ~> f83 [A <= A + I, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] f65 ~> f75 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= 0*K] f55 ~> f65 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= F + G, J <= J] f45 ~> f55 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= 0*K, I <= I, J <= J] f37 ~> f45 [A <= 0*K, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] f27 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= 0*K, H <= H, I <= I, J <= J] f17 ~> f27 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= K + E, G <= G, H <= H, I <= I, J <= J] f83 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] + Loop: [0.0 <= D + E] f17 ~> f17 [A <= A, B <= B, C <= C, D <= E, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] + Loop: [0.1 <= K + F] f27 ~> f27 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= E, G <= G, H <= H, I <= I, J <= J] + Loop: [0.2 <= E + G] f37 ~> f37 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= D, H <= H, I <= I, J <= J] + Loop: [0.3 <= A + E] f45 ~> f45 [A <= G, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] + Loop: [0.4 <= K + G + H] f55 ~> f55 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= D, I <= I, J <= J] + Loop: [0.5 <= K + I] f65 ~> f65 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= E, J <= J] + Loop: [0.6 <= K + H + J] f75 ~> f75 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= G] + Loop: [0.7 <= K + A] f83 ~> f83 [A <= H, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] + Applied Processor: FlowAbstraction + Details: () * Step 6: LareProcessor WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,E,F,G,H,I,J,0.0,0.1,0.2,0.3,0.4,0.5,0.6,0.7] f0 ~> f17 [K ~=> A,K ~=> D,huge ~=> B,huge ~=> C] f17 ~> f17 [E ~=> D] f27 ~> f27 [E ~=> F] f37 ~> f37 [D ~=> G] f45 ~> f45 [G ~=> A] f55 ~> f55 [D ~=> H] f65 ~> f65 [E ~=> I] f75 ~> f75 [G ~=> J] f83 ~> f83 [H ~=> A] f83 ~> f93 [] f75 ~> f83 [A ~+> A,I ~+> A] f65 ~> f75 [K ~=> J] f55 ~> f65 [F ~+> I,G ~+> I] f45 ~> f55 [K ~=> H] f37 ~> f45 [K ~=> A] f27 ~> f37 [K ~=> G] f17 ~> f27 [E ~+> F,K ~+> F] f83 ~> exitus616 [] + Loop: [D ~+> 0.0,E ~+> 0.0] f17 ~> f17 [E ~=> D] + Loop: [F ~+> 0.1,K ~+> 0.1] f27 ~> f27 [E ~=> F] + Loop: [E ~+> 0.2,G ~+> 0.2] f37 ~> f37 [D ~=> G] + Loop: [A ~+> 0.3,E ~+> 0.3] f45 ~> f45 [G ~=> A] + Loop: [G ~+> 0.4,H ~+> 0.4,K ~+> 0.4] f55 ~> f55 [D ~=> H] + Loop: [I ~+> 0.5,K ~+> 0.5] f65 ~> f65 [E ~=> I] + Loop: [H ~+> 0.6,J ~+> 0.6,K ~+> 0.6] f75 ~> f75 [G ~=> J] + Loop: [A ~+> 0.7,K ~+> 0.7] f83 ~> f83 [H ~=> A] + Applied Processor: LareProcessor + Details: f0 ~> f93 [E ~=> A ,E ~=> D ,E ~=> F ,E ~=> G ,E ~=> H ,E ~=> I ,E ~=> J ,K ~=> A ,K ~=> D ,K ~=> G ,K ~=> H ,K ~=> J ,huge ~=> B ,huge ~=> C ,E ~+> A ,E ~+> F ,E ~+> I ,E ~+> 0.0 ,E ~+> 0.1 ,E ~+> 0.2 ,E ~+> 0.3 ,E ~+> 0.4 ,E ~+> 0.5 ,E ~+> 0.6 ,E ~+> 0.7 ,E ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> F ,K ~+> I ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> 0.2 ,K ~+> 0.3 ,K ~+> 0.4 ,K ~+> 0.5 ,K ~+> 0.6 ,K ~+> 0.7 ,K ~+> tick ,E ~*> A ,E ~*> I ,E ~*> 0.5 ,E ~*> 0.7 ,E ~*> tick ,K ~*> A ,K ~*> I ,K ~*> 0.1 ,K ~*> 0.4 ,K ~*> 0.5 ,K ~*> 0.6 ,K ~*> 0.7 ,K ~*> tick] f0 ~> exitus616 [E ~=> A ,E ~=> D ,E ~=> F ,E ~=> G ,E ~=> H ,E ~=> I ,E ~=> J ,K ~=> A ,K ~=> D ,K ~=> G ,K ~=> H ,K ~=> J ,huge ~=> B ,huge ~=> C ,E ~+> A ,E ~+> F ,E ~+> I ,E ~+> 0.0 ,E ~+> 0.1 ,E ~+> 0.2 ,E ~+> 0.3 ,E ~+> 0.4 ,E ~+> 0.5 ,E ~+> 0.6 ,E ~+> 0.7 ,E ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> F ,K ~+> I ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> 0.2 ,K ~+> 0.3 ,K ~+> 0.4 ,K ~+> 0.5 ,K ~+> 0.6 ,K ~+> 0.7 ,K ~+> tick ,E ~*> A ,E ~*> I ,E ~*> 0.5 ,E ~*> 0.7 ,E ~*> tick ,K ~*> A ,K ~*> I ,K ~*> 0.1 ,K ~*> 0.4 ,K ~*> 0.5 ,K ~*> 0.6 ,K ~*> 0.7 ,K ~*> tick] + f17> [E ~=> D,D ~+> 0.0,D ~+> tick,E ~+> 0.0,E ~+> tick,tick ~+> tick] + f27> [E ~=> F,F ~+> 0.1,F ~+> tick,tick ~+> tick,K ~+> 0.1,K ~+> tick] + f37> [D ~=> G,E ~+> 0.2,E ~+> tick,G ~+> 0.2,G ~+> tick,tick ~+> tick] + f45> [G ~=> A,A ~+> 0.3,A ~+> tick,E ~+> 0.3,E ~+> tick,tick ~+> tick] + f55> [D ~=> H,G ~+> 0.4,G ~+> tick,H ~+> 0.4,H ~+> tick,tick ~+> tick,K ~+> 0.4,K ~+> tick] + f65> [E ~=> I,I ~+> 0.5,I ~+> tick,tick ~+> tick,K ~+> 0.5,K ~+> tick] + f75> [G ~=> J,H ~+> 0.6,H ~+> tick,J ~+> 0.6,J ~+> tick,tick ~+> tick,K ~+> 0.6,K ~+> tick] + f83> [H ~=> A,A ~+> 0.7,A ~+> tick,tick ~+> tick,K ~+> 0.7,K ~+> tick] YES(?,POLY)