(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS evalgcdstart)) (VAR A B) (RULES evalgcdstart(A, B) -> Com_1(evalgcdentryin(A, B)) evalgcdentryin(A, B) -> Com_1(evalgcdreturnin(A, B)) [ 0 >= A ] evalgcdentryin(A, B) -> Com_1(evalgcdreturnin(A, B)) [ 0 >= B ] evalgcdentryin(A, B) -> Com_1(evalgcdbb7in(B, A)) [ A >= 1 /\ B >= 1 ] evalgcdbb7in(A, B) -> Com_1(evalgcdbb4in(A, B)) [ A >= B + 1 ] evalgcdbb7in(A, B) -> Com_1(evalgcdbb4in(A, B)) [ B >= A + 1 ] evalgcdbb7in(A, B) -> Com_1(evalgcdreturnin(A, B)) [ B = A ] evalgcdbb4in(A, B) -> Com_1(evalgcdbb5in(A, B)) [ A >= B + 1 ] evalgcdbb4in(A, B) -> Com_1(evalgcdbb6in(A, B)) [ B >= A ] evalgcdbb5in(A, B) -> Com_1(evalgcdbb7in(A - B, B)) [ A - B - 1 >= 0 ] evalgcdbb6in(A, B) -> Com_1(evalgcdbb7in(A, B - A)) [ -A + B >= 0 ] evalgcdreturnin(A, B) -> Com_1(evalgcdstop(A, B)) )