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