Re: reductions in Mizar

On Wed, 25 Jan 2012, [email protected] wrote:

>>> 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".


"correctness" can be used instead of "coherence", "compatibility", 
"reducibility", etc.

Artur