; @author Jonas Schöpf
; @author Aart Middeldorp
; @doi 10.48550/arXiv.2501.05240
; example 8
(format LCTRS)
(theory Ints)

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

(rule (f x) 2 :guard (and (<= 1 x) (<= x 3)))
(rule (f x) (g x) :guard (and (<= 2 x) (<= x 4)))
(rule (g x) (h x))
(rule (h x) y :guard (and (= x 2) (= y x)))
(rule (h x) y :guard (and (= x 3) (= y 2)))