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_int.plf | |
parent | a0054e9cc78822416d745e955c30f69cbb2a3aa7 (diff) |
update from the master
Diffstat (limited to 'proofs/signatures/th_int.plf')
-rw-r--r-- | proofs/signatures/th_int.plf | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/proofs/signatures/th_int.plf b/proofs/signatures/th_int.plf new file mode 100644 index 000000000..9a0a2d63c --- /dev/null +++ b/proofs/signatures/th_int.plf @@ -0,0 +1,25 @@ +(declare Int sort) + +(define arithpred_Int (! x (term Int) + (! y (term Int) + formula))) + +(declare >_Int arithpred_Int) +(declare >=_Int arithpred_Int) +(declare <_Int arithpred_Int) +(declare <=_Int arithpred_Int) + +(define arithterm_Int (! x (term Int) + (! y (term Int) + (term Int)))) + +(declare +_Int arithterm_Int) +(declare -_Int arithterm_Int) +(declare *_Int arithterm_Int) ; is * ok to use? +(declare /_Int arithterm_Int) ; is / ok to use? + +; a constant term +(declare a_int (! x mpz (term Int))) + +; unary negation +(declare u-_Int (! t (term Int) (term Int))) |