Re: [mizar] Was this supposed to be so?

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

> Piotr Rudnicki wrote:
> > 
> > Hi:
> > 
> > I appreciate Grzegorz's, as always deep and careful, explanation but
> > I expected an error that the skeleton of the proof disagrees with the
> > thesis.
> > 
> > On Tue, Aug 20, 2002 at 02:07:53PM -0600, Piotr Rudnicki wrote:
> > >
> > > I have expected an error in the following
> > >
> > >       for X, Y, Z being set st X = Y holds Y = X
> > >       proof let X, Y be set;
> > >         thus thesis;
> > >       end;
> > >
> > > but did not get any.  Such theorem would look pretty silly in an abstract.
> 
> My first thought was missing "let Z" in proof skeleton. I observe
> sometimes
> that my students write generalization steps ("let") for each variable
> but, of course, it is not necessary.  In your case thesis is
>   for Z being set st X = Y holds Y = X

I have missed it.

-- 
Piotr Rudnicki              CompSci, University of Alberta, Edmonton, Canada
email: piotr@cs.ualberta.ca                 http://web.cs.ualberta.ca/~piotr