Re: reductions in Mizar

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