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

(rule (g x) (g x))
(rule (v x i p q z) p :guard (>= i x))
(rule (v x i p q z) (v x (+ i 1) (+ p q) p z) :guard (< i x))
(rule (u x i p q z) (v x i p q (g 0)) :guard (> x 1))
(rule (u x i p q z) 1 :guard (= x 1))
(rule (u x i p q z) 0 :guard (<= x 0))
(rule (fastfib x) (u x 0 1 0 0))