*To*: Michael Norrish <Michael.Norrish at nicta.com.au>*Subject*: Re: [isabelle] Modular arithmetic theory?*From*: Amine Chaieb <chaieb at informatik.tu-muenchen.de>*Date*: Fri, 18 Nov 2005 07:30:40 +0100 (MET)*Cc*: Burkhart Wolff <bwolff at inf.ethz.ch>, isabelle-users at cl.cam.ac.uk, Hasan Amjad <ha227 at cam.ac.uk>*In-reply-to*: <17275.45584.259509.59952@raceme.rsise.anu.edu.au>*References*: <2F04C324-C280-4CE4-BA8A-894B0D332B51@galois.com> <17275.45584.259509.59952@raceme.rsise.anu.edu.au>

The problem with arith in the original problem lemma "(n mod 4294967296 + m mod 4294967296) mod 4294967296 = (m + n) mod 4294967296" by arith

Even with so-called "delta-elimination" enabled, I can't get comparable performance out of Cooper's algorithm, which is a shame.

I don't see why this is specific to cooper and not Omega test. Cheers, Amine

**Follow-Ups**:**Re: [isabelle] Modular arithmetic theory?***From:*Michael Norrish

**References**:**Re: [isabelle] Modular arithmetic theory?***From:*John Matthews

**Re: [isabelle] Modular arithmetic theory?***From:*Michael Norrish

- Previous by Date: [isabelle] JAR issue on Empirically Successful Automated Reasoning
- Next by Date: Re: [isabelle] Modular arithmetic theory?
- 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