; @author Jonas Schöpf
; @doi 10.1007/978-3-642-40885-4_24
; Example 2
(format LCTRS :smtlib 2.6)
(theory Ints)
(fun sum (-> Int Int))
(fun sum2 (-> Bool Int Int))
(fun geq (-> Int Int Bool))
(fun s (-> Int Int))
(fun plus (-> Int Int Int))
(fun p (-> Int Int))
(fun geq2 (-> Int Int Int Int Bool))

(rule (sum x) (sum2 (geq 0 x) x))
(rule (sum2 true x) 0)
(rule (sum2 false (s x)) (plus (s x) (sum x)))
(rule (plus (p x) y) (p (plus x y)))
(rule (plus (s x) y) (s (plus x y)))
(rule (plus 0 y) y)
(rule (s (p x)) x)
(rule (p (s x)) x)
(rule (geq x y) (geq2 x y 0 0))
(rule (geq2 (s x) y z u) (geq2 x y (s z) u))
(rule (geq2 (p x) y z u) (geq2 x y z (s u)))
(rule (geq2 0 (s x) y z) (geq2 0 x y (s z)))
(rule (geq2 0 (p x) y z) (geq2 0 x (s y) z))
(rule (geq2 0 0 (s x) (s y)) (geq2 0 0 x y))
(rule (geq2 0 0 x 0) true)
(rule (geq2 0 0 0 (s x)) false)