(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (VAR A B) (RULES f0(A, B) -> Com_1(f1(A, B)) [ A >= 1 /\ 0 >= B + 1 ] f1(A, B) -> Com_1(f1(A - B, B)) [ -B - 1 >= 0 /\ A - B - 2 >= 0 /\ A - 1 >= 0 /\ A >= B + 1 /\ 0 >= B + 1 ] )