(format LCTRS :logic QF_LIA)

(fun double 1 :sort (Int Int))

(rule (double x) 0 :guard (<= x 0))
(rule (double x) (+ 2 (double (- x 1))) :guard (> x 0))