; @author Jonas Schöpf
; Ctrl example from examples/llreve/llreve_rec_limit1unrolleda.ctrs
(format LCTRS :smtlib 2.6)
(theory Ints)
(fun u_13 (-> Int Int Int Int))
(fun f1 (-> Int Int))

(rule (u_13 n nx w_4) (+ n (+ nx w_4)))
(rule (f1 n) (u_13 n (- n 1) (f1 (- (- n 1) 1))) :guard (and (> n 1) (> (- n 1) 1)))
(rule (f1 n) (+ n (- n 1)) :guard (and (> n 1) (<= (- n 1) 1)))
(rule (f1 n) n :guard (<= n 1))