; @author Jonas Schöpf
; @doi 10.1007/978-3-642-40885-4_24
; Example 12
(format LCTRS :smtlib 2.6)
(theory Reals)

(fun sumroot (-> Real Real))
(fun sqrt (-> Real Real))

(rule (sumroot x) 0.0 :guard (>= 0.0 x))
(rule (sumroot x) (+ (sqrt x) (sumroot  (- x 1.0))) :guard (not (>= 0.0 x)))