Re: [mizar] The 'suppose' keyword

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

Hi Boris,

I have never used 'case' in 'per cases' ;-)  and since nobody has replied so far ...

If memory serves: 'suppose' and 'case' are not synonyms.  With 'suppose' you have to prove the same 'thing' in each case.  With 'case' in 'per cases', each 'case' contributes an implication to the thing being proved.   Hope this helps (assuming that I remember it right.)

Cheers, PR

On Fri, Apr 23, 2010 at 4:33 AM, Boris Schminke <schminkeba@gmail.com> wrote:

Dear All,
the 'suppose' keyword is not described in 'Mizar Lecture Notes',  but
it seems to be synonymic to the 'case' keyword in the 'per cases'
proof structure. Am I right?
Excuse me if the description could be found in another manual,
actually I haven't searched anywhere else, because in other parts
'Mizar Lecture Notes' seem to be the most up-to-date of what is
available.
Best regards,
Schminke Boris.

-- 
Piotr Rudnicki
http://www.cs.ualberta.ca/~piotr