[isabelle] Counterexamples produced by arith method
- To: isabelle-users at cl.cam.ac.uk
- Subject: [isabelle] Counterexamples produced by arith method
- From: Peter <views at gmx.de>
- Date: Sat, 12 Nov 2005 14:04:58 +0100
- User-agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.7.12) Gecko/20051007 Debian/1.7.12-1
lemma "a~=0 ==> (a*a) div a <= (a::nat)"
a * a div a = 2, a = 1
What has gone wrong there ?
Why do I get a counterexample that is none ?
This archive was generated by a fusion of
Pipermail (Mailman edition) and