diff options
author | PaulMeng <baolmeng@gmail.com> | 2016-04-20 14:43:18 -0500 |
---|---|---|
committer | PaulMeng <baolmeng@gmail.com> | 2016-04-20 14:43:18 -0500 |
commit | 904ffb6e73402bae537aa89e7fd8f0ab2e9d60e2 (patch) | |
tree | d96bb0c974bdea6170957d3e39d47a98f5c85ca0 /proofs/signatures/th_real.plf | |
parent | a0054e9cc78822416d745e955c30f69cbb2a3aa7 (diff) |
update from the master
Diffstat (limited to 'proofs/signatures/th_real.plf')
-rw-r--r-- | proofs/signatures/th_real.plf | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/proofs/signatures/th_real.plf b/proofs/signatures/th_real.plf new file mode 100644 index 000000000..3478e23ef --- /dev/null +++ b/proofs/signatures/th_real.plf @@ -0,0 +1,25 @@ +(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))) + +; unary negation +(declare u-_Real (! t (term Real) (term Real))) |