; @author Jonas Schöpf
; Ctrl example from examples/quad.ctrs
(format LCTRS :smtlib 2.6)
(theory Ints)
(fun quad (-> Int Int))
(fun twice (-> Int Int))
(fun u (-> Int Int Int Int))

(rule (quad x) (+ (twice x) (twice x)))
(rule (u x i z) z :guard (not (< i x)))
(rule (u x i z) (u x (+ i 1) (+ z 2)) :guard (< i x))
(rule (twice x) (u x 0 0))