(meta-info (comment "Ctrl example from examples-transformed/llreve/llreve_rec_cocome1a.ctrs"))
(format LCTRS :logic QF_LIA)
(fun u_9 2 :sort (Int Int Int))
(fun g1 1 :sort (Int Int))
(fun u_2 1 :sort (Int Int))
(fun triangle1 1 :sort (Int Int))

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