; @author Jonas Schöpf
; Ctrl example from examples/fact.ctrs
(format LCTRS :smtlib 2.6)
(theory Ints)

(fun fact1 (-> Int  Int))
(fun u (-> Int Int Int  Int))
(rule (u  n i z) (u  n (+  i 1) (*  z i)) :guard (<= i n))
(rule (u  n i z) z :guard (not (<= i n)))
(rule (fact1  n) (u  n 1 1))