; @author Jonas Schöpf
; @doi 10.1007/978-3-030-68446-4_2
; Example 1
(format LCTRS :smtlib 2.6)
(theory Ints)

(fun init (-> Int Int Int Int))
(fun m0 (-> Int Int Int Int))
(fun m1 (-> Int Int Int Int))
(fun m2 (-> Int Int Int Int))
(fun m3 (-> Int Int Int Int))
(fun m (-> Int Int Int Int))
(fun split (-> Int Int Int Int))
(fun merge (-> Int Int Int Int))
(fun tuple (-> Int Int Int Int Int))

(rule (init x y z) (m x y z))
(rule (m1 x y z) (m y y z))
(rule (m0 x y z) (split x y z))
(rule (m2 x y z) (m z y z))
(rule (m3 x y z) (merge y z z))
(rule (merge x y z) (merge (- x 1) y z) :guard (and (>= x 1) (>= y 1)))
(rule (split x y z) (split (- x 2) y z) :guard (>= x 2))
(rule (merge x y z) (merge x (- y 1) z) :guard (and (>= x 1) (>= y 1)))
(rule (m x y z) (tuple (m0 x u v) (m1 x u v) (m2 x u v) (m3 x u v)) :guard (and (>= x 2) (and (>= u 0) (and (>= v 0) (and (>= (+ x 1) (* 2 u)) (and (>= (* 2 u) x) (and (>= x (* 2 v)) (>= (+ (* 2 v) 1) x))))))))