Re: [isabelle] A proof for existential



On Aug 5, 2010 1:10pm, Tjark Weber <webertj at in.tum.de> wrote:
On Thu, 2010-08-05 at 11:19 +0100, John Munroe wrote:

> Thanks for the reply. What if ax2 was ax2 :"ALL x. (ALL y. x ~= y -->

> hx > hy) --> gx = 0", would the lemma follow from ax1 and ax2 then?



Yes; see the attached Isabelle theory for an automatic proof.


Thanks. Just curious, without using metis, what would a manual proof look like?

John



Regards,

Tjark





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