; @author Jonas Schöpf
; Ctrl example from examples/llreve/llreve_rec_cocome1a.ctrs
(format LCTRS :smtlib 2.6)
(theory Ints)
(fun u_23 (-> Int Int))
(fun g2 (-> Int Int Int))
(fun u_16 (-> Int Int))
(fun triangle2 (-> Int Int))

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