Re: [isabelle] A proof for existential

On Aug 5, 2010 1:10pm, Tjark Weber <webertj at> 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?




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