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

(theory Ints)

(fun u_9 (-> Int Int Int))
(fun g1 (-> Int Int))
(fun u_2 (-> Int Int))
(fun triangle1 (-> Int Int))

(rule (u_9 n w_4) (+ n w_4))
(rule (g1 n) (u_9 n (g1 (- n 1))) :guard (> n 0))
(rule (g1 n) 0 :guard (<= n 0))
(rule (u_2 w_2) w_2)
(rule (triangle1 n) (u_2 (g1 n)))