(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS evalfstart)) (VAR A B) (RULES evalfstart(A, B) -> Com_1(evalfentryin(A, B)) evalfentryin(A, B) -> Com_1(evalfbb3in(B, A)) evalfbb3in(A, B) -> Com_1(evalfbbin(A, B)) [ B >= 1 /\ 254 >= B ] evalfbb3in(A, B) -> Com_1(evalfreturnin(A, B)) [ 0 >= B ] evalfbb3in(A, B) -> Com_1(evalfreturnin(A, B)) [ B >= 255 ] evalfbbin(A, B) -> Com_1(evalfbb1in(A, B)) [ -B + 254 >= 0 /\ B - 1 >= 0 /\ 0 >= A + 1 ] evalfbbin(A, B) -> Com_1(evalfbb1in(A, B)) [ -B + 254 >= 0 /\ B - 1 >= 0 /\ A >= 1 ] evalfbbin(A, B) -> Com_1(evalfbb2in(A, B)) [ -B + 254 >= 0 /\ B - 1 >= 0 /\ A = 0 ] evalfbb1in(A, B) -> Com_1(evalfbb3in(A, B + 1)) [ -B + 254 >= 0 /\ B - 1 >= 0 ] evalfbb2in(A, B) -> Com_1(evalfbb3in(A, B - 1)) [ -B + 254 >= 0 /\ A - B + 254 >= 0 /\ -A - B + 254 >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ -A >= 0 /\ A >= 0 ] evalfreturnin(A, B) -> Com_1(evalfstop(A, B)) )