(meta-info (comment "Example 3 from Kop et al. 2013"))
(format LCTRS :logic QF_LIA)
(fun sum 1 :sort (Int Int))
(fun sum2 2 :sort (Bool Int Int))
(fun geq 2 :sort (Int Int Bool))
(fun plus 2 :sort (Int Int Int))

(rule (sum x) (sum2 (geq 0 x) x))
(rule (sum2 true x) 0)
(rule (sum2 false x) (plus x (sum (plus x (- 1)))))
(rule (plus n m) k :guard (= (+ n m) k))
(rule (geq n m) true :guard (>= n m))
(rule (geq n m) false :guard (< n m))