(format LCTRS :logic QF_LIA)

(fun double 1 :sort (Int Int))
(fun u 3 :sort (Int Int Int Int))
(fun sucsuc 1 :sort (Int Int))

(rule (double n) (u n 1 0))
(rule (u n  i  z) (u n (+ i 1) (sucsuc z)) :guard (<= i n))
(rule (u n  i  z) z :guard (not (<= i n)))
(rule (sucsuc x) (+ x 2))