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 int)?
Any way, presburger solves the problem above in 0.02 seconds.

Amine






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.