; @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) :var ((n Int) (w_4 Int)))
(rule (g1 n) (u_9 n (g1 (- n 1))) :guard (> n 0) :var ((n Int)))
(rule (g1 n) 0 :guard (<= n 0) :var ((n Int)))
(rule (u_2 w_2) w_2 :var ((w_2 Int)))
(rule (triangle1 n) (u_2 (g1 n)) :var ((n Int)))