(meta-info (comment "Example 1 Winkler et al. 2021"))
(format LCTRS :logic QF_LIA)

(fun init 3 :sort (Int Int Int Int))
(fun m0 3 :sort (Int Int Int Int))
(fun m1 3 :sort (Int Int Int Int))
(fun m2 3 :sort (Int Int Int Int))
(fun m3 3 :sort (Int Int Int Int))
(fun m 3 :sort (Int Int Int Int))
(fun split 3 :sort (Int Int Int Int))
(fun merge 3 :sort (Int Int Int Int))
(fun tuple 4 :sort (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))))))))