(meta-info (comment "Ctrl example from examples-transformed/student/fib10.ctrs"))
(format LCTRS :logic QF_LIA)
(fun v 5 :sort (Int Int Int Int Int Unit))
(fun return 1 :sort (Int Unit))
(fun u 5 :sort (Int Int Int Int Int Unit))
(fun fastfib 1 :sort (Int Unit))

(rule (v n fi fp fn i) (return fi) :guard (not (< i n)) :vars ((n Int) (fi Int) (fp Int) (fn Int) (i Int)))
(rule (v n fi fp fn i) (v n (+ fi fp) fi (+ fi fp) (+ i 1)) :guard (< i n) :vars ((n Int) (fi Int) (fp Int) (fn Int) (i Int)))
(rule (u n fi fp fn i) (v n fi fp fn 1) :guard (not (<= n 0)) :vars ((n Int) (fi Int) (fp Int) (fn Int) (i Int)))
(rule (u n fi fp fn i) (return 0) :guard (<= n 0) :vars ((n Int) (fi Int) (fp Int) (fn Int) (i Int)))
(rule (fastfib n) (u n 1 0 rnd1 rnd2) :vars ((n Int) (rnd1 Int) (rnd2 Int)))