Add more IntReal predicates (#3731)

diff --git a/proofs/signatures/th_lira.plf b/proofs/signatures/th_lira.plf
index 145980b24489e53e58f08e2ae6a407834f2814cc..a5b73d6b4fb46c9a10908dcd6365f465c1298677 100644 (file)
--- a/proofs/signatures/th_lira.plf
+++ b/proofs/signatures/th_lira.plf
@@ -59,8 +59,14 @@
     ((/_Real x y) (/_Real (reify_real_term x) (reify_real_term y)))
   ))
 
-; Predicates of the form (term Integer) >= (term Real) or negations thereof
-(declare >=_IntReal (! x (term Int) (! y (term Real) formula)))
+; Predicates of the form (term Integer) (comparison) (term Real)
+(define arithpred_IntReal (! x (term Int)
+                          (! y (term Real)
+                          formula)))
+(declare >_IntReal arithpred_IntReal)
+(declare >=_IntReal arithpred_IntReal)
+(declare <_IntReal  arithpred_IntReal)
+(declare <=_IntReal arithpred_IntReal)
 
 ; From an arith predicate, compute the equivalent real predicate
 ; All arith predicates are (possibly negated) >='s with a real on the right.