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