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