(meta-info (comment "Example 1 Kop Termination 2016 (without restriction to 16-bit Ints)"))
(format LCTRS :logic QF_LIA)

(fun sum 2 :sort (Int Int Int))

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