Re: The 'suppose' keyword
Piotr Rudnicki <[email protected]>
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <[email protected]> |
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 <[email protected]>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