(meta-info (comment "Example 7 (right LCTRS) from Kop et al. 2014"))
(format LCTRS :logic QF_LIA)

(fun fact 1 :sort (Int Int))
(fun u2 3 :sort (Int Int Int Int))
(fun return 1 :sort (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))