Re: [mizar] reductions in Mizar

[trybulec@math.uwb.edu.pl]

Hi:

I am for. If I recall originally "compatibility" was proposed. On the seminar
"reducibility" get stronger support. Mostly of Artur. And because he 
implemented it ...

Regards,
Andrzej


Cytowanie Josef Urban <josef.urban@gmail.com>:

> Hi All,
>
> > registration
> >    let x_1,...,x_n;
> >    reduce term1(x_1,...,x_n) to term2(x_1,...,x_n);
> >    reducibility
> >    proof
> >      thus term1(x_1,...,x_n) = term2(x_1,...,x_n);
> >    end;
> > end;
>
> I never remember the "correctness condition" keywords (coherence,
> compatibility, etc) used in different contexts. I just looked up the
> keyword used for "identify", and it is "compatibility".
>
> Should not there be some unification of these keywords? It seems that
> "reducibility" now proves the same thing for "reduce" as
> "compatibility" does for "identify".
>
> Josef