Re: [isabelle] arith on large modulus



It appears there is a bug. Which is not so easy do diagnose :-(

Tobias

John Matthews schrieb:
Hi,

I would like to automatically prove the following lemma:

lemma
   "[|\<not> 100 < nat (x); 0 \<le> x|]
    ==> nat x + 11 = nat ((x + 11) mod 4294967296)"

I thought this fell within the fragment that arith can handle, but it can't seem to prove it. I know how to prove this manually, but is there something else I can use to prove it in a single command?

Thanks,
-john






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