; Depends On: th_smt.plf
(declare Real sort)

(define arithpred_Real (! x (term Real)
                       (! y (term Real)
                         formula)))

(declare >_Real arithpred_Real)
(declare >=_Real arithpred_Real)
(declare <_Real  arithpred_Real)
(declare <=_Real arithpred_Real)

(define arithterm_Real (! x (term Real)
                       (! y (term Real)
                         (term Real))))

(declare +_Real arithterm_Real)
(declare -_Real arithterm_Real)
(declare *_Real arithterm_Real)  ; is * ok to use?
(declare /_Real arithterm_Real)  ; is / ok to use?

; a constant term
(declare a_real (! x mpq (term Real)))

(declare >=0_Real (! x (term Real) formula))
(declare =0_Real (! x (term Real) formula))
(declare >0_Real (! x (term Real) formula))
(declare distinct0_Real (! x (term Real) formula))

; unary negation
(declare u-_Real (! t (term Real) (term Real)))