(meta-info (comment "Ctrl example from examples/fib.ctrs"))
(format LCTRS :logic QF_LIA)

(fun fib1 1 :sort (Int  Int))
(fun fib 1 :sort (Int  Int))
(fun u 4 :sort (Int Int Int Int  Int))

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