(meta-info (comment "Ctrl example from examples-transformed/recurse.ctrs"))
(format LCTRS :logic QF_LIA)

(fun return_proc 1 :sort (Int result_proc))
(fun u 2 :sort (Int result_proc result_proc))
(fun proc_F 1 :sort (Int result_proc))

(rule (u n (return_proc m)) (return_proc (+ n m)))
(rule (proc_F n) (u n (proc_F (- n 1))) :guard (> n 0))
(rule (proc_F n) (return_proc n) :guard (<= n 0))