(meta-info (comment "Ctrl example from examples-transformed/student/fib04.ctrs"))
(format LCTRS :logic QF_LIA)
(fun w 5 :sort (Int Int Int Int Int Unit))
(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 (w n p1 p2 p i) (v n p p1 p (+ i 1)) :guard (not (< p p1)) :vars ((n Int) (p1 Int) (p2 Int) (p Int) (i Int)))
(rule (w n p1 p2 p i) (return -2) :guard (< p p1) :vars ((n Int) (p1 Int) (p2 Int) (p Int) (i Int)))
(rule (v n p1 p2 p i) (return p) :guard (not (< i n)) :vars ((n Int) (p1 Int) (p2 Int) (p Int) (i Int)))
(rule (v n p1 p2 p i) (w n p1 p2 (+ p1 p2) i) :guard (< i n) :vars ((n Int) (p1 Int) (p2 Int) (p Int) (i Int)))
(rule (u n p1 p2 p i) (v n p1 p2 p 1) :guard (and (and (not (< n 0)) (not (= n 0))) (not (= n 1))) :vars ((n Int) (p1 Int) (p2 Int) (p Int) (i Int)))
(rule (u n p1 p2 p i) (return 1) :guard (and (and (not (< n 0)) (not (= n 0))) (= n 1)) :vars ((n Int) (p1 Int) (p2 Int) (p Int) (i Int)))
(rule (u n p1 p2 p i) (return 0) :guard (and (not (< n 0)) (= n 0)) :vars ((n Int) (p1 Int) (p2 Int) (p Int) (i Int)))
(rule (u n p1 p2 p i) (return -1) :guard (< n 0) :vars ((n Int) (p1 Int) (p2 Int) (p Int) (i Int)))
(rule (fastfib x) (u x 1 0 rnd1 rnd2) :vars ((x Int) (rnd1 Int) (rnd2 Int)))