; @author Jonas Schöpf
; @doi 10.1007/978-3-642-40885-4_24
; Example 15
(format LCTRS :smtlib 2.6)
(theory Ints)

(fun eval1 (-> Int Int Int))
(fun eval2 (-> Int Int Int))
(fun eval3 (-> Int Int Int))

(rule (eval1 x y) (eval2 x y) :guard (and (and (> x 0) (> y 0)) (> x y)))
(rule (eval1 x y) (eval3 x y) :guard (and (and (> x 0) (> y 0)) (not (> x y))))
(rule (eval2 x y) (eval2 (+ x -1) (+ y 1)) :guard (> x 0))
(rule (eval2 x y) (eval1 x y) :guard (not (> x 0)))
(rule (eval3 x y) (eval3 (+ x 1) (+ y -1)) :guard (> y 0))
(rule (eval3 x y) (eval1 x y) :guard (not (> y 0)))