; @author Jonas Schöpf
; @author Aart Middeldorp
; example 9
(format LCTRS)
(theory Ints)

(sort Unit)

(fun f (-> Int Unit))
(fun g (-> Int Unit))
(fun h (-> Int Unit))
(fun a Unit)
(fun b Unit)
(fun c Unit)

(rule (f x) (g x) :guard (>= x 1))
(rule (f x) (h x) :guard (<= x 2))
(rule (g 1) a)
(rule (g x) b :guard (>= x 2))
(rule (g x) c :guard (< x 1))
(rule (h x) a :guard (<= x 1))
(rule (h x) b :guard (> x 1))