(format LCTRS :logic QF_LIA) (fun start 0 :sort (Int)) (fun f 1 :sort (Int Int)) (fun g 1 :sort (Int Int)) (fun h 1 :sort (Int Int)) (rule start (g (f input))) (rule (f x) x :guard (> x 0)) (rule (g x) (h x))