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