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

(fun double (-> Int Int))
(fun u (-> Int Int Int Int))
(fun sucsuc (-> Int Int))

(rule (double n) (u n 1 0))
(rule (u n  i  z) (u n (+ i 1) (sucsuc z)) :guard (<= i n))
(rule (u n  i  z) z :guard (not (<= i n)))
(rule (sucsuc x) (+ x 2))