(meta-info (comment "Ctrl example from examples-transformed/student/fib06.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 i fb p q) (return fb) :guard (not (<= i n)) :vars ((n Int) (i Int) (fb Int) (p Int) (q Int)))
(rule (v n i fb p q) (v n (+ i 1) (+ p q) (+ p q) p) :guard (<= i n) :vars ((n Int) (i Int) (fb Int) (p Int) (q Int)))
(rule (u n i fb p q) (v n 2 fb p q) :guard (and (not (< n 1)) (not (= n 1))) :vars ((n Int) (i Int) (fb Int) (p Int) (q Int)))
(rule (u n i fb p q) (return 1) :guard (and (not (< n 1)) (= n 1)) :vars ((n Int) (i Int) (fb Int) (p Int) (q Int)))
(rule (u n i fb p q) (return 0) :guard (< n 1) :vars ((n Int) (i Int) (fb Int) (p Int) (q Int)))
(rule (fastfib n) (u n rnd1 rnd2 1 0) :vars ((n Int) (rnd1 Int) (rnd2 Int)))