Re: [isabelle] Modular arithmetic theory?
-An attempt to decide a challenge problem
"(x div y) * y + (x mod y) = x"
(div, mod, + * all 2's complement operations,
such a property is required for the integers
in the Java Language Specification)
with an up-to-date wordlevel-BDD package
was only feasible for a bit-length of 5 (!).
why don't you use mod_div_equality (on nat) or zdiv_zmod_equality (on
Any way, presburger solves the problem above in 0.02 seconds.
This archive was generated by a fusion of
Pipermail (Mailman edition) and