YES
LCTRS
  Theories
    Core, Ints
  Sorts
    result_proc
  Signature
    proc_G: Int -> result_proc
    return_proc: Int -> result_proc
    v: (Int, result_proc) -> result_proc
  Rules
    proc_G(?11) -> return_proc(?11) [<=(?11, 1)]
    proc_G(?12) -> v(?12, proc_G(-(?12, 1))) [>(?12, 1)]
    v(?13, return_proc(?14)) -> return_proc(+(?13, ?14))
Confluent by Orthogonality with proof:
  no critical pairs

Elapsed Time:  43.59 ms