(meta-info (comment "Ctrl example from examples-transformed/recurse.ctrs"))
(format LCTRS :logic QF_LIA)
(fun v 2 :sort (Int result_proc result_proc))
(fun return_proc 1 :sort (Int result_proc))
(fun proc_G 1 :sort (Int result_proc))

(rule (v n (return_proc m)) (return_proc (+ n m)))
(rule (proc_G n) (v n (proc_G (- n 1))) :guard (> n 1))
(rule (proc_G n) (return_proc n) :guard (<= n 1))