; @author Jonas Schöpf
; @doi 10.4230/LIPIcs.FSCD.2018.30
; Example 23 (modified and corrected)
(format LCTRS :smtlib 2.6)
(theory Ints)

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

(rule (f x y) (+ (f z y) 1) :guard (and (>= x 1) (= z (- x 1))))
(rule (g 0 y) y :guard (<= x 0))
(rule (f x 0) (g 1 x) :guard (<= x 1))
(rule (g 1 1) (+ (g 1 0) 1))
(rule (h x) (+ (g 1 x) 1) :guard (<= x 1))
(rule (h x) (+ (+ (f z 0) 1) 1) :guard (and (> x 1) (= z (- x 1))))