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