; @author Jonas Schöpf
; Ctrl example from examples/eval.ctrs
(format LCTRS :smtlib 2.6)
(theory Ints)

(sort Unit)
(fun eval1 (-> Int Int  Unit))
(fun eval2 (-> Int Int  Unit))
(fun eval3 (-> 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)))