| Newsgroups |
gmane.comp.mathematics.mizar |
| Message-ID |
<[email protected]> |
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 <[email protected]>:
> 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
>