(meta-info (comment "Ctrl example from examples-transformed/sum2.ctrs"))
(format LCTRS :logic QF_LIA)
(fun u1 3 :sort (Int Int Int Int))
(fun u2 4 :sort (Int Int Int Int Int))
(fun sum2 1 :sort (Int Int))
(fun sum 1 :sort (Int Int))

(rule (u1 x i z) z :guard (not (<= i x)))
(rule (u2 x i j z) (u1 x (+ i 1) z) :guard (not (< j i)))
(rule (u2 x i j z) (u2 x i (+ j 1) (+ z 1)) :guard (< j i))
(rule (u1 x i z) (u2 x i 0 z) :guard (<= i x))
(rule (sum2 x) (u1 x 0 0))
(rule (sum x) (+ x (sum (- x 1))) :guard (< 0 x))
(rule (sum x) 0 :guard (<= x 0))