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

(fun fib1 (-> Int  Int))
(fun fib (-> Int  Int))
(fun u (-> Int Int Int Int  Int))

(rule (fib  x) (+  (fib  (-  x 1)) (fib  (-  x 2))) :guard (>= (- x 2) 0))
(rule (fib  1) 1)
(rule (fib  x) 0 :guard (<= x 0))
(rule (u  x i y z) y :guard (not (>= x i)))
(rule (u  x i y z) (u  x (+  i 1) z (+  y z)) :guard (>= x i))
(rule (fib1  x) (u  x 1 0 1))