(meta-info (comment "Ctrl example from examples-transformed/eval.ctrs"))
(format LCTRS :logic QF_LIA)

(fun eval1 2 :sort (Int Int  Unit))
(fun eval2 2 :sort (Int Int  Unit))
(fun eval3 2 :sort (Int Int  Unit))

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