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

(theory Ints)

(sort Unit)

(fun fun7 (-> Int Int Unit))
(fun fun1 (-> Int Int Unit))
(fun fun6 (-> Int Int Unit))
(fun fun5 (-> Int Int Unit))
(fun fun4 (-> Int Int Unit))
(fun fun3 (-> Int Int Unit))
(fun fun2 (-> Int Int Int Unit))
(fun fun8 (-> Int Int Unit))

(rule (fun7 x y) (fun1 x y))
(rule (fun6 x y) (fun7 x (- y 1)))
(rule (fun5 x y) (fun7 x y))
(rule (fun4 x y) (fun5 x input))
(rule (fun3 x y) (fun4 (- x 1) y))
(rule (fun2 x y i) (fun6 x y) :guard (not (= i 1)) :var ((i Int)))
(rule (fun2 x y i) (fun3 x y) :guard (= i 1) :var ((i Int)))
(rule (fun1 x y) (fun8 x y) :guard (and (<= x 0) (<= y 0)))
(rule (fun1 x y) (fun2 x y input) :guard (and (> x 0) (> y 0)))