(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS evalSequentialSinglestart)) (VAR A B) (RULES evalSequentialSinglestart(A, B) -> Com_1(evalSequentialSingleentryin(A, B)) evalSequentialSingleentryin(A, B) -> Com_1(evalSequentialSinglebb1in(0, B)) evalSequentialSinglebb1in(A, B) -> Com_1(evalSequentialSinglebb5in(A, B)) [ A >= 0 /\ A >= B ] evalSequentialSinglebb1in(A, B) -> Com_1(evalSequentialSinglebb2in(A, B)) [ A >= 0 /\ B >= A + 1 ] evalSequentialSinglebb2in(A, B) -> Com_1(evalSequentialSinglebbin(A, B)) [ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ 0 >= C + 1 ] evalSequentialSinglebb2in(A, B) -> Com_1(evalSequentialSinglebbin(A, B)) [ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ C >= 1 ] evalSequentialSinglebb2in(A, B) -> Com_1(evalSequentialSinglebb5in(A, B)) [ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 ] evalSequentialSinglebbin(A, B) -> Com_1(evalSequentialSinglebb1in(A + 1, B)) [ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 ] evalSequentialSinglebb5in(A, B) -> Com_1(evalSequentialSinglebb4in(A, B)) [ A >= 0 /\ B >= A + 1 ] evalSequentialSinglebb5in(A, B) -> Com_1(evalSequentialSinglereturnin(A, B)) [ A >= 0 /\ A >= B ] evalSequentialSinglebb4in(A, B) -> Com_1(evalSequentialSinglebb5in(A + 1, B)) [ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 ] evalSequentialSinglereturnin(A, B) -> Com_1(evalSequentialSinglestop(A, B)) [ A - B >= 0 /\ A >= 0 ] )