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