Re: [isabelle] arith on large modulus

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


John Matthews schrieb:

I would like to automatically prove the following 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?


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