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

(theory Ints)

(fun f (-> Int Int))

(rule (f x) (f (- 0 x)) :guard (> x 0))