; @author Jonas Schöpf
; @doi 10.1007/978-3-642-40885-4_24
; Example 3
(format LCTRS :smtlib 2.6)
(theory Ints)
(fun sum (-> Int Int))
(fun sum2 (-> Bool Int Int))
(fun geq (-> Int Int Bool))
(fun plus (-> 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))