diff options
Diffstat (limited to 'proofs/signatures/th_real.plf')
| -rw-r--r-- | proofs/signatures/th_real.plf | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/proofs/signatures/th_real.plf b/proofs/signatures/th_real.plf index 3478e23ef..3529779f3 100644 --- a/proofs/signatures/th_real.plf +++ b/proofs/signatures/th_real.plf @@ -1,3 +1,4 @@ +; Depends On: th_smt.plf (declare Real sort) (define arithpred_Real (! x (term Real) @@ -21,5 +22,10 @@ ; 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))) |