(meta-info (comment "Ctrl example from examples-transformed/student/fib08.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 a b c d) (return d) :guard (not (<= c n)) :vars ((n Int) (a Int) (b Int) (c Int) (d Int)))
(rule (v n a b c d) (v n b (+ a b) (+ c 1) (+ a b)) :guard (<= c n) :vars ((n Int) (a Int) (b Int) (c Int) (d Int)))
(rule (u n a b c d) (v n a b 2 d) :guard (and (not (< n 0)) (not (= n 1))) :vars ((n Int) (a Int) (b Int) (c Int) (d Int)))
(rule (u n a b c d) (return 1) :guard (and (not (< n 0)) (= n 1)) :vars ((n Int) (a Int) (b Int) (c Int) (d Int)))
(rule (u n a b c d) (return 0) :guard (< n 0) :vars ((n Int) (a Int) (b Int) (c Int) (d Int)))
(rule (fastfib n) (u n 0 1 rnd3 rnd4) :vars ((n Int) (rnd3 Int) (rnd4 Int)))