; @author Jonas Schöpf
; @doi 10.48550/arXiv.1601.03206
; Example 14
(format LCTRS :smtlib 2.6)
(theory Ints)

(fun sum (-> Int Int Int))

(rule (sum x y) 0 :guard (> x y))
(rule (sum x y) (+ x (sum (+ x 1) y)) :guard (<= x y))