; @author Jonas Schöpf
; Ctrl example from examples/sumsum.ctrs
(format LCTRS :smtlib 2.6)
(theory Ints)
(fun plus (-> Int Int Int))
(fun u0 (-> Int Int Int Int Int))
(fun u1 (-> Int Int Int Int Int))
(fun sumsum1 (-> Int Int))
(fun sumsum (-> Int Int))
(fun sum (-> 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))