*To*: Burkhart Wolff <bwolff at inf.ethz.ch>*Subject*: Re: [isabelle] Modular arithmetic theory?*From*: Amine Chaieb <chaieb at in.tum.de>*Date*: Fri, 18 Nov 2005 11:05:55 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <1131631775.5258.95.camel@localhost.localdomain>*References*: <1131631775.5258.95.camel@localhost.localdomain>

-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 (!).

Any way, presburger solves the problem above in 0.02 seconds. Amine

**Follow-Ups**:**Re: [isabelle] Modular arithmetic theory?***From:*Burkhart Wolff

**References**:**Re: [isabelle] Modular arithmetic theory?***From:*Burkhart Wolff

- Previous by Date: Re: [isabelle] Modular arithmetic theory?
- Next by Date: [isabelle] BCTCS 2006 - First Call for Participation
- Previous by Thread: Re: [isabelle] Modular arithmetic theory?
- Next by Thread: Re: [isabelle] Modular arithmetic theory?
- Cl-isabelle-users November 2005 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list