; @author Jonas Schöpf
; @author Fabian Mitterwallner
; @author Aart Middeldorp
; @doi 10.1007/978-3-031-63501-4_16
; Example 8
(format LCTRS :smtlib 2.6)

(theory Ints)

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

(rule (f a) (g 4 4))
(rule a (g (+ 1 1) (+ 3 1)))
(rule (g x y) (f (g z y)) :guard (= z (- x 2)) :var ((z Int)))