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