(meta-info (comment "Ctrl example from examples-transformed/sumsum.ctrs"))
(format LCTRS :logic QF_LIA)
(fun plus 2 :sort (Int Int Int))
(fun u0 4 :sort (Int Int Int Int Int))
(fun u1 4 :sort (Int Int Int Int Int))
(fun sumsum1 1 :sort (Int Int))
(fun sumsum 1 :sort (Int Int))
(fun sum 1 :sort (Int Int))

(rule (plus x y) (+ x y))
(rule (u0 x i j z) (u1 x i 0 z) :guard (>= x i))
(rule (u0 x i j z) z :guard (not (>= x i)))
(rule (u1 x i j z) (u1 x i (+ j 1) (+ z j)) :guard (>= i j))
(rule (u1 x i j z) (u0 x (+ i 1) j z) :guard (not (>= i j)))
(rule (sumsum1 x) (u0 x 0 0 0))
(rule (sumsum x) 0 :guard (<= x 0))
(rule (sumsum x) (plus (sumsum (- x 1)) (sum x)) :guard (>= (- x 1) 0))
(rule (sum x) (plus (sum (- x 1)) x) :guard (>= (- x 1) 0))
(rule (sum x) 0 :guard (<= x 0))