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

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