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

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

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