YES (format LCTRS :logic QF_LIA) (fun proc_G 1 :sort (Int result_proc)) (fun return_proc 1 :sort (Int result_proc)) (fun v 2 :sort (Int result_proc result_proc)) (rule (v n_0 (return_proc m_1)) (return_proc (+ n_0 m_1)) :vars ((n_0 Int) (m_1 Int))) (rule (proc_G n_2) (v n_2 (proc_G (- n_2 1))) :guard (> n_2 1) :vars ((n_2 Int))) (rule (proc_G n_3) (return_proc n_3) :guard (<= n_3 1) :vars ((n_3 Int))) Confluent by Parallel Closedness with proof: no critical pairs Elapsed Time: 14.14 ms