(meta-info (comment "Ctrl example from examples-transformed/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))
(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))
