; @author Jonas Schöpf
; @doi 10.4230/LIPIcs.FSCD.2018.30
; Example 19
(format LCTRS :smtlib 2.6)
(theory Ints)

(fun f (-> Int Int))
(fun g (-> Int Int Int))
(fun h (-> Int Int))

(rule (f x) (g x x) :guard (<= x 0))
(rule (h (f x)) (h x) :guard (>= x 0))
(rule (g (f x) y) (g x z) :guard (and (> x 0) (> z x)))
(rule (g x (+ x y)) (f y) :guard (and (> x 0) (> y 0)))