; @author Jonas Schöpf
; @author Aart Middeldorp
; @doi 10.1007/978-3-031-38499-8_27
; Example 11
(format LCTRS :smtlib 2.6)
(theory Ints)

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

(rule (f x y) (g a (+ y y)) :guard (and (>= y x) (= y 1)))
(rule (h (f x y)) (h (g b 2)) :guard (>= x y))
(rule a b)
(rule (g x y) (g y x))