(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS evalwhile2start)) (VAR A B C) (RULES evalwhile2start(A, B, C) -> Com_1(evalwhile2entryin(A, B, C)) evalwhile2entryin(A, B, C) -> Com_1(evalwhile2bb4in(B, B, C)) evalwhile2bb4in(A, B, C) -> Com_1(evalwhile2bb2in(A, B, B)) [ -A + B >= 0 /\ A >= 1 ] evalwhile2bb4in(A, B, C) -> Com_1(evalwhile2returnin(A, B, C)) [ -A + B >= 0 /\ 0 >= A ] evalwhile2bb2in(A, B, C) -> Com_1(evalwhile2bb1in(A, B, C)) [ B - C >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ A - 1 >= 0 /\ C >= 1 ] evalwhile2bb2in(A, B, C) -> Com_1(evalwhile2bb3in(A, B, C)) [ B - C >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ A - 1 >= 0 /\ 0 >= C ] evalwhile2bb1in(A, B, C) -> Com_1(evalwhile2bb2in(A, B, C - 1)) [ B - C >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ A + C - 2 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ A - 1 >= 0 ] evalwhile2bb3in(A, B, C) -> Com_1(evalwhile2bb4in(A - 1, B, C)) [ -C >= 0 /\ B - C - 1 >= 0 /\ A - C - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ A - 1 >= 0 ] evalwhile2returnin(A, B, C) -> Com_1(evalwhile2stop(A, B, C)) [ -A + B >= 0 /\ -A >= 0 ] )