; @author Jonas Schöpf
; @author Fabian Mitterwallner
; @author Aart Middeldorp
; @doi 10.48550/arXiv.2402.13552
; Example 5
(format LCTRS :smtlib 2.6)

(theory Ints)

(sort Unit)

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

(rule (f x) (g x))
(rule (f x) (h x) :guard (and (<= 1 x) (>= x 2)))
(rule (g x) (h 2) :guard (= x (* 2 z)))
(rule (g x) (h 1) :guard (= x (+ (* 2 z) 1)))