diff options
Diffstat (limited to 'proofs/signatures/th_bv.plf')
| -rw-r--r-- | proofs/signatures/th_bv.plf | 14 |
1 files changed, 0 insertions, 14 deletions
diff --git a/proofs/signatures/th_bv.plf b/proofs/signatures/th_bv.plf index 6012e052a..934951a86 100644 --- a/proofs/signatures/th_bv.plf +++ b/proofs/signatures/th_bv.plf @@ -3,20 +3,6 @@ (declare trust-bad (th_holds false)) ; helper stuff -(program mpz_sub ((x mpz) (y mpz)) mpz - (mp_add x (mp_mul (~1) y))) - -(program mp_ispos ((x mpz)) formula - (mp_ifneg x false true)) - -(program mpz_eq ((x mpz) (y mpz)) formula - (mp_ifzero (mpz_sub x y) true false)) - -(program mpz_lt ((x mpz) (y mpz)) formula - (mp_ifneg (mpz_sub x y) true false)) - -(program mpz_lte ((x mpz) (y mpz)) formula - (mp_ifneg (mpz_sub x y) true (mpz_eq x y))) (program mpz_ ((x mpz) (y mpz)) formula (mp_ifzero (mpz_sub x y) true false)) |