; @author Jonas Schöpf
; @doi 10.1007/978-3-319-12736-1_18
; Example 7 (right LCTRS)
(format LCTRS :smtlib 2.6)
(theory Ints)

(fun fact (-> Int Int))
(fun u2 (-> Int Int Int Int))
(fun return (-> Int Int))

(rule (fact x) (u2 x 1 1))
(rule (u2 x i z) (u2 x (+ i 1) (* z i)) :guard (<= i x))
(rule (u2 x i z) (return z) :guard (> i x))