(meta-info (comment "Ctrl example from examples-transformed/llreve/llreve_rec_cocome1a.ctrs"))
(format LCTRS :logic QF_LIA)
(fun u_23 1 :sort (Int Int))
(fun g2 2 :sort (Int Int Int))
(fun u_16 1 :sort (Int Int))
(fun triangle2 1 :sort (Int Int))

(rule (u_23 w_8) w_8 :vars ((w_8 Int)))
(rule (g2 n s) (u_23 (g2 (- n 1) (+ n s))) :guard (> n 0) :vars ((n Int) (s Int)))
(rule (g2 n s) s :guard (<= n 0) :vars ((n Int) (s Int)))
(rule (u_16 w_6) w_6 :vars ((w_6 Int)))
(rule (triangle2 n) (u_16 (g2 n 0)) :vars ((n Int)))