(meta-info (comment "Example 23 Winkler et al. 2018"))
(meta-info (comment "Modified and corrected example"))
(format LCTRS :logic QF_LIA)

(fun f 2 :sort (Int Int Int))
(fun g 2 :sort (Int Int Int))
(fun h 1 :sort (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))))