; @author Jonas Schöpf
; Ctrl example from examples/recurse.ctrs
(format LCTRS :smtlib 2.6)

(theory Ints)

(sort result_proc)

(fun v (-> Int result_proc result_proc))
(fun return_proc (-> Int result_proc))
(fun proc_G (-> 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))