(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS start))
(VAR A)
(RULES
  start(A) -> Com_1(eval(A))
  eval(A) -> Com_1(eval(2*B)) [ 2*B >= 0 /\ A = 2*B + 1 ]
)