; @author Jonas Schöpf
; @doi 10.4230/LIPIcs.FSCD.2018.30
; Example 3
(format LCTRS :smtlib 2.6)
(theory Ints)

(fun fact (-> Int Int))

(rule (fact x) 1 :guard (<= x 0))
(rule (fact x) (* (fact (- x 1)) x) :guard (>= (- x 1) 0))