(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)
(declare /_Real arithterm_Real)
; a constant term
(declare a_real (! x mpq (term Real)))
; unary negation ?
(declare u-_Real (! t (term Real) (term Real)))
;; normalization to >=, >
(declare <_to_>_Real
(! x (term Real)
(! y (term Real)
(! u (th_holds (<_Real x y))
(th_holds (>_Real y x))))))
(declare <=_to_>=_Real
(! x (term Real)
(! y (term Real)
(! u (th_holds (<=_Real x y))
(th_holds (>=_Real y x))))))
(declare not_<_to_>=_Real
(! x (term Real)
(! y (term Real)
(! u (th_holds (not (<_Real x y)))
(th_holds (>=_Real x y))))))
(declare not_<=_to_>_Real
(! x (term Real)
(! y (term Real)
(! u (th_holds (not (<=_Real x y)))
(th_holds (>_Real x y))))))
(declare not_>_to_>=_Real
(! x (term Real)
(! y (term Real)
(! u (th_holds (not (>_Real x y)))
(th_holds (>=_Real y x))))))
(declare not_>=_to_>_Real
(! x (term Real)
(! y (term Real)
(! u (th_holds (not (>=_Real x y)))
(th_holds (>_Real y x))))))
;; transitivity for >=, >
(declare trans_>=_>=_Real
(! x (term Real)
(! y (term Real)
(! z (term Real)
(! u1 (th_holds (>=_Real x y))
(! u2 (th_holds (>=_Real y z))
(th_holds (>=_Real x z))))))))
(declare trans_>=_>_Real
(! x (term Real)
(! y (term Real)
(! z (term Real)
(! u1 (th_holds (>=_Real x y))
(! u2 (th_holds (>_Real y z))
(th_holds (>_Real x z))))))))
(declare trans_>_>=_Real
(! x (term Real)
(! y (term Real)
(! z (term Real)
(! u1 (th_holds (>_Real x y))
(! u2 (th_holds (>=_Real y z))
(th_holds (>_Real x z))))))))
(declare trans_>_>_Real
(! x (term Real)
(! y (term Real)
(! z (term Real)
(! u1 (th_holds (>_Real x y))
(! u2 (th_holds (>_Real y z))
(th_holds (>_Real x z))))))))
; predicate with 0 assumed for the RHS
(define arithpred0_Real (! x (term Real)
formula))
(declare >0_Real arithpred0_Real)
(declare >=0_Real arithpred0_Real)
(declare <0_Real arithpred0_Real)
(declare <=0_Real arithpred0_Real)
(declare =0_Real arithpred0_Real)
(declare distinct0_Real arithpred0_Real)
;; conversion between arithpred0_Real and arithpred_Real
(declare norm_>_Real
(! x (term Real)
(! y (term Real)
(! t (th_holds (>_Real x y))
(th_holds (>0_Real (-_Real x y)))))))
(declare norm_>=_Real
(! x (term Real)
(! y (term Real)
(! t (th_holds (>=_Real x y))
(th_holds (>=0_Real (-_Real x y)))))))
(declare norm_<_Real
(! x (term Real)
(! y (term Real)
(! t (th_holds (<_Real x y))
(th_holds (<0_Real (-_Real x y)))))))
(declare norm_<=_Real
(! x (term Real)
(! y (term Real)
(! t (th_holds (<=_Real x y))
(th_holds (<=0_Real (-_Real x y)))))))
(declare norm_=_Real
(! x (term Real)
(! y (term Real)
(! t (th_holds (= Real x y))
(th_holds (=0_Real (-_Real x y)))))))
(declare norm_distinct_Real
(! x (term Real)
(! y (term Real)
(! t (th_holds (distinct Real x y))
(th_holds (distinct0_Real (-_Real x y)))))))
;; weaken to non-strict inequality
(declare >0_to_>=0_Real
(! x (term Real)
(! u (th_holds (>0_Real x))
(th_holds (>=0_Real x)))))