(meta-info (comment "Ctrl example from examples-transformed/sum_decl.ctrs"))
(format LCTRS :logic QF_LIA)
(fun sum3 2 :sort (Int Int Int))
(fun u_3 2 :sort (Int Int Int))
(fun sum_decl 1 :sort (Int Int))
(fun sum 1 :sort (Int Int))

(rule (sum3 x n) (+ n (sum3 x (+ n 1))) :guard (>= x n))
(rule (sum3 x n) 0 :guard (< x n))
(rule (u_3 z i) z :guard (<= i 0))
(rule (u_3 z i) (u_3 (+ z i) (- i 1)) :guard (> i 0))
(rule (sum_decl x) (u_3 0 x))
(rule (sum x) (+ x (sum (- x 1))) :guard (<= 0 (- x 1)))
(rule (sum x) 0 :guard (<= x 0))