Re: If A=B & (A contains C), why mizar doesn't infer (B contains C)

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

The way you have defined predicate 'contains' (strange name for what you
write in the definiens) it has three arguments and from the fact that
two of them are equal we cannnot infer what you want as with a 
different definiens it may be not true.

PR

On Wed, Jun 20, 2001 at 02:01:51PM +0800, Chen, Jing Chao (Jing Chao) wrote:
> Recently, I found that the proof of a very simple proposition cannot be
> accpted by Mizar.
> For example
> definition
>  let f, tm be set, t be Subset of tm;
>  pred t contains f means
>       t c= f;
> end;
> 
>  for f, tm1 be set, t1 be Subset of tm1,
>  tm2 be set, t2 be Subset of tm2 st
>     t1 contains f & t1=t2 holds t2 contains f;
> ::>                 *4
> This proposition can be simplified into 
>    A=B & (A contains C)  => B contains C.
> Clearly, it is ture. However, Mizar presented error 4.
> What deduction mechanism doesn't allow such an inference ?
> 
> Jingchao Chen

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

I am a fundamentalist: always fun before mental.