; @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)
(rule (g2 n s) (u_23 (g2 (- n 1) (+ n s))) :guard (> n 0))
(rule (g2 n s) s :guard (<= n 0))
(rule (u_16 w_6) w_6)
(rule (triangle2 n) (u_16 (g2 n 0)))