[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] A puzzle
On Thu, Jan 03, 2002 at 02:03:20PM +0100, Andrzej Trybulec wrote:
> In a new submitted article - AFINSQ_1 (The Authors:Tsunetou, Bancerek,
> Nakamura) the theorem Th2 says
>
> theorem Th2:
> k <= n implies k = k /\ n
>
> the next theorem has a straightforward justification:
>
> theorem
> k = k /\ n implies k <= n by Th2;
>
> ("/\" is the new notation for the intersection of sets, and the von
> Neuman construction is used in MML, so both are true)
>
> Mizar does not allow, as a rule, to justify "alpha implies beta" by
> "beta implies alpha" :-)
>
> Why it works in this case?
One explanation is that the following facts are obvious to the checker:
k > n implies k <> n;
k > n implies k >= n;
and intersection is commutative.
--
Piotr Rudnicki CompSci, Univerity of Alberta, Edmonton, Canada
email: piotr@cs.ualberta.ca http://web.cs.ualberta.ca/~piotr