; @author Jonas Schöpf
; Ctrl example from examples/nonterminate-simplify.ctrs
(format LCTRS :smtlib 2.6)

(theory Ints)

(fun g (-> Int Int))
(fun v (-> Int Int Int Int Int Int))
(fun u (-> Int Int Int Int Int Int))
(fun fastfib (-> 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) :var ((x Int)))
(rule (u x i p q z) 0 :guard (<= x 0))
(rule (fastfib x) (u x 0 1 0 0))